elaborator v1

lib/Check.hs

@@ -48,7 +48,12 @@ findType g (Pi _ a b) = do
     i <- findLevel g a
     j <- findLevel (incIndices a : map incIndices g) b
     pure $ Level $ max (i - 1) j -- This feels very sketchy, but certainly adds impredicativity
-findType g (Let _ v b) = findType g (subst 0 v b)
+findType g (Let _ Nothing v b) = findType g (subst 0 v b)
+findType g e@(Let _ (Just t) v b) = do
+    res <- findType g (subst 0 v b)
+    equiv <- betaEquiv t res
+    unless equiv $ throwError $ NotEquivalent t res e
+    pure t
 
 checkType :: Env -> Expr -> Result Expr
 checkType env t = runReaderT (findType [] t) env

lib/Elaborator.hs

@@ -0,0 +1,26 @@
+module Elaborator where
+
+import Data.List (elemIndex)
+import Expr (Expr)
+import qualified Expr as E
+import IR (IRExpr)
+import qualified IR as I
+
+type Binders = [Text]
+
+elaborate :: IRExpr -> State Binders Expr
+elaborate (I.Var n) = do
+    binders <- get
+    pure $ E.Var n . fromIntegral <$> elemIndex n binders ?: E.Free n
+elaborate (I.Level level) = pure $ E.Level level
+elaborate (I.App m n) = E.App <$> elaborate m <*> elaborate n
+elaborate (I.Abs x t b) = do
+    t' <- elaborate t
+    modify (x :)
+    E.Abs x t' <$> elaborate b
+elaborate (I.Pi x t b) = do
+    t' <- elaborate t
+    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

@@ -10,9 +10,6 @@ import Relude.Extra.Lens
 
 data Definition = Def {_ty :: Expr, _val :: Expr}
 
-makeDef :: Expr -> Expr -> Definition
-makeDef typ value = Def{_ty = typ, _val = value}
-
 tyL :: Lens' Definition Expr
 tyL = lens _ty setter
   where
@@ -41,12 +38,11 @@ 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)
 subst k s (Pi x m n) = Pi x (subst k s m) (subst (k + 1) (incIndices s) n)
