clean test

src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs

@@ -237,9 +237,7 @@ mkRecordNameSignature _ps rhs =
     indexedByHash (symbolParsed . (^. nameItemSymbol)) (run (execOutputList (evalState 0 helper)))
   where
     helper :: forall r. (r ~ '[State Int, Output (NameItem s)]) => Sem r ()
-    helper = do
-      -- forM_ ps emitParameters
-      forOf_ (rhsRecordStatements . each . _RecordStatementField) rhs emitField
+    helper = forOf_ (rhsRecordStatements . each . _RecordStatementField) rhs emitField
       where
         emitItem :: (Int -> NameItem s) -> Sem r ()
         emitItem mkitem = do
@@ -255,18 +253,3 @@ mkRecordNameSignature _ps rhs =
               _nameItemDefault = Nothing,
               _nameItemIndex
             }
-
--- emitParameters :: InductiveParameters s -> Sem r ()
--- emitParameters params = forM_ (params ^. inductiveParametersNames) emitParam
---   where
---     -- FIXME  implicitness!!
---     emitParam :: SymbolType s -> Sem r ()
---     emitParam sym = emitItem $ \_nameItemIndex ->
---       NameItem
---         { _nameItemSymbol = sym,
---           _nameItemType = fromMaybe defaultType (params ^? inductiveParametersRhs . _Just . inductiveParametersType),
---           _nameItemDefault = Nothing,
---           _nameItemIndex
---         }
---       where
---         defaultType = run (runReader (getLocSymbolType sym) Gen.smallUniverseExpression)

tests/positive/Monads/Identity.juvix

@@ -5,6 +5,8 @@ import Functor open;
 
 type Identity (a : Type) := mkIdentity {runIdentity : a};
 
+open Identity public;
+
 instance
 Identity-Functor : Functor Identity :=
   mkFunctor@{

tests/positive/Monads/Monad.juvix

@@ -13,3 +13,9 @@ type Monad (f : Type -> Type) :=
     syntax operator >>= bind;
     >>= : {A B : Type} -> f A -> (A -> f B) -> f B
   };
+
+open Monad public;
+
+syntax operator >> bind;
+>> {M : Type → Type} {A B : Type} {{Monad M}} (x : M
+  A) (y : M B) : M B := x >>= λ {_ := y};

tests/positive/Monads/MonadReader.juvix

@@ -10,3 +10,5 @@ type MonadReader (S : Type) (M : Type -> Type) :=
     ask : M S;
     reader : {A : Type} → (S → A) → M A
   };
+
+open MonadReader public;

tests/positive/Monads/MonadState.juvix

@@ -10,3 +10,9 @@ type MonadState (S : Type) (M : Type -> Type) :=
     get : M S;
     put : S -> M Unit
   };
+
+open MonadState public;
+
+modify {S : Type} {M : Type → Type} {{Monad M}} {{MonadState
+  S
+  M}} (f : S → S) : M Unit := get >>= λ {s := put (f s)};

tests/positive/Monads/ReaderT.juvix

@@ -8,6 +8,10 @@ import Functor open using {module Functor as MFunctor};
 type ReaderT (S : Type) (M : Type → Type) (A : Type) :=
   mkReaderT {runReaderT : S → M A};
 
+runReader {S A : Type} {M : Type
+  → Type} (r : S) (m : ReaderT S M A) : M A :=
+  ReaderT.runReaderT m r;
+
 instance
 ReaderT-Functor {S : Type} {M : Type
   → Type} {{func : Functor M}} : Functor (ReaderT S M) :=
@@ -34,9 +38,7 @@ ReaderT-Monad {S : Type} {M : Type → Type} {{mon : Monad M}}
     >>= {A B : Type} (x : ReaderT S M A) (f : A → ReaderT S M B)
       : ReaderT S M B :=
       mkReaderT
-        λ {s :=
-          ReaderT.runReaderT x s
-            MMonad.>>= λ {a := ReaderT.runReaderT (f a) s}}
+        λ {s := runReader s x MMonad.>>= λ {a := runReader s (f a)}}
   };
 
 import MonadReader open;
@@ -55,6 +57,7 @@ ReaderT-MonadReader {S : Type} {M : Type → Type} {{Monad M}}
 
 import MonadState open;
 import StateT open;
