diff options
Diffstat (limited to 'plugins/decl_mode/decl_proof_instr.ml')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 187 |
1 files changed, 126 insertions, 61 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 9d25681dcf..e19dc86c45 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Pp open Evd @@ -29,9 +29,30 @@ open Termops open Namegen open Goptions open Misctypes +open Sigma.Notations +open Context.Named.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration (* Strictness option *) +let clear ids { it = goal; sigma } = + let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in + let env = Goal.V82.env sigma goal in + let sign = Goal.V82.hyps sigma goal in + let cl = Goal.V82.concl sigma goal in + let evdref = ref (Evd.clear_metas sigma) in + let (hyps, concl) = + try Evarutil.clear_hyps_in_evi env evdref sign cl ids + with Evarutil.ClearDependencyError (id, _) -> + user_err (str "Cannot clear " ++ pr_id id) + in + let sigma = !evdref in + let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in + let sigma = Goal.V82.partial_solution_to sigma goal gl ev in + { it = [gl]; sigma } + let get_its_info gls = get_info gls.sigma gls.it let get_strictness,set_strictness = @@ -42,7 +63,7 @@ let _ = declare_bool_option { optsync = true; optdepr = false; - optname = "strict mode"; + optname = "strict proofs"; optkey = ["Strict";"Proofs"]; optread = get_strictness; optwrite = set_strictness } @@ -66,12 +87,12 @@ let tcl_erase_info gls = tcl_change_info_gen info_gen gls let special_whd gl= - let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let special_nf gl= - let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in - (fun t -> Closure.norm_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in + (fun t -> CClosure.norm_val infos (CClosure.inject t)) let is_good_inductive env ind = let mib,oib = Inductive.lookup_mind_specif env ind in @@ -86,7 +107,7 @@ Please \"suppose\" something or \"end\" it now." | _ -> () let mk_evd metalist gls = - let evd0= create_goal_evar_defs (sig_sig gls) in + let evd0= clear_metas (sig_sig gls) in let add_one (meta,typ) evd = meta_declare meta typ evd in List.fold_right add_one metalist evd0 @@ -125,25 +146,50 @@ let go_to_proof_mode () = (* closing gaps *) +(* spiwack: should use [Proofview.give_up] but that would require + moving the whole declarative mode into the new proof engine. It + will eventually have to be done. + + As far as I can tell, [daimon_tac] is used after a [thus thesis], + it will leave uninstantiated variables instead of giving a relevant + message at [Qed]. *) let daimon_tac gls = set_daimon_flag (); {it=[];sigma=sig_sig gls;} +let daimon_instr env p = + let (p,(status,_)) = + Proof.run_tactic env begin + Proofview.tclINDEPENDENT Proofview.give_up + end p + in + p,status + +let do_daimon () = + let env = Global.env () in + let status = + Proof_global.with_current_proof begin fun _ p -> + daimon_instr env p + end + in + if not status then Feedback.feedback Feedback.AddedAxiom else () + (* post-instruction focus management *) -(* spiwack: This used to fail if there was no focusing command - above, but I don't think it ever happened. I hope it doesn't mess - things up*) let goto_current_focus () = - Decl_mode.maximal_unfocus () + Decl_mode.unfocus () +(* spiwack: used to catch errors indicating lack of "focusing command" + in the proof tree. In the current implementation, however, entering + the declarative mode puts a focus first, there should, therefore, + never be exception raised here. *) let goto_current_focus_or_top () = goto_current_focus () (* return *) let close_tactic_mode () = - try goto_current_focus () + try do_daimon ();goto_current_focus () with Not_found -> error "\"return\" cannot be used outside of Declarative Proof Mode." @@ -164,7 +210,7 @@ let close_block bt pts = in match bt,stack with B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> - (goto_current_focus ()) + do_daimon ();goto_current_focus () | _, Claim::_ -> error "\"end claim\" expected." | _, Focus_claim::_ -> @@ -187,7 +233,7 @@ let close_previous_case pts = Proof.is_done pts then match get_top_stack pts with - Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...") + Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occurred ...") | Suppose_case :: Per (et,_,_,_) :: _ -> goto_current_focus () | _ -> error "Not inside a proof per cases or induction." @@ -195,7 +241,7 @@ let close_previous_case pts = match get_stack pts with Per (et,_,_,_) :: _ -> () | Suppose_case :: Per (et,_,_,_) :: _ -> - goto_current_focus () + do_daimon ();goto_current_focus () | _ -> error "Not inside a proof per cases or induction." (* Proof instructions *) @@ -203,7 +249,8 @@ let close_previous_case pts = (* automation *) let filter_hyps f gls = - let filter_aux (id,_,_) = + let filter_aux id = + let id = NamedDecl.get_id id in if f id then tclIDTAC else @@ -233,12 +280,16 @@ let prepare_goal items gls = filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls let my_automation_tac = ref - (Proofview.tclZERO (Errors.make_anomaly (Pp.str"No automation registered"))) + (Proofview.tclZERO (CErrors.make_anomaly (Pp.str"No automation registered"))) let register_automation_tac tac = my_automation_tac:= tac let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_automation_tac) +let warn_insufficient_justification = + CWarnings.create ~name:"declmode-insufficient-justification" ~category:"declmode" + (fun () -> strbrk "Insufficient justification.") + let justification tac gls= tclORELSE (tclSOLVE [tclTHEN tac (Proofview.V82.of_tactic assumption)]) @@ -247,7 +298,7 @@ let justification tac gls= error "Insufficient justification." else begin - msg_warning (str "Insufficient justification."); + warn_insufficient_justification (); daimon_tac gls end) gls @@ -305,11 +356,11 @@ let enstack_subsubgoals env se stack gls= let rc,_ = Reduction.dest_prod env apptype in let rec meta_aux last lenv = function [] -> (last,lenv,[]) - | (nam,_,typ)::q -> + | decl::q -> let nlast=succ last in let (llast,holes,metas) = meta_aux nlast (mkMeta nlast :: lenv) q in - (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in + (llast,holes,(nlast,special_nf gls (substl lenv (RelDecl.get_type decl)))::metas) in let (nlast,holes,nmetas) = meta_aux se.se_last_meta [] (List.rev rc) in let refiner = applist (appterm,List.rev holes) in @@ -366,7 +417,7 @@ let find_subsubgoal c ctyp skip submetas gls = se.se_meta submetas se.se_meta_list} else dfs (pred n) - with e when Errors.noncritical e -> + with e when CErrors.noncritical e -> begin enstack_subsubgoals env se stack gls; dfs n @@ -378,15 +429,15 @@ let concl_refiner metas body gls = let concl = pf_concl gls in let evd = sig_sig gls in let env = pf_env gls in - let sort = family_of_sort (Typing.sort_of env (ref evd) concl) in + let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in let rec aux env avoid subst = function [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen") | (n,typ)::rest -> let _A = subst_meta subst typ in let x = id_of_name_using_hdchar env _A Anonymous in let _x = fresh_id avoid x gls in - let nenv = Environ.push_named (_x,None,_A) env in - let asort = family_of_sort (Typing.sort_of nenv (ref evd) _A) in + let nenv = Environ.push_named (LocalAssum (_x,_A)) env in + let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) _A) in let nsubst = (n,mkVar _x)::subst in if List.is_empty rest then asort,_A,mkNamedLambda _x _A (subst_meta nsubst body) @@ -440,7 +491,7 @@ let thus_tac c ctyp submetas gls = Proofview.V82.of_tactic (exact_check proof) gls else let refiner = concl_refiner list proof gls in - Tactics.refine refiner gls + Tacmach.refine refiner gls (* general forward step *) @@ -467,7 +518,7 @@ let just_tac _then cut info gls0 = None -> Proofview.V82.of_tactic automation_tac gls | Some tac -> - Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in + Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in justification (tclTHEN items_tac method_tac) gls0 let instr_cut mkstat _thus _then cut gls0 = @@ -517,7 +568,7 @@ let instr_rew _thus rew_side cut gls0 = None -> Proofview.V82.of_tactic automation_tac gls | Some tac -> - Proofview.V82.of_tactic (Tacinterp.eval_tactic tac) gls in + Proofview.V82.of_tactic (Tacinterp.tactic_of_value (Tacinterp.default_ist ()) tac) gls in let just_tac gls = justification (tclTHEN items_tac method_tac) gls in let (c_id,_) = match cut.cut_stat.st_label with @@ -580,7 +631,7 @@ let assume_tac hyps gls = tclTHEN (push_intro_tac (fun id -> - Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label)) + Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label)) hyps tclIDTAC gls let assume_hyps_or_theses hyps gls = @@ -590,7 +641,7 @@ let assume_hyps_or_theses hyps gls = tclTHEN (push_intro_tac (fun id -> - Proofview.V82.of_tactic (convert_hyp (id,None,c))) nam) + Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,c)))) nam) | Hprop {st_label=nam;st_it=Thesis (tk)} -> tclTHEN (push_intro_tac @@ -602,7 +653,7 @@ let assume_st hyps gls = (fun st -> tclTHEN (push_intro_tac - (fun id -> Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) st.st_label)) + (fun id -> Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) st.st_label)) hyps tclIDTAC gls let assume_st_letin hyps gls = @@ -611,7 +662,7 @@ let assume_st_letin hyps gls = tclTHEN (push_intro_tac (fun id -> - Proofview.V82.of_tactic (convert_hyp (id,Some (fst st.st_it),snd st.st_it))) st.st_label)) + Proofview.V82.of_tactic (convert_hyp (LocalDef (id, fst st.st_it, snd st.st_it)))) st.st_label)) hyps tclIDTAC gls (* suffices *) @@ -705,7 +756,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 (Proofview.V82.of_tactic (convert_hyp (id,None,st.st_it))) + tclIFTHENELSE (Proofview.V82.of_tactic (convert_hyp (LocalAssum (id,st.st_it)))) begin match st.st_label with Anonymous -> @@ -748,7 +799,7 @@ let rec take_tac wits gls = match wits with [] -> tclIDTAC gls | wit::rest -> - let typ = pf_type_of gls wit in + let typ = pf_unsafe_type_of gls wit in tclTHEN (thus_tac wit typ []) (take_tac rest) gls @@ -772,9 +823,8 @@ let define_tac id args body gls = let cast_tac id_or_thesis typ gls = match id_or_thesis with - This id -> - let (_,body,_) = pf_get_hyp gls id in - Proofview.V82.of_tactic (convert_hyp (id,body,typ)) gls + | This id -> + Proofview.V82.of_tactic (id |> pf_get_hyp gls |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here." | Thesis Plain -> @@ -829,7 +879,7 @@ let start_tree env ind rp = let build_per_info etype casee gls = let concl=pf_concl gls in let env=pf_env gls in - let ctyp=pf_type_of gls casee in + let ctyp=pf_unsafe_type_of gls casee in let is_dep = dependent casee concl in let hd,args = decompose_app (special_whd gls ctyp) in let (ind,u) = @@ -844,7 +894,7 @@ let build_per_info etype casee gls = | _ -> mind.mind_nparams,None in let params,real_args = List.chop nparams args in let abstract_obj c body = - let typ=pf_type_of gls c in + let typ=pf_unsafe_type_of gls c in lambda_create env (typ,subst_term c body) in let pred= List.fold_right abstract_obj real_args (lambda_create env (ctyp,subst_term casee concl)) in @@ -1033,12 +1083,12 @@ let thesis_for obj typ per_info env= let cind,all_args=decompose_app typ in let ind,u = destInd cind in let _ = if not (eq_ind ind per_info.per_ind) then - errorlabstrm "thesis_for" + user_err ~hdr:"thesis_for" ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ str"cannot give an induction hypothesis (wrong inductive type).") in let params,args = List.chop per_info.per_nparams all_args in let _ = if not (List.for_all2 eq_constr params per_info.per_params) then - errorlabstrm "thesis_for" + user_err ~hdr:"thesis_for" ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ str "cannot give an induction hypothesis (wrong parameters).") in let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in @@ -1174,6 +1224,9 @@ let hrec_for fix_id per_info gls obj_id = let hd2 = applist (mkVar fix_id,args@[obj]) in compose_lam rc (Reductionops.whd_beta gls.sigma hd2) +let warn_missing_case = + CWarnings.create ~name:"declmode-missing-case" ~category:"declmode" + (fun () -> strbrk "missing case") let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = match tree, objs with @@ -1203,13 +1256,13 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let nparams = mind.mind_nparams in let concl=pf_concl gls in let env=pf_env gls in - let ctyp=pf_type_of gls casee in + let ctyp=pf_unsafe_type_of gls casee in let hd,all_args = decompose_app (special_whd gls ctyp) in let ind', u = destInd hd in let _ = assert (eq_ind ind' ind) in (* just in case *) let params,real_args = List.chop nparams all_args in let abstract_obj c body = - let typ=pf_type_of gls c in + let typ=pf_unsafe_type_of gls c in lambda_create env (typ,subst_term c body) in let elim_pred = List.fold_right abstract_obj real_args (lambda_create env (ctyp,subst_term casee concl)) in @@ -1244,12 +1297,12 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = (fun id -> hrec_for (out_name fix_name) per_info gls1 id) recs in - generalize hrecs gls1 + Proofview.V82.of_tactic (generalize hrecs) gls1 end; match bro with None -> - msg_warning (str "missing case"); - tacnext (mkMeta 1) + warn_missing_case (); + tacnext (mkMeta 1) | Some (sub_ids,tree) -> let br_args = List.filter @@ -1280,7 +1333,11 @@ let understand_my_constr env sigma c concl = Pretyping.understand_tcc env sigma ~expected_type:(Pretyping.OfType concl) (frob rawc) let my_refine c gls = - let oc sigma = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in + let oc = { run = begin fun sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in + Sigma.Unsafe.of_pair (c, sigma) + end } in Proofview.V82.of_tactic (Tactics.New.refine oc) gls (* end focus/claim *) @@ -1316,7 +1373,7 @@ let end_tac et2 gls = (default_justification (List.map mkVar clauses)) | ET_Induction,EK_nodep -> tclTHENLIST - [generalize (pi.per_args@[pi.per_casee]); + [Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee])); Proofview.V82.of_tactic (simple_induct (AnonHyp (succ (List.length pi.per_args)))); default_justification (List.map mkVar clauses)] | ET_Case_analysis,EK_dep tree -> @@ -1328,7 +1385,7 @@ let end_tac et2 gls = (initial_instance_stack clauses) [pi.per_casee] 0 tree | ET_Induction,EK_dep tree -> let nargs = (List.length pi.per_args) in - tclTHEN (generalize (pi.per_args@[pi.per_casee])) + tclTHEN (Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee]))) begin fun gls0 -> let fix_id = @@ -1336,7 +1393,7 @@ let end_tac et2 gls = let c_id = pf_get_new_id (Id.of_string "_main_arg") gls0 in tclTHENLIST - [fix (Some fix_id) (succ nargs); + [Proofview.V82.of_tactic (fix (Some fix_id) (succ nargs)); tclDO nargs (Proofview.V82.of_tactic introf); Proofview.V82.of_tactic (intro_mustbe_force c_id); execute_cases (Name fix_id) pi @@ -1444,27 +1501,35 @@ let rec postprocess pts instr = Type_errors.IllFormedRecBody(_,_,_,_,_)) -> anomaly (Pp.str "\"end induction\" generated an ill-formed fixpoint") end - | Pend _ -> - goto_current_focus_or_top () + | Pend (B_elim ET_Case_analysis) -> goto_current_focus () + | Pend B_proof -> Proof_global.set_proof_mode "Classic" + | Pend _ -> () let do_instr raw_instr pts = let has_tactic = preprocess pts raw_instr.instr in - begin + (* spiwack: hack! [preprocess] assumes that the [pts] is indeed the + current proof (and, actually so does [do_instr] later one, so + it's ok to do the same here. Ideally the proof should be properly + threaded through the commands here, but since the are interleaved + with actions on the proof mode, which is attached to the global + proof environment, it is not possible without heavy lifting. *) + let pts = Proof_global.give_me_the_proof () in + let pts = if has_tactic then let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in let gl = { it=List.hd gls ; sigma=sigma; } in let env= pf_env gl in - let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = env} in + let ist = {ltacvars = Id.Set.empty; genv = env} in let glob_instr = intern_proof_instr ist raw_instr in let instr = interp_proof_instr (get_its_info gl) env sigma glob_instr in - ignore (Pfedit.by (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp))) - else () end; - postprocess pts raw_instr.instr; - (* spiwack: this should restore a compatible semantics with - v8.3 where we never stayed focused on 0 goal. *) - Proof_global.set_proof_mode "Declarative" ; - Decl_mode.maximal_unfocus () + let (pts',_) = Proof.run_tactic (Global.env()) + (Proofview.V82.tactic (tclTHEN (eval_instr instr) clean_tmp)) pts in + pts' + else pts + in + Proof_global.simple_with_current_proof (fun _ _ -> pts); + postprocess pts raw_instr.instr let proof_instr raw_instr = let p = Proof_global.give_me_the_proof () in |