diff options
Diffstat (limited to 'src/Core/Reduction.idr')
| -rw-r--r-- | src/Core/Reduction.idr | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr index 7516648..9015d14 100644 --- a/src/Core/Reduction.idr +++ b/src/Core/Reduction.idr @@ -3,6 +3,7 @@ module Core.Reduction import Core.Environment import Core.Declarative import Core.Term +import Core.Term.NormalForm import Core.Term.Substitution import Core.Term.Thinned import Core.Thinning @@ -131,3 +132,25 @@ termStepImpliesSubjectWf (ConvStep step tyConv) = ConvWf (termStepImpliesSubject export typeStepImpliesSubjectWf : TypeStep env a b -> TypeWf env a typeStepImpliesSubjectWf = LiftWf . termStepImpliesSubjectWf + +-- Whnfs Do Not Reduce --------------------------------------------------------- + +export +whnfNoTermStep : Whnf t -> Not (TermStep env t u a) +whnfNoTermStep (Ntrl (App n)) (AppStep step tmWf) = whnfNoTermStep (Ntrl n) step +whnfNoTermStep (Ntrl (App n)) (PiBeta tyWf tmWf tmWf1) impossible +whnfNoTermStep n (ConvStep step tyConv) = whnfNoTermStep n step + +export +whnfNoTypeStep : Whnf a -> Not (TypeStep env a b) +whnfNoTypeStep = whnfNoTermStep + +export +whnfTypeRedStays : Whnf a -> TypeReduce env a b -> a = b +whnfTypeRedStays n (Refl tyWf) = Refl +whnfTypeRedStays n (Step step steps) = absurd (whnfNoTypeStep n step) + +export +whnfTermRedStays : Whnf t -> TermReduce env t u a -> t = u +whnfTermRedStays n (Refl tmWf) = Refl +whnfTermRedStays n (Step step steps) = absurd (whnfNoTermStep n step) |