From 1bf2a088387949c13602997d181e6f7d0f014b3f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 5 May 2019 16:32:17 +0200 Subject: rewrite.ml: drop the id returned by new_instance earlier We never use this id in rewrite.ml so don't bother threading it around. --- plugins/ltac/rewrite.ml | 90 +++++++++++++++++++++++++------------------------ 1 file changed, 46 insertions(+), 44 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 164bd7e118..950115146b 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1797,9 +1797,11 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance ~pstate atts binders (name,t) fields = let program_mode = atts.program in - new_instance ~pstate ~program_mode atts.polymorphic - name binders t (Some (true, CAst.make @@ CRecord (fields))) - ~global:atts.global ~generalize:false Hints.empty_hint_info + let _id, pstate = new_instance ~pstate ~program_mode atts.polymorphic + name binders t (Some (true, CAst.make @@ CRecord (fields))) + ~global:atts.global ~generalize:false Hints.empty_hint_info + in + pstate let declare_instance_refl ~pstate atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" @@ -1819,41 +1821,41 @@ let declare_instance_trans atts binders a aeq n lemma = let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans = init_setoid (); let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in - let _, pstate = anew_instance ~pstate atts binders instance [] in + let pstate = anew_instance ~pstate atts binders instance [] in match (refl,symm,trans) with - (None, None, None) -> pstate - | (Some lemma1, None, None) -> - snd @@ declare_instance_refl ~pstate atts binders a aeq n lemma1 - | (None, Some lemma2, None) -> - snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2 - | (None, None, Some lemma3) -> - snd @@ declare_instance_trans ~pstate atts binders a aeq n lemma3 - | (Some lemma1, Some lemma2, None) -> - let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in - snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2 - | (Some lemma1, None, Some lemma3) -> - let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in - let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in - snd @@ anew_instance ~pstate atts binders instance - [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1); - (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)] - | (None, Some lemma2, Some lemma3) -> - let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in - let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in - snd @@ anew_instance ~pstate atts binders instance - [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2); - (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)] - | (Some lemma1, Some lemma2, Some lemma3) -> - let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in - let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in - let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in - snd @@ anew_instance ~pstate atts binders instance - [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1); - (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2); - (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)] + (None, None, None) -> pstate + | (Some lemma1, None, None) -> + declare_instance_refl ~pstate atts binders a aeq n lemma1 + | (None, Some lemma2, None) -> + declare_instance_sym ~pstate atts binders a aeq n lemma2 + | (None, None, Some lemma3) -> + declare_instance_trans ~pstate atts binders a aeq n lemma3 + | (Some lemma1, Some lemma2, None) -> + let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in + declare_instance_sym ~pstate atts binders a aeq n lemma2 + | (Some lemma1, None, Some lemma3) -> + let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in + let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in + anew_instance ~pstate atts binders instance + [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1); + (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)] + | (None, Some lemma2, Some lemma3) -> + let pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in + let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in + anew_instance ~pstate atts binders instance + [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2); + (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)] + | (Some lemma1, Some lemma2, Some lemma3) -> + let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in + let pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in + let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in + anew_instance ~pstate atts binders instance + [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1); + (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2); + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)] let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) @@ -1952,15 +1954,15 @@ let warn_add_setoid_deprecated = let add_setoid ~pstate atts binders a aeq t n = warn_add_setoid_deprecated ?loc:a.CAst.loc (); init_setoid (); - let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in - let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in - let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in + let pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in + let pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in + let pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in - snd @@ anew_instance ~pstate atts binders instance - [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); - (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); - (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])] + anew_instance ~pstate atts binders instance + [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); + (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])] let make_tactic name = -- cgit v1.2.3 From 1c228b648cb1755cad3ec1f38690110d6fe14bc5 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 5 May 2019 16:58:10 +0200 Subject: rewrite.ml: remove outdated comment --- plugins/ltac/rewrite.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'plugins') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 950115146b..6f84e6c18d 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1977,7 +1977,6 @@ let warn_add_morphism_deprecated = let add_morphism_infer ~pstate atts m n : Proof_global.t option = warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); - (* NB: atts.program is ignored, program mode automatically set by vernacentries *) let instance_id = add_suffix n "_Proper" in let env = Global.env () in let evd = Evd.from_env env in -- cgit v1.2.3 From 8abacf00c6c39ec98085d531737d18edc9c19b2a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 2 May 2019 19:46:02 +0200 Subject: Proof_global: pass only 1 pstate when we don't want the proof stack Typically instead of [start_proof : ontop:Proof_global.t option -> bla -> Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and the pstate is pushed on the stack by a caller around the vernacentries/mlg level. Naming can be a bit awkward, hopefully it can be improved (maybe in a followup PR). We can see some patterns appear waiting for nicer combinators, eg in mlg we often only want to work with the current proof, not the stack. Behaviour should be similar modulo bugs, let's see what CI says. --- plugins/derive/derive.ml | 4 ++-- plugins/derive/derive.mli | 2 +- plugins/derive/g_derive.mlg | 2 +- plugins/extraction/extract_env.ml | 4 ---- plugins/extraction/extract_env.mli | 2 +- plugins/extraction/g_extraction.mlg | 8 ++++++- plugins/funind/functional_principles_proofs.ml | 9 ++++---- plugins/funind/functional_principles_types.ml | 11 +++++---- plugins/funind/g_indfun.mlg | 18 ++++++++------- plugins/funind/indfun.ml | 31 +++++++++++++++----------- plugins/funind/indfun.mli | 6 ++--- plugins/funind/invfun.ml | 8 +++---- plugins/funind/recdef.ml | 20 ++++++++--------- plugins/funind/recdef.mli | 4 +--- plugins/ltac/extratactics.mlg | 2 +- plugins/ltac/g_obligations.mlg | 4 ++-- plugins/ltac/g_rewrite.mlg | 3 ++- plugins/ltac/rewrite.ml | 6 ++--- plugins/ltac/rewrite.mli | 2 +- 19 files changed, 77 insertions(+), 69 deletions(-) (limited to 'plugins') diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 4769c2dc53..9c1882dc9a 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -101,8 +101,8 @@ let start_deriving f suchthat lemma = in let terminator = Proof_global.make_terminator terminator in - let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in - Proof_global.simple_with_current_proof begin fun _ p -> + let pstate = Proof_global.start_dependent_proof lemma kind goals terminator in + Proof_global.modify_proof begin fun p -> let p,_,() = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in p end pstate diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 6bb923118e..6e4bffa0b6 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -12,4 +12,4 @@ (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] and [lemma] as the proof. *) -val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t +val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.pstate diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index 214a9d8bb5..ee076f5ae3 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -24,5 +24,5 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } | ![ proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - { fun ~pstate -> Some Derive.(start_deriving f suchthat lemma) } + { fun ~pstate -> Some (Proof_global.push ~ontop:pstate Derive.(start_deriving f suchthat lemma)) } END diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 8f17f7b2dd..c5439ffaf6 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -751,10 +751,6 @@ let extract_and_compile l = (* Show the extraction of the current ongoing proof *) let show_extraction ~pstate = - let pstate = match pstate with - | None -> CErrors.user_err Pp.(str "No ongoing proof") - | Some pstate -> pstate - in init ~inner:true false false; let prf = Proof_global.give_me_the_proof pstate in let sigma, env = Pfedit.get_current_context pstate in diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 7ba7e05019..efd5b5575f 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -40,4 +40,4 @@ val structure_for_compute : (* Show the extraction of the current ongoing proof *) -val show_extraction : pstate:Proof_global.t option -> unit +val show_extraction : pstate:Proof_global.pstate -> unit diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index db1a389fe7..d43d90af60 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -179,5 +179,11 @@ END VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY | ![ proof ] [ "Show" "Extraction" ] - -> { fun ~pstate -> let () = show_extraction ~pstate in pstate } + -> { fun ~pstate:ontop -> + let pstate = Option.map Proof_global.get_current_pstate ontop in + let pstate = match pstate with + | None -> CErrors.user_err Pp.(str "No ongoing proof") + | Some pstate -> pstate + in + let () = show_extraction ~pstate in ontop } END diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f2b9ba2ec6..e38ea992ab 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -990,7 +990,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num ] in (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) - let pstate = Lemmas.start_proof ~ontop:None + let pstate = Lemmas.start_proof (*i The next call to mk_equation_id is valid since we are constructing the lemma Ensures by: obvious i*) @@ -1000,8 +1000,9 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num lemma_type in let pstate,_ = Pfedit.by (Proofview.V82.tactic prove_replacement) pstate in - let pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in - pstate, evd + let ontop = Proof_global.push ~ontop:None pstate in + ignore(Lemmas.save_proof_proved ?proof:None ~ontop ~opaque:Proof_global.Transparent ~idopt:None); + evd let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g = @@ -1015,7 +1016,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a Ensures by: obvious i*) let equation_lemma_id = (mk_equation_id f_id) in - evd := snd @@ generate_equation_lemma !evd all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num; + evd := generate_equation_lemma !evd all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num; let _ = match e with | Option.IsNone -> diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 2c107d39d9..7b26cb0c74 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -309,7 +309,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin evd := sigma; let hook = Lemmas.mk_hook (hook new_principle_type) in let pstate = - Lemmas.start_proof ~ontop:None + Lemmas.start_proof new_princ_name (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) !evd @@ -328,8 +328,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pstate in match entries with | [entry] -> - let pstate = discard_current pstate in - (id,(entry,persistence)), hook, pstate + (id,(entry,persistence)), hook | _ -> CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") @@ -381,7 +380,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) register_with_sort InProp; register_with_sort InSet in - let ((id,(entry,g_kind)),hook,pstate) = + let ((id,(entry,g_kind)),hook) = build_functional_principle evd interactive_proof old_princ_type new_sorts funs i proof_tac hook in @@ -520,7 +519,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ s::l_schemes -> s,l_schemes | _ -> anomaly (Pp.str "") in - let ((_,(const,_)),_,pstate) = + let ((_,(const,_)),_) = try build_functional_principle evd false first_type @@ -580,7 +579,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ (* If we reach this point, the two principle are not mutually recursive We fall back to the previous method *) - let ((_,(const,_)),_,pstate) = + let ((_,(const,_)),_) = build_functional_principle evd false diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index dbfc0fc91d..b8db3dc5ce 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -190,7 +190,9 @@ VERNAC COMMAND EXTEND Function | Vernacextend.VtSideff ids, _ when hard -> Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) | x -> x } - -> { do_generate_principle false (List.map snd recsl) } + -> { fun ~pstate:ontop -> + let pstate = do_generate_principle false (List.map snd recsl) in + Proof_global.maybe_push ~ontop pstate} END { @@ -228,30 +230,30 @@ VERNAC COMMAND EXTEND NewFunctionalScheme | ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } -> - { fun ~pstate -> + { fun ~pstate:ontop -> begin try - Functional_principles_types.build_scheme fas; pstate + Functional_principles_types.build_scheme fas; ontop with | Functional_principles_types.No_graph_found -> begin match fas with | (_,fun_name,_)::_ -> begin - let pstate = make_graph ~pstate (Smartlocate.global_with_alias fun_name) in - try Functional_principles_types.build_scheme fas; pstate + let ontop = make_graph ~ontop (Smartlocate.global_with_alias fun_name) in + try Functional_principles_types.build_scheme fas; ontop with | Functional_principles_types.No_graph_found -> CErrors.user_err Pp.(str "Cannot generate induction principle(s)") | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in - warning_error names e; pstate + warning_error names e; ontop end | _ -> assert false (* we can only have non empty list *) end | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in - warning_error names e; pstate + warning_error names e; ontop end } END @@ -266,5 +268,5 @@ END (***** debug only ***) VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY | ![ proof ] ["Generate" "graph" "for" reference(c)] -> - { make_graph (Smartlocate.global_with_alias c) } + { fun ~pstate:ontop -> make_graph ~ontop (Smartlocate.global_with_alias c) } END diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a6b088de0c..d47c12a7cb 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -410,7 +410,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error with e when CErrors.noncritical e -> on_error names e -let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = +let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in @@ -432,9 +432,9 @@ let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * V (Evd.from_env (Global.env ()),[]) fixpoint_exprl in - pstate, evd,List.rev rev_pconstants + None, evd,List.rev rev_pconstants | _ -> - let pstate = ComFixpoint.do_fixpoint ~ontop:pstate Global false fixpoint_exprl in + let pstate = ComFixpoint.do_fixpoint Global false fixpoint_exprl in let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> @@ -633,8 +633,8 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex fixpoint_exprl_with_new_bl -let do_generate_principle ~pstate pconstants on_error register_built interactive_proof - (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option = +let do_generate_principle pconstants on_error register_built interactive_proof + (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.pstate option = List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; let pstate, _is_struct = match fixpoint_exprl with @@ -661,7 +661,7 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive in if register_built then register_wf name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false - else pstate, false + else None, false |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with @@ -685,7 +685,7 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive in if register_built then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true - else pstate, true + else None, true | _ -> List.iter (function ((_na,ord,_args,_body,_type),_not) -> match ord with @@ -704,8 +704,8 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive let is_rec = List.exists (is_rec fix_names) recdefs in let pstate,evd,pconstants = if register_built - then register_struct ~pstate is_rec fixpoint_exprl - else pstate, Evd.from_env (Global.env ()), pconstants + then register_struct is_rec fixpoint_exprl + else None, Evd.from_env (Global.env ()), pconstants in let evd = ref evd in generate_principle @@ -839,9 +839,7 @@ let rec get_args b t : Constrexpr.local_binder_expr list * | _ -> [],b,t -let make_graph ~pstate (f_ref : GlobRef.t) = - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in +let make_graph env sigma (f_ref : GlobRef.t) = let c,c_body = match f_ref with | ConstRef c -> @@ -902,11 +900,18 @@ let make_graph ~pstate (f_ref : GlobRef.t) = [((CAst.make id,None),None,nal_tas,t,Some b),[]] in let mp = Constant.modpath c in - let pstate = do_generate_principle ~pstate [c,Univ.Instance.empty] error_error false false expr_list in + let pstate = do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list in (* We register the infos *) List.iter (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) expr_list; pstate) +let make_graph ~ontop f_ref = + let pstate = Option.map Proof_global.get_current_pstate ontop in + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in + Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop + (make_graph env sigma f_ref) + let do_generate_principle = do_generate_principle [] warning_error true diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index acf85f539e..cf4ef23d1a 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -5,10 +5,10 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit -val do_generate_principle : pstate:Proof_global.t option -> +val do_generate_principle : bool -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - Proof_global.t option + Proof_global.pstate option val functional_induction : bool -> @@ -17,4 +17,4 @@ val functional_induction : Ltac_plugin.Tacexpr.or_and_intro_pattern option -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma -val make_graph : pstate:Proof_global.t option -> GlobRef.t -> Proof_global.t option +val make_graph : ontop:Proof_global.t option -> GlobRef.t -> Proof_global.t option diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 2a0140f02c..03568fc6c7 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -803,7 +803,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list i*) let lem_id = mk_correct_id f_id in let (typ,_) = lemmas_types_infos.(i) in - let pstate = Lemmas.start_proof ~ontop:None + let pstate = Lemmas.start_proof lem_id (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem))) !evd @@ -811,7 +811,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let pstate = fst @@ Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i))) pstate in - let _ = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in + let () = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None in let finfo = find_Function_infos (fst f_as_constant) in (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) let _,lem_cst_constr = Evd.fresh_global @@ -865,13 +865,13 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - let pstate = Lemmas.start_proof ~ontop:None lem_id + let pstate = Lemmas.start_proof lem_id (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma (fst lemmas_types_infos.(i)) in let pstate = fst (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i))) pstate) in - let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in + let () = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None in let finfo = find_Function_infos (fst f_as_constant) in let _,lem_cst_constr = Evd.fresh_global (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index de1b592337..b4d0f092d8 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -72,7 +72,7 @@ let declare_fun f_id kind ?univs value = let ce = definition_entry ?univs value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; -let defined pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None +let defined pstate = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None let def_of_const t = match (Constr.kind t) with @@ -1367,10 +1367,9 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type ) g) in - let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None in - () + Lemmas.save_pstate_proved ~pstate ~opaque:opacity ~idopt:None in - let pstate = Lemmas.start_proof ~ontop:(Some pstate) + let pstate = Lemmas.start_proof na (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) sigma gls_type ~hook:(Lemmas.mk_hook hook) in @@ -1399,7 +1398,7 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type try Some (fst @@ by (Proofview.V82.tactic tclIDTAC) pstate) (* raises UserError _ if the proof is complete *) with UserError _ -> - defined pstate + (defined pstate; None) let com_terminate tcc_lemma_name @@ -1413,7 +1412,7 @@ let com_terminate nb_args ctx hook = let start_proof env ctx (tac_start:tactic) (tac_end:tactic) = - let pstate = Lemmas.start_proof ~ontop:None thm_name + let pstate = Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook in let pstate = fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) pstate in @@ -1431,7 +1430,8 @@ let com_terminate with EmptySubgoals -> (* a non recursive function declared with measure ! *) tcc_lemma_ref := Not_needed; - defined pstate + defined pstate; + None let start_equation (f:GlobRef.t) (term_f:GlobRef.t) (cont_tactic:Id.t list -> tactic) g = @@ -1459,7 +1459,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation let evd = Evd.from_ctx uctx in let f_constr = constr_of_monomorphic_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - let pstate = Lemmas.start_proof ~ontop:None eq_name (Global, false, Proof Lemma) ~sign evd + let pstate = Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign evd (EConstr.of_constr equation_lemma_type) in let pstate = fst @@ by (Proofview.V82.tactic (start_equation f_ref terminate_ref @@ -1489,13 +1489,13 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation } ) )) pstate in - let _ = Flags.silently (fun () -> Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None) () in + let _ = Flags.silently (fun () -> Lemmas.save_pstate_proved ~pstate ~opaque:opacity ~idopt:None) () in () (* Pp.msgnl (fun _ _ -> str "eqn finished"); *) let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq - generate_induction_principle using_lemmas : Proof_global.t option = + generate_induction_principle using_lemmas : Proof_global.pstate option = let open Term in let open Constr in let open CVars in diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index a006c2c354..84d7a399e1 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -14,6 +14,4 @@ bool -> int -> Constrexpr.constr_expr -> (pconstant -> Indfun_common.tcc_lemma_value ref -> pconstant -> - pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option - - + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.pstate option diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 4c186dce09..5e4969567d 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -1118,7 +1118,7 @@ END VERNAC COMMAND EXTEND OptimizeProof | ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } -> - { fun ~pstate -> Option.map Proof_global.compact_the_proof pstate } + { fun ~pstate -> Option.map Proof_global.(modify_current_pstate compact_the_proof) pstate } | [ "Optimize" "Heap" ] => { classify_as_proofstep } -> { Gc.compact () } END diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index de3a9c9fa9..d7918a58ac 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -80,8 +80,8 @@ GRAMMAR EXTEND Gram open Obligations -let obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.obligation ~ontop:pstate obl t) tac) -let next_obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.next_obligation ~ontop:pstate obl t) tac) +let obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.obligation obl t) tac)) +let next_obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.next_obligation obl t) tac)) let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater) diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 2fad1f6b6a..e3f4b8ef59 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -280,7 +280,8 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF (* This command may or may not open a goal *) => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater } -> { - add_morphism_infer atts m n + fun ~pstate:ontop -> + Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop (add_morphism_infer atts m n) } | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { VtStartProof(GuaranteesOpacity,[n]), VtLater } diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 6f84e6c18d..efca411754 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1974,7 +1974,7 @@ let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id")) -let add_morphism_infer ~pstate atts m n : Proof_global.t option = +let add_morphism_infer atts m n : Proof_global.pstate option = warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); let instance_id = add_suffix n "_Proper" in @@ -1991,7 +1991,7 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option = add_instance (Classes.mk_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); declare_projection n instance_id (ConstRef cst); - pstate + None else let kind = Decl_kinds.Global, atts.polymorphic, Decl_kinds.DefinitionBody Decl_kinds.Instance @@ -2008,7 +2008,7 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - let pstate = Lemmas.start_proof ~ontop:pstate ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in + let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) () let add_morphism ~pstate atts binders m s n = diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index a200cb5ced..cab7d0065e 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -89,7 +89,7 @@ val add_setoid : pstate:Proof_global.t option -> rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option -val add_morphism_infer : pstate:Proof_global.t option -> rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option +val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.pstate option val add_morphism : pstate:Proof_global.t option -> rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option -- cgit v1.2.3 From b8842c3c8d6e6d9d4c19a75453fca9f94de6fa49 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 3 May 2019 14:14:40 +0200 Subject: coqpp: add new ![] specifiers for structured proof interaction ![proof_stack] is equivalent to the old meaning of ![proof]: the body has type `pstate:Proof_global.t option -> Proof_global.t option` The other specifiers are for the following body types: ~~~ ![open_proof] `is_ontop:bool -> pstate` ![maybe_open_proof] `is_ontop:bool -> pstate option` ![proof] `pstate:pstate -> pstate` ![proof_opt_query] `pstate:pstate option -> unit` ![proof_query] `pstate:pstate -> unit` ~~~ The `is_ontop` is only used for the warning message when declaring a section variable inside a proof, we could also just stop warning. The specifiers look closely related to stm classifiers, but currently they're unconnected. Notably this means that a ![proof_query] doesn't have to be classified QUERY. ![proof_stack] is only used by g_rewrite/rewrite whose behaviour I don't fully understand, maybe we can drop it in the future. For compat we may want to consider keeping ![proof] with its old meaning and using some new name for the new meaning. OTOH fixing plugins to be stricter is easier if we change it as the errors tell us where it's used. --- plugins/derive/g_derive.mlg | 4 +-- plugins/extraction/g_extraction.mlg | 10 ++---- plugins/funind/g_indfun.mlg | 25 ++++++-------- plugins/funind/indfun.ml | 11 ++---- plugins/funind/indfun.mli | 2 +- plugins/ltac/extratactics.mlg | 6 ++-- plugins/ltac/g_ltac.mlg | 8 ++--- plugins/ltac/g_obligations.mlg | 16 ++++----- plugins/ltac/g_rewrite.mlg | 55 +++++++++++++----------------- plugins/ltac/rewrite.ml | 67 ++++++++++++++++++------------------- plugins/ltac/rewrite.mli | 35 ++++++++++++++----- 11 files changed, 117 insertions(+), 122 deletions(-) (limited to 'plugins') diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index ee076f5ae3..d25b8fd01c 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -23,6 +23,6 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac } VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } -| ![ proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - { fun ~pstate -> Some (Proof_global.push ~ontop:pstate Derive.(start_deriving f suchthat lemma)) } +| ![ open_proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> + { Derive.(start_deriving f suchthat lemma) } END diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index d43d90af60..487accbc9b 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -178,12 +178,6 @@ END (* Show the extraction of the current proof *) VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY -| ![ proof ] [ "Show" "Extraction" ] - -> { fun ~pstate:ontop -> - let pstate = Option.map Proof_global.get_current_pstate ontop in - let pstate = match pstate with - | None -> CErrors.user_err Pp.(str "No ongoing proof") - | Some pstate -> pstate - in - let () = show_extraction ~pstate in ontop } +| ![ proof_query ] [ "Show" "Extraction" ] + -> { show_extraction } END diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index b8db3dc5ce..cc772e96f3 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -177,7 +177,7 @@ let () = (* TASSI: n'importe quoi ! *) VERNAC COMMAND EXTEND Function -| ![ proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] +| ![ maybe_open_proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] => { let hard = List.exists (function | _,((_,(Some { CAst.v = CMeasureRec _ } | Some { CAst.v = CWfRec _}),_,_,_),_) -> true @@ -190,9 +190,7 @@ VERNAC COMMAND EXTEND Function | Vernacextend.VtSideff ids, _ when hard -> Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) | x -> x } - -> { fun ~pstate:ontop -> - let pstate = do_generate_principle false (List.map snd recsl) in - Proof_global.maybe_push ~ontop pstate} + -> { do_generate_principle false (List.map snd recsl) } END { @@ -227,33 +225,32 @@ let warning_error names e = } VERNAC COMMAND EXTEND NewFunctionalScheme -| ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] +| ![ maybe_open_proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } -> - { fun ~pstate:ontop -> - begin + { begin try - Functional_principles_types.build_scheme fas; ontop + Functional_principles_types.build_scheme fas; None with | Functional_principles_types.No_graph_found -> begin match fas with | (_,fun_name,_)::_ -> begin - let ontop = make_graph ~ontop (Smartlocate.global_with_alias fun_name) in - try Functional_principles_types.build_scheme fas; ontop + let pstate = make_graph (Smartlocate.global_with_alias fun_name) in + try Functional_principles_types.build_scheme fas; pstate with | Functional_principles_types.No_graph_found -> CErrors.user_err Pp.(str "Cannot generate induction principle(s)") | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in - warning_error names e; ontop + warning_error names e; pstate end | _ -> assert false (* we can only have non empty list *) end | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in - warning_error names e; ontop + warning_error names e; None end } END @@ -267,6 +264,6 @@ END (***** debug only ***) VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY -| ![ proof ] ["Generate" "graph" "for" reference(c)] -> - { fun ~pstate:ontop -> make_graph ~ontop (Smartlocate.global_with_alias c) } +| ![ maybe_open_proof ] ["Generate" "graph" "for" reference(c)] -> + { make_graph (Smartlocate.global_with_alias c) } END diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d47c12a7cb..6ea2eb579f 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -839,7 +839,9 @@ let rec get_args b t : Constrexpr.local_binder_expr list * | _ -> [],b,t -let make_graph env sigma (f_ref : GlobRef.t) = +let make_graph (f_ref : GlobRef.t) = + let env = Global.env() in + let sigma = Evd.from_env env in let c,c_body = match f_ref with | ConstRef c -> @@ -907,11 +909,4 @@ let make_graph env sigma (f_ref : GlobRef.t) = expr_list; pstate) -let make_graph ~ontop f_ref = - let pstate = Option.map Proof_global.get_current_pstate ontop in - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in - Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop - (make_graph env sigma f_ref) - let do_generate_principle = do_generate_principle [] warning_error true diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index cf4ef23d1a..c803484617 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -17,4 +17,4 @@ val functional_induction : Ltac_plugin.Tacexpr.or_and_intro_pattern option -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma -val make_graph : ontop:Proof_global.t option -> GlobRef.t -> Proof_global.t option +val make_graph : GlobRef.t -> Proof_global.pstate option diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 5e4969567d..4a2fb425ac 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -934,7 +934,7 @@ END VERNAC COMMAND EXTEND GrabEvars | ![ proof ] [ "Grab" "Existential" "Variables" ] => { classify_as_proofstep } - -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p)) pstate } + -> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.V82.grab_evars p) pstate } END (* Shelves all the goals under focus. *) @@ -966,7 +966,7 @@ END VERNAC COMMAND EXTEND Unshelve | ![ proof ] [ "Unshelve" ] => { classify_as_proofstep } - -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p)) pstate } + -> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.unshelve p) pstate } END (* Gives up on the goals under focus: the goals are considered solved, @@ -1118,7 +1118,7 @@ END VERNAC COMMAND EXTEND OptimizeProof | ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } -> - { fun ~pstate -> Option.map Proof_global.(modify_current_pstate compact_the_proof) pstate } + { fun ~pstate -> Proof_global.compact_the_proof pstate } | [ "Optimize" "Heap" ] => { classify_as_proofstep } -> { Gc.compact () } END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 7eb34158e8..9bf5bd1bda 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -376,7 +376,7 @@ let () = declare_int_option { let vernac_solve ~pstate n info tcom b = let open Goal_select in - let pstate, status = Proof_global.with_current_proof (fun etac p -> + let pstate, status = Proof_global.with_proof (fun etac p -> let with_end_tac = if b then Some etac else None in let global = match n with SelectAll | SelectList _ -> true | _ -> false in let info = Option.append info !print_info_trace in @@ -388,7 +388,7 @@ let vernac_solve ~pstate n info tcom b = let p = Proof.maximal_unfocus Vernacentries.command_focus p in p,status) pstate in if not status then Feedback.feedback Feedback.AddedAxiom; - Some pstate + pstate let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s @@ -438,7 +438,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve | ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in - Vernacentries.vernac_require_open_proof vernac_solve g n t def + vernac_solve g n t def } | ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => { @@ -450,7 +450,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve VtLater } -> { let t = rm_abstract t in - Vernacentries.vernac_require_open_proof vernac_solve Goal_select.SelectAll n t def + vernac_solve Goal_select.SelectAll n t def } END diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index d7918a58ac..c01b97c14d 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -80,25 +80,25 @@ GRAMMAR EXTEND Gram open Obligations -let obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.obligation obl t) tac)) -let next_obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.next_obligation obl t) tac)) +let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac +let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater) } VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } -| ![ proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> +| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> { obligation (num, Some name, Some t) tac } -| ![ proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> +| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> { obligation (num, Some name, None) tac } -| ![ proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> +| ![ open_proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> { obligation (num, None, Some t) tac } -| ![ proof ] [ "Obligation" integer(num) withtac(tac) ] -> +| ![ open_proof ] [ "Obligation" integer(num) withtac(tac) ] -> { obligation (num, None, None) tac } -| ![ proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> +| ![ open_proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> { next_obligation (Some name) tac } -| ![ proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } +| ![ open_proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } END VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index e3f4b8ef59..bb29323858 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -180,34 +180,34 @@ TACTIC EXTEND setoid_rewrite END VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) (Some lemma2) None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) None None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> { declare_relation atts a aeq n None None None } END VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts a aeq n None (Some lemma2) None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) None (Some lemma3) } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n None None (Some lemma3) } END @@ -234,66 +234,59 @@ GRAMMAR EXTEND Gram END VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) None None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None None None } END VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None (Some lemma2) None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None None (Some lemma3) } END VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> { add_setoid atts [] a aeq t n } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> { add_setoid atts binders a aeq t n } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] + | #[ atts = rewrite_attributes; ] ![ maybe_open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater } - -> { - fun ~pstate:ontop -> - Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop (add_morphism_infer atts m n) - } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] + -> { add_morphism_infer atts m n } + | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { VtStartProof(GuaranteesOpacity,[n]), VtLater } - -> { - add_morphism atts [] m s n - } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) + -> { add_morphism atts [] m s n } + | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { VtStartProof(GuaranteesOpacity,[n]), VtLater } - -> { - add_morphism atts binders m s n - } + -> { add_morphism atts binders m s n } END TACTIC EXTEND setoid_symmetry diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index efca411754..5d57a2f27f 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -23,7 +23,6 @@ open Tacticals.New open Tactics open Pretype_errors open Typeclasses -open Classes open Constrexpr open Globnames open Evd @@ -1795,17 +1794,17 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] -let anew_instance ~pstate atts binders (name,t) fields = +let anew_instance atts binders (name,t) fields = let program_mode = atts.program in - let _id, pstate = new_instance ~pstate ~program_mode atts.polymorphic + let _id, proof = Classes.new_instance ~program_mode atts.polymorphic name binders t (Some (true, CAst.make @@ CRecord (fields))) ~global:atts.global ~generalize:false Hints.empty_hint_info in - pstate + assert (Option.is_empty proof) (* refine:false with term *) -let declare_instance_refl ~pstate atts binders a aeq n lemma = +let declare_instance_refl atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" - in anew_instance ~pstate atts binders instance + in anew_instance atts binders instance [(qualid_of_ident (Id.of_string "reflexivity"),lemma)] let declare_instance_sym atts binders a aeq n lemma = @@ -1818,41 +1817,41 @@ let declare_instance_trans atts binders a aeq n lemma = in anew_instance atts binders instance [(qualid_of_ident (Id.of_string "transitivity"),lemma)] -let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans = +let declare_relation atts ?(binders=[]) a aeq n refl symm trans = init_setoid (); let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in - let pstate = anew_instance ~pstate atts binders instance [] in + let () = anew_instance atts binders instance [] in match (refl,symm,trans) with - (None, None, None) -> pstate + (None, None, None) -> () | (Some lemma1, None, None) -> - declare_instance_refl ~pstate atts binders a aeq n lemma1 + declare_instance_refl atts binders a aeq n lemma1 | (None, Some lemma2, None) -> - declare_instance_sym ~pstate atts binders a aeq n lemma2 + declare_instance_sym atts binders a aeq n lemma2 | (None, None, Some lemma3) -> - declare_instance_trans ~pstate atts binders a aeq n lemma3 + declare_instance_trans atts binders a aeq n lemma3 | (Some lemma1, Some lemma2, None) -> - let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in - declare_instance_sym ~pstate atts binders a aeq n lemma2 + let () = declare_instance_refl atts binders a aeq n lemma1 in + declare_instance_sym atts binders a aeq n lemma2 | (Some lemma1, None, Some lemma3) -> - let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in - let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let () = declare_instance_refl atts binders a aeq n lemma1 in + let () = declare_instance_trans atts binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in - anew_instance ~pstate atts binders instance + anew_instance atts binders instance [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1); (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)] | (None, Some lemma2, Some lemma3) -> - let pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in - let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let () = declare_instance_sym atts binders a aeq n lemma2 in + let () = declare_instance_trans atts binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in - anew_instance ~pstate atts binders instance + anew_instance atts binders instance [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2); (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)] | (Some lemma1, Some lemma2, Some lemma3) -> - let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in - let pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in - let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in + let () = declare_instance_refl atts binders a aeq n lemma1 in + let () = declare_instance_sym atts binders a aeq n lemma2 in + let () = declare_instance_trans atts binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in - anew_instance ~pstate atts binders instance + anew_instance atts binders instance [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1); (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2); (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)] @@ -1951,15 +1950,15 @@ let warn_add_setoid_deprecated = CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () -> Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation.")) -let add_setoid ~pstate atts binders a aeq t n = +let add_setoid atts binders a aeq t n = warn_add_setoid_deprecated ?loc:a.CAst.loc (); init_setoid (); - let pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in - let pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in - let pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in + let () = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in + let () = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in + let () = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in - anew_instance ~pstate atts binders instance + anew_instance atts binders instance [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])] @@ -1988,7 +1987,7 @@ let add_morphism_infer atts m n : Proof_global.pstate option = (None,(instance,uctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in - add_instance (Classes.mk_instance + Classes.add_instance (Classes.mk_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); declare_projection n instance_id (ConstRef cst); None @@ -1999,7 +1998,7 @@ let add_morphism_infer atts m n : Proof_global.pstate option = let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in let hook _ _ _ = function | Globnames.ConstRef cst -> - add_instance (Classes.mk_instance + Classes.add_instance (Classes.mk_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); declare_projection n instance_id (ConstRef cst) @@ -2011,7 +2010,7 @@ let add_morphism_infer atts m n : Proof_global.pstate option = let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) () -let add_morphism ~pstate atts binders m s n = +let add_morphism atts binders m s n = init_setoid (); let instance_id = add_suffix n "_Proper" in let instance_name = (CAst.make @@ Name instance_id),None in @@ -2021,12 +2020,12 @@ let add_morphism ~pstate atts binders m s n = [cHole; s; m]) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - let _, pstate = new_instance ~pstate + let _, pstate = Classes.new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic instance_name binders instance_t None ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in - pstate + Option.get pstate (* no instance body -> always open proof *) (** Bind to "rewrite" too *) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index cab7d0065e..e1cbc46b3b 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -81,18 +81,35 @@ val cl_rewrite_clause : val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option -val declare_relation : pstate:Proof_global.t option -> rewrite_attributes -> - ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> - constr_expr option -> constr_expr option -> constr_expr option -> Proof_global.t option - -val add_setoid : pstate:Proof_global.t option -> - rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> - Id.t -> Proof_global.t option +val declare_relation + : rewrite_attributes + -> ?binders:local_binder_expr list + -> constr_expr + -> constr_expr + -> Id.t + -> constr_expr option + -> constr_expr option + -> constr_expr option + -> unit + +val add_setoid + : rewrite_attributes + -> local_binder_expr list + -> constr_expr + -> constr_expr + -> constr_expr + -> Id.t + -> unit val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.pstate option -val add_morphism : pstate:Proof_global.t option -> - rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option +val add_morphism + : rewrite_attributes + -> local_binder_expr list + -> constr_expr + -> constr_expr + -> Id.t + -> Proof_global.pstate val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr -- cgit v1.2.3 From 02fda88fc065577f3f9604477db2e03eb4d5a9b4 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 7 May 2019 14:34:06 +0200 Subject: Alternate syntax for ![]: VERNAC EXTEND Foo STATE proof eg ![proof] becomes STATE proof This commits still supports the old ![] so there is redundancy: ~~~ VERNAC EXTEND Foo STATE proof | ... VERNAC EXTEND Foo | ![proof] ... ~~~ with the ![] form being local to the rule and the STATE form applying to the whole EXTEND except for the rules with a ![]. --- plugins/derive/g_derive.mlg | 4 ++-- plugins/extraction/g_extraction.mlg | 4 ++-- plugins/funind/g_indfun.mlg | 12 ++++++------ plugins/ltac/extratactics.mlg | 8 ++++---- plugins/ltac/g_ltac.mlg | 6 +++--- plugins/ltac/g_obligations.mlg | 14 +++++++------- 6 files changed, 24 insertions(+), 24 deletions(-) (limited to 'plugins') diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index d25b8fd01c..526989fdf3 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -22,7 +22,7 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac } -VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } -| ![ open_proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> +VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof +| [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> { Derive.(start_deriving f suchthat lemma) } END diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index 487accbc9b..9ea3fbeaf4 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -177,7 +177,7 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF END (* Show the extraction of the current proof *) -VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY -| ![ proof_query ] [ "Show" "Extraction" ] +VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY STATE proof_query +| [ "Show" "Extraction" ] -> { show_extraction } END diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index cc772e96f3..8c9b1e7ba4 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -176,8 +176,8 @@ let () = } (* TASSI: n'importe quoi ! *) -VERNAC COMMAND EXTEND Function -| ![ maybe_open_proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] +VERNAC COMMAND EXTEND Function STATE maybe_open_proof +| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] => { let hard = List.exists (function | _,((_,(Some { CAst.v = CMeasureRec _ } | Some { CAst.v = CWfRec _}),_,_,_),_) -> true @@ -224,8 +224,8 @@ let warning_error names e = } -VERNAC COMMAND EXTEND NewFunctionalScheme -| ![ maybe_open_proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] +VERNAC COMMAND EXTEND NewFunctionalScheme STATE maybe_open_proof +| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } -> { begin @@ -263,7 +263,7 @@ VERNAC COMMAND EXTEND NewFunctionalCase END (***** debug only ***) -VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY -| ![ maybe_open_proof ] ["Generate" "graph" "for" reference(c)] -> +VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY STATE maybe_open_proof +| ["Generate" "graph" "for" reference(c)] -> { make_graph (Smartlocate.global_with_alias c) } END diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 4a2fb425ac..0ded60d9c7 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -931,8 +931,8 @@ END (* spiwack: I put it in extratactics because it is somewhat tied with the semantics of the LCF-style tactics, hence with the classic tactic mode. *) -VERNAC COMMAND EXTEND GrabEvars -| ![ proof ] [ "Grab" "Existential" "Variables" ] +VERNAC COMMAND EXTEND GrabEvars STATE proof +| [ "Grab" "Existential" "Variables" ] => { classify_as_proofstep } -> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.V82.grab_evars p) pstate } END @@ -963,8 +963,8 @@ TACTIC EXTEND unshelve END (* Command to add every unshelved variables to the focus *) -VERNAC COMMAND EXTEND Unshelve -| ![ proof ] [ "Unshelve" ] +VERNAC COMMAND EXTEND Unshelve STATE proof +| [ "Unshelve" ] => { classify_as_proofstep } -> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.unshelve p) pstate } END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 9bf5bd1bda..960e5b76f8 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -434,13 +434,13 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false } -VERNAC { tactic_mode } EXTEND VernacSolve -| ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +VERNAC { tactic_mode } EXTEND VernacSolve STATE proof +| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in vernac_solve g n t def } -| ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => { let anon_abstracting_tac = is_anonymous_abstract t in let solving_tac = is_explicit_terminator t in diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index c01b97c14d..58c8dabd79 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -87,18 +87,18 @@ let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), V } -VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } -| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> +VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_proof +| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> { obligation (num, Some name, Some t) tac } -| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> +| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> { obligation (num, Some name, None) tac } -| ![ open_proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> +| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> { obligation (num, None, Some t) tac } -| ![ open_proof ] [ "Obligation" integer(num) withtac(tac) ] -> +| [ "Obligation" integer(num) withtac(tac) ] -> { obligation (num, None, None) tac } -| ![ open_proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> +| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> { next_obligation (Some name) tac } -| ![ open_proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } +| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } END VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF -- cgit v1.2.3 From 445dee163b7a2c9d4cc24da739d743d80fcec529 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 20 May 2019 16:49:03 +0200 Subject: Funind: use maybe_open_proof a bit less --- plugins/funind/g_indfun.mlg | 14 +++++++------- plugins/funind/indfun.ml | 4 ++-- plugins/funind/indfun.mli | 2 +- 3 files changed, 10 insertions(+), 10 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 8c9b1e7ba4..bdd30aae0a 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -224,33 +224,33 @@ let warning_error names e = } -VERNAC COMMAND EXTEND NewFunctionalScheme STATE maybe_open_proof +VERNAC COMMAND EXTEND NewFunctionalScheme | ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } -> { begin try - Functional_principles_types.build_scheme fas; None + Functional_principles_types.build_scheme fas with | Functional_principles_types.No_graph_found -> begin match fas with | (_,fun_name,_)::_ -> begin - let pstate = make_graph (Smartlocate.global_with_alias fun_name) in - try Functional_principles_types.build_scheme fas; pstate + make_graph (Smartlocate.global_with_alias fun_name); + try Functional_principles_types.build_scheme fas with | Functional_principles_types.No_graph_found -> CErrors.user_err Pp.(str "Cannot generate induction principle(s)") | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in - warning_error names e; pstate + warning_error names e end | _ -> assert false (* we can only have non empty list *) end | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in - warning_error names e; None + warning_error names e end } END @@ -263,7 +263,7 @@ VERNAC COMMAND EXTEND NewFunctionalCase END (***** debug only ***) -VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY STATE maybe_open_proof +VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY | ["Generate" "graph" "for" reference(c)] -> { make_graph (Smartlocate.global_with_alias c) } END diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 6ea2eb579f..16df34e214 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -903,10 +903,10 @@ let make_graph (f_ref : GlobRef.t) = in let mp = Constant.modpath c in let pstate = do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list in + assert (Option.is_empty pstate); (* We register the infos *) List.iter (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) - expr_list; - pstate) + expr_list) let do_generate_principle = do_generate_principle [] warning_error true diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index c803484617..cd39266378 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -17,4 +17,4 @@ val functional_induction : Ltac_plugin.Tacexpr.or_and_intro_pattern option -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma -val make_graph : GlobRef.t -> Proof_global.pstate option +val make_graph : GlobRef.t -> unit -- cgit v1.2.3 From 99154fcb97653c606d2e62e0a0521c4afddff44c Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 20 May 2019 17:11:00 +0200 Subject: Rename Proof_global.{pstate -> t} --- plugins/derive/derive.mli | 2 +- plugins/extraction/extract_env.mli | 2 +- plugins/funind/indfun.ml | 2 +- plugins/funind/indfun.mli | 2 +- plugins/funind/recdef.ml | 2 +- plugins/funind/recdef.mli | 2 +- plugins/ltac/rewrite.ml | 2 +- plugins/ltac/rewrite.mli | 4 ++-- 8 files changed, 9 insertions(+), 9 deletions(-) (limited to 'plugins') diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 6e4bffa0b6..6bb923118e 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -12,4 +12,4 @@ (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] and [lemma] as the proof. *) -val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.pstate +val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index efd5b5575f..7d04fee7c1 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -40,4 +40,4 @@ val structure_for_compute : (* Show the extraction of the current ongoing proof *) -val show_extraction : pstate:Proof_global.pstate -> unit +val show_extraction : pstate:Proof_global.t -> unit diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 16df34e214..7c6669d0fc 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -634,7 +634,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex let do_generate_principle pconstants on_error register_built interactive_proof - (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.pstate option = + (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option = List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; let pstate, _is_struct = match fixpoint_exprl with diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index cd39266378..47d37b29a5 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -8,7 +8,7 @@ val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit val do_generate_principle : bool -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - Proof_global.pstate option + Proof_global.t option val functional_induction : bool -> diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b4d0f092d8..5a682e7231 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1495,7 +1495,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq - generate_induction_principle using_lemmas : Proof_global.pstate option = + generate_induction_principle using_lemmas : Proof_global.t option = let open Term in let open Constr in let open CVars in diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index 84d7a399e1..90f9c449b1 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -14,4 +14,4 @@ bool -> int -> Constrexpr.constr_expr -> (pconstant -> Indfun_common.tcc_lemma_value ref -> pconstant -> - pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.pstate option + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 5d57a2f27f..26d477fee0 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1973,7 +1973,7 @@ let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id")) -let add_morphism_infer atts m n : Proof_global.pstate option = +let add_morphism_infer atts m n : Proof_global.t option = warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); let instance_id = add_suffix n "_Proper" in diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index e1cbc46b3b..5aabb946d5 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -101,7 +101,7 @@ val add_setoid -> Id.t -> unit -val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.pstate option +val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option val add_morphism : rewrite_attributes @@ -109,7 +109,7 @@ val add_morphism -> constr_expr -> constr_expr -> Id.t - -> Proof_global.pstate + -> Proof_global.t val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr -- cgit v1.2.3 From 0f1814bcbaafbd93d7c7587eef8826a80b65477f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 17:52:19 +0200 Subject: [function] always open a proof when used with `wf` or `measure` --- plugins/funind/g_indfun.mlg | 47 ++++++++++++++++++++++++++++++--------------- plugins/funind/indfun.ml | 36 ++++++++++++++++++++++++---------- plugins/funind/indfun.mli | 6 ++++-- plugins/funind/recdef.ml | 13 ++++++------- plugins/funind/recdef.mli | 24 ++++++++++++++--------- 5 files changed, 83 insertions(+), 43 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index bdd30aae0a..833ff9f1ed 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -173,24 +173,41 @@ let () = let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer +let is_proof_termination_interactively_checked recsl = + List.exists (function + | _,((_,( Some { CAst.v = CMeasureRec _ } + | Some { CAst.v = CWfRec _}),_,_,_),_) -> true + | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_) + | _,((_,None,_,_,_),_) -> false) recsl + +let classify_as_Fixpoint recsl = + Vernac_classifier.classify_vernac + (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) + +let classify_funind recsl = + match classify_as_Fixpoint recsl with + | Vernacextend.VtSideff ids, _ + when is_proof_termination_interactively_checked recsl -> + Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) + | x -> x + +let is_interactive recsl = + match classify_funind recsl with + | Vernacextend.VtStartProof _, _ -> true + | _ -> false + } -(* TASSI: n'importe quoi ! *) -VERNAC COMMAND EXTEND Function STATE maybe_open_proof +VERNAC COMMAND EXTEND Function STATE CUSTOM | ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] - => { let hard = List.exists (function - | _,((_,(Some { CAst.v = CMeasureRec _ } - | Some { CAst.v = CWfRec _}),_,_,_),_) -> true - | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_) - | _,((_,None,_,_,_),_) -> false) recsl in - match - Vernac_classifier.classify_vernac - (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) - with - | Vernacextend.VtSideff ids, _ when hard -> - Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) - | x -> x } - -> { do_generate_principle false (List.map snd recsl) } + => { classify_funind recsl } + -> { + if is_interactive recsl then + Vernacextend.VtOpenProof (fun () -> + do_generate_principle_interactive (List.map snd recsl)) + else + Vernacextend.VtDefault (fun () -> + do_generate_principle (List.map snd recsl)) } END { diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 7c6669d0fc..bb6db1f5cf 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -459,7 +459,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation -let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body +let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body pre_hook = let type_of_f = Constrexpr_ops.mkCProdN args ret_type in @@ -500,8 +500,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas (* No proof done *) () in - Recdef.recursive_definition - is_mes fname rec_impls + Recdef.recursive_definition ~interactive_proof + ~is_mes fname rec_impls type_of_f wf_rel_expr rec_arg_num @@ -510,7 +510,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas using_lemmas -let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas args ret_type body = +let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas args ret_type body = let wf_arg_type,wf_arg = match wf_arg with | None -> @@ -570,7 +570,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas in wf_rel_with_mes,false in - register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg + register_wf interactive_proof ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg using_lemmas args ret_type body let map_option f = function @@ -633,7 +633,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex fixpoint_exprl_with_new_bl -let do_generate_principle pconstants on_error register_built interactive_proof +let do_generate_principle_aux pconstants on_error register_built interactive_proof (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option = List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; let pstate, _is_struct = @@ -660,7 +660,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof true in if register_built - then register_wf name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false + then register_wf interactive_proof name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false else None, false |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = @@ -684,7 +684,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof true in if register_built - then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true + then register_mes interactive_proof name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true else None, true | _ -> List.iter (function ((_na,ord,_args,_body,_type),_not) -> @@ -902,11 +902,27 @@ let make_graph (f_ref : GlobRef.t) = [((CAst.make id,None),None,nal_tas,t,Some b),[]] in let mp = Constant.modpath c in - let pstate = do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list in + let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error false false expr_list in assert (Option.is_empty pstate); (* We register the infos *) List.iter (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) expr_list) -let do_generate_principle = do_generate_principle [] warning_error true +(* *************** statically typed entrypoints ************************* *) + +let do_generate_principle_interactive fixl : Proof_global.t = + match + do_generate_principle_aux [] warning_error true true fixl + with + | Some pstate -> pstate + | None -> + CErrors.anomaly + (Pp.str"indfun: leaving no open proof in interactive mode") + +let do_generate_principle fixl : unit = + match do_generate_principle_aux [] warning_error true false fixl with + | Some _pstate -> + CErrors.anomaly + (Pp.str"indfun: leaving a goal open in non-interactive mode") + | None -> () diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 47d37b29a5..1ba245a45d 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -6,9 +6,11 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit val do_generate_principle : - bool -> + (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit + +val do_generate_principle_interactive : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - Proof_global.t option + Proof_global.t val functional_induction : bool -> diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5a682e7231..e2321d233c 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1395,12 +1395,10 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type ) tclIDTAC) g end) pstate in - try - Some (fst @@ by (Proofview.V82.tactic tclIDTAC) pstate) (* raises UserError _ if the proof is complete *) - with UserError _ -> - (defined pstate; None) + if Proof_global.get_open_goals pstate = 0 then (defined pstate; None) else Some pstate let com_terminate + interactive_proof tcc_lemma_name tcc_lemma_ref is_mes @@ -1430,8 +1428,8 @@ let com_terminate with EmptySubgoals -> (* a non recursive function declared with measure ! *) tcc_lemma_ref := Not_needed; - defined pstate; - None + if interactive_proof then Some pstate + else (defined pstate; None) let start_equation (f:GlobRef.t) (term_f:GlobRef.t) (cont_tactic:Id.t list -> tactic) g = @@ -1494,7 +1492,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation (* Pp.msgnl (fun _ _ -> str "eqn finished"); *) -let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq +let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : Proof_global.t option = let open Term in let open Constr in @@ -1585,6 +1583,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num (* XXX STATE Why do we need this... why is the toplevel protection not enough *) funind_purify (fun () -> let pstate = com_terminate + interactive_proof tcc_lemma_name tcc_lemma_constr is_mes functional_ref diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index 90f9c449b1..b92ac3a0ec 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -5,13 +5,19 @@ val tclUSER_if_not_mes : bool -> Names.Id.t list option -> Tacmach.tactic + val recursive_definition : -bool -> - Names.Id.t -> - Constrintern.internalization_env -> - Constrexpr.constr_expr -> - Constrexpr.constr_expr -> - int -> Constrexpr.constr_expr -> (pconstant -> - Indfun_common.tcc_lemma_value ref -> - pconstant -> - pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option + interactive_proof:bool -> + is_mes:bool -> + Names.Id.t -> + Constrintern.internalization_env -> + Constrexpr.constr_expr -> + Constrexpr.constr_expr -> + int -> + Constrexpr.constr_expr -> + (pconstant -> + Indfun_common.tcc_lemma_value ref -> + pconstant -> + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> + Constrexpr.constr_expr list -> + Proof_global.t option -- cgit v1.2.3 From 2ebd73901edb94030aa804572cbe86d486ca6732 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 17:50:44 +0200 Subject: [rewrite] Add Morphism syntax made different for module type parameters --- plugins/ltac/g_rewrite.mlg | 12 ++++++--- plugins/ltac/rewrite.ml | 62 ++++++++++++++++++++++++---------------------- plugins/ltac/rewrite.mli | 3 ++- 3 files changed, 43 insertions(+), 34 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index bb29323858..1a84158df7 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -276,10 +276,14 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF { add_setoid atts binders a aeq t n } - | #[ atts = rewrite_attributes; ] ![ maybe_open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] - (* This command may or may not open a goal *) - => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater } - -> { add_morphism_infer atts m n } + | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] + => { VtStartProof(GuaranteesOpacity, [n]), VtLater } + -> { if Lib.is_modtype () then + CErrors.user_err Pp.(str "Add Morphism cannot be used in a module type. Use Parameter Morphism instead."); + add_morphism_interactive atts m n } + | #[ atts = rewrite_attributes; ] [ "Declare" "Morphism" constr(m) ":" ident(n) ] + => { VtSideff([n]), VtLater } + -> { add_morphism_as_parameter atts m n } | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { add_morphism atts [] m s n } diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 26d477fee0..c568f63903 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1973,42 +1973,46 @@ let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id")) -let add_morphism_infer atts m n : Proof_global.t option = +let add_morphism_as_parameter atts m n : unit = + init_setoid (); + let instance_id = add_suffix n "_Proper" in + let env = Global.env () in + let evd = Evd.from_env env in + let uctx, instance = build_morphism_signature env evd m in + let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id + (Entries.ParameterEntry + (None,(instance,uctx),None), + Decl_kinds.IsAssumption Decl_kinds.Logical) + in + Classes.add_instance (Classes.mk_instance + (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); + declare_projection n instance_id (ConstRef cst) + +let add_morphism_interactive atts m n : Proof_global.t = warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); let instance_id = add_suffix n "_Proper" in let env = Global.env () in let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in - if Lib.is_modtype () then - let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id - (Entries.ParameterEntry - (None,(instance,uctx),None), - Decl_kinds.IsAssumption Decl_kinds.Logical) - in + let kind = Decl_kinds.Global, atts.polymorphic, + Decl_kinds.DefinitionBody Decl_kinds.Instance + in + let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in + let hook _ _ _ = function + | Globnames.ConstRef cst -> Classes.add_instance (Classes.mk_instance - (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); - declare_projection n instance_id (ConstRef cst); - None - else - let kind = Decl_kinds.Global, atts.polymorphic, - Decl_kinds.DefinitionBody Decl_kinds.Instance - in - let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in - let hook _ _ _ = function - | Globnames.ConstRef cst -> - Classes.add_instance (Classes.mk_instance - (PropGlobal.proper_class env evd) Hints.empty_hint_info - atts.global (ConstRef cst)); - declare_projection n instance_id (ConstRef cst) - | _ -> assert false - in - let hook = Lemmas.mk_hook hook in - Flags.silently - (fun () -> - let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in - Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) () + (PropGlobal.proper_class env evd) Hints.empty_hint_info + atts.global (ConstRef cst)); + declare_projection n instance_id (ConstRef cst) + | _ -> assert false + in + let hook = Lemmas.mk_hook hook in + Flags.silently + (fun () -> + let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in + fst Pfedit.(by (Tacinterp.interp tac) pstate)) () let add_morphism atts binders m s n = init_setoid (); diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 5aabb946d5..3ef33c6dc9 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -101,7 +101,8 @@ val add_setoid -> Id.t -> unit -val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option +val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t +val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit val add_morphism : rewrite_attributes -- cgit v1.2.3 From a7a6fa3219134004f1fc6c757f1c16281724f38f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 24 May 2019 14:57:33 +0200 Subject: [vernac] more precise types for Add Morph, Instance, and Function --- plugins/funind/indfun.ml | 4 ++-- plugins/ltac/rewrite.ml | 12 ++++++------ 2 files changed, 8 insertions(+), 8 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index bb6db1f5cf..241da053b7 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -434,7 +434,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in None, evd,List.rev rev_pconstants | _ -> - let pstate = ComFixpoint.do_fixpoint Global false fixpoint_exprl in + ComFixpoint.do_fixpoint Global false fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> @@ -448,7 +448,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp (Evd.from_env (Global.env ()),[]) fixpoint_exprl in - pstate,evd,List.rev rev_pconstants + None,evd,List.rev rev_pconstants let generate_correction_proof_wf f_ref tcc_lemma_ref diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c568f63903..caeedadbf4 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1796,11 +1796,11 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance atts binders (name,t) fields = let program_mode = atts.program in - let _id, proof = Classes.new_instance ~program_mode atts.polymorphic - name binders t (Some (true, CAst.make @@ CRecord (fields))) + let _id = Classes.new_instance ~program_mode atts.polymorphic + name binders t (true, CAst.make @@ CRecord (fields)) ~global:atts.global ~generalize:false Hints.empty_hint_info in - assert (Option.is_empty proof) (* refine:false with term *) + () let declare_instance_refl atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" @@ -2024,12 +2024,12 @@ let add_morphism atts binders m s n = [cHole; s; m]) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - let _, pstate = Classes.new_instance + let _id, pstate = Classes.new_instance_interactive ~program_mode:atts.program ~global:atts.global atts.polymorphic - instance_name binders instance_t None + instance_name binders instance_t ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in - Option.get pstate (* no instance body -> always open proof *) + pstate (* no instance body -> always open proof *) (** Bind to "rewrite" too *) -- cgit v1.2.3 From 06df92fffc05d501fefdcf949625a33bd52f1980 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 27 May 2019 15:53:50 +0200 Subject: [classes] remove program mode from the new_instance_* APIs --- plugins/ltac/rewrite.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index caeedadbf4..792cd5f9ef 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1795,8 +1795,7 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance atts binders (name,t) fields = - let program_mode = atts.program in - let _id = Classes.new_instance ~program_mode atts.polymorphic + let _id = Classes.new_instance atts.polymorphic name binders t (true, CAst.make @@ CRecord (fields)) ~global:atts.global ~generalize:false Hints.empty_hint_info in @@ -2025,7 +2024,7 @@ let add_morphism atts binders m s n = in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in let _id, pstate = Classes.new_instance_interactive - ~program_mode:atts.program ~global:atts.global atts.polymorphic + ~global:atts.global atts.polymorphic instance_name binders instance_t ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in -- cgit v1.2.3 From cfbfce0639a4e608210b21227f923a4f27ab6752 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 27 May 2019 17:11:53 +0200 Subject: [rewrite] remove program_mode from attributes (unused) --- plugins/ltac/rewrite.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 792cd5f9ef..7b286e69dc 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -42,13 +42,13 @@ module NamedDecl = Context.Named.Declaration (** Typeclass-based generalized rewriting. *) -type rewrite_attributes = { polymorphic : bool; program : bool; global : bool } +type rewrite_attributes = { polymorphic : bool; global : bool } let rewrite_attributes = let open Attributes.Notations in Attributes.(polymorphic ++ program ++ locality) >>= fun ((polymorphic, program), locality) -> let global = not (Locality.make_section_locality locality) in - Attributes.Notations.return { polymorphic; program; global } + Attributes.Notations.return { polymorphic; global } (** Constants used by the tactic. *) -- cgit v1.2.3