Module CLF.Typ

External contextual LF types.

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

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

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

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

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

    *)
  3. | Arrow of {
    1. location : Syncom.Location.t;
    2. domain : t;
    3. range : t;
    4. orientation : [ `Forward | `Backward ];
    }
    (*
    • Arrow { domain; range; orientation = `Forward; _ } is the type domain -> range.
    • Arrow { range; domain; orientation = `Backward; _ } is the type range <- domain.
    *)
  4. | Pi of {
    1. location : Syncom.Location.t;
    2. parameter_identifier : Syncom.Identifier.t Support.Option.t;
    3. parameter_type : t;
    4. plicity : Syncom.Plicity.t;
    5. body : t;
    }
    (*
    • Pi { parameter_identifier = Option.Some "x"; parameter_type = t; body; _ } is the dependent product type { x : t } body. The variable "x" ranges over LF terms.
    • Pi { parameter_identifier = Option.None; parameter_type = t; body; _ } is the dependent product type { _ : t } body.
    *)
  5. | Block of {
    1. location : Syncom.Location.t;
    2. elements : [ `Unnamed of t | `Record of (Syncom.Identifier.t * t) Support.List1.t ];
    }
    (*
    • Block { elements = `Unnamed t; _ } is the block type block t.
    • Block { elements = `Record [("x1", t1); ("x2", t2); ...; ("xn", tn)]; _ } is the block type block (x1 : t1, x2 : t2, ..., xn : tn). This is a dependent sum type, or telescope, with tj being able to refer to "xi" when i < j.
    *)