{-# OPTIONS --allow-unsolved-metas #-}

open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_)


-- Syntax of Mixed terms and Rewriting contexts
module SyntaxRew
  {{ Α : Set }}    -- type level constants
  {{ C : Set }}    -- term level constants

  {{ Var : Set }}  -- variables
  {{ decEqVar : Decidable (_≡_ {A = Var}) }}


  {{ Κ : Set }} -- proof term symbols

  where

{-
open import LF
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants
  {{ Var }}  -- variables
  {{ decEqVar }} 
-}

open import Syntax --{{Α}} {{C}} {{T}} {{K}} {{Var}} {{UVar}} 
  {{ Α }}    -- type level constants
  {{ C }}    -- term level constants
  {{ Var }}  -- variables
  {{ decEqVar }} 

  {{ Κ }}     -- proof term constants
  public

-- Mixed terms

data MT : Set where
  symbM : Κ → MT
  go : Go → MT
  _apM_ : MT → MT → MT
  <_,_>M : t → MT → MT
  lamM : Κ → MT → MT

-- helper lemata to convince Agda
open import Data.Product using (_×_ ; _,_)
open import Relation.Binary.PropositionalEquality using (refl)

inspect-apM : {e₁ e₂ : MT} {ê₁ ê₂ : MT} →
  e₁ apM ê₁ ≡ e₂ apM ê₂ →
  e₁ ≡ e₂ × ê₁ ≡ ê₂
inspect-apM refl = refl , refl

inspect-<>M : {M₁ M₂ : t} {ê₁ ê₂ : MT} →
  < M₁ , ê₁ >M ≡ < M₂ , ê₂ >M →
  M₁ ≡ M₂ × ê₁ ≡ ê₂
inspect-<>M refl = refl , refl

inspect-lamM : {κ₁ κ₂ : Κ} {ê₁ ê₂ : MT} →
  lamM κ₁ ê₁ ≡ lamM κ₂ ê₂ →
  κ₁ ≡ κ₂ × ê₁ ≡ ê₂
inspect-lamM refl = refl , refl

-- embeding of Mixed terms to Proof terms

inMT : PT → MT
inMT (symbP κ) = symbM κ
inMT (e apP e₁) = (inMT e) apM (inMT e₁)
inMT < M , e >P = < M , (inMT e) >M
inMT (lamP κ e) = lamM κ (inMT e)

open import Relation.Binary.PropositionalEquality using (cong ; cong₂)

injective-inMT : {e₁ e₂ : PT} → inMT e₁ ≡ inMT e₂ → e₁ ≡ e₂
injective-inMT {symbP x₁} {symbP .x₁} refl = cong symbP refl
injective-inMT {symbP x₁} {e₂ apP e₃} ()
injective-inMT {symbP x₁} {< x₂ , e₂ >P} ()
injective-inMT {symbP x₁} {lamP x₂ e₂} ()
injective-inMT {e₁ apP e₂} {symbP x₁} ()
injective-inMT {e₁ apP e₂} {e₃ apP e₄} x
  with inspect-apM x
... | eql , eqr  = cong₂ (λ e e' → e apP e') (injective-inMT eql) (injective-inMT eqr)
injective-inMT {e₁ apP e₂} {< x₁ , e₃ >P} ()
injective-inMT {e₁ apP e₂} {lamP x₁ e₃} ()
injective-inMT {< x₁ , e₁ >P} {symbP x₂} ()
injective-inMT {< x₁ , e₁ >P} {e₂ apP e₃} ()
injective-inMT {< x₁ , e₁ >P} {< x₂ , e₂ >P} x
  with inspect-<>M x
... | refl , eq = cong (<_,_>P x₁) (injective-inMT eq)
injective-inMT {< x₁ , e₁ >P} {lamP x₂ e₂} ()
injective-inMT {lamP x₁ e₁} {symbP x₂} ()
injective-inMT {lamP x₁ e₁} {e₂ apP e₃} ()
injective-inMT {lamP x₁ e₁} {< x₂ , e₂ >P} ()
injective-inMT {lamP x₁ e₁} {lamP x₂ e₂} x
  with inspect-lamM x
... | refl , eq = cong (lamP x₁) (injective-inMT eq)




-- single value substitution on mixed terms
_[_/_]MT : MT → t → Var → MT
symbM κ [ M / x ]MT = symbM κ
(e apM e') [ M / x ]MT = (e [ M / x ]MT) apM (e' [ M / x ]MT)
< M , e >M [ N / x ]MT = < M [ N / x ]t , e [ N / x ]MT >M
lamM κ e [ M / x ]MT = lamM κ (e [ M / x ]MT)
go G [ M / x ]MT = go (G [ M / x ]Go )


open import Relation.Binary.PropositionalEquality using ( refl ; cong₂ ; cong )

