package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
doc/extraction_plugin/Extraction_plugin/Miniml/index.html
Module Extraction_plugin.MinimlSource
Source
type ml_type = | Tarr of ml_type * ml_type| Tglob of Names.GlobRef.t * ml_type list| Tvar of int| Tvar' of int| Tmeta of ml_meta| Tdummy of kill_reason| Tunknown| Taxiom
Source
type inductive_kind = | Singleton| Coinductive| Standard| Record of Names.GlobRef.t option list
Source
type ml_ind_packet = {ip_typename : Names.Id.t;ip_consnames : Names.Id.t array;ip_logical : bool;ip_sign : signature;ip_vars : Names.Id.t list;ip_types : ml_type list array;
}Source
type ml_ind = {ind_kind : inductive_kind;ind_nparams : int;ind_packets : ml_ind_packet array;ind_equiv : equiv;
}We now store some typing information on constructors and cases to avoid type-unsafe optimisations. This will be either the type of the applied constructor or the type of the head of the match.
Nota : the constructor MLtuple and the extension of MLcase to general patterns have been proposed by P.N. Tollitte for his Relation Extraction plugin. MLtuple is currently not used by the main extraction, as well as deep patterns.
Source
and ml_ast = | MLrel of int| MLapp of ml_ast * ml_ast list| MLlam of ml_ident * ml_ast| MLletin of ml_ident * ml_ast * ml_ast| MLglob of Names.GlobRef.t| MLcons of ml_type * Names.GlobRef.t * ml_ast list| MLtuple of ml_ast list| MLcase of ml_type * ml_ast * ml_branch array| MLfix of int * Names.Id.t array * ml_ast array| MLexn of string| MLdummy of kill_reason| MLaxiom| MLmagic of ml_ast| MLuint of Uint63.t| MLfloat of Float64.t| MLparray of ml_ast array * ml_ast
Source
and ml_pattern = | Pcons of Names.GlobRef.t * ml_pattern list| Ptuple of ml_pattern list| Prel of int(*Cf. the idents in the branch.
*)Prel 1is the last one.| Pwild| Pusual of Names.GlobRef.t(*Shortcut for Pcons (r,
*)Prel n;...;Prel 1) *
Source
type ml_decl = | Dind of Names.MutInd.t * ml_ind| Dtype of Names.GlobRef.t * Names.Id.t list * ml_type| Dterm of Names.GlobRef.t * ml_ast * ml_type| Dfix of Names.GlobRef.t array * ml_ast array * ml_type array
Source
type ml_spec = | Sind of Names.MutInd.t * ml_ind| Stype of Names.GlobRef.t * Names.Id.t list * ml_type option| Sval of Names.GlobRef.t * ml_type
Source
and ml_module_type = | MTident of Names.ModPath.t| MTfunsig of Names.MBId.t * ml_module_type * ml_module_type| MTsig of Names.ModPath.t * ml_module_sig| MTwith of ml_module_type * ml_with_declaration
Source
and ml_with_declaration = | ML_With_type of Names.Id.t list * Names.Id.t list * ml_type| ML_With_module of Names.Id.t list * Names.ModPath.t
Source
type ml_structure_elem = | SEdecl of ml_decl| SEmodule of ml_module| SEmodtype of ml_module_type
Source
and ml_module_expr = | MEident of Names.ModPath.t| MEfunctor of Names.MBId.t * ml_module_type * ml_module_expr| MEstruct of Names.ModPath.t * ml_module_structure| MEapply of ml_module_expr * ml_module_expr
Source
type language_descr = {keywords : Names.Id.Set.t;file_suffix : string;file_naming : Names.ModPath.t -> string;preamble : Names.Id.t -> Pp.t option -> Names.ModPath.t list -> unsafe_needs -> Pp.t;pp_struct : ml_structure -> Pp.t;sig_suffix : string option;sig_preamble : Names.Id.t -> Pp.t option -> Names.ModPath.t list -> unsafe_needs -> Pp.t;pp_sig : ml_signature -> Pp.t;pp_decl : ml_decl -> Pp.t;
}