aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/obligations.ml
blob: 1ab24b670b6f56e3027df71039c45a6c403e902d (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
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
open Printf
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 Constr
open Vars
open Names
open Evd
open Pp
open CErrors
open Util

module NamedDecl = Context.Named.Declaration

let get_fix_exn, stm_get_fix_exn = Hook.make ()

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 key None)
  (Evd.undefined_map evm)

type oblinfo =
  { ev_name: int * Id.t;
    ev_hyps: Context.Named.t;
    ev_status: bool * 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 }

(** 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 Constr.kind 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 =
             let open Context.Named.Declaration in
	     match hyps, args with
		 (LocalAssum _ :: tlh), (c :: tla) ->
		   aux tlh tla ((substrec (depth, fixrels) c) :: acc)
	       | (LocalDef _ :: tlh), (_ :: tla) ->
		   aux tlh tla acc
	       | [], [] -> acc
	       | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
	  in aux hyps args []
	in
	  if List.exists
            (fun x -> match Constr.kind 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 _ ->
	Constr.map_with_binders succfix substrec (depth, 1 :: fixrels) c
    | _ -> Constr.map_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 Constr.kind c with
    | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
    | _ -> Constr.map_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 open Context.Named.Declaration in
  let rec aux acc n = function
      decl :: tl ->
	let t', s, trans = subst_evar_constr evs n mkVar (NamedDecl.get_type decl) in
	let t'' = subst_vars acc 0 t' in
	let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in
	let s' = Int.Set.union s s' in
	let trans' = Id.Set.union trans trans' in
	  (match decl with
            | LocalDef (id,c,_) ->
		let c', s'', trans'' = subst_evar_constr evs n mkVar c in
		let c' = subst_vars acc 0 c' in
		  mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
		Int.Set.union s'' s',
		Id.Set.union trans'' trans'
	    | LocalAssum (id,_) ->
		mkNamedProd_or_LetIn (LocalAssum (id, 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 =
  let pop t = Vars.lift (-1) t in
  if Int.equal n 0 then Some t
  else
    match Constr.kind t with
      | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (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 " ^ Pp.string_of_ppcmds @@ Evar.print 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.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 hyps = EConstr.Unsafe.to_named_context hyps in
         let concl = EConstr.Unsafe.to_constr ev.evar_concl in
         let evtyp, deps, transp = etype_of_evar l hyps 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,_) -> o
           | _ -> match status with
                 | Some o -> o
                 | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))
         in
         let force_status, status, chop = match status with
	   | Evar_kinds.Define true as stat ->
	      if not (Int.equal chop fs) then true, Evar_kinds.Define false, None
	      else false, stat, Some chop
	   | s -> false, s, None
	 in
	 let info = { ev_name = (n, nstr);
		      ev_hyps = hyps; ev_status = force_status, status; ev_chop = chop;
		      ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = None }
	 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 = force_status, status;
	    ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
      in
      let force_status, status = match status with
	| Evar_kinds.Define true when Id.Set.mem name transparent ->
	  true, Evar_kinds.Define false
	| _ -> force_status, status
      in name, typ, src, (force_status, 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);
  UnivGen.constr_of_global (Coqlib.coq_reference "Obligations" md name)
let hide_obligation = safe_init_constant tactics_module "obligation"

let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
let error s = pperror (str s)

let reduce c =
  let env = Global.env () in
  let sigma = Evd.from_env env in
  EConstr.Unsafe.to_constr (Reductionops.clos_norm_flags CClosure.betaiota env sigma (EConstr.of_constr c))

exception NoObligations of Id.t option

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

type obligation_info =
    (Names.Id.t * types * Evar_kinds.t Loc.located *
       (bool * 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 : pconstant obligation_body option;
    obl_status : bool * 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 (lident option * Constrexpr.recursion_order_expr) list
  | IsCoFixpoint

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

type program_info_aux = {
  prg_name: Id.t;
  prg_body: constr;
  prg_type: constr;
  prg_ctx:  UState.t;
  prg_univdecl: UState.universe_decl;
  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 : (UState.t -> unit) Lemmas.declaration_hook;
  prg_opaque : bool;
  prg_sign: named_context_val;
}

type program_info = program_info_aux CEphemeron.key

let get_info x =
  try CEphemeron.get x
  with CEphemeron.InvalidKey ->
    CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker.")

let assumption_message = Declare.assumption_message

let default_tactic = ref (Proofview.tclUNIT ())

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

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

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

let shrink_obligations = ref true

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

let _ =
  declare_bool_option
    { optdepr  = true; (* remove in 8.8 *)
      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 ()) (EConstr.of_constr o.obl_type)

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

let obl_substitution expand obls deps =
  Int.Set.fold
    (fun x acc ->
       let xobl = obls.(x) in
       match get_obligation_body expand xobl with
       | None -> acc
       | Some oblb -> (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 Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (** FIXME *) with
    | Prod (_,_,b) -> subst1 n b
    | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
    | _ ->
	user_err ~hdr:"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 (Constr.map 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 -> Constr.map aux c
      else Constr.map aux c
  in Constr.map 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 = Id.Map

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

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

let from_prg, program_tcc_summary_tag =
  Summary.ref_tag ProgMap.empty ~name:"program-tcc-table"

let close sec =
  if not (ProgMap.is_empty !from_prg) then
    let keys = map_keys !from_prg in
      user_err ~hdr:"Program" 
	(str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
	   prlist_with_sep spc (fun x -> Id.print 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 = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None)
    (UState.subst prg.prg_ctx) in
  let opaque = prg.prg_opaque in
  let fix_exn = Hook.get get_fix_exn () in
  let typ = nf typ in
  let body = nf body in
  let env = Global.env () in
  let uvars = Univ.LSet.union
      (Univops.universes_of_constr env typ)
      (Univops.universes_of_constr env body) in
  let uctx = UState.restrict prg.prg_ctx uvars in
  let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl in
  let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
  let () = progmap_remove prg in
  let ubinders = UState.universe_binders uctx in
  DeclareDef.declare_definition prg.prg_name
    prg.prg_kind ce ubinders prg.prg_implicits
    (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r uctx; r))

let rec lam_index n t acc =
  match Constr.kind 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 { CAst.loc; v = 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 = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (** FIXME *) 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), Safe_typing.empty_private_constants)

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 env = Global.env () in
        let sigma = Evd.from_env env in
        let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
        let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
	let term = EConstr.Unsafe.to_constr term in
	let typ = EConstr.Unsafe.to_constr 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 opaque = first.prg_opaque 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 (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 univs = UState.const_univ_entry ~poly first.prg_ctx in
  let fix_exn = Hook.get get_fix_exn () in
  let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
    fixnames fixdecls fixtypes fiximps in
    (* Declare notations *)
    List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
    Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
    let gr = List.hd kns in
    Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
    List.iter progmap_remove l; gr

let decompose_lam_prod c ty =
  let open Context.Rel.Declaration in
  let rec aux ctx c ty =
    match Constr.kind c, Constr.kind ty with
    | LetIn (x, b, t, c), LetIn (x', b', t', ty)
	 when Constr.equal b b' && Constr.equal t t' ->
       let ctx' = Context.Rel.add (LocalDef (x,b',t')) ctx in
       aux ctx' c ty
    | _, LetIn (x', b', t', ty) ->
       let ctx' = Context.Rel.add (LocalDef (x',b',t')) ctx in
       aux ctx' (lift 1 c) ty
    | LetIn (x, b, t, c), _ ->
       let ctx' = Context.Rel.add (LocalDef (x,b,t)) ctx in
       aux ctx' c (lift 1 ty)
    | Lambda (x, b, t), Prod (x', b', t')
       (* By invariant, must be convertible *) ->
       let ctx' = Context.Rel.add (LocalAssum (x,b')) ctx in
       aux ctx' t t'
    | Cast (c, _, _), _ -> aux ctx c ty
    | _, _ -> ctx, c, ty
  in aux Context.Rel.empty c ty

let shrink_body c ty =
  let ctx, b, ty =
    match ty with
    | None ->
       let ctx, b = decompose_lam_assum c in
       ctx, b, None
    | Some ty ->
       let ctx, b, ty = decompose_lam_prod c ty in
       ctx, b, Some ty
  in
  let b', ty', n, args =
    List.fold_left (fun (b, ty, i, args) decl ->
        if noccurn 1 b && Option.cata (noccurn 1) true ty then
	  subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args
	else
          let open Context.Rel.Declaration in
	  let args = if is_local_assum decl then mkRel i :: args else args in
          mkLambda_or_LetIn decl b, Option.map (mkProd_or_LetIn decl) ty,
	  succ i, args)
     (b, ty, 1, []) ctx
  in ctx, b', ty', Array.of_list args

let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]

let add_hint local prg cst =
  Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst)

let it_mkLambda_or_LetIn_or_clean t ctx =
  let open Context.Rel.Declaration in
  let fold t decl =
    if is_local_assum decl then mkLambda_or_LetIn decl t
    else
      if noccurn 1 t then subst1 mkProp t
      else mkLambda_or_LetIn decl t
  in
  Context.Rel.fold_inside fold ctx ~init:t

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 -> false, { obl with obl_body = Some (TermObl body) }
  | force, Evar_kinds.Define opaque ->
      let opaque = not force && opaque in
      let poly = pi2 prg.prg_kind in
      let ctx, body, ty, args =
	if get_shrink_obligations () && not poly then
	  shrink_body body ty else [], body, ty, [||]
      in
      let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
      let ce =
        { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
          const_entry_secctx = None;
	  const_entry_type = ty;
          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 add_hint (Locality.make_section_locality None) prg constant;
      definition_message obl.obl_name;
      let body = match uctx with
        | Polymorphic_const_entry uctx ->
          Some (DefinedObl (constant, Univ.UContext.instance uctx))
        | Monomorphic_const_entry _ ->
          Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx))
      in
      true, { obl with obl_body = body }

let init_prog_info ?(opaque = false) sign n udecl 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.tag Evar_kinds.InternalHole; obl_type = t;
	       obl_status = false, 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 = t; obl_status = o;
	      obl_deps = d; obl_tac = tac })
	  obls, b
  in
  let ctx = UState.make_flexible_nonalgebraic ctx in
    { prg_name = n ; prg_body = b; prg_type = reduce t; 
      prg_ctx = ctx; prg_univdecl = udecl;
      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; prg_opaque = opaque;
      prg_sign = sign }

let map_cardinal m =
  let i = ref 0 in
  ProgMap.iter (fun _ v ->
		if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m;
  !i

exception Found of program_info

let map_first m =
  try
    ProgMap.iter (fun _ v ->
		  if snd (CEphemeron.get v).prg_obligations > 0 then
		    raise (Found v)) m;
    assert(false)
  with Found x -> x

let get_prog name =
  let prg_infos = !from_prg in
    match name with
	Some n ->
	  (try get_info (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 -> get_info (map_first prg_infos)
	       | _ ->
                let progs = Id.Set.elements (ProgMap.domain prg_infos) in
                let prog = List.hd progs in
                let progs = prlist_with_sep pr_comma Id.print progs in
                user_err 
                  (str "More than one program with unsolved obligations: " ++ progs
                  ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print prog ++ str "\""))

let get_any_prog () =
  let prg_infos = !from_prg in
  let n = map_cardinal prg_infos in
  if n > 0 then get_info (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 GlobRef.t

let obligations_message rem =
  if rem > 0 then
    if Int.equal rem 1 then
      Flags.if_verbose Feedback.msg_info (int rem ++ str " obligation remaining")
    else
      Flags.if_verbose Feedback.msg_info (int rem ++ str " obligations remaining")
  else
    Flags.if_verbose Feedback.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 -> get_info (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 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 err_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
  (* spiwack: the status is dropped. *)
  let (entry,_,ctx') = Pfedit.build_constant_by_tactic
    id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in
  let env = Global.env () in
  let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
  let body, () = Future.force entry.const_entry_body in
  let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in
  Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body));
  (fst body), entry.const_entry_type, Evd.evar_universe_context ctx'

let obligation_terminator name num guard hook auto pf =
  let open Proof_global in
  let term = Lemmas.universe_proof_terminator guard hook in
  match pf with
  | Admitted _ -> apply_terminator term pf
  | Proved (opq, id, proof) ->
    let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in
    let env = Global.env () in
    let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
    let ty = entry.Entries.const_entry_type in
    let (body, cstr), () = Future.force entry.Entries.const_entry_body in
    let sigma = Evd.from_ctx uctx in
    let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
    Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body);
    (** Declare the obligation ourselves and drop the hook *)
    let prg = get_info (ProgMap.find name !from_prg) in
    (** Ensure universes are substituted properly in body and type *)
    let body = EConstr.to_constr sigma (EConstr.of_constr body) in
    let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in
    let ctx = Evd.evar_universe_context sigma in
    let obls, rem = prg.prg_obligations in
    let obl = obls.(num) in
    let status =
      match obl.obl_status, opq with
      | (_, Evar_kinds.Expand), Opaque -> err_not_transp ()
      | (true, _), Opaque -> err_not_transp ()
      | (false, _), Opaque -> Evar_kinds.Define true
      | (_, Evar_kinds.Define true), Transparent ->
        Evar_kinds.Define false
      | (_, status), Transparent -> status
    in
    let obl = { obl with obl_status = false, status } in
    let ctx =
      if pi2 prg.prg_kind then ctx
      else UState.union prg.prg_ctx ctx
    in
    let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
    let (_, obl) = declare_obligation prg obl body ty uctx in
    let obls = Array.copy obls in
    let _ = obls.(num) <- obl in
    let prg_ctx =
      if pi2 (prg.prg_kind) then (* Polymorphic *)
        (** We merge the new universes and constraints of the
            polymorphic obligation with the existing ones *)
        UState.union prg.prg_ctx ctx
      else
        (** The first obligation declares the univs of the constant,
            each subsequent obligation declares its own additional
            universes and constraints if any *)
        UState.make (Global.universes ())
    in
    let prg = { prg with prg_ctx } in
    try
      ignore (update_obls prg obls (pred rem));
      if pred rem > 0 then
        begin
          let deps = dependencies obls num in
          if not (Int.Set.is_empty deps) then
            ignore (auto (Some name) None deps)
        end
    with e when CErrors.noncritical e ->
      let e = CErrors.push e in
      pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))

let obligation_hook prg obl num auto ctx' _ gr =
  let obls, rem = prg.prg_obligations in
  let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in
  let transparent = evaluable_constant cst (Global.env ()) in
  let () = match obl.obl_status with
      (true, Evar_kinds.Expand) 
    | (true, Evar_kinds.Define true) ->
       if not transparent then err_not_transp ()
    | _ -> ()
in
  let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
  let inst, ctx' =
    if not (pi2 prg.prg_kind) (* Not polymorphic *) then
      (* The universe context was declared globally, we continue
         from the new global environment. *)
      let evd = Evd.from_env (Global.env ()) in
      let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in
      Univ.Instance.empty, Evd.evar_universe_context ctx'
    else
      (* We get the right order somehow, but surely it could be enforced in a clearer way. *)
      let uctx = UState.context ctx' in
      Univ.UContext.instance uctx, ctx'
  in
  let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in
  let () = if transparent then add_hint true prg cst in
  let obls = Array.copy obls in
  let _ = obls.(num) <- obl in
  let prg = { prg with prg_ctx = ctx' } in
  let () =
    try ignore (update_obls prg obls (pred rem))
    with e when CErrors.noncritical e ->
      let e = CErrors.push e in
      pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
  in
  if pred rem > 0 then begin
    let deps = dependencies obls num in
    if not (Int.Set.is_empty deps) then
      ignore (auto (Some prg.prg_name) None deps)
  end

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
  let remaining = deps_remaining obls obl.obl_deps in
  let () =
    if not (Option.is_empty obl.obl_body) then
      pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.");
    if not (List.is_empty remaining) then
      pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
        ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining));
  in
  let obl = subst_deps_obl obls obl in
  let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in
  let evd = Evd.from_ctx prg.prg_ctx in
  let evd = Evd.update_sigma_env evd (Global.env ()) in
  let auto n tac oblset = auto_solve_obligations n ~oblset tac in
  let terminator guard hook =
    Proof_global.make_terminator
      (obligation_terminator prg.prg_name num guard hook auto) in
  let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
  let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator hook in
  let _ = Pfedit.by !default_tactic in
  Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac

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 >= 0 && 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 _ -> None
    | 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 -> !default_tactic
	    in
	    let evd = Evd.from_ctx prg.prg_ctx in
	    let evd = Evd.update_sigma_env evd (Global.env ()) in
	    let t, ty, ctx =
              solve_by_tac obl.obl_name (evar_of_obligation obl) tac
                (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
            in
            let uctx = if pi2 prg.prg_kind
              then Polymorphic_const_entry (UState.context ctx)
              else Monomorphic_const_entry (UState.context_set ctx)
            in
            let prg = {prg with prg_ctx = ctx} in
            let def, obl' = declare_obligation prg obl t ty uctx in
              obls.(i) <- obl';
	      if def && not (pi2 prg.prg_kind) then (
	        (* Declare the term constraints with the first obligation only *)
	        let evd = Evd.from_env (Global.env ()) in
	        let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in
		let ctx' = Evd.evar_universe_context evd in
		  Some {prg with prg_ctx = ctx'})
	      else Some prg
	  else None
	with e when CErrors.noncritical e ->
          let (e, _) = CErrors.push e in
          match e with
	  | Refiner.FailError (_, s) ->
	      user_err ?loc:(fst obl.obl_location) ~hdr:"solve_obligation" (Lazy.force s)
          | e -> None (* FIXME really ? *)

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 prgref = ref prg in
  let _ =
    Array.iteri (fun i x ->
      if p i then
        match solve_obligation_by_tac !prgref obls' i tac with
	| None -> ()
 	| Some prg' ->
	   prgref := prg';
	   let deps = dependencies obls i in
 	   (set := Int.Set.union !set deps;
 	    decr rem))
      obls'
  in
    update_obls !prgref 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 (get_info 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
    match solve_obligation_by_tac prg obls' n tac with
    | Some prg' -> ignore(update_obls prg' obls' (pred rem))
    | None -> ()

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 Feedback.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 Feedback.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;
			 let x = subst_deps_obl obls x in
                         let env = Global.env () in
                         let sigma = Evd.from_env env in
			 Feedback.msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
				   str "of" ++ spc() ++ Id.print n ++ str ":" ++ spc () ++
                                   hov 1 (Printer.pr_constr_env env sigma 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 (fun x -> show_obligations_of_prg ~msg (get_info x)) progs

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

let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
                   ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
  let sign = Decls.initialize_named_context_for_proof () in
  let info = Id.print n ++ str " has type-checked" in
  let prg = init_prog_info sign ~opaque n univdecl 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 Feedback.msg_info (info ++ str ".");
    let cst = declare_definition prg in
      Defined cst)
  else (
    let len = Array.length obls in
    let _ = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in
      progmap_add n (CEphemeron.create 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 ?(univdecl=UState.default_univ_decl) ?tactic
                           ?(kind=Global,false,Definition) ?(reduce=reduce)
    ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
  let sign = Decls.initialize_named_context_for_proof () in
  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 sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind)
       notations obls imps kind reduce hook 
     in progmap_add n (CEphemeron.create 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 = Monomorphic_const_entry (UState.context_set prg.prg_ctx) in
            let kn = Declare.declare_constant x.obl_name ~local:true
              (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural)
            in
              assumption_message x.obl_name;
              obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
        | 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