Compare commits

...

9 Commits

12 changed files with 557 additions and 269 deletions

View File

@ -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'
ln -sfL $$(nix path-info '.#quox')/bin/quox quox
@echo [build] 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'
ln -sfL $$(nix path-info '.#quox-tests')/bin/quox-tests quox-tests
@echo [build] 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'
prove $$(nix path-info '.#quox-tests')/bin/quox-tests
nix build $(NIXFLAGS) --no-link '.#quox-tests'
prove $$(nix path-info $(NIXFLAGS) '.#quox-tests')/bin/quox-tests
.PHONY: clean
clean:
@echo [clean]
rm -f quox quox-tests result
.SILENT:

View File

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

View File

@ -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

View File

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

View File

@ -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

View File

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

View File

@ -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
Carlo Angiuli and
Daniel Gratzer},
author = {Jonathan Sterling and 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

View File

@ -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
opts : List (OptDescr OptMod)
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
public export
Mod : Type
Mod = Options -> IO Options
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
putStrLn "expecting getArgs to start with exe name"
exitFailure
[] => failureWith ["expected getArgs to start with exe name"]
export
getTestOpts : IO Options
getTestOpts =
case getOpt Permute opts !getArgs1 of
MkResult opts [] [] [] => pure $ makeOpts opts
res => do
traverse_ putStrLn $ res.errors ++ [usageInfo "quox test suite" opts]
exitFailure
MkResult opts [] [] [] => makeOpts opts
res => failureWith $ res.errors ++ usage

View File

@ -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
success : ToInfo a => a -> IO Result
success = pure . Tried True . toInfo
export
isRealTest : Test -> Bool
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
Left err => failure err
Right val => result True val
Left err => result False err
export %inline
export
test : (ToInfo e, ToInfo a) => String -> Lazy (Either e a) -> Test
test label val =
testIO label $ MkEitherT $ lazyToIO val
test label 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
Right val => failure [("success", val)]
Left err => if p err then result True () else result False err
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
header tests = "1..\{show $ length tests}"
export
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
Runner = ReaderT Nat IO
private %inline
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
record RunnerEnv where
constructor RE
indent : Nat
color : Bool
private
numbered : List a -> List (Nat, a)
numbered = go 1 where
Runner : Type -> Type
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}"]
local (plus 2) $ putIndentLines $ toLines info
Skip reason => putIndentLines
["ok \{show index} - \{test.label} # skip \{reason}"]
Todo reason => putIndentLines
["ok \{show index} - \{test.label} # todo \{reason}"]
putOk ok index test.label
local {indent $= plus 2} $ putIndentLines $ toLines info
Skip reason =>
putOk' Yellow True index "\{test.label} # skip \{reason}"
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}"]
res <- local (plus 4) $ runList tests
putIndentLines ["\{isOk res} \{show index} - \{label}"]
putIndentLines [!(col Magenta "# Subtest: ") ++ label]
res <- local {indent $= plus 4} $ runList tests
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]
all id <$> traverse run' (numbered tests)
putColor Cyan $ header 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
run ver tests = do
putStrLn "TAP version \{show ver}"
pure $ if !(runReaderT 0 $ runList tests)
main : Options -> List Test -> IO ExitCode
main opts tests = do
let tests = filterMatch opts.pattern $
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)

View File

@ -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
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
main = TAP.main !getTestOpts allTests

View File

@ -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
%hide Quox.Equal.subT
subT = Lib.subT
%hide Lib.subT
equalT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
equalT = Quox.Equal.equalT
%hide Quox.Equal.equalT
equalT = Lib.equalT
%hide Lib.equalT
subE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
subE = Quox.Equal.subE
%hide Quox.Equal.subE
subE = Lib.subE
%hide Lib.subE
equalE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
equalE = Quox.Equal.equalE
%hide Quox.Equal.equalE
equalE = Lib.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)))))
(Lam "x" (TUsed (Lam "y" (TUsed (BVT 0)))))
equalT (Lam "x" $ TUsed $ Lam "y" $ TUsed $ BVT 1)
(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",

116
tests/Tests/Reduce.idr Normal file
View File

@ -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")
]
]