module Generic.Semantics where

open import Size
open import Data.Bool
open import Data.List.Base as L hiding (lookup ; [_])
open import Data.Product as P hiding (,_)
open import Function
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≑-Reasoning

open import var
open import rel
open import indexed
open import environment as E
open import Generic.Syntax

module _ {I : Set} where

 Alg : (d : Desc I) (π“₯ 𝓒 : I ─Scoped) β†’ Set
 Alg d π“₯ 𝓒 = {i : I} β†’ [ ⟦ d ⟧ (Kripke π“₯ 𝓒) i ⟢ 𝓒 i ]

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

 _─Comp : List I β†’ I ─Scoped β†’ List I β†’ Set
 (Ξ“ ─Comp) 𝓒 Ξ” = {s : Size} {i : I} β†’ Tm d s i Ξ“ β†’ 𝓒 i Ξ”

record Sem {I : Set} (d : Desc I) (π“₯ 𝓒 : I ─Scoped) : Set where
 field  th^π“₯   : {i : I} β†’ Thinnable (π“₯ i)
        var    : {i : I} β†’ [ π“₯ i                   ⟢ 𝓒 i ]
        alg    : {i : I} β†’ [ ⟦ d ⟧ (Kripke π“₯ 𝓒) i  ⟢ 𝓒 i ]

 sem   :  {Ξ“ Ξ” : List I} β†’ (Ξ“ ─Env) π“₯ Ξ” β†’ (Ξ“ ─Comp) 𝓒 Ξ”
 body  :  {Ξ“ Ξ” : List I} {s : Size} β†’ (Ξ“ ─Env) π“₯ Ξ” β†’ βˆ€ Θ i β†’ Scope (Tm d s) Θ i Ξ“ β†’ Kripke π“₯ 𝓒 Θ i Ξ”

 sem ρ (`var k) = var (lookup ρ k)
 sem ρ (`con t) = alg (fmap d (body ρ) t)

 body ρ []       i t = sem ρ t
 body ρ (_ ∷ _)  i t = Ξ» Οƒ vs β†’ sem (vs >> th^Env th^π“₯ ρ Οƒ) t

 closed : ([] ─Comp) 𝓒 []
 closed = sem Ξ΅

open import varlike
module _ {I : Set} {π“₯ 𝓒 : I ─Scoped} where

 reify : VarLike π“₯ β†’ {Ξ“ : List I} β†’ βˆ€ Ξ” i β†’ Kripke π“₯ 𝓒 Ξ” i Ξ“ β†’ Scope 𝓒 Ξ” i Ξ“
 reify vl^π“₯ []         i b = b
 reify vl^π“₯ Ξ”@(_ ∷ _)  i b = b (freshΚ³ vl^Var Ξ”) (freshΛ‘ vl^π“₯ _)

module _ {I : Set} where

 record Syntactic (d : Desc I) (π“₯ : I ─Scoped) : Set where
   field
     var    : {i : I} β†’ [ π“₯ i ⟢ Tm d ∞ i ]
     vl^π“₯  : VarLike π“₯

   semantics : Sem d π“₯ (Tm d ∞)
   Sem.var   semantics = var
   Sem.th^π“₯  semantics = th^π“₯ vl^π“₯
   Sem.alg   semantics = `con ∘ fmap d (reify vl^π“₯)

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

 sy^Var : Syntactic d Var
 Syntactic.var    sy^Var = `var
 Syntactic.vl^π“₯  sy^Var = vl^Var

-- Records are better for the paper, definitions using
-- copatterns are better for the legibility of goals...
module OnlyForDisplayRenaming {I : Set} {d : Desc I} where

 Renaming : Sem d Var (Tm d ∞)
 Renaming = record
   { th^π“₯  = Ξ» k ρ β†’ lookup ρ k
   ; var   = `var
   ; alg   = `con ∘ fmap d (reify vl^Var) }

 ren :  {Ξ“ Ξ” : List I} β†’ (Ξ“ ─Env) Var Ξ” β†’
        (Ξ“ ─Comp) (Tm d ∞) Ξ”
 ren = Sem.sem Renaming

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

 Renaming : Sem d Var (Tm d ∞)
 Sem.th^π“₯  Renaming = Ξ» k ρ β†’ lookup ρ k
 Sem.var   Renaming = `var
 Sem.alg   Renaming = `con ∘ fmap d (reify vl^Var)

 ren :  {Ξ“ Ξ” : List I} β†’ (Ξ“ ─Env) Var Ξ” β†’
        (Ξ“ ─Comp) (Tm d ∞) Ξ”
 ren = Sem.sem Renaming

 th^Tm : {i : I} β†’ Thinnable (Tm d ∞ i)
 th^Tm t ρ = Sem.sem Renaming ρ t

 vl^Tm : VarLike (Tm d ∞)
 new   vl^Tm = `var z
 th^π“₯  vl^Tm = th^Tm

 lookup-base^Tm : {Ξ“ : List I} {Οƒ : I} (k : Var Οƒ Ξ“) β†’ lookup (base vl^Tm) k ≑ `var k
 lookup-base^Tm z                              = refl
 lookup-base^Tm (s k) rewrite lookup-base^Tm k = refl

 base^VarTm^R : βˆ€ {Ξ“} β†’ βˆ€[ VarTm^R ] (base vl^Var {Ξ“}) (base vl^Tm)
 lookup^R base^VarTm^R k = begin
   `var (lookup (base vl^Var) k) β‰‘βŸ¨ cong `var (lookup-base^Var k) ⟩
   `var k                        β‰‘βŸ¨ sym (lookup-base^Tm k) ⟩
   lookup (base vl^Tm) k ∎

 sy^Tm : Syntactic d (Tm d ∞)
 Syntactic.var   sy^Tm = id
 Syntactic.vl^π“₯  sy^Tm = vl^Tm

-- Same thing as with Renaming
module OnlyForDisplaySubstitution {I : Set} {d : Desc I} where

 Substitution : Sem d (Tm d ∞) (Tm d ∞)
 Substitution = record
   { th^π“₯  = Ξ» t ρ β†’ ren ρ t
   ; var   = id
   ; alg   = `con ∘ fmap d (reify vl^Tm) }

 sub :  {Ξ“ Ξ” : List I} β†’ (Ξ“ ─Env) (Tm d ∞) Ξ” β†’
        (Ξ“ ─Comp) (Tm d ∞) Ξ”
 sub = Sem.sem Substitution

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

 Substitution : Sem d (Tm d ∞) (Tm d ∞)
 Sem.th^π“₯  Substitution = Ξ» t ρ β†’ ren ρ t
 Sem.var   Substitution = id
 Sem.alg   Substitution = `con ∘ fmap d (reify vl^Tm)

 sub :  {Ξ“ Ξ” : List I} β†’ (Ξ“ ─Env) (Tm d ∞) Ξ” β†’
        (Ξ“ ─Comp) (Tm d ∞) Ξ”
 sub = Sem.sem Substitution

 infix 5 _[_
 infix 6 _/0]

 _/0] : βˆ€ {Οƒ Ξ“} β†’ Tm d ∞ Οƒ Ξ“ β†’ (Οƒ ∷ Ξ“ ─Env) (Tm d ∞) Ξ“
 _/0] = singleton vl^Tm

 _[_ : βˆ€ {Οƒ Ο„ Ξ“} β†’ Tm d ∞ Ο„ (Οƒ ∷ Ξ“) β†’ (Οƒ ∷ Ξ“ ─Env) (Tm d ∞) Ξ“ β†’ Tm d ∞ Ο„ Ξ“
 t [ ρ = sub ρ t