From e824d429363262a9ff9db117282fe15289b5ab59 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 5 Oct 2014 15:15:58 +0200 Subject: A version of convert_concl and convert_hyp in new proof engine. Not very optimized though (if we apply convert_hyp on any hyp, a new evar will be generated for every different hyp...). --- plugins/decl_mode/decl_proof_instr.ml | 14 ++++----- plugins/omega/coq_omega.ml | 10 +++---- plugins/quote/quote.ml | 4 +-- plugins/xml/README | 15 ---------- proofs/logic.ml | 10 +++---- proofs/logic.mli | 3 ++ proofs/proofview.ml | 2 ++ proofs/proofview.mli | 2 ++ tactics/eauto.ml4 | 4 +-- tactics/rewrite.ml | 4 +-- tactics/tactics.ml | 54 +++++++++++++++++++++++++++-------- tactics/tactics.mli | 6 ++-- 12 files changed, 76 insertions(+), 52 deletions(-) delete mode 100644 plugins/xml/README diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index a21447fbb..470dc9d9c 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -580,7 +580,7 @@ let assume_tac hyps gls = tclTHEN (push_intro_tac (fun id -> - convert_hyp (id,None,st.st_it)) st.st_label)) + Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label)) hyps tclIDTAC gls let assume_hyps_or_theses hyps gls = @@ -590,7 +590,7 @@ let assume_hyps_or_theses hyps gls = tclTHEN (push_intro_tac (fun id -> - convert_hyp (id,None,c)) nam) + Proofview.V82.of_tactic (convert_hyp (id,None,c))) nam) | Hprop {st_label=nam;st_it=Thesis (tk)} -> tclTHEN (push_intro_tac @@ -602,7 +602,7 @@ let assume_st hyps gls = (fun st -> tclTHEN (push_intro_tac - (fun id -> convert_hyp (id,None,st.st_it)) st.st_label)) + (fun id -> Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label)) hyps tclIDTAC gls let assume_st_letin hyps gls = @@ -611,7 +611,7 @@ let assume_st_letin hyps gls = tclTHEN (push_intro_tac (fun id -> - convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label)) + Proofview.V82.of_tactic (convert_hyp (id,Some (fst st.st_it),snd st.st_it))) st.st_label)) hyps tclIDTAC gls (* suffices *) @@ -705,7 +705,7 @@ let rec consider_match may_intro introduced available expected gls = error "Not enough sub-hypotheses to match statements." (* should tell which ones *) | id::rest_ids,(Hvar st | Hprop st)::rest -> - tclIFTHENELSE (convert_hyp (id,None,st.st_it)) + tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) begin match st.st_label with Anonymous -> @@ -774,11 +774,11 @@ let cast_tac id_or_thesis typ gls = match id_or_thesis with This id -> let (_,body,_) = pf_get_hyp gls id in - convert_hyp (id,body,typ) gls + Proofview.V82.of_tactic (convert_hyp (id,body,typ)) gls | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here." | Thesis Plain -> - convert_concl typ DEFAULTcast gls + Proofview.V82.of_tactic (convert_concl typ DEFAULTcast) gls (* per cases *) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index f8fd71ae2..847fda8cd 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -566,7 +566,7 @@ let abstract_path typ path t = let focused_simpl path gl = let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in - convert_concl_no_check newc DEFAULTcast gl + Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl let focused_simpl path = focused_simpl path @@ -1806,15 +1806,15 @@ let destructure_hyps = match destructurate_type (pf_nf typ) with | Kapp(Nat,_) -> (Tacticals.New.tclTHEN - (Proofview.V82.tactic (convert_hyp_no_check + (convert_hyp_no_check (i,body, - (mkApp (Lazy.force coq_neq, [| t1;t2|]))))) + (mkApp (Lazy.force coq_neq, [| t1;t2|])))) (loop lit)) | Kapp(Z,_) -> (Tacticals.New.tclTHEN - (Proofview.V82.tactic (convert_hyp_no_check + (convert_hyp_no_check (i,body, - (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))) + (mkApp (Lazy.force coq_Zne, [| t1;t2|])))) (loop lit)) | _ -> loop lit end diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index ed7f18001..64166a0de 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -457,8 +457,8 @@ let quote f lid = | _ -> assert false in match ivs.variable_lhs with - | None -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast) - | Some _ -> Proofview.V82.tactic (Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast) + | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast + | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast end let gen_quote cont c f lid = diff --git a/plugins/xml/README b/plugins/xml/README deleted file mode 100644 index e3bcdaf05..000000000 --- a/plugins/xml/README +++ /dev/null @@ -1,15 +0,0 @@ -The xml export plugin for Coq has been discontinued for lack of users: -it was most certainly broken while imposing a non-negligible cost on -Coq development. Its purpose was to give export Coq's kernel objects -in xml form for treatment by external tools. - -If you are looking for such a tool, you may want to look at commit -7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9 responsible for the deletion -of this plugin (for instance, git checkout -7cfe0a70eda671ada6a46cd779ef9308f7e0fdb9^ including the "^", will lead -you to the last commit before the xml plugin was deleted). - -Bear in mind, however, that the plugin was not working properly at the -time. You may want instead to write to the original author of the -plugin, Claudio Sacerdoti-Coen at sacerdot@cs.unibo.it. He has a -stable version of the plugin for an old version of Coq. diff --git a/proofs/logic.ml b/proofs/logic.ml index 5de7b901d..2d302510e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -492,18 +492,18 @@ and mk_casegoals sigma goal goalacc p c = (acc'',lbrty,conclty,sigma,p',c') -let convert_hyp sign sigma (id,b,bt as d) = +let convert_hyp check sign sigma (id,b,bt as d) = let env = Global.env() in let reorder = ref [] in let sign' = apply_to_hyp sign id (fun _ (_,c,ct) _ -> let env = Global.env_of_context sign in - if !check && not (is_conv env sigma bt ct) then + if check && not (is_conv env sigma bt ct) then error ("Incorrect change of the type of "^(Id.to_string id)^"."); - if !check && not (Option.equal (is_conv env sigma) b c) then + if check && not (Option.equal (is_conv env sigma) b c) then error ("Incorrect change of the body of "^(Id.to_string id)^"."); - if !check then reorder := check_decl_position env sign d; + if check then reorder := check_decl_position env sign d; d) in reorder_val_context env sign' !reorder @@ -665,7 +665,7 @@ let prim_refiner r sigma goal = ([sg], sigma) | Convert_hyp (id,copt,ty) -> - let (gl,ev,sigma) = mk_goal (convert_hyp sign sigma (id,copt,ty)) cl in + let (gl,ev,sigma) = mk_goal (convert_hyp !check sign sigma (id,copt,ty)) cl in let sigma = Goal.V82.partial_solution_to sigma goal gl ev in ([gl], sigma) diff --git a/proofs/logic.mli b/proofs/logic.mli index da54ef0a8..7714b8658 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -51,3 +51,6 @@ type refiner_error = exception RefinerError of refiner_error val catchable_exception : exn -> bool + +val convert_hyp : bool -> Environ.named_context_val -> evar_map -> + Context.named_declaration -> Environ.named_context_val diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 9f8458ba7..8fe924e0f 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -877,6 +877,8 @@ module Goal = struct let hyps { env=env } = Environ.named_context env let concl { concl=concl } = concl + let raw_concl { concl=concl } = concl + let nf_enter_t = Goal.nf_enter begin fun env sigma concl self -> {env=env;sigma=sigma;concl=concl;self=self} end diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 0eae9b605..ebaa63267 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -403,6 +403,8 @@ module Goal : sig val env : 'a t -> Environ.env val sigma : 'a t -> Evd.evar_map + val raw_concl : 'a t -> Term.constr + (* [nf_enter t] execute the goal-dependent tactic [t] in each goal independently. In particular [t] need not backtrack the same way in each goal. *) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 334e0c22a..eb9ffd425 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -563,7 +563,7 @@ let autounfold_one db cl gl = if did then match cl with | Some hyp -> change_in_hyp None (fun env sigma -> sigma, c') hyp gl - | None -> convert_concl_no_check c' DEFAULTcast gl + | None -> Proofview.V82.of_tactic (convert_concl_no_check c' DEFAULTcast) gl else tclFAIL 0 (str "Nothing to unfold") gl (* Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *) @@ -611,7 +611,7 @@ END TACTIC EXTEND convert_concl_no_check -| ["convert_concl_no_check" constr(x) ] -> [ Proofview.V82.tactic (convert_concl_no_check x DEFAULTcast) ] +| ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ] END diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 63885318c..0207b9b0f 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1543,7 +1543,7 @@ let cl_rewrite_clause_newtac ?abs strat clause = | Some id, (undef, Some p, newt) -> assert_replacing id newt (new_refine (undef, p)) | Some id, (undef, None, newt) -> - Proofview.V82.tactic (Tacmach.convert_hyp_no_check (id, None, newt)) + convert_hyp_no_check (id, None, newt) | None, (undef, Some p, newt) -> Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1555,7 +1555,7 @@ let cl_rewrite_clause_newtac ?abs strat clause = Proofview.Refine.refine make end | None, (undef, None, newt) -> - Proofview.V82.tactic (Tacmach.convert_concl_no_check newt DEFAULTcast) + convert_concl_no_check newt DEFAULTcast in Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 68aac55c8..391affd11 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -118,8 +118,38 @@ let _ = let introduction = Tacmach.introduction let refine = Tacmach.refine -let convert_concl = Tacmach.convert_concl -let convert_hyp = Tacmach.convert_hyp + +let convert_concl ?(unsafe=false) ty k = + Proofview.Goal.nf_enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let conclty = Proofview.Goal.raw_concl gl in + let sigma = + if not unsafe then begin + ignore (Typing.type_of env sigma ty); + let sigma,b = Reductionops.infer_conv env sigma ty conclty in + if not b then error "Not convertible."; + sigma + end else sigma in + Tacticals.New.tclTHEN + (Proofview.V82.tclEVARS sigma) + (Proofview.Refine.refine (fun h -> + let (h,x) = Proofview.Refine.new_evar h env ty in + (h, if k == DEFAULTcast then x else mkCast(x,k,conclty)))) + end + +let convert_hyp ?(unsafe=false) d = + Proofview.Goal.nf_enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let ty = Proofview.Goal.raw_concl gl in + let sign = convert_hyp (not unsafe) (named_context_val env) sigma d in + let env = reset_with_named_context sign env in + Proofview.Refine.refine (fun h -> Proofview.Refine.new_evar h env ty) + end + +let convert_concl_no_check = convert_concl ~unsafe:true +let convert_hyp_no_check = convert_hyp ~unsafe:true let convert_gen pb x y = Proofview.Goal.enter begin fun gl -> @@ -390,11 +420,11 @@ let bind_red_expr_occurrences occs nbcl redexp = certain hypothesis *) let reduct_in_concl (redfun,sty) gl = - convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl + Proofview.V82.of_tactic (convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty) gl let reduct_in_hyp redfun (id,where) gl = - convert_hyp_no_check - (pf_reduce_decl redfun where (pf_get_hyp gl id) gl) gl + Proofview.V82.of_tactic (convert_hyp_no_check + (pf_reduce_decl redfun where (pf_get_hyp gl id) gl)) gl let revert_cast (redfun,kind as r) = if kind == DEFAULTcast then (redfun,REVERTcast) else r @@ -413,7 +443,7 @@ let tclWITHEVARS f k gl = let e_reduct_in_concl (redfun,sty) gl = tclWITHEVARS (fun env sigma -> redfun env sigma (pf_concl gl)) - (fun c -> convert_concl_no_check c sty) gl + (fun c -> Proofview.V82.of_tactic (convert_concl_no_check c sty)) gl let e_pf_reduce_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env sigma = match c with @@ -430,7 +460,7 @@ let e_pf_reduce_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env let e_reduct_in_hyp redfun (id,where) gl = tclWITHEVARS (e_pf_reduce_decl redfun where (pf_get_hyp gl id)) - convert_hyp_no_check gl + (fun s -> Proofview.V82.of_tactic (convert_hyp_no_check s)) gl type change_arg = env -> evar_map -> evar_map * constr @@ -1690,7 +1720,7 @@ let constructor_tac with_evars expctdnumopt i lbind = let apply_tac = general_apply true false with_evars None (dloc,(cons,lbind)) in (Tacticals.New.tclTHENLIST [Proofview.V82.tclEVARS sigma; - Proofview.V82.tactic (convert_concl_no_check redcl DEFAULTcast); + convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) end @@ -2098,9 +2128,9 @@ let letin_tac_gen with_eq abs ty = let (sigma,newcl,eq_tac) = eq_tac gl in Tacticals.New.tclTHENLIST [ Proofview.V82.tclEVARS sigma; - Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast); + convert_concl_no_check newcl DEFAULTcast; intro_gen (NamingMustBe (dloc,id)) (decode_hyp lastlhyp) true false; - Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls); + Tacticals.New.tclMAP convert_hyp_no_check depdecls; eq_tac ])) end @@ -3894,7 +3924,7 @@ let symmetry_red allowred = match with_eqn with | Some eq_data,_,_ -> Tacticals.New.tclTHEN - (Proofview.V82.tactic (convert_concl_no_check concl DEFAULTcast)) + (convert_concl_no_check concl DEFAULTcast) (Tacticals.New.pf_constr_of_global eq_data.sym apply) | None,eq,eq_kind -> prove_symmetry eq eq_kind end @@ -3986,7 +4016,7 @@ let transitivity_red allowred t = match with_eqn with | Some eq_data,_,_ -> Tacticals.New.tclTHEN - (Proofview.V82.tactic (convert_concl_no_check concl DEFAULTcast)) + (convert_concl_no_check concl DEFAULTcast) (match t with | None -> Tacticals.New.pf_constr_of_global eq_data.trans eapply | Some t -> Tacticals.New.pf_constr_of_global eq_data.trans (fun trans -> apply_list [trans;t])) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 6ecb48101..c2beefdfb 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -32,8 +32,10 @@ val is_quantified_hypothesis : Id.t -> goal sigma -> bool val introduction : Id.t -> tactic val refine : constr -> tactic -val convert_concl : constr -> cast_kind -> tactic -val convert_hyp : named_declaration -> tactic +val convert_concl : ?unsafe:bool -> types -> cast_kind -> unit Proofview.tactic +val convert_hyp : ?unsafe:bool -> named_declaration -> unit Proofview.tactic +val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic +val convert_hyp_no_check : named_declaration -> unit Proofview.tactic val thin : Id.t list -> tactic val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> tactic -- cgit v1.2.3