module Semiring.Syntax where
open import SOAS.Common
open import SOAS.Context
open import SOAS.Variable
open import SOAS.Families.Core
open import SOAS.Construction.Structure
open import SOAS.ContextMaps.Inductive
open import SOAS.Metatheory.Syntax
open import Semiring.Signature
private
variable
Ξ Ξ Ξ : Ctx
Ξ± : *T
π : Familyβ
module SR:Terms (π : Familyβ) where
data SR : Familyβ where
var : β βΎΜ£ SR
mvar : π Ξ± Ξ β Sub SR Ξ Ξ β SR Ξ± Ξ
π : SR * Ξ
_β_ : SR * Ξ β SR * Ξ β SR * Ξ
π : SR * Ξ
_β_ : SR * Ξ β SR * Ξ β SR * Ξ
infixl 20 _β_
infixl 30 _β_
open import SOAS.Metatheory.MetaAlgebra β
F π
SRα΅ : MetaAlg SR
SRα΅ = record
{ πππ = Ξ» where
(zeroβ β
_) β π
(addβ β
a , b) β _β_ a b
(oneβ β
_) β π
(multβ β
a , b) β _β_ a b
; π£ππ = var ; ππ£ππ = Ξ» πͺ mΞ΅ β mvar πͺ (tabulate mΞ΅) }
module SRα΅ = MetaAlg SRα΅
module _ {π : Familyβ}(πα΅ : MetaAlg π) where
open MetaAlg πα΅
π€ππ : SR βΎΜ£ π
π : Sub SR Ξ Ξ β Ξ ~[ π ]β Ξ
π (t β Ο) new = π€ππ t
π (t β Ο) (old v) = π Ο v
π€ππ (mvar πͺ mΞ΅) = ππ£ππ πͺ (π mΞ΅)
π€ππ (var v) = π£ππ v
π€ππ π = πππ (zeroβ β
tt)
π€ππ (_β_ a b) = πππ (addβ β
π€ππ a , π€ππ b)
π€ππ π = πππ (oneβ β
tt)
π€ππ (_β_ a b) = πππ (multβ β
π€ππ a , π€ππ b)
π€ππα΅β : MetaAlgβ SRα΅ πα΅ π€ππ
π€ππα΅β = record
{ β¨πππβ© = Ξ»{ {t = t} β β¨πππβ© t }
; β¨π£ππβ© = refl
; β¨ππ£ππβ© = Ξ»{ {πͺ = πͺ}{mΞ΅} β cong (ππ£ππ πͺ) (dext (π-tab mΞ΅)) } }
where
open β‘-Reasoning
β¨πππβ© : (t : β
SR Ξ± Ξ) β π€ππ (SRα΅.πππ t) β‘ πππ (β
β π€ππ t)
β¨πππβ© (zeroβ β
_) = refl
β¨πππβ© (addβ β
_) = refl
β¨πππβ© (oneβ β
_) = refl
β¨πππβ© (multβ β
_) = refl
π-tab : (mΞ΅ : Ξ ~[ SR ]β Ξ)(v : β Ξ± Ξ ) β π (tabulate mΞ΅) v β‘ π€ππ (mΞ΅ v)
π-tab mΞ΅ new = refl
π-tab mΞ΅ (old v) = π-tab (mΞ΅ β old) v
module _ (g : SR βΎΜ£ π)(gα΅β : MetaAlgβ SRα΅ πα΅ g) where
open MetaAlgβ gα΅β
π€ππ! : (t : SR Ξ± Ξ) β π€ππ t β‘ g t
π-ix : (mΞ΅ : Sub SR Ξ Ξ)(v : β Ξ± Ξ ) β π mΞ΅ v β‘ g (index mΞ΅ v)
π-ix (x β mΞ΅) new = π€ππ! x
π-ix (x β mΞ΅) (old v) = π-ix mΞ΅ v
π€ππ! (mvar πͺ mΞ΅) rewrite cong (ππ£ππ πͺ) (dext (π-ix mΞ΅))
= trans (sym β¨ππ£ππβ©) (cong (g β mvar πͺ) (tabβixβid mΞ΅))
π€ππ! (var v) = sym β¨π£ππβ©
π€ππ! π = sym β¨πππβ©
π€ππ! (_β_ a b) rewrite π€ππ! a | π€ππ! b = sym β¨πππβ©
π€ππ! π = sym β¨πππβ©
π€ππ! (_β_ a b) rewrite π€ππ! a | π€ππ! b = sym β¨πππβ©
SR:Syn : Syntax
SR:Syn = record
{ β
F = β
F
; β
:CS = β
:CompatStr
; mvarα΅’ = SR:Terms.mvar
; π:Init = Ξ» π β let open SR:Terms π in record
{ β₯ = SR β SRα΅
; β₯-is-initial = record { ! = Ξ»{ {π β πα΅} β π€ππ πα΅ β π€ππα΅β πα΅ }
; !-unique = Ξ»{ {π β πα΅} (f β fα΅β) {x = t} β π€ππ! πα΅ f fα΅β t } } } }
open Syntax SR:Syn public
open SR:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands SRα΅ public
open import SOAS.Metatheory SR:Syn public