diff options
| -rw-r--r-- | obs.ipkg | 1 | ||||
| -rw-r--r-- | src/Core/Reduction.idr | 47 |
2 files changed, 48 insertions, 0 deletions
@@ -10,6 +10,7 @@ modules = Core.Context , Core.Declarative , Core.Name + , Core.Reduction , Core.Term , Core.Term.Environment , Core.Term.Substitution diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr new file mode 100644 index 0000000..0b3a651 --- /dev/null +++ b/src/Core/Reduction.idr @@ -0,0 +1,47 @@ +module Core.Reduction + +import Core.Context +import Core.Declarative +import Core.Term +import Core.Term.Environment +import Core.Term.Substitution + +public export +data TermStep : Env sx -> Term sx -> Term sx -> Term sx -> Type where + PiBeta : + TypeWf env f -> + TermWf (env :< f) t g -> + TermWf env u f -> + --- + TermStep env (App (Abs n t) u) (subst t $ sub1 u) (subst g $ sub1 u) + AppStep : + TermStep env t u (Pi n f g) -> + TermWf env a f -> + --- + TermStep env (App t a) (App u a) (subst g $ sub1 a) + StepConv : + TermStep env t u a -> + TypeConv env a b -> + --- + TermStep env t u b + +public export +TypeStep : Env sx -> Term sx -> Term sx -> Type +TypeStep env a b = TermStep env a b Set + +namespace Type + public export + data TypeRed : Env sx -> Term sx -> Term sx -> Type where + Stay : TypeWf env a -> TypeRed env a a + (::) : TypeStep env a b -> TypeRed env b c -> TypeRed env a c + +namespace Term + public export + data TermRed : Env sx -> Term sx -> Term sx -> Term sx -> Type where + Stay : TermWf env t a -> TermRed env t t a + (::) : TermStep env t u a -> TermRed env u v a -> TermRed env t v a + +%name TypeStep step +%name TermStep step +%name TypeRed steps +%name TermRed steps |