Module LF.Object

LF kinds, types and terms blurred together.

type t =
  1. | Raw_identifier of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. identifier : Beluga_syntax.Syncom.Identifier.t;
    3. prefixed : Stdlib.Bool.t;
    }
    (*
    • 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.

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

    *)
  3. | Raw_type of {
    1. location : Beluga_syntax.Syncom.Location.t;
    }
  4. | Raw_hole of {
    1. location : Beluga_syntax.Syncom.Location.t;
    }
  5. | 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.

    *)
  6. | 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;
    }
  7. | Raw_arrow of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. domain : t;
    3. range : t;
    4. orientation : [ `Forward | `Backward ];
    }
  8. | Raw_annotated of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. object_ : t;
    3. sort : t;
    }
  9. | 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.

    *)