module Inception.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 Inception.Signature
private
variable
Ξ Ξ Ξ : Ctx
Ξ± : IAT
π : Familyβ
module IA:Terms (π : Familyβ) where
data IA : Familyβ where
var : β βΎΜ£ IA
mvar : π Ξ± Ξ β Sub IA Ξ Ξ β IA Ξ± Ξ
rec : IA L Ξ β IA P Ξ β IA A Ξ
inc : IA A (L β Ξ) β IA A (P β Ξ) β IA A Ξ
open import SOAS.Metatheory.MetaAlgebra β
F π
IAα΅ : MetaAlg IA
IAα΅ = record
{ πππ = Ξ» where
(recβ β
a , b) β rec a b
(incβ β
a , b) β inc a b
; π£ππ = var ; ππ£ππ = Ξ» πͺ mΞ΅ β mvar πͺ (tabulate mΞ΅) }
module IAα΅ = MetaAlg IAα΅
module _ {π : Familyβ}(πα΅ : MetaAlg π) where
open MetaAlg πα΅
π€ππ : IA βΎΜ£ π
π : Sub IA Ξ Ξ β Ξ ~[ π ]β Ξ
π (t β Ο) new = π€ππ t
π (t β Ο) (old v) = π Ο v
π€ππ (mvar πͺ mΞ΅) = ππ£ππ πͺ (π mΞ΅)
π€ππ (var v) = π£ππ v
π€ππ (rec a b) = πππ (recβ β
π€ππ a , π€ππ b)
π€ππ (inc a b) = πππ (incβ β
π€ππ a , π€ππ b)
π€ππα΅β : MetaAlgβ IAα΅ πα΅ π€ππ
π€ππα΅β = record
{ β¨πππβ© = Ξ»{ {t = t} β β¨πππβ© t }
; β¨π£ππβ© = refl
; β¨ππ£ππβ© = Ξ»{ {πͺ = πͺ}{mΞ΅} β cong (ππ£ππ πͺ) (dext (π-tab mΞ΅)) } }
where
open β‘-Reasoning
β¨πππβ© : (t : β
IA Ξ± Ξ) β π€ππ (IAα΅.πππ t) β‘ πππ (β
β π€ππ t)
β¨πππβ© (recβ β
_) = refl
β¨πππβ© (incβ β
_) = refl
π-tab : (mΞ΅ : Ξ ~[ IA ]β Ξ)(v : β Ξ± Ξ ) β π (tabulate mΞ΅) v β‘ π€ππ (mΞ΅ v)
π-tab mΞ΅ new = refl
π-tab mΞ΅ (old v) = π-tab (mΞ΅ β old) v
module _ (g : IA βΎΜ£ π)(gα΅β : MetaAlgβ IAα΅ πα΅ g) where
open MetaAlgβ gα΅β
π€ππ! : (t : IA Ξ± Ξ) β π€ππ t β‘ g t
π-ix : (mΞ΅ : Sub IA Ξ Ξ)(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 β¨π£ππβ©
π€ππ! (rec a b) rewrite π€ππ! a | π€ππ! b = sym β¨πππβ©
π€ππ! (inc a b) rewrite π€ππ! a | π€ππ! b = sym β¨πππβ©
IA:Syn : Syntax
IA:Syn = record
{ β
F = β
F
; β
:CS = β
:CompatStr
; mvarα΅’ = IA:Terms.mvar
; π:Init = Ξ» π β let open IA:Terms π in record
{ β₯ = IA β IAα΅
; β₯-is-initial = record { ! = Ξ»{ {π β πα΅} β π€ππ πα΅ β π€ππα΅β πα΅ }
; !-unique = Ξ»{ {π β πα΅} (f β fα΅β) {x = t} β π€ππ! πα΅ f fα΅β t } } } }
open Syntax IA:Syn public
open IA:Terms public
open import SOAS.Families.Build public
open import SOAS.Syntax.Shorthands IAα΅ public
open import SOAS.Metatheory IA:Syn public