diff options
| -rw-r--r-- | obs.ipkg | 1 | ||||
| -rw-r--r-- | src/Core/Reduction.idr | 23 | ||||
| -rw-r--r-- | src/Core/Term/NormalForm.idr | 22 |
3 files changed, 46 insertions, 0 deletions
@@ -11,6 +11,7 @@ modules , Core.Environment , Core.Reduction , Core.Term + , Core.Term.NormalForm , Core.Term.Substitution , Core.Term.Thinned , Core.Thinning 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) diff --git a/src/Core/Term/NormalForm.idr b/src/Core/Term/NormalForm.idr new file mode 100644 index 0000000..9984bee --- /dev/null +++ b/src/Core/Term/NormalForm.idr @@ -0,0 +1,22 @@ +module Core.Term.NormalForm + +import Core.Term + +-- Definition ------------------------------------------------------------------ + +public export +data Neutral : Term n -> Type where + Var : Neutral (Var i) + App : Neutral t -> Neutral (App t u) + +public export +data Whnf : Term n -> Type where + Ntrl : Neutral t -> Whnf t + + Set : Whnf Set + + Pi : Whnf (Pi a b) + Abs : Whnf (Abs t) + +%name Neutral n, m +%name Whnf n, m |