-- NOTE with-K
module Solver.AddMax where

import Algebra

open import Data.Bool using (Bool ; true ; false)
open import Data.Nat.NP
import Data.Nat.Properties as Props
open import Data.Fin using (Fin ; Ordering ; less ; equal ; greater)
import Data.Fin.Props as FP
open import Data.List 
open import Data.Vec hiding ([_] ; _++_)

open import Data.Maybe using (Maybe ; just ; nothing)


open import Relation.Binary.PropositionalEquality hiding ([_])

open import Relation.Nullary using (Dec ; yes ; no)

module ℕP = Algebra.CommutativeSemiring Props.commutativeSemiring 
module ℕ⊔ = Algebra.CommutativeSemiringWithoutOne Props.⊔-⊓-0-commutativeSemiringWithoutOne



+-distr-⊔ :  a m n  a + (m  n)  (a + m)  (a + n)
+-distr-⊔ zero m n = refl
+-distr-⊔ (suc a) m n = cong suc (+-distr-⊔ a m n)

+-distr-⊔' :  m n a  (m  n) + a  (m + a)  (n + a)
+-distr-⊔' m n a = trans (ℕP.+-comm (m  n) a) (trans (+-distr-⊔ a m n) 
               (cong₂ _⊔_ (ℕP.+-comm a m) (ℕP.+-comm a n)))

⊔-idem :  m  m  m  m
⊔-idem zero = refl
⊔-idem (suc m) = cong suc (⊔-idem m)

