quox/lib/Quox/OPE/Cover.idr

module Quox.OPE.Cover

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

%default total


public export
data Cover'_ : (overlap : Bool) -> xs `Sub'` zs -> ys `Sub'` zs -> Type where
  CE : Cover'_ ov End End
  CL : Cover'_ ov p q -> Cover'_ ov   (Keep p) (Drop q)
  CR : Cover'_ ov p q -> Cover'_ ov   (Drop p) (Keep q)
  C2 : Cover'_ ov p q -> Cover'_ True (Keep p) (Keep q)

parameters (p : xs `Sub'` zs) (q : ys `Sub'` zs)
  public export
  0 Cover' : Type
  Cover' = Cover'_ True p q

  public export
  0 Partition' : Type
  Partition' = Cover'_ False p q


public export
record Cover_ {a : Type} {xs, ys, zs : Scope a} (overlap : Bool)
              (p : xs `Sub` zs) (q : ys `Sub` zs) where
  constructor MkCover
  0 cover : Cover'_ overlap p.lte q.lte

parameters (p : xs `Sub` zs) (q : ys `Sub` zs)
  public export
  0 Cover : Type
  Cover = Cover_ True p q

  public export
  0 Partition : Type
  Partition = Cover_ False p q


private %inline
covCast' : {0 p, p' : xs `Sub'` zs} -> {0 q, q' : ys `Sub'` zs} ->
           (0 pe : p = p') -> (0 qe : q = q') ->
           Cover'_ overlap p' q' -> Cover'_ overlap p q
covCast' pe qe c = replace {p = id} (sym $ cong2 (Cover'_ overlap) pe qe) c


parameters {0 overlap : Bool} {0 p : xs `Sub` zs} {0 q : ys `Sub` zs}
  export %inline
  left : Cover_ overlap p q -> Cover_ overlap (keep p) (drop q)
  left (MkCover cover) = MkCover $ covCast' (keepLte p) (dropLte q) $ CL cover

  export %inline
  right : Cover_ overlap p q -> Cover_ overlap (drop p) (keep q)
  right (MkCover cover) = MkCover $ covCast' (dropLte p) (keepLte q) $ CR cover

  export %inline
  both : Cover_ overlap p q -> Cover (keep p) (keep q)
  both (MkCover cover) = MkCover $ covCast' (keepLte p) (keepLte q) $ C2 cover


export
allLeft' : (sx : Length xs) => Partition' (refl' @{sx}) (zero' @{sx})
allLeft' {sx = Z}   = CE
allLeft' {sx = S s} = CL allLeft'

export
allRight' : (sx : Length xs) => Partition' (zero' @{sx}) (refl' @{sx})
allRight' {sx = Z}   = CE
allRight' {sx = S s} = CR allRight'

export
both' : (sx : Length xs) => Cover' (refl' @{sx}) (refl' @{sx})
both' {sx = Z}   = CE
both' {sx = S s} = C2 both'


export %inline
allLeft : (sx : Length xs) => Partition (refl @{sx}) (zero @{sx})
allLeft = MkCover $ rewrite reflLte {sx} in rewrite zeroLte {sx} in allLeft'

export %inline
allRight : (sx : Length xs) => Partition (zero @{sx}) (refl @{sx})
allRight = MkCover $ rewrite reflLte {sx} in rewrite zeroLte {sx} in allRight'

export %inline
allBoth : (sx : Length xs) => Cover (refl @{sx}) (refl @{sx})
allBoth = MkCover $ rewrite reflLte {sx} in both'