Module CLF.Object

Contextual LF types, terms and patterns blurred together.

type t =
  1. | Raw_identifier of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t * [ `Plain | `Hash | `Dollar ];
    3. prefixed : Stdlib.Bool.t;
    }
    (*
    • Raw_identifier { identifier = "$x"; modifier = `Dollar; _ } is the substitution variable "$x".
    • Raw_identifier { identifier = "#x"; modifier = `Hash; _ } is the parameter variable "#x".
    • Raw_identifier { identifier = "x"; prefixed = false; _ } is the variable or constant "x".
    • Raw_identifier { identifier = "x"; prefixed = true; _ } is the prefixed variable or constant "(x)".

    A prefixed constant may appear as an argument, or as applicand in prefix notation irrespective of its pre-defined fixity and associativity.

    *)
  2. | Raw_qualified_identifier of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Qualified_identifier.t;
    3. prefixed : Stdlib.Bool.t;
    }
    (*
    • Raw_qualified_identifier { identifier = "M.x"; prefixed = false; _ } is the constant "M.x".
    • Raw_qualified_identifier { identifier = "M.x"; prefixed = true; _ } is the prefixed constant "(M.x)".

    Since identifiers are ambiguous with qualified identifiers in the parser, the following may be assumed during disambiguation: List.length (Qualified_identifier.namespaces identifier) >= 1.

    Qualified identifiers are ambiguous with named projections.

    A prefixed constant may appear as an argument, or as applicand in prefix notation irrespective of its pre-defined fixity and associativity.

    *)
  3. | Raw_hole of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. variant : [ `Underscore | `Unlabelled | `Labelled of Beluga_syntax.Syncom.Identifier.t ];
    }
  4. | Raw_pi of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. parameter_identifier : Beluga_syntax.Syncom.Identifier.t Support.Option.t;
    3. parameter_sort : t Support.Option.t;
    4. plicity : Beluga_syntax.Syncom.Plicity.t;
    5. body : t;
    }
    (*

    Raw_pi { parameter_identifier = Option.Some "x"; parameter_sort = Option.Some t; body; _ } is the Pi kind or type { x : t } body.

    It is a syntax error to omit the parameter sort. Implicit Pis currently do not have a corresponding syntax, but it may be added in the future.

    *)
  5. | Raw_lambda of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. parameter_identifier : Beluga_syntax.Syncom.Identifier.t Support.Option.t;
    3. parameter_sort : t Support.Option.t;
    4. body : t;
    }
  6. | Raw_arrow of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. domain : t;
    3. range : t;
    4. orientation : [ `Forward | `Backward ];
    }
  7. | Raw_annotated of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. object_ : t;
    3. sort : t;
    }
  8. | Raw_application of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. objects : t Support.List2.t;
    }
    (*

    Raw_application { objects; _ } is the juxtaposition of objects delimited by whitespaces. objects may contain prefix, infix or postfix operators, along with operands. These are rewritten during the disambiguation to the external syntax.

    *)
  9. | Raw_block of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. elements : (Beluga_syntax.Syncom.Identifier.t Support.Option.t * t) Support.List1.t;
    }
  10. | Raw_tuple of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. elements : t Support.List1.t;
    }
  11. | Raw_projection of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. object_ : t;
    3. projection : [ `By_identifier of Beluga_syntax.Syncom.Identifier.t | `By_position of Support.Int.t ];
    }
  12. | Raw_substitution of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. object_ : t;
    3. substitution : Context_object.t;
    }