-- embeding in PT distributes over substitution
inMT-[/]-dist : {e : PT } {N : t} {x : Var} →
  inMT (e [ N / x ]PT) ≡ (inMT e) [ N / x ]MT
inMT-[/]-dist {symbP κ} = refl
inMT-[/]-dist {e apP e₁} = cong₂ (λ e' e'' → e' apM e'') inMT-[/]-dist inMT-[/]-dist
inMT-[/]-dist {< M , e >P} {N} {x}  = cong (λ e' → < ( M [ N /  x ]t ) , e' >M) inMT-[/]-dist
inMT-[/]-dist {lamP κ e} = cong (λ e' → lamM κ e') inMT-[/]-dist 




-- inMT is cong
inMT-PT : {e₁ e₂ : PT} → inMT e₁ ≡ inMT e₂ → e₁ ≡ e₂
inMT-PT {symbP x} {symbP x₁} refl = cong symbP refl
inMT-PT {symbP x} {e₂ apP e₃} ()
inMT-PT {symbP x} {< x₁ , e₂ >P} ()
inMT-PT {symbP x} {lamP x₁ e₂} ()
inMT-PT {e₁ apP e₂} {symbP x} ()
inMT-PT {e₁ apP e₂} {e₃ apP e₄} eq 
  with inspect-apM eq
... | eql , eqr = cong₂ (λ x x₁ → x apP x₁) (injective-inMT eql) (injective-inMT eqr)
inMT-PT {e₁ apP e₂} {< x , e₃ >P} ()
inMT-PT {e₁ apP e₂} {lamP x e₃} ()
inMT-PT {< x , e₁ >P} {symbP x₁} ()
inMT-PT {< x , e₁ >P} {e₂ apP e₃} ()
inMT-PT {< x , e₁ >P} {< x₁ , e₂ >P} eq
  with inspect-<>M eq
... | eq₁ , eq₂ = cong₂ (λ x₂ y → < x₂ , y >P) eq₁ (inMT-PT eq₂)
inMT-PT {< x , e₁ >P} {lamP x₁ e₂} ()
inMT-PT {lamP x e₁} {symbP x₁} ()
inMT-PT {lamP x e₁} {e₂ apP e₃} ()
inMT-PT {lamP x e₁} {< x₁ , e₂ >P} ()
inMT-PT {lamP x e₁} {lamP x₁ e₂} eq
  with inspect-lamM eq
... | eq₁ , eq₂ = cong₂ (λ x₂ y → lamP x₂ y) eq₁ (inMT-PT eq₂)

open import Data.Product using (∃)
inMT-PT' : {e₁ : MT} {e₂ : PT} → e₁ ≡ inMT e₂ → (∃ λ e₁' → inMT e₁' ≡ e₁)
inMT-PT' {symbM x} {symbP .x} refl = (symbP x) , refl
inMT-PT' {symbM x} {e₂ apP e₃} ()
inMT-PT' {symbM x} {< x₁ , e₂ >P} ()
inMT-PT' {symbM x} {lamP x₁ e₂} ()
inMT-PT' {go x} {symbP x₁} ()
inMT-PT' {go x} {e₂ apP e₃} ()
inMT-PT' {go x} {< x₁ , e₂ >P} ()
inMT-PT' {go x} {lamP x₁ e₂} ()
inMT-PT' {e₁ apM e₂} {symbP x} ()
inMT-PT' {.(inMT e₂) apM .(inMT e₃)} {e₂ apP e₃} refl = (e₂ apP e₃) , refl
inMT-PT' {e₁ apM e₂} {< x , e₃ >P} ()
inMT-PT' {e₁ apM e₂} {lamP x e₃} ()
inMT-PT' {< x , e₁ >M} {symbP x₁} ()
inMT-PT' {< x , e₁ >M} {e₂ apP e₃} ()
inMT-PT' {< x , .(inMT e₂) >M} {< .x , e₂ >P} refl = < x , e₂ >P , refl
inMT-PT' {< x , e₁ >M} {lamP x₁ e₂} ()
inMT-PT' {lamM x e₁} {symbP x₁} ()
inMT-PT' {lamM x e₁} {e₂ apP e₃} ()
inMT-PT' {lamM x e₁} {< x₁ , e₂ >P} ()
inMT-PT' {lamM x .(inMT e₂)} {lamP .x e₂} refl = (lamP x e₂) , refl





-- Rewriting contexts

data RewC : Set where
  ● : RewC
  _ap_ : MT → RewC → RewC
  <_,_> : t → RewC → RewC
  lam : Κ → RewC → RewC


-- Hole replacement with rewriting context is a rewriting context

