diff options
Diffstat (limited to 'proofs/refiner.ml')
| -rw-r--r-- | proofs/refiner.ml | 64 |
1 files changed, 22 insertions, 42 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index ea8543b0..be32aadd 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -1,19 +1,21 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp open CErrors open Util open Evd -open Environ open Proof_type open Logic -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration let sig_it x = x.it let project x = x.sigma @@ -21,7 +23,7 @@ let project x = x.sigma (* Getting env *) 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 pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) let refiner pr goal_sigma = let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in @@ -30,8 +32,8 @@ let refiner pr goal_sigma = (* Profiling refiner *) let refiner = if Flags.profile then - let refiner_key = Profile.declare_profile "refiner" in - Profile.profile2 refiner_key refiner + let refiner_key = CProfile.declare_profile "refiner" in + CProfile.profile2 refiner_key refiner else refiner (*********************) @@ -60,10 +62,10 @@ let tclIDTAC_MESSAGE s gls = Feedback.msg_info (hov 0 s); tclIDTAC gls (* General failure tactic *) -let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s) +let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s) (* A special exception for levels for the Fail tactic *) -exception FailError of int * std_ppcmds Lazy.t +exception FailError of int * Pp.t Lazy.t (* The Fail tactic *) let tclFAIL lvl s g = raise (FailError (lvl,lazy s)) @@ -82,7 +84,7 @@ 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."); + if ng<nf+nl then user_err ~hdr:"Refiner.thensn_tac" (str "Not enough subgoals."); 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)) @@ -161,30 +163,10 @@ let tclMAP tacfun l = (* 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 Goal.V82.progress rslt ptree then rslt - else errorlabstrm "Refiner.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 {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 + else user_err ~hdr:"Refiner.PROGRESS" (str"Failed to progress.") (* Execute tac, show the names of new hypothesis names created by tac in the "as" format and then forget everything. From the logical @@ -197,31 +179,29 @@ let tclNOTSAMEGOAL (tac : tactic) goal = destruct), this is not detected by this tactical. *) let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) :Proof_type.goal list Evd.sigma = - let oldhyps:Context.Named.t = pf_hyps goal in + let oldhyps = 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.t list = + let hyps = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in - let cmp d1 d2 = Names.Id.equal (get_id d1) (get_id d2) in + let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in let newhyps = List.map (fun hypl -> List.subtract cmp 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 d -> (Names.Id.to_string (get_id d)) ^ " " ^ acc) + (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc) "" lh)) "" newhyps in Feedback.msg_notice - (str (emacs_str "<infoH>") + (str "<infoH>" ++ (hov 0 (str s)) - ++ (str (emacs_str "</infoH>"))); + ++ (str "</infoH>")); tclIDTAC goal;; @@ -316,7 +296,7 @@ let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) let tclDO n t = let rec dorec k = - if k < 0 then errorlabstrm "Refiner.tclDO" + if k < 0 then user_err ~hdr:"Refiner.tclDO" (str"Wrong argument : Do needs a positive integer."); if Int.equal k 0 then tclIDTAC else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1))) |