Module Term.Pattern

External contextual LF term patterns.

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

    Variable { identifier = "x"; _ } is the LF-bound variable pattern "x".

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

    Meta_variable { identifier = "x"; _ } is the term-level meta-variable pattern "x".

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

    Parameter_variable { identifier = "#x"; _ } is the term-level parameter variable pattern with name "#x".

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

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

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

    Wildcard _ is the term-level catch-all pattern _.

    *)
  6. | Tuple of {
    1. location : Syncom.Location.t;
    2. terms : t Support.List1.t;
    }
    (*

    Tuple { terms; _ } is the tuple pattern <p1; p2; ...; pn> if terms = [p1; p2; ...; pn].

    *)
  7. | 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; _ } is the pattern for the projection of a tuple term. This projection is used to indicate which element of a tuple the scrutinee is matched against in a case-expression. This is typically used for parameter variable patterns such as #p.1.

    *)
  8. | 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 pattern \x:t. body.

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

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

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

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

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

    *)
  11. | Type_annotated of {
    1. location : Syncom.Location.t;
    2. term : t;
    3. typ : Typ.t;
    }
    (*

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

    *)