From 1b92c226e563643da187b8614d5888dc4855eb43 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- plugins/decl_mode/decl_expr.mli | 2 +- plugins/decl_mode/decl_interp.ml | 12 ++-- plugins/decl_mode/decl_mode.ml | 4 +- plugins/decl_mode/decl_mode_plugin.mllib | 6 -- plugins/decl_mode/decl_mode_plugin.mlpack | 5 ++ plugins/decl_mode/decl_proof_instr.ml | 99 ++++++++++++++++++++----------- plugins/decl_mode/g_decl_mode.ml4 | 34 +++++------ plugins/decl_mode/ppdecl_proof.ml | 2 +- 8 files changed, 96 insertions(+), 68 deletions(-) delete mode 100644 plugins/decl_mode/decl_mode_plugin.mllib create mode 100644 plugins/decl_mode/decl_mode_plugin.mlpack (limited to 'plugins/decl_mode') diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 79ef3d18..29ecb94c 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -99,4 +99,4 @@ type proof_instr = (Term.constr statement, Term.constr, proof_pattern, - Tacexpr.glob_tactic_expr) gen_proof_instr + Geninterp.Val.t) gen_proof_instr diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 2a44dca2..a862423e 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Constrexpr @@ -96,7 +96,7 @@ let rec add_vars_of_simple_pattern globs = function add_vars_of_simple_pattern globs p | CPatCstr (_,_,pl1,pl2) -> List.fold_left add_vars_of_simple_pattern - (List.fold_left add_vars_of_simple_pattern globs pl1) pl2 + (Option.fold_left (List.fold_left add_vars_of_simple_pattern) globs pl1) pl2 | CPatNotation(_,_,(pl,pll),pl') -> List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pl'::pll)) | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs @@ -153,8 +153,8 @@ let interp_constr check_sort env sigma c = fst (understand env sigma (fst c)) let special_whd env = - let infos=Closure.create_clos_infos Closure.betadeltaiota env in - (fun t -> Closure.whd_val infos (Closure.inject t)) + let infos=CClosure.create_clos_infos CClosure.all env in + (fun t -> CClosure.whd_val infos (CClosure.inject t)) let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq)) @@ -384,7 +384,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = let interp_cut interp_it env sigma cut= let nenv,nstat = interp_it env sigma cut.cut_stat in - {cut with + { cut_using=Option.map (Tacinterp.Value.of_closure (Tacinterp.default_ist ())) cut.cut_using; cut_stat=nstat; cut_by=interp_justification_items nenv sigma cut.cut_by} @@ -403,7 +403,7 @@ let interp_suffices_clause env sigma (hyps,cot)= match hyp with (Hprop st | Hvar st) -> match st.st_label with - Name id -> Environ.push_named (id,None,st.st_it) env0 + Name id -> Environ.push_named (Context.Named.Declaration.LocalAssum (id,st.st_it)) env0 | _ -> env in let nenv = List.fold_right push_one locvars env in nenv,res diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index acee3d6c..92d40890 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -9,7 +9,7 @@ open Names open Term open Evd -open Errors +open CErrors open Util let daimon_flag = ref false @@ -116,7 +116,7 @@ let get_top_stack pts = let get_stack pts = Proof.get_at_focus proof_focus pts let get_last env = match Environ.named_context env with - | (id,_,_)::_ -> id + | decl :: _ -> Context.Named.Declaration.get_id decl | [] -> error "no previous statement to use" diff --git a/plugins/decl_mode/decl_mode_plugin.mllib b/plugins/decl_mode/decl_mode_plugin.mllib deleted file mode 100644 index 39342dbd..00000000 --- a/plugins/decl_mode/decl_mode_plugin.mllib +++ /dev/null @@ -1,6 +0,0 @@ -Decl_mode -Decl_interp -Decl_proof_instr -Ppdecl_proof -G_decl_mode -Decl_mode_plugin_mod diff --git a/plugins/decl_mode/decl_mode_plugin.mlpack b/plugins/decl_mode/decl_mode_plugin.mlpack new file mode 100644 index 00000000..1b84a079 --- /dev/null +++ b/plugins/decl_mode/decl_mode_plugin.mlpack @@ -0,0 +1,5 @@ +Decl_mode +Decl_interp +Decl_proof_instr +Ppdecl_proof +G_decl_mode diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index ba9fb728..d30fcf60 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Pp open Evd @@ -29,9 +29,27 @@ open Termops open Namegen open Goptions open Misctypes +open Sigma.Notations +open 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, _) -> + errorlabstrm "" (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 +60,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 +84,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 +104,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 @@ -151,7 +169,7 @@ let do_daimon () = daimon_instr env p end in - if not status then Pp.feedback Feedback.AddedAxiom else () + if not status then Feedback.feedback Feedback.AddedAxiom else () (* post-instruction focus management *) @@ -228,7 +246,8 @@ let close_previous_case pts = (* automation *) let filter_hyps f gls = - let filter_aux (id,_,_) = + let filter_aux id = + let id = get_id id in if f id then tclIDTAC else @@ -258,12 +277,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)]) @@ -272,7 +295,7 @@ let justification tac gls= error "Insufficient justification." else begin - msg_warning (str "Insufficient justification."); + warn_insufficient_justification (); daimon_tac gls end) gls @@ -330,11 +353,12 @@ 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 + let open Context.Rel.Declaration in + (llast,holes,(nlast,special_nf gls (substl lenv (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 @@ -391,7 +415,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 @@ -403,15 +427,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) @@ -465,7 +489,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 *) @@ -492,7 +516,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 = @@ -542,7 +566,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 @@ -605,7 +629,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 = @@ -615,7 +639,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 @@ -627,7 +651,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 = @@ -636,7 +660,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 *) @@ -730,7 +754,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 -> @@ -798,8 +822,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 + let body = pf_get_hyp gls id |> get_value in + Proofview.V82.of_tactic (convert_hyp (of_tuple (id,body,typ))) gls | Thesis (For _ ) -> error "\"thesis for ...\" is not applicable here." | Thesis Plain -> @@ -1199,6 +1223,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 @@ -1269,12 +1296,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 @@ -1305,7 +1332,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 *) @@ -1341,7 +1372,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 -> @@ -1353,7 +1384,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 = @@ -1361,7 +1392,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 diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index b62cfd6a..6c17dcc4 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -8,7 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Util +DECLARE PLUGIN "decl_mode_plugin" + open Compat open Pp open Decl_expr @@ -24,17 +25,14 @@ open Ppdecl_proof let pr_goal gs = let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in let env = Goal.V82.env sigma g in - let preamb,thesis,penv,pc = - (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), - (str "thesis := " ++ fnl ()), - Printer.pr_context_of env sigma, - Printer.pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) - in - preamb ++ - str" " ++ hv 0 (penv ++ fnl () ++ - str (Printer.emacs_str "") ++ - str "============================" ++ fnl () ++ - thesis ++ str " " ++ pc) ++ fnl () + let concl = Goal.V82.concl sigma g in + let goal = + Printer.pr_context_of env sigma ++ cut () ++ + str "============================" ++ cut () ++ + str "thesis :=" ++ cut () ++ + Printer.pr_goal_concl_style_env env sigma concl in + str " *** Declarative Mode ***" ++ fnl () ++ fnl () ++ + str " " ++ v 0 goal let pr_subgoals ?(pr_first=true) _ sigma _ _ _ gll = match gll with @@ -60,7 +58,7 @@ let interp_proof_instr _ { Evd.it = gl ; sigma = sigma }= let vernac_decl_proof () = let pf = Proof_global.give_me_the_proof () in if Proof.is_done pf then - Errors.error "Nothing left to prove here." + CErrors.error "Nothing left to prove here." else begin Decl_proof_instr.go_to_proof_mode () ; @@ -87,7 +85,7 @@ let vernac_proof_instr instr = (* Only declared at raw level, because only used in vernac commands. *) let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type = - Genarg.make0 None "proof_instr" + Genarg.make0 "proof_instr" (* We create a new parser entry [proof_mode]. The Declarative proof mode will replace the normal parser entry for tactics with this one. *) @@ -95,14 +93,14 @@ let proof_mode : vernac_expr Gram.entry = Gram.entry_create "vernac:proof_command" (* Auxiliary grammar entry. *) let proof_instr : raw_proof_instr Gram.entry = - Pcoq.create_generic_entry "proof_instr" (Genarg.rawwit wit_proof_instr) + Pcoq.create_generic_entry Pcoq.utactic "proof_instr" (Genarg.rawwit wit_proof_instr) let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr let classify_proof_instr = function | { instr = Pescape |Pend B_proof } -> VtProofMode "Classic", VtNow - | _ -> VtProofStep false, VtLater + | _ -> Vernac_classifier.classify_as_proofstep (* We use the VERNAC EXTEND facility with a custom non-terminal to populate [proof_mode] with a new toplevel interpreter. @@ -135,7 +133,7 @@ let _ = set = begin fun () -> (* We set the command non terminal to [proof_mode] (which we just defined). *) - G_vernac.set_command_entry proof_mode ; + Pcoq.set_command_entry proof_mode ; (* We substitute the goal printer, by the one we built for the proof mode. *) Printer.set_printer_pr { Printer.default_printer_pr with @@ -147,7 +145,7 @@ let _ = reset = begin fun () -> (* We restore the command non terminal to [noedit_mode]. *) - G_vernac.set_command_entry G_vernac.noedit_mode ; + Pcoq.set_command_entry Pcoq.Vernac_.noedit_mode ; (* We restore the goal printer to default *) Printer.set_printer_pr Printer.default_printer_pr end diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 4c71f041..59a0bb5a 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Pp open Decl_expr open Names -- cgit v1.2.3