_[_]RewC : RewC → RewC → RewC
● [ C' ]RewC = C'
(e ap C ) [ C' ]RewC = _ap_ e (C [ C' ]RewC)
< M , C > [ C' ]RewC = < M , C [ C' ]RewC >
lam κ C [ C' ]RewC = lam κ (C [ C' ]RewC)


-- Hole replacement with mixed term is a mixed term
_[_] : RewC → MT → MT
● [ ê ] = ê
(e ap C ) [ ê ] = e apM (C [ ê ])
< M , C > [ ê ] = < M , C [ ê ] >M
lam κ C [ ê ] = lamM κ (C [ ê ])


-- hole replacement commutes 
RewC-MT-[]-comm : {C₁ C₂ : RewC} {ê : MT} → 
 ((C₁ [ C₂ ]RewC) [ ê ] ) ≡ C₁ [ (C₂ [ ê ] ) ]
RewC-MT-[]-comm {●} = refl
RewC-MT-[]-comm {e ap C₁} = cong (_apM_ e) (RewC-MT-[]-comm {C₁ = C₁})
RewC-MT-[]-comm {< M , C₁ >} = cong (<_,_>M M) (RewC-MT-[]-comm  {C₁ = C₁})
RewC-MT-[]-comm {lam κ C₁} = cong (lamM κ) (RewC-MT-[]-comm  {C₁ = C₁})
 

open import Relation.Nullary using (yes ; no )

