1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: refiner.ml 11897 2009-02-09 19:28:02Z barras $ *)
25
type transformation_tactic = proof_tree -> (goal list * validation)
27
let hypotheses gl = gl.evar_hyps
28
let conclusion gl = gl.evar_concl
31
let project x = x.sigma
33
let pf_status pf = pf.open_subgoals
35
let is_complete pf = (0 = (pf_status pf))
37
let on_open_proofs f pf = if is_complete pf then pf else f pf
39
let and_status = List.fold_left (+) 0
43
let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps
44
let pf_hyps gls = named_context_of_val (sig_it gls).evar_hyps
49
| None -> error "It is a leaf."
51
if List.length pfl >= n then
52
(match list_chop (n-1) pfl with
53
| left,(wanted::right) ->
56
if (List.length pfl' = 1)
57
& (List.hd pfl').goal = wanted.goal
59
let pf' = List.hd pfl' in
60
let spfl = left@(pf'::right) in
61
let newstatus = and_status (List.map pf_status spfl) in
63
open_subgoals = newstatus;
66
error "descend: validation"))
69
error "Too few subproofs"
72
(* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
74
[ (v1 [p_1 ... p_l1]) ; (v2 [ p_(l1+1) ... p_(l1+l2) ]) ; ... ;
75
(vk [ p_(l1+...+l(k-1)+1) ... p_(l1+...lk) ]) ]
78
let rec mapshape nl (fl : (proof_tree list -> proof_tree) list)
79
(l : proof_tree list) =
83
let m,l = list_chop h l in
84
(List.hd fl m) :: (mapshape t (List.tl fl) l)
86
(* [frontier : proof_tree -> goal list * validation]
87
given a proof [p], [frontier p] gives [(l,v)] where [l] is the list of goals
88
to be solved to complete the proof, and [v] is the corresponding
96
let p' = List.hd lp' in
97
if Evd.eq_evar_info p'.goal p.goal then
100
errorlabstrm "Refiner.frontier"
101
(str"frontier was handed back a ill-formed proof.")))
103
let gll,vl = List.split(List.map frontier pfl) in
106
let pfl' = mapshape (List.map List.length gll) vl retpfl in
108
open_subgoals = and_status (List.map pf_status pfl');
109
ref = Some(r,pfl')}))
111
(* TODO LEM: I might have to make sure that these hooks are called
112
only when called from solve_nth_pftreestate; I can build the hook
113
call into the "f", then.
115
let solve_hook = ref ignore
116
let set_solve_hook = (:=) solve_hook
118
let rec frontier_map_rec f n p =
119
if n < 1 || n > p.open_subgoals then p else
123
if Evd.eq_evar_info p'.goal p.goal then
129
errorlabstrm "Refiner.frontier_map"
130
(str"frontier_map was handed back a ill-formed proof.")
134
(fun (n,acc) p -> (n-p.open_subgoals,frontier_map_rec f n p::acc))
136
let pfl' = List.rev rpfl' in
138
open_subgoals = and_status (List.map pf_status pfl');
141
let frontier_map f n p =
142
let nmax = p.open_subgoals in
143
let n = if n < 0 then nmax + n + 1 else n in
144
if n < 1 || n > nmax then
145
errorlabstrm "Refiner.frontier_map" (str "No such subgoal");
146
frontier_map_rec f n p
148
let rec frontier_mapi_rec f i p =
149
if p.open_subgoals = 0 then p else
153
if Evd.eq_evar_info p'.goal p.goal then
159
errorlabstrm "Refiner.frontier_mapi"
160
(str"frontier_mapi was handed back a ill-formed proof.")
164
(fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc))
166
let pfl' = List.rev rpfl' in
168
open_subgoals = and_status (List.map pf_status pfl');
171
let frontier_mapi f p = frontier_mapi_rec f 1 p
173
(* [list_pf p] is the lists of goals to be solved in order to complete the
176
let list_pf p = fst (frontier p)
178
let rec nb_unsolved_goals pf = pf.open_subgoals
180
(* leaf g is the canonical incomplete proof of a goal g *)
187
(* refiner r is a tactic applying the rule r *)
189
let check_subproof_connection gl spfl =
190
list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl
192
let abstract_operation syntax semantics gls =
193
let (sgl_sigma,validation) = semantics gls in
194
let hidden_proof = validation (List.map leaf sgl_sigma.it) in
197
assert (check_subproof_connection sgl_sigma.it spfl);
198
{ open_subgoals = and_status (List.map pf_status spfl);
200
ref = Some(Nested(syntax,hidden_proof),spfl)})
202
let abstract_tactic_expr ?(dflt=false) te tacfun gls =
203
abstract_operation (Tactic(te,dflt)) tacfun gls
205
let abstract_tactic ?(dflt=false) te =
206
!abstract_tactic_box := Some te;
207
abstract_tactic_expr ~dflt (Tacexpr.TacAtom (dummy_loc,te))
209
let abstract_extended_tactic ?(dflt=false) s args =
210
abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args))
212
let refiner = function
214
let prim_fun = prim_refiner pr in
216
let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in
217
({it=sgl; sigma = sigma'},
219
assert (check_subproof_connection sgl spfl);
220
{ open_subgoals = and_status (List.map pf_status spfl);
221
goal = goal_sigma.it;
222
ref = Some(r,spfl) })))
225
| Nested (_,_) | Decl_proof _ ->
226
failwith "Refiner: should not occur"
228
(* Daimon is a canonical unfinished proof *)
232
({it=[];sigma=gls.sigma},
237
ref = Some(Daimon,[])})
240
let norm_evar_tac gl = refiner (Prim Change_evars) gl
242
let norm_evar_proof sigma pf =
243
let nf_subgoal i sgl =
244
let (gll,v) = norm_evar_tac {it=sgl.goal;sigma=sigma} in
245
v (List.map leaf gll.it) in
246
frontier_mapi nf_subgoal pf
248
(* [extract_open_proof : proof_tree -> constr * (int * constr) list]
249
takes a (not necessarly complete) proof and gives a pair (pfterm,obl)
250
where pfterm is the constr corresponding to the proof
251
and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)]
252
where the mi are metavariables numbers, and ci are their types.
253
Their proof should be completed in order to complete the initial proof *)
255
let extract_open_proof sigma pf =
257
let meta_cnt = ref 0 in
260
if Evd.mem sigma (existential_of_int !meta_cnt) then f ()
264
let open_obligations = ref [] in
265
let rec proof_extractor vl = function
266
| {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
268
| {ref=Some(Nested(_,hidden_proof),spfl)} ->
269
let sgl,v = frontier hidden_proof in
270
let flat_proof = v spfl in
271
proof_extractor vl flat_proof
273
| {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf
275
| {ref=(None|Some(Daimon,[]));goal=goal} ->
279
try let n = proof_variable_index id vl in (n,id)
280
with Not_found -> failwith "caught")
281
(ids_of_named_context (named_context_of_val goal.evar_hyps)) in
283
Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in
285
List.map (fun (n,id) -> (n,lookup_named_val id goal.evar_hyps))
288
List.fold_right (fun (_,decl) c -> mkNamedProd_or_LetIn decl c)
289
sorted_env goal.evar_concl in
290
let inst = List.filter (fun (_,(_,b,_)) -> b = None) sorted_env in
291
let meta = next_meta () in
292
open_obligations := (meta,abs_concl):: !open_obligations;
293
applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) inst)
295
| _ -> anomaly "Bug: a case has been forgotten in proof_extractor"
297
let pfterm = proof_extractor [] pf in
298
(pfterm, List.rev !open_obligations)
300
(*********************)
302
(*********************)
304
(* unTAC : tactic -> goal sigma -> proof sigma *)
307
let (gl_sigma,v) = tac g in
308
{ it = v (List.map leaf gl_sigma.it); sigma = gl_sigma.sigma }
310
let unpackage glsig = (ref (glsig.sigma)),glsig.it
312
let repackage r v = {it=v;sigma = !r}
314
let apply_sig_tac r tac g =
315
check_for_interrupt (); (* Breakpoint *)
316
let glsigma,v = tac (repackage r g) in
320
let idtac_valid = function
322
| _ -> anomaly "Refiner.idtac_valid"
324
(* [goal_goal_list : goal sigma -> goal list sigma] *)
325
let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma}
327
(* forces propagation of evar constraints *)
328
let tclNORMEVAR = norm_evar_tac
330
(* identity tactic without any message *)
331
let tclIDTAC gls = (goal_goal_list gls, idtac_valid)
333
(* the message printing identity tactic *)
334
let tclIDTAC_MESSAGE s gls =
335
msg (hov 0 s); tclIDTAC gls
337
(* General failure tactic *)
338
let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
340
(* A special exception for levels for the Fail tactic *)
341
exception FailError of int * std_ppcmds
343
(* The Fail tactic *)
344
let tclFAIL lvl s g = raise (FailError (lvl,s))
347
let (sigr,g) = unpackage gls in
348
(sigr,[g],idtac_valid)
350
let finish_tac (sigr,gl,p) = (repackage sigr gl, p)
352
(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
353
let thens3parts_tac tacfi tac tacli (sigr,gs,p) =
354
let nf = Array.length tacfi in
355
let nl = Array.length tacli in
356
let ng = List.length gs in
357
if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
360
(list_map_i (fun i ->
361
apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
363
(sigr, List.flatten gll,
364
compose p (mapshape (List.map List.length gll) pl))
366
(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
367
let thensf_tac taci tac = thens3parts_tac taci tac [||]
369
(* Apply [taci.(i)] on the last n subgoals and [tac] on the others *)
370
let thensl_tac tac taci = thens3parts_tac [||] tac taci
372
(* Apply [tac i] on the ith subgoal (no subgoals number check) *)
373
let thensi_tac tac (sigr,gs,p) =
375
List.split (list_map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs) in
376
(sigr, List.flatten gll, compose p (mapshape (List.map List.length gll) pl))
378
let then_tac tac = thensf_tac [||] tac
380
let non_existent_goal n =
381
errorlabstrm ("No such goal: "^(string_of_int n))
382
(str"Trying to apply a tactic to a non existent goal")
384
(* Apply tac on the i-th goal (if i>0). If i<0, then start counting from
385
the last goal (i=-1). *)
386
let theni_tac i tac ((_,gl,_) as subgoals) =
387
let nsg = List.length gl in
388
let k = if i < 0 then nsg + i + 1 else i in
389
if nsg < 1 then errorlabstrm "theni_tac" (str"No more subgoals.")
390
else if k >= 1 & k <= nsg then
392
(Array.init k (fun i -> if i+1 = k then tac else tclIDTAC)) tclIDTAC
394
else non_existent_goal k
396
(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
397
applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
398
the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
399
subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
400
error if the number of resulting subgoals is strictly less than [n+m] *)
401
let tclTHENS3PARTS tac1 tacfi tac tacli gls =
402
finish_tac (thens3parts_tac tacfi tac tacli (then_tac tac1 (start_tac gls)))
404
(* [tclTHENSFIRSTn tac1 [|t1 ; ... ; tn|] tac2 gls] applies the tactic [tac1]
405
to [gls] and applies [t1], ..., [tn] to the first [n] resulting
406
subgoals, and [tac2] to the others subgoals. Raises an error if
407
the number of resulting subgoals is strictly less than [n] *)
408
let tclTHENSFIRSTn tac1 taci tac = tclTHENS3PARTS tac1 taci tac [||]
410
(* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1]
411
to [gls] and applies [t1], ..., [tn] to the last [n] resulting
412
subgoals, and [tac2] to the other subgoals. Raises an error if the
413
number of resulting subgoals is strictly less than [n] *)
414
let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci
416
(* [tclTHEN_i tac taci gls] applies the tactic [tac] to [gls] and applies
417
[(taci i)] to the i_th resulting subgoal (starting from 1), whatever the
418
number of subgoals is *)
419
let tclTHEN_i tac taci gls =
420
finish_tac (thensi_tac taci (then_tac tac (start_tac gls)))
422
let tclTHENLASTn tac1 taci = tclTHENSLASTn tac1 tclIDTAC taci
423
let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC
425
(* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
426
[tac2] to every resulting subgoals *)
427
let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||]
429
(* [tclTHENSV tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to
430
[gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
431
an error if the number of resulting subgoals is not [n] *)
432
let tclTHENSV tac1 tac2v =
433
tclTHENS3PARTS tac1 tac2v (tclFAIL_s "Wrong number of tactics.") [||]
435
let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l)
437
(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
438
to the last resulting subgoal *)
439
let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|]
441
(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
442
to the first resulting subgoal *)
443
let tclTHENFIRST tac1 tac2 = tclTHENSFIRSTn tac1 [|tac2|] tclIDTAC
445
(* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More
446
convenient than [tclTHEN] when [n] is large. *)
447
let rec tclTHENLIST = function
449
| t1::tacl -> tclTHEN t1 (tclTHENLIST tacl)
454
(* various progress criterions *)
455
let same_goal gl subgoal =
456
eq_constr (conclusion subgoal) (conclusion gl) &&
457
eq_named_context_val (hypotheses subgoal) (hypotheses gl)
460
let weak_progress gls ptree =
461
(List.length gls.it <> 1) ||
462
(not (same_goal (List.hd gls.it) ptree.it))
464
let progress gls ptree =
465
(not (eq_evar_map ptree.sigma gls.sigma)) ||
466
(weak_progress gls ptree)
469
(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
470
the goal unchanged *)
471
let tclPROGRESS tac ptree =
472
let rslt = tac ptree in
473
if progress (fst rslt) ptree then rslt
474
else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.")
476
(* weak_PROGRESS tac ptree applies tac to the goal ptree and fails
477
if tac leaves the goal unchanged, possibly modifying sigma *)
478
let tclWEAK_PROGRESS tac ptree =
479
let rslt = tac ptree in
480
if weak_progress (fst rslt) ptree then rslt
481
else errorlabstrm "Refiner.tclWEAK_PROGRESS" (str"Failed to progress.")
484
(* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals,
485
one of them being identical to the original goal *)
486
let tclNOTSAMEGOAL (tac : tactic) goal =
487
let rslt = tac goal in
488
let gls = (fst rslt).it in
489
if List.exists (same_goal goal.it) gls
490
then errorlabstrm "Refiner.tclNOTSAMEGOAL"
491
(str"Tactic generated a subgoal identical to the original goal.")
494
let catch_failerror e =
495
if catchable_exception e then check_for_interrupt ()
497
| FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))
498
| Stdpp.Exc_located(_, LtacLocated (_,FailError (0,_))) ->
499
check_for_interrupt ()
500
| FailError (lvl,s) -> raise (FailError (lvl - 1, s))
501
| Stdpp.Exc_located(s,FailError (lvl,s')) ->
502
raise (Stdpp.Exc_located(s,FailError (lvl - 1, s')))
503
| Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
505
(Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s'))))
508
(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
509
let tclORELSE0 t1 t2 g =
512
with (* Breakpoint *)
513
| e -> catch_failerror e; t2 g
515
(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
517
let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
519
(* applies t1;t2then if t1 succeeds or t2else if t1 fails
520
t2* are called in terminal position (unless t1 produces more than
522
let tclORELSE_THEN t1 t2then t2else gls =
524
try Some(tclPROGRESS t1 gls)
525
with e -> catch_failerror e; None
529
let (sigr,gl) = unpackage sgl in
530
finish_tac (then_tac t2then (sigr,gl,v))
532
(* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
533
let tclTRY f = (tclORELSE0 f tclIDTAC)
535
let tclTHENTRY f g = (tclTHEN f (tclTRY g))
537
(* Try the first tactic that does not fail in a list of tactics *)
539
let rec tclFIRST = function
540
| [] -> tclFAIL_s "No applicable tactic."
541
| t::rest -> tclORELSE0 t (tclFIRST rest)
543
let ite_gen tcal tac_if continue tac_else gl=
544
let success=ref false in
546
let result=tac_if gl in
547
success:=true;result in
554
tcal tac_if0 continue gl
555
with (* Breakpoint *)
556
| e -> catch_failerror e; tac_else0 e gl
558
(* Try the first tactic and, if it succeeds, continue with
559
the second one, and if it fails, use the third one *)
561
let tclIFTHENELSE=ite_gen tclTHEN
563
(* Idem with tclTHENS and tclTHENSV *)
565
let tclIFTHENSELSE=ite_gen tclTHENS
567
let tclIFTHENSVELSE=ite_gen tclTHENSV
569
let tclIFTHENTRYELSEMUST tac1 tac2 gl =
570
tclIFTHENELSE tac1 (tclTRY tac2) tac2 gl
572
(* Fails if a tactic did not solve the goal *)
573
let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.")
575
(* Try the first thats solves the current goal *)
576
let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
579
(* Iteration tacticals *)
583
if k < 0 then errorlabstrm "Refiner.tclDO"
584
(str"Wrong argument : Do needs a positive integer.");
585
if k = 0 then tclIDTAC
586
else if k = 1 then t else (tclTHEN t (dorec (k-1)))
591
(* Beware: call by need of CAML, g is needed *)
592
let rec tclREPEAT t g =
593
tclORELSE_THEN t (tclREPEAT t) tclIDTAC g
595
let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
597
(* Repeat on the first subgoal (no failure if no more subgoal) *)
598
let rec tclREPEAT_MAIN t g =
599
(tclORELSE (tclTHEN_i t (fun i -> if i = 1 then (tclREPEAT_MAIN t) else
600
tclIDTAC)) tclIDTAC) g
602
(*s Tactics handling a list of goals. *)
604
type validation_list = proof_tree list -> proof_tree list
606
type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
608
(* Functions working on goal list for correct backtracking in Prolog *)
610
let tclFIRSTLIST = tclFIRST
611
let tclIDTAC_list gls = (gls, fun x -> x)
613
(* first_goal : goal list sigma -> goal sigma *)
616
let gl = gls.it and sig_0 = gls.sigma in
617
if gl = [] then error "first_goal";
618
{ it = List.hd gl; sigma = sig_0 }
620
(* goal_goal_list : goal sigma -> goal list sigma *)
622
let goal_goal_list gls =
623
let gl = gls.it and sig_0 = gls.sigma in { it = [gl]; sigma = sig_0 }
625
(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
627
let apply_tac_list tac glls =
628
let (sigr,lg) = unpackage glls in
631
let (gl,p) = apply_sig_tac sigr tac g1 in
632
let n = List.length gl in
633
(repackage sigr (gl@rest),
634
fun pfl -> let (pfg,pfrest) = list_chop n pfl in (p pfg)::pfrest)
635
| _ -> error "apply_tac_list"
637
let then_tactic_list tacl1 tacl2 glls =
638
let (glls1,pl1) = tacl1 glls in
639
let (glls2,pl2) = tacl2 glls1 in
640
(glls2, compose pl1 pl2)
642
(* Transform a tactic_list into a tactic *)
644
let tactic_list_tactic tac gls =
645
let (glres,vl) = tac (goal_goal_list gls) in
646
(glres, compose idtac_valid vl)
650
(* The type of proof-trees state and a few utilities
651
A proof-tree state is built from a proof-tree, a set of global
652
constraints, and a stack which allows to navigate inside the
653
proof-tree remembering how to rebuild the global proof-tree
654
possibly after modification of one of the focused children proof-tree.
655
The number in the stack corresponds to
656
either the selected subtree and the validation is a function from a
657
proof-tree list consisting only of one proof-tree to the global
659
or -1 when the move is done behind a registered tactic in which
660
case the validation corresponds to a constant function giving back
661
the original proof-tree. *)
666
tstack : (int * validation) list }
668
let proof_of_pftreestate pts = pts.tpf
669
let is_top_pftreestate pts = pts.tstack = []
670
let cursor_of_pftreestate pts = List.map fst pts.tstack
671
let evc_of_pftreestate pts = pts.tpfsigma
673
let top_goal_of_pftreestate pts =
674
{ it = goal_of_proof pts.tpf; sigma = pts.tpfsigma }
676
let nth_goal_of_pftreestate n pts =
677
let goals = fst (frontier pts.tpf) in
678
try {it = List.nth goals (n-1); sigma = pts.tpfsigma }
679
with Invalid_argument _ | Failure _ -> non_existent_goal n
681
let traverse n pts = match n with
682
| 0 -> (* go to the parent *)
683
(match pts.tstack with
684
| [] -> error "traverse: no ancestors"
686
let pf = v [pts.tpf] in
687
let pf = norm_evar_proof pts.tpfsigma pf in
690
tpfsigma = pts.tpfsigma })
691
| -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *)
692
(match pts.tpf.ref with
693
| Some (Nested (_,spf),_) ->
694
let v = (fun pfl -> pts.tpf) in
696
tstack = (-1,v)::pts.tstack;
697
tpfsigma = pts.tpfsigma }
698
| _ -> error "traverse: not a tactic-node")
699
| n -> (* when n>0, go to the nth child *)
700
let (npf,v) = descend n pts.tpf in
702
tpfsigma = pts.tpfsigma;
703
tstack = (n,v):: pts.tstack }
705
let change_constraints_pftreestate newgc pts = { pts with tpfsigma = newgc }
707
let app_tac sigr tac p =
708
let (gll,v) = tac {it=p.goal;sigma= !sigr} in
710
v (List.map leaf gll.it)
712
(* modify proof state at current position *)
714
let map_pftreestate f pts =
715
let sigr = ref pts.tpfsigma in
716
let tpf' = f sigr pts.tpf in
718
if !sigr == pts.tpfsigma then tpf' else norm_evar_proof !sigr tpf' in
721
tstack = pts.tstack }
723
(* solve the nth subgoal with tactic tac *)
725
let solve_nth_pftreestate n tac =
727
(fun sigr pt -> frontier_map (app_tac sigr tac) n pt)
729
let solve_pftreestate = solve_nth_pftreestate 1
731
(* This function implements a poor man's undo at the current goal.
732
This is a gross approximation as it does not attempt to clean correctly
733
the global constraints given in tpfsigma. *)
735
let weak_undo_pftreestate pts =
736
let pf = leaf pts.tpf.goal in
738
tpfsigma = pts.tpfsigma;
739
tstack = pts.tstack }
741
(* Gives a new proof (a leaf) of a goal gl *)
742
let mk_pftreestate g =
745
tpfsigma = Evd.empty }
747
(* Extracts a constr from a proof-tree state ; raises an error if the
748
proof is not complete or the state does not correspond to the head
751
let extract_open_pftreestate pts =
752
extract_open_proof pts.tpfsigma pts.tpf
754
let extract_pftreestate pts =
755
if pts.tstack <> [] then
756
errorlabstrm "extract_pftreestate" (str"Proof blocks need to be closed");
757
let pfterm,subgoals = extract_open_pftreestate pts in
758
let exl = Evarutil.non_instantiated pts.tpfsigma in
759
if subgoals <> [] or exl <> [] then
760
errorlabstrm "extract_proof"
761
(if subgoals <> [] then
762
str "Attempt to save an incomplete proof"
764
str "Attempt to save a proof with existential variables still non-instantiated");
765
let env = Global.env_of_context pts.tpf.goal.evar_hyps in
766
nf_betaiota_preserving_vm_cast env pts.tpfsigma pfterm
767
(* strong whd_betaiotaevar env pts.tpfsigma pfterm *)
769
local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm
771
(* Focus on the first leaf proof in a proof-tree state *)
773
let rec first_unproven pts =
774
let pf = (proof_of_pftreestate pts) in
775
if is_complete_proof pf then
776
errorlabstrm "first_unproven" (str"No unproven subgoals");
777
if is_leaf_proof pf then
783
if not(is_complete_proof pf) then n else failwith "caught")
784
1 (children_of_proof pf)
786
first_unproven (traverse childnum pts)
788
(* Focus on the last leaf proof in a proof-tree state *)
790
let rec last_unproven pts =
791
let pf = proof_of_pftreestate pts in
792
if is_complete_proof pf then
793
errorlabstrm "last_unproven" (str"No unproven subgoals");
794
if is_leaf_proof pf then
797
let children = (children_of_proof pf) in
798
let nchilds = List.length children in
802
if not(is_complete_proof pf) then n else failwith "caught")
803
1 (List.rev children)
805
last_unproven (traverse (nchilds-childnum+1) pts)
807
let rec nth_unproven n pts =
808
let pf = proof_of_pftreestate pts in
809
if is_complete_proof pf then
810
errorlabstrm "nth_unproven" (str"No unproven subgoals");
811
if is_leaf_proof pf then
815
errorlabstrm "nth_unproven" (str"Not enough unproven subgoals")
817
let children = children_of_proof pf in
818
let rec process i k = function
820
errorlabstrm "nth_unproven" (str"Not enough unproven subgoals")
822
let k1 = nb_unsolved_goals pf1 in
824
process (i+1) (k-k1) rest
826
nth_unproven k (traverse i pts)
830
let rec node_prev_unproven loc pts =
831
let pf = proof_of_pftreestate pts in
832
match cursor_of_pftreestate pts with
833
| [] -> last_unproven pts
835
if is_complete_proof pf or loc = 1 then
836
node_prev_unproven n (traverse 0 pts)
838
let child = List.nth (children_of_proof pf) (loc - 2) in
839
if is_complete_proof child then
840
node_prev_unproven (loc - 1) pts
842
first_unproven (traverse (loc - 1) pts)
844
let rec node_next_unproven loc pts =
845
let pf = proof_of_pftreestate pts in
846
match cursor_of_pftreestate pts with
847
| [] -> first_unproven pts
849
if is_complete_proof pf ||
850
loc = (List.length (children_of_proof pf)) then
851
node_next_unproven n (traverse 0 pts)
852
else if is_complete_proof (List.nth (children_of_proof pf) loc) then
853
node_next_unproven (loc + 1) pts
855
last_unproven(traverse (loc + 1) pts)
857
let next_unproven pts =
858
let pf = proof_of_pftreestate pts in
859
if is_leaf_proof pf then
860
match cursor_of_pftreestate pts with
861
| [] -> error "next_unproven"
862
| n::_ -> node_next_unproven n (traverse 0 pts)
864
node_next_unproven (List.length (children_of_proof pf)) pts
866
let prev_unproven pts =
867
let pf = proof_of_pftreestate pts in
868
if is_leaf_proof pf then
869
match cursor_of_pftreestate pts with
870
| [] -> error "prev_unproven"
871
| n::_ -> node_prev_unproven n (traverse 0 pts)
873
node_prev_unproven 1 pts
875
let rec top_of_tree pts =
876
if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
878
(* FIXME: cette fonction n'est (as of October 2007) appelée nulle part *)
879
let change_rule f pts =
883
{pt with ref=Some (f oldrule,l)}
884
| _ -> invalid_arg "change_rule" in
885
map_pftreestate mark_top pts
887
let match_rule p pts =
888
match (proof_of_pftreestate pts).ref with
892
let rec up_until_matching_rule p pts =
893
if is_top_pftreestate pts then
896
let one_up = traverse 0 pts in
897
if match_rule p one_up then
900
up_until_matching_rule p one_up
902
let rec up_to_matching_rule p pts =
903
if match_rule p pts then
906
if is_top_pftreestate pts then
909
let one_up = traverse 0 pts in
910
up_to_matching_rule p one_up
913
let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
915
(* Pretty-printers. *)
917
let pp_info = ref (fun _ _ _ -> assert false)
918
let set_info_printer f = pp_info := f
920
let tclINFO (tac : tactic) gls =
921
let (sgl,v) as res = tac gls in
923
let pf = v (List.map leaf (sig_it sgl)) in
924
let sign = named_context_of_val (sig_it gls).evar_hyps in
925
msgnl (hov 0 (str" == " ++
926
!pp_info (project gls) sign pf))
927
with e when catchable_exception e ->
928
msgnl (hov 0 (str "Info failed to apply validation"))
added
removed
proofs/refiner.ml
