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
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
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