Ltac2_plugin.Tac2expr
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 raw_typexpr_r =
| CTypVar of Names.Name.t |
| CTypArrow of raw_typexpr * raw_typexpr |
| CTypRef of type_constant or_tuple or_relid * raw_typexpr list |
and raw_typexpr = raw_typexpr_r CAst.t
type raw_typedef =
| CTydDef of raw_typexpr option |
| CTydAlg of (uid * raw_typexpr list) list |
| CTydRec of (lid * mutable_flag * raw_typexpr) list |
| CTydOpn |
type 'a glb_typexpr =
| GTypVar of 'a |
| GTypArrow of 'a glb_typexpr * 'a glb_typexpr |
| GTypRef of type_constant or_tuple * 'a glb_typexpr list |
type glb_alg_type = {
galg_constructors : (uid * int glb_typexpr list) list; | (* Constructors of the algebraic type *) |
galg_nconst : int; | (* Number of constant constructors *) |
galg_nnonconst : int; | (* Number of non-constant constructors *) |
}
type glb_typedef =
| GTydDef of int glb_typexpr option |
| GTydAlg of glb_alg_type |
| GTydRec of (lid * mutable_flag * int glb_typexpr) list |
| GTydOpn |
type type_scheme = int * int glb_typexpr
type raw_quant_typedef = Names.lident list * raw_typedef
type glb_quant_typedef = int * glb_typedef
type raw_patexpr_r =
| CPatVar of Names.Name.t |
| CPatAtm of atom |
| CPatRef of ltac_constructor or_tuple or_relid * raw_patexpr list |
| CPatRecord of (ltac_projection or_relid * raw_patexpr) list |
| CPatCnv of raw_patexpr * raw_typexpr |
| CPatOr of raw_patexpr list |
| CPatAs of raw_patexpr * Names.lident |
Tactic expressions
and raw_patexpr = raw_patexpr_r CAst.t
type raw_tacexpr_r =
| CTacAtm of atom |
| CTacRef of tacref or_relid |
| CTacCst of ltac_constructor or_tuple or_relid |
| CTacFun of raw_patexpr list * raw_tacexpr |
| CTacApp of raw_tacexpr * raw_tacexpr list |
| CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr |
| CTacCnv of raw_tacexpr * raw_typexpr |
| CTacSeq of raw_tacexpr * raw_tacexpr |
| CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr |
| CTacCse of raw_tacexpr * raw_taccase list |
| CTacRec of raw_tacexpr option * raw_recexpr |
| CTacPrj of raw_tacexpr * ltac_projection or_relid |
| CTacSet of raw_tacexpr * ltac_projection or_relid * raw_tacexpr |
| 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 glb_pat =
| GPatVar of Names.Name.t |
| GPatAtm of atom |
| GPatRef of ctor_data_for_patterns * glb_pat list |
| GPatOr of glb_pat list |
| GPatAs of glb_pat * Names.Id.t |
module PartialPat : sig ... end
type case_info = type_constant or_tuple
type 'a open_match = {
opn_match : 'a; | |
opn_branch : (Names.Name.t * Names.Name.t array * 'a) Names.KNmap.t; | (* Invariant: should not be empty *) |
opn_default : Names.Name.t * 'a; |
}
type glb_tacexpr =
| GTacAtm of atom |
| GTacVar of Names.Id.t |
| GTacRef of ltac_constant |
| GTacFun of Names.Name.t list * glb_tacexpr |
| GTacApp of glb_tacexpr * glb_tacexpr list |
| GTacLet of rec_flag * (Names.Name.t * glb_tacexpr) list * glb_tacexpr |
| GTacCst of case_info * int * glb_tacexpr list |
| GTacCse of glb_tacexpr * case_info * glb_tacexpr array * (Names.Name.t array * glb_tacexpr) array |
| GTacPrj of type_constant * glb_tacexpr * int |
| GTacSet of type_constant * glb_tacexpr * int * glb_tacexpr |
| GTacOpn of ltac_constructor * glb_tacexpr list |
| GTacWth of glb_tacexpr open_match |
| GTacFullMatch of glb_tacexpr * (glb_pat * glb_tacexpr) list |
| GTacExt : (_, 'a) Tac2dyn.Arg.tag * 'a -> glb_tacexpr |
| GTacPrm of ml_tactic_name * glb_tacexpr list |
type strexpr =
| StrVal of mutable_flag * rec_flag * (Names.lname * raw_tacexpr) list | (* Term definition *) |
| StrTyp of rec_flag * (Libnames.qualid * redef_flag * raw_quant_typedef) list | (* Type definition *) |
| StrPrm of Names.lident * raw_typexpr * ml_tactic_name | (* External definition *) |
| StrSyn of sexpr list * int option * raw_tacexpr | (* Syntactic extensions *) |
| StrMut of Libnames.qualid * Names.lident option * raw_tacexpr | (* Redefinition of mutable globals *) |
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 frame =
| FrLtac of ltac_constant |
| FrAnon of glb_tacexpr |
| FrPrim of ml_tactic_name |
| FrExtn : ('a, 'b) Tac2dyn.Arg.tag * 'b -> frame |
type backtrace = frame list