aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/obligations.ml
blob: be5711820a61b0da0a078442a6b242ff8f919380 (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
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
open Printf
open Globnames
open Libobject
open Entries
open Decl_kinds
open Declare

(**
   - Get types of existentials ;
   - Flatten dependency tree (prefix order) ;
   - Replace existentials by De Bruijn indices in term, applied to the right arguments ;
   - Apply term prefixed by quantification on "existentials".
*)

open Term
open Context
open Vars
open Names
open Evd
open Pp
open Errors
open Util

let declare_fix_ref = ref (fun _ _ _ _ _ _ -> assert false)
let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)

let trace s =
  if !Flags.debug then msg_debug s
  else ()

let succfix (depth, fixrels) =
  (succ depth, List.map succ fixrels)

let check_evars env evm =
  Evar.Map.iter
  (fun key evi ->
   let (loc,k) = evar_source key evm in
     match k with
     | Evar_kinds.QuestionMark _
     | Evar_kinds.ImplicitArg (_,_,false) -> ()
     | _ ->
       Pretype_errors.error_unsolvable_implicit loc env
         evm (Evarutil.nf_evar_info evm evi) k None)
  (Evd.undefined_map evm)

type oblinfo =
  { ev_name: int * Id.t;
    ev_hyps: named_context;
    ev_status: Evar_kinds.obligation_definition_status;
    ev_chop: int option;
    ev_src: Evar_kinds.t Loc.located;
    ev_typ: types;
    ev_tac: unit Proofview.tactic option;
    ev_deps: Int.Set.t }

