diff options
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 696 |
1 files changed, 88 insertions, 608 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index a540eef6..5cd85547 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refiner.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - +open Compat open Pp open Util open Term @@ -18,183 +17,20 @@ open Sign open Environ open Reductionops open Type_errors -open Proof_trees open Proof_type open Logic -type transformation_tactic = proof_tree -> (goal list * validation) - -let hypotheses gl = gl.evar_hyps -let conclusion gl = gl.evar_concl let sig_it x = x.it let project x = x.sigma -let pf_status pf = pf.open_subgoals - -let is_complete pf = (0 = (pf_status pf)) - -let on_open_proofs f pf = if is_complete pf then pf else f pf - -let and_status = List.fold_left (+) 0 - (* Getting env *) -let pf_env gls = Global.env_of_context (sig_it gls).evar_hyps -let pf_hyps gls = named_context_of_val (sig_it gls).evar_hyps - - -let descend n p = - match p.ref with - | None -> error "It is a leaf." - | Some(r,pfl) -> - if List.length pfl >= n then - (match list_chop (n-1) pfl with - | left,(wanted::right) -> - (wanted, - (fun pfl' -> - if false (* debug *) then assert - (List.length pfl'=1 & (List.hd pfl').goal = wanted.goal); - let pf' = List.hd pfl' in - let spfl = left@(pf'::right) in - let newstatus = and_status (List.map pf_status spfl) in - { p with - open_subgoals = newstatus; - ref = Some(r,spfl) })) - | _ -> assert false) - else - error "Too few subproofs" - - -(* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]] - gives - [ (v1 [p_1 ... p_l1]) ; (v2 [ p_(l1+1) ... p_(l1+l2) ]) ; ... ; - (vk [ p_(l1+...+l(k-1)+1) ... p_(l1+...lk) ]) ] - *) - -let rec mapshape nl (fl : (proof_tree list -> proof_tree) list) - (l : proof_tree list) = - match nl with - | [] -> [] - | h::t -> - let m,l = list_chop h l in - (List.hd fl m) :: (mapshape t (List.tl fl) l) - -(* [frontier : proof_tree -> goal list * validation] - given a proof [p], [frontier p] gives [(l,v)] where [l] is the list of goals - to be solved to complete the proof, and [v] is the corresponding - validation *) - -let rec frontier p = - match p.ref with - | None -> - ([p.goal], - (fun lp' -> - let p' = List.hd lp' in - if Evd.eq_evar_info p'.goal p.goal then - p' - else - errorlabstrm "Refiner.frontier" - (str"frontier was handed back a ill-formed proof."))) - | Some(r,pfl) -> - let gll,vl = List.split(List.map frontier pfl) in - (List.flatten gll, - (fun retpfl -> - let pfl' = mapshape (List.map List.length gll) vl retpfl in - { p with - open_subgoals = and_status (List.map pf_status pfl'); - ref = Some(r,pfl')})) - -(* TODO LEM: I might have to make sure that these hooks are called - only when called from solve_nth_pftreestate; I can build the hook - call into the "f", then. - *) -let solve_hook = ref ignore -let set_solve_hook = (:=) solve_hook - -let rec frontier_map_rec f n p = - if n < 1 || n > p.open_subgoals then p else - match p.ref with - | None -> - let p' = f p in - if Evd.eq_evar_info p'.goal p.goal then - begin - !solve_hook p'; - p' - end - else - errorlabstrm "Refiner.frontier_map" - (str"frontier_map was handed back a ill-formed proof.") - | Some(r,pfl) -> - let (_,rpfl') = - List.fold_left - (fun (n,acc) p -> (n-p.open_subgoals,frontier_map_rec f n p::acc)) - (n,[]) pfl in - let pfl' = List.rev rpfl' in - { p with - open_subgoals = and_status (List.map pf_status pfl'); - ref = Some(r,pfl')} - -let frontier_map f n p = - let nmax = p.open_subgoals in - let n = if n < 0 then nmax + n + 1 else n in - if n < 1 || n > nmax then - errorlabstrm "Refiner.frontier_map" (str "No such subgoal"); - frontier_map_rec f n p - -let rec frontier_mapi_rec f i p = - if p.open_subgoals = 0 then p else - match p.ref with - | None -> - let p' = f i p in - if Evd.eq_evar_info p'.goal p.goal then - begin - !solve_hook p'; - p' - end - else - errorlabstrm "Refiner.frontier_mapi" - (str"frontier_mapi was handed back a ill-formed proof.") - | Some(r,pfl) -> - let (_,rpfl') = - List.fold_left - (fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc)) - (i,[]) pfl in - let pfl' = List.rev rpfl' in - { p with - open_subgoals = and_status (List.map pf_status pfl'); - ref = Some(r,pfl')} - -let frontier_mapi f p = frontier_mapi_rec f 1 p - -(* [list_pf p] is the lists of goals to be solved in order to complete the - proof [p] *) - -let list_pf p = fst (frontier p) - -let rec nb_unsolved_goals pf = pf.open_subgoals - -(* leaf g is the canonical incomplete proof of a goal g *) - -let leaf g = - { open_subgoals = 1; - goal = g; - ref = None } - -(* refiner r is a tactic applying the rule r *) - -let check_subproof_connection gl spfl = - list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl - -let abstract_operation syntax semantics gls = - let (sgl_sigma,validation) = semantics gls in - let hidden_proof = validation (List.map leaf sgl_sigma.it) in - (sgl_sigma, - fun spfl -> - assert (check_subproof_connection sgl_sigma.it spfl); - { open_subgoals = and_status (List.map pf_status spfl); - goal = gls.it; - ref = Some(Nested(syntax,hidden_proof),spfl)}) +let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) +let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) + +let abstract_operation syntax semantics = + semantics let abstract_tactic_expr ?(dflt=false) te tacfun gls = abstract_operation (Tactic(te,dflt)) tacfun gls @@ -207,16 +43,11 @@ let abstract_extended_tactic ?(dflt=false) s args = abstract_tactic ~dflt (Tacexpr.TacExtend (dummy_loc, s, args)) let refiner = function - | Prim pr as r -> + | Prim pr -> let prim_fun = prim_refiner pr in (fun goal_sigma -> let (sgl,sigma') = prim_fun goal_sigma.sigma goal_sigma.it in - ({it=sgl; sigma = sigma'}, - (fun spfl -> - assert (check_subproof_connection sgl spfl); - { open_subgoals = and_status (List.map pf_status spfl); - goal = goal_sigma.it; - ref = Some(r,spfl) }))) + {it=sgl; sigma = sigma'}) | Nested (_,_) | Decl_proof _ -> @@ -226,83 +57,15 @@ let refiner = function | Daimon -> fun gls -> - ({it=[];sigma=gls.sigma}, - fun spfl -> - assert (spfl=[]); - { open_subgoals = 0; - goal = gls.it; - ref = Some(Daimon,[])}) + {it=[];sigma=gls.sigma} let norm_evar_tac gl = refiner (Prim Change_evars) gl -let norm_evar_proof sigma pf = - let nf_subgoal i sgl = - let (gll,v) = norm_evar_tac {it=sgl.goal;sigma=sigma} in - v (List.map leaf gll.it) in - frontier_mapi nf_subgoal pf - -(* [extract_open_proof : proof_tree -> constr * (int * constr) list] - takes a (not necessarly complete) proof and gives a pair (pfterm,obl) - where pfterm is the constr corresponding to the proof - and [obl] is an [int*constr list] [ (m1,c1) ; ... ; (mn,cn)] - where the mi are metavariables numbers, and ci are their types. - Their proof should be completed in order to complete the initial proof *) - -let extract_open_proof sigma pf = - let next_meta = - let meta_cnt = ref 0 in - let rec f () = - incr meta_cnt; - if Evd.mem sigma (existential_of_int !meta_cnt) then f () - else !meta_cnt - in f - in - let open_obligations = ref [] in - let rec proof_extractor vl = function - | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf - - | {ref=Some(Nested(_,hidden_proof),spfl)} -> - let sgl,v = frontier hidden_proof in - let flat_proof = v spfl in - proof_extractor vl flat_proof - - | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf - - | {ref=(None|Some(Daimon,[]));goal=goal} -> - let visible_rels = - map_succeed - (fun id -> - try let n = proof_variable_index id vl in (n,id) - with Not_found -> failwith "caught") - (ids_of_named_context (named_context_of_val goal.evar_hyps)) in - let sorted_rels = - Sort.list (fun (n1,_) (n2,_) -> n1 > n2 ) visible_rels in - let sorted_env = - List.map (fun (n,id) -> (n,lookup_named_val id goal.evar_hyps)) - sorted_rels in - let abs_concl = - List.fold_right (fun (_,decl) c -> mkNamedProd_or_LetIn decl c) - sorted_env goal.evar_concl in - let inst = List.filter (fun (_,(_,b,_)) -> b = None) sorted_env in - let meta = next_meta () in - open_obligations := (meta,abs_concl):: !open_obligations; - applist (mkMeta meta, List.map (fun (n,_) -> mkRel n) inst) - - | _ -> anomaly "Bug: a case has been forgotten in proof_extractor" - in - let pfterm = proof_extractor [] pf in - (pfterm, List.rev !open_obligations) - (*********************) (* Tacticals *) (*********************) -(* unTAC : tactic -> goal sigma -> proof sigma *) - -let unTAC tac g = - let (gl_sigma,v) = tac g in - { it = v (List.map leaf gl_sigma.it); sigma = gl_sigma.sigma } let unpackage glsig = (ref (glsig.sigma)),glsig.it @@ -310,13 +73,9 @@ let repackage r v = {it=v;sigma = !r} let apply_sig_tac r tac g = check_for_interrupt (); (* Breakpoint *) - let glsigma,v = tac (repackage r g) in + let glsigma = tac (repackage r g) in r := glsigma.sigma; - (glsigma.it,v) - -let idtac_valid = function - [pf] -> pf - | _ -> anomaly "Refiner.idtac_valid" + glsigma.it (* [goal_goal_list : goal sigma -> goal list sigma] *) let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma} @@ -325,7 +84,7 @@ let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma} let tclNORMEVAR = norm_evar_tac (* identity tactic without any message *) -let tclIDTAC gls = (goal_goal_list gls, idtac_valid) +let tclIDTAC gls = goal_goal_list gls (* the message printing identity tactic *) let tclIDTAC_MESSAGE s gls = @@ -344,23 +103,22 @@ let tclFAIL_lazy lvl s g = raise (FailError (lvl,s)) let start_tac gls = let (sigr,g) = unpackage gls in - (sigr,[g],idtac_valid) + (sigr,[g]) -let finish_tac (sigr,gl,p) = (repackage sigr gl, p) +let finish_tac (sigr,gl) = repackage sigr gl -(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *) -let thens3parts_tac tacfi tac tacli (sigr,gs,p) = +(* Apply [tacfi.(i)] on the first n subgoals, [tacli.(i)] on the last + m subgoals, and [tac] on the others *) +let thens3parts_tac tacfi tac tacli (sigr,gs) = let nf = Array.length tacfi in let nl = Array.length tacli in let ng = List.length gs in if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals."); - let gll,pl = - List.split + let gll = (list_map_i (fun i -> apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac)) 0 gs) in - (sigr, List.flatten gll, - compose p (mapshape (List.map List.length gll) pl)) + (sigr,List.flatten gll) (* Apply [taci.(i)] on the first n subgoals and [tac] on the others *) let thensf_tac taci tac = thens3parts_tac taci tac [||] @@ -369,10 +127,10 @@ let thensf_tac taci tac = thens3parts_tac taci tac [||] let thensl_tac tac taci = thens3parts_tac [||] tac taci (* Apply [tac i] on the ith subgoal (no subgoals number check) *) -let thensi_tac tac (sigr,gs,p) = - let gll,pl = - List.split (list_map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs) in - (sigr, List.flatten gll, compose p (mapshape (List.map List.length gll) pl)) +let thensi_tac tac (sigr,gs) = + let gll = + list_map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in + (sigr, List.flatten gll) let then_tac tac = thensf_tac [||] tac @@ -382,7 +140,7 @@ let non_existent_goal n = (* Apply tac on the i-th goal (if i>0). If i<0, then start counting from the last goal (i=-1). *) -let theni_tac i tac ((_,gl,_) as subgoals) = +let theni_tac i tac ((_,gl) as subgoals) = let nsg = List.length gl in let k = if i < 0 then nsg + i + 1 else i in if nsg < 1 then errorlabstrm "theni_tac" (str"No more subgoals.") @@ -451,42 +209,29 @@ let rec tclTHENLIST = function let tclMAP tacfun l = List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC -(* various progress criterions *) -let same_goal gl subgoal = - eq_constr (conclusion subgoal) (conclusion gl) && - eq_named_context_val (hypotheses subgoal) (hypotheses gl) - - -let weak_progress gls ptree = - (List.length gls.it <> 1) || - (not (same_goal (List.hd gls.it) ptree.it)) - -let progress gls ptree = - (progress_evar_map ptree.sigma gls.sigma) || - (weak_progress gls ptree) - +(* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves +the goal unchanged *) +let tclWEAK_PROGRESS tac ptree = + let rslt = tac ptree in + if Goal.V82.weak_progress rslt ptree then rslt + else errorlabstrm "Refiner.WEAK_PROGRESS" (str"Failed to progress.") (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves the goal unchanged *) let tclPROGRESS tac ptree = let rslt = tac ptree in - if progress (fst rslt) ptree then rslt + if Goal.V82.progress rslt ptree then rslt else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.") -(* weak_PROGRESS tac ptree applies tac to the goal ptree and fails - if tac leaves the goal unchanged, possibly modifying sigma *) -let tclWEAK_PROGRESS tac ptree = - let rslt = tac ptree in - if weak_progress (fst rslt) ptree then rslt - else errorlabstrm "Refiner.tclWEAK_PROGRESS" (str"Failed to progress.") - - (* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals, one of them being identical to the original goal *) let tclNOTSAMEGOAL (tac : tactic) goal = + let same_goal gls1 evd2 gl2 = + Goal.V82.same_goal gls1.sigma gls1.it evd2 gl2 + in let rslt = tac goal in - let gls = (fst rslt).it in - if List.exists (same_goal goal.it) gls + let {it=gls;sigma=sigma} = rslt in + if List.exists (same_goal goal sigma) gls then errorlabstrm "Refiner.tclNOTSAMEGOAL" (str"Tactic generated a subgoal identical to the original goal.") else rslt @@ -494,15 +239,15 @@ let tclNOTSAMEGOAL (tac : tactic) goal = let catch_failerror e = if catchable_exception e then check_for_interrupt () else match e with - | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) - | Stdpp.Exc_located(_, LtacLocated (_,FailError (0,_))) -> + | FailError (0,_) | Loc.Exc_located(_, FailError (0,_)) + | Loc.Exc_located(_, LtacLocated (_,FailError (0,_))) -> check_for_interrupt () | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) - | Stdpp.Exc_located(s,FailError (lvl,s')) -> - raise (Stdpp.Exc_located(s,FailError (lvl - 1, s'))) - | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> + | Loc.Exc_located(s,FailError (lvl,s')) -> + raise (Loc.Exc_located(s,FailError (lvl - 1, s'))) + | Loc.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> raise - (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s')))) + (Loc.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s')))) | e -> raise e (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) @@ -525,9 +270,9 @@ let tclORELSE_THEN t1 t2then t2else gls = with e -> catch_failerror e; None with | None -> t2else gls - | Some (sgl,v) -> + | Some sgl -> let (sigr,gl) = unpackage sgl in - finish_tac (then_tac t2then (sigr,gl,v)) + finish_tac (then_tac t2then (sigr,gl)) (* TRY f tries to apply f, and if it fails, leave the goal unchanged *) let tclTRY f = (tclORELSE0 f tclIDTAC) @@ -587,6 +332,27 @@ let tclDO n t = in dorec n +(* Fails if a tactic hasn't finished after a certain amount of time *) + +exception TacTimeout + +let tclTIMEOUT n t g = + let timeout_handler _ = raise TacTimeout in + let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in + ignore (Unix.alarm n); + let restore_timeout () = + ignore (Unix.alarm 0); + Sys.set_signal Sys.sigalrm psh + in + try + let res = t g in + restore_timeout (); + res + with + | TacTimeout | Loc.Exc_located(_,TacTimeout) -> + restore_timeout (); + errorlabstrm "Refiner.tclTIMEOUT" (str"Timeout!") + | e -> restore_timeout (); raise e (* Beware: call by need of CAML, g is needed *) let rec tclREPEAT t g = @@ -601,14 +367,12 @@ let rec tclREPEAT_MAIN t g = (*s Tactics handling a list of goals. *) -type validation_list = proof_tree list -> proof_tree list - -type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list +type tactic_list = (goal list sigma) -> (goal list sigma) (* Functions working on goal list for correct backtracking in Prolog *) let tclFIRSTLIST = tclFIRST -let tclIDTAC_list gls = (gls, fun x -> x) +let tclIDTAC_list gls = gls (* first_goal : goal list sigma -> goal sigma *) @@ -628,286 +392,20 @@ let apply_tac_list tac glls = let (sigr,lg) = unpackage glls in match lg with | (g1::rest) -> - let (gl,p) = apply_sig_tac sigr tac g1 in - let n = List.length gl in - (repackage sigr (gl@rest), - fun pfl -> let (pfg,pfrest) = list_chop n pfl in (p pfg)::pfrest) + let gl = apply_sig_tac sigr tac g1 in + repackage sigr (gl@rest) | _ -> error "apply_tac_list" let then_tactic_list tacl1 tacl2 glls = - let (glls1,pl1) = tacl1 glls in - let (glls2,pl2) = tacl2 glls1 in - (glls2, compose pl1 pl2) + let glls1 = tacl1 glls in + let glls2 = tacl2 glls1 in + glls2 (* Transform a tactic_list into a tactic *) let tactic_list_tactic tac gls = - let (glres,vl) = tac (goal_goal_list gls) in - (glres, compose idtac_valid vl) - - - -(* The type of proof-trees state and a few utilities - A proof-tree state is built from a proof-tree, a set of global - constraints, and a stack which allows to navigate inside the - proof-tree remembering how to rebuild the global proof-tree - possibly after modification of one of the focused children proof-tree. - The number in the stack corresponds to - either the selected subtree and the validation is a function from a - proof-tree list consisting only of one proof-tree to the global - proof-tree - or -1 when the move is done behind a registered tactic in which - case the validation corresponds to a constant function giving back - the original proof-tree. *) - -type pftreestate = { - tpf : proof_tree ; - tpfsigma : evar_map; - tstack : (int * validation) list } - -let proof_of_pftreestate pts = pts.tpf -let is_top_pftreestate pts = pts.tstack = [] -let cursor_of_pftreestate pts = List.map fst pts.tstack -let evc_of_pftreestate pts = pts.tpfsigma - -let top_goal_of_pftreestate pts = - { it = goal_of_proof pts.tpf; sigma = pts.tpfsigma } - -let nth_goal_of_pftreestate n pts = - let goals = fst (frontier pts.tpf) in - try {it = List.nth goals (n-1); sigma = pts.tpfsigma } - with Invalid_argument _ | Failure _ -> non_existent_goal n - -let traverse n pts = match n with - | 0 -> (* go to the parent *) - (match pts.tstack with - | [] -> error "traverse: no ancestors" - | (_,v)::tl -> - let pf = v [pts.tpf] in - let pf = norm_evar_proof pts.tpfsigma pf in - { tpf = pf; - tstack = tl; - tpfsigma = pts.tpfsigma }) - | -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *) - (match pts.tpf.ref with - | Some (Nested (_,spf),_) -> - let v = (fun pfl -> pts.tpf) in - { tpf = spf; - tstack = (-1,v)::pts.tstack; - tpfsigma = pts.tpfsigma } - | _ -> error "traverse: not a tactic-node") - | n -> (* when n>0, go to the nth child *) - let (npf,v) = descend n pts.tpf in - { tpf = npf; - tpfsigma = pts.tpfsigma; - tstack = (n,v):: pts.tstack } - -let change_constraints_pftreestate newgc pts = { pts with tpfsigma = newgc } - -let app_tac sigr tac p = - let (gll,v) = tac {it=p.goal;sigma= !sigr} in - sigr := gll.sigma; - v (List.map leaf gll.it) - -(* modify proof state at current position *) - -let map_pftreestate f pts = - let sigr = ref pts.tpfsigma in - let tpf' = f sigr pts.tpf in - let tpf'' = - if !sigr == pts.tpfsigma then tpf' else norm_evar_proof !sigr tpf' in - { tpf = tpf''; - tpfsigma = !sigr; - tstack = pts.tstack } - -(* solve the nth subgoal with tactic tac *) - -let solve_nth_pftreestate n tac = - map_pftreestate - (fun sigr pt -> frontier_map (app_tac sigr tac) n pt) - -let solve_pftreestate = solve_nth_pftreestate 1 - -(* This function implements a poor man's undo at the current goal. - This is a gross approximation as it does not attempt to clean correctly - the global constraints given in tpfsigma. *) - -let weak_undo_pftreestate pts = - let pf = leaf pts.tpf.goal in - { tpf = pf; - tpfsigma = pts.tpfsigma; - tstack = pts.tstack } - -(* Gives a new proof (a leaf) of a goal gl *) -let mk_pftreestate g = - { tpf = leaf g; - tstack = []; - tpfsigma = Evd.empty } - -(* Extracts a constr from a proof-tree state ; raises an error if the - proof is not complete or the state does not correspond to the head - of the proof-tree *) - -let extract_open_pftreestate pts = - extract_open_proof pts.tpfsigma pts.tpf - -let extract_pftreestate pts = - if pts.tstack <> [] then - errorlabstrm "extract_pftreestate" (str"Proof blocks need to be closed"); - let pfterm,subgoals = extract_open_pftreestate pts in - let exl = Evarutil.non_instantiated pts.tpfsigma in - if subgoals <> [] or exl <> [] then - errorlabstrm "extract_proof" - (if subgoals <> [] then - str "Attempt to save an incomplete proof" - else - str "Attempt to save a proof with existential variables still non-instantiated"); - let env = Global.env_of_context pts.tpf.goal.evar_hyps in - nf_betaiota_preserving_vm_cast env pts.tpfsigma pfterm - (* strong whd_betaiotaevar env pts.tpfsigma pfterm *) - (*** - local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm - ***) -(* Focus on the first leaf proof in a proof-tree state *) - -let rec first_unproven pts = - let pf = (proof_of_pftreestate pts) in - if is_complete_proof pf then - errorlabstrm "first_unproven" (str"No unproven subgoals"); - if is_leaf_proof pf then - pts - else - let childnum = - list_try_find_i - (fun n pf -> - if not(is_complete_proof pf) then n else failwith "caught") - 1 (children_of_proof pf) - in - first_unproven (traverse childnum pts) - -(* Focus on the last leaf proof in a proof-tree state *) - -let rec last_unproven pts = - let pf = proof_of_pftreestate pts in - if is_complete_proof pf then - errorlabstrm "last_unproven" (str"No unproven subgoals"); - if is_leaf_proof pf then - pts - else - let children = (children_of_proof pf) in - let nchilds = List.length children in - let childnum = - list_try_find_i - (fun n pf -> - if not(is_complete_proof pf) then n else failwith "caught") - 1 (List.rev children) - in - last_unproven (traverse (nchilds-childnum+1) pts) - -let rec nth_unproven n pts = - let pf = proof_of_pftreestate pts in - if is_complete_proof pf then - errorlabstrm "nth_unproven" (str"No unproven subgoals"); - if is_leaf_proof pf then - if n = 1 then - pts - else - errorlabstrm "nth_unproven" (str"Not enough unproven subgoals") - else - let children = children_of_proof pf in - let rec process i k = function - | [] -> - errorlabstrm "nth_unproven" (str"Not enough unproven subgoals") - | pf1::rest -> - let k1 = nb_unsolved_goals pf1 in - if k1 < k then - process (i+1) (k-k1) rest - else - nth_unproven k (traverse i pts) - in - process 1 n children - -let rec node_prev_unproven loc pts = - let pf = proof_of_pftreestate pts in - match cursor_of_pftreestate pts with - | [] -> last_unproven pts - | n::l -> - if is_complete_proof pf or loc = 1 then - node_prev_unproven n (traverse 0 pts) - else - let child = List.nth (children_of_proof pf) (loc - 2) in - if is_complete_proof child then - node_prev_unproven (loc - 1) pts - else - first_unproven (traverse (loc - 1) pts) - -let rec node_next_unproven loc pts = - let pf = proof_of_pftreestate pts in - match cursor_of_pftreestate pts with - | [] -> first_unproven pts - | n::l -> - if is_complete_proof pf || - loc = (List.length (children_of_proof pf)) then - node_next_unproven n (traverse 0 pts) - else if is_complete_proof (List.nth (children_of_proof pf) loc) then - node_next_unproven (loc + 1) pts - else - last_unproven(traverse (loc + 1) pts) - -let next_unproven pts = - let pf = proof_of_pftreestate pts in - if is_leaf_proof pf then - match cursor_of_pftreestate pts with - | [] -> error "next_unproven" - | n::_ -> node_next_unproven n (traverse 0 pts) - else - node_next_unproven (List.length (children_of_proof pf)) pts - -let prev_unproven pts = - let pf = proof_of_pftreestate pts in - if is_leaf_proof pf then - match cursor_of_pftreestate pts with - | [] -> error "prev_unproven" - | n::_ -> node_prev_unproven n (traverse 0 pts) - else - node_prev_unproven 1 pts - -let rec top_of_tree pts = - if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts) - -(* FIXME: cette fonction n'est (as of October 2007) appelée nulle part *) -let change_rule f pts = - let mark_top _ pt = - match pt.ref with - Some (oldrule,l) -> - {pt with ref=Some (f oldrule,l)} - | _ -> invalid_arg "change_rule" in - map_pftreestate mark_top pts - -let match_rule p pts = - match (proof_of_pftreestate pts).ref with - Some (r,_) -> p r - | None -> false - -let rec up_until_matching_rule p pts = - if is_top_pftreestate pts then - raise Not_found - else - let one_up = traverse 0 pts in - if match_rule p one_up then - pts - else - up_until_matching_rule p one_up - -let rec up_to_matching_rule p pts = - if match_rule p pts then - pts - else - if is_top_pftreestate pts then - raise Not_found - else - let one_up = traverse 0 pts in - up_to_matching_rule p one_up + let glres = tac (goal_goal_list gls) in + glres (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} @@ -918,42 +416,24 @@ let pp_info = ref (fun _ _ _ -> assert false) let set_info_printer f = pp_info := f let tclINFO (tac : tactic) gls = - let (sgl,v) as res = tac gls in - begin try - let pf = v (List.map leaf (sig_it sgl)) in - let sign = named_context_of_val (sig_it gls).evar_hyps in - msgnl (hov 0 (str" == " ++ - !pp_info (project gls) sign pf)) - with e when catchable_exception e -> - msgnl (hov 0 (str "Info failed to apply validation")) - end; - res - -let pp_proof = ref (fun _ _ _ -> assert false) -let set_proof_printer f = pp_proof := f - -let print_pftreestate {tpf = pf; tpfsigma = sigma; tstack = stack } = - (if stack = [] - then str "Rooted proof tree is:" - else (str "Proof tree at occurrence [" ++ - prlist_with_sep (fun () -> str ";") (fun (n,_) -> int n) - (List.rev stack) ++ str "] is:")) ++ fnl() ++ - !pp_proof sigma (Global.named_context()) pf ++ - Evd.pr_evar_map sigma + msgnl (hov 0 (str "Warning: info is currently not working")); + tac gls (* Check that holes in arguments have been resolved *) -let check_evars env sigma evm gl = +let check_evars env sigma extsigma gl = let origsigma = gl.sigma in let rest = - Evd.fold (fun ev evi acc -> - if not (Evd.mem origsigma ev) && not (Evd.is_defined sigma ev) - then Evd.add acc ev evi else acc) - evm Evd.empty + Evd.fold_undefined (fun evk evi acc -> + if Evd.is_undefined extsigma evk & not (Evd.mem origsigma evk) then + evi::acc + else + acc) + sigma [] in - if rest <> Evd.empty then - let (evk,evi) = List.hd (Evd.to_list rest) in - let (loc,k) = evar_source evk rest in + if rest <> [] then + let evi = List.hd rest in + let (loc,k) = evi.evar_source in let evi = Evarutil.nf_evar_info sigma evi in Pretype_errors.error_unsolvable_implicit loc env sigma evi k None @@ -962,5 +442,5 @@ let tclWITHHOLES accept_unresolved_holes tac sigma c gl = else let res = tclTHEN (tclEVARS sigma) (tac c) gl in if not accept_unresolved_holes then - check_evars (pf_env gl) (fst res).sigma sigma gl; + check_evars (pf_env gl) (res).sigma sigma gl; res |