congL :  {A B C : Set} {x x' y}  (f : A  B  C)  x  x'  f x y  f x' y 
congL f refl = refl

congR :  {A B C : Set} {x : A}{y y' : B}  (f : A  B  C)  y  y'  f x y  f x y' 
congR f refl = refl

module NatSyntax (nrVars : )(G : Vec  nrVars) where

  Env = Vec  nrVars
  Var = Fin nrVars

  data Syn : Set where
    con :   Syn 
    var : Var  Syn
    _:+_ : Syn  Syn  Syn 
    _:u_ : Syn  Syn  Syn

  infixl 4 _:+_

  eval : Syn  
  eval (con x) = x
  eval (var x) = lookup x G
  eval (syn :+ syn₁) = eval syn + eval syn₁
  eval (syn :u syn₁) = eval syn  eval syn₁


  data N1 : Syn  Set where 
    con_::[] :  x  N1 (con x)
    var_::_ :  {S} (i : Var)  N1 S  N1 (var i :+ S) 

  data N2 : Syn  Set where
    lift :  {S}  N1 S  N2 S
    max  :  {S S'}  N1 S  N2 S'  N2 (S :u S')

  record N1Proof S : Set where
    constructor _⊢_
    field
      {S'} : Syn
      term : N1 S'
      proof : eval S  eval S' 

  record N2Proof S : Set where
    constructor _⊢_
    field
      {S'} : Syn
      term : N2 S'
      proof : eval S  eval S'

  liftP :  {S}  N1Proof S  N2Proof S
  liftP (term  proof) = (lift term)  proof

  incr :  {S'} S  N1 S'  N1Proof (S :+ S')
  incr S con x ::[] = con eval S + x ::[]  refl
  incr {var .i :+ S'} S (var i :: s1) with incr S s1
  ... | s1'  p = (var i :: s1')  trans (sym (ℕP.+-assoc (eval S) (lookup i G) (eval S'))) 
                                   (trans(congL _+_ (ℕP.+-comm (eval S) (lookup i G)))
                                   (trans (ℕP.+-assoc (lookup i G) (eval S) (eval S')) 
                                   (cong (_+_ (lookup i G)) p)))

  append :  {S S'}  N1 S  N1 S'  N1Proof (S :+ S')
  append con x ::[] s2 = incr _ s2
  append (var i :: s1) s2 with append s1 s2
  ... |  s3  proof = var i :: s3  trans (ℕP.+-assoc (lookup i G) _ _) (cong (_+_ (lookup i G)) proof)

  insert :  {S} i  N1 S  N1Proof (var i :+ S)
  insert i con x ::[] = (var i :: con x ::[])  refl
  insert {var .j :+ S} i (var j :: s1) with Data.Fin.toℕ i ≤? Data.Fin.toℕ j
  ... | yes _ = var i :: var j :: s1  refl
  ... | no  _ with insert i s1
  ... | t  proof = var j :: t  trans (sym (ℕP.+-assoc (lookup i G) (lookup j G) (eval S))) 
                                       (trans
                                          (congL _+_ (ℕP.+-comm (lookup i G) (lookup j G))
                                           )
                                       (trans (ℕP.+-assoc (lookup j G) _ _) (cong (_+_ (lookup j G)) proof)))

  merge :  {S S'}  N1 S  N1 S'  N1Proof (S :+ S')
  merge con x ::[] s2 = incr _ s2
  merge (var i :: s1) s2 with merge s1 s2
  ... | t1  p1 with insert i t1
  ... | t2  p2 = t2  trans (trans (ℕP.+-assoc (lookup i G) _ _) (cong (_+_ (lookup i G)) p1)) p2

  mapN1-N2 :  {S S'}  N1 S  N2 S'  N2Proof (S :+ S')
  mapN1-N2 s1 (lift x) = liftP (merge s1 x)
  mapN1-N2 {S} s1 (max x s2) with merge s1 x | mapN1-N2 s1 s2
  ... | t1  p1 | t2  p2 = (max t1 t2)  trans (+-distr-⊔ (eval S) _ _) (cong₂ _⊔_ p1 p2)

  u-merge :  {S S'}  N2 S  N2 S'  N2Proof (S :u S')
  u-merge (lift x)   s2 = max x s2  refl
  u-merge {S :u S'} (max x s1) s2 with u-merge s1 s2
  ... | t  p = (max x t)  trans (ℕ⊔.+-assoc (eval S) _ _) (cong (_⊔_ (eval S)) p)

  +-merge :  {S S'}  N2 S  N2 S'  N2Proof (S :+ S')
  +-merge (lift x)   s2 = mapN1-N2 x s2
  +-merge {S :u S'} (max x s1) s2 with mapN1-N2 x s2 |  +-merge s1 s2
  ... | tx  px | ts  ps with u-merge tx ts
  ... | t  p = t  trans (trans (+-distr-⊔' (eval S) _ _) (cong₂ _⊔_ px ps)) p

  _≤ℕ_ :     Bool
  m ≤ℕ n with m ≤? n
  ... | yes _ = true
  ... | no  _ = false

  _≤1_ :  {S S'}  N1 S  N1 S'  Bool
  con x ::[] ≤1 con x₁ ::[] = x ≤ℕ x₁
  con x ::[] ≤1 (var i :: ys) = true
  (var i :: xs) ≤1 con x ::[] = false
  (var i :: xs) ≤1 (var j :: ys) with Data.Fin.compare i j
  (var .(Data.Fin.inject least) :: xs) ≤1 (var j :: ys) | less .j least = true
  (var .j :: xs) ≤1 (var j :: ys) | equal .j = xs ≤1 ys
  (var i :: xs) ≤1 (var .(Data.Fin.inject least) :: ys) | greater .i least = false

  _≡1_ :  {S S'}  N1 S  N1 S'  Maybe (eval S  eval S')
  con x ::[] ≡1 con x₁ ::[] with x  x₁
  ... | yes p = just p
  ... | no _  = nothing
  con x ::[] ≡1 (var i :: s2) = nothing
  (var i :: s1) ≡1 con x ::[] = nothing
  (var i :: s1) ≡1 (var i₁ :: s2) with i FP.≟ i₁ | s1 ≡1 s2
  ... | yes p | just p2 = just (cong₂ _+_ (cong₂ lookup p (refl {x = G})) p2)
  ... | yes p | nothing = nothing
  ... | no  _ | m = nothing
    where open import Data.Fin.Props

  N2-insert :  {S S'}  N1 S  N2 S'  N2Proof (S :u S')
  N2-insert {S} x (lift x₁) with x ≤1 x₁
  ... | true = max x (lift x₁)  refl
  ... | false = max x₁ (lift x)  ℕ⊔.+-comm (eval S) _
  N2-insert {S} {S' :u S''} x (max x₁ s) with x ≤1 x₁
  ... | true  = (max x (max x₁ s))  refl
  ... | false with N2-insert x s
  ... | t  p = (max x₁ t)  trans (trans (sym (ℕ⊔.+-assoc (eval S) (eval S') (eval S'')))
                                      (trans (congL _⊔_ (ℕ⊔.+-comm (eval S) _))
                                       (ℕ⊔.+-assoc (eval S') _ _))) (cong (_⊔_ (eval S')) p) 
  Tran =  {S}  N2 S  N2Proof S

  sort : Tran
  sort (lift x) = lift x  refl
  sort {S :u S'} (max x s1) with sort s1
  ... | s2  p2 with N2-insert x s2
  ... | s3  p3 = s3  (trans (cong (_⊔_ (eval S)) p2) p3)  

  nub : Tran
  nub (lift x) = lift x  refl
  nub {S :u S'} (max x (lift x₁)) with x ≡1 x₁
  ... | just p  = (lift x)  trans (cong (_⊔_ (eval S)) (sym p)) (⊔-idem (eval S))
  ... | nothing = max x (lift x₁)  refl
  nub {S :u (S' :u S'')} (max x (max x₁ x₂)) with nub (max x₁ x₂) | x ≡1 x₁
  ... | t2  p2 | just p  = t2  trans (trans (sym (ℕ⊔.+-assoc (eval S) (eval S') (eval S''))) 
                                   (congL _⊔_ (trans (congL _⊔_ p) (⊔-idem (eval S'))))) p2
  ... | t2  p2 | nothing = max x t2  cong (_⊔_ (eval S)) p2

  norm2 : (x : Syn)  N2Proof x
  norm2 (con x) = (lift con x ::[])  refl
  norm2 (var x) = lift (var x :: con 0 ::[])  ℕP.+-comm 0 (lookup x G)
  norm2 (x :+ x₁) with norm2 x | norm2 x₁
  ... | s1  p1 | s2  p2 with +-merge s1 s2
  ... | s3  p3 = s3  (trans (cong₂ _+_ p1 p2) p3)
  norm2 (x :u x₁) with norm2 x | norm2 x₁
  ... | s1  p1 | s2  p2 with u-merge s1 s2
  ... | s3  p3 = s3  trans (cong₂ _⊔_ p1 p2) p3


  _∘S_ : Tran  Tran  Tran
  (f ∘S g) x =  (N2Proof.term (f (N2Proof.term (g x))))  trans (N2Proof.proof (g x)) (N2Proof.proof (f (N2Proof.term (g x))))

  norm : (x : Syn)  N2Proof x
  norm x with norm2 x
  ... | t1  p1 with (nub ∘S sort) t1
  ... | t2  p2 = t2  trans p1 p2

  proof : (x y : Syn)  eval (N2Proof.S' (norm x))  eval (N2Proof.S' (norm y))
             eval x  eval y
  proof x y eq = trans (N2Proof.proof (norm x)) (trans eq (sym (N2Proof.proof (norm y))))

test :  (x y : )  5 + x + (9 + y + 10)  12 + y + x + 12
test x y = proof (con 5 :+ x' :+ (con 9 :+ y' :+ con 10)) (con 12 :+ y' :+ x' :+ con 12) refl where
  open NatSyntax 2 (x  y  [])
  x' = var Data.Fin.zero
  y' = var (Data.Fin.suc Data.Fin.zero)

test' :  (x y : )  ((x + 3)  (2 + y)) + 7  (2 + y + 7)  (5 + x + 5)
test' x y = proof LHS RHS refl where
  open NatSyntax 2 (x  y  [])
  #_ = con
  x' = var Data.Fin.zero
  y' = var (Data.Fin.suc Data.Fin.zero)
  LHS = ((x' :+ # 3) :u (# 2 :+ y')) :+ # 7 
  RHS = (# 2 :+ y' :+ # 7) :u (# 5 :+ x' :+ # 5) 

test3 :  x  1 + (x  x + 0)  1 + x
test3 x = proof LHS RHS refl where
  open NatSyntax 1 (x  [])
  #_ = con
  x' = var Data.Fin.zero
  LHS = # 1 :+ (x' :u x' :+ # 0)
  RHS = # 1 :+ x'