(* spiwack: Store field for internalizing ev_tac in evar_infos' evar_extra. *)
let evar_tactic = Store.field ()

(** Substitute evar references in t using De Bruijn indices,
  where n binders were passed through. *)

let subst_evar_constr evs n idf t = 
  let seen = ref Int.Set.empty in
  let transparent = ref Id.Set.empty in
  let evar_info id = List.assoc_f Evar.equal id evs in
  let rec substrec (depth, fixrels) c = match kind_of_term c with
    | Evar (k, args) ->
	let { ev_name = (id, idstr) ;
	      ev_hyps = hyps ; ev_chop = chop } =
	  try evar_info k
	  with Not_found ->
	    anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found")
	in
        seen := Int.Set.add id !seen;
	  (* Evar arguments are created in inverse order,
	     and we must not apply to defined ones (i.e. LetIn's)
	  *)
	let args =
	  let n = match chop with None -> 0 | Some c -> c in
	  let (l, r) = List.chop n (List.rev (Array.to_list args)) in
	    List.rev r
	in
	let args =
	  let rec aux hyps args acc =
	     match hyps, args with
		 ((_, None, _) :: tlh), (c :: tla) ->
		   aux tlh tla ((substrec (depth, fixrels) c) :: acc)
	       | ((_, Some _, _) :: tlh), (_ :: tla) ->
		   aux tlh tla acc
	       | [], [] -> acc
	       | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
	  in aux hyps args []
	in
	  if List.exists
            (fun x -> match kind_of_term x with
            | Rel n -> Int.List.mem n fixrels
            | _ -> false) args
          then
	    transparent := Id.Set.add idstr !transparent;
	  mkApp (idf idstr, Array.of_list args)
    | Fix _ ->
	map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c
    | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c
  in
  let t' = substrec (0, []) t in
    t', !seen, !transparent


(** Substitute variable references in t using De Bruijn indices,
  where n binders were passed through. *)
let subst_vars acc n t =
  let var_index id = Util.List.index Id.equal id acc in
  let rec substrec depth c = match kind_of_term c with
    | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
    | _ -> map_constr_with_binders succ substrec depth c
  in
    substrec 0 t

(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
    to a product : forall H1 : t1, ..., forall Hn : tn, concl.
    Changes evars and hypothesis references to variable references.
*)
let etype_of_evar evs hyps concl =
  let rec aux acc n = function
      (id, copt, t) :: tl ->
	let t', s, trans = subst_evar_constr evs n mkVar t in
	let t'' = subst_vars acc 0 t' in
	let rest, s', trans' = aux (id :: acc) (succ n) tl in
	let s' = Int.Set.union s s' in
	let trans' = Id.Set.union trans trans' in
	  (match copt with
	      Some c -> 
		let c', s'', trans'' = subst_evar_constr evs n mkVar c in
		let c' = subst_vars acc 0 c' in
		  mkNamedProd_or_LetIn (id, Some c', t'') rest,
		Int.Set.union s'' s',
		Id.Set.union trans'' trans'
	    | None ->
		mkNamedProd_or_LetIn (id, None, t'') rest, s', trans')
    | [] ->
	let t', s, trans = subst_evar_constr evs n mkVar concl in
	  subst_vars acc 0 t', s, trans
  in aux [] 0 (List.rev hyps)

let trunc_named_context n ctx =
  let len = List.length ctx in
    List.firstn (len - n) ctx

let rec chop_product n t =
  if Int.equal n 0 then Some t
  else
    match kind_of_term t with
      | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
      | _ -> None

let evar_dependencies evm oev =
  let one_step deps =
    Evar.Set.fold (fun ev s ->
      let evi = Evd.find evm ev in
      let deps' = evars_of_filtered_evar_info evi in
      if Evar.Set.mem oev deps' then
	invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ string_of_existential oev)
      else Evar.Set.union deps' s)
      deps deps
  in
  let rec aux deps =
    let deps' = one_step deps in
      if Evar.Set.equal deps deps' then deps
      else aux deps'
  in aux (Evar.Set.singleton oev)
      
let move_after (id, ev, deps as obl) l = 
  let rec aux restdeps = function
    | (id', _, _) as obl' :: tl -> 
	let restdeps' = Evar.Set.remove id' restdeps in
	  if Evar.Set.is_empty restdeps' then
	    obl' :: obl :: tl
	  else obl' :: aux restdeps' tl
    | [] -> [obl]
  in aux (Evar.Set.remove id deps) l
    
let sort_dependencies evl =
  let rec aux l found list =
    match l with
    | (id, ev, deps) as obl :: tl ->
	let found' = Evar.Set.union found (Evar.Set.singleton id) in
	  if Evar.Set.subset deps found' then
	    aux tl found' (obl :: list)
	  else aux (move_after obl tl) found list
    | [] -> List.rev list
  in aux evl Evar.Set.empty []

open Environ

let eterm_obligations env name evm fs ?status t ty = 
  (* 'Serialize' the evars *)
  let nc = Environ.named_context env in
  let nc_len = Context.named_context_length nc in
  let evm = Evarutil.nf_evar_map_undefined evm in
  let evl = Evarutil.non_instantiated evm in
  let evl = Evar.Map.bindings evl in
  let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
  let sevl = sort_dependencies evl in
  let evl = List.map (fun (id, ev, _) -> id, ev) sevl in
  let evn =
    let i = ref (-1) in
      List.rev_map (fun (id, ev) -> incr i;
		      (id, (!i, Id.of_string
			      (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i))),
		       ev)) evl
  in
  let evts =
    (* Remove existential variables in types and build the corresponding products *)
    List.fold_right
      (fun (id, (n, nstr), ev) l ->
	 let hyps = Evd.evar_filtered_context ev in
	 let hyps = trunc_named_context nc_len hyps in
	 let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in
	 let evtyp, hyps, chop =
	   match chop_product fs evtyp with
	   | Some t -> t, trunc_named_context fs hyps, fs
	   | None -> evtyp, hyps, 0
	 in
	 let loc, k = evar_source id evm in
	 let status = match k with Evar_kinds.QuestionMark o -> Some o | _ -> status in
	 let status, chop = match status with
	   | Some (Evar_kinds.Define true as stat) ->
	       if not (Int.equal chop fs) then Evar_kinds.Define false, None
	       else stat, Some chop
	   | Some s -> s, None
	   | None -> Evar_kinds.Define true, None
	 in
	 let tac = match Store.get ev.evar_extra evar_tactic with
	   | Some t ->
	       if Dyn.has_tag t "tactic" then
		 Some (Tacinterp.interp 
			  (Tacinterp.globTacticIn (Tacinterp.tactic_out t)))
	       else None
	   | None -> None
	 in
	 let info = { ev_name = (n, nstr);
		      ev_hyps = hyps; ev_status = status; ev_chop = chop;
		      ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
	 in (id, info) :: l)
      evn []
  in
  let t', _, transparent = (* Substitute evar refs in the term by variables *)
    subst_evar_constr evts 0 mkVar t 
  in
  let ty, _, _ = subst_evar_constr evts 0 mkVar ty in
  let evars = 
    List.map (fun (ev, info) ->
      let { ev_name = (_, name); ev_status = status;
	    ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
      in
      let status = match status with
	| Evar_kinds.Define true when Id.Set.mem name transparent ->
	  Evar_kinds.Define false
	| _ -> status
      in name, typ, src, status, deps, tac) evts
  in
  let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
  let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
    Array.of_list (List.rev evars), (evnames, evmap), t', ty

let tactics_module = ["Program";"Tactics"]
let safe_init_constant md name () =
  Coqlib.check_required_library ("Coq"::md);
  Coqlib.gen_constant "Obligations" md name
let hide_obligation = safe_init_constant tactics_module "obligation"

let pperror cmd = Errors.errorlabstrm "Program" cmd
let error s = pperror (str s)

let reduce c =
  Reductionops.clos_norm_flags Closure.betaiota (Global.env ()) Evd.empty c

exception NoObligations of Id.t option

let explain_no_obligations = function
    Some ident -> str "No obligations for program " ++ str (Id.to_string ident)
  | None -> str "No obligations remaining"

type obligation_info =
    (Names.Id.t * Term.types * Evar_kinds.t Loc.located *
     Evar_kinds.obligation_definition_status * Int.Set.t * unit Proofview.tactic option) array

type 'a obligation_body = 
  | DefinedObl of 'a
  | TermObl of constr

type obligation =
  { obl_name : Id.t;
    obl_type : types;
    obl_location : Evar_kinds.t Loc.located;
    obl_body : constant obligation_body option;
    obl_status : Evar_kinds.obligation_definition_status;
    obl_deps : Int.Set.t;
    obl_tac : unit Proofview.tactic option;
  }

type obligations = (obligation array * int)

type fixpoint_kind =
  | IsFixpoint of (Id.t Loc.located option * Constrexpr.recursion_order_expr) list
  | IsCoFixpoint

type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list

type program_info = {
  prg_name: Id.t;
  prg_body: constr;
  prg_type: constr;
  prg_ctx:  Evd.evar_universe_context;
  prg_obligations: obligations;
  prg_deps : Id.t list;
  prg_fixkind : fixpoint_kind option ;
  prg_implicits : (Constrexpr.explicitation * (bool * bool * bool)) list;
  prg_notations : notations ;
  prg_kind : definition_kind;
  prg_reduce : constr -> constr;
  prg_hook : unit Lemmas.declaration_hook;
}

let assumption_message = Declare.assumption_message

let (set_default_tactic, get_default_tactic, print_default_tactic) = 
  Tactic_option.declare_tactic_option "Program tactic"

(* true = All transparent, false = Opaque if possible *)
let proofs_transparency = ref true

let set_proofs_transparency = (:=) proofs_transparency
let get_proofs_transparency () = !proofs_transparency

open Goptions

let _ =
  declare_bool_option
    { optsync  = true;
      optdepr  = false;
      optname  = "transparency of Program obligations";
      optkey   = ["Transparent";"Obligations"];
      optread  = get_proofs_transparency;
      optwrite = set_proofs_transparency; }

(* true = hide obligations *)
let hide_obligations = ref false

let set_hide_obligations = (:=) hide_obligations
let get_hide_obligations () = !hide_obligations

let _ =
  declare_bool_option
    { optsync  = true;
      optdepr  = false;
      optname  = "Hidding of Program obligations";
      optkey   = ["Hide";"Obligations"];
      optread  = get_hide_obligations;
      optwrite = set_hide_obligations; }

let shrink_obligations = ref false

let set_shrink_obligations = (:=) shrink_obligations
let get_shrink_obligations () = !shrink_obligations

let _ =
  declare_bool_option
    { optsync  = true;
      optdepr  = false;
      optname  = "Shrinking of Program obligations";
      optkey   = ["Shrink";"Obligations"];
      optread  = get_shrink_obligations;
      optwrite = set_shrink_obligations; }

let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type

let get_body obl = 
  match obl.obl_body with
  | None -> assert false
  | Some (DefinedObl c) ->
    let ctx = Environ.constant_context (Global.env ()) c in
    let pc = (c, Univ.UContext.instance ctx) in
      DefinedObl pc
  | Some (TermObl c) -> 
      TermObl c

let get_obligation_body expand obl =
  let c = get_body obl in
  let c' = 
    if expand && obl.obl_status == Evar_kinds.Expand then
      (match c with
      | DefinedObl pc -> constant_value_in (Global.env ()) pc
      | TermObl c -> c)
    else (match c with
    | DefinedObl pc -> mkConstU pc
    | TermObl c -> c)
  in c'

let obl_substitution expand obls deps =
  Int.Set.fold
    (fun x acc ->
       let xobl = obls.(x) in
       let oblb =
	 try get_obligation_body expand xobl
	 with e when Errors.noncritical e -> assert false
       in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
    deps []

let subst_deps expand obls deps t =
  let osubst = obl_substitution expand obls deps in
    (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)

let rec prod_app t n =
  match kind_of_term (strip_outer_cast t) with
    | Prod (_,_,b) -> subst1 n b
    | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
    | _ ->
	errorlabstrm "prod_app"
	  (str"Needed a product, but didn't find one" ++ fnl ())


(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
let prod_applist t nL = List.fold_left prod_app t nL

let replace_appvars subst =
  let rec aux c = 
    let f, l = decompose_app c in
      if isVar f then
	try
	  let c' = List.map (map_constr aux) l in
	  let (t, b) = Id.List.assoc (destVar f) subst in
	    mkApp (delayed_force hide_obligation, 
		   [| prod_applist t c'; applistc b c' |])
	with Not_found -> map_constr aux c
      else map_constr aux c
  in map_constr aux
       
let subst_prog expand obls ints prg =
  let subst = obl_substitution expand obls ints in
    if get_hide_obligations () then
      (replace_appvars subst prg.prg_body,
       replace_appvars subst ((* Termops.refresh_universes *) prg.prg_type))
    else 
      let subst' = List.map (fun (n, (_, b)) -> n, b) subst in
	(Vars.replace_vars subst' prg.prg_body,
	 Vars.replace_vars subst' ((* Termops.refresh_universes *) prg.prg_type))

let subst_deps_obl obls obl =
  let t' = subst_deps true obls obl.obl_deps obl.obl_type in
    { obl with obl_type = t' }

module ProgMap = Map.Make(Id)

let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)

let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []

let map_cardinal m =
  let i = ref 0 in
    ProgMap.iter (fun _ _ -> incr i) m;
    !i

exception Found of program_info

let map_first m =
  try
    ProgMap.iter (fun _ v -> raise (Found v)) m;
    assert(false)
  with Found x -> x

let from_prg : program_info ProgMap.t ref =
  Summary.ref ProgMap.empty ~name:"program-tcc-table"

let close sec =
  if not (ProgMap.is_empty !from_prg) then
    let keys = map_keys !from_prg in
      errorlabstrm "Program" 
	(str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
	   prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++
	   (str (if Int.equal (List.length keys) 1 then " has " else " have ") ++
	      str "unsolved obligations"))

let input : program_info ProgMap.t -> obj =
  declare_object
    { (default_object "Program state") with
      cache_function = (fun (na, pi) -> from_prg := pi);
      load_function = (fun _ (_, pi) -> from_prg := pi);
      discharge_function = (fun _ -> close "section"; None);
      classify_function = (fun _ -> close "module"; Dispose) }
    
open Evd

let progmap_remove prg =
  Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg))
  
let progmap_add n prg =
  Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg))

let progmap_replace prg' = 
  Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg))

let rec intset_to = function
    -1 -> Int.Set.empty
  | n -> Int.Set.add n (intset_to (pred n))

let subst_body expand prg =
  let obls, _ = prg.prg_obligations in
  let ints = intset_to (pred (Array.length obls)) in
    subst_prog expand obls ints prg

let declare_definition prg =
  let body, typ = subst_body true prg in
  let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
    (Evd.evar_universe_context_subst prg.prg_ctx) in
  let ce =
    definition_entry ~types:(nf typ) ~poly:(pi2 prg.prg_kind) 
      ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
  in
    progmap_remove prg;
    !declare_definition_ref prg.prg_name 
      prg.prg_kind ce prg.prg_implicits
      (Lemmas.mk_hook (fun l r ->
         Lemmas.call_hook (fun exn -> exn) prg.prg_hook l r; r))

open Pp

let rec lam_index n t acc =
  match kind_of_term t with
    | Lambda (Name n', _, _) when Id.equal n n' ->
      acc
    | Lambda (_, _, b) ->
	lam_index n b (succ acc)
    | _ -> raise Not_found

let compute_possible_guardness_evidences (n,_) fixbody fixtype =
  match n with
  | Some (loc, n) -> [lam_index n fixbody 0]
  | None ->
      (* If recursive argument was not given by user, we try all args.
	 An earlier approach was to look only for inductive arguments,
	 but doing it properly involves delta-reduction, and it finally
         doesn't seem to worth the effort (except for huge mutual
	 fixpoints ?) *)
      let m = nb_prod fixtype in
      let ctx = fst (decompose_prod_n_assum m fixtype) in
	List.map_i (fun i _ -> i) 0 ctx

let mk_proof c = ((c, Univ.ContextSet.empty), Declareops.no_seff)

let declare_mutual_definition l =
  let len = List.length l in
  let first = List.hd l in
  let fixdefs, fixtypes, fiximps =
    List.split3
      (List.map (fun x -> 
	let subs, typ = (subst_body true x) in
	let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in
	let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in
	  x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
  in
(*   let fixdefs = List.map reduce_fix fixdefs in *)
  let fixkind = Option.get first.prg_fixkind in
  let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
  let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
  let (local,poly,kind) = first.prg_kind in
  let fixnames = first.prg_deps in
  let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in
  let indexes, fixdecls =
    match fixkind with
      | IsFixpoint wfl ->
	  let possible_indexes =
	    List.map3 compute_possible_guardness_evidences
              wfl fixdefs fixtypes in
	  let indexes = 
            Pretyping.search_guard Loc.ghost (Global.env())
              possible_indexes fixdecls in
          Some indexes, 
          List.map_i (fun i _ ->
            mk_proof (mkFix ((indexes,i),fixdecls))) 0 l
      | IsCoFixpoint ->
          None,
          List.map_i (fun i _ ->
            mk_proof (mkCoFix (i,fixdecls))) 0 l
  in
  (* Declare the recursive definitions *)
  let ctx = Evd.evar_context_universe_context first.prg_ctx in
  let kns = List.map4 (!declare_fix_ref (local, poly, kind) ctx) 
    fixnames fixdecls fixtypes fiximps in
    (* Declare notations *)
    List.iter Metasyntax.add_notation_interpretation first.prg_notations;
    Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
    let gr = List.hd kns in
    let kn = match gr with ConstRef kn -> kn | _ -> assert false in
      Lemmas.call_hook (fun exn -> exn) first.prg_hook local gr;
      List.iter progmap_remove l; kn

let shrink_body c = 
  let ctx, b = decompose_lam c in
  let b', n, args = 
    List.fold_left (fun (b, i, args) (n,t) ->
      if noccurn 1 b then 
	subst1 mkProp b, succ i, args
      else mkLambda (n,t,b), succ i, mkRel i :: args)
     (b, 1, []) ctx
  in List.map (fun (c,t) -> (c,None,t)) ctx, b', Array.of_list args
      
let declare_obligation prg obl body ty uctx =
  let body = prg.prg_reduce body in
  let ty = Option.map prg.prg_reduce ty in
  match obl.obl_status with
  | Evar_kinds.Expand -> { obl with obl_body = Some (TermObl body) }
  | Evar_kinds.Define opaque ->
      let opaque = if get_proofs_transparency () then false else opaque in
      let poly = pi2 prg.prg_kind in
      let ctx, body, args = 
	if get_shrink_obligations () && not poly then
	  shrink_body body else [], body, [||] 
      in
      let ce = 
        { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff);
          const_entry_secctx = None;
	  const_entry_type = if List.is_empty ctx then ty else None;
	  const_entry_polymorphic = poly;
	  const_entry_universes = uctx;
	  const_entry_opaque = opaque;
          const_entry_inline_code = false;
          const_entry_feedback = None;
      } in
    (** ppedrot: seems legit to have obligations as local *)
      let constant = Declare.declare_constant obl.obl_name ~local:true
	(DefinitionEntry ce,IsProof Property)
      in
	if not opaque then
	  Hints.add_hints false [Id.to_string prg.prg_name]
	    (Hints.HintsUnfoldEntry [EvalConstRef constant]);
	definition_message obl.obl_name;
	{ obl with obl_body = 
	    if poly then 
	      Some (DefinedObl constant)
	    else
	      Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }

let init_prog_info n b t ctx deps fixkind notations obls impls kind reduce hook =
  let obls', b = 
    match b with
    | None ->
	assert(Int.equal (Array.length obls) 0);
	let n = Nameops.add_suffix n "_obligation" in
	  [| { obl_name = n; obl_body = None;
	       obl_location = Loc.ghost, Evar_kinds.InternalHole; obl_type = t;
	       obl_status = Evar_kinds.Expand; obl_deps = Int.Set.empty;
	       obl_tac = None } |],
	mkVar n
    | Some b ->
	Array.mapi
	  (fun i (n, t, l, o, d, tac) ->
            { obl_name = n ; obl_body = None; 
	      obl_location = l; obl_type = reduce t; obl_status = o;
	      obl_deps = d; obl_tac = tac })
	  obls, b
  in
    { prg_name = n ; prg_body = b; prg_type = reduce t; 
      prg_ctx = ctx; 
      prg_obligations = (obls', Array.length obls');
      prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
      prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; 
      prg_hook = hook; }

let get_prog name =
  let prg_infos = !from_prg in
    match name with
	Some n ->
	  (try ProgMap.find n prg_infos
	   with Not_found -> raise (NoObligations (Some n)))
      | None ->
	  (let n = map_cardinal prg_infos in
	     match n with
		 0 -> raise (NoObligations None)
	       | 1 -> map_first prg_infos
	       | _ -> 
                   error ("More than one program with unsolved obligations: "^
                    String.concat ", " 
                     (List.map string_of_id
                      (ProgMap.fold (fun k _ s -> k::s) prg_infos []))))

let get_any_prog () =
  let prg_infos = !from_prg in
  let n = map_cardinal prg_infos in
  if n > 0 then map_first prg_infos
  else raise (NoObligations None)

let get_prog_err n =
  try get_prog n with NoObligations id -> pperror (explain_no_obligations id)

let get_any_prog_err () =
  try get_any_prog () with NoObligations id -> pperror (explain_no_obligations id)

let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0

let all_programs () =
  ProgMap.fold (fun k p l -> p :: l) !from_prg []

type progress =
    | Remain of int
    | Dependent
    | Defined of global_reference

let obligations_message rem =
  if rem > 0 then
    if Int.equal rem 1 then
      Flags.if_verbose msg_info (int rem ++ str " obligation remaining")
    else
      Flags.if_verbose msg_info (int rem ++ str " obligations remaining")
  else
    Flags.if_verbose msg_info (str "No more obligations remaining")

let update_obls prg obls rem =
  let prg' = { prg with prg_obligations = (obls, rem) } in
    progmap_replace prg';
    obligations_message rem;
    if rem > 0 then Remain rem
    else (
      match prg'.prg_deps with
      | [] ->
	  let kn = declare_definition prg' in
	    progmap_remove prg';
	    Defined kn
      | l ->
	  let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
	    if List.for_all (fun x -> obligations_solved x) progs then
	      let kn = declare_mutual_definition progs in
		Defined (ConstRef kn)
	    else Dependent)

let is_defined obls x = not (Option.is_empty obls.(x).obl_body)

let deps_remaining obls deps =
  Int.Set.fold
    (fun x acc ->
      if is_defined obls x then acc
      else x :: acc)
    deps []

let dependencies obls n =
  let res = ref Int.Set.empty in
    Array.iteri
      (fun i obl ->
	if not (Int.equal i n) && Int.Set.mem n obl.obl_deps then
	  res := Int.Set.add i !res)
      obls;
    !res

let goal_kind poly = Decl_kinds.Local, poly, Decl_kinds.DefinitionBody Decl_kinds.Definition

let goal_proof_kind poly = Decl_kinds.Local, poly, Decl_kinds.Proof Decl_kinds.Lemma

let kind_of_obligation poly o =
  match o with
  | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly
  | _ -> goal_proof_kind poly

let not_transp_msg =
  str "Obligation should be transparent but was declared opaque." ++ spc () ++
    str"Use 'Defined' instead."

let error_not_transp () = pperror not_transp_msg

let rec string_of_list sep f = function
    [] -> ""
  | x :: [] -> f x
  | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl

(* Solve an obligation using tactics, return the corresponding proof term *)

let solve_by_tac name evi t poly ctx =
  let id = name in
  let concl = evi.evar_concl in
  (* spiwack: the status is dropped. *)
  let (entry,_,ctx') = Pfedit.build_constant_by_tactic 
    id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in
  let env = Global.env () in
  let entry = Term_typing.handle_entry_side_effects env entry in
  let body, eff = Future.force entry.Entries.const_entry_body in
  assert(Declareops.side_effects_is_empty eff);
  assert(Univ.ContextSet.is_empty (snd body));
  Inductiveops.control_only_guard (Global.env ()) (fst body);
  (fst body), entry.Entries.const_entry_type, ctx'

let rec solve_obligation prg num tac =
  let user_num = succ num in
  let obls, rem = prg.prg_obligations in
  let obl = obls.(num) in
    if not (Option.is_empty obl.obl_body) then
      pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")
    else
      match deps_remaining obls obl.obl_deps with
      | [] ->
          let obl = subst_deps_obl obls obl in
          let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
            let evd = Evd.from_env ~ctx:prg.prg_ctx Environ.empty_env in
            Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type
              (fun ctx' -> Lemmas.mk_hook (fun strength gr ->
		let cst = match gr with ConstRef cst -> cst | _ -> assert false in
		let obl =
		  let transparent = evaluable_constant cst (Global.env ()) in
		  let body =
		    match obl.obl_status with
		    | Evar_kinds.Expand ->
			if not transparent then error_not_transp ()
			else DefinedObl cst
		    | Evar_kinds.Define opaque ->
			if not opaque && not transparent then error_not_transp ()
			else DefinedObl cst
		  in
		    if transparent then
		      Hints.add_hints true [Id.to_string prg.prg_name]
			(Hints.HintsUnfoldEntry [EvalConstRef cst]);
		    { obl with obl_body = Some body }
		in
		let obls = Array.copy obls in
		let _ = obls.(num) <- obl in
		let ctx' = 
		  let ctx = 
		    match ctx' with
		    | None -> prg.prg_ctx
		    | Some ctx' -> ctx'
		  in
  		    if not (pi2 prg.prg_kind) (* Not polymorphic *) then
		      (* This context is already declared globally, we cannot 
			 instantiate the rigid variables anymore *) 
		      Evd.abstract_undefined_variables ctx
		    else ctx
		in
		let res = 
		  try update_obls 
			{prg with prg_body = prg.prg_body;
			  prg_type = prg.prg_type;
			  prg_ctx = ctx' }
			  
			obls (pred rem)
		  with e when Errors.noncritical e ->
                    pperror (Errors.print (Cerrors.process_vernac_interp_error e))
		in
		  match res with
		  | Remain n when n > 0 ->
		      let deps = dependencies obls num in
			if not (Int.Set.is_empty deps) then
			  ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps)
		  | _ -> ()));
	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
		     Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type);
	    ignore (Pfedit.by (snd (get_default_tactic ())));
	    Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
      | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
		      ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))

