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
|
all: quox
|
||||||
|
|
||||||
|
NIXFLAGS := --no-warn-dirty
|
||||||
|
|
||||||
# these two are real files, but always ask nix if they need remaking
|
# these two are real files, but always ask nix if they need remaking
|
||||||
.PHONY: quox
|
.PHONY: quox
|
||||||
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
|
.PHONY: quox-tests
|
||||||
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
|
.PHONY: lib
|
||||||
lib:
|
lib:
|
||||||
nix build --no-link '.#quox-lib'
|
@echo [build] quox-lib
|
||||||
|
nix build $(NIXFLAGS) --no-link '.#quox-lib'
|
||||||
|
|
||||||
.PHONY: test
|
.PHONY: test
|
||||||
test:
|
test:
|
||||||
nix run -- '.#quox-tests' -V 14
|
nix run $(NIXFLAGS) -- '.#quox-tests' -V 14 -c
|
||||||
|
|
||||||
.PHONY: prove
|
.PHONY: prove
|
||||||
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
|
.PHONY: clean
|
||||||
clean:
|
clean:
|
||||||
|
@echo [clean]
|
||||||
rm -f quox quox-tests result
|
rm -f quox quox-tests result
|
||||||
|
|
||||||
|
.SILENT:
|
||||||
|
|
|
@ -1,7 +1,6 @@
|
||||||
module Quox.Equal
|
module Quox.Equal
|
||||||
|
|
||||||
import public Quox.Syntax
|
import public Quox.Syntax
|
||||||
import public Quox.Reduce
|
|
||||||
import Control.Monad.Either
|
import Control.Monad.Either
|
||||||
import Generics.Derive
|
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
|
%name DScopeTerm body
|
||||||
|
|
||||||
public export %inline
|
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
|
||| same as `F` but as a term
|
||||||
public export %inline
|
public export %inline
|
||||||
|
|
|
@ -83,7 +83,10 @@ mutual
|
||||||
pushSubstsEWith th ph (F x) =
|
pushSubstsEWith th ph (F x) =
|
||||||
ncloE $ F x
|
ncloE $ F x
|
||||||
pushSubstsEWith th ph (B i) =
|
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) =
|
pushSubstsEWith th ph (f :@ s) =
|
||||||
ncloE $ subs f th ph :@ subs s th ph
|
ncloE $ subs f th ph :@ subs s th ph
|
||||||
pushSubstsEWith th ph (s :# a) =
|
pushSubstsEWith th ph (s :# a) =
|
||||||
|
@ -162,3 +165,135 @@ weakT t = t //. shift 1
|
||||||
public export %inline
|
public export %inline
|
||||||
weakE : Elim d n -> Elim d (S n)
|
weakE : Elim d n -> Elim d (S n)
|
||||||
weakE t = t //. shift 1
|
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.Context,
|
||||||
Quox.Equal,
|
Quox.Equal,
|
||||||
Quox.Name,
|
Quox.Name,
|
||||||
Quox.Reduce,
|
|
||||||
Quox.Typing,
|
Quox.Typing,
|
||||||
Quox.Typechecker
|
Quox.Typechecker
|
||||||
|
|
16
quox.bib
16
quox.bib
|
@ -72,10 +72,20 @@
|
||||||
doi = {10.1145/1292597.1292608}
|
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,
|
@inproceedings{xtt,
|
||||||
author = {Jonathan Sterling and
|
author = {Jonathan Sterling and Carlo Angiuli and Daniel Gratzer},
|
||||||
Carlo Angiuli and
|
|
||||||
Daniel Gratzer},
|
|
||||||
editor = {Herman Geuvers},
|
editor = {Herman Geuvers},
|
||||||
title = {Cubical Syntax for Reflection-Free Extensional Equality},
|
title = {Cubical Syntax for Reflection-Free Extensional Equality},
|
||||||
booktitle = {4th International Conference on Formal Structures for Computation
|
booktitle = {4th International Conference on Formal Structures for Computation
|
||||||
|
|
|
@ -4,41 +4,110 @@ import Data.String
|
||||||
import System
|
import System
|
||||||
import System.Console.GetOpt
|
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
|
public export
|
||||||
record Options where
|
record Options where
|
||||||
constructor Opts
|
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 : IO (List String)
|
||||||
getArgs1 =
|
getArgs1 =
|
||||||
case !getArgs of
|
case !getArgs of
|
||||||
_ :: args => pure args
|
_ :: args => pure args
|
||||||
[] => do
|
[] => failureWith ["expected getArgs to start with exe name"]
|
||||||
putStrLn "expecting getArgs to start with exe name"
|
|
||||||
exitFailure
|
|
||||||
|
|
||||||
export
|
export
|
||||||
getTestOpts : IO Options
|
getTestOpts : IO Options
|
||||||
getTestOpts =
|
getTestOpts =
|
||||||
case getOpt Permute opts !getArgs1 of
|
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
|
|
||||||
|
|
208
tests/TAP.idr
208
tests/TAP.idr
|
@ -1,14 +1,20 @@
|
||||||
module TAP
|
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 public Control.Monad.Either
|
||||||
import Data.String
|
import Data.String
|
||||||
|
import Data.List
|
||||||
import Data.List.Elem
|
import Data.List.Elem
|
||||||
import Data.SnocList
|
import Data.SnocList
|
||||||
import Control.Monad.Reader
|
import Control.Monad.Reader
|
||||||
import Control.Monad.State
|
import Control.Monad.State
|
||||||
|
import Control.ANSI
|
||||||
import System
|
import System
|
||||||
|
|
||||||
|
%default total
|
||||||
|
|
||||||
|
|
||||||
public export
|
public export
|
||||||
Info : Type
|
Info : Type
|
||||||
Info = List (String, String)
|
Info = List (String, String)
|
||||||
|
@ -39,24 +45,30 @@ toLines xs = "---" :: concatMap toLines1 xs <+> ["..."]
|
||||||
|
|
||||||
public export interface ToInfo e where toInfo : e -> Info
|
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
|
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 : Lazy a -> IO a
|
||||||
lazyToIO val = primIO $ \w => MkIORes (force val) w
|
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 : (ToInfo e, ToInfo a) => String -> EitherT e IO a -> Test
|
||||||
testIO label act = One $ MakeTest label $ do
|
testIO label act = One $ MakeTest label $ do
|
||||||
case !(runEitherT act) of
|
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 : (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 : String -> String -> Test
|
||||||
todoWith label reason = One $ MakeTest label $ pure $ Todo reason
|
todoWith label reason = One $ MakeTest label $ pure $ Todo reason
|
||||||
|
|
||||||
export %inline
|
export
|
||||||
todo : String -> Test
|
todo : String -> Test
|
||||||
todo label = todoWith label ""
|
todo label = todoWith label ""
|
||||||
|
|
||||||
private %inline
|
private
|
||||||
makeSkip : String -> String -> Test
|
makeSkip : String -> String -> Test
|
||||||
makeSkip label reason = One $ MakeTest label $ pure $ Skip reason
|
makeSkip label reason = One $ MakeTest label $ pure $ Skip reason
|
||||||
|
|
||||||
export %inline
|
export
|
||||||
skipWith : Test -> String -> Test
|
skipWith : Test -> String -> Test
|
||||||
skipWith (One t) reason = makeSkip t.label reason
|
skipWith (One t) reason = makeSkip t.label reason
|
||||||
skipWith (Group l _) reason = makeSkip l reason
|
skipWith (Group l _) reason = makeSkip l reason
|
||||||
|
skipWith (Note n) _ = Note n
|
||||||
|
|
||||||
export %inline
|
export
|
||||||
skip : Test -> Test
|
skip : Test -> Test
|
||||||
skip test = skipWith test ""
|
skip test = skipWith test ""
|
||||||
|
|
||||||
|
@ -98,78 +110,119 @@ testThrows : (ToInfo e, Show a) =>
|
||||||
String -> (e -> Bool) -> Lazy (Either e a) -> Test
|
String -> (e -> Bool) -> Lazy (Either e a) -> Test
|
||||||
testThrows label p act = One $ MakeTest label $ do
|
testThrows label p act = One $ MakeTest label $ do
|
||||||
case !(lazyToIO act) of
|
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 :-
|
infix 1 :-
|
||||||
export %inline
|
export
|
||||||
(:-) : String -> List Test -> Test
|
(:-) : String -> List Test -> Test
|
||||||
(:-) = Group
|
(:-) = Group
|
||||||
|
|
||||||
export %inline
|
export
|
||||||
bailOut : Test
|
bailOut : Test
|
||||||
bailOut = One $ MakeTest "bail out" $ do
|
bailOut = One $ MakeTest "bail out" $ do
|
||||||
putStrLn "Bail out!"
|
putStrLn "Bail out!"
|
||||||
exitFailure
|
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
|
private
|
||||||
makePrefix : SnocList String -> String
|
|
||||||
makePrefix [<] = ""
|
|
||||||
makePrefix (xs :< x) = foldr (\a, b => "\{a}/\{b}") x xs
|
|
||||||
|
|
||||||
private %inline
|
|
||||||
withPrefix : SnocList String -> TestBase -> Test
|
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
|
mutual
|
||||||
export %inline
|
export
|
||||||
flattenWith : SnocList String -> List Test -> List Test
|
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
|
export
|
||||||
flatten1With : SnocList String -> Test -> List Test
|
flatten1With : SnocList String -> Test -> List Test
|
||||||
flatten1With pfx (One t) = [withPrefix pfx t]
|
flatten1With pfx (One t) = [withPrefix pfx t]
|
||||||
flatten1With pfx (Group x ts) = flattenWith (pfx :< x) ts
|
flatten1With pfx (Group x ts) = flattenWith (pfx :< x) ts
|
||||||
|
flatten1With pfx (Note n) = [Note n]
|
||||||
|
|
||||||
export %inline
|
export
|
||||||
flatten : List Test -> List Test
|
flatten : List Test -> List Test
|
||||||
flatten = flattenWith [<]
|
flatten = flattenWith [<]
|
||||||
|
|
||||||
export %inline
|
export
|
||||||
flatten1 : Test -> List Test
|
flatten1 : Test -> List Test
|
||||||
flatten1 = flatten1With [<]
|
flatten1 = flatten1With [<]
|
||||||
|
|
||||||
|
|
||||||
|
private
|
||||||
|
record RunnerEnv where
|
||||||
|
constructor RE
|
||||||
|
indent : Nat
|
||||||
|
color : Bool
|
||||||
|
|
||||||
|
|
||||||
private
|
private
|
||||||
Runner : Type -> Type
|
Runner : Type -> Type
|
||||||
Runner = ReaderT Nat IO
|
Runner = ReaderT RunnerEnv IO
|
||||||
|
|
||||||
private %inline
|
private
|
||||||
putIndentLines : List String -> Runner ()
|
putIndentLines : List String -> Runner ()
|
||||||
putIndentLines xs = traverse_ (putStrLn . indent !ask) xs
|
putIndentLines xs = traverse_ (putStrLn . indent (!ask).indent) xs
|
||||||
|
|
||||||
private %inline
|
private
|
||||||
isOk : Bool -> String
|
isOk : Bool -> String
|
||||||
isOk b = if b then "ok" else "not ok"
|
isOk b = if b then "ok" else "not ok"
|
||||||
|
|
||||||
private %inline
|
private
|
||||||
toBool : Result -> Bool
|
toBool : Result -> Bool
|
||||||
toBool (Tried ok _) = ok
|
toBool (Tried ok _) = ok
|
||||||
toBool _ = True
|
toBool _ = True
|
||||||
|
|
||||||
|
|
||||||
private
|
private
|
||||||
numbered : List a -> List (Nat, a)
|
numbered : (a -> Bool) -> List a -> List (Nat, a)
|
||||||
numbered = go 1 where
|
numbered p = go 1 where
|
||||||
go : Nat -> List a -> List (Nat, a)
|
go : Nat -> List a -> List (Nat, a)
|
||||||
go _ [] = []
|
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
|
private
|
||||||
run1' : (Nat, TestBase) -> Runner Bool
|
run1' : (Nat, TestBase) -> Runner Bool
|
||||||
|
@ -177,12 +230,12 @@ run1' (index, test) = do
|
||||||
res <- liftIO test.run
|
res <- liftIO test.run
|
||||||
case res of
|
case res of
|
||||||
Tried ok info => do
|
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
|
pure $ toBool res
|
||||||
|
|
||||||
mutual
|
mutual
|
||||||
|
@ -190,30 +243,47 @@ mutual
|
||||||
run' : (Nat, Test) -> Runner Bool
|
run' : (Nat, Test) -> Runner Bool
|
||||||
run' (index, One test) = run1' (index, test)
|
run' (index, One test) = run1' (index, test)
|
||||||
run' (index, Group label tests) = do
|
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
|
pure res
|
||||||
|
run' (_, Note note) = do
|
||||||
|
putIndentLines [!(col Magenta "# ") ++ note]
|
||||||
|
pure True
|
||||||
|
|
||||||
private
|
private
|
||||||
runList : List Test -> Runner Bool
|
runList : List Test -> Runner Bool
|
||||||
runList tests = do
|
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
|
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
|
then ExitSuccess
|
||||||
else ExitFailure 70
|
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.Unicode
|
||||||
import Tests.Lexer
|
import Tests.Lexer
|
||||||
import Tests.Parser
|
import Tests.Parser
|
||||||
|
import Tests.Reduce
|
||||||
import Tests.Equal
|
import Tests.Equal
|
||||||
import System
|
import System
|
||||||
|
|
||||||
|
@ -13,13 +14,8 @@ allTests = [
|
||||||
Unicode.tests,
|
Unicode.tests,
|
||||||
Lexer.tests,
|
Lexer.tests,
|
||||||
Parser.tests,
|
Parser.tests,
|
||||||
|
Reduce.tests,
|
||||||
Equal.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
|
|
||||||
|
|
|
@ -1,6 +1,6 @@
|
||||||
module Tests.Equal
|
module Tests.Equal
|
||||||
|
|
||||||
import Quox.Equal
|
import Quox.Equal as Lib
|
||||||
import Quox.Pretty
|
import Quox.Pretty
|
||||||
import TAP
|
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 : {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 : {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 : {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 : {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
|
export
|
||||||
|
@ -112,19 +112,35 @@ tests = "equality & subtyping" :- [
|
||||||
|
|
||||||
"lambda" :- [
|
"lambda" :- [
|
||||||
testEq "λ x ⇒ [x] ≡ λ x ⇒ [x]" $
|
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]" $
|
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]" $
|
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]" $
|
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]" $
|
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",
|
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