some reduction tests & fixes

Makefile

@@ -1,30 +1,38 @@
 all: quox
 
+NIXFLAGS := --no-warn-dirty
+
 # these two are real files, but always ask nix if they need remaking
 .PHONY: quox
 quox:
-	nix build --no-link '.#quox'
+	@echo [build] quox
-	ln -sfL $$(nix path-info '.#quox')/bin/quox quox
+	nix build $(NIXFLAGS) --no-link '.#quox'
+	ln -sfL $$(nix path-info $(NIXFLAGS) '.#quox')/bin/quox quox
 
 .PHONY: quox-tests
 quox-tests:
-	nix build --no-link '.#quox-tests'
+	@echo [build] quox-tests
-	ln -sfL $$(nix path-info '.#quox-tests')/bin/quox-tests quox-tests
+	nix build $(NIXFLAGS) --no-link '.#quox-tests'
+	ln -sfL $$(nix path-info $(NIXFLAGS) '.#quox-tests')/bin/quox-tests quox-tests
 
 
 .PHONY: lib
 lib:
-	nix build --no-link '.#quox-lib'
+	@echo [build] quox-lib
+	nix build $(NIXFLAGS) --no-link '.#quox-lib'
 
 .PHONY: test
 test:
-	nix run -- '.#quox-tests' -V 14
+	nix run $(NIXFLAGS) -- '.#quox-tests' -V 14 -c
 
 .PHONY: prove
 prove:
-	nix build --no-link '.#quox-tests'
+	nix build $(NIXFLAGS) --no-link '.#quox-tests'
-	prove $$(nix path-info '.#quox-tests')/bin/quox-tests
+	prove $$(nix path-info $(NIXFLAGS) '.#quox-tests')/bin/quox-tests
 
 .PHONY: clean
 clean:
+	@echo [clean]
 	rm -f quox quox-tests result
+
+.SILENT:

lib/Quox/Equal.idr

@@ -1,7 +1,6 @@
 module Quox.Equal
 
 import public Quox.Syntax
-import public Quox.Reduce
 import Control.Monad.Either
 import Generics.Derive
 

lib/Quox/Reduce.idr

