Define traversal kits.

4 files changed, 95 insertions, 5 deletions

diff --git a/inky.ipkg b/inky.ipkg
index 5225ed9..5fc47ba 100644
--- a/inky.ipkg
+++ b/inky.ipkg
@@ -6,3 +6,5 @@ options = "--total"
 
 modules
   = Inky.Binding
+  , Inky.Erased
+  , Inky.Kit
diff --git a/src/Inky/Binding.idr b/src/Inky/Binding.idr
index 7562f27..4d8260a 100644
--- a/src/Inky/Binding.idr
+++ b/src/Inky/Binding.idr
@@ -71,16 +71,16 @@ BS = S
 -- Binders to names ------------------------------------------------------------
 
 export
-name : forall w. (b : Binder) -> Name (w :< b)
-name b = Element b ((snocSem w b b).rightToLeft (Left Refl))
+nameOf : forall w. (b : Binder) -> Name (w :< b)
+nameOf b = Element b ((snocSem w b b).rightToLeft (Left Refl))
 
 export
 binder : Name w -> Binder
 binder = fst
 
 export
-binderName : binder {w = w :< b} (name {w} b) = b
-binderName = Refl
+binderNameOf : binder {w = w :< b} (nameOf {w} b) = b
+binderNameOf = Refl
 
 -- Empty world -----------------------------------------------------------------
 
@@ -115,6 +115,10 @@ strip (Element n member) =
             id $
             (snocSem w b n).leftToRight member))
 
+public export
+stripWith : {b : Binder} -> Lazy a -> Lazy (Name w -> a) -> Name (w :< b) -> a
+stripWith x f = maybe x f . strip
+
 -- Freshness -------------------------------------------------------------------
 
 export
@@ -135,7 +139,7 @@ soRecomputable : (0 s : So b) -> So b
 soRecomputable Oh = Oh
 
 export
-sucFresh : b `FreshIn` w -> S b `FreshIn` w :< b
+sucFresh : b `FreshIn` w -> BS b `FreshIn` w :< b
 sucFresh prf = soRecomputable (snocLength w b prf)
 
 -- World inclusion -------------------------------------------------------------
diff --git a/src/Inky/Erased.idr b/src/Inky/Erased.idr
new file mode 100644
index 0000000..05bb29e
--- /dev/null
+++ b/src/Inky/Erased.idr
@@ -0,0 +1,6 @@
+module Inky.Erased
+
+public export
+record Erased (t : Type) where
+  constructor Forget
+  0 val : t
diff --git a/src/Inky/Kit.idr b/src/Inky/Kit.idr
new file mode 100644
index 0000000..d7dc286
--- /dev/null
+++ b/src/Inky/Kit.idr
@@ -0,0 +1,78 @@
+module Inky.Kit
+
+import Control.Monad.Identity
+import Inky.Binding
+import Inky.Erased
+
+public export
+record TrKit (env : World -> World -> Type) (res : World -> Type) where
+  constructor MkTrKit
+  name : forall w, v. env w v -> Name w -> res v
+  binder : forall w, v. env w v -> Binder -> Binder
+  extend : forall w, v. (b : Binder) -> (e : env w v) -> env (w :< b) (v :< binder e b)
+
+export
+map : (forall w. res1 w -> res2 w) -> TrKit env res1 -> TrKit env res2
+map f kit = MkTrKit
+  { name = f .: kit.name
+  , binder = kit.binder
+  , extend = kit.extend
+  }
+
+export
+pure : Applicative m => TrKit env res -> TrKit env (m . res)
+pure = map pure
+
+export
+Coerce : TrKit (Erased .: (<=)) Name
+Coerce = MkTrKit (\e => coerce e.val) (const id) (\b, e => Forget (snocMono b e.val))
+
+public export
+record Supply (w : World) where
+  constructor MkSupply
+  seed : Binder
+  fresh : seed `FreshIn` w
+
+public export
+record SubstEnv (res : World -> Type) (w, v : World) where
+  constructor MkEnv
+  name : Name w -> res v
+  supply : Supply v
+
+export
+substKitE :
+  Monad m =>
+  (var : forall w. Name w -> m (res w)) ->
+  (coerce : forall w, v. (0 _ : w <= v) -> res w -> m (res v)) ->
+  TrKit (SubstEnv (m . res)) (m . res)
+substKitE var coerce = MkTrKit
+  { name = \e, n => e.name n
+  , binder = \e, _ => e.supply.seed
+  , extend = \b, e => MkEnv
+    { name =
+      stripWith
+        (var (nameOf e.supply.seed))
+        (\n => do
+          n <- e.name n
+          coerce (freshLte e.supply.fresh) n)
+    , supply = MkSupply
+      { seed = BS e.supply.seed
+      , fresh = sucFresh e.supply.fresh
+      }
+    }
+  }
+
+public export
+interface Traverse (0 t : World -> Type) where
+  var : Name w -> t w
+
+  traverseE : Applicative m => TrKit env (m . t) -> env w v -> t w -> m (t v)
+
+  renameE : Applicative m => TrKit env (m . Name) -> env w v -> t w -> m (t v)
+  renameE kit = traverseE (Kit.map (Prelude.map var) kit)
+
+  traverse : TrKit env t -> env w v -> t w -> t v
+  traverse kit e t = (traverseE (Kit.pure kit) e t).runIdentity
+
+  rename : TrKit env Name -> env w v -> t w -> t v
+  rename kit e t = (renameE (Kit.pure kit) e t).runIdentity