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

add pushSubsts' to just have the term without proof

Browse source
This commit is contained in:
rhiannon morris 2021-12-23 19:03:04 +01:00
parent 568dba6f0b
commit b5cfc7b23b
1 changed files with 35 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -305,47 +305,57 @@ ncloE e = Element e %search
mutual mutual
||| if the input term has any top-level closures, push them under one layer of ||| if the input term has any top-level closures, push them under one layer of
||| syntax ||| syntax
export export %inline
pushSubstsT : Term d n -> NotCloTerm d n pushSubstsT : Term d n -> NotCloTerm d n
pushSubstsT s = pushSubstsT' id id s pushSubstsT s = pushSubstsTWith id id s
||| if the input elimination has any top-level closures, push them under one ||| if the input elimination has any top-level closures, push them under one
||| layer of syntax ||| layer of syntax
export export %inline
pushSubstsE : Elim d n -> NotCloElim d n pushSubstsE : Elim d n -> NotCloElim d n
pushSubstsE e = pushSubstsE' id id e pushSubstsE e = pushSubstsEWith id id e
private private
pushSubstsT' : DSubst dfrom dto -> TSubst dto from to -> pushSubstsTWith : DSubst dfrom dto -> TSubst dto from to ->
Term dfrom from -> NotCloTerm dto to Term dfrom from -> NotCloTerm dto to
pushSubstsT' th ph (TYPE l) = pushSubstsTWith th ph (TYPE l) =
ncloT $ TYPE l ncloT $ TYPE l
pushSubstsT' th ph (Pi qty qtm x a b) = pushSubstsTWith th ph (Pi qty qtm x a b) =
ncloT $ Pi qty qtm x (subs a th ph) (subs b th (push ph)) ncloT $ Pi qty qtm x (subs a th ph) (subs b th (push ph))
pushSubstsT' th ph (Lam x t) = pushSubstsTWith th ph (Lam x t) =
ncloT $ Lam x $ subs t th $ push ph ncloT $ Lam x $ subs t th $ push ph
pushSubstsT' th ph (E e) = pushSubstsTWith th ph (E e) =
let Element e _ = pushSubstsE' th ph e in ncloT $ E e let Element e _ = pushSubstsEWith th ph e in ncloT $ E e
pushSubstsT' th ph (CloT s ps) = pushSubstsTWith th ph (CloT s ps) =
pushSubstsT' th (comp' th ps ph) s pushSubstsTWith th (comp' th ps ph) s
pushSubstsT' th ph (DCloT s ps) = pushSubstsTWith th ph (DCloT s ps) =
pushSubstsT' (ps . th) ph s pushSubstsTWith (ps . th) ph s
private private
pushSubstsE' : DSubst dfrom dto -> TSubst dto from to -> pushSubstsEWith : DSubst dfrom dto -> TSubst dto from to ->
Elim dfrom from -> NotCloElim dto to Elim dfrom from -> NotCloElim dto to
pushSubstsE' th ph (F x) = pushSubstsEWith th ph (F x) =
ncloE $ F x ncloE $ F x
pushSubstsE' th ph (B i) = pushSubstsEWith th ph (B i) =
assert_total pushSubstsE $ ph !! i assert_total pushSubstsE $ ph !! i
pushSubstsE' 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
pushSubstsE' th ph (s :# a) = pushSubstsEWith th ph (s :# a) =
ncloE $ subs s th ph :# subs a th ph ncloE $ subs s th ph :# subs a th ph
pushSubstsE' th ph (CloE e ps) = pushSubstsEWith th ph (CloE e ps) =
pushSubstsE' th (comp' th ps ph) e pushSubstsEWith th (comp' th ps ph) e
pushSubstsE' th ph (DCloE e ps) = pushSubstsEWith th ph (DCloE e ps) =
pushSubstsE' (ps . th) ph e pushSubstsEWith (ps . th) ph e
public export %inline
pushSubstsT' : Term d n -> Term d n
pushSubstsT' s = (pushSubstsT s).fst
public export %inline
pushSubstsE' : Elim d n -> Elim d n
pushSubstsE' e = (pushSubstsE e).fst
parameters {auto _ : Alternative f} parameters {auto _ : Alternative f}