package coq

  1. Overview
  2. Docs
Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.0.tar.gz
sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3

doc/ltac2_plugin/Ltac2_plugin/Tac2expr/index.html

Module Ltac2_plugin.Tac2expr

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. | CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list
  3. | CPatCnv of raw_patexpr * raw_typexpr

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_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 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. | GTacExt : (_, 'a) Tac2dyn.Arg.tag * 'a -> glb_tacexpr
  14. | 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