module howe where
open import Data.Nat
open import Data.Vec
open import Data.List
open import Data.Product
import Data.Fin  as F
import Relation.Binary as B
open import Relation.Binary.PropositionalEquality hiding (subst)
open import Relation.Nullary

module Utils where
  plus0 : (n : ℕ) → n + 0 ≡ n
  plus0 zero = refl
  plus0 (suc n) rewrite plus0 n = refl

  suc-on-right : (n m : ℕ) → n + suc m ≡ suc (n + m)
  suc-on-right zero m = refl
  suc-on-right (suc n) m rewrite suc-on-right n m = refl

  plus-commute : (n m : ℕ) → n + m ≡ m + n
  plus-commute zero m rewrite plus0 m = refl
  plus-commute (suc n) m rewrite suc-on-right m n | plus-commute n m = refl

  bracket-≤ : {n m : ℕ}(x : ℕ) → n ≤ m → n + x ≤ m + x
  bracket-≤ {n} {m} zero prf rewrite plus0 n | plus0 m = prf
  bracket-≤ {n} {m} (suc x) prf rewrite suc-on-right n x | suc-on-right m x =
    s≤s (bracket-≤ x prf)

  remove-suc-right : {n m : ℕ} → n ≤ m → n ≤ suc m
  remove-suc-right z≤n = z≤n
  remove-suc-right (s≤s prf) = s≤s (remove-suc-right prf)

  remove-suc-left : {n m : ℕ} → suc n ≤ m → n ≤ m
  remove-suc-left (s≤s prf) = remove-suc-right prf

  remove-+-left : {n m x : ℕ} → x + n ≤ m → n ≤ m
  remove-+-left {n} {m} {zero} prf = prf
  remove-+-left {n} {m} {suc x} prf =
    remove-+-left {n}{m}{x} (remove-suc-left {x + n} {m} prf)

  remove-+-right : {n m x : ℕ} → n + x ≤ m → n ≤ m
  remove-+-right {n}{m}{x} rewrite plus-commute n x = remove-+-left {n}{m}{x}


record LCS : Set₁ where
  constructor lcs
  field
    O : Set
    Canon : O → Set
    arity : O → List ℕ

data Term (L : LCS) : Set where
  var : ℕ → Term L
  op  : (o : LCS.O L) → Vec (Term L) (length (LCS.arity L o)) → Term L

data WellBound {L : LCS} : ℕ → Term L → Set
data WellBoundMany {L : LCS} : {m : ℕ} →  ℕ → ℕ → Vec (Term L) m → Set

data WellBound {L : LCS} where
  var : {n m : ℕ} → n < m → WellBound m (var n)
  op  : (o : LCS.O L){m : ℕ}(args : Vec (Term L) (length (LCS.arity L o)))
      → WellBoundMany 0 m args → WellBound m (op o args)
data WellBoundMany {L : LCS} where
  nil  : {k n : ℕ} → WellBoundMany k n []
  cons : {k n m : ℕ}(h : Term L)(rest : Vec (Term L) m)
       → WellBound (n + k) h
       → WellBoundMany (suc k) n rest
       → WellBoundMany k n (h ∷ rest)

Closed : {L : LCS} → Term L → Set
Closed = WellBound 0

mutual
  well-bound-weaken : {L : LCS}{n m : ℕ}{t : Term L} → n ≤ m → WellBound n t
                    → WellBound m t
  well-bound-weaken prf (var x) =
    var (B.IsPartialOrder.trans
          (B.IsTotalOrder.isPartialOrder
            (B.IsDecTotalOrder.isTotalOrder
              (B.DecTotalOrder.isDecTotalOrder decTotalOrder))) x prf)
  well-bound-weaken prf (op o args x) =
    op o args (well-bound-many-weaken prf x)

  well-bound-many-weaken : {L : LCS}{n m k len : ℕ}{v : Vec (Term L) len}
                         → n ≤ m → WellBoundMany k n v → WellBoundMany k m v
  well-bound-many-weaken prf nil = nil
  well-bound-many-weaken {k = k} prf (cons _ _ x wbm) =
    cons _ _
      (well-bound-weaken (Utils.bracket-≤ k prf) x)
      (well-bound-many-weaken prf wbm)


data IsCanon {L : LCS} : Term L → Set where
  op  : {o : LCS.O L}(args : _) → LCS.Canon L o → IsCanon (op o args)