and obligation (user_num, name, typ) tac =
  let num = pred user_num in
  let prg = get_prog_err name in
  let obls, rem = prg.prg_obligations in
    if num < Array.length obls then
      let obl = obls.(num) in
	match obl.obl_body with
	    None -> solve_obligation prg num tac
	  | Some r -> error "Obligation already solved"
    else error (sprintf "Unknown obligation number %i" (succ num))


and solve_obligation_by_tac prg obls i tac =
  let obl = obls.(i) in
    match obl.obl_body with
    | Some _ -> false
    | None ->
	try
	  if List.is_empty (deps_remaining obls obl.obl_deps) then
	    let obl = subst_deps_obl obls obl in
	    let tac =
	      match tac with
	      | Some t -> t
	      | None ->
		  match obl.obl_tac with
		  | Some t -> t
		  | None -> snd (get_default_tactic ())
	    in
	    let t, ty, ctx = 
	      solve_by_tac obl.obl_name (evar_of_obligation obl) tac 
	        (pi2 !prg.prg_kind) !prg.prg_ctx
	    in
	    let uctx = Evd.evar_context_universe_context ctx in
	      prg := {!prg with prg_ctx = ctx};
	      obls.(i) <- declare_obligation !prg obl t ty uctx;
	      true
	  else false
	with e when Errors.noncritical e ->
          let e = Errors.push e in
          match e with
	  | Refiner.FailError (_, s) ->
	      user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
          | e -> false

and solve_prg_obligations prg ?oblset tac =
  let obls, rem = prg.prg_obligations in
  let rem = ref rem in
  let obls' = Array.copy obls in
  let set = ref Int.Set.empty in
  let p = match oblset with
    | None -> (fun _ -> true)
    | Some s -> set := s;
      (fun i -> Int.Set.mem i !set)
  in
  let prg = ref prg in
  let _ =
    Array.iteri (fun i x ->
      if p i && solve_obligation_by_tac prg obls' i tac then
 	let deps = dependencies obls i in
 	  (set := Int.Set.union !set deps;
 	   decr rem))
      obls'
  in
    update_obls !prg obls' !rem

and solve_obligations n tac =
  let prg = get_prog_err n in
    solve_prg_obligations prg tac

and solve_all_obligations tac =
  ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg

and try_solve_obligation n prg tac =
  let prg = get_prog prg in
  let obls, rem = prg.prg_obligations in
  let obls' = Array.copy obls in
  let prgref = ref prg in
    if solve_obligation_by_tac prgref obls' n tac then
      ignore(update_obls !prgref obls' (pred rem));

and try_solve_obligations n tac =
  try ignore (solve_obligations n tac) with NoObligations _ -> ()

and auto_solve_obligations n ?oblset tac : progress =
  Flags.if_verbose msg_info (str "Solving obligations automatically...");
  try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent

open Pp
let show_obligations_of_prg ?(msg=true) prg =
  let n = prg.prg_name in
  let obls, rem = prg.prg_obligations in
  let showed = ref 5 in
    if msg then msg_info (int rem ++ str " obligation(s) remaining: ");
    Array.iteri (fun i x ->
		   match x.obl_body with
		   | None ->
		       if !showed > 0 then (
			 decr showed;
			 msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
				   str "of" ++ spc() ++ str (Id.to_string n) ++ str ":" ++ spc () ++
				   hov 1 (Printer.pr_constr_env (Global.env ()) Evd.empty x.obl_type ++
					    str "." ++ fnl ())))
		   | Some _ -> ())
      obls

let show_obligations ?(msg=true) n =
  let progs = match n with
    | None -> all_programs ()
    | Some n ->
	try [ProgMap.find n !from_prg]
	with Not_found -> raise (NoObligations (Some n))
  in List.iter (show_obligations_of_prg ~msg) progs

let show_term n =
  let prg = get_prog_err n in
  let n = prg.prg_name in
    (str (Id.to_string n) ++ spc () ++ str":" ++ spc () ++
	     Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
	    ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)

let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) obls =
  let info = str (Id.to_string n) ++ str " has type-checked" in
  let prg = init_prog_info n term t ctx [] None [] obls implicits kind reduce hook in
  let obls,_ = prg.prg_obligations in
  if Int.equal (Array.length obls) 0 then (
    Flags.if_verbose msg_info (info ++ str ".");
    let cst = declare_definition prg in
      Defined cst)
  else (
    let len = Array.length obls in
    let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
      progmap_add n prg;
      let res = auto_solve_obligations (Some n) tactic in
	match res with
	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
	| _ -> res)

let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
    ?(hook=Lemmas.mk_hook (fun _ _ -> ())) notations fixkind =
  let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
    List.iter
    (fun  (n, b, t, imps, obls) ->
     let prg = init_prog_info n (Some b) t ctx deps (Some fixkind) 
       notations obls imps kind reduce hook 
     in progmap_add n prg) l;
    let _defined =
      List.fold_left (fun finished x ->
	if finished then finished
	else
	  let res = auto_solve_obligations (Some x) tactic in
	    match res with
	    | Defined _ -> 
		(* If one definition is turned into a constant, 
		   the whole block is defined. *) true
	    | _ -> false)
	false deps
    in ()

