compiles, getting stuck somewhere though

app/Main.hs

@@ -1,7 +1,6 @@
 module Main where
 
-import Eval (Env, emptyEnv)
+import Program (handleAndParseFile)
-import Parser (handleFile)
 import Repl
 
 main :: IO ()
@@ -9,8 +8,8 @@ main = do
     args <- getArgs
     case args of
         [] -> void repl
-        files -> handleFiles emptyEnv files
+        files -> handleFiles files
 
-handleFiles :: Env -> [String] -> IO ()
+handleFiles :: [String] -> IO ()
-handleFiles _ [] = putTextLn "success!"
+handleFiles [] = putTextLn "success!"
-handleFiles env (file : rest) = runExceptT (handleFile env file) >>= either putStrLn (`handleFiles` rest)
+handleFiles (file : rest) = runExceptT (handleAndParseFile file) >>= either putStrLn (const $ handleFiles rest)

app/Repl.hs

@@ -4,10 +4,12 @@ import Check (findType)
 import Data.List (stripPrefix)
 import qualified Data.Map.Strict as M
 import Data.Text (pack)
+import Elaborator
 import Errors (Result)
 import Eval
 import Expr
 import Parser
+import Program
 import System.Console.Haskeline
 import System.Directory (createDirectoryIfMissing, getHomeDirectory)
 import System.FilePath ((</>))
@@ -37,21 +39,22 @@ parseCommand (Just input)
 
 handleInput :: Env -> String -> InputT IO Env
 handleInput env input =
-    let (res, env') = parseDefEmpty env (pack input)
+    case parseDef "repl" (pack input) of
-     in case res of
+        Left err -> outputStrLn err >> pure env
-            Left err -> outputStrLn err >> pure env'
+        Right irDef -> case evalDef env irDef of
-            Right () -> pure env'
+            Left err -> outputStrLn (toString err) >> pure env
+            Right env' -> pure env'
 
-actOnParse :: Env -> String -> (Expr -> InputT IO ()) -> InputT IO ()
+actOnParse :: String -> (Expr -> InputT IO ()) -> InputT IO ()
-actOnParse env input action = case parseExpr env (pack input) of
+actOnParse input action = case parseExpr "repl" (pack input) of
     Left err -> outputStrLn err
-    Right expr -> action expr
+    Right expr -> action $ elaborate expr
 
 printErrorOrResult :: Env -> (Expr -> ReaderT Env Result Expr) -> Expr -> InputT IO ()
 printErrorOrResult env action expr = putTextLn $ either toText pretty $ runReaderT (action expr) env
 
 parseActPrint :: Env -> String -> (Expr -> ReaderT Env Result Expr) -> InputT IO ()
-parseActPrint env input action = actOnParse env input (printErrorOrResult env action)
+parseActPrint env input action = actOnParse input (printErrorOrResult env action)
 
 lookupAct :: Env -> String -> (Definition -> InputT IO ()) -> InputT IO ()
 lookupAct env input action = maybe (outputStrLn $ "'" ++ input ++ "' unbound") action $ M.lookup (pack input) env
@@ -75,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 $ handleFile env filename) >>= either ((>> loop env) . outputStrLn) loop
+            Just (LoadFile filename) -> lift (runExceptT $ handleAndParseFile filename) >>= either ((>> loop env) . outputStrLn) loop
             Just (Input input) -> handleInput env input >>= loop

examples/computation.pg

@@ -4,19 +4,19 @@
 
 -- the natural number `n` is encoded as the function taking any function
 -- `A -> A` and repeating it `n` times
-nat : * := forall (A : *), (A -> A) -> A -> A;
+def nat : * := forall (A : *), (A -> A) -> A -> A;
 
 -- zero is the constant function
-zero : nat := fun (A : *) (f : A -> A) (x : A) => x;
+def zero : nat := fun (A : *) (f : A -> A) (x : A) => x;
 
 -- `suc n` composes one more `f` than `n`
-suc : nat -> nat := fun (n : nat) (A : *) (f : A -> A) (x : A) => f ((n A f) x);
+def suc : nat -> nat := fun (n : nat) (A : *) (f : A -> A) (x : A) => f ((n A f) x);
 
 -- addition can be encoded as usual
-plus : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A f) (n A f x);
+def plus : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A f) (n A f x);
 
 -- likewise for multiplication
-times : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A (n A f)) x;
+def times : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A (n A f)) x;
 
 -- unforunately, it is impossible to prove induction on Church numerals,
 -- which makes it really hard to prove standard theorems, or do anything really.
@@ -24,16 +24,16 @@ times : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m
 -- but we can still do computations with Church numerals
 
 -- first some abbreviations for numbers will be handy
