Module Meta.Thing

Meta-objects, meta-types, meta-patterns.

type t =
  1. | RawSchema of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. schema : Beluga_syntax.Syncom.Qualified_identifier.t;
    }
    (*

    RawSchema { schema; _ } is the context schema schema.

    *)
  2. | RawContext of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. context : Synprs__.Synprs_definition.CLF.Context_object.t;
    }
    (*

    RawPlain { context; _ } is the boxed contextual LF context [context].

    *)
  3. | RawTurnstile of {
    1. location : Beluga_syntax.Syncom.Location.t;
    2. context : Synprs__.Synprs_definition.CLF.Context_object.t;
    3. object_ : Synprs__.Synprs_definition.CLF.Context_object.t;
    4. variant : [ `Plain | `Hash | `Dollar | `Dollar_hash ];
    }
    (*
    • RawTurnstile { context; variant = `Plain; object_; _ } is the meta-thing [context |- object_] or (context |- object_).
    • RawTurnstile { context; variant = `Hash; object_; _ } is the meta-thing #[context |- object_] or #(context |- object_).
    • RawTurnstile { context; variant = `Dollar; object_; _ } is the meta-thing $[context |- object_] or $(context |- object_).
    • RawTurnstile { context; variant = `Dollar_hash; object_; _ } is the meta-thing $[context |-# object_] or $(context |-# object_).
    *)