From b89ece01704e3b8040e75687f1f8524027d7f7e8 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 1 Apr 2023 13:01:44 +0100
Subject: Define Reduction.

---
 src/Core/Reduction.idr | 47 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)
 create mode 100644 src/Core/Reduction.idr

(limited to 'src/Core')

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
-- 
cgit v1.2.3