1 files changed, 74 insertions, 0 deletions
diff --git a/src/Data/Term.idr b/src/Data/Term.idr
new file mode 100644
index 0000000..95fd9f8
--- /dev/null
+++ b/src/Data/Term.idr
@@ -0,0 +1,74 @@
+module Data.Term
+
+import public Data.Vect
+import Data.Vect.Properties.Map
+import Syntax.PreorderReasoning
+
+%prefix_record_projections off
+
+-- Definition ------------------------------------------------------------------
+
+public export
+record Signature where
+  Operator : Nat -> Type
+
+%name Signature sig
+
+public export
+data Term : Signature -> Nat -> Type where
+  Var : Fin n -> Term sig n
+  Op : sig.Operator k -> Vect k (Term sig n) -> Term sig n
+
+%name Term t, u, v
+
+-- Substitution ----------------------------------------------------------------
+
+export
+pure : (Fin k -> Fin n) -> Fin k -> Term sig n
+pure r = Var . r
+
+export
+(<$>) : (Fin k -> Term sig n) -> Term sig k -> Term sig n
+f <$> Var i = f i
+f <$> Op op ts = Op op (map (\t => f <$> assert_smaller ts t) ts)
+
+-- Extensional Equality --------------------------------------------------------
+
+public export
+0 (.=.) : Rel (Fin k -> Term sig n)
+f .=. g = (i : Fin k) -> f i = g i
+
+-- Substitution is Monadic -----------------------------------------------------
+
+export
+(.) : (Fin k -> Term sig n) -> (Fin j -> Term sig k) -> Fin j -> Term sig n
+f . g = (f <$>) . g
+
+-- Properties
+
+export
+subUnit : (t : Term sig n) -> Var <$> t = t
+subUnit (Var i) = Refl
+subUnit (Op op ts) = cong (Op op) $ Calc $
+  |~ map (Var <$>) ts
+  ~~ map id ts        ...(mapExtensional (Var <$>) id (\t => subUnit (assert_smaller ts t)) ts)
+  ~~ ts               ...(mapId ts)
+
+export
+subAssoc :
+  (f : Fin k -> Term sig n) ->
+  (g : Fin j -> Term sig k) ->
+  (t : Term sig j) ->
+  (f . g) <$> t = f <$> g <$> t
+subAssoc f g (Var i) = Refl
+subAssoc f g (Op op ts) = cong (Op op) $ Calc $
+  |~ map ((f . g) <$>) ts
+  ~~ map ((f <$>) . (g <$>)) ts   ...(mapExtensional ((f . g) <$>) ((f <$>) . (g <$>)) (\t => subAssoc f g (assert_smaller ts t)) ts)
+  ~~ map (f <$>) (map (g <$>) ts) ..<(mapFusion (f <$>) (g <$>) ts)
+
+export
+subComp :
+  (f : Fin k -> Term sig n) ->
+  (r : Fin j -> Fin k) ->
+  f . pure r .=. f . r
+subComp f r i = Refl