record Eval (L : LCS) : Set₁ where
  constructor eval
  field
    _⇓_ : Term L → Term L → Set
    steps : ℕ → Term L → Term L → Set
    -- Expected properties of a stepping relation
    eval-to-canon : {t t' : Term L} → t ⇓ t' → IsCanon t'
    canon-to-canon : {t : Term L} → IsCanon t → t ⇓ t
    deterministic : {t t₁ t₂ : Term L} → t ⇓ t₁ → t ⇓ t₂ → t₁ ≡ t₂
    -- Indexed steps
    steps-eventually : {t t' : Term L} → t ⇓ t' → Σ ℕ λ n → steps n t t'
    steps-agrees : {t t' : Term L}{n : ℕ} → steps n t t' → t ⇓ t'

mutual
  -- This relies on the fact that we only ever substitute closed terms
  subst : {L : LCS} → Term L → ℕ → Term L → Term L
  subst new n (var x) with compare x n
  ... | less .x k = var x
  ... | equal .n = new
  ... | greater .n k = var (n + k)
  subst {L} new n (op o args) = op o (subst-many 0 new n args)

  subst-many : {L : LCS}{n : ℕ} → ℕ → Term L → ℕ → Vec (Term L) n → Vec (Term L) n
  subst-many m new n [] = []
  subst-many m new n (x ∷ v) = subst new (n + m) x ∷ subst-many (suc m) new n v

mutual
  subst-closes : {L : LCS}{n x : ℕ}(t t' : Term L)
               → x < n
               → WellBound (suc n) t → Closed t'
               → WellBound n (subst t' x t)
  subst-closes {x = x} .(var n) t' x<n (var {n} prf) closed with compare n x
  subst-closes {_} {_} {.(suc (m + k))} .(var m) t' x<n (var {.m} prf) closed
    | less m k = var (Utils.remove-+-right (Utils.remove-suc-left x<n))
  subst-closes {_} {_} {.m} .(var m) t' x<n (var {.m} prf) closed
    | equal m = well-bound-weaken z≤n closed
  subst-closes {_} {_} {.m} .(var (suc (m + k))) t' x<n (var {.(suc (m + k))} (s≤s prf)) closed
    | greater m k = var prf
  subst-closes .(op o args) t' x<n (op o args x) closed =
    op o _ (subst-closes-many args t' x<n x closed)

  subst-closes-many : {L : LCS}{len n k x : ℕ}(v : Vec (Term L) len)(t : Term L)
                    → x < n
                    → WellBoundMany k (suc n) v → Closed t
                    → WellBoundMany k n (subst-many k t x v)
  subst-closes-many .[] t x<n nil closed = nil
  subst-closes-many {k = k} .(h ∷ rest) t x<n (cons h rest x wb) closed
    rewrite Utils.plus0 k =
      cons _ _ (subst-closes h t (Utils.bracket-≤ _ x<n) x closed)
        (subst-closes-many rest t x<n wb closed)

data Close {L : LCS} : ℕ → Term L → Term L → Term L → Term L → Set where
  zero : (t t' : Term L) → Close 0 t t t' t'
  suc  : {n : ℕ}(t₁ t₁' t₂ t₃ t₃' : Term L)
       → Close n (subst t₂ 0 t₁) (subst t₂ 0 t₁') t₃ t₃'
       → Close (suc n) t₁ t₁' t₃ t₃'

close-equals : {L : LCS}{n : ℕ}(t t₁ t₂ : Term L) → Close n t t t₁ t₂
             → t₁ ≡ t₂
close-equals t t₁ .t₁ (zero .t .t₁) = refl
close-equals t t₁ t₂ (suc .t .t t₃ .t₁ .t₂ closing)
  rewrite close-equals _ _ _ closing = refl

close-flip : {L : LCS}{n : ℕ}{t₁ t₂ t₁' t₂' : Term L}
  → Close n t₁ t₂ t₁' t₂' → Close n t₂ t₁ t₂' t₁'
close-flip (zero t₁ t₁') = zero t₁ t₁'
close-flip (suc t₁ t₂ t₃ t₁' t₂' closed) =
  suc t₂ t₁ t₃ t₂' t₁' (close-flip closed)

close-split : {L : LCS}{n : ℕ}{t₁ t₃ t₁' t₃' : Term L}(t₂ : Term L)
  → Close n t₁ t₃ t₁' t₃'
  → Σ (Term L) λ {
    t₂' → Close n t₁ t₂ t₁' t₂' × Close n t₂ t₃ t₂' t₃'
   }
close-split t₂ (zero t t') = (t₂ , ( {!zero t t₂!} , {!!} ))
close-split t₂ (suc t₁ t₁' t₄ t₃ t₃' prf) = {!!}


module Equivalence (L : LCS)(E : Eval L) where
  open LCS L
  open Eval E

  data _≈*_·_ : {m : ℕ} → Vec (Term L) m → Vec (Term L) m → ℕ → Set
  record _≈_ (t₁ t₂ : Term L) : Set

  record _≈_ (t₁ t₂ : Term L) where
    coinductive
    constructor equiv
    field
      coterm₁ : {o : O}(args : _) → t₁ ⇓ op o args → Σ _ λ t₄ → t₂ ⇓ op o t₄
      coterm₂ : {o : O}(args : _) → t₂ ⇓ op o args → Σ _ λ t₄ → t₁ ⇓ op o t₄
      run :
        {o : O}(args args' : _)
        → t₁ ⇓ op o args → t₂ ⇓ op o args'
        → args ≈* args' · 0

  data _≈*_·_ where
    nil  : (n : ℕ) → [] ≈* [] · n
    cons : {m : ℕ}(n : ℕ)(h h' : Term L)(rest rest' : Vec (Term L) m)
         → ((c c' : Term L) → Close n h h' c c' → c ≈ c')
         → rest ≈* rest' · suc n
         → (h ∷ rest) ≈* (h' ∷ rest') · n
  open _≈_
  open _≈*_·_

  oper-injective : {o : O}{args args' : Vec (Term L) _}
                 → Term.op o args ≡ Term.op o args'
                 → args ≡ args'
  oper-injective refl = refl
  mutual
    reflexivity-many : {m k : ℕ}(v : Vec (Term L) m) → v ≈* v · k
    reflexivity-many {k} [] = nil _
    reflexivity-many {k} (x ∷ v) =
      cons _ x x v v matching (reflexivity-many v)
      where matching : (c c' : Term L) → Close _ x x c c' → c ≈ c'
            matching c c' closing rewrite close-equals x c c' closing =
              reflexivity c'

    reflexivity : (t : Term L) → t ≈ t
    reflexivity t .run args args' run₁ run₂
      rewrite oper-injective (deterministic run₁ run₂) =
        reflexivity-many args'
    reflexivity t .coterm₁ t₃ run₁ = (t₃ , run₁)
    reflexivity t .coterm₂ t₃ run₁ = (t₃ , run₁)
  mutual
    symmetry-many : {m k : ℕ}(v v' : Vec (Term L) m)
                  → v ≈* v' · k → v' ≈* v · k
    symmetry-many .[] .[] (nil n) = nil _
    symmetry-many .(h ∷ rest) .(h' ∷ rest') (cons n h h' rest rest' x prf) =
      cons n h' h rest' rest matching (symmetry-many rest rest' prf)
      where matching : (c c' : Term L) → Close n h' h c c' → c ≈ c'
            matching c c' close = symmetry _ _ (x c' c (close-flip close))

    symmetry : (t t' : Term L) → t ≈ t' → t' ≈ t
    symmetry t t' eq .run args args' run₁ run₂ =
      symmetry-many args' args (eq .run args' args run₂ run₁)
    symmetry t t' eq .coterm₁ t₃ run₁ = eq .coterm₂ t₃ run₁
    symmetry t t' eq .coterm₂ t₃ run₁ = eq .coterm₁ t₃ run₁

  mutual
    transitivity-many : {m k : ℕ}(v v' v'' : Vec (Term L) m)
                      → v ≈* v' · k → v' ≈* v'' · k
                      → v ≈* v'' · k
    transitivity-many .[] .[] v'' (nil n) eq₂ = eq₂
    transitivity-many .(h ∷ rest) .(h' ∷ rest') .(h'' ∷ rest'') (cons n h h' rest rest' x eq₁) (cons .n .h' h'' .rest' rest'' x₁ eq₂) =
      cons n h h'' rest rest'' matching (transitivity-many _ _ _ eq₁ eq₂)
      where matching : (c c' : Term L) → Close n h h'' c c' → c ≈ c'
            matching c c' closed = {!!}

    transitivity : (t t' t'' : Term L) → t ≈ t' → t' ≈ t'' → t ≈ t''
    transitivity t t' t'' eq₁ eq₂ .run args args'' run₁ run₃
      with eq₁ .coterm₁ args run₁
    ... | t₂' , run₂ with eval-to-canon run₂
    ... | op args' x =
      transitivity-many args args' args''
        (eq₁ .run args args' run₁ run₂)
        (eq₂ .run args' args'' run₂ run₃)
    transitivity t t' t'' eq₁ eq₂ .coterm₁ t₃ run₁ =
      let (t₄ , run₂) = eq₁ .coterm₁ t₃ run₁
      in eq₂ .coterm₁ t₄ run₂
    transitivity t t' t'' eq₁ eq₂ .coterm₂ t₃ run₁ =
      let (t₄ , run₂) = eq₂ .coterm₂ t₃ run₁
      in eq₁ .coterm₂ t₄ run₂