diff options
| -rw-r--r-- | src/Core/Reduction.idr | 61 |
1 files changed, 56 insertions, 5 deletions
diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr index 9e1d318..50926bc 100644 --- a/src/Core/Reduction.idr +++ b/src/Core/Reduction.idr @@ -1,6 +1,7 @@ module Core.Reduction import Core.Environment +import Core.Environment.Extension import Core.Declarative import Core.Term import Core.Term.NormalForm @@ -18,16 +19,13 @@ data TermStep : Env n -> Term n -> Term n -> Term n -> Type where TermStep env t u (Pi a b) -> TermWf env v a -> --- - TermStep env (App t v) (App u v) (subst b $ Wkn (id _) :< pure v) + TermStep env (App t v) (App u v) (subst1 b v) PiBeta : TypeWf env a -> TermWf (env :< pure a) t b -> TermWf env u a -> --- - TermStep env - (App (Abs t) u) - (subst t $ Wkn (id _) :< pure u) - (subst b $ Wkn (id _) :< pure u) + TermStep env (App (Abs t) u) (subst1 t u) (subst1 b u) ConvStep : TermStep env t u a -> TypeConv env a b -> @@ -187,3 +185,56 @@ termRedDeterministic (Refl _) steps2 n m = whnfTermRedStays n steps2 termRedDeterministic steps1 (Refl _) n m = sym $ whnfTermRedStays m steps1 termRedDeterministic (Step step1 steps1) (Step step2 steps2) n m = termRedDeterministic steps1 (rewrite termStepDeterministic step1 step2 in steps2) n m + +-- Weakening ------------------------------------------------------------------- + +export +weakenTermStep : + TermStep env1 t u a -> + ExtendsWf thin env2 env1 -> + TermStep env2 (wkn t thin) (wkn u thin) (wkn a thin) +weakenTermStep (AppStep {b, v} step tmWf) extWf = + rewrite wknSubst1 b v thin in + AppStep + (weakenTermStep step extWf) + (weakenTermWf tmWf extWf) +weakenTermStep (PiBeta {a, b, t, u} tyWf tmWf tmWf1) extWf = + let tyWf = weakenTypeWf tyWf extWf in + rewrite wknSubst1 t u thin in + rewrite wknSubst1 b u thin in + PiBeta tyWf + (termWfRespEq + (weakenTermWf tmWf $ MkExtWf (Keep' extWf.ext) (extWf.wf :< tyWf)) + (Refl :< sym (wknId $ wkn a thin))) + (weakenTermWf tmWf1 extWf) +weakenTermStep (ConvStep step tyConv) extWf = + ConvStep (weakenTermStep step extWf) (weakenTypeConv tyConv extWf) + +export +weakenTypeStep : + TypeStep env1 a b -> + ExtendsWf thin env2 env1 -> + TypeStep env2 (wkn a thin) (wkn b thin) +weakenTypeStep = weakenTermStep + +export +weakenTypeRed : + TypeReduce env1 a b -> + ExtendsWf thin env2 env1 -> + TypeReduce env2 (wkn a thin) (wkn b thin) +weakenTypeRed (Refl tyWf) extWf = Refl (weakenTypeWf tyWf extWf) +weakenTypeRed (Step step steps) extWf = + Step + (weakenTypeStep step extWf) + (weakenTypeRed steps extWf) + +export +weakenTermRed : + TermReduce env1 t u a -> + ExtendsWf thin env2 env1 -> + TermReduce env2 (wkn t thin) (wkn u thin) (wkn a thin) +weakenTermRed (Refl tmWf) extWf = Refl (weakenTermWf tmWf extWf) +weakenTermRed (Step step steps) extWf = + Step + (weakenTermStep step extWf) + (weakenTermRed steps extWf) |