@@ -1,130 +0,0 @@
-module Quox.Reduce
-
-import public Quox.Syntax
-
-%default total
-
-
-public export
-data IsRedexT : Term d n -> Type where
-  IsUpsilonT : IsRedexT $ E (_ :# _)
-  IsCloT     : IsRedexT $ CloT {}
-  IsDCloT    : IsRedexT $ DCloT {}
-
-public export %inline
-NotRedexT : Term d n -> Type
-NotRedexT = Not . IsRedexT
-
-public export
-data IsRedexE : Elim d n -> Type where
-  IsUpsilonE : IsRedexE $ E _ :# _
-  IsBetaLam  : IsRedexE $ (Lam {} :# Pi {}) :@ _
-  IsCloE     : IsRedexE $ CloE {}
-  IsDCloE    : IsRedexE $ DCloE {}
-
-public export %inline
-NotRedexE : Elim d n -> Type
-NotRedexE = Not . IsRedexE
-
-
-export %inline
-isRedexT : (t : Term d n) -> Dec (IsRedexT t)
-isRedexT (E (_ :# _))   = Yes IsUpsilonT
-isRedexT (CloT {})      = Yes IsCloT
-isRedexT (DCloT {})     = Yes IsDCloT
-isRedexT (TYPE _)       = No $ \x => case x of {}
-isRedexT (Pi {})        = No $ \x => case x of {}
-isRedexT (Lam {})       = No $ \x => case x of {}
-isRedexT (E (F _))      = No $ \x => case x of {}
-isRedexT (E (B _))      = No $ \x => case x of {}
-isRedexT (E (_ :@ _))   = No $ \x => case x of {}
-isRedexT (E (CloE {}))  = No $ \x => case x of {}
-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
-isRedexE (F x)                         = No $ \x => case x of {}
-isRedexE (B i)                         = No $ \x => case x of {}
-isRedexE (F _                    :@ _) = No $ \x => case x of {}
-isRedexE (B _                    :@ _) = 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 {}   :# TYPE _)   :@ _) = No $ \x => case x of {}
-isRedexE ((Lam {}   :# Lam {})   :@ _) = No $ \x => case x of {}
-isRedexE ((Lam {}   :# E _)      :@ _) = No $ \x => case x of {}
-isRedexE ((Lam {}   :# CloT {})  :@ _) = No $ \x => case x of {}
-isRedexE ((Lam {}   :# DCloT {}) :@ _) = No $ \x => case x of {}
-isRedexE ((E _      :# _)        :@ _) = No $ \x => case x of {}
-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 (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
-RedexTerm : Nat -> Nat -> Type
-RedexTerm d n = Subset (Term d n) IsRedexT
-
-public export %inline
-NonRedexTerm : Nat -> Nat -> Type
-NonRedexTerm d n = Subset (Term d n) NotRedexT
-
-
-public export %inline
-RedexElim : Nat -> Nat -> Type
-RedexElim d n = Subset (Elim d n) IsRedexE
-
-public export %inline
-NonRedexElim : Nat -> Nat -> Type
-NonRedexElim d n = Subset (Elim d n) NotRedexE
-
-
-||| substitute a term with annotation for the bound variable of a `ScopeTerm`
-export %inline
-substScope : (arg, argTy : Term d n) -> (body : ScopeTerm d n) -> Term d n
-substScope arg argTy (TUsed   body) = body // one (arg :# argTy)
-substScope arg argTy (TUnused body) = body
-
-export %inline
-stepT' : (s : Term d n) -> IsRedexT s -> Term d n
-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)
-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
-stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e
-
-export %inline
-stepE : (e : Elim d n) -> Either (NotRedexE e) (Elim d n)
-stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n
-
-export covering
-whnfT : Term d n -> NonRedexTerm d n
-whnfT s = case stepT s of
-               Right s'   => whnfT s'
-               Left  done => Element s done
-
-export covering
-whnfE : Elim d n -> NonRedexElim d n
-whnfE e = case stepE e of
-               Right e'   => whnfE e'
-               Left  done => Element e done

lib/Quox/Syntax/Term/Base.idr

@@ -90,8 +90,8 @@ mutual
 %name DScopeTerm body
 
 public export %inline
-Arr : Qty -> Term d n -> Term d n -> Term d n
+Arr : (qty : Qty) -> (arg, res : Term d n) -> Term d n
-Arr pi a b = Pi {qty = pi, x = "_", arg = a, res = TUnused b}
+Arr {qty, arg, res} = Pi {qty, x = "_", arg, res = TUnused res}
 
 ||| same as `F` but as a term
 public export %inline

lib/Quox/Syntax/Term/Reduce.idr

@@ -83,7 +83,10 @@ mutual
   pushSubstsEWith th ph (F x) =
     ncloE $ F x
   pushSubstsEWith th ph (B i) =
-    assert_total pushSubstsE $ ph !! i
+    let res = ph !! i in
+    case choose $ topCloE res of
+         Left  _ => assert_total pushSubstsE res
+         Right _ => ncloE res
   pushSubstsEWith th ph (f :@ s) =
     ncloE $ subs f th ph :@ subs s th ph
   pushSubstsEWith th ph (s :# a) =
@@ -162,3 +165,135 @@ weakT t = t //. shift 1
 public export %inline
 weakE : Elim d n -> Elim d (S n)
 weakE t = t //. shift 1
+
+
+mutual
+  public export
+  data IsRedexT : Term d n -> Type where
+    IsUpsilonT : IsRedexT $ E (_ :# _)
+    IsCloT     : IsRedexT $ CloT {}
+    IsDCloT    : IsRedexT $ DCloT {}
+    IsERedex   : IsRedexE e -> IsRedexT $ E e
+
+  public export %inline
+  NotRedexT : Term d n -> Type
+  NotRedexT = Not . IsRedexT
+
+  public export
+  data IsRedexE : Elim d n -> Type where
+    IsUpsilonE : IsRedexE $ E _ :# _
+    IsBetaLam  : IsRedexE $ (Lam {} :# Pi {}) :@ _
+    IsCloE     : IsRedexE $ CloE {}
+    IsDCloE    : IsRedexE $ DCloE {}
+
+  public export %inline
+  NotRedexE : Elim d n -> Type
+  NotRedexE = Not . IsRedexE
+
+
+mutual
+  export %inline
+  isRedexT : (t : Term d n) -> Dec (IsRedexT t)
+  isRedexT (E (tm :# ty)) = Yes IsUpsilonT
+  isRedexT (CloT {})      = Yes IsCloT
+  isRedexT (DCloT {})     = Yes IsDCloT
+  isRedexT (E (CloE  {})) = Yes $ IsERedex IsCloE
+  isRedexT (E (DCloE {})) = Yes $ IsERedex IsDCloE
+  isRedexT (E e@(_ :@ _)) with (isRedexE e)
+    _ | Yes yes = Yes $ IsERedex yes
+    _ | No  no  = No \case IsERedex p => no p
+  isRedexT (TYPE {}) = No $ \x => case x of {}
+  isRedexT (Pi   {}) = No $ \x => case x of {}
+  isRedexT (Lam  {}) = No $ \x => case x of {}
+  isRedexT (E (F _)) = No $ \x => case x of IsERedex _ impossible
+  isRedexT (E (B _)) = No $ \x => case x of IsERedex _ impossible
+
+  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
+  isRedexE (F x)                         = No $ \x => case x of {}
+  isRedexE (B i)                         = No $ \x => case x of {}
+  isRedexE (F _                    :@ _) = No $ \x => case x of {}
+  isRedexE (B _                    :@ _) = 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 {}   :# TYPE _)   :@ _) = No $ \x => case x of {}
+  isRedexE ((Lam {}   :# Lam {})   :@ _) = No $ \x => case x of {}
+  isRedexE ((Lam {}   :# E _)      :@ _) = No $ \x => case x of {}
+  isRedexE ((Lam {}   :# CloT {})  :@ _) = No $ \x => case x of {}
+  isRedexE ((Lam {}   :# DCloT {}) :@ _) = No $ \x => case x of {}
+  isRedexE ((E _      :# _)        :@ _) = No $ \x => case x of {}
+  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 (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
+RedexTerm : Nat -> Nat -> Type
+RedexTerm d n = Subset (Term d n) IsRedexT
+
+public export %inline
+NonRedexTerm : Nat -> Nat -> Type
+NonRedexTerm d n = Subset (Term d n) NotRedexT
+
+
+public export %inline
+RedexElim : Nat -> Nat -> Type
+RedexElim d n = Subset (Elim d n) IsRedexE
+
+public export %inline
+NonRedexElim : Nat -> Nat -> Type
+NonRedexElim d n = Subset (Elim d n) NotRedexE
+
+
+||| substitute a term with annotation for the bound variable of a `ScopeTerm`
+export %inline
+substScope : (arg, argTy : Term d n) -> (body : ScopeTerm d n) -> Term d n
+substScope arg argTy (TUsed   body) = body // one (arg :# argTy)
+substScope arg argTy (TUnused body) = body
+
+mutual
+  export %inline
+  stepT' : (s : Term d n) -> IsRedexT s -> Term d n
+  stepT' (E (s :# _)) IsUpsilonT   = s
+  stepT' (CloT  s th) IsCloT       = pushSubstsTWith' id th s
+  stepT' (DCloT s th) IsDCloT      = pushSubstsTWith' th id s
+  stepT' (E e)        (IsERedex p) = E $ stepE' e p
+
+  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
+  stepE' (DCloE e th) IsDCloE = pushSubstsEWith' th id e
+
+export %inline
+stepT : (s : Term d n) -> Either (NotRedexT s) (Term d n)
+stepT s = case isRedexT s of Yes y => Right $ stepT' s y; No n => Left n
+
+export %inline
+stepE : (e : Elim d n) -> Either (NotRedexE e) (Elim d n)
+stepE e = case isRedexE e of Yes y => Right $ stepE' e y; No n => Left n
+
+export covering
+whnfT : Term d n -> NonRedexTerm d n
+whnfT s = case stepT s of
+               Right s'   => whnfT s'
+               Left  done => Element s done
+
+export covering
+whnfE : Elim d n -> NonRedexElim d n
+whnfE e = case stepE e of
+               Right e'   => whnfE e'
+               Left  done => Element e done

lib/quox-lib.ipkg

@@ -32,6 +32,5 @@ modules =
   Quox.Context,
   Quox.Equal,
   Quox.Name,
-  Quox.Reduce,
   Quox.Typing,
   Quox.Typechecker

quox.bib

@@ -72,10 +72,20 @@
   doi       = {10.1145/1292597.1292608}
 }
 
+@article{ott-good,
+  author  = {Lo{\"{\i}}c Pujet and Nicolas Tabareau},
+  title   = {Observational equality: now for good},
+  journal = {Proc. {ACM} Program. Lang.},
+  volume  = {6},
+  number  = {{POPL}},
+  pages   = {1--27},
+  year    = {2022},
+  url     = {https://doi.org/10.1145/3498693},
+  doi     = {10.1145/3498693},
+}
+
 @inproceedings{xtt,
-  author    = {Jonathan Sterling and
+  author    = {Jonathan Sterling and Carlo Angiuli and Daniel Gratzer},
-               Carlo Angiuli and
-               Daniel Gratzer},
   editor    = {Herman Geuvers},
   title     = {Cubical Syntax for Reflection-Free Extensional Equality},
   booktitle = {4th International Conference on Formal Structures for Computation

tests/Options.idr

@@ -4,41 +4,110 @@ import Data.String
 import System
 import System.Console.GetOpt
 
+%default total
+
+
+public export
+data TAPVersion = V13 | V14
+
+export
+readVersion : String -> Maybe TAPVersion
+readVersion "13" = Just V13
+readVersion "14" = Just V14
+readVersion _    = Nothing
+
+export Show TAPVersion where show V13 = "13"; show V14 = "14"
+
 
 public export
 record Options where
   constructor Opts
-  tapVersion : String
+  version : TAPVersion
+  pattern : Maybe String
+  color   : Bool
 
-defaultOpts = Opts {tapVersion = "13"}
+export
+defaultOpts : Options
+defaultOpts = Opts {
+  version = V13,
+  pattern = Nothing,
+  color   = False
+}
 
-OptMod = Options -> Options
+public export
-
+Mod : Type
-opts : List (OptDescr OptMod)
+Mod = Options -> IO Options
-opts = [
-  MkOpt ['V'] ["version"]
-    (ReqArg (\v => the OptMod {tapVersion := v}) "VERSION")
-    "TAP version to output (13 or 14, default 13)"
-]
--- [todo] get rid of "the OptMod" when type inference is better, maybe
-
-makeOpts : List OptMod -> Options
-makeOpts = foldl (flip ($)) defaultOpts
 
 
+export
+failureWith : List String -> IO a
+failureWith msgs = do
+  traverse_ (\s => putStrLn "# \{s}") msgs
+  putStrLn "\nBail out!"
+  exitFailure
+
+private
+setTapVer : String -> Mod
+setTapVer ver opts =
+  case readVersion ver of
+       Just v  => pure $ {version := v} opts
+       Nothing => failureWith ["unrecognised TAP version '\{ver}'"]
+
+private
+setPat : String -> Mod
+setPat str opts = pure $ {pattern := Just str} opts
+
+mutual
+  export
+  opts : List (OptDescr Mod)
+  opts =
+    [ MkOpt {
+        description = "show this help",
+        shortNames  = ['h', '?'], longNames = ["help"],
+        argDescr    = NoArg $ const $ failureWith usage
+      },
+      MkOpt {
+        description = "TAP version to output (13 or 14, default 13)",
+        shortNames  = ['V'], longNames = ["version"],
+        argDescr    = ReqArg setTapVer "VERSION"
+      },
+      MkOpt {
+        description = "only run tests containing STR in their group or label",
+        shortNames  = ['F'], longNames = ["filter"],
+        argDescr    = ReqArg setPat "STR"
+      },
+      MkOpt {
+        description = "don't colour-code results (default)",
+        shortNames  = ['C'], longNames = ["no-color", "no-colour"],
+        argDescr    = NoArg $ pure . {color := False}
+      },
+      MkOpt {
+        description = "colour-code results (not TAP compliant)",
+        shortNames  = ['c'], longNames = ["color", "colour"],
+        argDescr    = NoArg $ pure . {color := True}
+      }
+    ]
+
+  export
+  usage : List String
+  usage = assert_total $ "quox test suite" :: lines (usageInfo "" opts)
+
+
+export
+makeOpts : List Mod -> IO Options
+makeOpts = foldlM (\x, f => f x) defaultOpts
+
+
+export
 getArgs1 : IO (List String)
 getArgs1 =
   case !getArgs of
        _ :: args => pure args
-       []        => do
+       []        => failureWith ["expected getArgs to start with exe name"]
-         putStrLn "expecting getArgs to start with exe name"
-         exitFailure
 
 export
 getTestOpts : IO Options
 getTestOpts =
   case getOpt Permute opts !getArgs1 of
-       MkResult opts [] [] [] => pure $ makeOpts opts
+       MkResult opts [] [] [] => makeOpts opts
-       res => do
+       res                    => failureWith $ res.errors ++ usage
-         traverse_ putStrLn $ res.errors ++ [usageInfo "quox test suite" opts]
-         exitFailure

tests/TAP.idr

@@ -1,14 +1,20 @@
 module TAP
--- [todo] extract this and Quox.Error to their own packages
+-- [todo] extract this to its own package?
 
+import Options
 import public Control.Monad.Either
 import Data.String
+import Data.List
 import Data.List.Elem
 import Data.SnocList
 import Control.Monad.Reader
 import Control.Monad.State
+import Control.ANSI
 import System
 
+%default total
+
+
 public export
 Info : Type
 Info = List (String, String)
@@ -39,24 +45,30 @@ toLines xs = "---" :: concatMap toLines1 xs <+> ["..."]
 
 public export interface ToInfo e where toInfo : e -> Info
 
-export %inline ToInfo () where toInfo () = []
+export ToInfo () where toInfo () = []
 
-export %inline Show a => ToInfo (List (String, a)) where toInfo = map (map show)
+export Show a => ToInfo (List (String, a)) where toInfo = map (map show)
 
 
 export
-data Test = One TestBase | Group String (List Test)
+data Test
+= One TestBase
+| Group String (List Test)
+| Note String
 
 
-private %inline
+export
-success : ToInfo a => a -> IO Result
+isRealTest : Test -> Bool
-success = pure . Tried True . toInfo
+isRealTest (One   _)   = True
+isRealTest (Group _ _) = True
+isRealTest (Note  _)   = False
 
-private %inline
-failure : ToInfo e => e -> IO Result
-failure = pure . Tried False . toInfo
 
-private %inline
+private
+result : ToInfo a => Bool -> a -> IO Result
+result ok = pure . Tried ok . toInfo
+
+private
 lazyToIO : Lazy a -> IO a
 lazyToIO val = primIO $ \w => MkIORes (force val) w
 
@@ -64,32 +76,32 @@ export
 testIO : (ToInfo e, ToInfo a) => String -> EitherT e IO a -> Test
 testIO label act = One $ MakeTest label $ do
   case !(runEitherT act) of
-       Right val => success val
+       Right val => result True  val
-       Left  err => failure err
+       Left  err => result False err
 
-export %inline
+export
 test : (ToInfo e, ToInfo a) => String -> Lazy (Either e a) -> Test
-test label val =
+test label val = testIO label $ MkEitherT $ lazyToIO val
-  testIO label $ MkEitherT $ lazyToIO val
 
-export %inline
+export
 todoWith : String -> String -> Test
 todoWith label reason = One $ MakeTest label $ pure $ Todo reason
 
-export %inline
+export
 todo : String -> Test
 todo label = todoWith label ""
 
-private %inline
+private
 makeSkip : String -> String -> Test
 makeSkip label reason = One $ MakeTest label $ pure $ Skip reason
 
-export %inline
+export
 skipWith : Test -> String -> Test
 skipWith (One   t)   reason = makeSkip t.label reason
 skipWith (Group l _) reason = makeSkip l       reason
+skipWith (Note  n)   _      = Note n
 
-export %inline
+export
 skip : Test -> Test
 skip test = skipWith test ""
 
@@ -98,78 +110,119 @@ testThrows : (ToInfo e, Show a) =>
              String -> (e -> Bool) -> Lazy (Either e a) -> Test
 testThrows label p act = One $ MakeTest label $ do
   case !(lazyToIO act) of
-       Left  err => if p err then success () else failure err
+       Left  err => if p err then result True () else result False err
-       Right val => failure [("success", val)]
+       Right val => result False [("success", val)]
 
 infix 1 :-
-export %inline
+export
 (:-) : String -> List Test -> Test
 (:-) = Group
 
-export %inline
+export
 bailOut : Test
 bailOut = One $ MakeTest "bail out" $ do
   putStrLn "Bail out!"
   exitFailure
 
+export
+note : String -> Test
+note = Note
 
 
-export %inline
+
-header : List a -> String
+export
-header tests = "1..\{show $ length tests}"
+header : List Test -> String
+header tests =
+  let count = length $ filter isRealTest tests in
+  "1..\{show count}"
+
 
 private
-makePrefix : SnocList String -> String
-makePrefix [<]       = ""
-makePrefix (xs :< x) = foldr (\a, b => "\{a}/\{b}") x xs
-
-private %inline
 withPrefix : SnocList String -> TestBase -> Test
-withPrefix pfx b = One $ {label := "[\{makePrefix pfx}] \{b.label}"} b
+withPrefix pfx = One . {label $= (makePrefix pfx ++)}
+  where makePrefix = concatMap $ \s => "\{s} ⟫ "
 
 mutual
-  export %inline
+  export
   flattenWith : SnocList String -> List Test -> List Test
-  flattenWith pfx = concatMap (flatten1With pfx)
+  flattenWith pfx tests =
+    concatMap (\t => flatten1With pfx (assert_smaller tests t)) tests
 
   export
   flatten1With : SnocList String -> Test -> List Test
   flatten1With pfx (One   t)    = [withPrefix pfx t]
   flatten1With pfx (Group x ts) = flattenWith (pfx :< x) ts
+  flatten1With pfx (Note  n)    = [Note n]
 
-export %inline
+export
 flatten : List Test -> List Test
 flatten = flattenWith [<]
 
-export %inline
+export
 flatten1 : Test -> List Test
 flatten1 = flatten1With [<]
 
 
 private
-Runner : Type -> Type
+record RunnerEnv where
-Runner = ReaderT Nat IO
+  constructor RE
-
+  indent : Nat
-private %inline
+  color  : Bool
-putIndentLines : List String -> Runner ()
-putIndentLines xs = traverse_ (putStrLn . indent !ask) xs
-
-private %inline
-isOk : Bool -> String
-isOk b = if b then "ok" else "not ok"
-
-private %inline
-toBool : Result -> Bool
-toBool (Tried ok _) = ok
-toBool _ = True
 
 
 private
-numbered : List a -> List (Nat, a)
+Runner : Type -> Type
-numbered = go 1 where
+Runner = ReaderT RunnerEnv IO
+
+private
+putIndentLines : List String -> Runner ()
+putIndentLines xs = traverse_ (putStrLn . indent (!ask).indent) xs
+
+private
+isOk : Bool -> String
+isOk b = if b then "ok" else "not ok"
+
+private
+toBool : Result -> Bool
+toBool (Tried ok _) = ok
+toBool _            = True
+
+
+private
+numbered : (a -> Bool) -> List a -> List (Nat, a)
+numbered p = go 1 where
   go : Nat -> List a -> List (Nat, a)
   go _ []        = []
-  go i (x :: xs) = (i, x) :: go (S i) xs
+  go i (x :: xs) =
+    if p x then (i, x) :: go (S i) xs
+           else (0, x) :: go i     xs
+
+
+private
+col : Color -> String -> Runner String
+col c str = pure $ if (!ask).color then show $ colored c str else str
+
+private
+putColor : Color -> String -> Runner ()
+putColor c str = putIndentLines [!(col c str)]
+
+private
+okCol : Bool -> Color
+okCol True  = Green
+okCol False = Red
+
+private
+putOk' : Color -> Bool -> Nat -> String -> Runner ()
+putOk' c ok index label =
+  putIndentLines [!(col c "\{isOk ok} \{show index}") ++ " - \{label}"]
+
+private
+putOk : Bool -> Nat -> String -> Runner ()
+putOk ok = putOk' (okCol ok) ok
+
+private
+putVersion : TAPVersion -> Runner ()
+putVersion ver = putColor Cyan "TAP version \{show ver}"
 
 private
 run1' : (Nat, TestBase) -> Runner Bool
@@ -177,12 +230,12 @@ run1' (index, test) = do
   res <- liftIO test.run
   case res of
        Tried ok info => do
-         putIndentLines ["\{isOk ok} \{show index} - \{test.label}"]
+         putOk ok index test.label
-         local (plus 2) $ putIndentLines $ toLines info
+         local {indent $= plus 2} $ putIndentLines $ toLines info
-       Skip reason => putIndentLines
+       Skip reason =>
-         ["ok \{show index} - \{test.label}  # skip \{reason}"]
+         putOk' Yellow True index "\{test.label}  # skip \{reason}"
-       Todo reason => putIndentLines
+       Todo reason =>
-         ["ok \{show index} - \{test.label}  # todo \{reason}"]
+         putOk' Yellow True index "\{test.label}  # todo \{reason}"
   pure $ toBool res
 
 mutual
@@ -190,30 +243,47 @@ mutual
   run' : (Nat, Test) -> Runner Bool
   run' (index, One test) = run1' (index, test)
   run' (index, Group label tests) = do
-    putIndentLines ["# Subtest: \{label}"]
+    putIndentLines [!(col Magenta "# Subtest: ") ++ label]
-    res <- local (plus 4) $ runList tests
+    res <- local {indent $= plus 4} $ runList tests
-    putIndentLines ["\{isOk res} \{show index} - \{label}"]
+    putOk res index label
     pure res
+  run' (_, Note note) = do
+    putIndentLines [!(col Magenta "# ") ++ note]
+    pure True
 
   private
   runList : List Test -> Runner Bool
   runList tests = do
-    putIndentLines [header tests]
+    putColor Cyan $ header tests
-    all id <$> traverse run' (numbered tests)
+    let tests' = numbered isRealTest tests
+    all id <$> traverse (\t => run' (assert_smaller tests t)) tests'
+
+
+mutual
+  export
+  filterMatch : Maybe String -> List Test -> List Test
+  filterMatch Nothing    tests = tests
+  filterMatch (Just pat) tests =
+    mapMaybe (\t => filterMatch1 pat (assert_smaller tests t)) tests
+
+  export
+  filterMatch1 : String -> Test -> Maybe Test
+  filterMatch1 pat test@(One base) =
+    guard (pat `isInfixOf` base.label) $> test
+  filterMatch1 pat all@(Group label tests) =
+    if pat `isInfixOf` label then Just all else
+    case filterMatch (Just pat) tests of
+         []  => Nothing
+         res => Just $ Group label res
+  filterMatch1 pat note@(Note _) = Just note
 
 
 export
-run : (ver : Nat) -> List Test -> IO ExitCode
+main : Options -> List Test -> IO ExitCode
-run ver tests = do
+main opts tests = do
-  putStrLn "TAP version \{show ver}"
+  let tests = filterMatch opts.pattern $
-  pure $ if !(runReaderT 0 $ runList tests)
+              case opts.version of V13 => flatten tests; V14 => tests
+  let act = do putVersion opts.version; runList tests
+  pure $ if !(runReaderT (RE 0 opts.color) act)
             then ExitSuccess
             else ExitFailure 70
-
-export
-main : List Test -> IO ()
-main tests = exitWith !(run 14 tests)
-
-export
-mainFlat : List Test -> IO ()
-mainFlat tests = exitWith !(run 13 $ flatten tests)

tests/Tests.idr

@@ -5,6 +5,7 @@ import TAP
 import Tests.Unicode
 import Tests.Lexer
 import Tests.Parser
+import Tests.Reduce
 import Tests.Equal
 import System
 
@@ -13,13 +14,8 @@ allTests = [
   Unicode.tests,
   Lexer.tests,
   Parser.tests,
+  Reduce.tests,
   Equal.tests
 ]
 
-main = do
+main = TAP.main !getTestOpts allTests
-  opts <- getTestOpts
-  go <- case opts.tapVersion of
-    "13" => pure TAP.mainFlat
-    "14" => pure TAP.main
-    _    => do putStrLn "unrecognised TAP version; use 13 or 14"; exitFailure
-  go allTests

tests/Tests/Equal.idr

@@ -1,6 +1,6 @@
 module Tests.Equal
 
-import Quox.Equal
+import Quox.Equal as Lib
 import Quox.Pretty
 import TAP
 
@@ -32,20 +32,20 @@ testNeq label = testThrows label $ const True
 
 
 subT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
-subT = Quox.Equal.subT
+subT = Lib.subT
-%hide Quox.Equal.subT
+%hide Lib.subT
 
 equalT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
-equalT = Quox.Equal.equalT
+equalT = Lib.equalT
-%hide Quox.Equal.equalT
+%hide Lib.equalT
 
 subE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
-subE = Quox.Equal.subE
+subE = Lib.subE
-%hide Quox.Equal.subE
+%hide Lib.subE
 
 equalE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
-equalE = Quox.Equal.equalE
+equalE = Lib.equalE
-%hide Quox.Equal.equalE
+%hide Lib.equalE
 
 
 export
@@ -112,19 +112,35 @@ tests = "equality & subtyping" :- [
 
     "lambda" :- [
       testEq "λ x ⇒ [x] ≡ λ x ⇒ [x]" $
-        equalT (Lam "x" (TUsed (BVT 0))) (Lam "x" (TUsed (BVT 0))),
+        equalT (Lam "x" $ TUsed $ BVT 0) (Lam "x" $ TUsed $ BVT 0),
       testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $
-        equalT (Lam "x" (TUsed (BVT 0))) (Lam "x" (TUsed (BVT 0))),
+        equalT (Lam "x" $ TUsed $ BVT 0) (Lam "x" $ TUsed $ BVT 0),
       testEq "λ x ⇒ [x] ≡ λ y ⇒ [y]" $
-        equalT (Lam "x" (TUsed (BVT 0))) (Lam "y" (TUsed (BVT 0))),
+        equalT (Lam "x" $ TUsed $ BVT 0) (Lam "y" $ TUsed $ BVT 0),
       testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $
-        equalT (Lam "x" (TUsed (BVT 0))) (Lam "y" (TUsed (BVT 0))),
+        equalT (Lam "x" $ TUsed $ BVT 0) (Lam "y" $ TUsed $ BVT 0),
       testNeq "λ x y ⇒ [x] ≢ λ x y ⇒ [y]" $
-        equalT (Lam "x" (TUsed (Lam "y" (TUsed (BVT 1)))))
+        equalT (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 1)
-               (Lam "x" (TUsed (Lam "y" (TUsed (BVT 0)))))
+               (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 0),
+      testEq "λ x ⇒ [a] ≡ λ x ⇒ [a]  (TUsed vs TUnused)" $
+        equalT (Lam "x" $ TUsed   $ FT "a")
+               (Lam "x" $ TUnused $ FT "a")
     ],
 
-    todo "term closure",
+    "term closure" :- [
+      testEq "[x]{} ≡ [x]" $
+        equalT (CloT (BVT 0) id) (BVT 0) {n = 1},
+      testEq "[x]{a/x} ≡ [a]" $
+        equalT (CloT (BVT 0) (F "a" ::: id)) (FT "a"),
+      testEq "[x]{a/x,b/y} ≡ [a]" $
+        equalT (CloT (BVT 0) (F "a" ::: F "b" ::: id)) (FT "a"),
+      testEq "(λy. [x]){y/y, a/x} ≡ λy. [a]  (TUnused)" $
+        equalT (CloT (Lam "y" $ TUnused $ BVT 0) (F "a" ::: id))
+               (Lam "y" $ TUnused $ FT "a"),
+      testEq "(λy. [x]){y/y, a/x} ≡ λy. [a]  (TUsed)" $
+        equalT (CloT (Lam "y" $ TUsed $ BVT 1) (F "a" ::: id))
+               (Lam "y" $ TUsed $ FT "a")
+    ],
 
     todo "term d-closure",
 

tests/Tests/Reduce.idr

@@ -0,0 +1,116 @@
+module Tests.Reduce
+
+import Quox.Syntax as Lib
+import TermImpls
+import TAP
+
+
+testWhnf : (Eq b, Show b) => (a -> (Subset b _)) ->
+           String -> a -> b -> Test
+testWhnf whnf label from to = test "\{label}  (whnf)" $
+  let result = fst (whnf from) in
+  if result == to
+     then Right ()
+     else with Prelude.(::)
+          Left [("expected", to), ("received", result)]
+
+testNoStep : forall p. Show a => ((x : a) -> Either (p x) a) ->
+            String -> a -> Test
+testNoStep step label e = test "\{label}  (no step)" $
+  case step e of
+       Left  _  => Right ()
+       Right e' => with Prelude.(::) Left [("reduced", e')]
+
+
+parameters {default 0 d, n : Nat}
+  testWhnfT : String -> Term d n -> Term d n -> Test
+  testWhnfT = testWhnf whnfT
+
+  testWhnfE : String -> Elim d n -> Elim d n -> Test
+  testWhnfE = testWhnf whnfE
+
+  testNoStepE : String -> Elim d n -> Test
+  testNoStepE = testNoStep stepE
+
+  testNoStepT : String -> Term d n -> Test
+  testNoStepT = testNoStep stepT
+
+
+tests = "whnf" :- [
+  "head constructors" :- [
+    testNoStepT "★₀" $ TYPE 0,
+    testNoStepT "[A] ⊸ [B]" $
+      Arr One (FT "A") (FT "B"),
+    testNoStepT "(x: [A]) ⊸ [B [x]]" $
+      Pi One "x" (FT "A") (TUsed $ E $ F "B" :@ BVT 0),
+    testNoStepT "λx. [x]" $
+      Lam "x" $ TUsed $ BVT 0,
+    testNoStepT "[f [a]]" $
+      E $ F "f" :@ FT "a"
+  ],
+
+  "neutrals" :- [
+    testNoStepE "x" {n = 1} $ BV 0,
+    testNoStepE "a"         $ F "a",
+    testNoStepE "f [a]"     $ F "f" :@ FT "a",
+    testNoStepE "★₀ ∷ ★₁"   $ TYPE 0 :# TYPE 1
+  ],
+
+  "redexes" :- [
+    testWhnfE "[a] ∷ [A]"
+      (FT "a" :# FT "A")
+      (F "a"),
+    testWhnfT "[★₁ ∷ ★₃]"
+      (E (TYPE 1 :# TYPE 3))
+      (TYPE 1),
+    testWhnfE "(λx. [x] ∷ [A] ⊸ [A]) [a]"
+      ((Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
+      (F "a")
+  ],
+
+  "elim closure" :- [
+    testWhnfE "x{}" {n = 1}
+      (CloE (BV 0) id)
+      (BV 0),
+    testWhnfE "x{a/x}"
+      (CloE (BV 0) (F "a" ::: id))
+      (F "a"),
+    testWhnfE "x{x/x,a/y}" {n = 1}
+      (CloE (BV 0) (BV 0 ::: F "a" ::: id))
+      (BV 0),
+    testWhnfE "x{(y{a/y})/x}"
+      (CloE (BV 0) ((CloE (BV 0) (F "a" ::: id)) ::: id))
+      (F "a"),
+    testWhnfE "(x y){f/x,a/y}"
+      (CloE (BV 0 :@ BVT 1) (F "f" ::: F "a" ::: id))
+      (F "f" :@ FT "a"),
+    testWhnfE "([y] ∷ [x]){A/x}" {n = 1}
+      (CloE (BVT 1 :# BVT 0) (F "A" ::: id))
+      (BV 0),
+    testWhnfE "([y] ∷ [x]){A/x,a/y}"
+      (CloE (BVT 1 :# BVT 0) (F "A" ::: F "a" ::: id))
+      (F "a")
+  ],
+
+  "term closure" :- [
+    testWhnfT "(λy. x){a/x}"
+      (CloT (Lam "x" $ TUnused $ BVT 0) (F "a" ::: id))
+      (Lam "x" $ TUnused $ FT "a")
+  ],
+
+  "looking inside […]" :- [
+    testWhnfT "[(λx. x ∷ A ⊸ A) [a]]"
+      (E $ (Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
+      (FT "a")
+  ],
+
+  "nested redex" :- [
+    note "whnf only looks at top level redexes",
+    testNoStepT "λy. [(λx. [x] ∷ [A] ⊸ [A]) [y]]" $
+      Lam "y" $ TUsed $ E $
+        (Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ BVT 0,
+    testNoStepE "f [(λx. [x] ∷ [A] ⊸ [A]) [a]]" $
+      F "a" :@
+      E ((Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
+  ]
+]