||| "order preserving embeddings", for recording a correspondence between
||| a smaller scope and part of a larger one.
module Quox.OPE

import Quox.NatExtra
import Data.Nat

%default total


public export
data OPE : Nat -> Nat -> Type where
  Id   : OPE n n
  Drop : OPE m n -> OPE m     (S n)
  Keep : OPE m n -> OPE (S m) (S n)
%name OPE p, q

public export %inline Injective Drop where injective Refl = Refl
public export %inline Injective Keep where injective Refl = Refl

public export
opeZero : {n : Nat} -> OPE 0 n
opeZero {n = 0}   = Id
opeZero {n = S n} = Drop opeZero

public export
(.) : OPE m n -> OPE n p -> OPE m p
p      . Id     = p
Id     . q      = q
p      . Drop q = Drop $ p . q
Drop p . Keep q = Drop $ p . q
Keep p . Keep q = Keep $ p . q

public export
toLTE : {m : Nat} -> OPE m n -> m `LTE` n
toLTE Id       = reflexive
toLTE (Drop p) = lteSuccRight $ toLTE p
toLTE (Keep p) = LTESucc      $ toLTE p


public export
keepN : (n : Nat) -> OPE a b -> OPE (n + a) (n + b)
keepN 0     p = p
keepN (S n) p = Keep $ keepN n p

public export
dropInner' : LTE' m n -> OPE m n
dropInner' LTERefl      = Id
dropInner' (LTESuccR p) = Drop $ dropInner' $ force p

public export
dropInner : {n : Nat} -> LTE m n -> OPE m n
dropInner = dropInner' . fromLTE

public export
dropInnerN : (m : Nat) -> OPE n (m + n)
dropInnerN 0     = Id
dropInnerN (S m) = Drop $ dropInnerN m


public export
interface Tighten t where
  tighten : OPE m n -> t n -> Maybe (t m)

parameters {auto _ : Tighten t}
  export %inline
  tightenInner : {n : Nat} -> m `LTE` n -> t n -> Maybe (t m)
  tightenInner = tighten . dropInner

  export %inline
  tightenN : (m : Nat) -> t (m + n) -> Maybe (t n)
  tightenN m = tighten $ dropInnerN m

  export %inline
  tighten1 : t (S n) -> Maybe (t n)
  tighten1 = tightenN 1