]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_extraction/miniml.ml
Change Sort.merge (deprecated) with List.merge
[helm.git] / matita / components / ng_extraction / miniml.ml
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 (************************************************************************)
8
9 (*i $Id: miniml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
10
11 (*s Target language for extraction: a core ML called MiniML. *)
12
13 open Coq
14
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
17    object. *)
18
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). *)
22
23 type kill_reason = Ktype | Kother
24
25 type sign = Keep | Kill of kill_reason
26
27
28 (* Convention: outmost lambda/product gives the head of the list. *)
29
30 type signature = sign list
31
32 (*s ML type expressions. *)
33
34 type ml_type =
35   | Tarr    of ml_type * ml_type
36   | Tglob   of NReference.reference * ml_type list
37   | Tvar    of int
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
41   | Tunknown
42   | Taxiom
43
44 and ml_meta = { id : int; mutable contents : ml_type option }
45
46 (* ML type schema.
47    The integer is the number of variable in the schema. *)
48
49 type ml_schema = int * ml_type
50
51 (*s ML inductive types. *)
52
53 type inductive_kind =
54   | Singleton
55   | Coinductive
56   | Standard
57   | Record of NReference.reference list
58
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.
65 *)
66
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;
72   ip_logical : bool;
73   ip_sign : signature;
74   ip_vars : identifier list;
75   ip_types : (ml_type list) array
76 }
77
78 (* [ip_nparams] contains the number of parameters. *)
79
80 type ml_ind = {
81   ind_kind : inductive_kind;
82   ind_nparams : int;
83   ind_packets : ml_ind_packet array;
84 }
85
86 (*s ML terms. *)
87
88 type ml_ident =
89   | Dummy
90   | Id of identifier
91   | Tmp of identifier
92
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"
97 *)
98
99 type constructor_info = {
100   c_kind : inductive_kind;
101   c_typs : ml_type list;
102 }
103
104 type branch_same =
105   | BranchNone
106   | BranchFun of Intset.t
107   | BranchCst of Intset.t
108
109 type match_info = {
110   m_kind : inductive_kind;
111   m_typs : ml_type list;
112   m_same : branch_same
113 }
114
115 type ml_branch = NReference.reference * ml_ident list * ml_ast
116
117 and ml_ast =
118   | MLrel    of int
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
126   | MLexn    of string
127   | MLdummy
128   | MLaxiom
129   | MLmagic  of ml_ast
130
131 (*s ML declarations. *)
132
133 type ml_decl =
134   | Dind  of ml_ind
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
138
139 type ml_spec =
140   | Sind  of ml_ind
141   | Stype of NReference.reference * identifier list * ml_type option
142   | Sval  of NReference.reference * ml_type
143
144 type ml_specif =
145   | Spec of ml_spec
146
147 and ml_module_sig = (label * ml_specif) list
148
149 type ml_structure_elem =
150   | SEdecl of ml_decl
151
152 and ml_module_structure = (label * ml_structure_elem) list
153
154 type ml_structure = module_path * ml_module_structure
155
156 type ml_signature = module_path * ml_module_sig
157
158 type unsafe_needs = {
159   mldummy : bool;
160   tdummy : bool;
161   tunknown : bool;
162   magic : bool
163 }
164
165 type language_descr = {
166   keywords : Idset.t;
167
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;
172
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;
177
178   (* for an isolated declaration print *)
179   pp_decl : ml_decl -> std_ppcmds;
180
181 }