module Subst_list where

open import Ty                         using (Var; Con; _⇒_; 𝕋; 𝕋𝕋; 𝕋𝕋s; 𝕍ar; _≟t_)
open import Relation.Nullary.Decidable using (⌊_⌋)
open import Data.List                  using (List; []; _∷_; filter; map)
open import Data.Product               using (_×_; _,_; proj₁; proj₂; ∃; Σ)
open import Data.Maybe.Core            using (Maybe; nothing; just)
open import Data.Bool                  using (false)
open import Data.Nat                   using (_≟_)
open import Relation.Nullary.Core      using (yes; no)
open import Function                   using (_∘_)

open import Relation.Binary            using (Decidable)
open import Relation.Binary.PropositionalEquality using (cong; _≡_; refl; sym)
open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_; _≡⟨_⟩_; _∎)


Mapping : Set
Mapping = 𝕍ar × 𝕋

Subs : Set
Subs = List Mapping

emptySubs : Subs
emptySubs = []

insert : 𝕍ar → 𝕋 → Subs → Subs
insert v τ s = (v , τ) ∷ s

sub : 𝕋 → 𝕍ar → 𝕋 → 𝕋
-- substitute τ for v in t' 
sub τ v (Var v') with v ≟ v'
... | yes _ = τ
... | no _ = Var v'
sub τ v (Con c) = Con c
sub τ v (τ₁ ⇒ τ₂) = (sub τ v τ₁) ⇒ (sub τ v τ₂)

apply : Subs → 𝕋 → 𝕋
apply [] τ = τ
apply ((v , τ₀) ∷ s) τ = apply s (sub τ₀ v τ)

applyP : Subs → 𝕋𝕋 → 𝕋𝕋
applyP [] p       = p  -- needed because otherwise agda does not take into account the 
                       -- fact that applyP [] (τ₁ , τ₂) ≡ (τ₁ , τ₂)
applyP s (τ₁ , τ₂) = (apply s τ₁ , apply s τ₂)

applyL : Subs → 𝕋𝕋s → 𝕋𝕋s
applyL [] l = l -- this is needed because otherwise agda does not take into account the 
                -- fact that applyL [] l ≡ l
applyL s l = map (applyP s) l

_∘s_ : Subs → Subs → Subs
s₁ ∘s []             = s₁ 
s₁ ∘s ((v , τ) ∷ s₂) = (v , apply s₁ τ) ∷ (s₁ ∘s s₂)

_≺_ : Subs → Subs → Set
s₁ ≺ s₂ = ∃ (\s → (s ∘s s₁) ≡ s₂)

_∘ms_ : Maybe Subs → Maybe Subs → Maybe Subs
nothing ∘ms nothing   = nothing
just s₁ ∘ms just []   = just s₁ 
just s₁ ∘ms just ((v , τ)∷ s₂) = just ((v , apply s₁ τ) ∷ (s₁ ∘s s₂))
nothing ∘ms just _    = nothing
just _  ∘ms nothing   = nothing

invL : ∀ {A B : Set} {a : A} {b : B} {c : A} {d : B} → ((a , b) ≡ (c , d)) → (a ≡ c)
invL {A} {B} {a} {b} {.a} {.b} refl = refl

invR : ∀ {A B : Set} {a : A} {b : B} {c : A} {d : B} → (((a , b) ≡ (c , d)) → (b ≡ d))
invR {A} {B} {a} {b} {.a} {.b} refl = refl

invHd : ∀ {A : Set} {a : A} {x : List A} {b : A} {y : List A} → ((a ∷ x) ≡ (b ∷ y)) → (a ≡ b)
invHd {A} {a} {x} {.a} {.x} refl = refl

invTl : ∀ {A : Set} {a : A} {x : List A} {b : A} {y : List A} → (((a ∷ x) ≡ (b ∷ y)) → (x ≡ y))
invTl {A} {a} {x} {.a} {.x} refl = refl

invJust : ∀ {A : Set} {n : A} {m : A} → (just n ≡ just m) → n ≡ m
invJust {A} {n} {.n} refl = refl 

invL⇒ : ∀ {a b c d : 𝕋} → ((a ⇒ b) ≡ (c ⇒ d)) → (a ≡ c)
invL⇒ {a} {b} { .a} {.b} refl = refl

invR⇒ : ∀ {a b c d : 𝕋} → ((a ⇒ b) ≡ (c ⇒ d)) → (b ≡ d)
invR⇒ {a} {b} {.a} {.b} refl = refl

_≟m_ : Decidable {A = Mapping} _≡_
-- Equality on pairs (v,t).
(v , τ) ≟m (v' , τ') with v ≟ v' 
(v , τ) ≟m (.v , τ') | yes refl with τ ≟t τ'
(v , τ) ≟m (.v , .τ) | yes refl | yes refl = yes refl
(v , τ) ≟m (.v , τ') | yes refl | no prf   = no (prf ∘ invR)
(v , τ) ≟m (v' , τ') | no prf   = no (prf ∘ invL)

_≟s_ : Decidable {A = Subs} _≡_
-- Equality on values of type Subs (lists of pairs (v,t)).
[]        ≟s [] = yes refl
(m1 ∷ s1) ≟s (m2 ∷ s2) with m1 ≟m m2 
(m1 ∷ s1) ≟s (.m1 ∷ s2)  | yes refl with s1 ≟s s2
(m1 ∷ s1) ≟s (.m1 ∷ .s1) | yes refl | yes refl = yes refl
(m1 ∷ s1) ≟s (.m1 ∷ s2)  | yes refl | no prf   = no (prf ∘ invTl)
(m1 ∷ s1) ≟s (m2 ∷ s2)   | no prf   = no (prf ∘ invHd)
[]         ≟s (_ ∷ _) = no (λ ())
(_ ∷ _)    ≟s []      = no (λ ())

_≟ms_ : Decidable {A = Maybe Subs} _≡_
nothing ≟ms nothing = yes refl
just s1  ≟ms just s2 with s1 ≟s s2
just s1 ≟ms just .s1 | yes refl = yes refl
just s1 ≟ms just s2  | no prf   = no (prf ∘ invJust)
nothing ≟ms just _  = no λ()
just _  ≟ms nothing = no λ()

lemmaApply0 : ∀ t → apply emptySubs t ≡ t
lemmaApply0 (Var v)   = refl
lemmaApply0 (Con c)   = refl
lemmaApply0 (ta ⇒ tb) = begin
   apply emptySubs (ta ⇒ tb) ≡⟨ refl ⟩
   apply emptySubs ta ⇒ apply emptySubs tb ≡⟨ cong (λ ta → (ta ⇒ apply emptySubs tb)) (lemmaApply0 ta) ⟩
   ta ⇒ apply emptySubs tb ≡⟨ cong (_⇒_ ta) (lemmaApply0 tb) ⟩
   ta ⇒ tb
   ∎ 

lemmaS0 : ∀ (s : Subs) → (emptySubs ∘s s) ≡ s 
lemmaS0 []             = refl
lemmaS0 ((v , t) ∷ s1) = begin
   emptySubs ∘s ((v , t) ∷ s1)                 ≡⟨ refl ⟩
   (v , apply emptySubs t) ∷ (emptySubs ∘s s1) ≡⟨ cong (λ t → ((v , t) ∷ (emptySubs ∘s s1))) (lemmaApply0 t) ⟩
   (v , t ) ∷ (emptySubs ∘s s1)                ≡⟨ cong (λ s → (v , t) ∷ s) (lemmaS0 s1) ⟩
   ((v , t ) ∷ s1)
   ∎ 

comm_apply : ∀ s τ₁ τ₂ → (apply s τ₁ ≡ apply s τ₂) → (apply s τ₂ ≡ apply s τ₁)
comm_apply s τ₁ τ₂ = sym