-one   : nat := suc zero;
+def one   : nat := suc zero;
-two   : nat := suc one;
+def two   : nat := suc one;
-three : nat := suc two;
+def three : nat := suc two;
-four  : nat := suc three;
+def four  : nat := suc three;
-five  : nat := suc four;
+def five  : nat := suc four;
-six   : nat := suc five;
+def six   : nat := suc five;
-seven : nat := suc six;
+def seven : nat := suc six;
-eight : nat := suc seven;
+def eight : nat := suc seven;
-nine  : nat := suc eight;
+def nine  : nat := suc eight;
-ten   : nat := suc nine;
+def ten   : nat := suc nine;
 
 -- now we can do a bunch of computations, even at the type level
 -- the way we can do this is by defining equality (see <examples/logic.pg> for
@@ -43,22 +43,22 @@ ten   : nat := suc nine;
 -- equivalent
 
 -- first we do need a definition of equality
-eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
+def eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y;
-eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
+def eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx;
-eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) =>
+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;
-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) =>
+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);
-eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) :=
+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`
-one_plus_one_is_two : eq nat (plus one one) two := eq_refl nat two;
+def one_plus_one_is_two : eq nat (plus one one) two := eq_refl nat two;
 
 -- we can likewise compute 2 + 2
-two_plus_two_is_four : eq nat (plus two two) four := eq_refl nat four;
+def two_plus_two_is_four : eq nat (plus two two) four := eq_refl nat four;
 
 -- even multiplication works
-two_times_five_is_ten : eq nat (times two five) ten := eq_refl nat ten;
+def two_times_five_is_ten : eq nat (times two five) ten := eq_refl nat ten;

lib/Check.hs

@@ -33,6 +33,7 @@ findType g (Var x n) = do
     validateType g t
     pure t
 findType _ (Free n) = envLookupTy n
+findType _ (Axiom n) = envLookupTy n
 findType g e@(App m n) = do
     (a, b) <- findType g m >>= matchPi m
     a' <- findType g n

lib/Elaborator.hs

@@ -8,19 +8,22 @@ import qualified IR as I
 
 type Binders = [Text]
 
-elaborate :: IRExpr -> State Binders Expr
+elaborate :: IRExpr -> Expr
-elaborate (I.Var n) = do
+elaborate ir = evalState (elaborate' ir) []
-    binders <- get
+    where
-    pure $ E.Var n . fromIntegral <$> elemIndex n binders ?: E.Free n
+    elaborate' :: IRExpr -> State Binders Expr
-elaborate (I.Level level) = pure $ E.Level level
+    elaborate' (I.Var n) = do
-elaborate (I.App m n) = E.App <$> elaborate m <*> elaborate n
+        binders <- get
-elaborate (I.Abs x t b) = do
+        pure $ E.Var n . fromIntegral <$> elemIndex n binders ?: E.Free n
-    t' <- elaborate t
+    elaborate' (I.Level level) = pure $ E.Level level
-    modify (x :)
+    elaborate' (I.App m n) = E.App <$> elaborate' m <*> elaborate' n
-    E.Abs x t' <$> elaborate b
+    elaborate' (I.Abs x t b) = do
-elaborate (I.Pi x t b) = do
+        t' <- elaborate' t
-    t' <- elaborate t
+        modify (x :)
-    modify (x :)
+        E.Abs x t' <$> elaborate' b
-    E.Pi x t' <$> elaborate b
+    elaborate' (I.Pi x t b) = do
-elaborate (I.Let name Nothing val body) = E.Let name Nothing <$> elaborate val <*> elaborate body
+        t' <- elaborate' t
-elaborate (I.Let name (Just t) val body) = E.Let name . Just <$> elaborate t <*> elaborate val <*> elaborate body
+        modify (x :)
+        E.Pi x t' <$> elaborate' b
+    elaborate' (I.Let name Nothing val body) = E.Let name Nothing <$> elaborate' val <*> elaborate' body
+    elaborate' (I.Let name (Just t) val body) = E.Let name . Just <$> elaborate' t <*> elaborate' val <*> elaborate' body

lib/Eval.hs

@@ -38,6 +38,7 @@ subst k s (Var x n)
     | n > k = Var x (n - 1)
     | otherwise = Var x n
 subst _ _ (Free s) = Free s
+subst _ _ (Axiom s) = Axiom s
 subst _ _ (Level i) = Level i
 subst k s (App m n) = App (subst k s m) (subst k s n)
 subst k s (Abs x m n) = Abs x (subst k s m) (subst (k + 1) (incIndices s) n)
@@ -89,6 +90,7 @@ betaEquiv e1 e2
             (Free n, Free m) -> pure $ n == m
             (Free n, e) -> envLookupVal n >>= betaEquiv e
             (e, Free n) -> envLookupVal n >>= betaEquiv e
+            (Axiom n, Axiom m) -> pure $ n == m
             (Level i, Level j) -> pure $ i == j
             (Abs _ t1 v1, Abs _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2 -- i want idiom brackets
             (Pi _ t1 v1, Pi _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2

lib/Expr.hs

@@ -3,6 +3,7 @@ module Expr where
 data Expr where
     Var :: Text -> Integer -> Expr
     Free :: Text -> Expr
+    Axiom :: Text -> Expr
     Level :: Integer -> Expr
     App :: Expr -> Expr -> Expr
     Abs :: Text -> Expr -> Expr -> Expr
@@ -13,6 +14,7 @@ data Expr where
 instance Eq Expr where
     (Var _ n) == (Var _ m) = n == m
     (Free s) == (Free t) = s == t
+    (Axiom s) == (Axiom t) = s == t
     (Level i) == (Level j) = i == j
     (App e1 e2) == (App f1 f2) = e1 == f1 && e2 == f2
     (Abs _ t1 b1) == (Abs _ t2 b2) = t1 == t2 && b1 == b2
@@ -23,6 +25,7 @@ instance Eq Expr where
 occursFree :: Integer -> Expr -> Bool
 occursFree n (Var _ k) = n == k
 occursFree _ (Free _) = False
+occursFree _ (Axiom _) = False
 occursFree _ (Level _) = False
 occursFree n (App a b) = on (||) (occursFree n) a b
 occursFree n (Abs _ a b) = occursFree n a || occursFree (n + 1) b
@@ -34,6 +37,7 @@ shiftIndices d c (Var x k)
     | k >= c = Var x (k + d)
     | otherwise = Var x k
 shiftIndices _ _ (Free s) = Free s
+shiftIndices _ _ (Axiom s) = Axiom s
 shiftIndices _ _ (Level i) = Level i
 shiftIndices d c (App m n) = App (shiftIndices d c m) (shiftIndices d c n)
 shiftIndices d c (Abs x m n) = Abs x (shiftIndices d c m) (shiftIndices d (c + 1) n)
@@ -105,6 +109,7 @@ showBinding (ident, params, val) =
 helper :: Integer -> Expr -> Text
 helper _ (Var s _) = s
 helper _ (Free s) = s
+helper _ (Axiom s) = s
 helper _ (Level i)
     | i == 0 = "*"
     | otherwise = "*" <> show i

lib/IR.hs

@@ -30,13 +30,11 @@ data IRExpr
 data IRDef
     = Def
         { defName :: Text
-        , defParams :: [Param]
         , defAscription :: Maybe IRExpr
         , defBody :: IRExpr
         }
     | Axiom
         { axiomName :: Text
-        , axiomParams :: [Param]
         , axiomAscription :: IRExpr
         }
 

lib/Parser.hs

@@ -137,7 +137,7 @@ pAxiom = lexeme $ label "axiom" $ do
     params <- pManyParams
     ascription <- fmap (flip (foldr (uncurry Pi)) params) pAscription
     eat ";"
-    pure $ Axiom ident params ascription
+    pure $ Axiom ident ascription
 
 pDef :: Parser IRDef
 pDef = lexeme $ label "definition" $ do
@@ -149,7 +149,7 @@ pDef = lexeme $ label "definition" $ do
     eat ":="
     body <- pIRExpr
     eat ";"
-    pure $ Def ident params ascription body
+    pure $ Def ident ascription $ foldr (uncurry Abs) body params
 
 pIRDef :: Parser IRDef
 pIRDef = pDef <|> pAxiom
@@ -185,4 +185,4 @@ parseExpr :: String -> Text -> Either String IRExpr
 parseExpr = parserWrapper pIRExpr
 
 handleFile :: String -> ExceptT String IO IRProgram
-handleFile filename = (toString `withExceptT` runPreprocessor filename) >>= hoistEither . parseProgram filename
+handleFile filename = toString `withExceptT` runPreprocessor filename >>= hoistEither . parseProgram filename

lib/Program.hs

@@ -0,0 +1,51 @@
+module Program where
+
+import Check
+import Control.Monad.Except
+import qualified Data.Map.Strict as M
+import Elaborator
+import Errors
+import Eval (Env, checkBeta)
+import qualified Eval
+import Expr (Expr)
+import qualified Expr
+import IR
+import Parser (parseProgram)
+import Preprocessor (runPreprocessor)
+
+insertDef :: Text -> Expr -> Expr -> Env -> Env
+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
+    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
+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
+
+evalDef :: Env -> IRDef -> Result Env
+evalDef = flip (execStateT . handleDef)
+
+handleProgram :: IRProgram -> Result Env
+handleProgram = flip execStateT M.empty . mapM_ handleDef
+
+handleAndParseProgram :: String -> Text -> Either String Env
+handleAndParseProgram filename input = (first toString . handleProgram) =<< parseProgram filename input
+
+handleAndParseFile :: String -> ExceptT String IO Env
+handleAndParseFile filename = toString `withExceptT` runPreprocessor filename >>= hoistEither . handleAndParseProgram filename

perga.cabal

@@ -33,6 +33,7 @@ library perga-lib
                         IR
                         Parser
                         Preprocessor
+                        Program
 
     hs-source-dirs:     lib
     build-depends:      base ^>=4.19.1.0