module Generic.Simulation where

open import Size
open import Data.List hiding ([_] ; lookup ; zip)
open import Function
open import Relation.Binary.PropositionalEquality hiding ([_])

open import indexed
open import var hiding (_<$>_)
open import varlike
open import rel
open import environment
open import Generic.Syntax
open import Generic.Semantics
open import Generic.Zip

module _ {I : Set} {π“₯₁ π“₯β‚‚ 𝓒₁ 𝓒₂ : I β†’ List I β†’ Set} (𝓑^π“₯  : Rel π“₯₁ π“₯β‚‚) (𝓑^𝓒  : Rel 𝓒₁ 𝓒₂) where

 reify^R : {vl₁ : VarLike π“₯₁} {vlβ‚‚ : VarLike π“₯β‚‚} (vl^R : VarLike^R 𝓑^π“₯ vl₁ vlβ‚‚) β†’
           {Ξ“ : List I} β†’ βˆ€ Ξ” Οƒ β†’ {k₁ : Kripke π“₯₁ 𝓒₁ Ξ” Οƒ Ξ“} {kβ‚‚ : Kripke π“₯β‚‚ 𝓒₂ Ξ” Οƒ Ξ“} β†’
           Kripke^R 𝓑^π“₯ 𝓑^𝓒 Ξ” Οƒ k₁ kβ‚‚ β†’ rel 𝓑^𝓒 (reify vl₁ Ξ” Οƒ k₁) (reify vlβ‚‚ Ξ” Οƒ kβ‚‚)
 reify^R vl^R []         Οƒ k^R = k^R
 reify^R vl^R Ξ”@(_ ∷ _)  Οƒ k^R = k^R (freshΚ³ vl^Var Ξ”) (VarLike^R.freshΛ‘^R vl^R _)

 record Sim (d : Desc I) (𝓒₁ : Sem d π“₯₁ 𝓒₁) (𝓒₂ : Sem d π“₯β‚‚ 𝓒₂) : Set where
   field  th^R   : {Ξ“ Ξ” : List I} {i : I} {v₁ : π“₯₁ i Ξ“} {vβ‚‚ : π“₯β‚‚ i Ξ“} β†’ (Οƒ : Thinning Ξ“ Ξ”) β†’ rel 𝓑^π“₯ v₁ vβ‚‚ β†’ rel 𝓑^π“₯ (Sem.th^π“₯ 𝓒₁ v₁ Οƒ) (Sem.th^π“₯ 𝓒₂ vβ‚‚ Οƒ)
          var^R  : {Ξ“ : List I} {i : I} {v₁ : π“₯₁ i Ξ“} {vβ‚‚ : π“₯β‚‚ i Ξ“} β†’ rel 𝓑^π“₯ v₁ vβ‚‚ β†’ rel 𝓑^𝓒 (Sem.var 𝓒₁ v₁) (Sem.var 𝓒₂ vβ‚‚)
          alg^R  :  {Ξ“ Ξ” : List I} {i : I} {s : Size} β†’ (b : ⟦ d ⟧ (Scope (Tm d s)) i Ξ“) β†’ {ρ₁ : (Ξ“ ─Env) π“₯₁ Ξ”} {ρ₂ : (Ξ“ ─Env) π“₯β‚‚ Ξ”} β†’ βˆ€[ 𝓑^π“₯ ] ρ₁ ρ₂ β†’
                    let  v₁ = fmap d (Sem.body 𝓒₁ ρ₁) b
                         vβ‚‚ = fmap d (Sem.body 𝓒₂ ρ₂) b
                    in Zip d (Kripke^R 𝓑^π“₯ 𝓑^𝓒) v₁ vβ‚‚ β†’ rel 𝓑^𝓒 (Sem.alg 𝓒₁ v₁) (Sem.alg 𝓒₂ vβ‚‚)

   sim   :  {Ξ“ Ξ” : List I} {ρ₁ : (Ξ“ ─Env) π“₯₁ Ξ”} {ρ₂ : (Ξ“ ─Env) π“₯β‚‚ Ξ”} {i : I} {s : Size} β†’ βˆ€[ 𝓑^π“₯ ] ρ₁ ρ₂ β†’ (t : Tm d s i Ξ“) β†’ rel 𝓑^𝓒 (Sem.sem 𝓒₁ ρ₁ t) (Sem.sem 𝓒₂ ρ₂ t)
   body  :  {Ξ“ Θ : List I} {ρ₁ : (Ξ“ ─Env) π“₯₁ Θ} {ρ₂ : (Ξ“ ─Env) π“₯β‚‚ Θ} {s : Size} β†’ βˆ€[ 𝓑^π“₯ ] ρ₁ ρ₂ β†’ βˆ€ Ξ” j β†’ (t : Scope (Tm d s) Ξ” j Ξ“) β†’
            Kripke^R 𝓑^π“₯ 𝓑^𝓒 Ξ” j (Sem.body 𝓒₁ ρ₁ Ξ” j t) (Sem.body 𝓒₂ ρ₂ Ξ” j t)

   sim ρ (`var k) = var^R (lookup^R ρ k)
   sim ρ (`con t) = alg^R t ρ (zip d (body ρ) t)

   body ρ []       i t = sim ρ t
   body ρ (Οƒ ∷ Ξ”)  i t = Ξ» Οƒ ρ′ β†’ sim (ρ′ >>^R (th^R Οƒ <$>^R ρ)) t

module _ {I : Set} {d : Desc I} where

 RenExt : Sim Eq^R Eq^R d Renaming Renaming
 Sim.th^R   RenExt = Ξ» ρ β†’ cong (lookup ρ)
 Sim.var^R  RenExt = cong `var
 Sim.alg^R  RenExt = Ξ» _ _ β†’
   cong `con ∘ zip^reify Eq^R (reify^R Eq^R Eq^R (vl^Refl vl^Var)) d

 SubExt : Sim Eq^R Eq^R d Substitution Substitution
 Sim.th^R   SubExt = Ξ» ρ β†’ cong (ren ρ)
 Sim.var^R  SubExt = id
 Sim.alg^R  SubExt = Ξ» _ _ β†’
   cong `con ∘ zip^reify Eq^R (reify^R Eq^R Eq^R (vl^Refl vl^Tm)) d

module _ {I : Set} {d : Desc I} where

 vl^VarTm : VarLike^R VarTm^R vl^Var (vl^Tm {d = d})
 VarLike^R.new^R  vl^VarTm = refl
 VarLike^R.th^R   vl^VarTm = Ξ» Οƒ β†’ cong (ren Οƒ)

 RenSub : Sim VarTm^R Eq^R d Renaming Substitution
 Sim.var^R  RenSub = id
 Sim.th^R   RenSub = Ξ» { _ refl β†’ refl }
 Sim.alg^R  RenSub = Ξ» _ _ β†’
   cong `con ∘ zip^reify (mkRel (_≑_ ∘ `var)) (reify^R VarTm^R Eq^R vl^VarTm) d

 rensub :  {Ξ“ Ξ” : List I} (ρ : Thinning Ξ“ Ξ”) {i : I} (t : Tm d ∞ i Ξ“) β†’ ren ρ t ≑ sub (`var <$> ρ) t
 rensub ρ = Sim.sim RenSub (pack^R (Ξ» _ β†’ refl))