{-
-- Distributivity of substitution over Goals and Definite Clauses

[/]Go-dist : {G : Go} {M : t} {x : Var} {θ : Θ} →
  (θ ΘGo (G [ M / x ]Go)) ≡ (θ ΘGo G) [ (θ Θt M) / x ]Go

[/]De-dist : {D : De} {M : t} {x : Var} {θ : Θ} →
  (θ ΘDe (D [ M / x ]De)) ≡ (θ ΘDe D) [ (θ Θt M) / x ]De

-- definition

[/]Go-dist {at A} = cong (at) [/]T-dist
[/]Go-dist {D ⇒ G} = cong₂ _⇒_ ([/]De-dist {D = D})  ([/]Go-dist {G = G})
[/]Go-dist {∃Go x' A G} {x = x} with decEqVar x x'
... | yes _ = refl
... | no _ = cong₂ (∃Go x') [/]T-dist ([/]Go-dist {G = G})
[/]Go-dist {∀Go x' A G} {x = x} with decEqVar x x'
... | yes _ = refl
... | no _ = cong₂ (∀Go x') [/]T-dist ([/]Go-dist {G = G})

[/]De-dist {at A} = cong (at) [/]T-dist
[/]De-dist {G ⇒ D} = cong₂ _⇒_ ([/]Go-dist {G = G})  ([/]De-dist {D = D})
[/]De-dist {∀D x' A D} {x = x} with decEqVar x x'
... | yes _ = refl
... | no _ = cong₂ (∀D x') [/]T-dist ([/]De-dist {D = D})
-}


open import Data.Product using ( ∃ )

-- when we identify a goal G in MT and we identify another ê in MT 
-- then there is unique rewC C' s.t. G is identified in ê 

unique-RewC-Go : {C₁ C₂ : RewC} {ê : MT} {G : Go} →
  C₁ [ go G ] ≡ C₂ [ ê ] →
  ∃ λ C' →  C' [ go G ] ≡ ê ×  ∀ { ê' } → C₁ [ ê' ] ≡ C₂ [ C' [ ê' ] ]

-- 
unique-RewC-Go {●} {●} refl = ● , (refl , (λ {x} → refl))
unique-RewC-Go {●} {e ap C₂} ()
unique-RewC-Go {●} {< M , C₂ >} ()
unique-RewC-Go {●} {lam κ C₂} ()
unique-RewC-Go {e ap C₁} {●} refl = (e ap C₁) , refl , (λ {x} → refl)
unique-RewC-Go {e ap C₁} {e' ap C₂} eq
  with inspect-apM eq
... | refl , eq'
  with unique-RewC-Go eq'
... | C' , eq'' , res  = C' , eq'' , cong (_apM_ e) res
unique-RewC-Go {e ap C₁} {< M , C₂ >} ()
unique-RewC-Go {e ap C₁} {lam κ C₂} ()
unique-RewC-Go {< M , C₁ >} {●} refl = < M , C₁ > , refl , (λ {x} → refl)
unique-RewC-Go {< M , C₁ >} {e ap C₂} ()
unique-RewC-Go {< M , C₁ >} {< M' , C₂ >} eq
  with inspect-<>M eq
... | refl , eq'
  with unique-RewC-Go eq'
... | C' , eq'' , res  = C' , eq'' , cong (<_,_>M M) res
unique-RewC-Go {< M , C₁ >} {lam κ C₂} ()
unique-RewC-Go {lam κ C₁} {●} refl = lam κ C₁ , refl , (λ {x} → refl)
unique-RewC-Go {lam κ C₁} {e ap C₂} ()
unique-RewC-Go {lam κ C₁} {< M , C₂ >} ()
unique-RewC-Go {lam κ C₁} {lam κ' C₂} eq
  with inspect-lamM eq
... | refl , eq'
  with unique-RewC-Go eq'
... | C' , eq'' , res  = C' , eq'' , cong (lamM κ) res



unique-RewC-Go' : {C₁ C₂ : RewC} {ê ê' : MT} {G : Go} →
  C₁ [ go G ] ≡ C₂ [ ê ] →
  ∃ λ C' →  C' [ go G ] ≡ ê ×  C₁ [ ê' ] ≡ C₂ [ C' [ ê' ] ]

-- 
unique-RewC-Go' {●} {●} refl = ● , (refl , (refl))
unique-RewC-Go' {●} {e ap C₂} ()
unique-RewC-Go' {●} {< M , C₂ >} ()
unique-RewC-Go' {●} {lam κ C₂} ()
unique-RewC-Go' {e ap C₁} {●} refl = (e ap C₁) , refl , (refl)
unique-RewC-Go' {e ap C₁} {e' ap C₂} eq
  with inspect-apM eq
... | refl , eq'
  with unique-RewC-Go' eq'
... | C' , eq'' , res  = C' , eq'' , cong (_apM_ e) res
unique-RewC-Go' {e ap C₁} {< M , C₂ >} ()
unique-RewC-Go' {e ap C₁} {lam κ C₂} ()
unique-RewC-Go' {< M , C₁ >} {●} refl = < M , C₁ > , refl , (refl)
unique-RewC-Go' {< M , C₁ >} {e ap C₂} ()
unique-RewC-Go' {< M , C₁ >} {< M' , C₂ >} eq
  with inspect-<>M eq
... | refl , eq'
  with unique-RewC-Go' eq'
... | C' , eq'' , res  = C' , eq'' , cong (<_,_>M M) res
unique-RewC-Go' {< M , C₁ >} {lam κ C₂} ()
unique-RewC-Go' {lam κ C₁} {●} refl = lam κ C₁ , refl , (refl)
unique-RewC-Go' {lam κ C₁} {e ap C₂} ()
unique-RewC-Go' {lam κ C₁} {< M , C₂ >} ()
unique-RewC-Go' {lam κ C₁} {lam κ' C₂} eq
  with inspect-lamM eq
... | refl , eq'
  with unique-RewC-Go' eq'
... | C' , eq'' , res  = C' , eq'' , cong (lamM κ) res



-- simultaneous substitution for mixed terms
_ΘMT_ : ∀ {S Γ Γ'} → Θ S Γ Γ' → MT → MT
θ ΘMT symbM κ = symbM κ
θ ΘMT go G = go (θ ΘGo G)
θ ΘMT (ê apM ê₁) = (θ ΘMT ê) apM (θ ΘMT ê₁ )
θ ΘMT < M , ê >M = < θ Θt M , θ ΘMT ê >M
θ ΘMT lamM κ ê = lamM κ (θ ΘMT ê)

{-
--congruence
unit-ε-MT : {ê : MT} → ε ΘMT ê ≡ ê
unit-ε-MT {symbM κ} = refl
unit-ε-MT {go G} = cong (λ G' → go G') unit-ε-Go
unit-ε-MT {ê apM ê₁} = cong₂ (λ ê' ê₁' → ê' apM ê₁') unit-ε-MT unit-ε-MT
unit-ε-MT {< M , ê >M} = cong₂ (λ M' ê' → < M' , ê' >M) unit-ε-t unit-ε-MT
unit-ε-MT {lamM κ ê} = cong (λ ê' → lamM κ ê') unit-ε-MT
-}

-- simultaneous substtution for rewriting contexts
_ΘC_ : ∀ { S Γ Γ'} → Θ S Γ Γ' → RewC → RewC
θ ΘC ● = ●
θ ΘC (e ap C₁) = (θ ΘMT e) ap (θ ΘC C₁)
θ ΘC < M , C₁ > = < θ Θt M , θ ΘC C₁ >
θ ΘC lam κ C₁ = lam κ (θ ΘC C₁)

{-
-- congruence 
unit-ε-RewC : {C : RewC} → ε ΘC C ≡ C
unit-ε-RewC {●} = refl
unit-ε-RewC {e ap C₁} = cong₂ (λ e' C₁' → e' ap C₁') unit-ε-MT unit-ε-RewC
unit-ε-RewC {< M , C₁ >} = cong₂ (λ M' C₁' → < M' , C₁' >) unit-ε-t unit-ε-RewC
unit-ε-RewC {lam κ C₁} = cong (λ C₁' → lam κ C₁') unit-ε-RewC
-}