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

make (//) lazier

Browse source
This commit is contained in:
rhiannon morris 2021-09-09 23:54:18 +02:00
parent b29c56e0ae
commit 8c675d01d5
2 changed files with 13 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Quox/Syntax/Subst.idr
View file

@ -35,7 +35,7 @@ export Ord (f to) => Ord (Subst f from to) where compare = compare `on` repr
infixl 8 // infixl 8 //
public export public export
interface FromVar env => CanSubst env term where interface FromVar env => CanSubst env term where
(//) : term from -> Subst env from to -> term to (//) : term from -> Lazy (Subst env from to) -> term to
public export public export
CanSubst1 : (Nat -> Type) -> Type CanSubst1 : (Nat -> Type) -> Type

12
src/Quox/Syntax/Term.idr
View file

@ -189,9 +189,10 @@ export
CanSubst (Elim d) (Elim d) where CanSubst (Elim d) (Elim d) where
F x // _ = F x F x // _ = F x
B i // th = th !! i B i // th = th !! i
CloE e ph // th = CloE e $ assert_total $ ph . th CloE e ph // th = assert_total CloE e $ ph . th
e // Shift SZ = e e // th = case force th of
e // th = CloE e th Shift SZ => e
th => CloE e th
||| does the minimal reasonable work: ||| does the minimal reasonable work:
||| - deletes the closure around an atomic constant like `TYPE` ||| - deletes the closure around an atomic constant like `TYPE`
@ -204,8 +205,9 @@ CanSubst (Elim d) (Term d) where
TYPE l // _ = TYPE l TYPE l // _ = TYPE l
E e // th = E $ e // th E e // th = E $ e // th
CloT s ph // th = CloT s $ ph . th CloT s ph // th = CloT s $ ph . th
s // Shift SZ = s s // th = case force th of
s // th = CloT s th Shift SZ => s
th => CloT s th
export CanShift (Term d) where i // by = i // Shift by {env=(Elim d)} export CanShift (Term d) where i // by = i // Shift by {env=(Elim d)}
export CanShift (Elim d) where i // by = i // Shift by {env=(Elim d)} export CanShift (Elim d) where i // by = i // Shift by {env=(Elim d)}