summaryrefslogtreecommitdiff
path: root/plugins/extraction/table.ml
blob: 497ddf03240182a95466311e2b663b0b99f382d7 (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
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

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

(** Sets and maps for [global_reference] that use the "user" [kernel_name]
    instead of the canonical one *)

module Refmap' = Map.Make(RefOrdered_env)
module Refset' = Set.Make(RefOrdered_env)

(*S Utilities about [module_path] and [kernel_names] and [global_reference] *)

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

let repr_of_r = function
  | ConstRef kn -> repr_con kn
  | IndRef (kn,_)
  | ConstructRef ((kn,_),_) -> repr_mind kn
  | VarRef _ -> assert false

let modpath_of_r r =
  let mp,_,_ = repr_of_r r in mp

let label_of_r r =
  let _,_,l = repr_of_r r in l

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

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

let raw_string_of_modfile = function
  | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f)))
  | _ -> assert false

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

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

let at_toplevel mp =
  is_modfile mp || is_toplevel mp

let rec mp_length mp =
  let mp0 = current_toplevel () in
  let rec len = function
    | mp when mp = mp0 -> 1
    | MPdot (mp,_) -> 1 + len mp
    | _ -> 1
  in len mp

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

let rec prefixes_mp mp = match mp with
  | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
  | _ -> MPset.singleton mp

let rec get_nth_label_mp n = function
  | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp
  | _ -> failwith "get_nth_label: not enough MPdot"

let common_prefix_from_list mp0 mpl =
  let prefixes = prefixes_mp mp0 in
  let rec f = function
    | [] -> None
    | mp :: l -> if MPset.mem mp prefixes then Some mp else f l
  in f mpl

let rec parse_labels2 ll mp1 = function
  | mp when mp1=mp -> mp,ll
  | MPdot (mp,l) -> parse_labels2 (l::ll) mp1 mp
  | mp -> mp,ll

let labels_of_ref r =
  let mp_top = current_toplevel () in
  let mp,_,l = repr_of_r r in
  parse_labels2 [l] mp_top mp


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

(* Theses tables are not registered within coq save/undo mechanism
   since we reset their contents at each run of Extraction *)

(*s Constants tables. *)

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

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

(*s Inductives table. *)

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

let inductive_kinds =
  ref (Mindmap_env.empty : inductive_kind Mindmap_env.t)
let init_inductive_kinds () = inductive_kinds := Mindmap_env.empty
let add_inductive_kind kn k =
    inductive_kinds := Mindmap_env.add kn k !inductive_kinds
let is_coinductive r =
  let kn = match r with
    | ConstructRef ((kn,_),_) -> kn
    | IndRef (kn,_) -> kn
    | _ -> assert false
  in
  try Mindmap_env.find kn !inductive_kinds = Coinductive
  with Not_found -> false

let is_coinductive_type = function
  | Tglob (r,_) -> is_coinductive r
  | _ -> false

let get_record_fields r =
  let kn = match r with
    | ConstructRef ((kn,_),_) -> kn
    | IndRef (kn,_) -> kn
    | _ -> assert false
  in
  try match Mindmap_env.find kn !inductive_kinds with
    | Record f -> f
    | _ -> []
  with Not_found -> []

let record_fields_of_type = function
  | Tglob (r,_) -> get_record_fields r
  | _ -> []

(*s Recursors table. *)

(* NB: here we can use the equivalence between canonical
   and user constant names : Cset is fine, no need for [Cset_env] *)

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

let add_recursors env kn =
  let mk_con id =
    make_con_equiv
      (modpath (user_mind kn))
      (modpath (canonical_mind 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 c_rec = mk_con (Nameops.add_suffix id "_rec")
       and c_rect = mk_con (Nameops.add_suffix id "_rect") in
       recursors := Cset.add c_rec (Cset.add c_rect !recursors))
    mib.mind_packets

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

(*s Record tables. *)

(* NB: here, working modulo name equivalence is ok *)

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 Table of used axioms *)

let info_axioms = ref Refset'.empty
let log_axioms = ref Refset'.empty
let init_axioms () = info_axioms := Refset'.empty; log_axioms := Refset'.empty
let add_info_axiom r = info_axioms := Refset'.add r !info_axioms
let remove_info_axiom r = info_axioms := Refset'.remove r !info_axioms
let add_log_axiom r = log_axioms := Refset'.add r !log_axioms

let opaques = ref Refset'.empty
let init_opaques () = opaques := Refset'.empty
let add_opaque r = opaques := Refset'.add r !opaques
let remove_opaque r = opaques := Refset'.remove r !opaques

