Define term reduction.

2 files changed, 98 insertions, 0 deletions

diff --git a/src/Core/Declarative.idr b/src/Core/Declarative.idr
index 38e6ccd..1292fc9 100644
--- a/src/Core/Declarative.idr
+++ b/src/Core/Declarative.idr
@@ -8,10 +8,15 @@ import Core.Thinning
 
 -- Definition ------------------------------------------------------------------
 
+public export
 data EnvWf : Env n -> Type
+public export
 data TypeWf : Env n -> Term n -> Type
+public export
 data TypeConv : Env n -> Term n -> Term n -> Type
+public export
 data TermWf : Env n -> Term n -> Term n -> Type
+public export
 data TermConv : Env n -> Term n -> Term n -> Term n -> Type
 
 data EnvWf where
diff --git a/src/Core/Reduction.idr b/src/Core/Reduction.idr
new file mode 100644
index 0000000..40829f3
--- /dev/null
+++ b/src/Core/Reduction.idr
@@ -0,0 +1,93 @@
+module Core.Reduction
+
+import Core.Environment
+import Core.Declarative
+import Core.Term
+import Core.Term.Substitution
+import Core.Term.Thinned
+import Core.Thinning
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data TermStep : Env n -> Term n -> Term n -> Term n -> Type where
+  AppStep :
+    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)
+  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)
+  ConvStep :
+    TermStep env t u a ->
+    TypeConv env a b ->
+    ---
+    TermStep env t u b
+
+public export
+TypeStep : Env n -> Term n -> Term n -> Type
+TypeStep env a b = TermStep env a b Set
+
+public export
+data ReflTransClosure : (refl : a -> Type) -> (step : a -> a -> Type) -> a -> a -> Type where
+  Refl :
+    {0 refl : a -> Type} ->
+    refl x ->
+    ---
+    ReflTransClosure refl step x x
+  Step :
+    {0 step : a -> a -> Type} ->
+    step x y ->
+    ReflTransClosure refl step y z ->
+    ---
+    ReflTransClosure refl step x z
+
+public export
+TypeReduce : Env n -> Term n -> Term n -> Type
+TypeReduce env = ReflTransClosure (TypeWf env) (TypeStep env)
+
+public export
+TermReduce : Env n -> Term n -> Term n -> Term n -> Type
+TermReduce env t u a = ReflTransClosure (\t => TermWf env t a) (\t, u => TermStep env t u a) t u
+
+%name TermStep step
+%name ReflTransClosure steps
+
+-- Respects Environment Quotient -----------------------------------------------
+
+export
+termStepRespEq : TermStep env1 t u a -> env1 =~= env2 -> TermStep env2 t u a
+termStepRespEq (AppStep step tmWf) prf =
+  AppStep
+    (termStepRespEq step prf)
+    (termWfRespEq tmWf prf)
+termStepRespEq (PiBeta tyWf tmWf tmWf1) prf =
+  PiBeta
+    (typeWfRespEq tyWf prf)
+    (termWfRespEq tmWf $ prf :< Refl)
+    (termWfRespEq tmWf1 prf)
+termStepRespEq (ConvStep step tyConv) prf =
+  ConvStep
+    (termStepRespEq step prf)
+    (typeConvRespEq tyConv prf)
+
+export
+typeStepRespEq : TypeStep env1 a b -> env1 =~= env2 -> TypeStep env2 a b
+typeStepRespEq = termStepRespEq
+
+export
+typeRedRespEq : TypeReduce env1 a b -> env1 =~= env2 -> TypeReduce env2 a b
+typeRedRespEq (Refl tyWf) prf = Refl (typeWfRespEq tyWf prf)
+typeRedRespEq (Step step steps) prf = Step (typeStepRespEq step prf) (typeRedRespEq steps prf)
+
+export
+termRedRespEq : TermReduce env1 t u a -> env1 =~= env2 -> TermReduce env2 t u a
+termRedRespEq (Refl tmWf) prf = Refl (termWfRespEq tmWf prf)
+termRedRespEq (Step step steps) prf = Step (termStepRespEq step prf) (termRedRespEq steps prf)