From ca14b0bb67c9db000736333a056fc147c6f5199c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Sep 2015 14:16:54 +0200 Subject: Removing uselessly duplicated function in Evd. --- plugins/decl_mode/decl_proof_instr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/decl_mode/decl_proof_instr.ml') diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 714cd86341..f8ddd5f80c 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -86,7 +86,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 -- cgit v1.2.3 From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 13 Oct 2015 18:30:47 +0200 Subject: Fix some typos. --- plugins/decl_mode/decl_proof_instr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/decl_mode/decl_proof_instr.ml') diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 714cd86341..1a90806476 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -212,7 +212,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." -- cgit v1.2.3 From 4a76d2034983462175219426ec47c45a3c60d4fe Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 11 Oct 2015 14:47:52 +0200 Subject: Constraining refine to monotonic functions. --- plugins/decl_mode/decl_proof_instr.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'plugins/decl_mode/decl_proof_instr.ml') diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index d8c5b8a956..1741df533d 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -29,6 +29,7 @@ open Termops open Namegen open Goptions open Misctypes +open Sigma.Notations (* Strictness option *) @@ -1305,7 +1306,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 *) -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- plugins/decl_mode/decl_proof_instr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/decl_mode/decl_proof_instr.ml') diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 1a90806476..ba9fb728c1 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- plugins/decl_mode/decl_proof_instr.ml | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) (limited to 'plugins/decl_mode/decl_proof_instr.ml') diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index f47b355417..22a646b3f8 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -30,6 +30,7 @@ open Namegen open Goptions open Misctypes open Sigma.Notations +open Context.Named.Declaration (* Strictness option *) @@ -229,7 +230,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 @@ -331,11 +333,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 @@ -411,7 +414,7 @@ let concl_refiner metas body gls = 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 nenv = Environ.push_named (LocalAssum (_x,_A)) env in let asort = family_of_sort (Typing.sort_of nenv (ref evd) _A) in let nsubst = (n,mkVar _x)::subst in if List.is_empty rest then @@ -606,7 +609,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 = @@ -616,7 +619,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 @@ -628,7 +631,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 = @@ -637,7 +640,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 *) @@ -731,7 +734,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 -> @@ -799,8 +802,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 -> -- cgit v1.2.3 From 1a8c37ca352c95b4cd530efbbf47f0e7671d1fb3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 Feb 2016 13:31:54 +0100 Subject: Renaming functions in Typing to stick to the standard e_* scheme. --- plugins/decl_mode/decl_proof_instr.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/decl_mode/decl_proof_instr.ml') diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index f47b355417..47d8eeca28 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -404,7 +404,7 @@ 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 -> @@ -412,7 +412,7 @@ let concl_refiner metas body gls = 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 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) -- cgit v1.2.3 From f358d7b4c962f5288ad9ce2dc35802666c882422 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 22 Feb 2016 10:32:57 +0100 Subject: The tactic generic argument now returns a value rather than a glob_expr. The glob_expr was actually always embedded as a VFun, so this patch should not change anything semantically. The only change occurs in the plugin API where one should use the Tacinterp.tactic_of_value function instead of Tacinterp.eval_tactic. Moreover, this patch allows to use tactics returning arguments from the ML side. --- plugins/decl_mode/decl_proof_instr.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/decl_mode/decl_proof_instr.ml') diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index adfcb3e60d..090b293f5c 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -496,7 +496,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 = @@ -546,7 +546,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 -- cgit v1.2.3