made repl preserve environment

app/Main.hs

@@ -1,5 +1,6 @@
 module Main where
 
+import qualified Data.Map.Strict as M
 import Program (handleAndParseFile)
 import Repl
 
@@ -12,4 +13,4 @@ main = do
 
 handleFiles :: [String] -> IO ()
 handleFiles [] = putTextLn "success!"
-handleFiles (file : rest) = runExceptT (handleAndParseFile file) >>= either putStrLn (const $ handleFiles rest)
+handleFiles (file : rest) = runExceptT (handleAndParseFile M.empty file) >>= either putStrLn (const $ handleFiles rest)

app/Repl.hs

@@ -78,5 +78,5 @@ repl = do
             Just (ValueQuery input) -> lookupAct env input (putTextLn . pretty . _val) >> loop env
             Just (Normalize input) -> parseActPrint env input normalize >> loop env
             Just (WeakNormalize input) -> parseActPrint env input whnf >> loop env
-            Just (LoadFile filename) -> lift (runExceptT $ handleAndParseFile filename) >>= either ((>> loop env) . outputStrLn) loop
+            Just (LoadFile filename) -> lift (runExceptT $ handleAndParseFile env filename) >>= either ((>> loop env) . outputStrLn) loop
             Just (Input input) -> handleInput env input >>= loop

examples/classical.pg

@@ -2,7 +2,7 @@
 
 -- excluded middle!
 -- P ∨ ~P
-axiom em (P : *) : or (P) (not P);
+axiom em (P : *) : or P (not P);
 
 -- ~~P => P
 def dne (P : *) (nnp : not (not P)) : P :=

examples/computation.pg

@@ -1,3 +1,5 @@
+@include logic.pg
+
 -- without recursion, computation is kind of hard
 -- we can, however, define natural numbers using the Church encoding and do
 -- computation with them
@@ -42,17 +44,6 @@ def ten   : nat := suc nine;
 -- then perga will only accept our proof if `plus one one` and `two` are beta
 -- equivalent
 
--- first we do need a definition of equality
-def eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
-def eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
-def eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) =>
-    Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy;
-def eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) =>
-    Hyz P (Hxy P Hx);
-def eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
-  fun (P : B -> *) (Hfx : P (f x)) =>
-      H (fun (a : A) => P (f a)) Hfx;
-
 -- since `plus one one` and `two` are beta-equivalent, `eq_refl nat two` is a
 -- proof that `1 + 1 = 2`
 def one_plus_one_is_two : eq nat (plus one one) two := eq_refl nat two;

lib/Eval.hs

@@ -99,8 +99,11 @@ betaEquiv e1 e2
             (e, Let _ _ v b) -> betaEquiv (subst 0 v b) e
             _ -> pure False -- remaining cases impossible or false
 
-checkBeta :: Env -> Expr -> Expr -> Result Bool
-checkBeta env e1 e2 = runReaderT (betaEquiv e1 e2) env
+checkBeta :: Env -> Expr -> Expr -> Expr -> Result ()
+checkBeta env e1 e2 ctxt = case runReaderT (betaEquiv e1 e2) env of
+    Left err -> Left err
+    Right False -> Left $ NotEquivalent e1 e2 ctxt
+    Right True -> Right ()
 
 isSortPure :: Expr -> Bool
 isSortPure (Level _) = True

lib/Program.hs

@@ -19,33 +19,31 @@ insertDef name ty body = M.insert name (Eval.Def ty body)
 handleDef :: IRDef -> StateT Env Result ()
 handleDef (Axiom name ty) = do
     env <- get
-    whenLeft_ (checkType env $ elaborate ty) throwError
+    _ <- liftEither $ checkType env $ elaborate ty
     modify $ insertDef name (elaborate ty) (Expr.Axiom name)
 handleDef (Def name Nothing irBody) = do
     env <- get
-    let body = elaborate irBody
-    let ty = checkType env body
-    either throwError (modify . flip (insertDef name) body) ty
+    ty <- liftEither $ checkType env body
+    modify $ insertDef name ty body
+  where
+    body = elaborate irBody
 handleDef (Def name (Just irTy) irBody) = do
     env <- get
-    let body = elaborate irBody
-    let ty = elaborate irTy
-    let mty' = checkType env body
-    whenLeft_ mty' throwError
-    whenRight_ mty' $ \ty' -> do
-        case checkBeta env ty ty' of
-            Left err -> throwError err
-            Right False -> throwError $ NotEquivalent ty ty' body
-            Right True -> modify $ insertDef name ty' body
+    ty' <- liftEither $ checkType env body
+    liftEither $ checkBeta env ty ty' body
+    modify $ insertDef name ty' body
+  where
+    body = elaborate irBody
+    ty = elaborate irTy
 
 evalDef :: Env -> IRDef -> Result Env
 evalDef = flip (execStateT . handleDef)
 
-handleProgram :: IRProgram -> Result Env
-handleProgram = flip execStateT M.empty . mapM_ handleDef
+handleProgram :: Env -> IRProgram -> Result Env
+handleProgram env = flip execStateT env . mapM_ handleDef
 
-handleAndParseProgram :: String -> Text -> Either String Env
-handleAndParseProgram filename input = (first toString . handleProgram) =<< parseProgram filename input
+handleAndParseProgram :: Env -> String -> Text -> Either String Env
+handleAndParseProgram env filename input = (first toString . handleProgram env) =<< parseProgram filename input
 
-handleAndParseFile :: String -> ExceptT String IO Env
-handleAndParseFile filename = toString `withExceptT` runPreprocessor filename >>= hoistEither . handleAndParseProgram filename
+handleAndParseFile :: Env -> String -> ExceptT String IO Env
+handleAndParseFile env filename = toString `withExceptT` runPreprocessor filename >>= hoistEither . handleAndParseProgram env filename