(*s Extraction modes: modular or monolithic, library or minimal ?

Nota:
 - Recursive Extraction : monolithic, minimal
 - Separate Extraction : modular, minimal
 - Extraction Library : modular, library
*)

let modular_ref = ref false
let library_ref = ref false

let set_modular b = modular_ref := b
let modular () = !modular_ref

let set_library b = library_ref := b
let library () = !library_ref

(*s Printing. *)

(* The following functions work even on objects not in [Global.env ()].
   Warning: for inductive objects, this only works if an [extract_inductive]
   have been done earlier, otherwise we can only ask the Nametab about
   currently visible objects. *)

let safe_basename_of_global r =
  let last_chance r =
    try Nametab.basename_of_global r
    with Not_found ->
      anomaly "Inductive object unknown to extraction and not globally visible"
  in
  match r with
    | ConstRef kn -> id_of_label (con_label kn)
    | IndRef (kn,0) -> id_of_label (mind_label kn)
    | IndRef (kn,i) ->
      (try (snd (lookup_ind kn)).ind_packets.(i).ip_typename
       with Not_found -> last_chance r)
    | ConstructRef ((kn,i),j) ->
      (try (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
       with Not_found -> last_chance r)
    | VarRef _ -> assert false

let string_of_global r =
 try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r)
 with e when Errors.noncritical e -> string_of_id (safe_basename_of_global r)

let safe_pr_global r = str (string_of_global r)

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

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

let pr_long_mp mp =
  let lid = repr_dirpath (Nametab.dirpath_of_module mp) in
  str (String.concat "." (List.map string_of_id (List.rev lid)))

let pr_long_global ref = pr_path (Nametab.path_of_global ref)

(*S Warning and Error messages. *)

let err s = errorlabstrm "Extraction" s

let warning_axioms () =
  let info_axioms = Refset'.elements !info_axioms in
  if info_axioms = [] then ()
  else begin
    let s = if List.length info_axioms = 1 then "axiom" else "axioms" in
    msg_warning
      (str ("The following "^s^" must be realized in the extracted code:")
       ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
       ++ str "." ++ fnl ())
  end;
  let log_axioms = Refset'.elements !log_axioms in
  if log_axioms = [] then ()
  else begin
    let s = if List.length log_axioms = 1 then "axiom was" else "axioms were"
    in
    msg_warning
      (str ("The following logical "^s^" encountered:") ++
       hov 1
         (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n")
       ++
       str "Having invalid logical axiom in the environment when extracting" ++
       spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
       fnl ())
  end;
  if !Flags.load_proofs = Flags.Dont && info_axioms@log_axioms <> [] then
    msg_warning
      (str "Some of these axioms might be due to option -dont-load-proofs.")

let warning_opaques accessed =
  let opaques = Refset'.elements !opaques in
  if opaques = [] then ()
  else
    let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in
    if accessed then
      msg_warning
	(str "The extraction is currently set to bypass opacity,\n" ++
	 str "the following opaque constant bodies have been accessed :" ++
	 lst ++ str "." ++ fnl ())
    else
      msg_warning
	(str "The extraction now honors the opacity constraints by default,\n" ++
	 str "the following opaque constants have been extracted as axioms :" ++
	 lst ++ str "." ++ fnl () ++
	 str "If necessary, use \"Set Extraction AccessOpaque\" to change this."
	 ++ fnl ())

let warning_both_mod_and_cst q mp r =
 msg_warning
   (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++
    str "do you mean module " ++
    pr_long_mp mp ++
    str " or object " ++
    pr_long_global r ++ str " ?" ++ fnl () ++
    str "First choice is assumed, for the second one please use " ++
    str "fully qualified name." ++ fnl ())

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

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 warning_id s =
  msg_warning (str ("The identifier "^s^
		    " contains __ which is reserved for the extraction"))

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

let error_inductive r =
  err (safe_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 mp1 mp2 =
  err (str "The Coq modules " ++ pr_long_mp mp1 ++ str " and " ++
       pr_long_mp mp2 ++ str " have the same ML name.\n" ++
       str "This is not supported yet. Please do some renaming first.")

let error_no_module_expr mp =
  err (str "The module " ++ pr_long_mp mp
       ++ str " has no body, it probably comes from\n"
       ++ str "some Declare Module outside any Module Type.\n"
       ++ str "This situation is currently unsupported by the extraction.")

let error_singleton_become_prop id =
  err (str "The informative inductive type " ++ pr_id id ++
       str " has a Prop instance.\n" ++
       str "This happens when a sort-polymorphic singleton inductive type\n" ++
       str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++
       str "The Ocaml extraction cannot handle this situation yet.\n" ++
       str "Instead, use a sort-monomorphic type such as (True /\\ True)\n" ++
       str "or extract to Haskell.")

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

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

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

let error_MPfile_as_mod mp b =
  let s1 = if b then "asked" else "required" in
  let s2 = if b then "extract some objects of this module or\n" else "" in
  err (str ("Extraction of file "^(raw_string_of_modfile mp)^
	    ".v as a module is "^s1^".\n"^
	    "Monolithic Extraction cannot deal with this situation.\n"^
	    "Please "^s2^"use (Recursive) Extraction Library instead.\n"))

let msg_non_implicit r n id =
  let name = match id with
    | Anonymous -> ""
    | Name id -> "(" ^ string_of_id id ^ ") "
  in
  "The " ^ (ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r)

let error_non_implicit msg =
  err (str (msg ^ " still occurs after extraction.") ++
       fnl () ++ str "Please check the Extraction Implicit declarations.")

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

let info_file f =
  Flags.if_verbose message
    ("The file "^f^" has been created by extraction.")


(*S The Extraction auxiliary commands *)

(* The objects defined below should survive an arbitrary time,
   so we register them to coq save/undo mechanism. *)

let my_bool_option name initval =
  let flag = ref initval in
  let access = fun () -> !flag in
  let _ = declare_bool_option
    {optsync = true;
     optdepr = false;
     optname = "Extraction "^name;
     optkey = ["Extraction"; name];
     optread = access;
     optwrite = (:=) flag }
  in
  access

(*s Extraction AccessOpaque *)

let access_opaque = my_bool_option "AccessOpaque" true

(*s Extraction AutoInline *)

let auto_inline = my_bool_option "AutoInline" false

(*s Extraction TypeExpand *)

let type_expand = my_bool_option "TypeExpand" true

(*s Extraction KeepSingleton *)

let keep_singleton = my_bool_option "KeepSingleton" false

(*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], which anyway
     cannot be activated currently (cf [Mlutil.branch_as_fun])
   - the linear let and beta reduction [opt_lin_let] and [opt_lin_beta]
     (may lead to complexity blow-up, subsumed by finer reductions
      when inlining recursors).
*)

let int_flag_init = 1 + 2 + 4 + 8 (*+ 16*) + 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;
           optdepr = false;
	   optname = "Extraction Optimize";
	   optkey = ["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;
            optdepr = false;
            optname = "Extraction Flag";
            optkey = ["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

let lang_ref = ref Ocaml

let lang () = !lang_ref

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

let _ = declare_summary "Extraction Lang"
	  { freeze_function = (fun () -> !lang_ref);
	    unfreeze_function = ((:=) lang_ref);
	    init_function = (fun () -> lang_ref := Ocaml) }

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 : bool * global_reference list -> obj =
  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);
       classify_function = (fun o -> Substitute o);
       discharge_function =
	(fun (_,(b,l)) -> Some (b, List.map pop_global_reference l));
       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) }

