module UVMHS.Tests.Core (g__TESTS__UVMHS__Tests__Core) where

import UVMHS.Core
import UVMHS.Lib.Testing

𝔱 "core:iter" [| isEmpty []           |] [| True  |]
𝔱 "core:iter" [| isEmpty [𝕟 1]        |] [| False |]
𝔱 "core:iter" [| isEmpty Nil          |] [| True  |]
𝔱 "core:iter" [| isEmpty (𝕟 1 :& Nil) |] [| False |]

𝔱 "core:iter" [| list $ range (𝕟 0) (𝕟 0) |] [| list []        |]
𝔱 "core:iter" [| list $ range (𝕟 1) (𝕟 1) |] [| list []        |]
𝔱 "core:iter" [| list $ range (𝕟 0) (𝕟 1) |] [| list [𝕟 0]     |]
𝔱 "core:iter" [| list $ range (𝕟 0) (𝕟 2) |] [| list [𝕟 0,𝕟 1] |]
𝔱 "core:iter" [| list $ range (𝕟 1) (𝕟 3) |] [| list [𝕟 1,𝕟 2] |]

𝔱 "core:iter" [| list $ upto (𝕟 0) |] [| list []        |]
𝔱 "core:iter" [| list $ upto (𝕟 1) |] [| list [𝕟 0]     |]
𝔱 "core:iter" [| list $ upto (𝕟 2) |] [| list [𝕟 0,𝕟 1] |]

𝔱 "core:iter" [| list $ keepN (𝕟 0) [𝕟 0,𝕟 1] |] [| list []        |]
𝔱 "core:iter" [| list $ keepN (𝕟 1) [𝕟 0,𝕟 1] |] [| list [𝕟 0]     |]
𝔱 "core:iter" [| list $ keepN (𝕟 2) [𝕟 0,𝕟 1] |] [| list [𝕟 0,𝕟 1] |]
𝔱 "core:iter" [| list $ keepN (𝕟 3) [𝕟 0,𝕟 1] |] [| list [𝕟 0,𝕟 1] |]

𝔱 "core:iter" [| list $ replicate (𝕟 0) $ 𝕟 42 |] [| list [] |]
𝔱 "core:iter" [| list $ replicate (𝕟 2) $ 𝕟 42 |] [| list [𝕟 42,𝕟 42] |]

𝔱 "core:dict" [| dict𝐷 [𝕟 1 ↦♭ 𝕟 2,𝕟 1 ↦♭ 𝕟 3] |] [| dict𝐷 [𝕟 1 ↦♭ 𝕟 2] |]

𝔱 "core:lens" [| alter (keyL $ 𝕤 "x") (map (+ 𝕟 1)) ("x" ↦♭ 𝕟 1) |] [| "x" ↦♭ 𝕟 2 |]
𝔱 "core:lens" [| alter (keyL $ 𝕤 "x") (map (+ 𝕟 1)) ("y" ↦♭ 𝕟 1) |] [| "y" ↦♭ 𝕟 1 |]
𝔱 "core:lens" [| alter (keyL $ 𝕤 "x") (map (+ 𝕟 1)) (dict𝐷 ["x" ↦♭ 𝕟 10,"y" ↦♭ 𝕟 20]) |] 
              [| dict𝐷 ["x" ↦♭ 𝕟 11,"y" ↦♭ 𝕟 20] |]
𝔱 "core:lens" [| alter (keyL $ 𝕤 "x") (const None) ("x" ↦♭ 𝕟 1) |] [| dø𝐷 |]
𝔱 "core:lens" [| alter (keyL $ 𝕤 "x") (const None) ("y" ↦♭ 𝕟 1) |] [| "y" ↦♭ 𝕟 1 |]
𝔱 "core:lens" [| alter (keyL $ 𝕤 "x") (const None) (dict𝐷 ["x" ↦♭ 𝕟 10,"y" ↦♭ 𝕟 20]) |] 
              [| dict𝐷 ["y" ↦♭ 𝕟 20] |]

newtype CR a = CR { forall a. CR a -> ContT ℕ64 (ReaderT (ℕ64 ∧ ℕ64) ID) a
unCR ∷ ContT ℕ64 (ReaderT (ℕ64 ∧ ℕ64) ID) a }
  deriving
  ( (forall a. a -> CR a) -> Return CR
forall a. a -> CR a
forall (m :: * -> *). (forall a. a -> m a) -> Return m
$creturn :: forall a. a -> CR a
return :: forall a. a -> CR a
Return,(forall a b. CR a -> (a -> CR b) -> CR b) -> Bind CR
forall a b. CR a -> (a -> CR b) -> CR b
forall (m :: * -> *).
(forall a b. m a -> (a -> m b) -> m b) -> Bind m
$c≫= :: forall a b. CR a -> (a -> CR b) -> CR b
≫= :: forall a b. CR a -> (a -> CR b) -> CR b
Bind,(forall a b. (a -> b) -> CR a -> CR b) -> Functor CR
forall a b. (a -> b) -> CR a -> CR b
forall (t :: * -> *).
(forall a b. (a -> b) -> t a -> t b) -> Functor t
$cmap :: forall a b. (a -> b) -> CR a -> CR b
map :: forall a b. (a -> b) -> CR a -> CR b
Functor,Bind CR
Return CR
Functor CR
(Functor CR, Return CR, Bind CR) => Monad CR
forall (m :: * -> *). (Functor m, Return m, Bind m) => Monad m
Monad
  , MonadCont ℕ64
  , MonadReader (ℕ64 ∧ ℕ64)
  )

