package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type mutable_flag = bool
type rec_flag = bool
type redef_flag = bool
type lid = Names.Id.t
type uid = Names.Id.t
type ltac_constant = Names.KerName.t
type ltac_alias = Names.KerName.t
type ltac_constructor = Names.KerName.t
type ltac_projection = Names.KerName.t
type type_constant = Names.KerName.t
type tacref =
  1. | TacConstant of ltac_constant
  2. | TacAlias of ltac_alias
type 'a or_relid =
  1. | RelId of Libnames.qualid
  2. | AbsKn of 'a
Misc
type ml_tactic_name = {
  1. mltac_plugin : string;
  2. mltac_tactic : string;
}
type 'a or_tuple =
  1. | Tuple of int
  2. | Other of 'a
Type syntax
type raw_typexpr_r =
  1. | CTypVar of Names.Name.t
  2. | CTypArrow of raw_typexpr * raw_typexpr
  3. | CTypRef of type_constant or_tuple or_relid * raw_typexpr list
and raw_typexpr = raw_typexpr_r CAst.t
type raw_typedef =
  1. | CTydDef of raw_typexpr option
  2. | CTydAlg of (uid * raw_typexpr list) list
  3. | CTydRec of (lid * mutable_flag * raw_typexpr) list
  4. | CTydOpn
type 'a glb_typexpr =
  1. | GTypVar of 'a
  2. | GTypArrow of 'a glb_typexpr * 'a glb_typexpr
  3. | GTypRef of type_constant or_tuple * 'a glb_typexpr list
type glb_alg_type = {
  1. galg_constructors : (uid * int glb_typexpr list) list;
    (*

    Constructors of the algebraic type

    *)
  2. galg_nconst : int;
    (*

    Number of constant constructors

    *)
  3. galg_nnonconst : int;
    (*

    Number of non-constant constructors

    *)
}
type glb_typedef =
  1. | GTydDef of int glb_typexpr option
  2. | GTydAlg of glb_alg_type
  3. | GTydRec of (lid * mutable_flag * int glb_typexpr) list
  4. | GTydOpn
type type_scheme = int * int glb_typexpr
type raw_quant_typedef = Names.lident list * raw_typedef
type glb_quant_typedef = int * glb_typedef
Term syntax
type atom =
  1. | AtmInt of int
  2. | AtmStr of string
type raw_patexpr_r =
  1. | CPatVar of Names.Name.t
  2. | CPatAtm of atom
  3. | CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
  4. | CPatRecord of (ltac_projection or_relid * raw_patexpr) list
  5. | CPatCnv of raw_patexpr * raw_typexpr
  6. | CPatOr of raw_patexpr list
  7. | CPatAs of raw_patexpr * Names.lident

Tactic expressions

and raw_patexpr = raw_patexpr_r CAst.t
type raw_tacexpr_r =
  1. | CTacAtm of atom
  2. | CTacRef of tacref or_relid
  3. | CTacCst of ltac_constructor or_tuple or_relid
  4. | CTacFun of raw_patexpr list * raw_tacexpr
  5. | CTacApp of raw_tacexpr * raw_tacexpr list
  6. | CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr
  7. | CTacCnv of raw_tacexpr * raw_typexpr
  8. | CTacSeq of raw_tacexpr * raw_tacexpr
  9. | CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr
  10. | CTacCse of raw_tacexpr * raw_taccase list
  11. | CTacRec of raw_tacexpr option * raw_recexpr
  12. | CTacPrj of raw_tacexpr * ltac_projection or_relid
  13. | CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr
  14. | CTacExt : ('a, _) Tac2dyn.Arg.tag * 'a -> raw_tacexpr_r
and raw_tacexpr = raw_tacexpr_r CAst.t
and raw_taccase = raw_patexpr * raw_tacexpr
and raw_recexpr = (ltac_projection or_relid * raw_tacexpr) list
type ctor_indx =
  1. | Closed of int
  2. | Open of ltac_constructor
type ctor_data_for_patterns = {
  1. ctyp : type_constant option;
  2. cnargs : int;
  3. cindx : ctor_indx;
}
type glb_pat =
  1. | GPatVar of Names.Name.t
  2. | GPatAtm of atom
  3. | GPatRef of ctor_data_for_patterns * glb_pat list
  4. | GPatOr of glb_pat list
  5. | GPatAs of glb_pat * Names.Id.t
module PartialPat : sig ... end
type case_info = type_constant or_tuple
type 'a open_match = {
  1. opn_match : 'a;
  2. opn_branch : (Names.Name.t * Names.Name.t array * 'a) Names.KNmap.t;
    (*

    Invariant: should not be empty

    *)
  3. opn_default : Names.Name.t * 'a;
}
type glb_tacexpr =
  1. | GTacAtm of atom
  2. | GTacVar of Names.Id.t
  3. | GTacRef of ltac_constant
  4. | GTacFun of Names.Name.t list * glb_tacexpr
  5. | GTacApp of glb_tacexpr * glb_tacexpr list
  6. | GTacLet of rec_flag * (Names.Name.t * glb_tacexpr) list * glb_tacexpr
  7. | GTacCst of case_info * int * glb_tacexpr list
  8. | GTacCse of glb_tacexpr * case_info * glb_tacexpr array * (Names.Name.t array * glb_tacexpr) array
  9. | GTacPrj of type_constant * glb_tacexpr * int
  10. | GTacSet of type_constant * glb_tacexpr * int * glb_tacexpr
  11. | GTacOpn of ltac_constructor * glb_tacexpr list
  12. | GTacWth of glb_tacexpr open_match
  13. | GTacFullMatch of glb_tacexpr * (glb_pat * glb_tacexpr) list
  14. | GTacExt : (_, 'a) Tac2dyn.Arg.tag * 'a -> glb_tacexpr
  15. | GTacPrm of ml_tactic_name * glb_tacexpr list
Parsing & Printing
type exp_level =
  1. | E5
  2. | E4
  3. | E3
  4. | E2
  5. | E1
  6. | E0
type sexpr =
  1. | SexprStr of string CAst.t
  2. | SexprInt of int CAst.t
  3. | SexprRec of Loc.t * Names.Id.t option CAst.t * sexpr list
Toplevel statements
type strexpr =
  1. | StrVal of mutable_flag * rec_flag * (Names.lname * raw_tacexpr) list
    (*

    Term definition

    *)
  2. | StrTyp of rec_flag * (Libnames.qualid * redef_flag * raw_quant_typedef) list
    (*

    Type definition

    *)
  3. | StrPrm of Names.lident * raw_typexpr * ml_tactic_name
    (*

    External definition

    *)
  4. | StrSyn of sexpr list * int option * raw_tacexpr
    (*

    Syntactic extensions

    *)
  5. | StrMut of Libnames.qualid * Names.lident option * raw_tacexpr
    (*

    Redefinition of mutable globals

    *)
Dynamic semantics

Values are represented in a way similar to OCaml, i.e. they contrast immediate integers (integers, constructors without arguments) and structured blocks (tuples, arrays, constructors with arguments), as well as a few other base cases, namely closures, strings, named constructors, and dynamic type coming from the Coq implementation.

type tag = int
type frame =
  1. | FrLtac of ltac_constant
  2. | FrAnon of glb_tacexpr
  3. | FrPrim of ml_tactic_name
  4. | FrExtn : ('a, 'b) Tac2dyn.Arg.tag * 'b -> frame
type backtrace = frame list
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct