fixed issues in parser, added η-equality for functions

README.md

@@ -22,8 +22,6 @@ A dependently typed system
 
 # TODO
 
-* Parser
-
 * Fun types
   * Id
 

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
-
+        guardS (show a1 ++ " | " ++ show a2) =<< convert (VClos env1 a1) (VClos env2 a2)
-        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)
         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

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),
+  ("suc",   PTSuc),
-  ("⊤-ind", PTTopInd),
+  ("Type",  PTType)
-  ("⊥-ind", PTBotInd),
+]
-  ("ℕ-ind", PTNatInd),
+
-  ("Σ-ind", PTSigInd),
+tokenmap : List (Lexer, PiTokenKind)
-  ("λ",     PTLambda),
+tokenmap = [
-  (".",     PTDot),
+  (exact "⊤-ind", PTTopInd),
-  ("→",     PTArrow),
+  (exact "⊥-ind", PTBotInd),
-  ("Π",     PTPi),
+  (exact "ℕ-ind", PTNatInd),
-  ("Σ",     PTSigma),
+  (exact "Σ-ind", PTSigInd),
-  (",",     PTComma),
+  (is 'λ',        PTLambda),
-  ("(",     PTLParen),
+  (is '.',        PTDot),
-  (")",     PTRParen),
+  (is '→',        PTArrow),
-  (":",     PTColon),
+  (is 'Π',        PTPi),
-  ("≔",     PTDefEq),
+  (is '∏',        PTPi),
-  ("⊤",     PTTop),
+  (is 'Σ',        PTSigma),
-  ("⊥",     PTBot),
+  (is '∑',        PTSigma),
-  ("ℕ",     PTNat),
+  (is ',',        PTComma),
-  ("★",     PTStar)
+  (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

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