package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (5)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.interp/PrimNotations/index.html

Module PrimNotationsSource

Sourcetype rawnum = NumTok.Signed.t

The unique id string below will be used to refer to a particular registered interpreter/uninterpreter of number or string notation. Using the same uid for different (un)interpreters will fail. If at most one interpretation of prim token is used per scope, then the scope name could be used as unique id.

Sourcetype prim_token_uid = private string
Sourcetype 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> Glob_term.glob_constr
Sourcetype 'a prim_token_uninterpreter = Glob_term.any_glob_constr -> 'a option
Sourcetype 'a prim_token_interpretation = 'a prim_token_interpreter * 'a prim_token_uninterpreter
Sourceval register_rawnumeral_interpretation : ?allow_overwrite:bool -> string -> rawnum prim_token_interpretation -> prim_token_uid
Sourceval register_bignumeral_interpretation : ?allow_overwrite:bool -> string -> Z.t prim_token_interpretation -> prim_token_uid
Sourceval register_string_interpretation : ?allow_overwrite:bool -> string -> string prim_token_interpretation -> prim_token_uid

* Number notation

Sourcetype prim_token_notation_error =
  1. | UnexpectedTerm of Constr.t
  2. | UnexpectedNonOptionTerm of Constr.t
Sourceexception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_token_notation_error
Sourcetype numnot_option =
  1. | Nop
  2. | Warning of NumTok.UnsignedNat.t
  3. | Abstract of NumTok.UnsignedNat.t
Sourcetype int_ty = {
  1. dec_uint : Names.inductive;
  2. dec_int : Names.inductive;
  3. hex_uint : Names.inductive;
  4. hex_int : Names.inductive;
  5. uint : Names.inductive;
  6. int : Names.inductive;
}
Sourcetype z_pos_ty = {
  1. z_ty : Names.inductive;
  2. pos_ty : Names.inductive;
}
Sourcetype number_ty = {
  1. int : int_ty;
  2. decimal : Names.inductive;
  3. hexadecimal : Names.inductive;
  4. number : Names.inductive;
}
Sourcetype pos_neg_int63_ty = {
  1. pos_neg_int63_ty : Names.inductive;
}
Sourcetype target_kind =
  1. | Int of int_ty
  2. | UInt of int_ty
  3. | Z of z_pos_ty
  4. | Int63 of pos_neg_int63_ty
  5. | Float64
  6. | Number of number_ty
Sourcetype string_target_kind =
  1. | ListByte
  2. | Byte
  3. | PString
Sourcetype option_kind =
  1. | Direct
  2. | Option
  3. | Error
Sourcetype 'target conversion_kind = 'target * option_kind
Sourcetype to_post_arg =
  1. | ToPostCopy
  2. | ToPostAs of int
  3. | ToPostHole of Names.Id.t
  4. | ToPostCheck of Constr.t

A postprocessing translation to_post can be done after execution of the to_ty interpreter. The reverse translation is performed before the of_ty uninterpreter.

to_post is an array of n lists l_i of tuples (f, t, args). When the head symbol of the translated term matches one of the f in the list l_0 it is replaced by t and its arguments are translated acording to args where ToPostCopy means that the argument is kept unchanged and ToPostAs k means that the argument is recursively translated according to l_k. ToPostHole introduces an additional implicit argument hole (in the reverse translation, the corresponding argument is removed). ToPostCheck r behaves as ToPostCopy except in the reverse translation which fails if the copied term is not r. When n is null, no translation is performed.

Sourcetype ('target, 'warning) prim_token_notation_obj = {
  1. to_kind : 'target conversion_kind;
  2. to_ty : Names.GlobRef.t;
  3. to_post : (Names.GlobRef.t * Names.GlobRef.t * to_post_arg list) list array;
  4. of_kind : 'target conversion_kind;
  5. of_ty : Names.GlobRef.t;
  6. ty_name : Libnames.qualid;
  7. warning : 'warning;
}
Sourcetype string_notation_obj = (string_target_kind, unit) prim_token_notation_obj
Sourcetype prim_token_interp_info =
  1. | Uid of prim_token_uid
  2. | NumberNotation of number_notation_obj
  3. | StringNotation of string_notation_obj
Sourceval do_uninterp : print_float:bool -> prim_token_interp_info -> _ Glob_term.glob_constr_g -> Constrexpr.prim_token option
Sourceval int63_of_pos_bigint : Z.t -> Uint63.t

Conversion from bigint to int63