1
(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
20
let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
21
let pperror cmd = Util.errorlabstrm "Program" cmd
22
let error s = pperror (str s)
24
exception NoObligations of identifier option
26
let explain_no_obligations = function
27
Some ident -> str "No obligations for program " ++ str (string_of_id ident)
28
| None -> str "No obligations remaining"
30
type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t
31
* Tacexpr.raw_tactic_expr option) array
34
{ obl_name : identifier;
37
obl_body : constr option;
38
obl_status : obligation_definition_status;
40
obl_tac : Tacexpr.raw_tactic_expr option;
43
type obligations = (obligation array * int)
45
type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
51
prg_obligations: obligations;
52
prg_deps : identifier list;
53
prg_fixkind : Command.fixpoint_kind option ;
54
prg_implicits : (Topconstr.explicitation * (bool * bool)) list;
55
prg_notations : notations ;
56
prg_kind : definition_kind;
57
prg_hook : Tacexpr.declaration_hook;
60
let assumption_message id =
61
Flags.if_verbose message ((string_of_id id) ^ " is assumed")
63
let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
64
let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Tacexpr.TacId [])
66
let set_default_tactic t = default_tactic_expr := t; default_tactic := Tacinterp.eval_tactic t
68
(* true = All transparent, false = Opaque if possible *)
69
let proofs_transparency = ref true
71
let set_proofs_transparency = (:=) proofs_transparency
72
let get_proofs_transparency () = !proofs_transparency
79
optname = "transparency of Program obligations";
80
optkey = (SecondaryTable ("Transparent","Obligations"));
81
optread = get_proofs_transparency;
82
optwrite = set_proofs_transparency; }
84
let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type
86
let get_obligation_body expand obl =
87
let c = Option.get obl.obl_body in
88
if expand && obl.obl_status = Expand then
89
match kind_of_term c with
90
| Const c -> constant_value (Global.env ()) c
94
let subst_deps expand obls deps t =
98
let xobl = obls.(x) in
100
try get_obligation_body expand xobl
101
with _ -> assert(false)
102
in (xobl.obl_name, oblb) :: acc)
104
in(* Termops.it_mkNamedProd_or_LetIn t subst *)
105
Term.replace_vars subst t
107
let subst_deps_obl obls obl =
108
let t' = subst_deps false obls obl.obl_deps obl.obl_type in
109
{ obl with obl_type = t' }
111
module ProgMap = Map.Make(struct type t = identifier let compare = compare end)
113
let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)
117
ProgMap.iter (fun _ _ -> incr i) m;
120
exception Found of program_info
124
ProgMap.iter (fun _ v -> raise (Found v)) m;
128
let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
130
let freeze () = !from_prg, !default_tactic_expr
131
let unfreeze (v, t) = from_prg := v; set_default_tactic t
133
from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligation_tactic" [])
136
Summary.declare_summary "program-tcc-table"
137
{ Summary.freeze_function = freeze;
138
Summary.unfreeze_function = unfreeze;
139
Summary.init_function = init;
140
Summary.survive_module = false;
141
Summary.survive_section = false }
143
let progmap_union = ProgMap.fold ProgMap.add
145
let cache (_, (infos, tac)) =
147
set_default_tactic tac
151
{ (default_object "Program state") with
152
cache_function = cache;
153
load_function = (fun _ -> cache);
154
open_function = (fun _ -> cache);
155
classify_function = (fun _ -> Dispose);
156
export_function = (fun x -> Some x) }
160
let rec intset_to = function
162
| n -> Intset.add n (intset_to (pred n))
164
let subst_body expand prg =
165
let obls, _ = prg.prg_obligations in
166
let ints = intset_to (pred (Array.length obls)) in
167
subst_deps expand obls ints prg.prg_body,
168
subst_deps expand obls ints (Termops.refresh_universes prg.prg_type)
170
let declare_definition prg =
171
let body, typ = subst_body false prg in
172
(try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++
173
my_print_constr (Global.env()) body ++ str " : " ++
174
my_print_constr (Global.env()) prg.prg_type);
176
let (local, boxed, kind) = prg.prg_kind in
178
{ const_entry_body = body;
179
const_entry_type = Some typ;
180
const_entry_opaque = false;
181
const_entry_boxed = boxed}
183
(Command.get_declare_definition_hook ()) ce;
185
| Local when Lib.sections_are_opened () ->
187
SectionLocalDef(ce.const_entry_body,ce.const_entry_type,false) in
188
let _ = declare_variable prg.prg_name (Lib.cwd(),c,IsDefinition kind) in
189
print_message (Subtac_utils.definition_message prg.prg_name);
190
if Pfedit.refining () then
191
Flags.if_verbose msg_warning
192
(str"Local definition " ++ Nameops.pr_id prg.prg_name ++
193
str" is not visible from current goals");
197
Declare.declare_constant
198
prg.prg_name (DefinitionEntry ce,IsDefinition (pi3 prg.prg_kind))
200
let gr = ConstRef c in
201
if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
202
Impargs.declare_manual_implicits false gr prg.prg_implicits;
203
print_message (Subtac_utils.definition_message prg.prg_name);
204
prg.prg_hook local gr;
210
let rec lam_index n t acc =
211
match kind_of_term t with
212
| Lambda (na, _, b) ->
213
if na = Name n then acc
214
else lam_index n b (succ acc)
215
| _ -> raise Not_found
217
let compute_possible_guardness_evidences (n,_) fixbody fixtype =
219
| Some (loc, n) -> [lam_index n fixbody 0]
221
(* If recursive argument was not given by user, we try all args.
222
An earlier approach was to look only for inductive arguments,
223
but doing it properly involves delta-reduction, and it finally
224
doesn't seem to worth the effort (except for huge mutual
226
let m = Term.nb_prod fixtype in
227
let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
228
list_map_i (fun i _ -> i) 0 ctx
231
Reductionops.clos_norm_flags Closure.betaiotazeta (Global.env ()) Evd.empty
233
let declare_mutual_definition l =
234
let len = List.length l in
235
let first = List.hd l in
236
let fixdefs, fixtypes, fiximps =
239
let subs, typ = (subst_body false x) in
240
snd (decompose_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
242
(* let fixdefs = List.map reduce_fix fixdefs in *)
243
let fixkind = Option.get first.prg_fixkind in
244
let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
245
let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
246
let (local,boxed,kind) = first.prg_kind in
247
let fixnames = first.prg_deps in
248
let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
249
let indexes, fixdecls =
252
let possible_indexes =
253
list_map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in
254
let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
255
Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
257
None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
259
(* Declare the recursive definitions *)
260
let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in
261
(* Declare notations *)
262
List.iter (Command.declare_interning_data ([],[])) first.prg_notations;
263
Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames);
264
let gr = List.hd kns in
265
let kn = match gr with ConstRef kn -> kn | _ -> assert false in
266
first.prg_hook local gr; kn
268
let declare_obligation obl body =
269
match obl.obl_status with
270
| Expand -> { obl with obl_body = Some body }
273
{ const_entry_body = body;
274
const_entry_type = Some obl.obl_type;
276
(if get_proofs_transparency () then false
278
const_entry_boxed = false}
280
let constant = Declare.declare_constant obl.obl_name
281
(DefinitionEntry ce,IsProof Property)
283
print_message (Subtac_utils.definition_message obl.obl_name);
284
{ obl with obl_body = Some (mkConst constant) }
286
let red = Reductionops.nf_betaiota Evd.empty
288
let init_prog_info n b t deps fixkind notations obls impls kind hook =
291
(fun i (n, t, l, o, d, tac) ->
292
debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d));
293
{ obl_name = n ; obl_body = None;
294
obl_location = l; obl_type = red t; obl_status = o;
295
obl_deps = d; obl_tac = tac })
298
{ prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls');
299
prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
300
prg_implicits = impls; prg_kind = kind; prg_hook = hook; }
303
let prg_infos = !from_prg in
306
(try ProgMap.find n prg_infos
307
with Not_found -> raise (NoObligations (Some n)))
309
(let n = map_cardinal prg_infos in
311
0 -> raise (NoObligations None)
312
| 1 -> map_first prg_infos
313
| _ -> error "More than one program with unsolved obligations")
316
try get_prog n with NoObligations id -> pperror (explain_no_obligations id)
318
let obligations_solved prg = (snd prg.prg_obligations) = 0
321
(* msgnl (str "Updating obligations info"); *)
322
Lib.add_anonymous_leaf (input s)
327
| Defined of global_reference
329
let obligations_message rem =
332
Flags.if_verbose msgnl (int rem ++ str " obligation remaining")
334
Flags.if_verbose msgnl (int rem ++ str " obligations remaining")
336
Flags.if_verbose msgnl (str "No more obligations remaining")
338
let update_obls prg obls rem =
339
let prg' = { prg with prg_obligations = (obls, rem) } in
340
from_prg := map_replace prg.prg_name prg' !from_prg;
341
obligations_message rem;
343
if rem > 0 then Remain rem
345
match prg'.prg_deps with
347
let kn = declare_definition prg' in
348
from_prg := ProgMap.remove prg.prg_name !from_prg;
351
let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
352
if List.for_all (fun x -> obligations_solved x) progs then
353
(let kn = declare_mutual_definition progs in
354
from_prg := List.fold_left
356
ProgMap.remove x.prg_name acc) !from_prg progs;
357
Defined (ConstRef kn))
360
update_state (!from_prg, !default_tactic_expr);
363
let is_defined obls x = obls.(x).obl_body <> None
365
let deps_remaining obls deps =
368
if is_defined obls x then acc
372
let has_dependencies obls n =
373
let res = ref false in
376
if i <> n && Intset.mem n obl.obl_deps then
381
let kind_of_opacity o =
383
| Define false | Expand -> Subtac_utils.goal_kind
384
| _ -> Subtac_utils.goal_proof_kind
387
str "Obligation should be transparent but was declared opaque." ++ spc () ++
388
str"Use 'Defined' instead."
390
let warn_not_transp () = ppwarn not_transp_msg
391
let error_not_transp () = pperror not_transp_msg
393
let rec solve_obligation prg num =
394
let user_num = succ num in
395
let obls, rem = prg.prg_obligations in
396
let obl = obls.(num) in
397
if obl.obl_body <> None then
398
pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")
400
match deps_remaining obls obl.obl_deps with
402
let obl = subst_deps_obl obls obl in
403
Command.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
405
let cst = match gr with ConstRef cst -> cst | _ -> assert false in
407
let transparent = evaluable_constant cst (Global.env ()) in
409
match obl.obl_status with
411
if not transparent then error_not_transp ()
412
else constant_value (Global.env ()) cst
414
if not opaque && not transparent then error_not_transp ()
415
else Libnames.constr_of_global gr
416
in { obl with obl_body = Some body }
418
let obls = Array.copy obls in
419
let _ = obls.(num) <- obl in
420
match update_obls prg obls (pred rem) with
421
| Remain n when n > 0 ->
422
if has_dependencies obls num then
423
ignore(auto_solve_obligations (Some prg.prg_name) None)
425
trace (str "Started obligation " ++ int user_num ++ str " proof: " ++
426
Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
427
Pfedit.by !default_tactic;
428
Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
429
| l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
430
++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
432
and subtac_obligation (user_num, name, typ) =
433
let num = pred user_num in
434
let prg = get_prog_err name in
435
let obls, rem = prg.prg_obligations in
436
if num < Array.length obls then
437
let obl = obls.(num) in
438
match obl.obl_body with
439
None -> solve_obligation prg num
440
| Some r -> error "Obligation already solved"
441
else error (sprintf "Unknown obligation number %i" (succ num))
444
and solve_obligation_by_tac prg obls i tac =
445
let obl = obls.(i) in
446
match obl.obl_body with
450
if deps_remaining obls obl.obl_deps = [] then
451
let obl = subst_deps_obl obls obl in
456
match obl.obl_tac with
457
| Some t -> Tacinterp.interp t
458
| None -> !default_tactic
460
let t = Subtac_utils.solve_by_tac (evar_of_obligation obl) tac in
461
obls.(i) <- declare_obligation obl t;
465
| Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
466
| Stdpp.Exc_located(_, Refiner.FailError (_, s))
467
| Refiner.FailError (_, s) ->
468
user_err_loc (obl.obl_location, "solve_obligation", s)
471
and solve_prg_obligations prg tac =
472
let obls, rem = prg.prg_obligations in
474
let obls' = Array.copy obls in
476
Array.iteri (fun i x ->
477
if solve_obligation_by_tac prg obls' i tac then
481
update_obls prg obls' !rem
483
and solve_obligations n tac =
484
let prg = get_prog_err n in
485
solve_prg_obligations prg tac
487
and solve_all_obligations tac =
488
ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg
490
and try_solve_obligation n prg tac =
491
let prg = get_prog prg in
492
let obls, rem = prg.prg_obligations in
493
let obls' = Array.copy obls in
494
if solve_obligation_by_tac prg obls' n tac then
495
ignore(update_obls prg obls' (pred rem));
497
and try_solve_obligations n tac =
498
try ignore (solve_obligations n tac) with NoObligations _ -> ()
500
and auto_solve_obligations n tac : progress =
501
Flags.if_verbose msgnl (str "Solving obligations automatically...");
502
try solve_prg_obligations (get_prog_err n) tac with NoObligations _ -> Dependent
505
let show_obligations ?(msg=true) n =
506
let prg = get_prog_err n in
507
let n = prg.prg_name in
508
let obls, rem = prg.prg_obligations in
509
let showed = ref 5 in
510
if msg then msgnl (int rem ++ str " obligation(s) remaining: ");
511
Array.iteri (fun i x ->
512
match x.obl_body with
514
if !showed > 0 then (
516
msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
517
str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++
518
hov 1 (my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ())))
523
let prg = get_prog_err n in
524
let n = prg.prg_name in
525
msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++
526
my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
527
++ my_print_constr (Global.env ()) prg.prg_body)
529
let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic ?(hook=fun _ _ -> ()) obls =
530
Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
531
let prg = init_prog_info n b t [] None [] obls implicits kind hook in
532
let obls,_ = prg.prg_obligations in
533
if Array.length obls = 0 then (
534
Flags.if_verbose ppnl (str ".");
535
let cst = declare_definition prg in
536
from_prg := ProgMap.remove prg.prg_name !from_prg;
539
let len = Array.length obls in
540
let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
541
from_prg := ProgMap.add n prg !from_prg;
542
let res = auto_solve_obligations (Some n) tactic in
544
| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
547
let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun _ _ -> ()) notations fixkind =
548
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
549
let upd = List.fold_left
550
(fun acc (n, b, t, imps, obls) ->
551
let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind hook in
552
ProgMap.add n prg acc)
557
List.fold_left (fun finished x ->
558
if finished then finished
560
let res = auto_solve_obligations (Some x) tactic in
562
| Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true
567
let admit_obligations n =
568
let prg = get_prog_err n in
569
let obls, rem = prg.prg_obligations in
570
Array.iteri (fun i x ->
571
match x.obl_body with
573
let x = subst_deps_obl obls x in
574
let kn = Declare.declare_constant x.obl_name (ParameterEntry (x.obl_type,false), IsAssumption Conjectural) in
575
assumption_message x.obl_name;
576
obls.(i) <- { x with obl_body = Some (mkConst kn) }
579
ignore(update_obls prg obls 0)
581
exception Found of int
583
let array_find f arr =
584
try Array.iteri (fun i x -> if f x then raise (Found i)) arr;
588
let next_obligation n =
589
let prg = get_prog_err n in
590
let obls, rem = prg.prg_obligations in
592
try array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls
593
with Not_found -> anomaly "Could not find a solvable obligation."
594
in solve_obligation prg i
596
let default_tactic () = !default_tactic
added
removed
contrib/subtac/subtac_obligations.ml
