diff options
Diffstat (limited to 'plugins/extraction/miniml.mli')
| -rw-r--r-- | plugins/extraction/miniml.mli | 47 |
1 files changed, 27 insertions, 20 deletions
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index fbb1c116..1e491d36 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,9 +9,8 @@ (*s Target language for extraction: a core ML called MiniML. *) open Pp -open Util open Names -open Libnames +open Globnames (* The [signature] type is used to know how many arguments a CIC object expects, and what these arguments will become in the ML @@ -66,11 +65,11 @@ type inductive_kind = *) type ml_ind_packet = { - ip_typename : identifier; - ip_consnames : identifier array; + ip_typename : Id.t; + ip_consnames : Id.t array; ip_logical : bool; ip_sign : signature; - ip_vars : identifier list; + ip_vars : Id.t list; ip_types : (ml_type list) array } @@ -92,8 +91,8 @@ type ml_ind = { type ml_ident = | Dummy - | Id of identifier - | Tmp of identifier + | Id of Id.t + | Tmp of Id.t (** We now store some typing information on constructors and cases to avoid type-unsafe optimisations. This will be @@ -117,7 +116,7 @@ and ml_ast = | MLcons of ml_type * global_reference * ml_ast list | MLtuple of ml_ast list | MLcase of ml_type * ml_ast * ml_branch array - | MLfix of int * identifier array * ml_ast array + | MLfix of int * Id.t array * ml_ast array | MLexn of string | MLdummy | MLaxiom @@ -134,13 +133,13 @@ and ml_pattern = type ml_decl = | Dind of mutual_inductive * ml_ind - | Dtype of global_reference * identifier list * ml_type + | Dtype of global_reference * Id.t list * ml_type | Dterm of global_reference * ml_ast * ml_type | Dfix of global_reference array * ml_ast array * ml_type array type ml_spec = | Sind of mutual_inductive * ml_ind - | Stype of global_reference * identifier list * ml_type option + | Stype of global_reference * Id.t list * ml_type option | Sval of global_reference * ml_type type ml_specif = @@ -150,15 +149,15 @@ type ml_specif = and ml_module_type = | MTident of module_path - | MTfunsig of mod_bound_id * ml_module_type * ml_module_type + | MTfunsig of MBId.t * ml_module_type * ml_module_type | MTsig of module_path * ml_module_sig | MTwith of ml_module_type * ml_with_declaration and ml_with_declaration = - | ML_With_type of identifier list * identifier list * ml_type - | ML_With_module of identifier list * module_path + | ML_With_type of Id.t list * Id.t list * ml_type + | ML_With_module of Id.t list * module_path -and ml_module_sig = (label * ml_specif) list +and ml_module_sig = (Label.t * ml_specif) list type ml_structure_elem = | SEdecl of ml_decl @@ -167,11 +166,11 @@ type ml_structure_elem = and ml_module_expr = | MEident of module_path - | MEfunctor of mod_bound_id * ml_module_type * ml_module_expr + | MEfunctor of MBId.t * ml_module_type * ml_module_expr | MEstruct of module_path * ml_module_structure | MEapply of ml_module_expr * ml_module_expr -and ml_module_structure = (label * ml_structure_elem) list +and ml_module_structure = (Label.t * ml_structure_elem) list and ml_module = { ml_mod_expr : ml_module_expr; @@ -184,6 +183,8 @@ type ml_structure = (module_path * ml_module_structure) list type ml_signature = (module_path * ml_module_sig) list +type ml_flat_structure = ml_structure_elem list + type unsafe_needs = { mldummy : bool; tdummy : bool; @@ -192,16 +193,22 @@ type unsafe_needs = { } type language_descr = { - keywords : Idset.t; + keywords : Id.Set.t; (* Concerning the source file *) file_suffix : string; - preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; + (* the second argument is a comment to add to the preamble *) + preamble : + Id.t -> std_ppcmds option -> module_path list -> unsafe_needs -> + std_ppcmds; pp_struct : ml_structure -> std_ppcmds; (* Concerning a possible interface file *) sig_suffix : string option; - sig_preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; + (* the second argument is a comment to add to the preamble *) + sig_preamble : + Id.t -> std_ppcmds option -> module_path list -> unsafe_needs -> + std_ppcmds; pp_sig : ml_signature -> std_ppcmds; (* for an isolated declaration print *) |