From 5994096bb19d29de0bf4085cf209de5568c5f8d3 Mon Sep 17 00:00:00 2001 From: William Ball Date: Sat, 25 Jan 2025 10:39:50 -0800 Subject: [PATCH] Reverted back to commit 2c1f193d777 --- examples/logic.pg | 74 ++++++++++++++++++++++------------------------- lib/Check.hs | 17 +++++++++++ lib/Elaborator.hs | 12 ++++++++ lib/Errors.hs | 2 ++ lib/Eval.hs | 26 +++++++++++++++++ lib/Expr.hs | 20 +++++++++++++ lib/IR.hs | 10 +++++++ lib/Parser.hs | 42 +++++++++------------------ 8 files changed, 135 insertions(+), 68 deletions(-) diff --git a/examples/logic.pg b/examples/logic.pg index bdb58db..c1da0c2 100644 --- a/examples/logic.pg +++ b/examples/logic.pg @@ -11,7 +11,7 @@ def false_elim (A : ★) (contra : false) : A := contra A; -- True -def true : ★ := forall (A : ★), A -> A; +def true : ★ := forall (A : ★), A → A; def true_intro : true := [A : ★][x : A] x; @@ -19,10 +19,10 @@ def true_intro : true := [A : ★][x : A] x; -- Negation -def not (A : ★) : ★ := A -> false; +def not (A : ★) : ★ := A → false; -- introduction rule (kinda just the definition) -def not_intro (A : ★) (h : A -> false) : not A := h; +def not_intro (A : ★) (h : A → false) : not A := h; -- elimination rule def not_elim (A B : ★) (a : A) (na : not A) : B := na a B; @@ -42,31 +42,29 @@ infixl 10 ∧; def and_intro (A B : ★) (a : A) (b : B) : A ∧ B := ; -- left elimination rule -def and_elim_l (A B : ★) (ab : A ∧ B) : A := - ab A (fun (a : A) (b : B) => a); +def and_elim_l (A B : ★) (ab : A ∧ B) : A := π₁ ab; -- right elimination rule -def and_elim_r (A B : ★) (ab : A ∧ B) : B := - ab B (fun (a : A) (b : B) => b); +def and_elim_r (A B : ★) (ab : A ∧ B) : B := π₂ ab; -- -------------------------------------------------------------------------------------------------------------- -- Disjunction -- 2nd order disjunction -def ∨ (A B : ★) : ★ := forall (C : ★), (A -> C) -> (B -> C) -> C; +def ∨ (A B : ★) : ★ := forall (C : ★), (A → C) → (B → C) → C; infixl 5 ∨; -- left introduction rule def or_intro_l (A B : ★) (a : A) : A ∨ B := - fun (C : ★) (ha : A -> C) (hb : B -> C) => ha a; + fun (C : ★) (ha : A → C) (hb : B → C) => ha a; -- right introduction rule def or_intro_r (A B : ★) (b : B) : A ∨ B := - fun (C : ★) (ha : A -> C) (hb : B -> C) => hb b; + fun (C : ★) (ha : A → C) (hb : B → C) => hb b; -- elimination rule (kinda just the definition) -def or_elim (A B C : ★) (ab : A ∨ B) (ha : A -> C) (hb : B -> C) : C := +def or_elim (A B C : ★) (ab : A ∨ B) (ha : A → C) (hb : B → C) : C := ab C ha hb; -- -------------------------------------------------------------------------------------------------------------- @@ -74,14 +72,14 @@ def or_elim (A B C : ★) (ab : A ∨ B) (ha : A -> C) (hb : B -> C) : C := -- Existential -- 2nd order existential -def exists (A : ★) (P : A -> ★) : ★ := forall (C : ★), (forall (x : A), P x -> C) -> C; +def exists (A : ★) (P : A → ★) : ★ := forall (C : ★), (forall (x : A), P x → C) → C; -- introduction rule -def exists_intro (A : ★) (P : A -> ★) (a : A) (h : P a) : exists A P := - fun (C : ★) (g : forall (x : A), P x -> C) => g a h; +def exists_intro (A : ★) (P : A → ★) (a : A) (h : P a) : exists A P := + fun (C : ★) (g : forall (x : A), P x → C) => g a h; -- elimination rule (kinda just the definition) -def exists_elim (A B : ★) (P : A -> ★) (ex_a : exists A P) (h : forall (a : A), P a -> B) : B := +def exists_elim (A B : ★) (P : A → ★) (ex_a : exists A P) (h : forall (a : A), P a → B) : B := ex_a B h; -- -------------------------------------------------------------------------------------------------------------- @@ -89,53 +87,53 @@ def exists_elim (A B : ★) (P : A -> ★) (ex_a : exists A P) (h : forall (a : -- Universal -- 2nd order universal (just ∏, including it for completeness) -def all (A : ★) (P : A -> ★) : ★ := forall (a : A), P a; +def all (A : ★) (P : A → ★) : ★ := forall (a : A), P a; -- introduction rule -def all_intro (A : ★) (P : A -> ★) (h : forall (a : A), P a) : all A P := h; +def all_intro (A : ★) (P : A → ★) (h : forall (a : A), P a) : all A P := h; -- elimination rule -def all_elim (A : ★) (P : A -> ★) (h_all : all A P) (a : A) : P a := h_all a; +def all_elim (A : ★) (P : A → ★) (h_all : all A P) (a : A) : P a := h_all a; -- -------------------------------------------------------------------------------------------------------------- -- Equality -- 2nd order Leibniz equality -def 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; -- equality is reflexive -def 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; -- equality is symmetric -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_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; -- equality is transitive -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) => +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); -- equality is a universal congruence -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)) => +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; -- -------------------------------------------------------------------------------------------------------------- -- unique existence -def exists_uniq (A : ★) (P : A -> ★) : ★ := - exists A (fun (x : A) => P x ∧ (forall (y : A), P y -> eq A x y)); +def exists_uniq (A : ★) (P : A → ★) : ★ := + exists A (fun (x : A) => P x ∧ (forall (y : A), P y → eq A x y)); -def exists_uniq_elim (A B : ★) (P : A -> ★) (ex_a : exists_uniq A P) (h : forall (a : A), P a -> (forall (y : A), P y -> eq A a y) -> B) : B := - exists_elim A B (fun (x : A) => P x ∧ (forall (y : A), P y -> eq A x y)) ex_a - (fun (a : A) (h2 : P a ∧ (forall (y : A), P y -> eq A a y)) => - h a (and_elim_l (P a) (forall (y : A), P y -> eq A a y) h2) - (and_elim_r (P a) (forall (y : A), P y -> eq A a y) h2)); +def exists_uniq_elim (A B : ★) (P : A → ★) (ex_a : exists_uniq A P) (h : forall (a : A), P a → (forall (y : A), P y → eq A a y) → B) : B := + exists_elim A B (fun (x : A) => P x ∧ (forall (y : A), P y → eq A x y)) ex_a + (fun (a : A) (h2 : P a ∧ (forall (y : A), P y → eq A a y)) => + h a (and_elim_l (P a) (forall (y : A), P y → eq A a y) h2) + (and_elim_r (P a) (forall (y : A), P y → eq A a y) h2)); def exists_uniq_t (A : ★) : ★ := exists A (fun (x : A) => forall (y : A), eq A x y); -def exists_uniq_t_elim (A B : ★) (ex_a : exists_uniq_t A) (h : forall (a : A), (forall (y : A), eq A a y) -> B) : B := +def exists_uniq_t_elim (A B : ★) (ex_a : exists_uniq_t A) (h : forall (a : A), (forall (y : A), eq A a y) → B) : B := exists_elim A B (fun (x : A) => forall (y : A), eq A x y) ex_a (fun (a : A) (h2 : forall (y : A), eq A a y) => h a h2); -- -------------------------------------------------------------------------------------------------------------- @@ -154,16 +152,14 @@ section Theorems -- ~A ∧ ~B => ~(A ∨ B) def de_morgan2 (h : not A ∧ not B) : not (A ∨ B) := fun (contra : A ∨ B) => - or_elim A B false contra - (and_elim_l (not A) (not B) h) - (and_elim_r (not A) (not B) h); + or_elim A B false contra (π₁ h) (π₂ h); -- ~A ∨ ~B => ~(A ∧ B) def de_morgan3 (h : not A ∨ not B) : not (A ∧ B) := fun (contra : A ∧ B) => or_elim (not A) (not B) false h - (fun (na : not A) => na (and_elim_l A B contra)) - (fun (nb : not B) => nb (and_elim_r A B contra)); + (fun (na : not A) => na (π₁ contra)) + (fun (nb : not B) => nb (π₂ contra)); -- the last one (~(A ∧ B) => ~A ∨ ~B) is not possible constructively @@ -220,7 +216,7 @@ section Theorems 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 := + def contrapositive (f : A → B) (nb : not B) : not A := fun (a : A) => nb (f a); end Theorems diff --git a/lib/Check.hs b/lib/Check.hs index c790bfe..55ecce0 100644 --- a/lib/Check.hs +++ b/lib/Check.hs @@ -16,6 +16,12 @@ matchPi x mt = (Pi _ a b) -> pure (a, b) t -> throwError $ ExpectedPiType x t +matchProd :: Expr -> Expr -> ReaderT Env Result (Expr, Expr) +matchProd x mt = + whnf mt >>= \case + (Prod a b) -> pure (a, b) + t -> throwError $ ExpectedProdType x t + findLevel :: Context -> Expr -> ReaderT Env Result Integer findLevel g a = do s <- findType g a @@ -72,6 +78,17 @@ findType g e@(Let _ (Just t) v b) = do _ <- findType g t betaEquiv' e t res pure t +findType g (Prod a b) = do + aSort <- findType g a + bSort <- findType g b + liftEither $ compSort a b aSort bSort +findType g (Pair a b) = do + aType <- findType g a + bType <- findType g b + validateType g $ Prod aType bType + pure $ Prod aType bType +findType g (Pi1 x) = fst <$> (findType g x >>= matchProd x) +findType g (Pi2 x) = snd <$> (findType g x >>= matchProd x) checkType :: Env -> Expr -> Result Expr checkType env t = runReaderT (findType [] t) env diff --git a/lib/Elaborator.hs b/lib/Elaborator.hs index 9d2492f..b0cc77d 100644 --- a/lib/Elaborator.hs +++ b/lib/Elaborator.hs @@ -116,6 +116,10 @@ usedVars (I.Let name ascr value body) = saveState $ do ascr' <- traverse usedVars ascr removeName name S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body +usedVars (I.Prod m n) = S.union <$> usedVars m <*> usedVars n +usedVars (I.Pair m n) = S.union <$> usedVars m <*> usedVars n +usedVars (I.Pi1 x) = usedVars x +usedVars (I.Pi2 x) = usedVars x -- traverse the body of a definition, adding the necessary section arguments to -- any definitions made within the section @@ -142,6 +146,10 @@ traverseBody (I.Let name ascr value body) = saveState $ do value' <- traverseBody value removeName name I.Let name ascr' value' <$> traverseBody body +traverseBody (I.Prod m n) = I.Prod <$> traverseBody m <*> traverseBody n +traverseBody (I.Pair m n) = I.Pair <$> traverseBody m <*> traverseBody n +traverseBody (I.Pi1 x) = I.Pi1 <$> traverseBody x +traverseBody (I.Pi2 x) = I.Pi2 <$> traverseBody x mkPi :: (Text, IRExpr) -> IRExpr -> IRExpr mkPi (param, typ) = I.Pi param typ @@ -206,3 +214,7 @@ elaborate ir = evalState (elaborate' ir) [] ty' <- elaborate' ty modify (name :) E.Let name (Just ty') val' <$> elaborate' body + elaborate' (I.Prod m n) = E.Prod <$> elaborate' m <*> elaborate' n + elaborate' (I.Pair m n) = E.Pair <$> elaborate' m <*> elaborate' n + elaborate' (I.Pi1 x) = E.Pi1 <$> elaborate' x + elaborate' (I.Pi2 x) = E.Pi2 <$> elaborate' x diff --git a/lib/Errors.hs b/lib/Errors.hs index a4a91a2..298f4d5 100644 --- a/lib/Errors.hs +++ b/lib/Errors.hs @@ -9,6 +9,7 @@ data Error = UnboundVariable Text | NotASort Expr | ExpectedPiType Expr Expr + | ExpectedProdType Expr Expr | NotEquivalent Expr Expr Expr | PNMissingType Text | DuplicateDefinition Text @@ -18,6 +19,7 @@ instance Pretty Error where pretty (UnboundVariable x) = "Unbound variable: '" <> pretty x <> "'" pretty (NotASort x) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> "is not a type" pretty (ExpectedPiType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> hang 4 ("is not a function, instead is type" <> line <> pretty t) + pretty (ExpectedProdType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> hang 4 ("is not a pair, instead is type" <> line <> pretty t) pretty (NotEquivalent a a' e) = group $ hang 4 ("Cannot unify" <> line <> pretty a) diff --git a/lib/Eval.hs b/lib/Eval.hs index bc32fa4..51d4060 100644 --- a/lib/Eval.hs +++ b/lib/Eval.hs @@ -45,6 +45,10 @@ 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 t v b) = Let x t (subst k s v) (subst (k + 1) (incIndices s) b) +subst k s (Prod m n) = Prod (subst k s m) (subst k s n) +subst k s (Pair m n) = Pair (subst k s m) (subst k s n) +subst k s (Pi1 x) = Pi1 (subst k s x) +subst k s (Pi2 x) = Pi2 (subst k s x) envLookupVal :: Text -> ReaderT Env Result Expr envLookupVal n = asks ((_val <$>) . M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure @@ -59,6 +63,12 @@ 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 (Prod a b) = Prod <$> reduce a <*> reduce b +reduce (Pair a b) = Pair <$> reduce a <*> reduce b +reduce (Pi1 (Pair a _)) = pure a +reduce (Pi2 (Pair _ b)) = pure b +reduce (Pi1 x) = Pi1 <$> reduce x +reduce (Pi2 x) = Pi2 <$> reduce x reduce e = pure e normalize :: Expr -> ReaderT Env Result Expr @@ -78,6 +88,18 @@ whnf (App m n) = do else whnf $ App m' n whnf (Free n) = envLookupVal n >>= whnf whnf (Let _ _ v b) = whnf $ subst 0 v b +whnf (Pi1 (Pair a _)) = pure a +whnf (Pi2 (Pair _ b)) = pure b +whnf (Pi1 x) = do + x' <- whnf x + if x == x' + then pure $ Pi1 x + else whnf $ Pi1 x' +whnf (Pi2 x) = do + x' <- whnf x + if x == x' + then pure $ Pi2 x + else whnf $ Pi2 x' whnf e = pure e betaEquiv :: Expr -> Expr -> ReaderT Env Result Bool @@ -99,6 +121,10 @@ betaEquiv e1 e2 (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 + (Prod a b, Prod a' b') -> (&&) <$> betaEquiv a a' <*> betaEquiv b b' + (Pair a b, Pair a' b') -> (&&) <$> betaEquiv a a' <*> betaEquiv b b' + (Pi1 x, Pi1 x') -> betaEquiv x x' + (Pi2 x, Pi2 x') -> betaEquiv x x' _ -> pure False -- remaining cases impossible, false, or redundant betaEquiv' :: Expr -> Expr -> Expr -> ReaderT Env Result () diff --git a/lib/Expr.hs b/lib/Expr.hs index 2bb721b..5fce231 100644 --- a/lib/Expr.hs +++ b/lib/Expr.hs @@ -15,6 +15,10 @@ data Expr where Abs :: Text -> Expr -> Expr -> Expr Pi :: Text -> Expr -> Expr -> Expr Let :: Text -> Maybe Expr -> Expr -> Expr -> Expr + Prod :: Expr -> Expr -> Expr + Pair :: Expr -> Expr -> Expr + Pi1 :: Expr -> Expr + Pi2 :: Expr -> Expr deriving (Show, Ord) instance Pretty Expr where @@ -30,6 +34,10 @@ instance Eq Expr where (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 + (Prod x1 y1) == (Prod x2 y2) = x1 == x2 && y1 == y2 + (Pair x1 y1) == (Pair x2 y2) = x1 == x2 && y1 == y2 + (Pi1 x) == (Pi1 y) = x == y + (Pi2 x) == (Pi2 y) = x == y _ == _ = False occursFree :: Integer -> Expr -> Bool @@ -42,6 +50,10 @@ 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 (Prod x y) = occursFree n x || occursFree n y +occursFree n (Pair x y) = occursFree n x || occursFree n y +occursFree n (Pi1 x) = occursFree n x +occursFree n (Pi2 x) = occursFree n x shiftIndices :: Integer -> Integer -> Expr -> Expr shiftIndices d c (Var x k) @@ -55,6 +67,10 @@ 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 t v b) = Let x t (shiftIndices d c v) (shiftIndices d (c + 1) b) +shiftIndices d c (Prod m n) = Prod (shiftIndices d c m) (shiftIndices d c n) +shiftIndices d c (Pair m n) = Pair (shiftIndices d c m) (shiftIndices d c n) +shiftIndices d c (Pi1 x) = Pi1 (shiftIndices d c x) +shiftIndices d c (Pi2 x) = Pi2 (shiftIndices d c x) incIndices :: Expr -> Expr incIndices = shiftIndices 1 0 @@ -206,6 +222,10 @@ prettyExpr k expr = case expr of where (binds, body) = collectLets expr bindings = sep $ map pretty binds + (Prod x y) -> parens $ parens (pretty x) <+> "×" <+> parens (pretty y) + (Pair x y) -> parens $ pretty x <> "," <+> pretty y + (Pi1 x) -> parens $ "π₁" <+> parens (pretty x) + (Pi2 x) -> parens $ "π₂" <+> parens (pretty x) prettyT :: Expr -> Text prettyT = renderStrict . layoutSmart defaultLayoutOptions . pretty diff --git a/lib/IR.hs b/lib/IR.hs index ae654a0..c0c45e2 100644 --- a/lib/IR.hs +++ b/lib/IR.hs @@ -27,6 +27,16 @@ data IRExpr , letValue :: IRExpr , letBody :: IRExpr } + | Prod + { prodLeft :: IRExpr + , prodRight :: IRExpr + } + | Pair + { pairLeft :: IRExpr + , pairRight :: IRExpr + } + | Pi1 IRExpr + | Pi2 IRExpr deriving (Show, Eq, Ord) data IRSectionDef diff --git a/lib/Parser.hs b/lib/Parser.hs index c5974f5..e0605ef 100644 --- a/lib/Parser.hs +++ b/lib/Parser.hs @@ -17,25 +17,12 @@ import qualified Text.Megaparsec.Char.Lexer as L newtype TypeError = TE Error deriving (Eq, Ord) -data InfixDef = InfixDef - { infixFixity :: Fixity - , infixOp :: Text -> IRExpr -> IRExpr -> IRExpr - } - data Fixity = InfixL Int | InfixR Int deriving (Eq, Show) -type Operators = Map Text InfixDef - -initialOps :: Operators -initialOps = - M.fromAscList - [ ("→", InfixDef (InfixR 2) (const $ Pi "")) - , ("->", InfixDef (InfixR 2) (const $ Pi "")) - , ("×", InfixDef (InfixL 10) (const Prod)) - ] +type Operators = Map Text Fixity type Parser = ParsecT TypeError Text (State Operators) @@ -59,7 +46,7 @@ symbol :: Text -> Parser () symbol = void . L.symbol skipSpace symbols :: String -symbols = "→!@#$%^&*-+=<>,./?[]{}\\|`~'\"∧∨⊙×≅" +symbols = "!@#$%^&*-+=<>,./?[]{}\\|`~'\"∧∨⊙×≅" pKeyword :: Text -> Parser () pKeyword keyword = void $ lexeme (string keyword <* notFollowedBy alphaNumChar) @@ -219,7 +206,7 @@ pInfix = parseWithPrec 0 op <- lookAhead pSymbol operators <- get case M.lookup op operators of - Just (InfixDef fixity opFun) -> do + Just fixity -> do let (opPrec, nextPrec) = case fixity of InfixL p -> (p, p) InfixR p -> (p, p + 1) @@ -228,19 +215,16 @@ pInfix = parseWithPrec 0 else do _ <- pSymbol rhs <- parseWithPrec nextPrec - continue prec $ opFun op lhs rhs + continue prec (App (App (Var op) lhs) rhs) Nothing -> fail $ "unknown operator '" ++ toString op ++ "'" -pIRExpr :: Parser IRExpr -pIRExpr = lexeme $ choice [pLAbs, pALAbs, pPAbs, pLet, pInfix] +pAppTerm :: Parser IRExpr +pAppTerm = lexeme $ choice [pLAbs, pALAbs, pPAbs, pLet, pInfix] --- pAppTerm :: Parser IRExpr --- pAppTerm = lexeme $ choice [pLAbs, pALAbs, pPAbs, pLet, pInfix] --- --- pIRExpr :: Parser IRExpr --- pIRExpr = lexeme $ do --- e <- pAppTerm --- option e $ (symbol "->" <|> symbol "→") >> Pi "" e <$> pIRExpr +pIRExpr :: Parser IRExpr +pIRExpr = lexeme $ do + e <- pAppTerm + option e $ (symbol "->" <|> symbol "→") >> Pi "" e <$> pIRExpr pAscription :: Parser IRExpr pAscription = lexeme $ try $ symbol ":" >> label "type" pIRExpr @@ -248,7 +232,7 @@ pAscription = lexeme $ try $ symbol ":" >> label "type" pIRExpr pAxiom :: Parser IRDef pAxiom = lexeme $ label "axiom" $ do pKeyword "axiom" - ident <- pIdentifier <|> pSymbol + ident <- pIdentifier params <- pManyParams ascription <- fmap (flip (foldr mkPi) params) pAscription symbol ";" @@ -281,7 +265,7 @@ pFixityDec = do , InfixR <$> (lexeme (char 'r') >> lexeme L.decimal) ] ident <- pSymbol - modify $ M.insert ident $ InfixDef fixity $ (App .) . App . Var + modify (M.insert ident fixity) symbol ";" pSection :: Parser IRSectionDef @@ -300,7 +284,7 @@ pIRProgram :: Parser IRProgram pIRProgram = skipSpace >> concat <$> some pIRDef parserWrapper :: Parser a -> String -> Text -> Either String a -parserWrapper p filename input = first errorBundlePretty $ evalState (runParserT p filename input) initialOps +parserWrapper p filename input = first errorBundlePretty $ evalState (runParserT p filename input) M.empty parseProgram :: String -> Text -> Either String IRProgram parseProgram = parserWrapper pIRProgram