summaryrefslogtreecommitdiff
path: root/contrib/extraction/table.ml
blob: 6d39faee30ef156ac1c63853d4ac3c32f241a5db (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id: table.ml 10209 2007-10-09 21:49:37Z letouzey $ i*)

open Names
open Term
open Declarations
open Nameops
open Summary
open Libobject
open Goptions
open Libnames
open Util
open Pp
open Miniml

(*S Utilities concerning [module_path] and [kernel_names] *)

let occur_kn_in_ref kn =
 function
  | IndRef (kn',_)
  | ConstructRef ((kn',_),_) -> kn = kn'
  | ConstRef _ -> false
  | VarRef _ -> assert false

let modpath_of_r r = match r with 
    | ConstRef kn -> con_modpath kn
    | IndRef (kn,_)
    | ConstructRef ((kn,_),_) -> modpath kn
    | VarRef _ -> assert false

let label_of_r r = match r with 
    | ConstRef kn -> con_label kn
    | IndRef (kn,_)
    | ConstructRef ((kn,_),_) -> label kn
    | VarRef _ -> assert false

let current_toplevel () = fst (Lib.current_prefix ())

let rec base_mp = function 
  | MPdot (mp,l) -> base_mp mp 
  | mp -> mp 

let is_modfile = function 
  | MPfile _ -> true 
  | _ -> false

let is_toplevel mp = 
  mp = initial_path || mp = current_toplevel ()

let at_toplevel mp = 
  is_modfile mp || is_toplevel mp

let visible_kn kn = at_toplevel (base_mp (modpath kn))
let visible_con kn = at_toplevel (base_mp (con_modpath kn))

(*S The main tables: constants, inductives, records, ... *)

(*s Constants tables. *) 

let terms = ref (Cmap.empty : ml_decl Cmap.t)
let init_terms () = terms := Cmap.empty
let add_term kn d = terms := Cmap.add kn d !terms
let lookup_term kn = Cmap.find kn !terms

let types = ref (Cmap.empty : ml_schema Cmap.t)
let init_types () = types := Cmap.empty
let add_type kn s = types := Cmap.add kn s !types
let lookup_type kn = Cmap.find kn !types 

(*s Inductives table. *)

let inductives = ref (KNmap.empty : (mutual_inductive_body * ml_ind) KNmap.t)
let init_inductives () = inductives := KNmap.empty
let add_ind kn mib ml_ind = inductives := KNmap.add kn (mib,ml_ind) !inductives
let lookup_ind kn = KNmap.find kn !inductives

(*s Recursors table. *)

let recursors = ref Cset.empty
let init_recursors () = recursors := Cset.empty

let add_recursors env kn = 
  let make_kn id = make_con (modpath kn) empty_dirpath (label_of_id id) in 
  let mib = Environ.lookup_mind kn env in 
  Array.iter 
    (fun mip -> 
       let id = mip.mind_typename in 
       let kn_rec = make_kn (Nameops.add_suffix id "_rec")
       and kn_rect = make_kn (Nameops.add_suffix id "_rect") in 
       recursors := Cset.add kn_rec (Cset.add kn_rect !recursors))
    mib.mind_packets

let is_recursor = function 
  | ConstRef kn -> Cset.mem kn !recursors
  | _ -> false

(*s Record tables. *)

let projs = ref (Refmap.empty : int Refmap.t)
let init_projs () = projs := Refmap.empty
let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs
let is_projection r = Refmap.mem r !projs
let projection_arity r = Refmap.find r !projs

(*s Tables synchronization. *)

let reset_tables () = 
  init_terms (); init_types (); init_inductives (); init_recursors (); 
  init_projs ()

(*s Printing. *)

(* The following functions work even on objects not in [Global.env ()].
   WARNING: for inductive objects, an extract_inductive must have been 
   done before. *)

let id_of_global = function 
  | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
  | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
  | ConstructRef ((kn,i),j) -> 
      (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
  | _ -> assert false

let pr_global r = 
 try Printer.pr_global r 
 with _ -> pr_id (id_of_global r)

(* idem, but with qualification, and only for constants. *)

let pr_long_global r = 
  try Printer.pr_global r 
  with _ -> match r with
    | ConstRef kn -> 
	let mp,_,l = repr_con kn in 
	str ((string_of_mp mp)^"."^(string_of_label l))
    | _ -> assert false

(*S Warning and Error messages. *)

let err s = errorlabstrm "Extraction" s

let error_axiom_scheme r i = 
  err (str "The type scheme axiom " ++ spc () ++
       pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ 
       str " type variable(s).") 

let warning_info_ax r =
  msg_warning (str "You must realize axiom " ++
		  pr_global r ++ str " in the extracted code.")

let warning_log_ax r = 
  msg_warning (str "This extraction depends on logical axiom" ++ spc () ++ 
		  pr_global r ++ str "." ++ spc() ++ 
		  str "Having false logical axiom in the environment when extracting" ++ 
		  spc () ++ str "may lead to incorrect or non-terminating ML terms.")

let check_inside_module () = 
  if Lib.is_modtype () then 
    err (str "You can't do that within a Module Type." ++ fnl () ++
	 str "Close it and try again.") 
  else if Lib.is_module () then 
    msg_warning
      (str "Extraction inside an opened module is experimental.\n" ++
       str "In case of problem, close it first.\n")

let check_inside_section () = 
  if Lib.sections_are_opened () then 
    err (str "You can't do that within a section." ++ fnl () ++
	 str "Close it and try again.")

let error_constant r = 
  err (pr_global r ++ str " is not a constant.") 

let error_inductive r = 
  err (pr_global r ++ spc () ++ str "is not an inductive type.")

let error_nb_cons () = 
  err (str "Not the right number of constructors.")

let error_module_clash s = 
  err (str ("There are two Coq modules with ML name " ^ s ^".\n") ++ 
       str "This is not allowed in ML. Please do some renaming first.")

let error_unknown_module m = 
  err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.") 

let error_toplevel () = 
  err (str "Toplevel pseudo-ML language can be used only at Coq toplevel.\n" ++
       str "You should use Extraction Language Ocaml or Haskell before.") 

let error_scheme () = 
  err (str "No Scheme modular extraction available yet.")

let error_not_visible r = 
  err (pr_global r ++ str " is not directly visible.\n" ++
       str "For example, it may be inside an applied functor." ++
       str "Use Recursive Extraction to get the whole environment.")

let error_MPfile_as_mod d = 
  err (str ("The whole file "^(string_of_dirpath d)^".v is used somewhere as a module.\n"^
	    "Extraction cannot currently deal with this situation.\n"))

let error_record r = 
  err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++
       str "To help extraction, please use an explicit name.") 

let check_loaded_modfile mp = match base_mp mp with 
  | MPfile dp -> if not (Library.library_is_loaded dp) then 
      err (str ("Please load library "^(string_of_dirpath dp^" first.")))
  | _ -> ()

(*S The Extraction auxiliary commands *)

(*s Extraction AutoInline *)

let auto_inline_ref = ref true

let auto_inline () = !auto_inline_ref

let _ = declare_bool_option 
	  {optsync = true;
	   optname = "Extraction AutoInline";
	   optkey = SecondaryTable ("Extraction", "AutoInline");
	   optread = auto_inline; 
	   optwrite = (:=) auto_inline_ref}

(*s Extraction TypeExpand *)

let type_expand_ref = ref true

let type_expand () = !type_expand_ref

let _ = declare_bool_option 
	  {optsync = true;
	   optname = "Extraction TypeExpand";
	   optkey = SecondaryTable ("Extraction", "TypeExpand");
	   optread = type_expand; 
	   optwrite = (:=) type_expand_ref}

(*s Extraction Optimize *)

type opt_flag = 
    { opt_kill_dum : bool; (* 1 *) 
      opt_fix_fun : bool;   (* 2 *)
      opt_case_iot : bool;  (* 4 *)
      opt_case_idr : bool;  (* 8 *)
      opt_case_idg : bool;  (* 16 *)
      opt_case_cst : bool;  (* 32 *)
      opt_case_fun : bool;  (* 64 *)
      opt_case_app : bool;  (* 128 *)
      opt_let_app : bool;   (* 256 *)
      opt_lin_let : bool;   (* 512 *)
      opt_lin_beta : bool } (* 1024 *)

let kth_digit n k = (n land (1 lsl k) <> 0)

let flag_of_int n = 
    { opt_kill_dum = kth_digit n 0;
      opt_fix_fun = kth_digit n 1;
      opt_case_iot = kth_digit n 2;
      opt_case_idr = kth_digit n 3;
      opt_case_idg = kth_digit n 4; 
      opt_case_cst = kth_digit n 5;
      opt_case_fun = kth_digit n 6;
      opt_case_app = kth_digit n 7;
      opt_let_app = kth_digit n 8;
      opt_lin_let = kth_digit n 9;
      opt_lin_beta = kth_digit n 10 }

(* For the moment, we allow by default everything except the type-unsafe 
   optimization [opt_case_idg]. *)

let int_flag_init = 1 + 2 + 4 + 8 + 32 + 64 + 128 + 256 + 512 + 1024

let int_flag_ref = ref int_flag_init
let opt_flag_ref = ref (flag_of_int int_flag_init)

let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n

let optims () = !opt_flag_ref

let _ = declare_bool_option 
	  {optsync = true; 
	   optname = "Extraction Optimize";
	   optkey = SecondaryTable ("Extraction", "Optimize");
	   optread = (fun () -> !int_flag_ref <> 0); 
	   optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}

let _ = declare_int_option
          { optsync = true;
            optname = "Extraction Flag";
            optkey = SecondaryTable("Extraction","Flag"); 
            optread = (fun _ -> Some !int_flag_ref); 
            optwrite = (function 
                          | None -> chg_flag 0
                          | Some i -> chg_flag (max i 0))}


(*s Extraction Lang *)

type lang = Ocaml | Haskell | Scheme | Toplevel

let lang_ref = ref Ocaml

let lang () = !lang_ref

let (extr_lang,_) = 
  declare_object 
    {(default_object "Extraction Lang") with  
       cache_function = (fun (_,l) -> lang_ref := l);
       load_function = (fun _ (_,l) -> lang_ref := l);
       export_function = (fun x -> Some x)}

let _ = declare_summary "Extraction Lang" 
	  { freeze_function = (fun () -> !lang_ref);
	    unfreeze_function = ((:=) lang_ref);
	    init_function = (fun () -> lang_ref := Ocaml);
	    survive_module = true;
	    survive_section = true }  
	  
let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)


(*s Extraction Inline/NoInline *)

let empty_inline_table = (Refset.empty,Refset.empty)

let inline_table = ref empty_inline_table

let to_inline r = Refset.mem r (fst !inline_table)

let to_keep r = Refset.mem r (snd !inline_table)

let add_inline_entries b l = 
  let f b = if b then Refset.add else Refset.remove in 
  let i,k = !inline_table in 
  inline_table := 
  (List.fold_right (f b) l i), 
  (List.fold_right (f (not b)) l k)

(* Registration of operations for rollback. *)

let (inline_extraction,_) =
  declare_object 
    {(default_object "Extraction Inline") with 
       cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
       load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
       export_function = (fun x -> Some x); 
       classify_function = (fun (_,o) -> Substitute o); 
       subst_function =
        (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
    }

let _ = declare_summary "Extraction Inline"
	  { freeze_function = (fun () -> !inline_table);
	    unfreeze_function = ((:=) inline_table);
	    init_function = (fun () -> inline_table := empty_inline_table);
	    survive_module = true;
	    survive_section = true }

(* Grammar entries. *)

let extraction_inline b l =
  check_inside_section (); 
  let refs = List.map Nametab.global l in 
  List.iter 
    (fun r -> match r with 
       | ConstRef _ -> ()
       | _ -> error_constant r) refs; 
  Lib.add_anonymous_leaf (inline_extraction (b,refs))

(* Printing part *)

let print_extraction_inline () = 
  let (i,n)= !inline_table in 
  let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in 
  msg 
    (str "Extraction Inline:" ++ fnl () ++ 
     Refset.fold
       (fun r p -> 
	  (p ++ str "  " ++ pr_long_global r ++ fnl ())) i' (mt ()) ++
     str "Extraction NoInline:" ++ fnl () ++ 
     Refset.fold
       (fun r p -> 
	  (p ++ str "  " ++ pr_long_global r ++ fnl ())) n (mt ()))

(* Reset part *)

let (reset_inline,_) = 
  declare_object
    {(default_object "Reset Extraction Inline") with  
       cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
       load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table); 
       export_function = (fun x -> Some x)}

let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())


(*s Extract Constant/Inductive. *)

(* UGLY HACK: to be defined in [extraction.ml] *)
let use_type_scheme_nb_args, register_type_scheme_nb_args = 
  let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r 

let customs = ref Refmap.empty

let add_custom r ids s = customs := Refmap.add r (ids,s) !customs

let is_custom r = Refmap.mem r !customs

let is_inline_custom r = (is_custom r) && (to_inline r) 

let find_custom r = snd (Refmap.find r !customs)

let find_type_custom r = Refmap.find r !customs

(* Registration of operations for rollback. *)

let (in_customs,_) = 
  declare_object 
    {(default_object "ML extractions") with 
       cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
       load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
       export_function = (fun x -> Some x); 
       classify_function = (fun (_,o) -> Substitute o); 
       subst_function =
        (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
    }

let _ = declare_summary "ML extractions"
	  { freeze_function = (fun () -> !customs);
	    unfreeze_function = ((:=) customs);
	    init_function = (fun () -> customs := Refmap.empty);
	    survive_module = true;
	    survive_section = true }

(* Grammar entries. *)

let extract_constant_inline inline r ids s =
  check_inside_section ();
  let g = Nametab.global r in 
  match g with 
    | ConstRef kn -> 
	let env = Global.env () in 
	let typ = Typeops.type_of_constant env kn in 
	let typ = Reduction.whd_betadeltaiota env typ in
	if Reduction.is_arity env typ 
	  then begin 
	    let nargs = use_type_scheme_nb_args env typ in 
	    if List.length ids <> nargs then error_axiom_scheme g nargs
	  end; 
	Lib.add_anonymous_leaf (inline_extraction (inline,[g]));
	Lib.add_anonymous_leaf (in_customs (g,ids,s))
    | _ -> error_constant g


let extract_inductive r (s,l) =
  check_inside_section ();
  let g = Nametab.global r in 
  match g with
    | IndRef ((kn,i) as ip) ->
	let mib = Global.lookup_mind kn in
	let n = Array.length mib.mind_packets.(i).mind_consnames in
	if n <> List.length l then error_nb_cons (); 
	Lib.add_anonymous_leaf (inline_extraction (true,[g]));
	Lib.add_anonymous_leaf (in_customs (g,[],s));
	list_iter_i
	  (fun j s -> 
	     let g = ConstructRef (ip,succ j) in 
	     Lib.add_anonymous_leaf (inline_extraction (true,[g]));
	     Lib.add_anonymous_leaf (in_customs (g,[],s))) l
    | _ -> error_inductive g