From 48e9a474ff71fd56b8592a71614166523c864b3c Mon Sep 17 00:00:00 2001 From: depsterr Date: Sat, 23 Jul 2022 06:01:17 +0200 Subject: [PATCH] =?UTF-8?q?fixed=20issues=20in=20parser,=20added=20=CE=B7-?= =?UTF-8?q?equality=20for=20functions?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- README.md | 2 - src/Core/Convert.idr | 33 ++++++++-------- src/Parser/Parse.idr | 80 ++++++++++++++++++++++++--------------- src/Parser/Tests.idr | 89 ++++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 156 insertions(+), 48 deletions(-) create mode 100644 src/Parser/Tests.idr diff --git a/README.md b/README.md index 177bb99..954f58c 100644 --- a/README.md +++ b/README.md @@ -22,8 +22,6 @@ A dependently typed system # TODO -* Parser - * Fun types * Id diff --git a/src/Core/Convert.idr b/src/Core/Convert.idr index fb06399..c293a95 100644 --- a/src/Core/Convert.idr +++ b/src/Core/Convert.idr @@ -23,38 +23,28 @@ convert u1 u2 = do logS ("with value representations '" ++ show u1' ++ "' and '" ++ show u2' ++ "'.") assert_total $ -- :( case (u1', u2') of + (VGen k1, VGen k2) => pure (k1 == k2) (VType, VType) => pure True (VTop, VTop) => pure True (VStar, VStar) => pure True (VBot, VBot) => pure True (VNat, VNat) => pure True - (VNatTr n, VNatTr m) => pure (n == m) - (VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2 <*> delay <$> convert x1 x2 - (VGen k1, VGen k2) => pure (k1 == k2) - - (VPair a1 b1, VPair a2 b2) => (&&) <$> convert a1 a2 <*> delay <$> convert b1 b2 - (VClos env1 (TLam sc1), VClos env2 (TLam sc2)) => do v <- VGen <$> fresh convert (VClos (v :: env1) sc1) (VClos (v :: env2) sc2) (VClos env1 (TPi a1 b1), VClos env2 (TPi a2 b2)) => do v <- VGen <$> fresh - - s1 <- case headM env1 of - Nothing => pure "" - Just x => pure (show x) - - s2 <- case headM env2 of - Nothing => pure "" - Just x => pure (show x) - - guardS (s1 ++ " | " ++ s2) =<< convert (VClos env1 a1) (VClos env2 a2) + guardS (show a1 ++ " | " ++ show a2) =<< convert (VClos env1 a1) (VClos env2 a2) convert (VClos (v :: env1) b1) (VClos (v :: env2) b2) + (VNatTr n, VNatTr m) => pure (n == m) + + (VPair a1 b1, VPair a2 b2) => (&&) <$> convert a1 a2 <*> delay <$> convert b1 b2 + (VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do termGuard env1 env2 c1 c2 termConv env1 env2 st1 st2 @@ -75,7 +65,16 @@ convert u1 u2 = do termGuard env1 env2 b1 b2 termGuard env1 env2 c1 c2 termConv env1 env2 f1 f2 - + + -- η rules + -- fresh cannot appear in vsc, so this is fine + (vsc, VClos env (TLam (TApp sc (TVar 0)))) => do + v <- VGen <$> fresh + convert vsc (VClos (v :: env) sc) + (VClos env (TLam (TApp sc (TVar 0))), vsc) => do + v <- VGen <$> fresh + convert vsc (VClos (v :: env) sc) + _ => pure False where termConv : Ctx n -> Ctx m -> Term n -> Term m -> PI Bool diff --git a/src/Parser/Parse.idr b/src/Parser/Parse.idr index 60f3260..e492d38 100644 --- a/src/Parser/Parse.idr +++ b/src/Parser/Parse.idr @@ -138,35 +138,44 @@ ignored (MkBounded (Tok PTIgnore _) _ _) = True ignored _ = False identifier : Lexer -identifier = some (alphaNum <|> symbol) +identifier = some (alphaNum <|> oneOf "-_") keywords : List (String, PiTokenKind) keywords = [ ("in", PTIn), ("let", PTLet), - ("Type", PTType), - ("⊤-ind", PTTopInd), - ("⊥-ind", PTBotInd), - ("ℕ-ind", PTNatInd), - ("Σ-ind", PTSigInd), - ("λ", PTLambda), - (".", PTDot), - ("→", PTArrow), - ("Π", PTPi), - ("Σ", PTSigma), - (",", PTComma), - ("(", PTLParen), - (")", PTRParen), - (":", PTColon), - ("≔", PTDefEq), - ("⊤", PTTop), - ("⊥", PTBot), - ("ℕ", PTNat), - ("★", PTStar) + ("suc", PTSuc), + ("Type", PTType) +] + +tokenmap : List (Lexer, PiTokenKind) +tokenmap = [ + (exact "⊤-ind", PTTopInd), + (exact "⊥-ind", PTBotInd), + (exact "ℕ-ind", PTNatInd), + (exact "Σ-ind", PTSigInd), + (is 'λ', PTLambda), + (is '.', PTDot), + (is '→', PTArrow), + (is 'Π', PTPi), + (is '∏', PTPi), + (is 'Σ', PTSigma), + (is '∑', PTSigma), + (is ',', PTComma), + (is '(', PTLParen), + (is ')', PTRParen), + (is ':', PTColon), + (is '≔', PTDefEq), + (is '⊤', PTTop), + (is '⊥', PTBot), + (is 'ℕ', PTNat), + (is '★', PTStar), + (is '0', PTZero) ] piTokenMap : TokenMap PiToken piTokenMap = (spaces, Tok PTIgnore) :: + toTokenMap tokenmap ++ [(identifier, \s => case lookup s keywords of (Just kind) => Tok kind s @@ -184,7 +193,13 @@ lexPi str = {- de bruijn indecies, and a Nat to keep track of context size -} mutual expr : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) - expr n env = ttopind n env + expr n env = tpi n env + <|> tsigma n env + <|> tarr n env + <|> expr1 n env + + expr1 : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + expr1 n env = ttopind n env <|> tbotind n env <|> tsuc n env <|> tnatind n env @@ -200,11 +215,9 @@ mutual <|> tbot <|> tnat <|> tzero - <|> tsigma n env <|> tpair n env <|> tlet n env <|> tlam n env - <|> tpi n env <|> tvar n env <|> paren n env @@ -264,17 +277,17 @@ mutual match PTLParen arg <- match PTIdentifier match PTColon - a <- term n env + a <- expr n env match PTRParen - b <- term (S n) (arg :: env) + b <- expr (S n) (arg :: env) pure (TSigma a (TLam b)) tpair : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) tpair n env = do match PTLParen - commit x <- expr n env match PTComma + commit y <- expr n env match PTRParen pure (TPair x y) @@ -308,7 +321,7 @@ mutual commit arg <- match PTIdentifier match PTDot - e <- term (S n) (arg :: env) + e <- expr (S n) (arg :: env) pure (TLam e) tpi : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) @@ -318,11 +331,19 @@ mutual match PTLParen arg <- match PTIdentifier match PTColon - a <- term n env + a <- expr n env match PTRParen - b <- term (S n) (arg :: env) + b <- expr (S n) (arg :: env) pure (TPi a b) + tarr : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) + tarr n env = do + l <- expr1 n env + match PTArrow + commit + r <- expr (S n) ("" :: env) + pure (TPi l r) + tapp : (n : Nat) -> Vect n String -> Term n -> Grammar state PiToken True (Term n) tapp n env e1 = do e2 <- term n env @@ -339,6 +360,7 @@ mutual paren : (n : Nat) -> Vect n String -> Grammar state PiToken True (Term n) paren n env = do match PTLParen + commit e <- expr n env match PTRParen pure e diff --git a/src/Parser/Tests.idr b/src/Parser/Tests.idr new file mode 100644 index 0000000..ffa4823 --- /dev/null +++ b/src/Parser/Tests.idr @@ -0,0 +1,89 @@ +module Parser.Tests + +import Core.Term +import Core.Check +import Core.Convert +import Core.Misc +import Core.Normalize +import Core.Value + +import Control.Monad.RWS +import Control.Monad.Identity +import Control.Monad.Either + +import Data.Fin + +import Parser.Parse + +%default total + +convCheck : Term 0 -> Term 0 -> Either String (Bool, List String) +convCheck a b = resolve action + where + action : PI Bool + action = do + x <- eval ctx0 a + y <- eval ctx0 b + convert x y + +{- λA. λx. x : ∏ (A : Type) → A → A -} +test_id : Either String (Bool, List String) +test_id = do + ty <- parse0 "Π ( A : Type ) A → A" + tr <- parse0 "λA.λx.x" + typecheck tr ty + +{- λA. λB. λf. λx. f x : ∏ (A : Type) ∏ (B : A → Type) ∏ (f : ∏ (x : A) B x) ∏ (x : A) B x -} +test_app : Either String (Bool, List String) +test_app = do + ty <- parse0 "Π (A : Type) Π (B : A → Type) Π (f : Π (x : A) B x) Π (x : A) B x" + tr <- parse0 "λA. λB. λf. λx. f x" + typecheck tr ty + +{- λf. f ≃ λf. λx. f x -} +eta_test : Either String (Bool, List String) +eta_test = do + a <- parse0 "λf. f" + b <- parse0 "λf. λx. f x" + convCheck a b + +additionty_test : Either String (Bool, List String) +additionty_test = do + ty <- parse0 "ℕ → ℕ → ℕ" + typecheck ty TType + +addition_test : Either String (Bool, List String) +addition_test = do + ty <- parse0 "ℕ → ℕ → ℕ" + tr <- parse0 "ℕ-ind (λ_. ℕ → ℕ) (λx.x) (λn.λnp.λm. suc (np m))" + typecheck tr ty + +-- no, not that kind +unit_test : Either String (Bool, List String) +unit_test = do + ty <- parse0 "⊤" + tr <- parse0 "★" + typecheck tr ty + +absurd_test : Either String (Bool, List String) +absurd_test = do + ty <- parse0 "Π(A : Type) ⊥ → A" + tr <- parse0 "λA. ⊥-ind (λ_. A)" + typecheck tr ty + + +pr1_test : Either String (Bool, List String) +pr1_test = do + tr <- parse0 $ "let pr1 : Π (A : Type) Π (B : A → Type) (Σ (a : A) B a) → A" + ++ "≔ λA.λB. Σ-ind A B (λ_. A) (λa.λBa. a)" + ++ "in ★" + typecheck tr TTop + +pr1_pr2_test : Either String (Bool, List String) +pr1_pr2_test = do + tr <- parse0 $ "let pr1 : Π (A : Type) Π (B : A → Type) (Σ (a : A) B a) → A" + ++ "≔ λA.λB. Σ-ind A B (λ_. A) (λa.λBa. a)" + ++ "in let pr2 : Π (A : Type) Π (B : A → Type) Π (s : Σ (a : A) B a) B (pr1 A B s)" + ++ "≔ λA.λB. Σ-ind A B (λs. B (pr1 A B s)) (λa.λBa. Ba)" + ++ "in ★" + typecheck tr TTop