(* Grammar entries. *)

let extraction_inline b l =
  let refs = List.map Smartlocate.global_with_alias 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 "  " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++
     str "Extraction NoInline:" ++ fnl () ++
     Refset'.fold
       (fun r p ->
	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) n (mt ()))

(* Reset part *)

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

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

(*s Extraction Implicit *)

type int_or_id = ArgInt of int | ArgId of identifier

let implicits_table = ref Refmap'.empty

let implicits_of_global r =
 try Refmap'.find r !implicits_table with Not_found -> []

let add_implicits r l =
  let typ = Global.type_of_global r in
  let rels,_ =
    decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in
  let names = List.rev_map fst rels in
  let n = List.length names in
  let check = function
    | ArgInt i ->
	if 1 <= i && i <= n then i
	else err (int i ++ str " is not a valid argument number for " ++
		  safe_pr_global r)
    | ArgId id ->
	(try list_index (Name id) names
	 with Not_found ->
	   err (str "No argument " ++ pr_id id ++ str " for " ++
		safe_pr_global r))
  in
  let l' = List.map check l in
  implicits_table := Refmap'.add r l' !implicits_table

(* Registration of operations for rollback. *)

let implicit_extraction : global_reference * int_or_id list -> obj =
  declare_object
    {(default_object "Extraction Implicit") with
       cache_function = (fun (_,(r,l)) -> add_implicits r l);
       load_function = (fun _ (_,(r,l)) -> add_implicits r l);
       classify_function = (fun o -> Substitute o);
       subst_function = (fun (s,(r,l)) -> (fst (subst_global s r), l))
    }

