@[reducible, inline]

abbrev MeTTaIL.Ctx : Type

A typing context: the sort of each free variable.

Equations

• MeTTaIL.Ctx = List (String × MeTTaIL.Cat)

def MeTTaIL.Rule.argSorts (r : Rule) : List Cat

The argument categories of a function symbol, read off its rule's non-terminal items in order.

Equations

• r.argSorts = List.flatMap MeTTaIL.Item.cats r.items

inductive MeTTaIL.WellSorted (p : Presentation) (Γ : Ctx) : AST → Cat → Prop

WellSorted p Γ t c: term t has sort c in context Γ, with every subterm well-sorted. A variable has its context sort; an application has its function symbol's result sort, with arguments well-sorted at the symbol's argument sorts.

• var {p : Presentation} {Γ : Ctx} {x : String} {c : Cat} : List.lookup x Γ = some c → WellSorted p Γ (AST.var (DottedPath.base x)) c
• sexp {p : Presentation} {Γ : Ctx} {l : Label} {args : List AST} (r : Rule) : r ∈ p.terms → r.label = l → WellSortedList p Γ args r.argSorts → WellSorted p Γ (AST.sexp l args) r.cat

inductive MeTTaIL.WellSortedList (p : Presentation) (Γ : Ctx) : List AST → List Cat → Prop

Pointwise well-sortedness of an argument list against a list of categories.

• nil {p : Presentation} {Γ : Ctx} : WellSortedList p Γ [] []
• cons {p : Presentation} {Γ : Ctx} {a : AST} {c : Cat} {as : List AST} {cs : List Cat} : WellSorted p Γ a c → WellSortedList p Γ as cs → WellSortedList p Γ (a :: as) (c :: cs)

theorem MeTTaIL.inst_wellSorted {p : Presentation} {Γ Δ : Ctx} {bnds : List (String × AST)} (hb : ∀ (x : String) (c : Cat), List.lookup x Δ = some c → WellSorted p Γ (AST.inst bnds (AST.var (DottedPath.base x))) c) {t : AST} {c : Cat} : WellSorted p Δ t c → WellSorted p Γ (AST.inst bnds t) c

The substitution lemma (inst half): instantiating a well-sorted term with a substitution that is well-sorted for the source context yields a well-sorted term. Proved by mutual induction on the well-sortedness derivation: a variable is handled by the substitution hypothesis, an application recurses into its arguments.

theorem MeTTaIL.instList_wellSorted {p : Presentation} {Γ Δ : Ctx} {bnds : List (String × AST)} (hb : ∀ (x : String) (c : Cat), List.lookup x Δ = some c → WellSorted p Γ (AST.inst bnds (AST.var (DottedPath.base x))) c) {ts : List AST} {cs : List Cat} : WellSortedList p Δ ts cs → WellSortedList p Γ (AST.instList bnds ts) cs