Module LF.Term

External LF terms.

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

    Variable { identifier = "x"; _ } is the term-level variable with name "x". It may be free or bound. If it is free, then an implicit type-level or kind-level Pi binder should be reconstructed for it.

    *)
  2. | 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".

    *)
  3. | 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.

    *)
  4. | 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"; parameter_type = Option.Some t; body; _ } is the term \(x : t). body. The variable "x" ranges over LF terms. The parameter identifier may be omitted (represented as _), and the parameter type annotation is typically omitted.

    *)
  5. | Wildcard of {
    1. location : Syncom.Location.t;
    }
    (*

    Wildcard { _ } is the omission _ of a fresh term-level variable. This is analogous to a fresh free variable.

    *)
  6. | 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.

    *)