From 7e184c20d545afb55f6e962b8bfea882b23699fa Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sun, 1 Jan 2023 12:11:50 +0000
Subject: Index normal forms with relevance.

- Remove container types.
- Replace sum types with booleans.
- Remove type annotation from absurd.
- Add original type as argument to cast.
- Make if (was case) take a lambda for the return type.
---
 src/Obs/Substitution.idr | 90 ++++++++++++++++++++++++++++++++++--------------
 1 file changed, 65 insertions(+), 25 deletions(-)

(limited to 'src/Obs/Substitution.idr')

diff --git a/src/Obs/Substitution.idr b/src/Obs/Substitution.idr
index 340afff..22a7272 100644
--- a/src/Obs/Substitution.idr
+++ b/src/Obs/Substitution.idr
@@ -1,43 +1,83 @@
 module Obs.Substitution
 
-import Data.Fin
+import public Data.List.Elem
 
 %default total
 
-public export
-interface Rename (0 x : Nat -> Type) where
-  rename : forall m, n . x n -> (Fin n -> Fin m) -> x m
+infix 5 ~|>
 
-public export
-interface Rename x => PointedRename x where
-  point : forall n . Fin n -> x n
+namespace Sorted
+  public export 0
+  Family : Type -> Type
+  Family a = a -> List a -> Type
 
-public export
-interface Subst (0 x, y, z : Nat -> Type) where
-  subst : forall m, n . x n -> (Fin n -> y m) -> z m
+  public export 0
+  Map : List a -> Family a -> List a -> Type
+  Map ctx x ctx' = {s : a} -> Elem s ctx -> x s ctx'
 
-public export
-Rename x => Subst x Fin x where
-  subst = rename
+  public export 0
+  Hom : Family a -> Family a -> Family a
+  Hom x y s ctx = forall ctx' . Map ctx x ctx' -> y s ctx'
+
+  public export 0
+  (~|>) : Family a -> Family a -> Type
+  x ~|> y = forall ctx . {s : a} -> x s ctx -> y s ctx
+
+  public export
+  interface Rename (0 a : _) (0 x : Family a) | x where
+    rename : x ~|> Hom Elem x
+
+  public export
+  interface Rename a x => PointedRename a (0 b : a -> Type) x | x where
+    point : forall ctx . {s : a} -> b s -> Elem s ctx -> x s ctx
+
+namespace Unsorted
+  public export 0
+  Family : Type -> Type
+  Family a = List a -> Type
+
+  public export 0
+  Hom : Sorted.Family a -> Unsorted.Family a -> Unsorted.Family a
+  Hom x y ctx = forall ctx' . Map ctx x ctx' -> y ctx'
+
+  public export 0
+  (~|>) : Unsorted.Family a -> Unsorted.Family a -> Type
+  x ~|> y = forall ctx . x ctx -> y ctx
+
+  public export
+  interface Rename (0 a : _) (0 x : Unsorted.Family a) | x where
+    rename : x ~|> Hom Elem x
 
 public export
-Rename Fin where
+Sorted.Rename a Elem where
   rename i f = f i
 
 public export
-PointedRename Fin where
-  point = id
+PointedRename a (const ()) Elem where
+  point _ = id
 
 public export
-add : (0 x : _) -> x n -> (Fin m -> x n) -> Fin (S m) -> x n
-add x v f FZ     = v
-add x v f (FS i) = f i
+add : (0 x : Sorted.Family a) -> x s' ctx' -> Map ctx x ctx' -> Map (s' :: ctx) x ctx'
+add x v f Here      = v
+add x v f (There i) = f i
 
 public export
-lift : PointedRename x => (k : _) -> (Fin m -> x n) -> Fin (k + m) -> x (k + n)
-lift 0     f = f
-lift (S k) f = add x (point FZ) (\i => rename (lift k f i) FS)
+lift : PointedRename a b x => (ctx : List (s ** b s))
+  -> Map ctx' x ctx''
+  -> Map (map DPair.fst ctx ++ ctx') x (map DPair.fst ctx ++ ctx'')
+lift [] f = f
+lift ((s ** y) :: ctx) f = add x (point y Here) (\i => rename (lift ctx f i) There)
 
-public export
-weaken : Rename x => (m : _) -> x n -> x (m + n)
-weaken m t = rename t (shift m)
+elemAppRight : (xs : List a) -> (0 ys : List a) -> Elem x ys -> Elem.Elem x (xs ++ ys)
+elemAppRight [] _ = id
+elemAppRight (x :: xs) ys = There . elemAppRight xs ys
+
+namespace Sorted
+  export
+  weaken : Sorted.Rename a x => (ctx : _) -> x ~|> (\s, ctx' => x s (ctx ++ ctx'))
+  weaken ctx t = rename t (elemAppRight ctx _)
+
+namespace Unsorted
+  export
+  weaken : Unsorted.Rename a x => (ctx : _) -> x ~|> (\ctx' => x (ctx ++ ctx'))
+  weaken ctx t = rename t (elemAppRight ctx _)
-- 
cgit v1.2.3