Compare commits
9 Commits
cde2a9b0d6
...
bc9344c6ba
Author | SHA1 | Date |
---|---|---|
rhiannon morris | bc9344c6ba | |
rhiannon morris | bd57a976a8 | |
rhiannon morris | 221b69e8e8 | |
rhiannon morris | de3e13bad8 | |
rhiannon morris | 2b756ae1bb | |
rhiannon morris | 818d559d58 | |
rhiannon morris | 3cf246b4dc | |
rhiannon morris | b0692c15b9 | |
rhiannon morris | 25f9df34ab |
24
Makefile
24
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'
|
||||
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:
|
||||
|
|
|
@ -1,7 +1,6 @@
|
|||
module Quox.Equal
|
||||
|
||||
import public Quox.Syntax
|
||||
import public Quox.Reduce
|
||||
import Control.Monad.Either
|
||||
import Generics.Derive
|
||||
|
||||
|
|
|
@ -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
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -32,6 +32,5 @@ modules =
|
|||
Quox.Context,
|
||||
Quox.Equal,
|
||||
Quox.Name,
|
||||
Quox.Reduce,
|
||||
Quox.Typing,
|
||||
Quox.Typechecker
|
||||
|
|
16
quox.bib
16
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
|
||||
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
|
||||
|
|
|
@ -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
|
||||
|
|
228
tests/TAP.idr
228
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
|
||||
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)
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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",
|
||||
|
||||
|
|
|
@ -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")
|
||||
]
|
||||
]
|
Loading…
Reference in New Issue