+import Identity open;
 import Stdlib.Data.Product open;
 
 liftReaderT {R A : Type} {M : Type → Type} (m : M A)
@@ -65,6 +68,19 @@ liftStateT {S A : Type} {M : Type → Type} {{Monad M}} (m : M
   mkStateT
     λ {s := m MMonad.>>= λ {a := MMonad.return (a, s)}};
 
+import Stdlib.Data.Nat open;
+
+askNat {M : Type → Type} {{Monad M}} : ReaderT Nat M Nat :=
+  ask;
+
+monadic : ReaderT Nat (StateT Nat Identity) Nat :=
+  askNat
+    >>= λ {n :=
+      liftReaderT (modify λ {m := m * n}) >> liftReaderT get};
+
+main : Nat :=
+  runIdentity (evalState 2 (runReader 5 monadic));
+
 -- FIXME fails instance termination
 -- instance
 -- StateT-MonadReader {R S : Type} {M : Type

tests/positive/Monads/StateT.juvix

@@ -9,6 +9,15 @@ import Stdlib.Data.Product open;
 type StateT (S : Type) (M : Type → Type) (A : Type) :=
   mkStateT {runStateT : S → M (A × S)};
 
+runState {S A : Type} {M : Type → Type} (s : S) (m : StateT
+  S
+  M
+  A) : M (A × S) := StateT.runStateT m s;
+
+evalState {S A : Type} {M : Type → Type} {{Functor
+  M}} (s : S) (m : StateT S M A) : M A :=
+  fst Functor.<$> runState s m;
+
 instance
 StateT-Functor {S : Type} {M : Type → Type} {{func : Functor
   M}} : Functor (StateT S M) :=
@@ -21,31 +30,34 @@ StateT-Functor {S : Type} {M : Type → Type} {{func : Functor
           λ {s := λ {(a, s') := f a, s'} MFunctor.<$> S→M⟨A×S⟩ s}
   };
 
--- instance
--- StateT-Monad {S : Type} {M : Type → Type} {{mon : Monad M}}
---   : Monad (StateT S M) :=
---   mkMonad@{
---     functor :=
---       StateT-Functor@{
---         func := MMonad.functor
---       };
---     return {A : Type} (a : A) : StateT S M A :=
---       mkStateT λ {s := MMonad.return (a, s)};
---     >>= {A B : Type} (x : StateT S M A) (f : A → StateT S M B)
---       : StateT S M B :=
---       mkStateT
---         λ {s :=
---           StateT.runStateT x s
---             MMonad.>>= λ {(a, s') := StateT.runStateT (f a) s'}}
---   };
-
--- import MonadState open;
--- import Stdlib.Data.Unit open;
-
--- instance
--- StateT-MonadState {S : Type} {M : Type → Type} {{Monad M}} : MonadState S (StateT S M) :=
---   mkMonadState@{
---     monad := StateT-Monad;
---     get : StateT S M S := mkStateT λ {s := MMonad.return (s, s)};
---     put (s : S) : StateT S M Unit := mkStateT λ {_ := MMonad.return (unit, s)};
---   };
+instance
+StateT-Monad {S : Type} {M : Type → Type} {{mon : Monad M}}
+  : Monad (StateT S M) :=
+  mkMonad@{
+    functor :=
+      StateT-Functor@{
+        func := MMonad.functor
+      };
+    return {A : Type} (a : A) : StateT S M A :=
+      mkStateT λ {s := MMonad.return (a, s)};
+    >>= {A B : Type} (x : StateT S M A) (f : A → StateT S M B)
+      : StateT S M B :=
+      mkStateT
+        λ {s :=
+          StateT.runStateT x s
+            MMonad.>>= λ {(a, s') := StateT.runStateT (f a) s'}}
+  };
+
+import MonadState open;
+import Stdlib.Data.Unit open;
+
+instance
+StateT-MonadState {S : Type} {M : Type → Type} {{Monad M}}
+  : MonadState S (StateT S M) :=
+  mkMonadState@{
+    monad := StateT-Monad;
+    get : StateT S M S :=
+      mkStateT λ {s := MMonad.return (s, s)};
+    put (s : S) : StateT S M Unit :=
+      mkStateT λ {_ := MMonad.return (unit, s)}
+  };