module Quox.OPE.Comp

import Quox.OPE.Basics
import Quox.OPE.Length
import Quox.OPE.Sub
import Data.DPair

import Control.Function
import Data.Nat

%default total


public export
data Comp' : ys `Sub'` zs -> xs `Sub'` ys -> xs `Sub'` zs -> Type where
  CEE : Comp' End End End
  CKK : Comp' p q pq -> Comp' (Keep p) (Keep q) (Keep pq)
  CKD : Comp' p q pq -> Comp' (Keep p) (Drop q) (Drop pq)
  CD0 : Comp' p q pq -> Comp' (Drop p) q        (Drop pq)

public export
record Comp {a : Type} {xs, ys, zs : Scope a}
            (p : ys `Sub` zs) (q : xs `Sub` ys) (pq : xs `Sub` zs) where
  constructor MkComp
  0 comp : Comp' p.lte q.lte pq.lte


export
compPrf' : (p : ys `Sub'` zs) -> (q : xs `Sub'` ys) -> Comp' p q (p . q)
compPrf' End      End      = CEE
compPrf' (Keep p) (Keep q) = CKK $ compPrf' p q
compPrf' (Keep p) (Drop q) = CKD $ compPrf' p q
compPrf' (Drop p) q        = CD0 $ compPrf' p q

export
0 compOk' : Comp' p q r -> r = (p . q)
compOk' CEE     = Refl
compOk' (CKK z) = cong Keep $ compOk' z
compOk' (CKD z) = cong Drop $ compOk' z
compOk' (CD0 z) = cong Drop $ compOk' z


export %inline
compPrf : (0 sy : Length ys) => (0 sz : Length zs) =>
       (p : ys `Sub` zs) -> (q : xs `Sub` ys) ->
       Comp p q ((p . q) @{sy} @{sz})
compPrf p q = MkComp $
  replace {p = Comp' p.lte q.lte} (sym $ compLte p q) $
    compPrf' p.lte q.lte


export
compZero' : (sx : Length xs) => (sy : Length ys) =>
            (p : xs `Sub'` ys) -> Comp' p (zero' @{sx}) (zero' @{sy})
compZero' {sx = Z,   sy = Z}   End      = CEE
compZero' {sx = S _, sy = S _} (Keep p) = CKD (compZero' p)
compZero'           {sy = S _} (Drop p) = CD0 (compZero' p)

export %inline
compZero : (sx : Length xs) => (sy : Length ys) =>
           (p : xs `Sub` ys) -> Comp p (zero @{sx}) (zero @{sy})
compZero p = MkComp $
  rewrite zeroLte {sx} in
  rewrite zeroLte {sx = sy} in
  compZero' {}

export
compIdLeft' : (sy : Length ys) =>
              (p : xs `Sub'` ys) -> Comp' (refl' @{sy}) p p
compIdLeft' {sy = Z}   End      = CEE
compIdLeft' {sy = S _} (Keep p) = CKK (compIdLeft' p)
compIdLeft' {sy = S _} (Drop p) = CKD (compIdLeft' p)

export %inline
compIdLeft : (sy : Length ys) =>
             (p : xs `Sub` ys) -> Comp (refl @{sy}) p p
compIdLeft {sy} p = MkComp $
  rewrite reflLte {sx = sy} in compIdLeft' {}

export
compIdRight' : (sx : Length xs) =>
               (p : xs `Sub'` ys) -> Comp' p (refl' @{sx}) p
compIdRight' {sx = Z}   End      = CEE
compIdRight' {sx = S _} (Keep p) = CKK (compIdRight' p)
compIdRight'            (Drop p) = CD0 (compIdRight' p)

export %inline
compIdRight : (sx : Length xs) =>
              (p : xs `Sub` ys) -> Comp p (refl @{sx}) p
compIdRight {sx} p = MkComp $ rewrite reflLte {sx} in compIdRight' {}

export
0 compAssoc' : (p : ys `Sub'` zs) -> (q : xs `Sub'` ys) -> (r : ws `Sub'` xs) ->
               p . (q . r) = (p . q) . r
compAssoc' End      End      End      = Refl
compAssoc' (Keep p) (Keep q) (Keep r) = cong Keep $ compAssoc' p q r
compAssoc' (Keep p) (Keep q) (Drop r) = cong Drop $ compAssoc' p q r
compAssoc' (Keep p) (Drop q) r        = cong Drop $ compAssoc' p q r
compAssoc' (Drop p) q        r        = cong Drop $ compAssoc' p q r
compAssoc' End (Drop _) _ impossible

export %inline
0 compAssoc : (sx : Length xs) => (sy : Length ys) => (sz : Length zs) =>
              (p : ys `Sub` zs) -> (q : xs `Sub` ys) -> (r : ws `Sub` xs) ->
              comp @{sy} @{sz} p (comp @{sx} @{sy} q r) =
                comp @{sx} @{sz} (comp @{sy} @{sz} p q) r
compAssoc p q r = lteEq $
  trans (transLte {}) $
  trans (cong (p.lte .) (transLte {})) $
  sym $
  trans (transLte {}) $
  trans (cong (. r.lte) (transLte {})) $
  sym $ compAssoc' {}

public export
0 Subscope : Scope a -> Type
Subscope ys = Exists (`Sub` ys)

public export
record SubMap' {a : Type} {xs, ys, zs : Scope a}
               (p : xs `Sub'` zs) (q : ys `Sub'` zs) where
  constructor SM'
  thin : xs `Sub'` ys
  0 comp : Comp' q thin p

public export
record SubMap {a : Type} {xs, ys, zs : Scope a}
              (p : xs `Sub` zs) (q : ys `Sub` zs) where
  constructor SM
  thin : xs `Sub` ys
  0 comp : Comp q thin p

export
0 submap' : SubMap p q -> SubMap' p.lte q.lte
submap' (SM thin comp) = SM' {thin = thin.lte, comp = comp.comp}

parameters (p : xs `Sub'` ys)
  export
  subId' : SubMap' p p
  subId' = SM' refl' (compIdRight' p)

  export
  subZero' : SubMap' Sub.zero' p
  subZero' = SM' zero' (compZero' p)

parameters {auto sx : Length xs} (p : xs `Sub` ys)
  export
  subId : SubMap p p
  subId = SM refl (compIdRight p)

  export
  subZero : SubMap Sub.zero p
  subZero = SM zero (compZero p)