Extract thinnings to a new module.

Also make the interface more abstract, so more efficient representations
can be swapped in with less cost.

4 files changed, 111 insertions, 52 deletions

diff --git a/obs.ipkg b/obs.ipkg
index d2454d3..9d706ae 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -12,4 +12,5 @@ main = Main
 modules
   = CC.Name
   , CC.Term
+  , CC.Thinning
   , Main
diff --git a/src/CC/Term.idr b/src/CC/Term.idr
index 2bae041..1806904 100644
--- a/src/CC/Term.idr
+++ b/src/CC/Term.idr
@@ -1,6 +1,7 @@
 module CC.Term
 
 import CC.Name
+import CC.Thinning
 
 -- Definition ------------------------------------------------------------------
 
@@ -56,3 +57,64 @@ export
 index : Env local global -> (k : Nat) -> (0 prf : IsVar k n local) -> Value global
 index (env :< (n, v)) 0 (Here eq) = v
 index (env :< _) (S k) (There prf) = index env k prf
+
+-- Weakening -------------------------------------------------------------------
+
+wknVar' :
+  forall src, tgt.
+  {0 thin : src `Thins` tgt} ->
+  (k : Nat) ->
+  (0 prf : IsVar k n src) ->
+  View thin ->
+  Nat
+wknVar' k prf (Drop thin) = S (wknVar' k prf (view thin))
+wknVar' 0 (Here eq) (Keep thin) = 0
+wknVar' (S k) (There prf) (Keep thin) = S (wknVar' k prf (view thin))
+
+wknIsVar' :
+  forall src, tgt, k.
+  {0 thin : src `Thins` tgt} ->
+  (prf : IsVar k n src) ->
+  (view : View thin) ->
+  IsVar (wknVar' k prf view) n tgt
+wknIsVar' prf (Drop thin) = There (wknIsVar' prf (view thin))
+wknIsVar' (Here eq) (Keep thin) = Here eq
+wknIsVar' (There prf) (Keep thin) = There (wknIsVar' prf (view thin))
+
+export
+wknVar : src `Thins` tgt -> {k : Nat} -> (0 prf : IsVar k n src) -> Nat
+wknVar thin {k} prf = wknVar' k prf (view thin)
+
+export
+wknIsVar :
+  (prf : IsVar k n src) ->
+  (thin : src `Thins` tgt) ->
+  IsVar (wknVar thin prf) n tgt
+wknIsVar prf thin = wknIsVar' prf (view thin)
+
+export
+wknTerm : Term src -> src `Thins` tgt -> Term tgt
+wknTerm (Var k n prf) thin = Var (wknVar thin prf) n (wknIsVar prf thin)
+wknTerm (Abs n t) thin = Abs n (wknTerm t (keep thin))
+wknTerm (App t u) thin = App (wknTerm t thin) (wknTerm u thin)
+wknTerm (Let n t u) thin = Let n (wknTerm t thin) (wknTerm u (keep thin))
+
+export
+wknNtrl : Neutral src -> src `Thins` tgt -> Neutral tgt
+export
+wknVal : Value src -> src `Thins` tgt -> Value tgt
+export
+wknClose : Closure src -> src `Thins` tgt -> Closure tgt
+export
+wknEnv : Env local src -> src `Thins` tgt -> Env local tgt
+
+wknNtrl (VVar k n prf) thin = VVar (wknVar thin prf) n (wknIsVar prf thin)
+wknNtrl (VApp n v) thin = VApp (wknNtrl n thin) (wknVal v thin)
+
+wknVal (Ntrl n) thin = Ntrl (wknNtrl n thin)
+wknVal (VAbs close) thin = VAbs (wknClose close thin)
+
+wknClose (Close n env t) thin = Close n (wknEnv env thin) t
+
+wknEnv [<] thin = [<]
+wknEnv (env :< (n, v)) thin = wknEnv env thin :< (n, wknVal v thin)
diff --git a/src/CC/Thinning.idr b/src/CC/Thinning.idr
new file mode 100644
index 0000000..284a230
--- /dev/null
+++ b/src/CC/Thinning.idr
@@ -0,0 +1,46 @@
+module CC.Thinning
+
+-- Definition ------------------------------------------------------------------
+
+export
+data Thins : (src, tgt : SnocList a) -> Type where
+  IsEmpty : [<] `Thins` [<]
+  IsDrop : src `Thins` tgt -> src `Thins` tgt :< x
+  IsKeep : src `Thins` tgt -> src :< x `Thins` tgt :< x
+
+%name Thins thin
+
+-- Operations ------------------------------------------------------------------
+
+export
+empty : [<] `Thins` [<]
+empty = IsEmpty
+
+export
+drop : src `Thins` tgt -> src `Thins` tgt :< x
+drop thin = IsDrop thin
+
+export
+keep : src `Thins` tgt -> src :< x `Thins` tgt :< x
+keep thin = IsKeep thin
+
+export
+id : {ctx : SnocList a} -> ctx `Thins` ctx
+id {ctx = [<]} = empty
+id {ctx = _ :< _} = keep id
+
+-- Views -----------------------------------------------------------------------
+
+public export
+data View : src `Thins` tgt -> Type where
+  Empty : View CC.Thinning.empty
+  Drop : (thin : src `Thins` tgt) -> View (drop thin)
+  Keep : (thin : src `Thins` tgt) -> View (keep thin)
+
+%name View view
+
+public export
+view : (thin : src `Thins` tgt) -> View thin
+view IsEmpty = Empty
+view (IsDrop thin) = Drop thin
+view (IsKeep thin) = Keep thin
diff --git a/src/Main.idr b/src/Main.idr
index 6a5fe1b..05208eb 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -2,6 +2,7 @@ module Main
 
 import CC.Name
 import CC.Term