let admit_prog prg =
  let obls, rem = prg.prg_obligations in
  let obls = Array.copy obls in
    Array.iteri 
      (fun i x ->
        match x.obl_body with
        | None ->
            let x = subst_deps_obl obls x in
	    let ctx = Evd.evar_context_universe_context prg.prg_ctx in
            let kn = Declare.declare_constant x.obl_name ~local:true
              (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
            in
              assumption_message x.obl_name;
              obls.(i) <- { x with obl_body = Some (DefinedObl kn) }
        | Some _ -> ())
      obls;
    ignore(update_obls prg obls 0)

let rec admit_all_obligations () =
  let prg = try Some (get_any_prog ()) with NoObligations _ -> None in
  match prg with
  | None -> ()
  | Some prg ->
    admit_prog prg;
    admit_all_obligations ()

let admit_obligations n =
  match n with
  | None -> admit_all_obligations ()
  | Some _ ->
    let prg = get_prog_err n in
    admit_prog prg

let next_obligation n tac =
  let prg = match n with
  | None -> get_any_prog_err ()
  | Some _ -> get_prog_err n
  in
  let obls, rem = prg.prg_obligations in
  let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in
  let i = match Array.findi is_open obls with
  | Some i -> i
  | None -> anomaly (Pp.str "Could not find a solvable obligation.")
  in
  solve_obligation prg i tac

let init_program () =
  Coqlib.check_required_library Coqlib.datatypes_module_name;
  Coqlib.check_required_library ["Coq";"Init";"Specif"];
  Coqlib.check_required_library ["Coq";"Program";"Tactics"]


let set_program_mode c =
  if c then
    if !Flags.program_mode then ()
    else begin
      init_program ();
      Flags.program_mode := true;
    end