module Quox.Thin.Eqv

import public Quox.Thin.Base
import public Quox.Thin.View
import Quox.NatExtra
import Syntax.PreorderReasoning

%default total

infix 6 `Eqv`

private
uip : (p, q : a = b) -> p = q
uip Refl Refl = Refl


public export
data Eqv : OPE m1 n1 mask1 -> OPE m2 n2 mask2 -> Type where
  EqvStop : Eqv Stop Stop
  EqvDrop : {0 p : OPE m1 n1 mask1} ->
            {0 q : OPE m2 n2 mask2} ->
            Eqv p q -> Eqv (Drop p eq1) (Drop q eq2)
  EqvKeep : {0 p : OPE m1 n1 mask1} ->
            {0 q : OPE m2 n2 mask2} ->
            Eqv p q -> Eqv (Keep p eq1) (Keep q eq2)
%name Eqv eqv

export Uninhabited (Stop     `Eqv` Drop p e) where uninhabited _ impossible
export Uninhabited (Stop     `Eqv` Keep p e) where uninhabited _ impossible
export Uninhabited (Drop p e `Eqv` Stop)     where uninhabited _ impossible
export Uninhabited (Drop p e `Eqv` Keep q f) where uninhabited _ impossible
export Uninhabited (Keep p e `Eqv` Stop)     where uninhabited _ impossible
export Uninhabited (Keep p e `Eqv` Drop q f) where uninhabited _ impossible

export
Reflexive (OPE m n mask) Eqv where
  reflexive {x = Stop}    = EqvStop
  reflexive {x = Drop {}} = EqvDrop reflexive
  reflexive {x = Keep {}} = EqvKeep reflexive

export
symmetric : p `Eqv` q -> q `Eqv` p
symmetric EqvStop       = EqvStop
symmetric (EqvDrop eqv) = EqvDrop $ symmetric eqv
symmetric (EqvKeep eqv) = EqvKeep $ symmetric eqv

export
transitive : p `Eqv` q -> q `Eqv` r -> p `Eqv` r
transitive EqvStop        EqvStop        = EqvStop
transitive (EqvDrop eqv1) (EqvDrop eqv2) = EqvDrop (transitive eqv1 eqv2)
transitive (EqvKeep eqv1) (EqvKeep eqv2) = EqvKeep (transitive eqv1 eqv2)


private
recompute' : {mask1, mask2, n1, n2 : Nat} ->
             (0 p : OPE m1 n1 mask1) -> (0 q : OPE m2 n2 mask2) ->
             (0 eqv : p `Eqv` q) -> p `Eqv` q
recompute' p q eqv with %syntactic (view p) | (view q)
  recompute' Stop Stop _ | StopV | StopV = EqvStop
  recompute' (Drop p _) (Drop q _) eqv | DropV _ p | DropV _ q =
    EqvDrop $ recompute' {eqv = let EqvDrop e = eqv in e, _}
  recompute' (Keep p _) (Keep q _) eqv | KeepV _ p | KeepV _ q =
    EqvKeep $ recompute' {eqv = let EqvKeep e = eqv in e, _}
  recompute' (Drop p _) (Keep q _) eqv | DropV _ p | KeepV _ q =
    void $ absurd eqv
  recompute' (Keep p _) (Drop q _) eqv | KeepV _ p | DropV _ q =
    void $ absurd eqv

private
recompute : {mask1, mask2, n1, n2 : Nat} ->
            {0 p : OPE m1 n1 mask1} -> {0 q : OPE m2 n2 mask2} ->
            (0 _ : p `Eqv` q) -> p `Eqv` q
recompute eqv = recompute' {eqv, _}


export
eqvIndices : {0 p : OPE m1 n1 mask1} -> {0 q : OPE m2 n2 mask2} ->
             p `Eqv` q -> (m1 = m2, n1 = n2, mask1 = mask2)
eqvIndices EqvStop = (Refl, Refl, Refl)
eqvIndices (EqvDrop eqv {eq1 = Refl, eq2 = Refl}) =
  let (Refl, Refl, Refl) = eqvIndices eqv in (Refl, Refl, Refl)
eqvIndices (EqvKeep eqv {eq1 = Refl, eq2 = Refl}) =
  let (Refl, Refl, Refl) = eqvIndices eqv in (Refl, Refl, Refl)

export
0 eqvMask : (p : OPE m1 n mask1) -> (q : OPE m2 n mask2) ->
            mask1 = mask2 -> p `Eqv` q
eqvMask Stop Stop _ = EqvStop
eqvMask (Drop ope1 Refl) (Drop {mask = mm2} ope2 eq2) Refl =
  EqvDrop $ eqvMask ope1 ope2 (doubleInj _ _ eq2)
eqvMask (Drop ope1 Refl) (Keep ope2 eq2) Refl =
  void $ notEvenOdd _ _ eq2
eqvMask (Keep ope1 eq1) (Keep ope2 eq2) Refl =
  EqvKeep $ eqvMask ope1 ope2 (doubleInj _ _ $ inj S $ trans (sym eq1) eq2)
eqvMask (Keep ope1 eq1) (Drop ope2 eq2) Refl =
  void $ notEvenOdd _ _ $ trans (sym eq2) eq1

export
0 eqvEq : (p, q : OPE m n mask) -> p `Eqv` q -> p === q
eqvEq Stop Stop EqvStop = Refl
eqvEq (Drop p eq1) (Drop q eq2) (EqvDrop eqv)
    with %syntactic (doubleInj _ _ $ trans (sym eq1) eq2)
  _ | Refl = cong2 Drop (eqvEq p q eqv) (uip eq1 eq2)
eqvEq (Keep p eq1) (Keep q eq2) (EqvKeep eqv)
    with %syntactic (doubleInj _ _ $ inj S $ trans (sym eq1) eq2)
  _ | Refl = cong2 Keep (eqvEq p q eqv) (uip eq1 eq2)

export
0 eqvEq' : (p : OPE m1 n1 mask1) -> (q : OPE m2 n2 mask2) ->
           p `Eqv` q -> p ~=~ q
eqvEq' p q eqv = let (Refl, Refl, Refl) = eqvIndices eqv in eqvEq p q eqv

export
0 maskEqInner : (0 ope1 : OPE m1 n mask1) -> (0 ope2 : OPE m2 n mask2) ->
                mask1 = mask2 -> m1 = m2
maskEqInner Stop Stop _ = Refl
maskEqInner (Drop ope1 Refl) (Drop ope2 Refl) eq =
  maskEqInner ope1 ope2 (doubleInj _ _ eq)
maskEqInner (Keep ope1 Refl) (Keep ope2 Refl) eq =
  cong S $ maskEqInner ope1 ope2 $ doubleInj _ _ $ inj S eq
maskEqInner (Drop ope1 Refl) (Keep ope2 Refl) eq = void $ notEvenOdd _ _ eq
maskEqInner (Keep {mask = mask1'} ope1 eq1) (Drop {mask = mask2'} ope2 eq2) eq =
  -- matching on eq1, eq2, or eq here triggers that weird coverage bug ☹
  void $ notEvenOdd _ _ $ Calc $
    |~ mask2' + mask2'
    ~~ mask2               ..<(eq2)
    ~~ mask1               ..<(eq)
    ~~ S (mask1' + mask1') ...(eq1)