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 : Length ys =>
        (zs : Scope a) -> (p : xs `Sub` ys ++ zs) -> Split xs ys zs p
split [<] p = MkSplit p zero Refl (endRight p)
split (zs :< z) p @{ys} with (p.view @{S (lengthApp ys %search)})
  split (zs :< z) (SubM (S (2 * n)) (Keep p) v0) | (KEEP v Refl) =
    case split zs (sub v) of
      MkSplit l r Refl t =>
        MkSplit l (keep r) Refl $
          rewrite viewIrrel v0 (KEEP v Refl) in
          trans (cong keep {a = sub v} t) $
          sym $ keepAppRight l r
  split (zs :< z) (SubM (2 * n) (Drop p) v0) | (DROP v Refl) =
    case split zs (sub v) of
      MkSplit l r Refl t =>
        MkSplit l (drop r) Refl $
          rewrite viewIrrel v0 (DROP v Refl) in
          trans (cong drop {a = sub v} t) $
          sym $ dropAppRight l r