-subst k s (Let x v b) = Let x (subst k s v) (subst (k + 1) (incIndices s) b)
+subst k s (Let x t v b) = Let x t (subst k s v) (subst (k + 1) (incIndices s) b)
 
 envLookupVal :: Text -> ReaderT Env Result Expr
 envLookupVal n = asks ((_val <$>) . M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure
@@ -63,7 +59,7 @@ whnf (App m n) = do
         then pure $ App m n
         else whnf $ App m' n
 whnf (Free n) = envLookupVal n >>= whnf
-whnf (Let _ v b) = whnf $ subst 0 v b
+whnf (Let _ _ v b) = whnf $ subst 0 v b
 whnf e = pure e
 
 reduce :: Expr -> ReaderT Env Result Expr
@@ -72,7 +68,7 @@ reduce (App m n) = App <$> reduce m <*> reduce n
 reduce (Abs x t v) = Abs x <$> reduce t <*> reduce v
 reduce (Pi x t v) = Pi x <$> reduce t <*> reduce v
 reduce (Free n) = envLookupVal n
-reduce (Let _ v b) = pure $ subst 0 v b
+reduce (Let _ _ v b) = pure $ subst 0 v b
 reduce e = pure e
 
 normalize :: Expr -> ReaderT Env Result Expr
@@ -91,15 +87,14 @@ betaEquiv e1 e2
         case (e1', e2') of
             (Var k1 _, Var k2 _) -> pure $ k1 == k2
             (Free n, Free m) -> pure $ n == m
-            (Axiom n, Axiom m) -> pure $ n == m
             (Free n, e) -> envLookupVal n >>= betaEquiv e
             (e, Free n) -> envLookupVal n >>= betaEquiv e
             (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
             (App m1 n1, App m2 n2) -> (&&) <$> betaEquiv m1 m2 <*> betaEquiv n1 n2
-            (Let _ v b, e) -> betaEquiv (subst 0 v b) e
+            (Let _ _ v b, e) -> betaEquiv (subst 0 v b) e
-            (e, Let _ v b) -> betaEquiv (subst 0 v b) e
+            (e, Let _ _ v b) -> betaEquiv (subst 0 v b) e
             _ -> pure False -- remaining cases impossible or false
 
 checkBeta :: Env -> Expr -> Expr -> Result Bool

lib/Expr.hs

@@ -7,7 +7,7 @@ data Expr where
     App :: Expr -> Expr -> Expr
     Abs :: Text -> Expr -> Expr -> Expr
     Pi :: Text -> Expr -> Expr -> Expr
-    Let :: Text -> Expr -> Expr -> Expr
+    Let :: Text -> Maybe Expr -> Expr -> Expr -> Expr
     deriving (Show, Ord)
 
 instance Eq Expr where
@@ -17,7 +17,7 @@ instance Eq Expr where
     (App e1 e2) == (App f1 f2) = e1 == f1 && e2 == f2
     (Abs _ t1 b1) == (Abs _ t2 b2) = t1 == t2 && b1 == b2
     (Pi _ t1 b1) == (Pi _ t2 b2) = t1 == t2 && b1 == b2
-    (Let _ v1 b1) == (Let _ v2 b2) = v1 == v2 && b1 == b2
+    (Let _ _ v1 b1) == (Let _ _ v2 b2) = v1 == v2 && b1 == b2
     _ == _ = False
 
 occursFree :: Integer -> Expr -> Bool
@@ -27,7 +27,7 @@ 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
 occursFree n (Pi _ a b) = occursFree n a || occursFree (n + 1) b
-occursFree n (Let _ v b) = occursFree n v || occursFree (n + 1) b
+occursFree n (Let _ _ v b) = occursFree n v || occursFree (n + 1) b
 
 shiftIndices :: Integer -> Integer -> Expr -> Expr
 shiftIndices d c (Var x k)
@@ -38,7 +38,7 @@ 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)
 shiftIndices d c (Pi x m n) = Pi x (shiftIndices d c m) (shiftIndices d (c + 1) n)
-shiftIndices d c (Let x v b) = Let x (shiftIndices d c v) (shiftIndices d (c + 1) b)
+shiftIndices d c (Let x t v b) = Let x t (shiftIndices d c v) (shiftIndices d (c + 1) b)
 
 incIndices :: Expr -> Expr
 incIndices = shiftIndices 1 0
@@ -59,7 +59,7 @@ collectLambdas (Abs x ty body) = ((x, ty) : params, final)
 collectLambdas e = ([], e)
 
 collectLets :: Expr -> ([Binding], Expr)
-collectLets (Let x val body) = ((x, params', val') : bindings, final)
+collectLets (Let x _ val body) = ((x, params', val') : bindings, final)
   where
     (bindings, final) = collectLets body
     (params, val') = collectLambdas val

lib/IR.hs

@@ -1,49 +1,43 @@
-{-# LANGUAGE TemplateHaskell #-}
-
 module IR where
 
-import Control.Lens
-
 type Param = (Text, IRExpr)
 
 data IRExpr
-    = Var {_varName :: Text}
+    = Var {varName :: Text}
-    | Level {_level :: Integer}
+    | Level {level :: Integer}
     | App
-        { _appFunc :: IRExpr
+        { appFunc :: IRExpr
-        , _appArg :: IRExpr
+        , appArg :: IRExpr
         }
     | Abs
-        { _absParamName :: Text
+        { absParamName :: Text
-        , _absParamType :: IRExpr
+        , absParamType :: IRExpr
-        , _absBody :: IRExpr
+        , absBody :: IRExpr
         }
     | Pi
-        { _piParamName :: Text
+        { piParamName :: Text
-        , _piParamType :: IRExpr
+        , piParamType :: IRExpr
-        , _piBody :: IRExpr
+        , piBody :: IRExpr
         }
     | Let
-        { _letVarName :: Text
+        { letVarName :: Text
-        , _letAscription :: Maybe IRExpr
+        , letAscription :: Maybe IRExpr
-        , _letValue :: IRExpr
+        , letValue :: IRExpr
-        , _letBody :: IRExpr
+        , letBody :: IRExpr
         }
     deriving (Show, Eq, Ord)
 
-makeLenses ''IRExpr
-
 data IRDef
     = Def
-        { _defName :: Text
+        { defName :: Text
-        , _defParams :: [Param]
+        , defParams :: [Param]
-        , _defAscription :: Maybe IRExpr
+        , defAscription :: Maybe IRExpr
-        , _defBody :: IRExpr
+        , defBody :: IRExpr
         }
     | Axiom
-        { _axiomName :: Text
+        { axiomName :: Text
-        , _axiomParams :: [Param]
+        , axiomParams :: [Param]
-        , _axiomAscription :: IRExpr
+        , axiomAscription :: IRExpr
         }
 
 type IRProgram = [IRDef]

lib/Parser.hs

@@ -158,21 +158,10 @@ pTerm :: Parser IRExpr
 pTerm =
     lexeme $
         label "term" $
-            choice
+            choice [between (char '(') (char ')') pIRExpr, pSort, pVar]
-                [ between (char '(') (char ')') pIRExpr
-                , pSort
-                , pVar
-                ]
 
 pAppTerm :: Parser IRExpr
-pAppTerm =
+pAppTerm = lexeme $ choice [pLAbs, pPAbs, pLet, pApp]
-    lexeme $
-        choice
-            [ pLAbs
-            , pPAbs
-            , pLet
-            , pApp
-            ]
 
 pIRExpr :: Parser IRExpr
 pIRExpr = lexeme $ try pArrow <|> pAppTerm

perga.cabal

@@ -38,7 +38,6 @@ library perga-lib
     build-depends:      base ^>=4.19.1.0
                       , relude
                       , filepath
-                      , lens
                       , megaparsec
                       , mtl
                       , parser-combinators