runCR ∷ ℕ64 → ℕ64 → CR ℕ64 → ℕ64
runCR :: ℕ64 -> ℕ64 -> CR ℕ64 -> ℕ64
runCR ℕ64
x ℕ64
y CR ℕ64
xM = ID ℕ64 -> ℕ64
forall a. ID a -> a
unID (ID ℕ64 -> ℕ64) -> ID ℕ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ (ℕ64 ∧ ℕ64) -> ReaderT (ℕ64 ∧ ℕ64) ID ℕ64 -> ID ℕ64
forall {k} r (m :: k -> *) (a :: k). r -> ReaderT r m a -> m a
runReaderT (ℕ64
x ℕ64 -> ℕ64 -> ℕ64 ∧ ℕ64
forall a b. a -> b -> a ∧ b
:* ℕ64
y) (ReaderT (ℕ64 ∧ ℕ64) ID ℕ64 -> ID ℕ64)
-> ReaderT (ℕ64 ∧ ℕ64) ID ℕ64 -> ID ℕ64
forall a b. (a -> b) -> a -> b
$ ContT ℕ64 (ReaderT (ℕ64 ∧ ℕ64) ID) ℕ64
-> ReaderT (ℕ64 ∧ ℕ64) ID ℕ64
forall (m :: * -> *) u. Return m => ContT u m u -> m u
evalContT (ContT ℕ64 (ReaderT (ℕ64 ∧ ℕ64) ID) ℕ64
 -> ReaderT (ℕ64 ∧ ℕ64) ID ℕ64)
-> ContT ℕ64 (ReaderT (ℕ64 ∧ ℕ64) ID) ℕ64
-> ReaderT (ℕ64 ∧ ℕ64) ID ℕ64
forall a b. (a -> b) -> a -> b
$ CR ℕ64 -> ContT ℕ64 (ReaderT (ℕ64 ∧ ℕ64) ID) ℕ64
forall a. CR a -> ContT ℕ64 (ReaderT (ℕ64 ∧ ℕ64) ID) a
unCR CR ℕ64
xM

execCR ∷ CR ℕ64 → ℕ64
execCR :: CR ℕ64 -> ℕ64
execCR = ℕ64 -> ℕ64 -> CR ℕ64 -> ℕ64
runCR ℕ64
0 ℕ64
0 

𝔱 "core:monads:cr" [| 0   |] [| execCR $ do fst ^$ ask |]
𝔱 "core:monads:cr" [| 0   |] [| execCR $ do snd ^$ ask |]
𝔱 "core:monads:cr" [| 30  |] [| execCR $ do putEnv $ 10 :* 20 ; x :* y ← ask ; return $ x + y |]
𝔱 "core:monads:cr" [| 10  |] [| execCR $ do putEnvL fstL 10 ; x :* y ← ask ; return $ x + y |]
𝔱 "core:monads:cr" [| 10  |] [| execCR $ do putEnvL fstL 10 ; reset (do x :* y ← ask ; return $ x + y) |]
𝔱 "core:monads:cr" [| 0   |] [| execCR $ do _←reset $ (do putEnvL fstL 10;return $ 𝕟64 0);x:*y←ask;return $ x + y |]
𝔱 "core:monads:cr" [| 110 |] 
  [| execCR $ do putEnvL fstL 10;x ← reset $ (do putEnvL fstL 100;askL fstL);y←askL fstL;return $ x + y |]
-- Note: this is why MonadReader has askL/localL as primitives, and not ask/local
𝔱 "core:monads:cr" [| 2 |] [| execCR $ do localL fstL 1 $ putEnvL sndL 2 ; askL sndL |]

