From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- proofs/refiner.ml | 270 +++++++++++++++++------------------------------------- 1 file changed, 86 insertions(+), 184 deletions(-) (limited to 'proofs/refiner.ml') diff --git a/proofs/refiner.ml b/proofs/refiner.ml index ca82e882..974fa212 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -1,22 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - 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'}) - - - | Nested (_,_) | Decl_proof _ -> - failwith "Refiner: should not occur" - - (* Daimon is a canonical unfinished proof *) - - | Daimon -> - fun gls -> - {it=[];sigma=gls.sigma} - - -let norm_evar_tac gl = refiner (Prim Change_evars) gl +(* Profiling refiner *) +let refiner = + if Flags.profile then + let refiner_key = Profile.declare_profile "refiner" in + Profile.profile2 refiner_key refiner + else refiner (*********************) (* Tacticals *) (*********************) -let unpackage glsig = (ref (glsig.sigma)),glsig.it +let unpackage glsig = (ref (glsig.sigma)), glsig.it -let repackage r v = {it=v;sigma = !r} +let repackage r v = {it = v; sigma = !r; } let apply_sig_tac r tac g = - check_for_interrupt (); (* Breakpoint *) + Control.check_for_interrupt (); (* Breakpoint *) let glsigma = tac (repackage r g) in r := glsigma.sigma; glsigma.it (* [goal_goal_list : goal sigma -> goal list sigma] *) -let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma} - -(* forces propagation of evar constraints *) -let tclNORMEVAR = norm_evar_tac +let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; } (* identity tactic without any message *) let tclIDTAC gls = goal_goal_list gls (* the message printing identity tactic *) let tclIDTAC_MESSAGE s gls = - msg (hov 0 s); tclIDTAC gls + Pp.msg_info (hov 0 s); pp_flush (); tclIDTAC gls (* General failure tactic *) let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s) @@ -102,8 +71,8 @@ let tclFAIL lvl s g = raise (FailError (lvl,lazy s)) let tclFAIL_lazy lvl s g = raise (FailError (lvl,s)) let start_tac gls = - let (sigr,g) = unpackage gls in - (sigr,[g]) + let sigr, g = unpackage gls in + (sigr, [g]) let finish_tac (sigr,gl) = repackage sigr gl @@ -115,7 +84,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) = let ng = List.length gs in if ng + (List.map_i (fun i -> apply_sig_tac sigr (if i=ng-nl then tacli.(nl-ng+i) else tac)) 0 gs) in (sigr,List.flatten gll) @@ -123,33 +92,14 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) = (* Apply [taci.(i)] on the first n subgoals and [tac] on the others *) let thensf_tac taci tac = thens3parts_tac taci tac [||] -(* Apply [taci.(i)] on the last n subgoals and [tac] on the others *) -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) = let gll = - list_map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in + 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 -let non_existent_goal n = - errorlabstrm ("No such goal: "^(string_of_int n)) - (str"Trying to apply a tactic to a non existent goal") - -(* 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 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.") - else if k >= 1 & k <= nsg then - thensf_tac - (Array.init k (fun i -> if i+1 = k then tac else tclIDTAC)) tclIDTAC - subgoals - else non_existent_goal k - (* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls] applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m] @@ -236,26 +186,55 @@ let tclNOTSAMEGOAL (tac : tactic) goal = (str"Tactic generated a subgoal identical to the original goal.") else rslt -let catch_failerror e = - if catchable_exception e then check_for_interrupt () +(* Execute tac and show the names of hypothesis create by tac in + the "as" format. The resulting goals are printed *after* the + as-expression, which forces pg to some gymnastic. TODO: Have + something similar (better?) in the xml protocol. *) +let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) + :Proof_type.goal list Evd.sigma = + let oldhyps:Context.named_context = pf_hyps goal in + let rslt:Proof_type.goal list Evd.sigma = tac goal in + let { it = gls; sigma = sigma; } = rslt in + let hyps:Context.named_context list = + List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in + let newhyps = + List.map + (fun hypl -> List.subtract Context.eq_named_declaration hypl oldhyps) + hyps + in + let emacs_str s = + if !Flags.print_emacs then s else "" in + let s = + let frst = ref true in + List.fold_left + (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ") + ^ (List.fold_left + (fun acc (nm,_,_) -> (Names.Id.to_string nm) ^ " " ^ acc) + "" lh)) + "" newhyps in + pp (str (emacs_str "") + ++ (hov 0 (str s)) + ++ (str (emacs_str "")) ++ fnl()); + rslt;; + + +let catch_failerror (e, info) = + if catchable_exception e then Control.check_for_interrupt () else match e with - | FailError (0,_) | Loc.Exc_located(_, FailError (0,_)) - | Loc.Exc_located(_, LtacLocated (_,FailError (0,_))) -> - check_for_interrupt () - | FailError (lvl,s) -> raise (FailError (lvl - 1, 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 - (Loc.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s')))) - | e -> raise e + | FailError (0,_) -> + Control.check_for_interrupt () + | FailError (lvl,s) -> + iraise (FailError (lvl - 1, s), info) + | e -> iraise (e, info) + (** FIXME: do we need to add a [Errors.push] here? *) (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) let tclORELSE0 t1 t2 g = try t1 g with (* Breakpoint *) - | e when Errors.noncritical e -> catch_failerror e; t2 g + | e when Errors.noncritical e -> + let e = Errors.push e in catch_failerror e; t2 g (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, then applies t2 *) @@ -267,11 +246,12 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 let tclORELSE_THEN t1 t2then t2else gls = match try Some(tclPROGRESS t1 gls) - with e when Errors.noncritical e -> catch_failerror e; None + with e when Errors.noncritical e -> + let e = Errors.push e in catch_failerror e; None with | None -> t2else gls | Some sgl -> - let (sigr,gl) = unpackage sgl in + let sigr, gl = unpackage sgl in finish_tac (then_tac t2then (sigr,gl)) (* TRY f tries to apply f, and if it fails, leave the goal unchanged *) @@ -292,13 +272,17 @@ let ite_gen tcal tac_if continue tac_else gl= success:=true;result in let tac_else0 e gl= if !success then - raise e + iraise e else - tac_else gl in - try - tcal tac_if0 continue gl - with (* Breakpoint *) - | e when Errors.noncritical e -> catch_failerror e; tac_else0 e gl + try + tac_else gl + with + e' when Errors.noncritical e' -> iraise e in + try + tcal tac_if0 continue gl + with (* Breakpoint *) + | e when Errors.noncritical e -> + let e = Errors.push e in catch_failerror e; tac_else0 e gl (* Try the first tactic and, if it succeeds, continue with the second one, and if it fails, use the third one *) @@ -327,32 +311,11 @@ let tclDO n t = let rec dorec k = if k < 0 then errorlabstrm "Refiner.tclDO" (str"Wrong argument : Do needs a positive integer."); - if k = 0 then tclIDTAC - else if k = 1 then t else (tclTHEN t (dorec (k-1))) + if Int.equal k 0 then tclIDTAC + else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1))) 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!") - | reraise -> restore_timeout (); raise reraise (* Beware: call by need of CAML, g is needed *) let rec tclREPEAT t g = @@ -362,81 +325,20 @@ let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t)) (* Repeat on the first subgoal (no failure if no more subgoal) *) let rec tclREPEAT_MAIN t g = - (tclORELSE (tclTHEN_i t (fun i -> if i = 1 then (tclREPEAT_MAIN t) else + (tclORELSE (tclTHEN_i t (fun i -> if Int.equal i 1 then (tclREPEAT_MAIN t) else tclIDTAC)) tclIDTAC) g -(*s Tactics handling a list of goals. *) - -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 - -(* first_goal : goal list sigma -> goal sigma *) - -let first_goal gls = - let gl = gls.it and sig_0 = gls.sigma in - if gl = [] then error "first_goal"; - { it = List.hd gl; sigma = sig_0 } - -(* goal_goal_list : goal sigma -> goal list sigma *) - -let goal_goal_list gls = - let gl = gls.it and sig_0 = gls.sigma in { it = [gl]; sigma = sig_0 } - -(* tactic -> tactic_list : Apply a tactic to the first goal in the list *) - -let apply_tac_list tac glls = - let (sigr,lg) = unpackage glls in - match lg with - | (g1::rest) -> - 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 = tacl1 glls in - let glls2 = tacl2 glls1 in - glls2 - -(* Transform a tactic_list into a tactic *) - -let tactic_list_tactic tac gls = - let glres = tac (goal_goal_list gls) in - glres - (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} -(* Pretty-printers. *) +let tclEVARUNIVCONTEXT ctx gls = tclIDTAC {gls with sigma= Evd.set_universe_context gls.sigma ctx} -let pp_info = ref (fun _ _ _ -> assert false) -let set_info_printer f = pp_info := f +(* Push universe context *) +let tclPUSHCONTEXT rigid ctx tac gl = + tclTHEN (tclEVARS (Evd.merge_context_set rigid (project gl) ctx)) tac gl -(* Check that holes in arguments have been resolved *) +let tclPUSHEVARUNIVCONTEXT ctx gl = + tclEVARS (Evd.merge_universe_context (project gl) ctx) gl -let check_evars env sigma extsigma gl = - let origsigma = gl.sigma in - let rest = - 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 <> [] 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 - -let tclWITHHOLES accept_unresolved_holes tac sigma c gl = - if sigma == project gl then tac c gl - else - let res = tclTHEN (tclEVARS sigma) (tac c) gl in - if not accept_unresolved_holes then - check_evars (pf_env gl) (res).sigma sigma gl; - res +let tclPUSHCONSTRAINTS cst gl = + tclEVARS (Evd.add_constraints (project gl) cst) gl -- cgit v1.2.3