diff --git a/.gitignore b/.gitignore index dee53c5..3736b22 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ build +depends *~ diff --git a/src/Quox.idr b/Main.idr similarity index 99% rename from src/Quox.idr rename to Main.idr index 8d1354e..8fd706b 100644 --- a/src/Quox.idr +++ b/Main.idr @@ -1,4 +1,4 @@ -module Quox +module Main import public Quox.Name import public Quox.Syntax diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..d412187 --- /dev/null +++ b/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 diff --git a/quox-exe.ipkg b/quox-exe.ipkg index 54a6a47..9277e65 100644 --- a/quox-exe.ipkg +++ b/quox-exe.ipkg @@ -1,7 +1,6 @@ package quox-exe executable = quox -main = Quox -sourcedir = "src" +main = Main depends = base, contrib, quox diff --git a/src/Quox/Reduce.idr b/src/Quox/Reduce.idr index 19fbd2b..50f4038 100644 --- a/src/Quox/Reduce.idr +++ b/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 diff --git a/src/Quox/Syntax/Term/Base.idr b/src/Quox/Syntax/Term/Base.idr index 22552f6..a377339 100644 --- a/src/Quox/Syntax/Term/Base.idr +++ b/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 diff --git a/tests/Makefile b/tests/Makefile new file mode 100644 index 0000000..c0de71e --- /dev/null +++ b/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 diff --git a/tests/TAP.idr b/tests/TAP.idr index 0367875..17acddf 100644 --- a/tests/TAP.idr +++ b/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 diff --git a/tests/Tests.idr b/tests/Tests.idr index b095b76..393c11a 100644 --- a/tests/Tests.idr +++ b/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] diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr new file mode 100644 index 0000000..4605607 --- /dev/null +++ b/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 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" + ]