let _ = declare_summary "Extraction Implicit"
	  { freeze_function = (fun () -> !implicits_table);
	    unfreeze_function = ((:=) implicits_table);
	    init_function = (fun () -> implicits_table := Refmap'.empty) }

(* Grammar entries. *)

let extraction_implicit r l =
  check_inside_section ();
  Lib.add_anonymous_leaf (implicit_extraction (Smartlocate.global_with_alias r,l))


(*s Extraction Blacklist of filenames not to use while extracting *)

let blacklist_table = ref Idset.empty

let modfile_ids = ref []
let modfile_mps = ref MPmap.empty

let reset_modfile () =
  modfile_ids := Idset.elements !blacklist_table;
  modfile_mps := MPmap.empty

let string_of_modfile mp =
  try MPmap.find mp !modfile_mps
  with Not_found ->
    let id = id_of_string (raw_string_of_modfile mp) in
    let id' = next_ident_away id !modfile_ids in
    let s' = string_of_id id' in
    modfile_ids := id' :: !modfile_ids;
    modfile_mps := MPmap.add mp s' !modfile_mps;
    s'

(* same as [string_of_modfile], but preserves the capital/uncapital 1st char *)

let file_of_modfile mp =
  let s0 = match mp with
    | MPfile f -> string_of_id (List.hd (repr_dirpath f))
    | _ -> assert false
  in
  let s = String.copy (string_of_modfile mp) in
  if s.[0] <> s0.[0] then s.[0] <- s0.[0];
  s

let add_blacklist_entries l =
  blacklist_table :=
    List.fold_right (fun s -> Idset.add (id_of_string (String.capitalize s)))
      l !blacklist_table

(* Registration of operations for rollback. *)

let blacklist_extraction : string list -> obj =
  declare_object
    {(default_object "Extraction Blacklist") with
       cache_function = (fun (_,l) -> add_blacklist_entries l);
       load_function = (fun _ (_,l) -> add_blacklist_entries l);
       subst_function = (fun (_,x) -> x)
    }

let _ = declare_summary "Extraction Blacklist"
	  { freeze_function = (fun () -> !blacklist_table);
	    unfreeze_function = ((:=) blacklist_table);
	    init_function = (fun () -> blacklist_table := Idset.empty) }

(* Grammar entries. *)

let extraction_blacklist l =
  let l = List.rev_map string_of_id l in
  Lib.add_anonymous_leaf (blacklist_extraction l)

(* Printing part *)

let print_extraction_blacklist () =
  msgnl
    (prlist_with_sep fnl pr_id (Idset.elements !blacklist_table))

(* Reset part *)

let reset_blacklist : unit -> obj =
  declare_object
    {(default_object "Reset Extraction Blacklist") with
       cache_function = (fun (_,_)-> blacklist_table := Idset.empty);
       load_function = (fun _ (_,_)-> blacklist_table := Idset.empty)}

let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())

(*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

let custom_matchs = ref Refmap'.empty

let add_custom_match r s =
  custom_matchs := Refmap'.add r s !custom_matchs

let indref_of_match pv =
  if Array.length pv = 0 then raise Not_found;
  let (_,pat,_) = pv.(0) in
  match pat with
    | Pusual (ConstructRef (ip,_)) -> IndRef ip
    | Pcons (ConstructRef (ip,_),_) -> IndRef ip
    | _ -> raise Not_found

let is_custom_match pv =
  try Refmap'.mem (indref_of_match pv) !custom_matchs
  with Not_found -> false

let find_custom_match pv =
  Refmap'.find (indref_of_match pv) !custom_matchs

(* Registration of operations for rollback. *)

let in_customs : global_reference * string list * string -> obj =
  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);
       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) }

let in_custom_matchs : global_reference * string -> obj =
  declare_object
    {(default_object "ML extractions custom matchs") with
       cache_function = (fun (_,(r,s)) -> add_custom_match r s);
       load_function = (fun _ (_,(r,s)) -> add_custom_match r s);
       classify_function = (fun o -> Substitute o);
       subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s))
    }

let _ = declare_summary "ML extractions custom match"
	  { freeze_function = (fun () -> !custom_matchs);
	    unfreeze_function = ((:=) custom_matchs);
	    init_function = (fun () -> custom_matchs := Refmap'.empty) }

(* Grammar entries. *)

let extract_constant_inline inline r ids s =
  check_inside_section ();
  let g = Smartlocate.global_with_alias 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 optstr =
  check_inside_section ();
  let g = Smartlocate.global_with_alias r in
  Dumpglob.add_glob (loc_of_reference r) g;
  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));
	Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s)))
	  optstr;
	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



(*s Tables synchronization. *)

let reset_tables () =
  init_terms (); init_types (); init_inductives ();
  init_inductive_kinds (); init_recursors ();
  init_projs (); init_axioms (); init_opaques (); reset_modfile ()