Module Synint.Sgn

type global_prag =
  1. | No_strengthening of {
    1. location : Syncom.Location.t;
    }
  2. | Warn_on_coverage_error of {
    1. location : Syncom.Location.t;
    }
  3. | Initiate_coverage_checking of {
    1. location : Syncom.Location.t;
    }
type prag =
  1. | NamePrag of {
    1. location : Syncom.Location.t;
    2. constant : Syncom.Qualified_identifier.t;
    3. meta_variable_base : Syncom.Identifier.t;
    4. computation_variable_base : Syncom.Identifier.t Support.Option.t;
    }
  2. | NotPrag of {
    1. location : Syncom.Location.t;
    }
  3. | OpenPrag of {
    1. location : Syncom.Location.t;
    2. module_identifier : Syncom.Qualified_identifier.t;
    }
  4. | DefaultAssocPrag of {
    1. location : Syncom.Location.t;
    2. associativity : Syncom.Associativity.t;
    }
  5. | PrefixFixityPrag of {
    1. location : Syncom.Location.t;
    2. constant : Syncom.Qualified_identifier.t;
    3. precedence : Support.Int.t Support.Option.t;
    4. postponed : Stdlib.Bool.t;
    }
  6. | InfixFixityPrag of {
    1. location : Syncom.Location.t;
    2. constant : Syncom.Qualified_identifier.t;
    3. precedence : Support.Int.t Support.Option.t;
    4. associativity : Syncom.Associativity.t Support.Option.t;
    5. postponed : Stdlib.Bool.t;
    }
  7. | PostfixFixityPrag of {
    1. location : Syncom.Location.t;
    2. constant : Syncom.Qualified_identifier.t;
    3. precedence : Support.Int.t Support.Option.t;
    4. postponed : Stdlib.Bool.t;
    }
  8. | AbbrevPrag of {
    1. location : Syncom.Location.t;
    2. module_identifier : Syncom.Qualified_identifier.t;
    3. abbreviation : Syncom.Identifier.t;
    }
    (*

    AbbrevPrag { module_identifier; abbreviation; _ } is the pragma --abbrev module_identifier abbreviation. for defining the alias abbreviation for the module module_identifier.

    *)
  9. | Query of {
    1. location : Syncom.Location.t;
    2. name : Syncom.Identifier.t Support.Option.t;
    3. typ : LF.typ * Syncom.Id.offset;
    4. expected_solutions : Support.Int.t Support.Option.t;
    5. maximum_tries : Support.Int.t Support.Option.t;
    }
    (*

    Logic programming query on LF type

    *)
type positivity_flag =
  1. | Nocheck
  2. | Positivity
  3. | Stratify of Syncom.Location.t * int
  4. | StratifyAll of Syncom.Location.t
type decl =
  1. | Typ of {
    1. location : Syncom.Location.t;
    2. cid : Syncom.Id.cid_typ;
    3. identifier : Syncom.Identifier.t;
    4. kind : LF.kind;
    }
    (*

    LF type family declaration

    *)
  2. | Const of {
    1. location : Syncom.Location.t;
    2. cid : Syncom.Id.cid_term;
    3. identifier : Syncom.Identifier.t;
    4. typ : LF.typ;
    }
    (*

    LF type constant declaration

    *)
  3. | CompTyp of {
    1. location : Syncom.Location.t;
    2. cid : Syncom.Id.cid_comp_typ;
    3. identifier : Syncom.Identifier.t;
    4. kind : Comp.kind;
    5. positivity_flag : positivity_flag;
    }
    (*

    Computation-level data type constant declaration

    *)
  4. | CompCotyp of {
    1. location : Syncom.Location.t;
    2. cid : Syncom.Id.cid_comp_cotyp;
    3. identifier : Syncom.Identifier.t;
    4. kind : Comp.kind;
    }
    (*

    Computation-level codata type constant declaration

    *)
  5. | CompConst of {
    1. location : Syncom.Location.t;
    2. cid : Syncom.Id.cid_comp_const;
    3. identifier : Syncom.Identifier.t;
    4. typ : Comp.typ;
    }
    (*

    Computation-level type constructor declaration

    *)
  6. | CompDest of {
    1. location : Syncom.Location.t;
    2. cid : Syncom.Id.cid_comp_dest;
    3. identifier : Syncom.Identifier.t;
    4. mctx : LF.mctx;
    5. observation_typ : Comp.typ;
    6. return_typ : Comp.typ;
    }
    (*

    Computation-level type destructor declaration

    *)
  7. | CompTypAbbrev of {
    1. location : Syncom.Location.t;
    2. cid : Syncom.Id.cid_comp_typdef;
    3. identifier : Syncom.Identifier.t;
    4. kind : Comp.kind;
    5. typ : Comp.typ;
    }
    (*

    Synonym declaration for computation-level type

    *)
  8. | Schema of {
    1. location : Syncom.Location.t;
    2. cid : Syncom.Id.cid_schema;
    3. identifier : Syncom.Identifier.t;
    4. schema : LF.schema;
    }
    (*

    Declaration of a specification for a set of contexts

    *)
  9. | Val of {
    1. location : Syncom.Location.t;
    2. cid : Syncom.Id.cid_prog;
    3. identifier : Syncom.Identifier.t;
    4. typ : Comp.typ;
    5. expression : Comp.exp;
    6. expression_value : Comp.value option;
    }
    (*

    Computation-level value declaration

    *)
  10. | Recursive_declarations of {
    1. location : Syncom.Location.t;
    2. declarations : decl Support.List1.t;
    }
    (*

    Mutually-recursive declarations

    *)
  11. | Theorem of {
    1. identifier : Syncom.Identifier.t;
    2. cid : Syncom.Id.cid_prog;
    3. typ : Comp.typ;
    4. body : Comp.thm;
    5. location : Syncom.Location.t;
    }
    (*

    Theorem declaration

    *)
  12. | Module of {
    1. location : Syncom.Location.t;
    2. cid : Syncom.Id.module_id;
    3. identifier : Syncom.Identifier.t;
    4. entries : entry list;
    }
    (*

    Namespace declaration for other declarations

    *)

Reconstructed signature element

and entry =
  1. | Pragma of {
    1. location : Syncom.Location.t;
    2. pragma : prag;
    }
  2. | Declaration of {
    1. location : Syncom.Location.t;
    2. declaration : decl;
    }
  3. | Comment of {
    1. location : Syncom.Location.t;
    2. content : Support.String.t;
    }
    (*

    Documentation comment

    *)
type sgn_file = {
  1. location : Syncom.Location.t;
  2. global_pragmas : global_prag list;
  3. entries : entry list;
}

Reconstructed Beluga project