module Quox.OPE.Split

import Quox.OPE.Basics
import Quox.OPE.Length
import Quox.OPE.Sub

%default total


public export
record Split {a : Type} (xs, ys, zs : Scope a) (p : xs `Sub` ys ++ zs) where
  constructor MkSplit
  {0 leftSub, rightSub : Scope a}
  leftThin : leftSub `Sub` ys
  rightThin : rightSub `Sub` zs
  0 eqScope : xs = leftSub ++ rightSub
  0 eqThin : p ~=~ leftThin ++ rightThin

export
split : (zs : Scope a) -> (p : xs `Sub` ys ++ zs) -> Split xs ys zs p
split [<] p = MkSplit p zero Refl Refl
split (zs :< z) (Keep p) with (split zs p)
  split (zs :< z) (Keep (l ++ r)) | MkSplit l r Refl Refl =
    MkSplit l (Keep r) Refl Refl
split (zs :< z) (Drop p) {xs} with (split zs p)
  split (zs :< z) (Drop (l ++ r)) {xs = _} | MkSplit l r Refl Refl =
    MkSplit l (Drop r) Refl Refl