newtype UR a = UR { forall a. UR a -> UContT (ReaderT (ℕ64 ∧ ℕ64) ID) a
unUR ∷ UContT (ReaderT (ℕ64 ∧ ℕ64) ID) a }
  deriving
  ( (forall a. a -> UR a) -> Return UR
forall a. a -> UR a
forall (m :: * -> *). (forall a. a -> m a) -> Return m
$creturn :: forall a. a -> UR a
return :: forall a. a -> UR a
Return,(forall a b. UR a -> (a -> UR b) -> UR b) -> Bind UR
forall a b. UR a -> (a -> UR b) -> UR b
forall (m :: * -> *).
(forall a b. m a -> (a -> m b) -> m b) -> Bind m
$c≫= :: forall a b. UR a -> (a -> UR b) -> UR b
≫= :: forall a b. UR a -> (a -> UR b) -> UR b
Bind,(forall a b. (a -> b) -> UR a -> UR b) -> Functor UR
forall a b. (a -> b) -> UR a -> UR b
forall (t :: * -> *).
(forall a b. (a -> b) -> t a -> t b) -> Functor t
$cmap :: forall a b. (a -> b) -> UR a -> UR b
map :: forall a b. (a -> b) -> UR a -> UR b
Functor,Bind UR
Return UR
Functor UR
(Functor UR, Return UR, Bind UR) => Monad UR
forall (m :: * -> *). (Functor m, Return m, Bind m) => Monad m
Monad
  , (forall a. (forall u. (a -> UR u) -> UR u) -> UR a)
-> (forall a u. (a -> UR u) -> UR a -> UR u) -> MonadUCont UR
forall a. (forall u. (a -> UR u) -> UR u) -> UR a
forall a u. (a -> UR u) -> UR a -> UR u
forall (m :: * -> *).
(forall a. (forall u. (a -> m u) -> m u) -> m a)
-> (forall a u. (a -> m u) -> m a -> m u) -> MonadUCont m
$cucallCC :: forall a. (forall u. (a -> UR u) -> UR u) -> UR a
ucallCC :: forall a. (forall u. (a -> UR u) -> UR u) -> UR a
$cuwithC :: forall a u. (a -> UR u) -> UR a -> UR u
uwithC :: forall a u. (a -> UR u) -> UR a -> UR u
MonadUCont
  , MonadReader (ℕ64 ∧ ℕ64)
  )

runUR ∷ ℕ64 → ℕ64 → UR ℕ64 → ℕ64
runUR :: ℕ64 -> ℕ64 -> UR ℕ64 -> ℕ64
runUR ℕ64
x ℕ64
y UR ℕ64
xM = ID ℕ64 -> ℕ64
forall a. ID a -> a
unID (ID ℕ64 -> ℕ64) -> ID ℕ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ (ℕ64 ∧ ℕ64) -> ReaderT (ℕ64 ∧ ℕ64) ID ℕ64 -> ID ℕ64
forall {k} r (m :: k -> *) (a :: k). r -> ReaderT r m a -> m a
runReaderT (ℕ64
x ℕ64 -> ℕ64 -> ℕ64 ∧ ℕ64
forall a b. a -> b -> a ∧ b
:* ℕ64
y) (ReaderT (ℕ64 ∧ ℕ64) ID ℕ64 -> ID ℕ64)
-> ReaderT (ℕ64 ∧ ℕ64) ID ℕ64 -> ID ℕ64
forall a b. (a -> b) -> a -> b
$ UContT (ReaderT (ℕ64 ∧ ℕ64) ID) ℕ64 -> ReaderT (ℕ64 ∧ ℕ64) ID ℕ64
forall (m :: * -> *) a. Return m => UContT m a -> m a
evalUContT (UContT (ReaderT (ℕ64 ∧ ℕ64) ID) ℕ64 -> ReaderT (ℕ64 ∧ ℕ64) ID ℕ64)
-> UContT (ReaderT (ℕ64 ∧ ℕ64) ID) ℕ64
-> ReaderT (ℕ64 ∧ ℕ64) ID ℕ64
forall a b. (a -> b) -> a -> b
$ UR ℕ64 -> UContT (ReaderT (ℕ64 ∧ ℕ64) ID) ℕ64
forall a. UR a -> UContT (ReaderT (ℕ64 ∧ ℕ64) ID) a
unUR UR ℕ64
xM

execUR ∷ UR ℕ64 → ℕ64
execUR :: UR ℕ64 -> ℕ64
execUR = ℕ64 -> ℕ64 -> UR ℕ64 -> ℕ64
runUR ℕ64
0 ℕ64
0 

𝔱 "core:monads:ur" [| 0   |] [| execUR $ do fst ^$ ask |]
𝔱 "core:monads:ur" [| 0   |] [| execUR $ do snd ^$ ask |]
𝔱 "core:monads:ur" [| 30  |] [| execUR $ do uputEnv $ 10 :* 20 ; x :* y ← ask ; return $ x + y |]
𝔱 "core:monads:ur" [| 10  |] [| execUR $ do uputEnvL fstL 10 ; x :* y ← ask ; return $ x + y |]
𝔱 "core:monads:ur" [| 10  |] [| execUR $ do uputEnvL fstL 10 ; ureset (do x :* y ← ask ; return $ x + y) |]
𝔱 "core:monads:ur" [| 0   |] [| execUR $ do _←ureset $ (do uputEnvL fstL 10;return $ 𝕟64 0);x:*y←ask;return $ x + y |]
𝔱 "core:monads:ur" [| 110 |]
  [| execUR $ do uputEnvL fstL 10;x ← ureset $ (do uputEnvL fstL 100;askL fstL);y←askL fstL;return $ x + y |]
-- Note: this is why MonadReader has askL/localL as primitives, and not ask/local
𝔱 "core:monads:ur" [| 2 |] [| execUR $ do localL fstL 1 $ uputEnvL sndL 2 ; askL sndL |]

𝑇D Test
buildTests