diff options
author | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:38:36 +0000 |
---|---|---|
committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:38:36 +0000 |
commit | 99efc1d3baaf818c1db0004e30a3fb611661a681 (patch) | |
tree | 52418e5a809d770b58296a59bfa6ec69c170ea7f | |
parent | 00d30f5330f4f1dd487d5754a0fb855a784efbf0 (diff) |
Less use of the list-based interface for goal-bound tactics.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17002 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | plugins/cc/cctac.ml | 4 | ||||
-rw-r--r-- | plugins/omega/coq_omega.ml | 2 | ||||
-rw-r--r-- | plugins/quote/quote.ml | 20 | ||||
-rw-r--r-- | proofs/proofview.ml | 1 | ||||
-rw-r--r-- | proofs/proofview.mli | 2 | ||||
-rw-r--r-- | proofs/tacmach.ml | 5 | ||||
-rw-r--r-- | proofs/tacmach.mli | 2 | ||||
-rw-r--r-- | proofs/tactic_debug.ml | 14 | ||||
-rw-r--r-- | tactics/contradiction.ml | 2 | ||||
-rw-r--r-- | tactics/elim.ml | 30 | ||||
-rw-r--r-- | tactics/equality.ml | 21 | ||||
-rw-r--r-- | tactics/extratactics.ml4 | 7 | ||||
-rw-r--r-- | tactics/inv.ml | 2 | ||||
-rw-r--r-- | tactics/tacticals.ml | 17 | ||||
-rw-r--r-- | tactics/tactics.ml | 84 | ||||
-rw-r--r-- | toplevel/auto_ind_decl.ml | 68 |
16 files changed, 139 insertions, 142 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 0d1238814..32e6d914f 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -247,7 +247,7 @@ let _M =mkMeta let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_apply Typing.type_of gl in + let type_of = Tacmach.New.pf_type_of gl in try (* type_of can raise exceptions *) match p.p_rule with Ax c -> Proofview.V82.tactic (exact_check c) @@ -473,7 +473,7 @@ let simple_reflexivity () = apply (Lazy.force _refl_equal) let f_equal = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in - let type_of = Tacmach.New.pf_apply Typing.type_of gl in + let type_of = Tacmach.New.pf_type_of gl in let cut_eq c1 c2 = try (* type_of can raise an exception *) let ty = Termops.refresh_universes (type_of c1) in diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index a647238bf..4d6f7b21f 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1653,7 +1653,7 @@ let onClearedName2 id tac = let destructure_hyps = Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_apply Typing.type_of gl in + let type_of = Tacmach.New.pf_type_of gl in let decidability = Tacmach.New.of_old decidability gl in let pf_nf = Tacmach.New.of_old pf_nf gl in let rec loop = function diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index 532a2f11d..21b221318 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -220,17 +220,16 @@ let compute_rhs bodyi index_of_f = (*s Now the function [compute_ivs] itself *) -let compute_ivs f cs = +let compute_ivs f cs gl = let cst = try destConst f with DestKO -> i_can't_do_that () in let body = Environ.constant_value (Global.env()) cst in match decomp_term body with | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> let (args3, body3) = decompose_lam body2 in let nargs3 = List.length args3 in - Goal.env >- fun env -> - Goal.defs >- fun sigma -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let is_conv = Reductionops.is_conv env sigma in - Goal.return begin match decomp_term body3 with | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *) let n_lhs_rhs = ref [] @@ -394,9 +393,6 @@ module Constrhash = Hashtbl.Make [lc: constr list]\\ [gl: goal sigma]\\ *) let quote_terms ivs lc = - (* spiwack: [Goal.return () >- fun () -> … ] suspends the effects in - [Coqlib.check_required_library]. *) - Goal.return () >- fun () -> Coqlib.check_required_library ["Coq";"quote";"Quote"]; let varhash = (Constrhash.create 17 : constr Constrhash.t) in let varlist = ref ([] : constr list) in (* list of variables *) @@ -443,10 +439,8 @@ let quote_terms ivs lc = auxl ivs.normal_lhs_rhs in let lp = List.map aux lc in - Goal.return begin (lp, (btree_of_array (Array.of_list (List.rev !varlist)) ivs.return_type )) - end (*s actually we could "quote" a list of terms instead of a single term. Ring for example needs that, but Ring doesn't use Quote @@ -456,9 +450,9 @@ let quote f lid = Proofview.Goal.enter begin fun gl -> let f = Tacmach.New.pf_global f gl in let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in - Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs -> + let ivs = compute_ivs f cl gl in let concl = Proofview.Goal.concl gl in - Proofview.Goal.lift (quote_terms ivs [concl]) >>= fun quoted_terms -> + let quoted_terms = quote_terms ivs [concl] in let (p, vm) = match quoted_terms with | [p], vm -> (p,vm) | _ -> assert false @@ -472,8 +466,8 @@ let gen_quote cont c f lid = Proofview.Goal.enter begin fun gl -> let f = Tacmach.New.pf_global f gl in let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in - Proofview.Goal.lift (compute_ivs f cl) >>= fun ivs -> - Proofview.Goal.lift (quote_terms ivs [c]) >>= fun quoted_terms -> + let ivs = compute_ivs f cl gl in + let quoted_terms = quote_terms ivs [c] in let (p, vm) = match quoted_terms with | [p], vm -> (p,vm) | _ -> assert false diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 1e0cc7c24..8a3511651 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -548,7 +548,6 @@ let in_proofview p k = type 'a glist = 'a list module Notations = struct - let (>-) = Goal.bind let (>=) = tclBIND let (>>=) t k = t >= fun l -> diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 5051e195a..207df891e 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -220,8 +220,6 @@ type 'a glist = private 'a list (* Notations for building tactics. *) module Notations : sig - (* Goal.bind *) - val (>-) : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive) -> 'b Goal.sensitive (* tclBIND *) val (>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 8e3ab5975..4928ffcfe 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -218,6 +218,11 @@ module New = struct let hyps = Environ.named_context_of_val hyps in Constrintern.construct_reference hyps id + + let pf_type_of gl t = + pf_apply type_of gl t + + let pf_ids_of_hyps gl = let hyps = Proofview.Goal.hyps gl in let hyps = Environ.named_context_of_val hyps in diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 1ca15d9ae..48c4f8d48 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -140,6 +140,8 @@ module New : sig val pf_global : identifier -> Proofview.Goal.t -> constr val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a + val pf_type_of : Proofview.Goal.t -> Term.constr -> Term.types + val pf_get_new_id : identifier -> Proofview.Goal.t -> identifier val pf_ids_of_hyps : Proofview.Goal.t -> identifier list val pf_hyps_types : Proofview.Goal.t -> (identifier * types) list diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index dc48cfc3b..1cc08fa49 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -42,22 +42,20 @@ let msg_tac_debug s = Proofview.NonLogical.print (s++fnl()) (* Prints the goal *) -let db_pr_goal = - let (>>=) = Goal.bind in - Goal.env >>= fun env -> - Goal.concl >>= fun concl -> +let db_pr_goal gl = + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl gl in let penv = print_named_context env in let pc = print_constr_env env concl in - Goal.return begin str" " ++ hv 0 (penv ++ fnl () ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () - end let db_pr_goal = - let (>>=) = Proofview.Notations.(>>=) in - Proofview.Goal.lift db_pr_goal >>= fun pg -> + Proofview.Goal.enter begin fun gl -> + let pg = db_pr_goal gl in Proofview.tclLIFT (msg_tac_debug (str "Goal:" ++ fnl () ++ pg)) + end (* Prints the commands *) diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 5a244fe7d..b5c496e26 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -87,7 +87,7 @@ let contradiction_term (c,lbind as cl) = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let type_of = Tacmach.New.pf_apply Typing.type_of gl in + let type_of = Tacmach.New.pf_type_of gl in try (* type_of can raise exceptions. *) let typ = type_of c in let _, ccl = splay_prod env sigma typ in diff --git a/tactics/elim.ml b/tactics/elim.ml index de4c58371..9c1107beb 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -87,7 +87,7 @@ let up_to_delta = ref false (* true *) let general_decompose recognizer c = Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_apply Typing.type_of gl in + let type_of = Tacmach.New.pf_type_of gl in try (* type_of can raise exceptions *) let typc = type_of c in Tacticals.New.tclTHENS (Proofview.V82.tactic (cut typc)) @@ -99,24 +99,22 @@ let general_decompose recognizer c = with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end -let head_in = - Goal.env >- fun env -> - Goal.defs >- fun sigma -> - Goal.return begin - fun indl t -> - try - let ity,_ = - if !up_to_delta - then find_mrectype env sigma t - else extract_mrectype t - in List.mem ity indl - with Not_found -> false - end +let head_in indl t gl = + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + try + let ity,_ = + if !up_to_delta + then find_mrectype env sigma t + else extract_mrectype t + in List.mem ity indl + with Not_found -> false let decompose_these c l = + Proofview.Goal.enter begin fun gl -> let indl = (*List.map inductive_of*) l in - Proofview.Goal.lift head_in >>= fun head_in -> - general_decompose (fun (_,t) -> head_in indl t) c + general_decompose (fun (_,t) -> head_in indl t gl) c + end let decompose_nonrec c = general_decompose diff --git a/tactics/equality.ml b/tactics/equality.ml index 284199586..14770af00 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -326,15 +326,15 @@ let find_elim hdcncl lft2rgt dep cls ot gl = mkConst c , eff | _ -> assert false -let type_of_clause = function - | None -> Proofview.Goal.enterl (fun gl -> Proofview.Goal.return (Proofview.Goal.concl gl)) - | Some id -> Proofview.Goal.enterl (fun gl -> Proofview.Goal.return (Tacmach.New.pf_get_hyp_typ id gl)) +let type_of_clause cls gl = match cls with + | None -> Proofview.Goal.concl gl + | Some id -> Tacmach.New.pf_get_hyp_typ id gl let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl = Proofview.Goal.enter begin fun gl -> let isatomic = isProd (whd_zeta hdcncl) in let dep_fun = if isatomic then dependent else dependent_no_evar in - type_of_clause cls >>= fun type_of_cls -> + let type_of_cls = type_of_clause cls gl in let dep = dep_proof_ok && dep_fun c type_of_cls in let (elim,effs) = Tacmach.New.of_old (find_elim hdcncl lft2rgt dep cls (Some t)) gl @@ -877,7 +877,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let onEquality with_evars tac (c,lbindc) = Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_apply Typing.type_of gl in + let type_of = Tacmach.New.pf_type_of gl in let reduce_to_quantified_ind = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl in try (* type_of can raise exceptions *) let t = type_of c in @@ -1674,20 +1674,20 @@ let cond_eq_term_right c t = Tacmach.New.of_old (cond_eq_term_right c t) let cond_eq_term c t = Tacmach.New.of_old (cond_eq_term c t) let rewrite_multi_assumption_cond cond_eq_term cl = - let rec arec = function + let rec arec hyps gl = match hyps with | [] -> error "No such assumption." | (id,_,t) ::rest -> begin try - cond_eq_term t >>= fun dir -> + let dir = cond_eq_term t gl in general_multi_rewrite dir false (mkVar id,NoBindings) cl - with | Failure _ | UserError _ -> arec rest + with | Failure _ | UserError _ -> arec rest gl end in Proofview.Goal.enter begin fun gl -> let hyps = Proofview.Goal.hyps gl in let hyps = Environ.named_context_of_val hyps in - arec hyps + arec hyps gl end let replace_multi_term dir_opt c = @@ -1697,9 +1697,6 @@ let replace_multi_term dir_opt c = | Some true -> cond_eq_term_left c | Some false -> cond_eq_term_right c in - let cond_eq_fun t = - Proofview.Goal.enterl (fun gl -> Proofview.Goal.return (cond_eq_fun t gl)) - in rewrite_multi_assumption_cond cond_eq_fun let _ = diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 088ce71d4..e4bcf658b 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -680,10 +680,8 @@ let mkCaseEq a : unit Proofview.tactic = let case_eq_intros_rewrite x = - Proofview.Goal.lift begin - Goal.concl >- fun concl -> - Goal.return (nb_prod concl) - end >>= fun n -> + Proofview.Goal.enter begin fun gl -> + let n = nb_prod (Proofview.Goal.concl gl) in (* Pp.msgnl (Printer.pr_lconstr x); *) Tacticals.New.tclTHENLIST [ mkCaseEq x; @@ -698,6 +696,7 @@ let case_eq_intros_rewrite x = rewrite_except h] end ] + end let rec find_a_destructable_match t = match kind_of_term t with diff --git a/tactics/inv.ml b/tactics/inv.ml index ebccd95b7..725508965 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -463,7 +463,7 @@ let raw_inversion inv_kind id status names = let concl = Proofview.Goal.concl gl in let c = mkVar id in let reduce_to_atomic_ind = Tacmach.New.pf_apply Tacred.reduce_to_atomic_ind gl in - let type_of = Tacmach.New.pf_apply Typing.type_of gl in + let type_of = Tacmach.New.pf_type_of gl in begin try Proofview.tclUNIT (reduce_to_atomic_ind (type_of c)) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 265af5b08..224762e0a 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -562,11 +562,9 @@ module New = struct tac2 id end - let fullGoal = - Proofview.Goal.enterl begin fun gl -> + let fullGoal gl = let hyps = Tacmach.New.pf_ids_of_hyps gl in - Proofview.Goal.return (None :: List.map Option.make hyps) - end + None :: List.map Option.make hyps let tryAllHyps tac = Proofview.Goal.enter begin fun gl -> @@ -574,8 +572,9 @@ module New = struct tclFIRST_PROGRESS_ON tac hyps end let tryAllHypsAndConcl tac = - fullGoal >>= fun fullGoal -> - tclFIRST_PROGRESS_ON tac fullGoal + Proofview.Goal.enter begin fun gl -> + tclFIRST_PROGRESS_ON tac (fullGoal gl) + end let onClause tac cl = Proofview.Goal.enter begin fun gl -> @@ -592,11 +591,7 @@ module New = struct let elim = Tacmach.New.of_old (mk_elim ind) gl in (* applying elimination_scheme just a little modified *) let indclause' = clenv_match_args indbindings indclause in - let type_of = Tacmach.New.pf_apply Typing.type_of gl in - begin try (* type_of can raise an exception *) - Proofview.Goal.return (Tacmach.New.of_old (fun gl -> mk_clenv_from gl (elim,type_of elim)) gl) - with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e - end >>= fun elimclause -> + let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_type_of gl elim)) gl in let indmv = match kind_of_term (last_arg elimclause.templval.Evd.rebus) with | Meta mv -> mv diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c317ca0d4..fd14dc938 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -421,23 +421,21 @@ type intro_name_flag = | IntroBasedOn of Id.t * Id.t list | IntroMustBe of Id.t -let find_name loc decl = function +let find_name loc decl x gl = match x with | IntroAvoid idl -> (* this case must be compatible with [find_intro_names] below. *) - Goal.env >- fun env -> - Goal.defs >- fun sigma -> - Goal.V82.to_sensitive (fresh_id idl (default_id env sigma decl)) - | IntroBasedOn (id,idl) -> Goal.V82.to_sensitive (fresh_id idl id) + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + Tacmach.New.of_old (fresh_id idl (default_id env sigma decl)) gl + | IntroBasedOn (id,idl) -> Tacmach.New.of_old (fresh_id idl id) gl | IntroMustBe id -> (* When name is given, we allow to hide a global name *) - Goal.hyps >- fun hyps -> + let hyps = Proofview.Goal.hyps gl in let hyps = Environ.named_context_of_val hyps in let ids_of_hyps = ids_of_named_context hyps in let id' = next_ident_away id ids_of_hyps in if not (Id.equal id' id) then user_err_loc (loc,"",pr_id id ++ str" is already used."); - Goal.return id' -let find_name loc decl x = - Proofview.Goal.lift (find_name loc decl x) + id' (* Returns the names that would be created by intros, without doing intros. This function is supposed to be compatible with an @@ -464,10 +462,10 @@ let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac = let concl = Proofview.Goal.concl gl in match kind_of_term concl with | Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) -> - find_name loc (name,None,t) name_flag >>= fun name -> + let name = find_name loc (name,None,t) name_flag gl in build_intro_tac name move_flag tac | LetIn (name,b,t,u) when not dep_flag || (dependent (mkRel 1) u) -> - find_name loc (name,Some b,t) name_flag >>= fun name -> + let name = find_name loc (name,Some b,t) name_flag gl in build_intro_tac name move_flag tac | _ -> begin if not force_flag then Proofview.tclZERO (RefinerError IntroNeedsProduct) @@ -1420,7 +1418,7 @@ let rewrite_hyp l2r id = tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let type_of = Tacmach.New.pf_apply Typing.type_of gl in + let type_of = Tacmach.New.pf_type_of gl in let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in try (* type_of can raise an exception *) let t = whd_betadeltaiota (type_of (mkVar id)) in @@ -1967,7 +1965,7 @@ let forward usetac ipat c = match usetac with | None -> Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_apply Typing.type_of gl in + let type_of = Tacmach.New.pf_type_of gl in begin try (* type_of can raise an exception *) let t = type_of c in Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c)) @@ -2206,7 +2204,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 = (letin_tac None (Name x) (mkVar id) None allHypsAndConcl) (atomize_one (i-1) ((mkVar x)::avoid)) | _ -> - let type_of = Tacmach.New.pf_apply Typing.type_of gl in + let type_of = Tacmach.New.pf_type_of gl in let id = id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in let x = Tacmach.New.of_old (fresh_id [] id) gl in @@ -3362,7 +3360,7 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc = | _ -> Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_apply Typing.type_of gl in + let type_of = Tacmach.New.pf_type_of gl in try (* type_of can raise an exception *) let x = id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in @@ -3586,20 +3584,21 @@ let dImp cls = let (forward_setoid_reflexivity, setoid_reflexivity) = Hook.make () let reflexivity_red allowred = + Proofview.Goal.enter begin fun gl -> (* PL: usual reflexivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) - let concl = if not allowred then Goal.concl + let concl = if not allowred then Proofview.Goal.concl gl else - Goal.concl >- fun c -> - Goal.env >- fun env -> - Goal.defs >- fun sigma -> - Goal.return (whd_betadeltaiota env sigma c) + let c = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + whd_betadeltaiota env sigma c in - Proofview.Goal.lift concl >>= fun concl -> match match_with_equality_type concl with | None -> Proofview.tclZERO NoEquationFound | Some _ -> one_constructor 1 NoBindings + end let reflexivity = Proofview.tclORELSE @@ -3641,19 +3640,19 @@ let match_with_equation c = Proofview.tclZERO NoEquationFound let symmetry_red allowred = + Proofview.Goal.enter begin fun gl -> (* PL: usual symmetry don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) let concl = if not allowred then - Goal.concl + Proofview.Goal.concl gl else - Goal.concl >- fun c -> - Goal.env >- fun env -> - Goal.defs >- fun sigma -> - Goal.return (whd_betadeltaiota env sigma c) + let c = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + whd_betadeltaiota env sigma c in - Proofview.Goal.lift concl >>= fun concl -> match_with_equation concl >= fun with_eqn -> match with_eqn with | Some eq_data,_,_ -> @@ -3663,6 +3662,7 @@ let symmetry_red allowred = (apply eq_data.sym) end | None,eq,eq_kind -> prove_symmetry eq eq_kind + end let symmetry = Proofview.tclORELSE @@ -3677,7 +3677,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_apply Typing.type_of gl in + let type_of = Tacmach.New.pf_type_of gl in try (* type_of can raise an exception *) let ctype = type_of (mkVar id) in let sign,t = decompose_prod_assum ctype in @@ -3722,41 +3722,42 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make () (* This is probably not very useful any longer *) let prove_transitivity hdcncl eq_kind t = - Proofview.Goal.lift begin match eq_kind with + Proofview.Goal.enter begin fun gl -> + let (eq1,eq2) = match eq_kind with | MonomorphicLeibnizEq (c1,c2) -> - Goal.return (mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |])) + mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]) | PolymorphicLeibnizEq (typ,c1,c2) -> - Goal.return (mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |])) + mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |]) | HeterogenousEq (typ1,c1,typ2,c2) -> - Goal.env >- fun env -> - Goal.defs >- fun sigma -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let type_of = Typing.type_of env sigma in let typt = type_of t in - Goal.return (mkApp(hdcncl, [| typ1; c1; typt ;t |]), mkApp(hdcncl, [| typt; t; typ2; c2 |])) - end >>= fun (eq1,eq2) -> + in Tacticals.New.tclTHENFIRST (Proofview.V82.tactic (cut eq2)) (Tacticals.New.tclTHENFIRST (Proofview.V82.tactic (cut eq1)) (Tacticals.New.tclTHENLIST [ Tacticals.New.tclDO 2 intro; Tacticals.New.onLastHyp simplest_case; Proofview.V82.tactic assumption ])) + end let transitivity_red allowred t = + Proofview.Goal.enter begin fun gl -> (* PL: usual transitivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) let concl = if not allowred then - Goal.concl + Proofview.Goal.concl gl else - Goal.concl >- fun c -> - Goal.env >- fun env -> - Goal.defs >- fun sigma -> - Goal.return (whd_betadeltaiota env sigma c) + let c = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + whd_betadeltaiota env sigma c in - Proofview.Goal.lift concl >>= fun concl -> match_with_equation concl >= fun with_eqn -> match with_eqn with | Some eq_data,_,_ -> @@ -3771,6 +3772,7 @@ let transitivity_red allowred t = match t with | None -> Proofview.tclZERO (Errors.UserError ("",str"etransitivity not supported for this relation.")) | Some t -> prove_transitivity eq eq_kind t + end let transitivity_gen t = Proofview.tclORELSE diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index c3d83b394..1173a2510 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -413,7 +413,7 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt = match (l1,l2) with | (t1::q1,t2::q2) -> Proofview.Goal.enter begin fun gl -> - let type_of = Tacmach.New.pf_apply Typing.type_of gl in + let type_of = Tacmach.New.pf_type_of gl in begin try (* type_of can raise an exception *) let tt1 = type_of t1 in if eq_constr t1 t2 then aux q1 q2 @@ -557,17 +557,17 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec = ( List.map (fun (_,seq,_,_ ) -> seq) list_id ) @ ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id ) in - let fresh_id s = - Goal.V82.to_sensitive begin fun gsig -> + let fresh_id s gl = + Tacmach.New.of_old begin fun gsig -> let fresh = fresh_id (!avoid) s gsig in avoid := fresh::(!avoid); fresh - end + end gl in - Proofview.Goal.lift (Goal.sensitive_list_map fresh_id first_intros) >>= fun fresh_first_intros -> - let fresh_id s = Proofview.Goal.lift (fresh_id s) in - fresh_id (Id.of_string "x") >>= fun freshn -> - fresh_id (Id.of_string "y") >>= fun freshm -> - fresh_id (Id.of_string "Z") >>= fun freshz -> + Proofview.Goal.enter begin fun gl -> + let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in + let freshn = fresh_id (Id.of_string "x") gl in + let freshm = fresh_id (Id.of_string "y") gl in + let freshz = fresh_id (Id.of_string "Z") gl in (* try with *) Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros; intro_using freshn ; @@ -586,13 +586,15 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). Tacticals.New.tclREPEAT ( Tacticals.New.tclTHENLIST [ simple_apply_in freshz (andb_prop()); - fresh_id (Id.of_string "Z") >>= fun fresht -> + Proofview.Goal.enter begin fun gl -> + let fresht = fresh_id (Id.of_string "Z") gl in (new_destruct false [Tacexpr.ElimOnConstr (Evd.empty,((mkVar freshz,NoBindings)))] None (None, Some (dl,IntroOrAndPattern [[ dl,IntroIdentifier fresht; dl,IntroIdentifier freshz]])) None) + end ]); (* Ci a1 ... an = Ci b1 ... bn @@ -620,6 +622,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). end ] + end let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") @@ -690,17 +693,17 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = ( List.map (fun (_,seq,_,_) -> seq) list_id ) @ ( List.map (fun (_,_,_,slb) -> slb) list_id ) in - let fresh_id s = - Goal.V82.to_sensitive begin fun gsig -> + let fresh_id s gl = + Tacmach.New.of_old begin fun gsig -> let fresh = fresh_id (!avoid) s gsig in avoid := fresh::(!avoid); fresh - end + end gl in - Proofview.Goal.lift (Goal.sensitive_list_map fresh_id first_intros) >>= fun fresh_first_intros -> - let fresh_id s = Proofview.Goal.lift (fresh_id s) in - fresh_id (Id.of_string "x") >>= fun freshn -> - fresh_id (Id.of_string "y") >>= fun freshm -> - fresh_id (Id.of_string "Z") >>= fun freshz -> + Proofview.Goal.enter begin fun gl -> + let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in + let freshn = fresh_id (Id.of_string "x") gl in + let freshm = fresh_id (Id.of_string "y") gl in + let freshz = fresh_id (Id.of_string "Z") gl in (* try with *) Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros; intro_using freshn ; @@ -737,6 +740,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec = Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean.")) end ] + end let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") @@ -830,17 +834,17 @@ let compute_dec_tact ind lnamesparrec nparrec = ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) @ ( List.map (fun (_,_,_,slb) -> slb) list_id ) in - let fresh_id s = - Goal.V82.to_sensitive begin fun gsig -> + let fresh_id s gl = + Tacmach.New.of_old begin fun gsig -> let fresh = fresh_id (!avoid) s gsig in avoid := fresh::(!avoid); fresh - end + end gl in - Proofview.Goal.lift (Goal.sensitive_list_map fresh_id first_intros) >>= fun fresh_first_intros -> - let fresh_id s = Proofview.Goal.lift (fresh_id s) in - fresh_id (Id.of_string "x") >>= fun freshn -> - fresh_id (Id.of_string "y") >>= fun freshm -> - fresh_id (Id.of_string "H") >>= fun freshH -> + Proofview.Goal.enter begin fun gl -> + let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in + let freshn = fresh_id (Id.of_string "x") gl in + let freshm = fresh_id (Id.of_string "y") gl in + let freshH = fresh_id (Id.of_string "H") gl in let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in let arfresh = Array.of_list fresh_first_intros in let xargs = Array.sub arfresh 0 (2*nparrec) in @@ -870,17 +874,20 @@ let compute_dec_tact ind lnamesparrec nparrec = ) (Tacticals.New.tclTHEN (destruct_on eqbnm) Auto.default_auto); - fresh_id (Id.of_string "H") >>= fun freshH2 -> + Proofview.Goal.enter begin fun gl -> + let freshH2 = fresh_id (Id.of_string "H") gl in Tacticals.New.tclTHENS (destruct_on_using (mkVar freshH) freshH2) [ (* left *) Tacticals.New.tclTHENLIST [ simplest_left; Proofview.V82.tactic (apply (mkApp(blI,Array.map(fun x->mkVar x) xargs))); Auto.default_auto - ]; + ] + ; (*right *) - fresh_id (Id.of_string "H") >>= fun freshH3 -> + Proofview.Goal.enter begin fun gl -> + let freshH3 = fresh_id (Id.of_string "H") gl in Tacticals.New.tclTHENLIST [ simplest_right ; Proofview.V82.tactic (unfold_constr (Lazy.force Coqlib.coq_not_ref)); @@ -901,8 +908,11 @@ let compute_dec_tact ind lnamesparrec nparrec = true; Equality.discr_tac false None ] + end ] + end ] + end let make_eq_decidability mind = let mib = Global.lookup_mind mind in |