Module CLF.Substitution

External contextual LF substitutions.

type t = {
  1. location : Syncom.Location.t;
  2. head : Substitution.Head.t;
  3. terms : Term.t Support.List.t;
}

{ Substitution.head; terms; _ } is the substitution

  • ^ if head = Head.None and terms = []
  • m1, m2, ..., mn if head = Head.None and terms = [m1; m2; ...; mn]
  • .. if head = Head.Identity _ and terms = []
  • .., m1, m2, ..., mn if head = Head.Identity _ and terms = [m1; m2; ...; mn]
  • $S if head = Head.Substitution_variable { identifier = "$S"; closure = Option.None; _ } and terms = []
  • $S[o] if head = Head.Substitution_variable { identifier = "$S"; closure = Option.Some o; _ } and terms = []
  • $S, m1, m2, ..., mn if head = Head.Substitution_variable { identifier = "$S"; closure = Option.None; _ } and terms = [m1; m2; ...; mn]
  • $S[o], m1, m2, ..., mn if head = Head.Substitution_variable { identifier = "$S"; closure = Option.Some o; _ } and terms = [m1; m2; ...; mn]
module Head : sig ... end
module Pattern : sig ... end

External contextual LF substitution patterns.