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: table.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
15 TypeInfo of NReference.reference * ml_schema
16 | TermInfo of NReference.reference * ml_decl
17 | InductiveInfo of NUri.uri * ml_ind
18 | GuessProjectionInfo of NUri.uri * int
19 | ConfirmProjectionInfo of NReference.reference
20 | RegisterId of string
21 | ReferenceNameInfo of NReference.reference * string
22 | RegisterModname of string
23 | ModnameInfo of string * string
25 type info = info_el list
30 ml_ind NUri.UriMap.t *
35 ((out_channel * Format.formatter) * (out_channel * Format.formatter)) option *
42 let set_keywords,get_keywords =
43 let keywords = ref Idset.empty in
44 ((:=) keywords),(fun () -> !keywords)
46 let preamble = "preamble.ml"
47 let upreamble = "Preamble"
49 let empty_modset = Idset.add preamble Idset.empty
51 Refmap.empty,Refmap.empty,NUri.UriMap.empty,NUri.UriMap.empty,Refmap.empty,get_keywords (),Refmap.empty,None,empty_modset,Stringmap.empty,Uriset.empty,"",empty_info
53 let register_info (dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos) info =
55 TypeInfo (ref,schema) ->
56 Refmap.add ref schema dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
57 | TermInfo (ref,schema) ->
58 dbty,Refmap.add ref schema dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
59 | InductiveInfo (uri,ind) ->
60 dbty,dbt,NUri.UriMap.add uri ind dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
61 | GuessProjectionInfo (uri,n) ->
62 dbty,dbt,dbi,NUri.UriMap.add uri n dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
63 | ConfirmProjectionInfo (NReference.Ref (uri,_) as ref) ->
65 let n = NUri.UriMap.find uri dbgp in
66 let dbgp = NUri.UriMap.remove uri dbgp in
67 dbty,dbt,dbi,dbgp,Refmap.add ref n dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
68 with Not_found -> dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos)
70 dbty,dbt,dbi,dbgp,dbp,Idset.add s dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
71 | ReferenceNameInfo (ref,name) ->
72 dbty,dbt,dbi,dbgp,dbp,dbids,Refmap.add ref name dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
73 | RegisterModname s ->
74 dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,Idset.add s dbmn1,dbmn2,dbo,curi,infos
75 | ModnameInfo (s,name) ->
76 dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,Stringmap.add s name dbmn2,dbo,curi,infos
78 let add_info_to_db (dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos) info =
79 dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,info::infos
81 let register_and_add_info ?(dummy=false) status info =
82 let db = status#ocaml_extraction_db in
83 let db = register_info db info in
84 let db = if dummy then db else add_info_to_db db info in
85 status#set_ocaml_extraction_db db
87 let register_infos = List.fold_left register_info
89 let refresh_uri_in_type ~refresh_uri_in_reference =
92 | Tarr (t1,t2) -> Tarr (aux t1, aux t2)
93 | Tglob (r,tl) -> Tglob (refresh_uri_in_reference r, List.map aux tl)
94 | Tmeta { id=id; contents=contents } ->
98 | Some typ -> Some (aux typ)
100 Tmeta { id=id; contents=contents' }
105 let refresh_uri_in_kind ~refresh_uri_in_reference =
110 | Record rl -> Record (List.map refresh_uri_in_reference rl)
112 let refresh_uri_in_packet ~refresh_uri_in_reference
114 ip_consreferences = rs;
121 { ip_reference = refresh_uri_in_reference r;
122 ip_consreferences = Array.map refresh_uri_in_reference rs;
128 ip_types = Array.map (List.map (refresh_uri_in_type ~refresh_uri_in_reference)) tys }
130 let refresh_uri_in_ind ~refresh_uri_in_reference
131 {ind_kind=k; ind_nparams=n; ind_packets=pa}
133 let k = refresh_uri_in_kind ~refresh_uri_in_reference k in
134 let pa = Array.map (refresh_uri_in_packet ~refresh_uri_in_reference) pa in
135 {ind_kind=k; ind_nparams=n; ind_packets=pa}
137 let refresh_uri_in_ast ~refresh_uri_in_reference =
140 | MLapp (t,tl) -> MLapp (aux t, List.map aux tl)
141 | MLlam (id,t) -> MLlam (id, aux t)
142 | MLletin (id,t1,t2) -> MLletin (id, aux t1, aux t2)
143 | MLglob r -> MLglob (refresh_uri_in_reference r)
144 | MLcons ({c_kind=ckind; c_typs=ctyps}, r, tl) ->
146 {c_kind=refresh_uri_in_kind ~refresh_uri_in_reference ckind;
147 c_typs=List.map (refresh_uri_in_type ~refresh_uri_in_reference) ctyps}
149 MLcons (cinfo, refresh_uri_in_reference r, List.map aux tl)
150 | MLcase ({m_kind=k; m_typs=typs; m_same=same},t,ba) ->
152 {m_kind=refresh_uri_in_kind ~refresh_uri_in_reference k;
153 m_typs=List.map (refresh_uri_in_type ~refresh_uri_in_reference) typs;
157 (fun (r,il,t) -> refresh_uri_in_reference r,il,aux t) ba in
158 MLcase (info,aux t,ba)
159 | MLfix (n,ida,ta) -> MLfix (n,ida,Array.map aux ta)
160 | MLmagic t -> MLmagic (aux t)
168 let refresh_uri_in_decl ~refresh_uri_in_reference =
170 Dind ind -> Dind (refresh_uri_in_ind ~refresh_uri_in_reference ind)
171 | Dtype (ref,il,ty) ->
173 (refresh_uri_in_reference ref, il,
174 refresh_uri_in_type ~refresh_uri_in_reference ty)
175 | Dterm (ref,ast,ty) ->
177 (refresh_uri_in_reference ref,
178 refresh_uri_in_ast ~refresh_uri_in_reference ast,
179 refresh_uri_in_type ~refresh_uri_in_reference ty)
180 | Dfix (refa, asta, tya) ->
182 (Array.map refresh_uri_in_reference refa,
183 Array.map (refresh_uri_in_ast ~refresh_uri_in_reference) asta,
184 Array.map (refresh_uri_in_type ~refresh_uri_in_reference) tya)
186 let refresh_uri_in_info_el ~refresh_uri_in_reference ~refresh_uri =
188 TypeInfo (ref,(n,typ)) ->
190 (refresh_uri_in_reference ref,
191 (n,refresh_uri_in_type ~refresh_uri_in_reference typ))
192 | TermInfo (ref,decl) ->
194 (refresh_uri_in_reference ref,
195 refresh_uri_in_decl ~refresh_uri_in_reference decl)
196 | InductiveInfo (uri,ind) ->
198 (refresh_uri uri, refresh_uri_in_ind ~refresh_uri_in_reference ind)
199 | GuessProjectionInfo (uri,n) ->
200 GuessProjectionInfo (refresh_uri uri, n)
201 | ConfirmProjectionInfo ref ->
202 ConfirmProjectionInfo (refresh_uri_in_reference ref)
203 | RegisterId s -> RegisterId s
204 | ReferenceNameInfo (ref,name) ->
205 ReferenceNameInfo (refresh_uri_in_reference ref,name)
206 | RegisterModname s -> RegisterModname s
207 | ModnameInfo (s,name) -> ModnameInfo (s,name)
209 let refresh_uri_in_info ~refresh_uri_in_reference ~refresh_uri infos =
211 (refresh_uri_in_info_el ~refresh_uri_in_reference ~refresh_uri)
214 class type g_status =
216 method ocaml_extraction_db: db
217 method get_info: info * 'self
220 class virtual status =
223 val ocaml_extraction_db = empty_db ()
224 method ocaml_extraction_db = ocaml_extraction_db
226 let db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos = self#ocaml_extraction_db in
227 infos,{< ocaml_extraction_db =
228 db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,empty_info >}
229 method set_ocaml_extraction_db v = {< ocaml_extraction_db = v >}
230 method set_ocaml_extraction_status
231 : 'status. #g_status as 'status -> 'self
232 = fun o -> {< ocaml_extraction_db = o#ocaml_extraction_db >}
235 let open_file status ~baseuri filename =
236 let db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,_,infos = status#ocaml_extraction_db in
238 let chml = open_out filename in
239 let chml = chml,Format.formatter_of_out_channel chml in
240 let chmli = open_out (filename ^ "i") in
241 let chmli = chmli,Format.formatter_of_out_channel chmli in
242 pp_with (snd chml) (str ("open " ^ upreamble ^ "\n") ++ fnl ());
243 pp_with (snd chmli) (str ("open " ^ upreamble ^ "\n") ++ fnl ());
244 let db = db1,db2,dbi,dbgp,dbp,dbids,dbrefs,Some (chml,chmli),dbmn1,dbmn2,dbo,baseuri,infos in
245 status#set_ocaml_extraction_db db
247 let close_file status =
248 let db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos = status#ocaml_extraction_db in
252 Format.pp_print_flush (snd (fst ch)) ();
253 Format.pp_print_flush (snd (snd ch)) ();
254 close_out (fst (fst ch));
255 close_out (fst (snd ch));
257 let db = db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos in
258 status#set_ocaml_extraction_db db
260 let print_ppcmds status ~in_ml cmds =
261 let _,_,_,_,_,_,_,ch,_,_,_,_,_ = status#ocaml_extraction_db in
265 let ch = if in_ml then fst ch else snd ch in
266 pp_with (snd ch) cmds
268 let to_be_included status uri =
269 let dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos =
270 status#ocaml_extraction_db
272 if Uriset.mem uri dbo then
275 let dbo = Uriset.add uri dbo in
277 status#set_ocaml_extraction_db
278 (dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos) in
281 let add_term status ref decl =
282 let info = TermInfo (ref,decl) in
283 register_and_add_info status info
285 let lookup_term status ref =
286 let _,dbt,_,_,_,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
289 let add_type status ref schema =
290 let info = TypeInfo (ref,schema) in
291 register_and_add_info status info
293 let lookup_type status ref =
294 let dbty,_,_,_,_,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
297 let add_name_for_reference status ref name =
298 let info = ReferenceNameInfo (ref,name) in
299 register_and_add_info status info
301 let name_of_reference status ref =
302 let _,_,_,_,_,_,dbrefs,_,_,_,_,_,_ = status#ocaml_extraction_db in
303 Refmap.find ref dbrefs
305 let add_modname_for_filename status ref name =
306 let info = ModnameInfo (ref,name) in
307 register_and_add_info status info
309 let modname_of_filename status ref =
310 let _,_,_,_,_,_,_,_,_,dbmn2,_,_,_ = status#ocaml_extraction_db in
311 Stringmap.find ref dbmn2
313 let add_global_ids status id =
314 let info = RegisterId id in
315 register_and_add_info status info
317 let get_global_ids status =
318 let _,_,_,_,_,dbids,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
321 let add_modname status id =
322 let info = RegisterModname id in
323 register_and_add_info status info
325 let get_modnames status =
326 let _,_,_,_,_,_,_,_,dbmn1,_,_,_,_ = status#ocaml_extraction_db in
329 let add_ind status ?dummy uri ind =
330 let info = InductiveInfo (uri,ind) in
331 register_and_add_info ?dummy status info
333 let lookup_ind status uri =
334 let _,_,dbi,_,_,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
335 NUri.UriMap.find uri dbi
337 let current_baseuri status =
338 let _,_,_,_,_,_,_,_,_,_,_,suri,_ = status#ocaml_extraction_db in suri
340 let guess_projection status ref n =
341 let info = GuessProjectionInfo (ref,n) in
342 register_and_add_info status info
344 let confirm_projection status ref =
345 let info = ConfirmProjectionInfo ref in
346 register_and_add_info status info
348 let is_projection status ref =
349 let _,_,_,_,dbp,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
352 let projection_arity status ref =
353 let _,_,_,_,dbp,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
356 let type_expand () = true
358 (*s Extraction Optimize *)
361 { opt_kill_dum : bool; (* 1 *)
362 opt_fix_fun : bool; (* 2 *)
363 opt_case_iot : bool; (* 4 *)
364 opt_case_idr : bool; (* 8 *)
365 opt_case_idg : bool; (* 16 *)
366 opt_case_cst : bool; (* 32 *)
367 opt_case_fun : bool; (* 64 *)
368 opt_case_app : bool; (* 128 *)
369 opt_let_app : bool; (* 256 *)
370 opt_lin_let : bool; (* 512 *)
371 opt_lin_beta : bool } (* 1024 *)
373 let kth_digit n k = (n land (1 lsl k) <> 0)
376 { opt_kill_dum = kth_digit n 0;
377 opt_fix_fun = kth_digit n 1;
378 opt_case_iot = kth_digit n 2;
379 opt_case_idr = kth_digit n 3;
380 opt_case_idg = kth_digit n 4;
381 opt_case_cst = kth_digit n 5;
382 opt_case_fun = kth_digit n 6;
383 opt_case_app = kth_digit n 7;
384 opt_let_app = kth_digit n 8;
385 opt_lin_let = kth_digit n 9;
386 opt_lin_beta = kth_digit n 10 }
388 (* For the moment, we allow by default everything except :
389 - the type-unsafe optimization [opt_case_idg], which anyway
390 cannot be activated currently (cf [Mlutil.branch_as_fun])
391 - the linear let and beta reduction [opt_lin_let] and [opt_lin_beta]
392 (may lead to complexity blow-up, subsumed by finer reductions
393 when inlining recursors).
396 let int_flag_init = 1 + 2 + 4 + 8 (*+ 16*) + 32 + 64 + 128 + 256 (*+ 512 + 1024*)
398 let opt_flag_ref = ref (flag_of_int int_flag_init)
400 let optims () = !opt_flag_ref