1 (************************************************************************)
2 (* v * The Coq Proof Assistant / The Coq Development Team *)
3 (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
4 (* \VV/ **************************************************************)
5 (* // * This file is distributed under the terms of the *)
6 (* * GNU Lesser General Public License Version 2.1 *)
7 (************************************************************************)
9 (*i $Id: miniml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
11 (*s Target language for extraction: a core ML called MiniML. *)
15 (* The [signature] type is used to know how many arguments a CIC
16 object expects, and what these arguments will become in the ML
19 (* We eliminate from terms: 1) types 2) logical parts.
20 [Kother] stands both for logical or other reasons
21 (for instance user-declared implicit arguments w.r.t. extraction). *)
23 type kill_reason = Ktype | Kother
25 type sign = Keep | Kill of kill_reason
28 (* Convention: outmost lambda/product gives the head of the list. *)
30 type signature = sign list
32 (*s ML type expressions. *)
35 | Tarr of ml_type * ml_type
36 | Tglob of NReference.reference * ml_type list
38 | Tvar' of int (* same as Tvar, used to avoid clash *)
39 | Tmeta of ml_meta (* used during ML type reconstruction *)
40 | Tdummy of kill_reason
44 and ml_meta = { id : int; mutable contents : ml_type option }
47 The integer is the number of variable in the schema. *)
49 type ml_schema = int * ml_type
51 (*s ML inductive types. *)
57 | Record of NReference.reference list
59 (* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
60 If the inductive is logical ([ip_logical = false]), then all other fields
61 are unused. Otherwise,
62 [ip_sign] is a signature concerning the arguments of the inductive,
63 [ip_vars] contains the names of the type variables surviving in ML,
64 [ip_types] contains the ML types of all constructors.
67 type ml_ind_packet = {
68 ip_reference : NReference.reference;
69 ip_consreferences : NReference.reference array;
70 ip_typename : identifier;
71 ip_consnames : identifier array;
74 ip_vars : identifier list;
75 ip_types : (ml_type list) array
78 (* [ip_nparams] contains the number of parameters. *)
81 ind_kind : inductive_kind;
83 ind_packets : ml_ind_packet array;
93 (** We now store some typing information on constructors
94 and cases to avoid type-unsafe optimisations.
95 For cases, we also store the set of branches to merge
96 in a common pattern, either "_ -> c" or "x -> f x"
99 type constructor_info = {
100 c_kind : inductive_kind;
101 c_typs : ml_type list;
106 | BranchFun of Intset.t
107 | BranchCst of Intset.t
110 m_kind : inductive_kind;
111 m_typs : ml_type list;
115 type ml_branch = NReference.reference * ml_ident list * ml_ast
119 | MLapp of ml_ast * ml_ast list
120 | MLlam of ml_ident * ml_ast
121 | MLletin of ml_ident * ml_ast * ml_ast
122 | MLglob of NReference.reference
123 | MLcons of constructor_info * NReference.reference * ml_ast list
124 | MLcase of match_info * ml_ast * ml_branch array
125 | MLfix of int * identifier array * ml_ast array
131 (*s ML declarations. *)
135 | Dtype of NReference.reference * identifier list * ml_type
136 | Dterm of NReference.reference * ml_ast * ml_type
137 | Dfix of NReference.reference array * ml_ast array * ml_type array
141 | Stype of NReference.reference * identifier list * ml_type option
142 | Sval of NReference.reference * ml_type
147 and ml_module_sig = (label * ml_specif) list
149 type ml_structure_elem =
152 and ml_module_structure = (label * ml_structure_elem) list
154 type ml_structure = module_path * ml_module_structure
156 type ml_signature = module_path * ml_module_sig
158 type unsafe_needs = {
165 type language_descr = {
168 (* Concerning the source file *)
169 file_suffix : string;
170 preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
171 pp_struct : ml_structure -> std_ppcmds;
173 (* Concerning a possible interface file *)
174 sig_suffix : string option;
175 sig_preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
176 pp_sig : ml_signature -> std_ppcmds;
178 (* for an isolated declaration print *)
179 pp_decl : ml_decl -> std_ppcmds;