+import CC.Thinning
 
 import Data.DPair
 import Data.List
@@ -37,57 +38,6 @@ eval env (Let n t u) = eval (env :< (n, eval env t)) u
 
 --------------------------------------------------------------------------------
 
-data Thins : (src, tgt : Context) -> Type where
-  Empty : [<] `Thins` [<]
-  Drop : src `Thins` tgt -> src `Thins` tgt :< n
-  Keep : src `Thins` tgt -> src :< n `Thins` tgt :< n
-
-%name Thins thin
-
-id : {ctx : Context} -> ctx `Thins` ctx
-id {ctx = [<]} = Empty
-id {ctx = _ :< _} = Keep id
-
-distance : src `Thins` tgt -> {k : Nat} -> (0 prf : IsVar k n src) -> Nat
-distance (Drop thin) prf = S (distance thin prf)
-distance (Keep thin) {k = 0} (Here eq) = 0
-distance (Keep thin) {k = S k} (There prf) = distance thin prf
-
-0 wknIsVar :
-  (prf : IsVar k n src) ->
-  (thin : src `Thins` tgt) ->
-  IsVar (distance thin prf + k) n tgt
-wknIsVar prf Empty impossible
-wknIsVar prf (Drop thin) = There (wknIsVar prf thin)
-wknIsVar (Here eq) (Keep thin) = Here eq
-wknIsVar (There {k} prf) (Keep thin) =
-  rewrite sym $ plusSuccRightSucc (distance thin prf) k in
-  There (wknIsVar prf thin)
-
-wknTerm : Term src -> src `Thins` tgt -> Term tgt
-wknTerm (Var k n prf) thin = Var (distance thin prf + k) n (wknIsVar prf thin)
-wknTerm (Abs n t) thin = Abs n (wknTerm t (Keep thin))
-wknTerm (App t u) thin = App (wknTerm t thin) (wknTerm u thin)
-wknTerm (Let n t u) thin = Let n (wknTerm t thin) (wknTerm u (Keep thin))
-
-wknNtrl : Neutral src -> src `Thins` tgt -> Neutral tgt
-wknVal : Value src -> src `Thins` tgt -> Value tgt
-wknClose : Closure src -> src `Thins` tgt -> Closure tgt
-wknEnv : Env local src -> src `Thins` tgt -> Env local tgt
-
-wknNtrl (VVar k n prf) thin = VVar (distance thin prf + k) n (wknIsVar prf thin)
-wknNtrl (VApp n v) thin = VApp (wknNtrl n thin) (wknVal v thin)
-
-wknVal (Ntrl n) thin = Ntrl (wknNtrl n thin)
-wknVal (VAbs close) thin = VAbs (wknClose close thin)
-
-wknClose (Close n env t) thin = Close n (wknEnv env thin) t
-
-wknEnv [<] thin = [<]
-wknEnv (env :< (n, v)) thin = wknEnv env thin :< (n, wknVal v thin)
-
---------------------------------------------------------------------------------
-
 quote : {ctx : _} -> Value ctx -> Term ctx
 quoteNtrl : {ctx : _} -> Neutral ctx -> Term ctx
 
@@ -96,7 +46,7 @@ quote (VAbs close@(Close n _ _)) =
   Abs n $
   assert_total $
   quote $
-  app (wknClose close (Drop id)) (Ntrl $ VVar 0 n $ Here $ reflexive {rel = (~~)})
+  app (wknClose close (drop id)) (Ntrl $ VVar 0 n $ Here $ reflexive {rel = (~~)})
 
 quoteNtrl (VVar k n prf) = Var k n prf
 quoteNtrl (VApp n v) = App (quoteNtrl n) (quote v)