Module CLF.Term

External contextual LF terms.

type t =
  1. | Variable of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    }
    (*

    Variable { identifier = "x"; _ } is the LF-bound term-level variable with name "x".

    *)
  2. | Meta_variable of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    }
    (*

    Meta_variable { identifier = "x"; _ } is the meta-variable with name "x". It may be free or bound.

    *)
  3. | Parameter_variable of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Identifier.t;
    }
    (*

    Parameter_variable { identifier = "#x"; _ } is the term-level parameter variable with name "#x". It may be free or bound.

    *)
  4. | Constant of {
    1. location : Syncom.Location.t;
    2. identifier : Syncom.Qualified_identifier.t;
    }
    (*

    Constant { identifier = "c"; _ } is the term-level constant with qualified identifier "c".

    *)
  5. | Substitution of {
    1. location : Syncom.Location.t;
    2. term : t;
    3. substitution : Substitution.t;
    }
    (*

    Substitution { term; substitution; _ } is the term term[substitution].

    *)
  6. | Application of {
    1. location : Syncom.Location.t;
    2. applicand : t;
    3. arguments : t Support.List1.t;
    }
    (*

    Application { applicand; arguments; _ } is the term-level application of applicand with arguments.

    If applicand = Term.Constant _ with resolved operator description operator, then List1.length arguments = Operator.arity operator.

    *)
  7. | Abstraction of {
    1. location : Syncom.Location.t;
    2. parameter_identifier : Syncom.Identifier.t Support.Option.t;
    3. parameter_type : Typ.t Support.Option.t;
    4. body : t;
    }
    (*
    • Abstraction { parameter_identifier = Option.Some "x"; body; _ } is the term \x. body.
    • Abstraction { parameter_identifier = Option.None; body; _ } is the term \_. body.
    *)
  8. | Hole of {
    1. location : Syncom.Location.t;
    2. variant : [ `Underscore | `Unlabelled | `Labelled of Syncom.Identifier.t ];
    }
    (*

    Hole { variant; _ } is the omission of a term for reconstruction.

    • If variant = `Underscore, then it is the hole _.
    • If variant = `Unlabelled, then it is the hole ?.
    • If variant = `Labelled label, then it is the hole ?label.
    *)
  9. | Tuple of {
    1. location : Syncom.Location.t;
    2. terms : t Support.List1.t;
    }
    (*

    Tuple { terms; _ } is the tuple term <t1; t2; ...; tn> if List1.to_list terms = [t1; t2; ...; tn].

    This should not be confused with computation-level tuples. The type of a contextual LF term-level tuple is a block.

    *)
  10. | Projection of {
    1. location : Syncom.Location.t;
    2. term : t;
    3. projection : [ `By_identifier of Syncom.Identifier.t | `By_position of Support.Int.t ];
    }
    (*
    • Projection { term = u; projection = `By_identifier x; _ } is the term u.x.
    • Projection { term = u; projection = `By_position n; _ } is the term u.n.
    *)
  11. | Type_annotated of {
    1. location : Syncom.Location.t;
    2. term : t;
    3. typ : Typ.t;
    }
    (*

    Type_annotated { term = u; typ = t; _ } is the term u : t.

    *)
module Pattern : sig ... end

External contextual LF term patterns.