From 8adfd9f8bab0a2a058155f375ca2e5e089d0080b Mon Sep 17 00:00:00 2001 From: William Ball Date: Sat, 30 Nov 2024 22:36:27 -0800 Subject: [PATCH] elaborator v1 --- lib/Check.hs | 7 ++++++- lib/Elaborator.hs | 26 +++++++++++++++++++++++++ lib/Eval.hs | 15 +++++---------- lib/Expr.hs | 10 +++++----- lib/IR.hs | 48 +++++++++++++++++++++-------------------------- lib/Parser.hs | 15 ++------------- perga.cabal | 1 - 7 files changed, 65 insertions(+), 57 deletions(-) create mode 100644 lib/Elaborator.hs diff --git a/lib/Check.hs b/lib/Check.hs index 7fc2306..026187d 100644 --- a/lib/Check.hs +++ b/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 diff --git a/lib/Elaborator.hs b/lib/Elaborator.hs new file mode 100644 index 0000000..726dfbc --- /dev/null +++ b/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 diff --git a/lib/Eval.hs b/lib/Eval.hs index 32e59d5..c30896b 100644 --- a/lib/Eval.hs +++ b/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 - (e, Let _ v b) -> 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 _ -> pure False -- remaining cases impossible or false checkBeta :: Env -> Expr -> Expr -> Result Bool diff --git a/lib/Expr.hs b/lib/Expr.hs index ffc09d0..d112518 100644 --- a/lib/Expr.hs +++ b/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 diff --git a/lib/IR.hs b/lib/IR.hs index 6a63faf..a8704d6 100644 --- a/lib/IR.hs +++ b/lib/IR.hs @@ -1,49 +1,43 @@ -{-# LANGUAGE TemplateHaskell #-} - module IR where -import Control.Lens - type Param = (Text, IRExpr) data IRExpr - = Var {_varName :: Text} - | Level {_level :: Integer} + = Var {varName :: Text} + | Level {level :: Integer} | App - { _appFunc :: IRExpr - , _appArg :: IRExpr + { appFunc :: IRExpr + , appArg :: IRExpr } | Abs - { _absParamName :: Text - , _absParamType :: IRExpr - , _absBody :: IRExpr + { absParamName :: Text + , absParamType :: IRExpr + , absBody :: IRExpr } | Pi - { _piParamName :: Text - , _piParamType :: IRExpr - , _piBody :: IRExpr + { piParamName :: Text + , piParamType :: IRExpr + , piBody :: IRExpr } | Let - { _letVarName :: Text - , _letAscription :: Maybe IRExpr - , _letValue :: IRExpr - , _letBody :: IRExpr + { letVarName :: Text + , letAscription :: Maybe IRExpr + , letValue :: IRExpr + , letBody :: IRExpr } deriving (Show, Eq, Ord) -makeLenses ''IRExpr - data IRDef = Def - { _defName :: Text - , _defParams :: [Param] - , _defAscription :: Maybe IRExpr - , _defBody :: IRExpr + { defName :: Text + , defParams :: [Param] + , defAscription :: Maybe IRExpr + , defBody :: IRExpr } | Axiom - { _axiomName :: Text - , _axiomParams :: [Param] - , _axiomAscription :: IRExpr + { axiomName :: Text + , axiomParams :: [Param] + , axiomAscription :: IRExpr } type IRProgram = [IRDef] diff --git a/lib/Parser.hs b/lib/Parser.hs index b752c35..307242e 100644 --- a/lib/Parser.hs +++ b/lib/Parser.hs @@ -158,21 +158,10 @@ pTerm :: Parser IRExpr pTerm = lexeme $ label "term" $ - choice - [ between (char '(') (char ')') pIRExpr - , pSort - , pVar - ] + choice [between (char '(') (char ')') pIRExpr, pSort, pVar] pAppTerm :: Parser IRExpr -pAppTerm = - lexeme $ - choice - [ pLAbs - , pPAbs - , pLet - , pApp - ] +pAppTerm = lexeme $ choice [pLAbs, pPAbs, pLet, pApp] pIRExpr :: Parser IRExpr pIRExpr = lexeme $ try pArrow <|> pAppTerm diff --git a/perga.cabal b/perga.cabal index 0b3cf4a..b78f3a1 100644 --- a/perga.cabal +++ b/perga.cabal @@ -38,7 +38,6 @@ library perga-lib build-depends: base ^>=4.19.1.0 , relude , filepath - , lens , megaparsec , mtl , parser-combinators