module Quox.Scope

import public Quox.OPE


public export
record Sub {a : Type} (t : Scoped a) (xs : Scope a) where
  constructor Su
  {0 support : Scope a}
  term : t support
  thin : support `LTE` xs

public export
CoverS : Sub s xs -> Sub t xs -> Type
CoverS ss tt = Cover ss.thin tt.thin

export %inline
inj : Length xs => t xs -> Sub t xs
inj x = Su x id

export %inline
flat : Sub (Sub t) xs -> Sub t xs
flat (Su (Su x q) p) = Su x (p . q)

export %inline
thinSub : xs `LTE` ys -> Sub t xs -> Sub t ys
thinSub p x = flat $ Su x p

export %inline
map : (forall x. s x -> t x) -> Sub s x -> Sub t x
map f = {term $= f}

public export
data Unit : Scoped a where
  Nil : Unit [<]

export %inline
unit : Length xs => Sub Unit xs
unit = Su [] zero

public export
record Coprod {a : Type} {xs, ys, zs : Scope a}
              (p : xs `LTE` zs) (q : ys `LTE` zs) where
  constructor Cop
  {0 scope : Scope a}
  {thin : scope `LTE` zs}
  {thinP : xs `LTE` scope}
  {thinQ : ys `LTE` scope}
  compP : Comp thin thinP p
  compQ : Comp thin thinQ q
  0 cover : Cover thinP thinQ

export
coprod : (p : xs `LTE` zs) -> (q : ys `LTE` zs) -> Coprod p q
coprod End      End      = %search
coprod (Keep p) (Keep q) = let Cop {} = coprod p q in %search
coprod (Keep p) (Drop q) = let Cop {} = coprod p q in %search
coprod (Drop p) (Keep q) = let Cop {} = coprod p q in %search
coprod (Drop p) (Drop q) =
  -- idk why this one is harder to solve
  let Cop compP compQ cover = coprod p q in
  Cop (CD0 compP) (CD0 compQ) cover

public export
record Pair {a : Type} (s, t : Scoped a) (zs : Scope a) where
  constructor MkPair
  fst : Sub s zs
  snd : Sub t zs
  0 cover : CoverS fst snd

export
pair : Sub s xs -> Sub t xs -> Sub (Pair s t) xs
pair (Su x p) (Su y q) =
  let c = coprod p q in
  Su (MkPair (Su x c.thinP) (Su y c.thinQ) c.cover) c.thin


public export
data Var : a -> Scope a -> Type where
  Only : Var x [< x]

export %inline
var : (0 x : a) -> [< x] `LTE` xs => Sub (Var x) xs
var x @{p} = Su Only p


infix 0 \\\, \\
public export
data Bind : (t : Scoped a) -> (new, old : Scope a) -> Type where
  (\\\) : new' `LTE` new -> t (old ++ new') -> Bind t new old

(\\) : (new : Scope a) -> Sub t (old ++ new) -> Sub (Bind t new) old
vs \\ Su term p with (split vs p)
  vs \\ Su term (l ++ r) | MkSplit l r Refl Refl = Su (r \\\ term) l