module Obs.Substitution

import public Data.List.Elem

%default total

infix 5 ~|>

namespace Sorted
  public export 0
  Family : Type -> Type
  Family a = a -> List a -> Type

  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 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
Sorted.Rename a Elem where
  rename i f = f i

public export
PointedRename a (const ()) Elem where
  point _ = id

public export
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 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)

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 _)