rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

new representation for scopes

Browse source
This commit is contained in:
rhiannon morris 2023-02-22 07:40:19 +01:00
parent c75f1514ba
commit 0e481a8098
14 changed files with 376 additions and 364 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
lib/Quox/Equal.idr
View file

@ -83,15 +83,15 @@ parameters (defs : Definitions' q g)
isSubSing ty =
let Element ty nc = whnf defs ty in
case ty of
TYPE _ => False
Pi {res, _} => isSubSing res.term
Lam {} => False
Sig {fst, snd, _} => isSubSing fst && isSubSing snd.term
Pair {} => False
Eq {} => True
DLam {} => False
E (s :# _) => isSubSing s
E _ => False
TYPE _ => False
Pi {res, _} => isSubSing res.term
Lam {} => False
Sig {fst, snd} => isSubSing fst && isSubSing snd.term
Pair {} => False
Eq {} => True
DLam {} => False
E (s :# _) => isSubSing s
E _ => False
parameters {auto _ : HasErr q m}
@ -141,13 +141,13 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
-- Γ, x : A ⊢ s = t : B
-- -----------------------------------------
-- Γ ⊢ (λx ⇒ s) = (λx ⇒ t) : (π·x : A) → B
(Lam _ b1, Lam _ b2) => compare0 ctx' res.term b1.term b2.term
(Lam b1, Lam b2) => compare0 ctx' res.term b1.term b2.term
-- Γ, x : A ⊢ s = e x : B
-- ----------------------------------
-- Γ ⊢ (λx ⇒ s) = e : (π·x : A) → B
(E e, Lam _ b) => eta e b
(Lam _ b, E e) => eta e b
(E e, Lam b) => eta e b
(Lam b, E e) => eta e b
(E e, E f) => Elim.compare0 ctx e f
_ => throwError $ WrongType ty s t
@ -156,8 +156,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
ctx' = ctx :< arg
eta : Elim q 0 n -> ScopeTerm q 0 n -> m ()
eta e (TUsed b) = compare0 ctx' res.term (toLamBody e) b
eta e (TUnused _) = clashT ty s t
eta e (S _ (Y b)) = compare0 ctx' res.term (toLamBody e) b
eta e (S _ (N _)) = clashT ty s t
compare0' ctx ty@(Sig {fst, snd, _}) s t = local {mode := Equal} $
case (s, t) of
@ -322,8 +322,8 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
Term.compare0 ctx arg s t
compare0' _ e@(_ :@ _) f _ _ = clashE e f
compare0' ctx (CasePair epi e _ eret _ _ ebody)
(CasePair fpi f _ fret _ _ fbody) ne nf =
compare0' ctx (CasePair epi e eret ebody)
(CasePair fpi f fret fbody) ne nf =
local {mode := Equal} $ do
compare0 ctx e f
ety <- computeElimType ctx e (noOr1 ne)
@ -334,7 +334,12 @@ parameters (defs : Definitions' q _) {auto _ : (CanEqual q m, Eq q)}
unless (epi == fpi) $ throwError $ ClashQ epi fpi
compare0' _ e@(CasePair {}) f _ _ = clashE e f
compare0' ctx (s :# a) (t :# _) _ _ = Term.compare0 ctx a s t
compare0' ctx (s :# a) (t :# b) _ _ =
Term.compare0 ctx !(bigger a b) s t
where
bigger : forall a. a -> a -> m a
bigger l r = asks mode <&> \case Super => l; _ => r
compare0' ctx (s :# a) f _ _ = Term.compare0 ctx a s (E f)
compare0' ctx e (t :# b) _ _ = Term.compare0 ctx b (E e) t
compare0' _ e@(_ :# _) f _ _ = clashE e f

4
lib/Quox/Name.idr
View file

@ -45,6 +45,10 @@ export
FromString Name where
fromString x = MakeName [<] (fromString x)
public export %inline
unq : BaseName -> Name
unq = MakeName [<]
export
toDots : Name -> String

16
lib/Quox/Pretty.idr
View file

@ -40,8 +40,8 @@ data HL
public export
data PPrec
= Outer
| Ann -- right of "::"
| AnnL -- left of "::"
| Ann -- right of "∷"
| AnnL -- left of "∷"
| Eq -- "_ ≡ _ : _"
| InEq -- arguments of ≡
-- ...
@ -153,12 +153,12 @@ withPrec d = local {prec := d}
public export data BinderSort = T | D
export %inline
unders : HasEnv m => BinderSort -> List Name -> m a -> m a
unders T xs = local {prec := Outer, tnames $= (xs ++)}
unders D xs = local {prec := Outer, dnames $= (xs ++)}
unders : HasEnv m => BinderSort -> List BaseName -> m a -> m a
unders T xs = local {prec := Outer, tnames $= (map unq xs ++)}
unders D xs = local {prec := Outer, dnames $= (map unq xs ++)}
export %inline
under : HasEnv m => BinderSort -> Name -> m a -> m a
under : HasEnv m => BinderSort -> BaseName -> m a -> m a
under t x = unders t [x]
@ -237,9 +237,9 @@ a </> b = cat [a, b]
||| wrapper for names that pretty-prints highlighted as a `TVar`.
public export data TVarName = TV Name
public export data TVarName = TV BaseName
export %inline PrettyHL TVarName where prettyM (TV x) = hlF TVar $ prettyM x
||| wrapper for names that pretty-prints highlighted as a `DVar`.
public export data DVarName = DV Name
public export data DVarName = DV BaseName
export %inline PrettyHL DVarName where prettyM (DV x) = hlF DVar $ prettyM x

30
lib/Quox/Reduce.idr
View file

@ -63,18 +63,18 @@ mutual
PushSubsts Term Reduce.isCloT where
pushSubstsWith th ph (TYPE l) =
nclo $ TYPE l
pushSubstsWith th ph (Pi qty x a body) =
nclo $ Pi qty x (a // th // ph) (body // th // ph)
pushSubstsWith th ph (Lam x body) =
nclo $ Lam x $ body // th // ph
pushSubstsWith th ph (Sig x a b) =
nclo $ Sig x (a // th // ph) (b // th // ph)
pushSubstsWith th ph (Pi qty a body) =
nclo $ Pi qty (a // th // ph) (body // th // ph)
pushSubstsWith th ph (Lam body) =
nclo $ Lam (body // th // ph)
pushSubstsWith th ph (Sig a b) =
nclo $ Sig (a // th // ph) (b // th // ph)
pushSubstsWith th ph (Pair s t) =
nclo $ Pair (s // th // ph) (t // th // ph)
pushSubstsWith th ph (Eq i ty l r) =
nclo $ Eq i (ty // th // ph) (l // th // ph) (r // th // ph)
pushSubstsWith th ph (DLam i body) =
nclo $ DLam i $ body // th // ph
pushSubstsWith th ph (Eq ty l r) =
nclo $ Eq (ty // th // ph) (l // th // ph) (r // th // ph)
pushSubstsWith th ph (DLam body) =
nclo $ DLam (body // th // ph)
pushSubstsWith th ph (E e) =
let Element e nc = pushSubstsWith th ph e in nclo $ E e
pushSubstsWith th ph (CloT s ps) =
@ -93,8 +93,8 @@ mutual
Right no => Element res no
pushSubstsWith th ph (f :@ s) =
nclo $ (f // th // ph) :@ (s // th // ph)
pushSubstsWith th ph (CasePair pi p x r y z b) =
nclo $ CasePair pi (p // th // ph) x (r // th // ph) y z (b // th // ph)
pushSubstsWith th ph (CasePair pi p r b) =
nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph)
pushSubstsWith th ph (f :% d) =
nclo $ (f // th // ph) :% (d // th)
pushSubstsWith th ph (s :# a) =
@ -197,13 +197,13 @@ mutual
let Element f fnf = whnf defs f in
case nchoose $ isLamHead f of
Left _ =>
let Lam {body, _} :# Pi {arg, res, _} = f
let Lam body :# Pi {arg, res, _} = f
s = s :# arg
in
whnf defs $ sub1 body s :# sub1 res s
Right nlh => Element (f :@ s) $ fnf `orNo` nlh
whnf defs (CasePair pi pair r ret x y body) =
whnf defs (CasePair pi pair ret body) =
let Element pair pairnf = whnf defs pair in
case nchoose $ isPairHead pair of
Left _ =>
@ -219,7 +219,7 @@ mutual
let Element f fnf = whnf defs f in
case nchoose $ isDLamHead f of
Left _ =>
let DLam {body, _} :# Eq {ty, l, r, _} = f
let DLam body :# Eq {ty = ty, l, r, _} = f
body = endsOr l r (dsub1 body p) p
in
whnf defs $ body :# dsub1 ty p

66
lib/Quox/Syntax/Term/Base.idr
View file

@ -47,22 +47,20 @@ mutual
TYPE : (l : Universe) -> Term q d n
||| function type
Pi : (qty : q) -> (x : Name) ->
(arg : Term q d n) -> (res : ScopeTerm q d n) -> Term q d n
Pi : (qty : q) -> (arg : Term q d n) ->
(res : ScopeTerm q d n) -> Term q d n
||| function term
Lam : (x : Name) -> (body : ScopeTerm q d n) -> Term q d n
Lam : (body : ScopeTerm q d n) -> Term q d n
||| pair type
Sig : (x : Name) -> (fst : Term q d n) -> (snd : ScopeTerm q d n) ->
Term q d n
Sig : (fst : Term q d n) -> (snd : ScopeTerm q d n) -> Term q d n
||| pair value
Pair : (fst, snd : Term q d n) -> Term q d n
||| equality type
Eq : (i : Name) -> (ty : DScopeTerm q d n) -> (l, r : Term q d n) ->
Term q d n
Eq : (ty : DScopeTerm q d n) -> (l, r : Term q d n) -> Term q d n
||| equality term
DLam : (i : Name) -> (body : DScopeTerm q d n) -> Term q d n
DLam : (body : DScopeTerm q d n) -> Term q d n
||| elimination
E : (e : Elim q d n) -> Term q d n
@ -87,11 +85,11 @@ mutual
||| pair destruction
|||
||| `CasePair 𝜋 𝑒 𝑟 𝐴 𝑥 𝑦 𝑡` is
||| `CasePair 𝜋 𝑒 ([𝑟], 𝐴) ([𝑥, 𝑦], 𝑡)` is
||| `𝐜𝐚𝐬𝐞 𝜋 · 𝑒 𝐫𝐞𝐭𝐮𝐫𝐧 𝑟 ⇒ 𝐴 𝐨𝐟 { (𝑥, 𝑦) ⇒ 𝑡 }`
CasePair : (qty : q) -> (pair : Elim q d n) ->
(r : Name) -> (ret : ScopeTerm q d n) ->
(x, y : Name) -> (body : ScopeTermN 2 q d n) ->
(ret : ScopeTerm q d n) ->
(body : ScopeTermN 2 q d n) ->
Elim q d n
||| dim application
@ -107,49 +105,51 @@ mutual
DCloE : (el : Elim q dfrom n) -> (th : Lazy (DSubst dfrom dto)) ->
Elim q dto n
||| a scope with some more bound term variables
public export
data ScopeTermN : Nat -> TermLike where
||| at least some variables are used
TUsed : (body : Term q d (s + n)) -> ScopeTermN s q d n
||| all variables are unused
TUnused : (body : Term q d n) -> ScopeTermN s q d n
0 CaseEnumArms : TermLike
CaseEnumArms q d n = SortedMap TagVal (Term q d n)
||| a scoped term with names
public export
record Scoped (s : Nat) (f : Nat -> Type) (n : Nat) where
constructor S
names : Vect s BaseName
body : ScopedBody s f n
public export
0 ScopeTerm : TermLike
ScopeTerm = ScopeTermN 1
||| a scope with some more bound dimension variable
public export
data DScopeTermN : Nat -> TermLike where
||| at least some variables are used
DUsed : (body : Term q (s + d) n) -> DScopeTermN s q d n
||| all variables are unused
DUnused : (body : Term q d n) -> DScopeTermN s q d n
data ScopedBody : Nat -> (Nat -> Type) -> Nat -> Type where
Y : (body : f (s + n)) -> ScopedBody s f n
N : (body : f n) -> ScopedBody s f n
public export
0 DScopeTerm : TermLike
0 ScopeTermN, DScopeTermN : Nat -> TermLike
ScopeTermN s q d n = Scoped s (Term q d) n
DScopeTermN s q d n = Scoped s (\d => Term q d n) d
public export
0 ScopeTerm, DScopeTerm : TermLike
ScopeTerm = ScopeTermN 1
DScopeTerm = DScopeTermN 1
%name Term s, t, r
%name Elim e, f
%name ScopeTermN body
%name DScopeTermN body
%name Scoped body
%name ScopedBody body
||| non dependent function type
public export %inline
Arr : (qty : q) -> (arg, res : Term q d n) -> Term q d n
Arr {qty, arg, res} = Pi {qty, x = "_", arg, res = TUnused res}
Arr {qty, arg, res} = Pi {qty, arg, res = S ["_"] $ N res}
||| non dependent equality type
public export %inline
Eq0 : (ty, l, r : Term q d n) -> Term q d n
Eq0 {ty, l, r} = Eq {i = "_", ty = DUnused ty, l, r}
Eq0 {ty, l, r} = Eq {ty = S ["_"] $ N ty, l, r}
||| non dependent pair type
public export %inline
And : (fst, snd : Term q d n) -> Term q d n
And {fst, snd} = Sig {x = "_", fst, snd = TUnused snd}
And {fst, snd} = Sig {fst, snd = S ["_"] $ N snd}
||| same as `F` but as a term
public export %inline

131
lib/Quox/Syntax/Term/Pretty.idr
View file

@ -32,25 +32,80 @@ ofD = hl Syntax "of"
returnD = hl Syntax "return"
export covering
prettyBindType : Pretty.HasEnv m =>
PrettyHL q => PrettyHL a => PrettyHL b =>
List q -> BaseName -> a -> Doc HL -> b -> m (Doc HL)
prettyBindType qtys x s arr t =
parensIfM Outer $ hang 2 $
parens !(prettyQtyBinds qtys $ TV x) <++> arr
<//> !(under T x $ prettyM t)
export covering
prettyLams : Pretty.HasEnv m => PrettyHL a =>
BinderSort -> List BaseName -> a -> m (Doc HL)
prettyLams sort names body = do
lam <- case sort of T => lamD; D => dlamD
header <- sequence $ [hl TVar <$> prettyM x | x <- names] ++ [darrowD]
body <- unders sort names $ prettyM body
parensIfM Outer $ sep (lam :: header) <//> body
export covering
prettyApps : Pretty.HasEnv m => PrettyHL f => PrettyHL a =>
f -> List a -> m (Doc HL)
prettyApps fun args =
parensIfM App =<< withPrec Arg
[|prettyM fun <//> (align . sep <$> traverse prettyM args)|]
export covering
prettyTuple : Pretty.HasEnv m => PrettyHL a => List a -> m (Doc HL)
prettyTuple = map (parens . align . separate commaD) . traverse prettyM
export covering
prettyArm : Pretty.HasEnv m => PrettyHL a =>
(List BaseName, Doc HL, a) -> m (Doc HL)
prettyArm (xs, pat, body) =
pure $ hang 2 $ sep
[hsep [pat, !darrowD],
!(withPrec Outer $ unders T xs $ prettyM body)]
export covering
prettyArms : Pretty.HasEnv m => PrettyHL a =>
List (List BaseName, Doc HL, a) -> m (Doc HL)
prettyArms = map (braces . align . sep) . traverse prettyArm
export covering
prettyCase : Pretty.HasEnv m =>
PrettyHL q => PrettyHL a => PrettyHL b => PrettyHL c =>
q -> a -> BaseName -> b -> List (List BaseName, Doc HL, c) ->
m (Doc HL)
prettyCase pi elim r ret arms =
pure $ align $ sep $
[hsep [caseD, !(prettyQtyBinds [pi] elim)],
hsep [returnD, !(prettyM r), !darrowD, !(under T r $ prettyM ret)],
hsep [ofD, !(prettyArms arms)]]
mutual
export covering
PrettyHL q => PrettyHL (Term q d n) where
prettyM (TYPE l) =
parensIfM App $ typeD <//> !(withPrec Arg $ prettyM l)
prettyM (Pi qty x s t) =
prettyM (Pi qty s (S [x] t)) =
prettyBindType [qty] x s !arrowD t
prettyM (Lam x t) =
let GotLams {names, body, _} = getLams' [x] t.term Refl in
prettyM (Lam (S x t)) =
let GotLams {names, body, _} = getLams' x t.term Refl in
prettyLams T (toList names) body
prettyM (Sig x s t) =
prettyBindType [] x s !timesD t
prettyM (Sig s (S [x] t)) =
prettyBindType {q} [] x s !timesD t
prettyM (Pair s t) =
let GotPairs {init, last, _} = getPairs t in
prettyTuple $ s :: init ++ [last]
prettyM (Eq _ (DUnused ty) l r) =
prettyM (Eq (S _ (N ty)) l r) =
parensIfM Eq !(withPrec InEq $ pure $
sep [!(prettyM l) <++> !eqndD, !(prettyM r) <++> colonD, !(prettyM ty)])
prettyM (Eq i (DUsed ty) l r) =
sep [!(prettyM l) <++> !eqndD,
!(prettyM r) <++> colonD, !(prettyM ty)])
prettyM (Eq (S [i] (Y ty)) l r) =
parensIfM App $
eqD <++>
sep [bracks !(withPrec Outer $ pure $ hang 2 $
@ -58,8 +113,8 @@ mutual
!(under D i $ prettyM ty)]),
!(withPrec Arg $ prettyM l),
!(withPrec Arg $ prettyM r)]
prettyM (DLam i t) =
let GotDLams {names, body, _} = getDLams' [i] t.term Refl in
prettyM (DLam (S i t)) =
let GotDLams {names, body, _} = getDLams' i t.term Refl in
prettyLams D (toList names) body
prettyM (E e) = bracks <$> prettyM e
prettyM (CloT s th) =
@ -78,7 +133,7 @@ mutual
prettyM (e :@ s) =
let GotArgs {fun, args, _} = getArgs' e [s] in
prettyApps fun args
prettyM (CasePair pi p r ret x y body) = do
prettyM (CasePair pi p (S [r] ret) (S [x, y] body)) = do
pat <- (parens . separate commaD . map (hl TVar)) <$>
traverse prettyM [x, y]
prettyCase pi p r ret [([x, y], pat, body)]
@ -97,62 +152,10 @@ mutual
[|withPrec SApp (prettyM e) </> prettyDSubst th|]
export covering
{s : Nat} -> PrettyHL q => PrettyHL (ScopeTermN s q d n) where
{s : Nat} -> PrettyHL q => PrettyHL (ScopedBody s (Term q d) n) where
prettyM body = prettyM body.term
export covering
prettyTSubst : Pretty.HasEnv m => PrettyHL q =>
TSubst q d from to -> m (Doc HL)
prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s
export covering
prettyBindType : Pretty.HasEnv m => PrettyHL q =>
List q -> Name -> Term q d n -> Doc HL ->
ScopeTerm q d n -> m (Doc HL)
prettyBindType qtys x s arr t =
parensIfM Outer $ hang 2 $
parens !(prettyQtyBinds qtys $ TV x) <++> arr
<//> !(under T x $ prettyM t)
export covering
prettyLams : Pretty.HasEnv m => PrettyHL q =>
BinderSort -> List Name -> Term q _ _ -> m (Doc HL)
prettyLams sort names body = do
lam <- case sort of T => lamD; D => dlamD
header <- sequence $ [hl TVar <$> prettyM x | x <- names] ++ [darrowD]
body <- unders sort names $ prettyM body
parensIfM Outer $ sep (lam :: header) <//> body
export covering
prettyApps : Pretty.HasEnv m => PrettyHL f => PrettyHL a =>
f -> List a -> m (Doc HL)
prettyApps fun args =
parensIfM App =<< withPrec Arg
[|prettyM fun <//> (align . sep <$> traverse prettyM args)|]
export covering
prettyTuple : Pretty.HasEnv m => PrettyHL a => List a -> m (Doc HL)
prettyTuple = map (parens . align . separate commaD) . traverse prettyM
export covering
prettyArm : Pretty.HasEnv m => PrettyHL a =>
(List Name, Doc HL, a) -> m (Doc HL)
prettyArm (xs, pat, body) =
pure $ hang 2 $ sep
[hsep [pat, !darrowD],
!(withPrec Outer $ unders T xs $ prettyM body)]
export covering
prettyArms : Pretty.HasEnv m => PrettyHL a =>
List (List Name, Doc HL, a) -> m (Doc HL)
prettyArms = map (braces . align . sep) . traverse prettyArm
export covering
prettyCase : Pretty.HasEnv m =>
PrettyHL q => PrettyHL a => PrettyHL b => PrettyHL c =>
q -> a -> Name -> b -> List (List Name, Doc HL, c) -> m (Doc HL)
prettyCase pi elim r ret arms =
pure $ align $ sep $
[hsep [caseD, !(prettyQtyBinds [pi] elim)],
hsep [returnD, !(prettyM r), !darrowD, !(under T r $ prettyM ret)],
hsep [ofD, !(prettyArms arms)]]

36
lib/Quox/Syntax/Term/Split.idr
View file

@ -11,8 +11,8 @@ import public Data.Vect
public export %inline
isLam : Term {} -> Bool
isLam (Lam {}) = True
isLam _ = False
isLam (Lam _) = True
isLam _ = False
public export
0 NotLam : Pred $ Term {}
@ -21,8 +21,8 @@ NotLam = No . isLam
public export %inline
isDLam : Term {} -> Bool
isDLam (DLam {}) = True
isDLam _ = False
isDLam (DLam _) = True
isDLam _ = False
public export
0 NotDLam : Pred $ Term {}
@ -113,25 +113,25 @@ getDArgs e = getDArgs' e []
infixr 1 :\\
public export
absN : Vect m Name -> Term q d (m + n) -> Term q d n
absN : Vect m BaseName -> Term q d (m + n) -> Term q d n
absN {m = 0} [] s = s
absN {m = S m} (x :: xs) s = Lam x $ TUsed $ absN xs $
rewrite sym $ plusSuccRightSucc m n in s
absN {m = S m} (x :: xs) s =
Lam $ S [x] $ Y $ absN xs $ rewrite sym $ plusSuccRightSucc m n in s
public export %inline
(:\\) : Vect m Name -> Term q d (m + n) -> Term q d n
(:\\) : Vect m BaseName -> Term q d (m + n) -> Term q d n
(:\\) = absN
infixr 1 :\\%
public export
dabsN : Vect m Name -> Term q (m + d) n -> Term q d n
dabsN : Vect m BaseName -> Term q (m + d) n -> Term q d n
dabsN {m = 0} [] s = s
dabsN {m = S m} (x :: xs) s = DLam x $ DUsed $ dabsN xs $
rewrite sym $ plusSuccRightSucc m d in s
dabsN {m = S m} (x :: xs) s =
DLam $ S [x] $ Y $ dabsN xs $ rewrite sym $ plusSuccRightSucc m d in s
public export %inline
(:\\%) : Vect m Name -> Term q (m + d) n -> Term q d n
(:\\%) : Vect m BaseName -> Term q (m + d) n -> Term q d n
(:\\%) = dabsN
@ -139,17 +139,17 @@ public export
record GetLams q d n where
constructor GotLams
{0 lams, rest : Nat}
names : Vect lams Name
names : Vect lams BaseName
body : Term q d rest
0 eq : lams + n = rest
0 notLam : NotLam body
export
getLams' : forall lams, rest.
Vect lams Name -> Term q d rest -> (0 eq : lams + n = rest) ->
Vect lams BaseName -> Term q d rest -> (0 eq : lams + n = rest) ->
GetLams q d n
getLams' xs s Refl = case nchoose $ isLam s of
Left y => let Lam x body = s in
Left y => let Lam (S [x] body) = s in
getLams' (x :: xs) (assert_smaller s body.term) Refl
Right n => GotLams xs s Refl n
@ -162,17 +162,17 @@ public export
record GetDLams q d n where
constructor GotDLams
{0 lams, rest : Nat}
names : Vect lams Name
names : Vect lams BaseName
body : Term q rest n
0 eq : lams + d = rest
0 notDLam : NotDLam body
export
getDLams' : forall lams, rest.
Vect lams Name -> Term q rest n -> (0 eq : lams + d = rest) ->
Vect lams BaseName -> Term q rest n -> (0 eq : lams + d = rest) ->
GetDLams q d n
getDLams' is s Refl = case nchoose $ isDLam s of
Left y => let DLam i body = s in
Left y => let DLam (S [i] body) = s in
getDLams' (i :: is) (assert_smaller s body.term) Refl
Right n => GotDLams is s Refl n

143
lib/Quox/Syntax/Term/Subst.idr
View file

@ -10,49 +10,53 @@ namespace CanDSubst
interface CanDSubst (0 tm : Nat -> Nat -> Type) where
(//) : tm dfrom n -> Lazy (DSubst dfrom dto) -> tm dto n
mutual
||| does the minimal reasonable work:
||| - deletes the closure around an atomic constant like `TYPE`
||| - deletes an identity substitution
||| - composes (lazily) with an existing top-level dim-closure
||| - otherwise, wraps in a new closure
export
CanDSubst (Term q) where
s // Shift SZ = s
TYPE l // _ = TYPE l
DCloT s ph // th = DCloT s $ ph . th
s // th = DCloT s th
||| does the minimal reasonable work:
||| - deletes the closure around an atomic constant like `TYPE`
||| - deletes an identity substitution
||| - composes (lazily) with an existing top-level dim-closure
||| - otherwise, wraps in a new closure
export
CanDSubst (Term q) where
s // Shift SZ = s
TYPE l // _ = TYPE l
DCloT s ph // th = DCloT s $ ph . th
s // th = DCloT s th
private
subDArgs : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
subDArgs (f :% d) th = subDArgs f th :% (d // th)
subDArgs e th = DCloE e th
private
subDArgs : Elim q dfrom n -> DSubst dfrom dto -> Elim q dto n
subDArgs (f :% d) th = subDArgs f th :% (d // th)
subDArgs e th = DCloE e th
||| does the minimal reasonable work:
||| - deletes the closure around a term variable
||| - deletes an identity substitution
||| - composes (lazily) with an existing top-level dim-closure
||| - immediately looks up bound variables in a
||| top-level sequence of dimension applications
||| - otherwise, wraps in a new closure
export
CanDSubst (Elim q) where
e // Shift SZ = e
F x // _ = F x
B i // _ = B i
f :% d // th = subDArgs (f :% d) th
DCloE e ph // th = DCloE e $ ph . th
e // th = DCloE e th
||| does the minimal reasonable work:
||| - deletes the closure around a term variable
||| - deletes an identity substitution
||| - composes (lazily) with an existing top-level dim-closure
||| - immediately looks up bound variables in a
||| top-level sequence of dimension applications
||| - otherwise, wraps in a new closure
export
CanDSubst (Elim q) where
e // Shift SZ = e
F x // _ = F x
B i // _ = B i
f :% d // th = subDArgs (f :% d) th
DCloE e ph // th = DCloE e $ ph . th
e // th = DCloE e th
export
CanDSubst (ScopeTermN s q) where
TUsed body // th = TUsed $ body // th
TUnused body // th = TUnused $ body // th
namespace DSubst.ScopeTermN
export %inline
(//) : ScopeTermN s q dfrom n -> Lazy (DSubst dfrom dto) ->
ScopeTermN s q dto n
S ns (Y body) // th = S ns $ Y $ body // th
S ns (N body) // th = S ns $ N $ body // th
export
{s : Nat} -> CanDSubst (DScopeTermN s q) where
DUsed body // th = DUsed $ body // pushN s th
DUnused body // th = DUnused $ body // th
namespace DSubst.DScopeTermN
export %inline
(//) : {s : Nat} ->
DScopeTermN s q dfrom n -> Lazy (DSubst dfrom dto) ->
DScopeTermN s q dto n
S ns (Y body) // th = S ns $ Y $ body // pushN s th
S ns (N body) // th = S ns $ N $ body // th
export %inline FromVar (Elim q d) where fromVar = B
@ -94,15 +98,21 @@ CanTSubst Term where
Shift SZ => s
th => CloT s th
export %inline
{s : Nat} -> CanTSubst (ScopeTermN s) where
TUsed body // th = TUsed $ body // pushN s th
TUnused body // th = TUnused $ body // th
namespace ScopeTermN
export %inline
(//) : {s : Nat} ->
ScopeTermN s q d from -> Lazy (TSubst q d from to) ->
ScopeTermN s q d to
S ns (Y body) // th = S ns $ Y $ body // pushN s th
S ns (N body) // th = S ns $ N $ body // th
export %inline
{s : Nat} -> CanTSubst (DScopeTermN s) where
DUsed body // th = DUsed $ body // map (// shift s) th
DUnused body // th = DUnused $ body // th
namespace DScopeTermN
export %inline
(//) : {s : Nat} ->
DScopeTermN s q d from -> Lazy (TSubst q d from to) ->
DScopeTermN s q d to
S ns (Y body) // th = S ns $ Y $ body // map (// shift s) th
S ns (N body) // th = S ns $ N $ body // th
export %inline CanShift (Term q d) where s // by = s // Shift by
export %inline CanShift (Elim q d) where e // by = e // Shift by
@ -136,23 +146,34 @@ weakE : {default 1 by : Nat} -> Elim q d n -> Elim q d (by + n)
weakE t = t // shift by
namespace ScopeTermN
export %inline
(.term) : {s : Nat} -> ScopeTermN s q d n -> Term q d (s + n)
(TUsed body).term = body
(TUnused body).term = weakT body {by = s}
parameters {s : Nat}
namespace ScopeTermBody
export %inline
(.term) : ScopedBody s (Term q d) n -> Term q d (s + n)
(Y b).term = b
(N b).term = weakT b {by = s}
namespace DScopeTermN
export %inline
(.term) : {s : Nat} -> DScopeTermN s q d n -> Term q (s + d) n
(DUsed body).term = body
(DUnused body).term = dweakT body {by = s}
namespace ScopeTermN
export %inline
(.term) : ScopeTermN s q d n -> Term q d (s + n)
t.term = t.body.term
namespace DScopeTermBody
export %inline
(.term) : ScopedBody s (\d => Term q d n) d -> Term q (s + d) n
(Y b).term = b
(N b).term = dweakT b {by = s}
namespace DScopeTermN
export %inline
(.term) : DScopeTermN s q d n -> Term q (s + d) n
t.term = t.body.term
export %inline
subN : ScopeTermN s q d n -> Vect s (Elim q d n) -> Term q d n
subN (TUsed body) es = body // fromVect es
subN (TUnused body) _ = body
subN (S _ (Y body)) es = body // fromVect es
subN (S _ (N body)) _ = body
export %inline
sub1 : ScopeTerm q d n -> Elim q d n -> Term q d n
@ -160,8 +181,8 @@ sub1 t e = subN t [e]
export %inline
dsubN : DScopeTermN s q d n -> Vect s (Dim d) -> Term q d n
dsubN (DUsed body) ps = body // fromVect ps
dsubN (DUnused body) _ = body
dsubN (S _ (Y body)) ps = body // fromVect ps
dsubN (S _ (N body)) _ = body
export %inline
dsub1 : DScopeTerm q d n -> Dim d -> Term q d n

60
lib/Quox/Typechecker.idr
View file

@ -28,29 +28,9 @@ popQ pi = popQs [< pi]
private %inline
weakI : IsQty q => InferResult' q d n -> InferResult' q d (S n)
weakI = {type $= weakT, qout $= (:< zero)}
private
lookupBound : IsQty q => q -> Var n -> TContext q d n -> InferResult' q d n
lookupBound pi VZ (ctx :< ty) =
InfRes {type = weakT ty, qout = (zero <$ ctx) :< pi}
lookupBound pi (VS i) (ctx :< _) =
weakI $ lookupBound pi i ctx
private %inline
lookupFree : CanTC' q g m => Name -> m (Definition' q g)
lookupFree x = lookupFree' !ask x
parameters {auto _ : IsQty q} {auto _ : CanTC q m}
mutual
-- [todo] it seems like the options here for dealing with substitutions are
-- to either push them or parametrise the whole typechecker over ambient
-- substitutions. both of them seem like the same amount of work for the
-- computer but pushing is less work for the me
||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ"
|||
||| `check ctx sg subj ty` checks that in the context `ctx`, the term
@ -116,19 +96,19 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
unless (k < l) $ throwError $ BadUniverse k l
pure $ zeroFor ctx
check' ctx sg (Pi qty _ arg res) ty = do
check' ctx sg (Pi qty arg res) ty = do
l <- expectTYPE !ask ty
expectEqualQ zero sg.fst
-- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
check0 ctx arg (TYPE l)
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
case res of
TUsed res => check0 (extendTy arg ctx) res (TYPE l)
TUnused res => check0 ctx res (TYPE l)
case res.body of
Y res => check0 (extendTy arg ctx) res (TYPE l)
N res => check0 ctx res (TYPE l)
-- then Ψ | Γ ⊢₀ (π·x : A) → B ⇐ Type ℓ
pure $ zeroFor ctx
check' ctx sg (Lam _ body) ty = do
check' ctx sg (Lam body) ty = do
(qty, arg, res) <- expectPi !ask ty
-- if Ψ | Γ, x : A ⊢ σ · t ⇐ B ⊳ Σ, ρ·x
-- with ρ ≤ σπ
@ -137,15 +117,15 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
-- then Ψ | Γ ⊢ σ · (λx ⇒ t) ⇐ (π·x : A) → B ⊳ Σ
popQ qty' qout
check' ctx sg (Sig _ fst snd) ty = do
check' ctx sg (Sig fst snd) ty = do
l <- expectTYPE !ask ty
expectEqualQ zero sg.fst
-- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
check0 ctx fst (TYPE l)
-- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
case snd of
TUsed snd => check0 (extendTy fst ctx) snd (TYPE l)
TUnused snd => check0 ctx snd (TYPE l)
case snd.body of
Y snd => check0 (extendTy fst ctx) snd (TYPE l)
N snd => check0 ctx snd (TYPE l)
-- then Ψ | Γ ⊢₀ (x : A) × B ⇐ Type ℓ
pure $ zeroFor ctx
@ -159,13 +139,13 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
-- then Ψ | Γ ⊢ σ · (s, t) ⇐ (x : A) × B ⊳ Σ₁ + Σ₂
pure $ qfst + qsnd
check' ctx sg (Eq _ t l r) ty = do
check' ctx sg (Eq t l r) ty = do
u <- expectTYPE !ask ty
expectEqualQ zero sg.fst
-- if Ψ, i | Γ ⊢₀ A ⇐ Type ℓ
case t of
DUsed t => check0 (extendDim ctx) t (TYPE u)
DUnused t => check0 ctx t (TYPE u)
case t.body of
Y t => check0 (extendDim ctx) t (TYPE u)
N t => check0 ctx t (TYPE u)
-- if Ψ | Γ ⊢₀ l ⇐ A‹0›
check0 ctx t.zero l
-- if Ψ | Γ ⊢₀ r ⇐ A‹1›
@ -173,7 +153,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
-- then Ψ | Γ ⊢₀ Eq [i ⇒ A] l r ⇐ Type ℓ
pure $ zeroFor ctx
check' ctx sg (DLam _ body) ty = do
check' ctx sg (DLam body) ty = do
(ty, l, r) <- expectEq !ask ty
-- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ
qout <- checkC (extendDim ctx) sg body.term ty.term
@ -204,11 +184,21 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
expectCompatQ sg.fst g.qty
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ 𝟎
pure $ InfRes {type = g.type.get, qout = zeroFor ctx}
where
lookupFree : Name -> m (Definition q)
lookupFree x = lookupFree' !ask x
infer' ctx sg (B i) =
-- if x : A ∈ Γ
-- then Ψ | Γ ⊢ σ · x ⇒ A ⊳ (𝟎, σ·x, 𝟎)
pure $ lookupBound sg.fst i ctx.tctx
where
lookupBound : q -> Var n -> TContext q d n -> InferResult' q d n
lookupBound pi VZ (ctx :< ty) =
InfRes {type = weakT ty, qout = zeroFor ctx :< pi}
lookupBound pi (VS i) (ctx :< _) =
let InfRes {type, qout} = lookupBound pi i ctx in
InfRes {type = weakT type, qout = qout :< zero}
infer' ctx sg (fun :@ arg) = do
-- if Ψ | Γ ⊢ σ · f ⇒ (π·x : A) → B ⊳ Σ₁
@ -222,7 +212,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
qout = funres.qout + argout
}
infer' ctx sg (CasePair pi pair _ ret _ _ body) = do
infer' ctx sg (CasePair pi pair ret body) = do
-- if 1 ≤ π
expectCompatQ one pi
-- if Ψ | Γ ⊢ 1 · pair ⇒ (x : A) × B ⊳ Σ₁

6
lib/Quox/Typing.idr
View file

@ -40,6 +40,10 @@ namespace TContext
pushD : TContext q d n -> TContext q (S d) n
pushD tel = map (// shift 1) tel
export %inline
zeroFor : IsQty q => Context tm n -> QOutput q n
zeroFor ctx = zero <$ ctx
namespace TyContext
public export %inline
empty : {d : Nat} -> TyContext q d 0
@ -75,7 +79,7 @@ namespace QOutput
export %inline
zeroFor : TyContext q _ n -> QOutput q n
zeroFor ctx = zero <$ ctx.tctx
zeroFor ctx = zeroFor ctx.tctx
public export

28
tests/TermImpls.idr
View file

@ -24,24 +24,24 @@ mutual
TYPE k == TYPE l = k == l
TYPE _ == _ = False
Pi qty1 _ arg1 res1 == Pi qty2 _ arg2 res2 =
Pi qty1 arg1 res1 == Pi qty2 arg2 res2 =
qty1 == qty2 && arg1 == arg2 && res1 == res2
Pi {} == _ = False
Lam _ body1 == Lam _ body2 = body1 == body2
Lam body1 == Lam body2 = body1 == body2
Lam {} == _ = False
Sig _ fst1 snd1 == Sig _ fst2 snd2 = fst1 == fst2 && snd1 == snd2
Sig fst1 snd1 == Sig fst2 snd2 = fst1 == fst2 && snd1 == snd2
Sig {} == _ = False
Pair fst1 snd1 == Pair fst2 snd2 = fst1 == fst2 && snd1 == snd2
Pair {} == _ = False
Eq _ ty1 l1 r1 == Eq _ ty2 l2 r2 =
Eq ty1 l1 r1 == Eq ty2 l2 r2 =
ty1 == ty2 && l1 == l2 && r1 == r2
Eq {} == _ = False
DLam _ body1 == DLam _ body2 = body1 == body2
DLam body1 == DLam body2 = body1 == body2
DLam {} == _ = False
E e == E f = e == f
@ -70,7 +70,7 @@ mutual
(fun1 :@ arg1) == (fun2 :@ arg2) = fun1 == fun2 && arg1 == arg2
(_ :@ _) == _ = False
CasePair q1 p1 _ r1 _ _ b1 == CasePair q2 p2 _ r2 _ _ b2 =
CasePair q1 p1 r1 b1 == CasePair q2 p2 r2 b2 =
q1 == q2 && p1 == p2 && r1 == r2 && b1 == b2
CasePair {} == _ = False
@ -93,18 +93,14 @@ mutual
DCloE {} == _ = False
export covering
Eq q => Eq (ScopeTermN s q d n) where
TUsed s == TUsed t = s == t
TUnused s == TUnused t = s == t
TUsed _ == TUnused _ = False
TUnused _ == TUsed _ = False
(forall n. Eq (f n)) => Eq (ScopedBody s f n) where
Y x == Y y = x == y
N x == N y = x == y
_ == _ = False
export covering
Eq q => Eq (DScopeTermN s q d n) where
DUsed s == DUsed t = s == t
DUnused s == DUnused t = s == t
DUsed _ == DUnused _ = False
DUnused _ == DUsed _ = False
(forall n. Eq (f n)) => Eq (Scoped s f n) where
S _ x == S _ y = x == y
export covering
PrettyHL q => Show (Term q d n) where

18
tests/Tests/Equal.idr
View file

@ -141,10 +141,10 @@ tests = "equality & subtyping" :- [
equalT empty (Arr One (FT "A") $ Arr One (FT "A") (FT "A"))
(["x", "y"] :\\ BVT 1)
(["x", "y"] :\\ BVT 0),
testEq "λ x ⇒ [a] = λ x ⇒ [a] (TUsed vs TUnused)" $
testEq "λ x ⇒ [a] = λ x ⇒ [a] (Y vs N)" $
equalT empty (Arr Zero (FT "B") (FT "A"))
(Lam "x" $ TUsed $ FT "a")
(Lam "x" $ TUnused $ FT "a"),
(Lam $ S ["x"] $ Y $ FT "a")
(Lam $ S ["x"] $ N $ FT "a"),
testEq "λ x ⇒ [f [x]] = [f] (η)" $
equalT empty (Arr One (FT "A") (FT "A"))
(["x"] :\\ E (F "f" :@ BVT 0))
@ -164,7 +164,7 @@ tests = "equality & subtyping" :- [
"equalities and uip" :-
let refl : Term q d n -> Term q d n -> Elim q d n
refl a x = (DLam "_" $ DUnused x) :# (Eq0 a x x)
refl a x = (DLam $ S ["_"] $ N x) :# (Eq0 a x x)
in
[
note #""refl [A] x" is an abbreviation for "(λᴰi ⇒ x) ∷ (x ≡ x : A)""#,
@ -208,7 +208,7 @@ tests = "equality & subtyping" :- [
{globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
let ty : forall n. Term Three 0 n
:= Sig "_" (FT "E") $ TUnused $ FT "E" in
:= Sig (FT "E") $ S ["_"] $ N $ FT "E" in
equalE (MkTyContext new [< ty, ty]) (BV 0) (BV 1),
testEq "E ≔ a ≡ a' : A, F ≔ E × E ∥ x : F, y : F ⊢ x = y"
@ -235,11 +235,11 @@ tests = "equality & subtyping" :- [
equalT empty (FT "A")
(CloT (BVT 1) (F "a" ::: F "b" ::: id))
(FT "b"),
testEq "(λy. [#1]){a} = λy. [a] : B ⇾ A (TUnused)" $
testEq "(λy. [#1]){a} = λy. [a] : B ⇾ A (N)" $
equalT empty (Arr Zero (FT "B") (FT "A"))
(CloT (Lam "y" $ TUnused $ BVT 0) (F "a" ::: id))
(Lam "y" $ TUnused $ FT "a"),
testEq "(λy. [#1]){a} = λy. [a] : B ⇾ A (TUsed)" $
(CloT (Lam $ S ["y"] $ N $ BVT 0) (F "a" ::: id))
(Lam $ S ["y"] $ N $ FT "a"),
testEq "(λy. [#1]){a} = λy. [a] : B ⇾ A (Y)" $
equalT empty (Arr Zero (FT "B") (FT "A"))
(CloT (["y"] :\\ BVT 1) (F "a" ::: id))
(["y"] :\\ FT "a")

115
tests/Tests/Reduce.idr
View file

@ -4,124 +4,113 @@ import Quox.Syntax as Lib
import Quox.Syntax.Qty.Three
import Quox.Equal
import TermImpls
import TypingImpls
import TAP
testWhnf : Eq b => Show b => (a -> (Subset b _)) -> String -> a -> b -> Test
testWhnf whnf label from to = test "\{label} (whnf)" $ do
let result = fst (whnf from)
unless (result == to) $
Left [("exp", to), ("got", result)] {a = List (String, b)}
parameters {0 isRedex : RedexTest tm} {auto _ : Whnf tm isRedex err}
{auto _ : ToInfo err}
{auto _ : forall d, n. Eq (tm Three d n)}
{auto _ : forall d, n. Show (tm Three d n)}
{default empty defs : Definitions Three}
{default 0 d, n : Nat}
testWhnf : String -> tm Three d n -> tm Three d n -> Test
testWhnf label from to = test "\{label} (whnf)" $ do
result <- bimap toInfo fst $ whnf defs from
unless (result == to) $ Left [("exp", show to), ("got", show result)]
testNoStep : Eq a => Show a => (a -> (Subset a _)) -> String -> a -> Test
testNoStep whnf label e = test "\{label} (no step)" $ do
let result = fst (whnf e)
unless (result == e) $ Left [("reduced", result)] {a = List (String, a)}
parameters {default empty defs : Definitions Three} {default 0 d, n : Nat}
testWhnfT : String -> Term Three d n -> Term Three d n -> Test
testWhnfT = testWhnf (whnf defs)
testWhnfE : String -> Elim Three d n -> Elim Three d n -> Test
testWhnfE = testWhnf (whnf defs)
testNoStepE : String -> Elim Three d n -> Test
testNoStepE = testNoStep (whnf defs)
testNoStepT : String -> Term Three d n -> Test
testNoStepT = testNoStep (whnf defs)
testNoStep : String -> tm Three d n -> Test
testNoStep label e = testWhnf label e e
tests = "whnf" :- [
"head constructors" :- [
testNoStepT "★₀" $ TYPE 0,
testNoStepT "[A] ⊸ [B]" $
testNoStep "★₀" $ TYPE 0,
testNoStep "[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]]" $
testNoStep "(x: [A]) ⊸ [B [x]]" $
Pi One (FT "A") (S ["x"] $ Y $ E $ F "B" :@ BVT 0),
testNoStep "λx. [x]" $
Lam $ S ["x"] $ Y $ BVT 0,
testNoStep "[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
testNoStep "x" {n = 1} $ BV 0,
testNoStep "a" $ F "a",
testNoStep "f [a]" $ F "f" :@ FT "a",
testNoStep "★₀ ∷ ★₁" $ TYPE 0 :# TYPE 1
],
"redexes" :- [
testWhnfE "[a] ∷ [A]"
testWhnf "[a] ∷ [A]"
(FT "a" :# FT "A")
(F "a"),
testWhnfT "[★₁ ∷ ★₃]"
testWhnf "[★₁ ∷ ★₃]"
(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")
testWhnf "(λx. [x] ∷ [A] ⊸ [A]) [a]"
(((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
(F "a")
],
"definitions" :- [
testWhnfE "a (transparent)"
testWhnf "a (transparent)"
{defs = fromList [("a", mkDef Zero (TYPE 1) (TYPE 0))]}
(F "a") (TYPE 0 :# TYPE 1)
],
"elim closure" :- [
testWhnfE "x{}" {n = 1}
testWhnf "x{}" {n = 1}
(CloE (BV 0) id)
(BV 0),
testWhnfE "x{a/x}"
testWhnf "x{a/x}"
(CloE (BV 0) (F "a" ::: id))
(F "a"),
testWhnfE "x{x/x,a/y}" {n = 1}
testWhnf "x{x/x,a/y}" {n = 1}
(CloE (BV 0) (BV 0 ::: F "a" ::: id))
(BV 0),
testWhnfE "x{(y{a/y})/x}"
testWhnf "x{(y{a/y})/x}"
(CloE (BV 0) ((CloE (BV 0) (F "a" ::: id)) ::: id))
(F "a"),
testWhnfE "(x y){f/x,a/y}"
testWhnf "(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}
testWhnf "([y] ∷ [x]){A/x}" {n = 1}
(CloE (BVT 1 :# BVT 0) (F "A" ::: id))
(BV 0),
testWhnfE "([y] ∷ [x]){A/x,a/y}"
testWhnf "([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 "y" $ TUnused $ BVT 0) (F "a" ::: id))
(Lam "y" $ TUnused $ FT "a"),
testWhnfT "(λy. y){a/x}"
(CloT (Lam "y" $ TUsed $ BVT 0) (F "a" ::: id))
(Lam "y" $ TUsed $ BVT 0)
testWhnf "(λy. x){a/x}"
(CloT (Lam $ S ["y"] $ N $ BVT 0) (F "a" ::: id))
(Lam $ S ["y"] $ N $ FT "a"),
testWhnf "(λy. y){a/x}"
(CloT (["y"] :\\ BVT 0) (F "a" ::: id))
(["y"] :\\ BVT 0)
],
"looking inside […]" :- [
testWhnfT "[(λx. x ∷ A ⊸ A) [a]]"
(E $ (Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
testWhnf "[(λx. x ∷ A ⊸ A) [a]]"
(E $ ((["x"] :\\ 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]]" $
testNoStep "λy. [(λx. [x] ∷ [A] ⊸ [A]) [y]]" $
["y"] :\\ E (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ BVT 0),
testNoStep "f [(λx. [x] ∷ [A] ⊸ [A]) [a]]" $
F "a" :@
E ((Lam "x" (TUsed $ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a"),
testNoStepT "λx. [y [x]]{x/x,a/y}" {n = 1} $
Lam "x" $ TUsed $ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id),
testNoStepE "f ([y [x]]{x/x,a/y})" {n = 1} $
E (((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a"),
testNoStep "λx. [y [x]]{x/x,a/y}" {n = 1} $
["x"] :\\ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id),
testNoStep "f ([y [x]]{x/x,a/y})" {n = 1} $
F "f" :@ CloT (E $ BV 1 :@ BVT 0) (BV 0 ::: F "a" ::: id)
]
]

48
tests/Tests/Typechecker.idr
View file

@ -36,8 +36,8 @@ inj act = do
reflTy : IsQty q => Term q d n
reflTy =
Pi zero "A" (TYPE 0) $ TUsed $
Pi one "x" (BVT 0) $ TUsed $
Pi zero (TYPE 0) $ S ["A"] $ Y $
Pi one (BVT 0) $ S ["x"] $ Y $
Eq0 (BVT 1) (BVT 0) (BVT 0)
reflDef : IsQty q => Term q d n
@ -56,8 +56,8 @@ defGlobals = fromList
("f", mkAbstract Any $ Arr One (FT "A") (FT "A")),
("g", mkAbstract Any $ Arr One (FT "A") (FT "B")),
("f2", mkAbstract Any $ Arr One (FT "A") $ Arr One (FT "A") (FT "A")),
("p", mkAbstract Any $ Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0),
("q", mkAbstract Any $ Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0),
("p", mkAbstract Any $ Pi One (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0),
("q", mkAbstract Any $ Pi One (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0),
("refl", mkDef Any reflTy reflDef)]
parameters (label : String) (act : Lazy (M ()))
@ -139,7 +139,7 @@ tests = "typechecker" :- [
check_ (ctx [<]) szero (Arr One (FT "C") (FT "D")) (TYPE 0),
testTC "0 · (1·x : A) → P x ⇐ ★₀" $
check_ (ctx [<]) szero
(Pi One "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0)
(Pi One (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0)
(TYPE 0),
testTCFail "0 · A ⊸ P ⇍ ★₀" $
check_ (ctx [<]) szero (Arr One (FT "A") $ FT "P") (TYPE 0),
@ -207,21 +207,20 @@ tests = "typechecker" :- [
"equalities" :- [
testTC "1 · (λᴰ i ⇒ a) ⇐ a ≡ a" $
check_ (ctx [<]) sone (DLam "i" $ DUnused $ FT "a")
check_ (ctx [<]) sone (DLam $ S ["i"] $ N $ FT "a")
(Eq0 (FT "A") (FT "a") (FT "a")),
testTC "0 · (λ p q ⇒ λᴰ i ⇒ p) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ (ctx [<]) szero
(Lam "p" $ TUsed $ Lam "q" $ TUnused $
DLam "i" $ DUnused $ BVT 0)
(Pi Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
Pi Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
(Lam $ S ["p"] $ Y $ Lam $ S ["q"] $ N $ DLam $ S ["i"] $ N $ BVT 0)
(Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["p"] $ Y $
Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["q"] $ Y $
Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0)),
testTC "0 · (λ p q ⇒ λᴰ i ⇒ q) ⇐ (ω·p q : a ≡ a') → p ≡ q" $
check_ (ctx [<]) szero
(Lam "p" $ TUnused $ Lam "q" $ TUsed $
DLam "i" $ DUnused $ BVT 0)
(Pi Any "p" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
Pi Any "q" (Eq0 (FT "A") (FT "a") (FT "a")) $ TUsed $
(Lam $ S ["p"] $ N $ Lam $ S ["q"] $ Y $
DLam $ S ["i"] $ N $ BVT 0)
(Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["p"] $ Y $
Pi Any (Eq0 (FT "A") (FT "a") (FT "a")) $ S ["q"] $ Y $
Eq0 (Eq0 (FT "A") (FT "a") (FT "a")) (BVT 1) (BVT 0))
],
@ -233,11 +232,11 @@ tests = "typechecker" :- [
testTC "cong" $
check_ (ctx [<]) sone
(["x", "y", "xy"] :\\ ["i"] :\\% E (F "p" :@ E (BV 0 :% BV 0)))
(Pi Zero "x" (FT "A") $ TUsed $
Pi Zero "y" (FT "A") $ TUsed $
Pi One "xy" (Eq0 (FT "A") (BVT 1) (BVT 0)) $ TUsed $
Eq "i" (DUsed $ E $ F "P" :@ E (BV 0 :% BV 0))
(E $ F "p" :@ BVT 2) (E $ F "p" :@ BVT 1)),
(Pi Zero (FT "A") $ S ["x"] $ Y $
Pi Zero (FT "A") $ S ["y"] $ Y $
Pi One (Eq0 (FT "A") (BVT 1) (BVT 0)) $ S ["xy"] $ Y $
Eq (S ["i"] $ Y $ E $ F "P" :@ E (BV 0 :% BV 0))
(E $ F "p" :@ BVT 2) (E $ F "p" :@ BVT 1)),
note "0·A : Type, 0·P : ω·A → Type,",
note "ω·p q : (1·x : A) → P x",
note "⊢",
@ -246,11 +245,12 @@ tests = "typechecker" :- [
testTC "funext" $
check_ (ctx [<]) sone
(["eq"] :\\ ["i"] :\\% ["x"] :\\ E (BV 1 :@ BVT 0 :% BV 0))
(Pi One "eq"
(Pi One "x" (FT "A") $ TUsed $
(Pi One
(Pi One (FT "A") $ S ["x"] $ Y $
Eq0 (E $ F "P" :@ BVT 0)
(E $ F "p" :@ BVT 0) (E $ F "q" :@ BVT 0)) $ TUsed $
Eq0 (Pi Any "x" (FT "A") $ TUsed $ E $ F "P" :@ BVT 0)
(FT "p") (FT "q"))
(E $ F "p" :@ BVT 0) (E $ F "q" :@ BVT 0)) $
S ["eq"] $ Y $
Eq0 (Pi Any (FT "A") $ S ["x"] $ Y $ E $ F "P" :@ BVT 0)
(FT "p") (FT "q"))
]
]