aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/funind/indfun_common.ml
blob: 13b242d5d9c9b1f7e34401149acf2cbbe61f2c51 (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
open Names
open Pp

open Libnames

let mk_prefix pre id = id_of_string (pre^(string_of_id id))
let mk_rel_id = mk_prefix "R_"
let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
let mk_complete_id id = Nameops.add_suffix (mk_rel_id id) "_complete"
let mk_equation_id id = Nameops.add_suffix id "_equation"

let msgnl m =
  ()

let invalid_argument s = raise (Invalid_argument s)


let fresh_id avoid s = Termops.next_global_ident_away true (id_of_string s) avoid

let fresh_name avoid s = Name (fresh_id avoid s)

let get_name avoid ?(default="H") = function
  | Anonymous -> fresh_name avoid default
  | Name n -> Name n

let array_get_start a =
  try 
    Array.init
      (Array.length a - 1)
      (fun i -> a.(i))
  with Invalid_argument "index out of bounds" -> 
    invalid_argument "array_get_start"
      
let id_of_name = function
    Name id -> id
  | _ -> raise Not_found

let locate  ref =
    let (loc,qid) = qualid_of_reference ref in
    Nametab.locate qid

let locate_ind ref =
  match locate ref with
    | IndRef x -> x
    | _ -> raise Not_found

let locate_constant ref =
  match locate ref with
    | ConstRef x -> x
    | _ -> raise Not_found


let locate_with_msg msg f x =
  try
    f x
  with
    | Not_found -> raise (Util.UserError("", msg))
    | e -> raise e


let filter_map filter f =
  let rec it = function
    | [] -> []
    | e::l ->
	if filter e
	then
	  (f e) :: it l
	else it l
  in
  it


let chop_rlambda_n  =
  let rec chop_lambda_n acc n rt =
      if n == 0
      then List.rev acc,rt
      else
	match rt with
	  | Rawterm.RLambda(_,name,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
	  | Rawterm.RLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
	  | _ -> 
	      raise (Util.UserError("chop_rlambda_n",
				    str "chop_rlambda_n: Not enough Lambdas"))
  in
  chop_lambda_n []

let chop_rprod_n  =
  let rec chop_prod_n acc n rt =
      if n == 0
      then List.rev acc,rt
      else
	match rt with
	  | Rawterm.RProd(_,name,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
	  | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
  in
  chop_prod_n []



let list_union_eq eq_fun l1 l2 =
  let rec urec = function
    | [] -> l2
    | a::l -> if List.exists (eq_fun a) l2 then urec l else a::urec l
  in
  urec l1

let list_add_set_eq eq_fun x l =
  if List.exists (eq_fun x) l then l else x::l

  


let const_of_id id =
  let _,princ_ref = 
    qualid_of_reference (Libnames.Ident (Util.dummy_loc,id))
  in
  try Nametab.locate_constant princ_ref
  with Not_found -> Util.error ("cannot find "^ string_of_id id)

let def_of_const t =
   match (Term.kind_of_term t) with
    Term.Const sp -> 
      (try (match (Global.lookup_constant sp) with
             {Declarations.const_body=Some c} -> Declarations.force c
	     |_ -> assert false)
       with _ -> assert false)
    |_ -> assert false

let coq_constant s =
  Coqlib.gen_constant_in_modules "RecursiveDefinition" 
    (Coqlib.init_modules @ Coqlib.arith_modules) s;;

let constant sl s =
  constr_of_reference
    (Nametab.locate (make_qualid(Names.make_dirpath 
			   (List.map id_of_string (List.rev sl)))
	       (id_of_string s)));;

let find_reference sl s =
    (Nametab.locate (make_qualid(Names.make_dirpath 
			   (List.map id_of_string (List.rev sl)))
	       (id_of_string s)));;

let eq = lazy(coq_constant "eq")
let refl_equal = lazy(coq_constant "refl_equal")

(*****************************************************************)
(* Copy of the standart save mechanism but without the much too  *)
(* slow reduction function                                       *) 
(*****************************************************************)
open Declarations
open Entries
open Decl_kinds
open Declare
let definition_message id =
  Options.if_verbose message ((string_of_id id) ^ " is defined")


let save with_clean id const (locality,kind) hook =
  let {const_entry_body = pft;
       const_entry_type = tpo;
       const_entry_opaque = opacity } = const in
  let l,r = match locality with
    | Local when Lib.sections_are_opened () ->
        let k = logical_kind_of_goal_kind kind in
	let c = SectionLocalDef (pft, tpo, opacity) in
	let _ = declare_variable id (Lib.cwd(), c, k) in
	(Local, VarRef id)
    | Local ->
        let k = logical_kind_of_goal_kind kind in
        let kn = declare_constant id (DefinitionEntry const, k) in
	(Global, ConstRef kn)
    | Global ->
        let k = logical_kind_of_goal_kind kind in
        let kn = declare_constant id (DefinitionEntry const, k) in
	(Global, ConstRef kn) in
  if with_clean then  Pfedit.delete_current_proof ();
  hook l r;
  definition_message id




let extract_pftreestate pts =
  let pfterm,subgoals = Refiner.extract_open_pftreestate pts in
  let tpfsigma = Refiner.evc_of_pftreestate pts in 
  let exl = Evarutil.non_instantiated tpfsigma  in
  if subgoals <> [] or exl <> [] then
    Util.errorlabstrm "extract_proof"
      (if subgoals <> [] then
        str "Attempt to save an incomplete proof"
      else
        str "Attempt to save a proof with existential variables still non-instantiated");
  let env = Global.env_of_context (Refiner.proof_of_pftreestate pts).Proof_type.goal.Evd.evar_hyps in
  env,tpfsigma,pfterm


let nf_betaiotazeta =
  let clos_norm_flags flgs env sigma t =
    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
  clos_norm_flags Closure.betaiotazeta  

let nf_betaiota =
  let clos_norm_flags flgs env sigma t =
    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
  clos_norm_flags Closure.betaiota  

let cook_proof do_reduce =
  let pfs = Pfedit.get_pftreestate () 
(*   and ident = Pfedit.get_current_proof_name ()  *)
  and (ident,strength,concl,hook) = Pfedit.current_proof_statement ()  in
  let env,sigma,pfterm = extract_pftreestate pfs in
  let pfterm = 
    if do_reduce
    then nf_betaiota env sigma pfterm
    else pfterm
  in
  (ident,
   ({ const_entry_body = pfterm;
      const_entry_type = Some concl;
      const_entry_opaque = false;
      const_entry_boxed = false},
    strength, hook))


let new_save_named opacity =
  let id,(const,persistence,hook) = cook_proof true  in
  let const = { const with const_entry_opaque = opacity } in
  save true id const persistence hook

let get_proof_clean do_reduce = 
  let result = cook_proof do_reduce in 
  Pfedit.delete_current_proof ();
  result

let with_full_print f a = 
  let old_implicit_args = Impargs.is_implicit_args ()
  and old_strict_implicit_args =  Impargs.is_strict_implicit_args ()
  and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
  let old_rawprint = !Options.raw_print in 
  Options.raw_print := true;
  Impargs.make_implicit_args false;
  Impargs.make_strict_implicit_args false;
  Impargs.make_contextual_implicit_args false;
  try 
    let res = f a in 
    Impargs.make_implicit_args old_implicit_args;
    Impargs.make_strict_implicit_args old_strict_implicit_args;
    Impargs.make_contextual_implicit_args old_contextual_implicit_args;
    Options.raw_print := old_rawprint;
    res
  with  
    | e -> 
	Impargs.make_implicit_args old_implicit_args;
	Impargs.make_strict_implicit_args old_strict_implicit_args;
	Impargs.make_contextual_implicit_args old_contextual_implicit_args;
	Options.raw_print := old_rawprint;
	raise e






(**********************)

type function_info = 
    { 
      function_constant : constant;
      graph_ind : inductive;
      equation_lemma : constant option;
      correctness_lemma : constant option;
      completeness_lemma : constant option; 
      rect_lemma : constant option;
      rec_lemma : constant option;
      prop_lemma : constant option;
      is_general : bool; (* Has this function been defined using general recursive definition *)
    }
      

(* type function_db  = function_info list *)

(* let function_table = ref ([] : function_db) *)


let from_function = ref Cmap.empty
let from_graph = ref Indmap.empty
(*
let rec do_cache_info finfo = function 
  | [] -> raise Not_found 
  | (finfo'::finfos as l) -> 
      if finfo' == finfo then l 
      else if finfo'.function_constant = finfo.function_constant 
      then finfo::finfos
      else
	let res = do_cache_info finfo finfos in 
	if res == finfos then l else  finfo'::l
  

let cache_Function (_,(finfos)) = 
  let new_tbl = 
    try do_cache_info finfos !function_table
    with Not_found -> finfos::!function_table
  in  
  if new_tbl != !function_table 
  then function_table := new_tbl
*)

let cache_Function (_,finfos) = 
  from_function := Cmap.add finfos.function_constant finfos !from_function;
  from_graph := Indmap.add finfos.graph_ind finfos !from_graph


let load_Function _  = cache_Function
let open_Function _ = cache_Function
let subst_Function (_,subst,finfos) = 
  let do_subst_con c = fst (Mod_subst.subst_con subst c)
  and do_subst_ind (kn,i) = (Mod_subst.subst_kn subst kn,i)
  in
  let function_constant' = do_subst_con finfos.function_constant in 
  let graph_ind' = do_subst_ind finfos.graph_ind in 
  let equation_lemma' = Util.option_smartmap do_subst_con finfos.equation_lemma in 
  let correctness_lemma' = Util.option_smartmap do_subst_con finfos.correctness_lemma in 
  let completeness_lemma' = Util.option_smartmap do_subst_con finfos.completeness_lemma in 
  let rect_lemma' = Util.option_smartmap do_subst_con finfos.rect_lemma in
  let rec_lemma' = Util.option_smartmap do_subst_con finfos.rec_lemma in 
  let prop_lemma' =  Util.option_smartmap do_subst_con finfos.prop_lemma in 
  if function_constant' == finfos.function_constant && 
    graph_ind' == finfos.graph_ind && 
    equation_lemma' == finfos.equation_lemma &&
    correctness_lemma' == finfos.correctness_lemma && 
    completeness_lemma' == finfos.completeness_lemma && 
    rect_lemma' == finfos.rect_lemma && 
    rec_lemma' == finfos.rec_lemma && 
    prop_lemma' == finfos.prop_lemma 
  then finfos 
  else
    { function_constant = function_constant';
      graph_ind = graph_ind';
      equation_lemma = equation_lemma' ;
      correctness_lemma = correctness_lemma' ;
      completeness_lemma = completeness_lemma' ;
      rect_lemma = rect_lemma' ;
      rec_lemma = rec_lemma';
      prop_lemma = prop_lemma';
      is_general = finfos.is_general
    }

let classify_Function (_,infos) = Libobject.Substitute infos

let export_Function infos = Some infos


let discharge_Function (_,finfos) = 
  let function_constant' = Lib.discharge_con finfos.function_constant
  and graph_ind' = Lib.discharge_inductive finfos.graph_ind 
  and equation_lemma' = Util.option_smartmap Lib.discharge_con finfos.equation_lemma 
  and correctness_lemma' = Util.option_smartmap Lib.discharge_con finfos.correctness_lemma 
  and completeness_lemma' = Util.option_smartmap Lib.discharge_con finfos.completeness_lemma 
  and rect_lemma' = Util.option_smartmap Lib.discharge_con finfos.rect_lemma 
  and rec_lemma' = Util.option_smartmap Lib.discharge_con finfos.rec_lemma
  and prop_lemma' = Util.option_smartmap Lib.discharge_con finfos.prop_lemma
  in
  if function_constant' == finfos.function_constant && 
    graph_ind' == finfos.graph_ind && 
    equation_lemma' == finfos.equation_lemma &&
    correctness_lemma' == finfos.correctness_lemma && 
    completeness_lemma' == finfos.completeness_lemma && 
    rect_lemma' == finfos.rect_lemma && 
    rec_lemma' == finfos.rec_lemma && 
    prop_lemma' == finfos.prop_lemma 
  then Some finfos 
  else
    Some { function_constant = function_constant' ;
	   graph_ind = graph_ind' ;
	   equation_lemma = equation_lemma' ;
	   correctness_lemma = correctness_lemma' ;
	   completeness_lemma = completeness_lemma';
	   rect_lemma = rect_lemma';
	   rec_lemma = rec_lemma';
	   prop_lemma = prop_lemma' ;
	   is_general = finfos.is_general
	 }    

open Term
let pr_info f_info = 
  str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
    str "function_constant_type := " ++ 
    (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++
    str "equation_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
    str "completeness_lemma :=" ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
    str "correctness_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
    str "rect_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++
    str "rec_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++
    str "prop_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
    str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () 

let pr_table tb = 
  let l = Cmap.fold (fun k v acc -> v::acc) tb [] in 
  Util.prlist_with_sep fnl pr_info l

let in_Function,out_Function = 
  Libobject.declare_object
    {(Libobject.default_object "FUNCTIONS_DB") with 
       Libobject.cache_function = cache_Function;
       Libobject.load_function  = load_Function;
       Libobject.classify_function  = classify_Function;
       Libobject.subst_function = subst_Function;
       Libobject.export_function = export_Function;
       Libobject.discharge_function = discharge_Function
(*        Libobject.open_function = open_Function; *)
    }



(* Synchronisation with reset *)
let freeze () = 
  !from_function,!from_graph
let unfreeze (functions,graphs) = 
(*   Pp.msgnl (str "unfreezing function_table : " ++ pr_table l); *)
  from_function := functions;
  from_graph := graphs

let init () = 
(*   Pp.msgnl (str "reseting function_table");  *)
  from_function := Cmap.empty;
  from_graph := Indmap.empty

let _ = 
  Summary.declare_summary "functions_db_sum"
    { Summary.freeze_function = freeze;
      Summary.unfreeze_function = unfreeze;
      Summary.init_function = init;
      Summary.survive_module = false; 
      Summary.survive_section = false }

let find_or_none id = 
  try Some 
    (match Nametab.locate (make_short_qualid id) with ConstRef c -> c | _ -> Util.anomaly "Not a constant" 
    ) 
  with Not_found -> None



let find_Function_infos f = 
  Cmap.find f !from_function


let find_Function_of_graph ind = 
  Indmap.find ind !from_graph
  
let update_Function finfo = 
(*   Pp.msgnl (pr_info finfo); *)
  Lib.add_anonymous_leaf (in_Function finfo)
      
  
let add_Function is_general f = 
  let f_id = id_of_label (con_label f) in 
  let equation_lemma = find_or_none (mk_equation_id f_id)
  and correctness_lemma = find_or_none (mk_correct_id f_id) 
  and completeness_lemma = find_or_none (mk_complete_id f_id) 
  and rect_lemma = find_or_none (Nameops.add_suffix f_id "_rect")
  and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec")
  and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind")
  and graph_ind = 
    match Nametab.locate (make_short_qualid (mk_rel_id f_id)) 
    with | IndRef ind -> ind | _ -> Util.anomaly "Not an inductive"
  in
  let finfos = 
    { function_constant = f;
      equation_lemma = equation_lemma;
      completeness_lemma = completeness_lemma;
      correctness_lemma = correctness_lemma;
      rect_lemma = rect_lemma;
      rec_lemma = rec_lemma;
      prop_lemma = prop_lemma;
      graph_ind = graph_ind;
      is_general = is_general
      
    }
  in
  update_Function finfos

let pr_table () = pr_table !from_function
(*********************************)
(* Debuging *)
let function_debug = ref false 
open Goptions

let function_debug_sig =
  {
    optsync = false;
    optname = "Function debug";
    optkey =  PrimaryTable("Function_debug");
    optread = (fun () -> !function_debug);
    optwrite = (fun b -> function_debug := b)
  }

let _ = declare_bool_option function_debug_sig


let do_observe () = 
  !function_debug = true
      
      
    
exception Building_graph of exn 
exception Defining_principle of exn