From cf26b7c9ec3c7dea22e30d07a27bd1089c3f5bd7 Mon Sep 17 00:00:00 2001 From: William Ball Date: Wed, 11 Dec 2024 14:12:56 -0800 Subject: [PATCH] trying out new lightweight Automathy function syntax --- examples/category.pg | 8 +++----- examples/logic.pg | 12 ++++++------ examples/peano.pg | 8 ++++---- lib/Check.hs | 12 +++++------- lib/Elaborator.hs | 34 ++++++++++++++-------------------- lib/Eval.hs | 16 ++++++++-------- lib/Expr.hs | 38 +++++++++++++++++++------------------- lib/IR.hs | 2 -- lib/Parser.hs | 40 ++++++++++++++++++++++++---------------- 9 files changed, 83 insertions(+), 87 deletions(-) diff --git a/examples/category.pg b/examples/category.pg index 4d0d863..dc5a434 100644 --- a/examples/category.pg +++ b/examples/category.pg @@ -25,8 +25,8 @@ section Category def × (A B C : Obj) (piA : C ~> A) (piB : C ~> B) := forall (D : Obj) (f : D ~> A) (g : D ~> B), exists_uniq (D ~> C) (fun (fxg : D ~> C) => - (eq (D ~> A) (comp D C A fxg piA) f) - ∧ (eq (D ~> B) (comp D C B fxg piB) g)); + eq (D ~> A) (comp D C A fxg piA) f + ∧ eq (D ~> B) (comp D C B fxg piB) g); section Inverses variable @@ -40,9 +40,7 @@ section Category def inv := inv_l ∧ inv_r; end Inverses - def ≅ (A B : Obj) := - exists (A ~> B) (fun (f : A ~> B) => - exists (B ~> A) (inv A B f)); + def ≅ (A B : Obj) := exists (A ~> B) (fun (f : A ~> B) => exists (B ~> A) (inv A B f)); infixl 20 ≅; diff --git a/examples/logic.pg b/examples/logic.pg index ffde90c..d28ee0c 100644 --- a/examples/logic.pg +++ b/examples/logic.pg @@ -13,7 +13,7 @@ def false_elim (A : ★) (contra : false) : A := contra A; def true : ★ := forall (A : ★), A → A; -def true_intro : true := fun (A : ★) (x : A) => x; +def true_intro : true := [A : ★][x : A] x; -- -------------------------------------------------------------------------------------------------------------- @@ -150,8 +150,8 @@ section Theorems -- ~(A ∨ B) => ~A ∧ ~B def de_morgan1 (h : not (A ∨ B)) : not A ∧ not B := and_intro (not A) (not B) - (fun (a : A) => h (or_intro_l A B a)) - (fun (b : B) => h (or_intro_r A B b)); + ([a : A] h (or_intro_l A B a)) + ([b : B] h (or_intro_r A B b)); -- ~A ∧ ~B => ~(A ∨ B) def de_morgan2 (h : not A ∧ not B) : not (A ∨ B) := @@ -178,8 +178,8 @@ section Theorems -- A ∨ B => B ∨ A def or_comm (h : A ∨ B) : B ∨ A := or_elim A B (B ∨ A) h - (fun (a : A) => or_intro_r B A a) - (fun (b : B) => or_intro_l B A b); + ([a : A] or_intro_r B A a) + ([b : B] or_intro_l B A b); -- A ∧ (B ∧ C) => (A ∧ B) ∧ C def and_assoc_l (h : A ∧ (B ∧ C)) : (A ∧ B) ∧ C := @@ -240,7 +240,7 @@ section Theorems -- Thanks Quinn! -- A ∨ B => ~B => A def disj_syllog (nb : not B) (hor : A ∨ B) : A := - or_elim A B A hor (fun (a : A) => a) (fun (b : B) => nb b A); + or_elim A B A hor ([a : A] a) ([b : B] nb b A); -- (A => B) => ~B => ~A def contrapositive (f : A → B) (nb : not B) : not A := diff --git a/examples/peano.pg b/examples/peano.pg index 28924ab..b04a6c3 100644 --- a/examples/peano.pg +++ b/examples/peano.pg @@ -478,7 +478,7 @@ def one_plus_one_two : one + one = two := -- First, associativity, namely that n + (m + p) = (n + m) + p. def plus_assoc : forall (n m p : nat), n + (m + p) = n + m + p - := fun (n m : nat) => + := [n m : nat] -- We prove this via induction on p for any fixed n and m. nat_ind (fun (p : nat) => n + (m + p) = n + m + p) @@ -524,7 +524,7 @@ def plus_assoc : forall (n m p : nat), n + (m + p) = n + m + p -- First, we will show that 0 + n = n. def plus_0_l : forall (n : nat), zero + n = n := -- We prove this by induction on n. - nat_ind (fun (n : nat) => zero + n = n) + nat_ind ([n : nat] zero + n = n) -- base case: WTS 0 + 0 = 0 -- This is just plus_0_r 0 (plus_0_r zero) @@ -543,7 +543,7 @@ def plus_0_l : forall (n : nat), zero + n = n := -- Next, we will show that (suc n) + m = suc (n + m). def plus_s_l (n : nat) : forall (m : nat), suc n + m = suc (n + m) := -- We proceed by induction on m. - nat_ind (fun (m : nat) => suc n + m = suc (n + m)) + nat_ind ([m : nat] suc n + m = suc (n + m)) -- base case: (suc n) + 0 = suc (n + 0) -- suc n + 0 = suc n = suc (n + 0) (eq_trans nat (suc n + zero) (suc n) (suc (n + zero)) @@ -579,7 +579,7 @@ def plus_s_l (n : nat) : forall (m : nat), suc n + m = suc (n + m) := -- Finally, we can prove commutativity. def plus_comm (n : nat) : forall (m : nat), n + m = m + n := -- As usual, we proceed by induction. - nat_ind (fun (m : nat) => n + m = m + n) + nat_ind ([m : nat] n + m = m + n) -- Base case: WTS n + 0 = 0 + n -- n + 0 = n = 0 + n diff --git a/lib/Check.hs b/lib/Check.hs index 01a8e87..c790bfe 100644 --- a/lib/Check.hs +++ b/lib/Check.hs @@ -13,7 +13,7 @@ type Context = [Expr] matchPi :: Expr -> Expr -> ReaderT Env Result (Expr, Expr) matchPi x mt = whnf mt >>= \case - (Pi _ a _ b) -> pure (a, b) + (Pi _ a b) -> pure (a, b) t -> throwError $ ExpectedPiType x t findLevel :: Context -> Expr -> ReaderT Env Result Integer @@ -57,16 +57,14 @@ findType g e@(App m n) = do a' <- findType g n betaEquiv' e a a' pure $ subst 0 n b -findType g f@(Abs x a asc m) = do +findType g (Abs x a m) = do validateType g a b <- findType (incIndices a : map incIndices g) m - whenJust asc (void . liftA2 ($>) (findType g) (betaEquiv' f b)) - validateType g (Pi x a Nothing b) - pure $ if occursFree 0 b then Pi x a Nothing b else Pi "" a Nothing b -findType g f@(Pi _ a asc b) = do + validateType g (Pi x a b) + pure $ if occursFree 0 b then Pi x a b else Pi "" a b +findType g (Pi _ a b) = do aSort <- findType g a bSort <- findType (incIndices a : map incIndices g) b - whenJust asc (void . liftA2 ($>) (findType g) (betaEquiv' f bSort)) liftEither $ compSort a b aSort bSort findType g (Let _ Nothing v b) = findType g (subst 0 v b) findType g e@(Let _ (Just t) v b) = do diff --git a/lib/Elaborator.hs b/lib/Elaborator.hs index 8f85180..04dbb2e 100644 --- a/lib/Elaborator.hs +++ b/lib/Elaborator.hs @@ -102,16 +102,14 @@ usedVars (I.Var name) = do usedVars I.Star = pure S.empty usedVars (I.Level _) = pure S.empty usedVars (I.App m n) = S.union <$> usedVars m <*> usedVars n -usedVars (I.Abs name ty ascr body) = saveState $ do +usedVars (I.Abs name ty body) = saveState $ do ty' <- usedVars ty - ascr' <- traverse usedVars ascr removeName name - S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body -usedVars (I.Pi name ty ascr body) = saveState $ do + S.union ty' <$> usedVars body +usedVars (I.Pi name ty body) = saveState $ do ty' <- usedVars ty - ascr' <- traverse usedVars ascr removeName name - S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body + S.union ty' <$> usedVars body usedVars (I.Let name ascr value body) = saveState $ do ty' <- usedVars value ascr' <- traverse usedVars ascr @@ -129,16 +127,14 @@ traverseBody (I.Var name) = do traverseBody I.Star = pure I.Star traverseBody (I.Level k) = pure $ I.Level k traverseBody (I.App m n) = I.App <$> traverseBody m <*> traverseBody n -traverseBody (I.Abs name ty ascr body) = saveState $ do +traverseBody (I.Abs name ty body) = saveState $ do ty' <- traverseBody ty - ascr' <- traverse traverseBody ascr removeName name - I.Abs name ty' ascr' <$> traverseBody body -traverseBody (I.Pi name ty ascr body) = saveState $ do + I.Abs name ty' <$> traverseBody body +traverseBody (I.Pi name ty body) = saveState $ do ty' <- traverseBody ty - ascr' <- traverse traverseBody ascr removeName name - I.Pi name ty' ascr' <$> traverseBody body + I.Pi name ty' <$> traverseBody body traverseBody (I.Let name ascr value body) = saveState $ do ascr' <- traverse traverseBody ascr value' <- traverseBody value @@ -146,10 +142,10 @@ traverseBody (I.Let name ascr value body) = saveState $ do I.Let name ascr' value' <$> traverseBody body mkPi :: (Text, IRExpr) -> IRExpr -> IRExpr -mkPi (param, typ) = I.Pi param typ Nothing +mkPi (param, typ) = I.Pi param typ mkAbs :: (Text, IRExpr) -> IRExpr -> IRExpr -mkAbs (param, typ) = I.Abs param typ Nothing +mkAbs (param, typ) = I.Abs param typ generalizeType :: IRExpr -> [(Text, IRExpr)] -> IRExpr generalizeType = foldr mkPi @@ -190,16 +186,14 @@ elaborate ir = evalState (elaborate' ir) [] elaborate' I.Star = pure E.Star elaborate' (I.Level level) = pure $ E.Level level elaborate' (I.App m n) = E.App <$> elaborate' m <*> elaborate' n - elaborate' (I.Abs x t a b) = saveBinders $ do + elaborate' (I.Abs x t b) = saveBinders $ do t' <- elaborate' t - a' <- traverse elaborate' a modify (x :) - E.Abs x t' a' <$> elaborate' b - elaborate' (I.Pi x t a b) = saveBinders $ do + E.Abs x t' <$> elaborate' b + elaborate' (I.Pi x t b) = saveBinders $ do t' <- elaborate' t - a' <- traverse elaborate' a modify (x :) - E.Pi x t' a' <$> elaborate' b + E.Pi x t' <$> elaborate' b elaborate' (I.Let name Nothing val body) = saveBinders $ do val' <- elaborate' val modify (name :) diff --git a/lib/Eval.hs b/lib/Eval.hs index 2e2e22c..bc32fa4 100644 --- a/lib/Eval.hs +++ b/lib/Eval.hs @@ -42,8 +42,8 @@ subst _ _ (Axiom s) = Axiom s subst _ _ Star = Star 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 a n) = Abs x (subst k s m) a (subst (k + 1) (incIndices s) n) -subst k s (Pi x m a n) = Pi x (subst k s m) a (subst (k + 1) (incIndices 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 t v b) = Let x t (subst k s v) (subst (k + 1) (incIndices s) b) envLookupVal :: Text -> ReaderT Env Result Expr @@ -53,10 +53,10 @@ envLookupTy :: Text -> ReaderT Env Result Expr envLookupTy n = asks ((_ty <$>) . M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure reduce :: Expr -> ReaderT Env Result Expr -reduce (App (Abs _ _ _ v) n) = pure $ subst 0 n v +reduce (App (Abs _ _ v) n) = pure $ subst 0 n v reduce (App m n) = App <$> reduce m <*> reduce n -reduce (Abs x t a v) = Abs x <$> reduce t <*> pure a <*> reduce v -reduce (Pi x t a v) = Pi x <$> reduce t <*> pure a <*> reduce v +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 e = pure e @@ -70,7 +70,7 @@ normalize e = do -- reduce until β reducts or let simplifications are impossible in head position whnf :: Expr -> ReaderT Env Result Expr -whnf (App (Abs _ _ _ v) n) = whnf $ subst 0 n v +whnf (App (Abs _ _ v) n) = whnf $ subst 0 n v whnf (App m n) = do m' <- whnf m if m == m' @@ -95,8 +95,8 @@ betaEquiv e1 e2 (Star, Star) -> pure True (Level i, Level j) -> pure $ i == j (App m1 n1, App m2 n2) -> (&&) <$> betaEquiv m1 m2 <*> betaEquiv n1 n2 - (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 + (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 (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, false, or redundant diff --git a/lib/Expr.hs b/lib/Expr.hs index 1fbe6db..2a5f1b0 100644 --- a/lib/Expr.hs +++ b/lib/Expr.hs @@ -12,8 +12,8 @@ data Expr where Star :: Expr Level :: Integer -> Expr App :: Expr -> Expr -> Expr - Abs :: Text -> Expr -> Maybe Expr -> Expr -> Expr - Pi :: Text -> Expr -> Maybe Expr -> Expr -> Expr + Abs :: Text -> Expr -> Expr -> Expr + Pi :: Text -> Expr -> Expr -> Expr Let :: Text -> Maybe Expr -> Expr -> Expr -> Expr deriving (Show, Ord) @@ -27,8 +27,8 @@ instance Eq Expr where Star == Star = True (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 - (Pi _ t1 _ b1) == (Pi _ t2 _ b2) = t1 == t2 && b1 == b2 + (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 _ == _ = False @@ -39,8 +39,8 @@ occursFree _ (Axiom _) = False occursFree _ Star = 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 -occursFree n (Pi _ a _ b) = occursFree n a || occursFree (n + 1) 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 shiftIndices :: Integer -> Integer -> Expr -> Expr @@ -52,8 +52,8 @@ shiftIndices _ _ (Axiom s) = Axiom s shiftIndices _ _ Star = Star 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 a n) = Abs x (shiftIndices d c m) a (shiftIndices d (c + 1) n) -shiftIndices d c (Pi x m a n) = Pi x (shiftIndices d c m) a (shiftIndices d (c + 1) 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 t v b) = Let x t (shiftIndices d c v) (shiftIndices d (c + 1) b) incIndices :: Expr -> Expr @@ -79,8 +79,8 @@ dedupNames = go [] go :: [Text] -> Expr -> Expr go bs (Var x k) = Var (varName bs x (fromIntegral k)) k go bs (App m n) = App (go bs m) (go bs n) - go bs (Abs x ty ascr b) = Abs (varName (x : bs) x 0) (go bs ty) (go bs <$> ascr) (go (x : bs) b) - go bs (Pi x ty ascr b) = Pi (varName (x : bs) x 0) (go bs ty) (go bs <$> ascr) (go (x : bs) b) + go bs (Abs x ty b) = Abs (varName (x : bs) x 0) (go bs ty) (go (x : bs) b) + go bs (Pi x ty b) = Pi (varName (x : bs) x 0) (go bs ty) (go (x : bs) b) go bs (Let x ascr val b) = Let (varName (x : bs) x 0) (go bs <$> ascr) (go bs val) (go (x : bs) b) go _ e = e @@ -99,7 +99,7 @@ instance Pretty Binding where pretty (Binding var params body) = group $ parens $ pretty var <+> align (sep (map pretty params)) <+> ":=" <+> pretty body collectLambdas :: Expr -> ([Param], Expr) -collectLambdas (Abs x ty _ body) = (Param x ty : params, final) +collectLambdas (Abs x ty body) = (Param x ty : params, final) where (params, final) = collectLambdas body collectLambdas e = ([], e) @@ -113,14 +113,14 @@ collectLets (Let x _ val body) = (Binding x params' val' : bindings, final) collectLets e = ([], e) collectPis :: Expr -> ([Param], Expr) -collectPis p@(Pi "" _ _ _) = ([], p) -collectPis (Pi x ty _ body) = (Param x ty : params, final) +collectPis p@(Pi "" _ _) = ([], p) +collectPis (Pi x ty body) = (Param x ty : params, final) where (params, final) = collectPis body collectPis e = ([], e) collectArrows :: Expr -> NonEmpty Expr -collectArrows (Pi "" t1 _ t2) = t1 :| toList rest +collectArrows (Pi "" t1 t2) = t1 :| toList rest where rest = collectArrows t2 collectArrows e = pure e @@ -133,10 +133,10 @@ collectApps e = pure e cleanNames :: Expr -> Expr cleanNames (App m n) = App (cleanNames m) (cleanNames n) -cleanNames (Abs x ty a body) = Abs x (cleanNames ty) a (cleanNames body) -cleanNames (Pi x ty a body) - | occursFree 0 body = Pi x (cleanNames ty) a (cleanNames body) - | otherwise = Pi "" ty a (cleanNames body) +cleanNames (Abs x ty body) = Abs x (cleanNames ty) (cleanNames body) +cleanNames (Pi x ty body) + | occursFree 0 body = Pi x (cleanNames ty) (cleanNames body) + | otherwise = Pi "" ty (cleanNames body) cleanNames e = e groupParams :: [Param] -> [ParamGroup] @@ -178,7 +178,7 @@ prettyExpr k expr = case expr of where (top :| rest) = NE.reverse $ collectApps expr application = group $ hang 4 $ prettyExpr 3 top <> line <> align (sep $ map (prettyExpr 4) rest) - Pi "" _ _ _ + Pi "" _ _ | k > 2 -> parens piType | otherwise -> piType where diff --git a/lib/IR.hs b/lib/IR.hs index 525b4ee..6cea276 100644 --- a/lib/IR.hs +++ b/lib/IR.hs @@ -13,13 +13,11 @@ data IRExpr | Abs { absParamName :: Text , absParamType :: IRExpr - , absAscription :: Maybe IRExpr , absBody :: IRExpr } | Pi { piParamName :: Text , piParamType :: IRExpr - , piAscription :: Maybe IRExpr , piBody :: IRExpr } | Let diff --git a/lib/Parser.hs b/lib/Parser.hs index 2d8f07c..e1366b5 100644 --- a/lib/Parser.hs +++ b/lib/Parser.hs @@ -10,7 +10,7 @@ import qualified Data.Text as T import Errors (Error (..)) import IR import Preprocessor -import Text.Megaparsec (MonadParsec (..), ParsecT, ShowErrorComponent (..), choice, errorBundlePretty, label, runParserT, try, between) +import Text.Megaparsec (MonadParsec (..), ParsecT, ShowErrorComponent (..), between, choice, errorBundlePretty, label, runParserT, try) import Text.Megaparsec.Char import qualified Text.Megaparsec.Char.Lexer as L @@ -79,29 +79,37 @@ pSomeParams ident = lexeme $ concat <$> some (pParamGroup ident) pManyParams :: Parser Text -> Parser [Param] pManyParams ident = lexeme $ concat <$> many (pParamGroup ident) -mkAbs :: Maybe IRExpr -> (Text, IRExpr) -> IRExpr -> IRExpr -mkAbs ascription (param, typ) = Abs param typ ascription +mkAbs :: (Text, IRExpr) -> IRExpr -> IRExpr +mkAbs (param, typ) = Abs param typ -mkPi :: Maybe IRExpr -> (Text, IRExpr) -> IRExpr -> IRExpr -mkPi ascription (param, typ) = Pi param typ ascription +mkPi :: (Text, IRExpr) -> IRExpr -> IRExpr +mkPi (param, typ) = Pi param typ pLAbs :: Parser IRExpr pLAbs = lexeme $ label "λ-abstraction" $ do _ <- pKeyword "fun" <|> symbol "λ" params <- pSomeParams pIdentifier - ascription <- optional pAscription _ <- symbol "=>" <|> symbol "⇒" body <- pIRExpr - pure $ foldr (mkAbs ascription) body params + pure $ foldr mkAbs body params + +pALAbs :: Parser IRExpr +pALAbs = lexeme $ label "λ-abstraction" $ do + _ <- symbol "[" + args <- some pIdentifier + _ <- symbol ":" + typ <- pIRExpr + _ <- symbol "]" + body <- pIRExpr + pure $ foldr (mkAbs . (,typ)) body args pPAbs :: Parser IRExpr pPAbs = lexeme $ label "Π-abstraction" $ do _ <- pKeyword "forall" <|> symbol "∏" <|> symbol "∀" params <- pSomeParams pIdentifier - ascription <- optional pAscription symbol "," body <- pIRExpr - pure $ foldr (mkPi ascription) body params + pure $ foldr mkPi body params pBinding :: Parser (Text, Maybe IRExpr, IRExpr) pBinding = lexeme $ label "binding" $ do @@ -114,8 +122,8 @@ pBinding = lexeme $ label "binding" $ do symbol ")" pure ( ident - , flip (foldr (mkPi Nothing)) params <$> ascription - , foldr (mkAbs Nothing) value params + , flip (foldr mkPi) params <$> ascription + , foldr mkAbs value params ) pLet :: Parser IRExpr @@ -190,12 +198,12 @@ pInfix = parseWithPrec 0 Nothing -> fail $ "unknown operator '" ++ toString op ++ "'" pAppTerm :: Parser IRExpr -pAppTerm = lexeme $ choice [pLAbs, pPAbs, pLet, pInfix] +pAppTerm = lexeme $ choice [pLAbs, pALAbs, pPAbs, pLet, pInfix] pIRExpr :: Parser IRExpr pIRExpr = lexeme $ do e <- pAppTerm - option e $ (symbol "->" <|> symbol "→") >> Pi "" e Nothing <$> pIRExpr + option e $ (symbol "->" <|> symbol "→") >> Pi "" e <$> pIRExpr pAscription :: Parser IRExpr pAscription = lexeme $ try $ symbol ":" >> label "type" pIRExpr @@ -205,7 +213,7 @@ pAxiom = lexeme $ label "axiom" $ do pKeyword "axiom" ident <- pIdentifier params <- pManyParams (pIdentifier <|> pSymbol) - ascription <- fmap (flip (foldr (mkPi Nothing)) params) pAscription + ascription <- fmap (flip (foldr mkPi) params) pAscription symbol ";" pure $ Axiom ident ascription @@ -221,11 +229,11 @@ pDef = lexeme $ label "definition" $ do pKeyword "def" ident <- pIdentifier <|> pSymbol params <- pManyParams pIdentifier - ascription <- fmap (flip (foldr (mkPi Nothing)) params) <$> optional pAscription + ascription <- fmap (flip (foldr mkPi) params) <$> optional pAscription symbol ":=" body <- pIRExpr symbol ";" - pure $ Def ident ascription $ foldr (mkAbs Nothing) body params + pure $ Def ident ascription $ foldr mkAbs body params pFixityDec :: Parser () pFixityDec = do