From 05ae14b5e7dc76a5c023703d135d8fbb2958b3d0 Mon Sep 17 00:00:00 2001 From: William Ball Date: Sun, 1 Dec 2024 18:06:03 -0800 Subject: [PATCH] made repl preserve environment --- app/Main.hs | 3 ++- app/Repl.hs | 2 +- examples/classical.pg | 2 +- examples/computation.pg | 13 ++----------- lib/Eval.hs | 7 +++++-- lib/Program.hs | 36 +++++++++++++++++------------------- 6 files changed, 28 insertions(+), 35 deletions(-) diff --git a/app/Main.hs b/app/Main.hs index f1eefa9..93de258 100644 --- a/app/Main.hs +++ b/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) diff --git a/app/Repl.hs b/app/Repl.hs index e826fcd..322483f 100644 --- a/app/Repl.hs +++ b/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 diff --git a/examples/classical.pg b/examples/classical.pg index 14bbd39..63b04c7 100644 --- a/examples/classical.pg +++ b/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 := diff --git a/examples/computation.pg b/examples/computation.pg index 189f30c..e565e7f 100644 --- a/examples/computation.pg +++ b/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; diff --git a/lib/Eval.hs b/lib/Eval.hs index 0d5bff4..876f271 100644 --- a/lib/Eval.hs +++ b/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 diff --git a/lib/Program.hs b/lib/Program.hs index 9e5b07a..7439ae3 100644 --- a/lib/Program.hs +++ b/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