more tests and minor cleanup

lib/Check.hs

@@ -1,6 +1,6 @@
-module Check where
+module Check (TypeCheckError (..), CheckResult (..), findType) where
 
-import Control.Monad.Except
+import Control.Monad.Except ( MonadError(throwError) )
 import Data.List (intercalate, (!?))
 
 import Control.Monad (unless)

lib/Expr.hs

@@ -22,16 +22,6 @@ instance Eq Expr where
     (Pi _ t1 b1) == (Pi _ t2 b2) = t1 == t2 && b1 == b2
     _ == _ = False
 
-infixl 4 <.>
-
-(<.>) :: Expr -> Expr -> Expr
-(<.>) = App
-
-infixr 2 .->
-
-(.->) :: Expr -> Expr -> Expr
-a .-> b = Pi "" a (incIndices b)
-
 occursFree :: Integer -> Expr -> Bool
 occursFree n (Var k _) = n == k
 occursFree _ Star = False

lib/Parser.hs

@@ -1,4 +1,4 @@
-module Parser where
+module Parser (pAll) where
 
 import Control.Monad
 import Control.Monad.State.Strict
@@ -7,7 +7,7 @@ import Data.Functor.Identity
 import Data.List (elemIndex)
 import Data.List.NonEmpty (NonEmpty ((:|)))
 import qualified Data.List.NonEmpty as NE
-import Expr (Expr (..), incIndices, (.->))
+import Expr (Expr (..), incIndices)
 import Text.Megaparsec hiding (State)
 import Text.Megaparsec.Char
 import qualified Text.Megaparsec.Char.Lexer as L
@@ -84,8 +84,7 @@ pArrow :: Parser Expr
 pArrow = lexeme $ label "->" $ do
     a <- pAppTerm
     _ <- defChoice $ "->" :| ["→"]
-    b <- pExpr
+    Pi "" a . incIndices <$> pExpr
-    pure $ a .-> b
 
 pApp :: Parser Expr
 pApp = foldl1 App <$> some pTerm

tests/ExprTests.hs

@@ -1,10 +1,10 @@
-module ExprTests where
+module ExprTests (tests) where
 
 import Expr
 import Test.HUnit
 
 inner :: Expr
-inner = Abs "x" (Var 0 "A") $ Var 2 "f" <.> Var 0 "x"
+inner = Abs "x" (Var 0 "A") $ App (Var 2 "f") (Var 0 "x")
 
 e1 :: Expr
 e1 = Abs "A" Star inner
@@ -19,12 +19,12 @@ incE1 =
             "incIndices e1"
             ( Abs "A" Star $
                 Abs "x" (Var 0 "A") $
-                    Var 3 "f" <.> Var 0 "x"
+                    App (Var 3 "f") (Var 0 "x")
             )
             (incIndices e1)
 
 after :: Expr
-after = Abs "x" (Var 2 "B") $ Var 1 "f" <.> Var 0 "x"
+after = Abs "x" (Var 2 "B") $ App (Var 1 "f") (Var 0 "x")
 
 substE1 :: Test
 substE1 =
@@ -40,7 +40,7 @@ betaNFe1 =
         assertEqual
             "e1 B"
             after
-            (betaNF $ e1 <.> Var 2 "B")
+            (betaNF $ App e1 $ Var 2 "B")
 
 tests :: Test
 tests =

tests/ParserTests.hs

@@ -1 +1,70 @@
-module ParserTests where
+module ParserTests (tests) where
+
+import Expr (Expr (..))
+import Parser (pAll)
+import Test.HUnit
+
+ident :: Expr
+ident =
+    Abs "A" Star $
+        Abs "x" (Var 0 "A") $
+            Var 0 "x"
+
+ident1 :: Test
+ident1 =
+    TestCase $
+        assertEqual
+            "ident 1"
+            (Right ident)
+            (pAll "lambda (A : *) . lambda (x : A) . x")
+
+ident2 :: Test
+ident2 =
+    TestCase $
+        assertEqual
+            "ident 2"
+            (Right ident)
+            (pAll "fun (A : *) (x : A) => x")
+
+double :: Expr
+double =
+    Abs "A" Star $
+        Abs "B" Star $
+            Abs "f" (Pi "" (Var 1 "A") (Var 1 "B")) $
+                Abs "g" (Pi "" (Var 2 "A") (Var 2 "B")) $
+                    Abs "x" (Var 3 "A") $
+                        App (Var 2 "f") (Var 0 "x")
+
+doubleTest :: Test
+doubleTest =
+    TestCase $
+        assertEqual
+            "double"
+            (Right double)
+            (pAll "fun (A B : *) (f g : A -> B) (x : A) => f x")
+
+theorem :: Expr
+theorem =
+    Abs "S" Star $
+        Abs "P" (Pi "" (Var 0 "S") Star) $
+            Abs "Q" (Pi "" (Var 1 "S") Star) $
+                Abs "HP" (Pi "x" (Var 2 "S") (App (Var 2 "P") (Var 0 "x"))) $
+                    Abs "H" (Pi "x" (Var 3 "S") (Pi "" (App (Var 3 "P") (Var 0 "x")) (App (Var 3 "Q") (Var 1 "x")))) $
+                        Abs "x" (Var 4 "S") (App (App (Var 1 "H") (Var 0 "x")) (App (Var 2 "HP") (Var 0 "x")))
+
+theoremTest :: Test
+theoremTest =
+    TestCase $
+        assertEqual
+            "theorem"
+            (Right theorem)
+            (pAll "fun (S : *) (P Q : S -> *) (HP : ∏ (x : S) . P x) (H : forall (x : S), P x -> Q x) (x : S) => H x (HP x)")
+
+tests :: Test
+tests =
+    TestList
+        [ TestLabel "ident1" ident1
+        , TestLabel "ident2" ident2
+        , TestLabel "double" doubleTest
+        , TestLabel "theorem" theoremTest
+        ]

tests/Tests.hs

@@ -1,11 +1,13 @@
 module Main where
 
 import qualified ExprTests as E
+import qualified ParserTests as P
 import qualified System.Exit as Exit
 import Test.HUnit
 
 tests :: Test
-tests = TestList [TestLabel "ExprTests" E.tests]
+tests = TestList [ TestLabel "ExprTests" E.tests
+                 , TestLabel "ParserTests" P.tests]
 
 main :: IO ()
 main = do