makefiles. again

i think this just means type preservation is modulo subtyping. which is
probably fine....?

.gitignore

@@ -1,2 +1,3 @@
 build
+depends
 *~

Main.idr

@@ -1,4 +1,4 @@
-module Quox
+module Main
 
 import public Quox.Name
 import public Quox.Syntax

Makefile

@@ -0,0 +1,22 @@
+all: lib exe
+
+.PHONY: lib
+lib:
+	idris2 --build quox.ipkg
+
+depends/quox: lib
+	mkdir -p depends
+	ln -sf ../build/ttc depends/quox
+
+.PHONY: exe
+exe: depends/quox
+	idris2 --build quox-exe.ipkg
+
+.PHONY: test
+test:
+	make -C tests test
+
+.PHONY: clean
+clean:
+	rm -rf build depends
+	make -C tests clean

quox-exe.ipkg

@@ -1,7 +1,6 @@
 package quox-exe
 
 executable = quox
-main = Quox
-sourcedir = "src"
+main = Main
 
 depends = base, contrib, quox

src/Quox/Reduce.idr

@@ -5,9 +5,9 @@ import public Quox.Syntax
 
 public export
 data IsRedexT : Term d n -> Type where
-  IsUpsilon : IsRedexT $ E (_ :# _)
-  IsCloT    : IsRedexT $ CloT {}
-  IsDCloT   : IsRedexT $ DCloT {}
+  IsUpsilonT : IsRedexT $ E (_ :# _)
+  IsCloT     : IsRedexT $ CloT {}
+  IsDCloT    : IsRedexT $ DCloT {}
 
 public export %inline
 NotRedexT : Term d n -> Type
@@ -15,9 +15,10 @@ NotRedexT = Not . IsRedexT
 
 public export
 data IsRedexE : Elim d n -> Type where
-  IsBetaLam : IsRedexE $ (Lam {} :# Pi {}) :@ _
-  IsCloE    : IsRedexE $ CloE {}
-  IsDCloE   : IsRedexE $ DCloE {}
+  IsUpsilonE : IsRedexE $ E _ :# _
+  IsBetaLam  : IsRedexE $ (Lam {} :# Pi {}) :@ _
+  IsCloE     : IsRedexE $ CloE {}
+  IsDCloE    : IsRedexE $ DCloE {}
 
 public export %inline
 NotRedexE : Elim d n -> Type
@@ -26,7 +27,7 @@ NotRedexE = Not . IsRedexE
 
 export %inline
 isRedexT : (t : Term d n) -> Dec (IsRedexT t)
-isRedexT (E (_ :# _))   = Yes IsUpsilon
+isRedexT (E (_ :# _))   = Yes IsUpsilonT
 isRedexT (CloT {})      = Yes IsCloT
 isRedexT (DCloT {})     = Yes IsDCloT
 isRedexT (TYPE _)       = No $ \x => case x of {}
@@ -40,6 +41,7 @@ isRedexT (E (DCloE {})) = No $ \x => case x of {}
 
 export %inline
 isRedexE : (e : Elim d n) -> Dec (IsRedexE e)
+isRedexE (E _ :# _)                    = Yes IsUpsilonE
 isRedexE ((Lam {} :# Pi {}) :@ _)      = Yes IsBetaLam
 isRedexE (CloE {})                     = Yes IsCloE
 isRedexE (DCloE {})                    = Yes IsDCloE
@@ -60,7 +62,11 @@ isRedexE ((CloT {}  :# _)        :@ _) = No $ \x => case x of {}
 isRedexE ((DCloT {} :# _)        :@ _) = No $ \x => case x of {}
 isRedexE (CloE {}                :@ _) = No $ \x => case x of {}
 isRedexE (DCloE {}               :@ _) = No $ \x => case x of {}
-isRedexE (_ :# _)                      = No $ \x => case x of {}
+isRedexE (TYPE _   :# _)               = No $ \x => case x of {}
+isRedexE (Pi {}    :# _)               = No $ \x => case x of {}
+isRedexE (Lam {}   :# _)               = No $ \x => case x of {}
+isRedexE (CloT {}  :# _)               = No $ \x => case x of {}
+isRedexE (DCloT {} :# _)               = No $ \x => case x of {}
 
 
 public export %inline
@@ -89,9 +95,9 @@ substScope arg argTy (TUnused body) = body
 
 export %inline
 stepT' : (s : Term d n) -> IsRedexT s -> Term d n
-stepT' (E (s :# _)) IsUpsilon = s
-stepT' (CloT  s th) IsCloT    = pushSubstsTWith' id th s
-stepT' (DCloT s th) IsDCloT   = pushSubstsTWith' th id s
+stepT' (E (s :# _)) IsUpsilonT = s
+stepT' (CloT  s th) IsCloT     = pushSubstsTWith' id th s
+stepT' (DCloT s th) IsDCloT    = pushSubstsTWith' th id s
 
 export %inline
 stepT : (s : Term d n) -> Either (NotRedexT s) (Term d n)
@@ -99,6 +105,7 @@ stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n
 
 export %inline
 stepE' : (e : Elim d n) -> IsRedexE e -> Elim d n
+stepE' (E e :# _) IsUpsilonE = e
 stepE' ((Lam {body, _} :# Pi {arg, res, _}) :@ s) IsBetaLam =
   substScope s arg body :# substScope s arg res
 stepE' (CloE  e th) IsCloE  = pushSubstsEWith' id th e

src/Quox/Syntax/Term/Base.idr

@@ -89,6 +89,10 @@ mutual
 %name ScopeTerm body
 %name DScopeTerm body
 
+public export %inline
+Arr : Qty -> Term d n -> Term d n -> Term d n
+Arr pi a b = Pi {qtm = pi, qty = zero, x = "_", arg = a, res = TUnused b}
+
 ||| same as `F` but as a term
 public export %inline
 FT : Name -> Term d n

tests/Makefile

@@ -0,0 +1,18 @@
+all: test
+
+.PHONY: lib
+lib:
+	make -C .. lib
+
+depends/quox: lib
+	mkdir -p depends
+	ln -sf ../../build/ttc depends/quox
+
+.PHONY: test
+test: depends/quox
+	idris2 --build tests.ipkg
+	build/exec/quox-tests
+
+.PHONY: clean
+clean:
+	rm -rf build depends

tests/TAP.idr

@@ -45,21 +45,36 @@ All ToInfo es => ToInfo (OneOf es) where
 
 export %inline ToInfo () where toInfo () = []
 
+export Show a => ToInfo (List (String, a)) where toInfo = map (map show)
+
+
 export
 data Test = One TestBase | Group String (List Test)
 
 
+private %inline
+success : ToInfo a => a -> IO Result
+success = pure . Tried True . toInfo
+
+private %inline
+failure : ToInfo e => e -> IO Result
+failure = pure . Tried False . toInfo
+
+private %inline
+lazyToIO : Lazy a -> IO a
+lazyToIO val = primIO $ \w => MkIORes (force val) w
+
 export
 testIO : (All ToInfo es, ToInfo a) => String -> ErrorT es IO a -> Test
 testIO label act = One $ MakeTest label $ do
   case !(runErrorT act) of
-       Left  err => pure $ Tried False $ toInfo err
-       Right val => pure $ Tried True  $ toInfo val
+       Right val => success val
+       Left  err => failure err
 
 export %inline
 test : (All ToInfo es, ToInfo a) => String -> Lazy (Error es a) -> Test
 test label val =
-  testIO label $ MkErrorT $ primIO $ \w => MkIORes (runError val) w
+  testIO label $ MkErrorT $ lazyToIO $ runError val
 
 export %inline
 todoWith : String -> String -> Test
@@ -77,11 +92,24 @@ export %inline
 skip : String -> Test
 skip label = skipWith label ""
 
+export
+testThrows : Show a => String -> Lazy (Error es a) -> Test
+testThrows label act = One $ MakeTest label $ do
+  case runError !(lazyToIO act) of
+       Left  err => success ()
+       Right val => failure [("success", val)]
+
 infix 0 :-
 export %inline
 (:-) : String -> List Test -> Test
 (:-) = Group
 
+export %inline
+bailOut : Test
+bailOut = One $ MakeTest "bail out" $ do
+  putStrLn "Bail out!"
+  exitFailure
+
 
 
 export %inline

tests/Tests.idr

@@ -1,7 +1,11 @@
 module Tests
 
+import Tests.Equal
+
 import TAP
 
-export main : IO ()
-main = run
-  [todo "write tests"]
+import System
+
+export main : IO Int
+main = exitWith =<< run
+  [Equal.tests]

tests/Tests/Equal.idr

@@ -0,0 +1,101 @@
+module Tests.Equal
+
+import Quox.Equal
+import Quox.Pretty
+import TAP
+
+export
+ToInfo Equal.Error where
+  toInfo (ClashT mode s t) =
+    [("clash",  "term"),
+     ("mode",   show mode),
+     ("left",  prettyStr True s),
+     ("right", prettyStr True t)]
+  toInfo (ClashU mode k l) =
+    [("clash",  "universe"),
+     ("mode",   show mode),
+     ("left",  prettyStr True k),
+     ("right", prettyStr True l)]
+  toInfo (ClashQ pi rh) =
+    [("clash",  "quantity"),
+     ("left",  prettyStr True pi),
+     ("right", prettyStr True rh)]
+
+
+M = Error [Equal.Error]
+
+testEq : String -> Lazy (M ()) -> Test
+testEq = test
+
+testNeq : String -> Lazy (M ()) -> Test
+testNeq = testThrows
+
+
+subT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
+subT = Quox.Equal.subT
+%hide Quox.Equal.subT
+
+equalT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
+equalT = Quox.Equal.equalT
+%hide Quox.Equal.equalT
+
+subE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
+subE = Quox.Equal.subE
+%hide Quox.Equal.subE
+
+equalE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
+equalE = Quox.Equal.equalE
+%hide Quox.Equal.equalE
+
+
+export
+tests : Test
+tests = "equality & subtyping" :- [
+    "universes" :- [
+        testEq "Type 0 == Type 0" $
+          equalT (TYPE (U 0)) (TYPE (U 0)),
+        testNeq "Type 0 =/= Type 1" $
+          equalT (TYPE (U 0)) (TYPE (U 1)),
+        testNeq "Type 1 =/= Type 0" $
+          equalT (TYPE (U 1)) (TYPE (U 0)),
+        testEq "Type 0 <: Type 0" $
+          subT (TYPE (U 0)) (TYPE (U 0)),
+        testEq "Type 0 <: Type 1" $
+          subT (TYPE (U 0)) (TYPE (U 1)),
+        testNeq "Type 1 </: Type 0" $
+          subT (TYPE (U 1)) (TYPE (U 0))
+      ],
+    todo "pi",
+    todo "lambda",
+    todo "term closure",
+    todo "term d-closure",
+
+    "free var" :- [
+        testEq "A == A" $
+          equalE (F "A") (F "A"),
+        testNeq "A =/= B" $
+          equalE (F "A") (F "B"),
+        testEq "A <: A" $
+          subE (F "A") (F "A"),
+        testNeq "A </: B" $
+          subE (F "A") (F "B")
+      ],
+    todo "bound var",
+    "application" :-
+      let a    = F "a"; a' = E a
+          A    = FT "A"
+          λxx  = Lam "x" (TUsed (BVT 0))
+          A_A  = Arr one A A
+          λxx' = λxx :# A_A
+      in [
+        testEq "(λx. x : A -> A) a == ((a : A) : A)  (β)" $
+          equalE (λxx' :@ a') (E (a' :# A) :# A),
+        testEq "(λx. x : _) a == a  (βυ)" $
+          equalE (λxx' :@ a') a
+      ],
+    todo "annotation",
+    todo "elim closure",
+    todo "elim d-closure",
+
+    todo "clashes"
+  ]