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_notation = Names.KerName.t

type ltac_constructor = Names.KerName.t

type ltac_projection = Names.KerName.t

type type_constant = Names.KerName.t

type tacref =

| TacConstant of ltac_constant
| TacAlias of ltac_alias

type 'a or_relid =

| RelId of Libnames.qualid
| AbsKn of 'a

Misc

type ml_tactic_name = {

mltac_plugin : string;
mltac_tactic : string;

}

type 'a or_tuple =

| Tuple of int
| Other of 'a

Type syntax

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

Term syntax

type atom =

| AtmInt of int
| AtmStr of string

type ctor_indx =

| Closed of int
| Open of ltac_constructor

type ctor_data_for_patterns = {

ctyp : type_constant option;
cnargs : int;
cindx : ctor_indx;

}

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

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
| CTacSyn of (Names.lname * raw_tacexpr) list * Names.KerName.t
| 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
| CTacGlb of int * (Names.lname * raw_tacexpr * int glb_typexpr option) list * glb_tacexpr * int glb_typexpr
(*
CTacGlb is essentially an expanded typed notation. Arguments bound with Anonymous have no type constraint.
*)

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

Parsing & Printing

type exp_level =

| E5
| E4
| E3
| E2
| E1
| E0

type sexpr =

| SexprStr of string CAst.t
| SexprInt of int CAst.t
| SexprRec of Loc.t * Names.Id.t option CAst.t * sexpr list

Toplevel statements

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
*)
| StrMut of Libnames.qualid * Names.lident option * raw_tacexpr
(*
Redefinition of mutable globals
*)

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2expr/index.html

Module `Ltac2_plugin.Tac2expr`

Misc

Type syntax

Term syntax

Parsing & Printing

Toplevel statements

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2expr/index.html

Module Ltac2_plugin.Tac2expr

Misc

Type syntax

Term syntax

Parsing & Printing

Toplevel statements

Module `Ltac2_plugin.Tac2expr`