Module Synprs

Parser Syntax Definition

The syntax for Beluga signatures after context-free parsing.

OCaml constructor names prefixed with "Raw" require data-dependent disambiguation or reduction during the disambiguation to the external syntax.

Parser LF Syntax

module LF : sig ... end

The intermediate representation of LF kinds, types and terms to delay the handling of data-dependent aspects of the grammar.

Parser Contextual LF Syntax

module CLF : sig ... end

The intermediate representation of contextual LF types, terms and patterns to delay the handling of data-dependent aspects of the grammar.

Parser Meta-Level Syntax

module Meta : sig ... end

The intermediate representation of meta-types, meta-objects and meta-patterns to delay the handling of data-dependent aspects of the grammar.

Parser Computation-Level Syntax

module Comp : sig ... end

The intermediate representation of computation-level kinds, types, expressions and patterns to delay the handling of data-dependent aspects of the grammar.

Parser Harpoon Syntax

module Harpoon : sig ... end

The intermediate representation of Harpoon proof scripts and REPL commands to delay the handling of data-dependent aspects of the grammar.

Parser Signature Syntax

module Signature : sig ... end

The intermediate representation of Beluga signatures to delay the handling of data-dependent aspects of the grammar.

Type Aliases

LF

type lf_object = LF.Object.t

Contextual LF

type clf_object = CLF.Object.t
type clf_context_object = CLF.Context_object.t

Meta-Level

type meta_thing = Meta.Thing.t
type meta_context_object = Meta.Context_object.t
type schema_object = Meta.Schema_object.t

Computation-Level

type comp_sort_object = Comp.Sort_object.t
type comp_expression_object = Comp.Expression_object.t
type comp_pattern_object = Comp.Pattern_object.t
type comp_copattern_object = Comp.Copattern_object.t
type comp_context_object = Comp.Context_object.t

Harpoon

type harpoon_proof = Harpoon.Proof.t
type harpoon_command = Harpoon.Command.t
type harpoon_directive = Harpoon.Directive.t
type harpoon_split_branch = Harpoon.Split_branch.t
type harpoon_split_branch_label = Harpoon.Split_branch.Label.t
type harpoon_suffices_branch = Harpoon.Suffices_branch.t
type harpoon_hypothetical = Harpoon.Hypothetical.t
type harpoon_repl_command = Harpoon.Repl.Command.t

Signature

type signature_pragma = Signature.Pragma.t
type signature_global_pragma = Signature.Global_pragma.t
type signature_totality_declaration = Signature.Totality.Declaration.t
type 'argument signature_totality_order = 'argument Signature.Totality.Order.t
type signature_declaration = Signature.Declaration.t
type signature_entry = Signature.Entry.t
type signature_file = Signature.signature_file
type signature = Signature.t

Common

include module type of struct include Syncom end

Operators

module Associativity = Syncom.Associativity
module Fixity = Syncom.Fixity
module Operator = Syncom.Operator

Annotations

module Depend = Syncom.Depend
module Inductivity = Syncom.Inductivity
module Plicity = Syncom.Plicity

Pretty-Printing

module Parenthesizer = Syncom.Parenthesizer

Identifiers

module Identifier = Syncom.Identifier
module Qualified_identifier = Syncom.Qualified_identifier
module Binding_tree = Syncom.Binding_tree
module Id = Syncom.Id
module HoleId = Syncom.HoleId

Legacy Names

module Name = Syncom.Name
module Gensym = Syncom.Gensym

Utilities

module Error = Syncom.Error
module Position = Syncom.Position
module Location = Syncom.Location

Explicit Arguments

val explicit_arguments_lf_kind : lf_object -> int
val explicit_arguments_lf_typ : lf_object -> int
val explicit_arguments_comp_kind : comp_sort_object -> int
val explicit_arguments_comp_typ : comp_sort_object -> int

Locations

LF

val location_of_lf_object : lf_object -> Beluga_syntax.Location.t
val set_location_of_lf_object : Beluga_syntax.Location.t -> lf_object -> lf_object

Contextual LF

val location_of_clf_object : clf_object -> Beluga_syntax.Location.t
val set_location_of_clf_object : Beluga_syntax.Location.t -> clf_object -> clf_object
val location_of_clf_context_object : clf_context_object -> Beluga_syntax.Location.t

Meta-Level

val location_of_meta_thing : meta_thing -> Beluga_syntax.Location.t
val location_of_schema_object : schema_object -> Beluga_syntax.Location.t
val location_of_meta_context_object : meta_context_object -> Beluga_syntax.Location.t

Computation-Level

val location_of_comp_sort_object : comp_sort_object -> Beluga_syntax.Location.t
val set_location_of_comp_sort_object : Beluga_syntax.Location.t -> comp_sort_object -> comp_sort_object
val location_of_comp_expression_object : comp_expression_object -> Beluga_syntax.Location.t
val set_location_of_comp_expression_object : Beluga_syntax.Location.t -> comp_expression_object -> comp_expression_object
val location_of_comp_pattern_object : comp_pattern_object -> Beluga_syntax.Location.t
val set_location_of_comp_pattern_object : Beluga_syntax.Location.t -> comp_pattern_object -> comp_pattern_object
val location_of_comp_copattern_object : comp_copattern_object -> Beluga_syntax.Location.t
val set_location_of_comp_copattern_object : Beluga_syntax.Location.t -> comp_copattern_object -> comp_copattern_object
val location_of_comp_context_object : comp_context_object -> Beluga_syntax.Location.t

Harpoon

val location_of_harpoon_proof : harpoon_proof -> Beluga_syntax.Location.t
val location_of_harpoon_command : harpoon_command -> Beluga_syntax.Location.t
val location_of_harpoon_directive : harpoon_directive -> Beluga_syntax.Location.t
val location_of_harpoon_split_branch : harpoon_split_branch -> Beluga_syntax.Location.t
val location_of_harpoon_split_branch_label : harpoon_split_branch_label -> Beluga_syntax.Location.t
val location_of_harpoon_suffices_branch : harpoon_suffices_branch -> Beluga_syntax.Location.t
val location_of_harpoon_hypothetical : harpoon_hypothetical -> Beluga_syntax.Location.t
val location_of_harpoon_repl_command : harpoon_repl_command -> Beluga_syntax.Location.t

Signature

val location_of_signature_pragma : signature_pragma -> Beluga_syntax.Location.t
val location_of_signature_global_pragma : signature_global_pragma -> Beluga_syntax.Location.t
val location_of_signature_totality_declaration : signature_totality_declaration -> Beluga_syntax.Location.t
val location_of_signature_totality_order : 'a Synprs__.Synprs_definition.Signature.Totality.Order.t -> Beluga_syntax.Location.t
val location_of_signature_entry : signature_entry -> Beluga_syntax.Location.t
val location_of_signature_declaration : signature_declaration -> Beluga_syntax.Location.t