diff options
Diffstat (limited to 'plugins')
65 files changed, 715 insertions, 592 deletions
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/g_derive.mlg b/plugins/derive/g_derive.mlg index 214a9d8bb5..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 } -| ![ proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - { fun ~pstate -> Some Derive.(start_deriving f suchthat 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/CHANGES b/plugins/extraction/CHANGES index 4bc3dba36e..bc7e1448f7 100644 --- a/plugins/extraction/CHANGES +++ b/plugins/extraction/CHANGES @@ -200,7 +200,7 @@ For the moment there are: Wf.well_founded_induction Wf.well_founded_induction_type Those constants does not match the auto-inlining criterion based on strictness. -Of course, you can still overide this behaviour via some Extraction NoInline. +Of course, you can still override this behaviour via some Extraction NoInline. * There is now a web page showing the extraction of all standard theories: http://www.lri.fr/~letouzey/extraction diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v index 36bb1148b6..02da168fd0 100644 --- a/plugins/extraction/ExtrOcamlBasic.v +++ b/plugins/extraction/ExtrOcamlBasic.v @@ -26,9 +26,9 @@ Extract Inductive prod => "( * )" [ "" ]. Extract Inductive sumbool => bool [ true false ]. Extract Inductive sumor => option [ Some None ]. -(** Restore lazyness of andb, orb. +(** Restore laziness of andb, orb. NB: without these Extract Constant, andb/orb would be inlined - by extraction in order to have lazyness, producing inelegant + by extraction in order to have laziness, producing inelegant (if ... then ... else false) and (if ... then true else ...). *) diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 59c57cc544..f46d09e335 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -573,7 +573,7 @@ let pp_ocaml_gen k mp rls olab = if is_mp_bound base then pp_ocaml_bound base rls else pp_ocaml_extern k base rls -(* For Haskell, things are simplier: we have removed (almost) all structures *) +(* For Haskell, things are simpler: we have removed (almost) all structures *) let pp_haskell_gen k mp rls = match rls with | [] -> assert false @@ -590,7 +590,7 @@ let pp_global k r = let s = List.hd ls in let mp,l = repr_of_r r in if ModPath.equal mp (top_visible_mp ()) then - (* simpliest situation: definition of r (or use in the same context) *) + (* simplest situation: definition of r (or use in the same context) *) (* we update the visible environment *) (add_visible (k,s) l; unquote s) else @@ -607,7 +607,7 @@ let pp_module mp = let ls = mp_renaming mp in match mp with | MPdot (mp0,l) when ModPath.equal mp0 (top_visible_mp ()) -> - (* simpliest situation: definition of mp (or use in the same context) *) + (* simplest situation: definition of mp (or use in the same context) *) (* we update the visible environment *) let s = List.hd ls in add_visible (Mod,s) l; s 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..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.t option -> unit +val show_extraction : pstate:Proof_global.t -> unit diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 9db7c8d8d3..051d1f8e0f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -115,7 +115,7 @@ let get_body lconstr = EConstr.of_constr (Mod_subst.force_constr lconstr) let get_opaque env c = EConstr.of_constr - (Opaqueproof.force_proof (Environ.opaque_tables env) c) + (Opaqueproof.force_proof Library.indirect_accessor (Environ.opaque_tables env) c) let applistc c args = EConstr.mkApp (c, Array.of_list args) diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index d7bb27f121..9ea3fbeaf4 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -93,7 +93,7 @@ VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY END VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY -(* Same, with content splitted in several files *) +(* Same, with content split in several files *) | [ "Separate" "Extraction" ne_global_list(l) ] -> { separate_extraction l } END @@ -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 ] [ "Show" "Extraction" ] - -> { fun ~pstate -> let () = show_extraction ~pstate in pstate } +VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY STATE proof_query +| [ "Show" "Extraction" ] + -> { show_extraction } END diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 4e229a94b6..c2c48f9565 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -101,7 +101,7 @@ let labels_of_ref r = (*S The main tables: constants, inductives, records, ... *) -(* Theses tables are not registered within coq save/undo mechanism +(* These tables are not registered within coq save/undo mechanism since we reset their contents at each run of Extraction *) (* We use [constant_body] (resp. [mutual_inductive_body]) as checksum @@ -842,7 +842,7 @@ let in_customs : GlobRef.t * string list * string -> obj = ~subst:(Some (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))) let in_custom_matchs : GlobRef.t * string -> obj = - declare_object @@ superglobal_object_nodischarge "ML extractions custom matchs" + declare_object @@ superglobal_object_nodischarge "ML extractions custom matches" ~cache:(fun (_,(r,s)) -> add_custom_match r s) ~subst:(Some (fun (subs,(r,s)) -> (fst (subst_global subs r), s))) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 287a374ab1..e38ea992ab 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -658,7 +658,7 @@ let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = *) (fun g -> -(* observe (str "Instanciation: removing hyp " ++ Ppconstr.pr_id hid); *) +(* observe (str "Instantiation: removing hyp " ++ Ppconstr.pr_id hid); *) thin [hid] g ) ) @@ -951,7 +951,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *) let f_def = Global.lookup_constant (fst (destConst evd f)) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in - let (f_body, _) = Option.get (Global.body_of_constant_body f_def) in + let (f_body, _) = Option.get (Global.body_of_constant_body Library.indirect_accessor f_def) in let f_body = EConstr.of_constr f_body in let params,f_body_with_params = decompose_lam_n evd nb_params f_body in let (_,num),(_,_,bodies) = destFix evd f_body_with_params in @@ -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 -> @@ -1082,7 +1083,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam } in let get_body const = - match Global.body_of_constant const with + match Global.body_of_constant Library.indirect_accessor const with | Some (body, _) -> let env = Global.env () in let sigma = Evd.from_env env in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index e9a2c285d0..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 @@ -413,7 +412,7 @@ let get_funs_constant mp = in function const -> let find_constant_body const = - match Global.body_of_constant const with + match Global.body_of_constant Library.indirect_accessor const with | Some (body, _) -> let body = Tacred.cbv_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) @@ -429,11 +428,11 @@ let get_funs_constant mp = let l_const = get_funs_constant const f in (* We need to check that all the functions found are in the same block - to prevent Reset stange thing + to prevent Reset strange thing *) let l_bodies = List.map find_constant_body (Array.to_list (Array.map fst l_const)) in let l_params,l_fixes = List.split (List.map decompose_lam l_bodies) in - (* all the paremeter must be equal*) + (* all the parameters must be equal*) let _check_params = let first_params = List.hd l_params in List.iter @@ -514,13 +513,13 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ ) fas in - (* We create the first priciple by tactic *) + (* We create the first principle by tactic *) let first_type,other_princ_types = match l_schemes with 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..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 -| ![ 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 - | _,((_,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) } +VERNAC COMMAND EXTEND Function STATE CUSTOM +| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] + => { 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 { @@ -225,33 +242,32 @@ let warning_error names e = } VERNAC COMMAND EXTEND NewFunctionalScheme -| ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] +| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } -> - { fun ~pstate -> - begin + { begin try - Functional_principles_types.build_scheme fas; pstate + Functional_principles_types.build_scheme fas 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 + 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; pstate + warning_error names e end } END @@ -265,6 +281,6 @@ END (***** debug only ***) VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY -| ![ proof ] ["Generate" "graph" "for" reference(c)] -> +| ["Generate" "graph" "for" reference(c)] -> { make_graph (Smartlocate.global_with_alias c) } END diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index e15e167ff3..201d953692 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1299,10 +1299,10 @@ let rec rebuild_return_type rt = | Constrexpr.CProdN(n,t') -> CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t') | Constrexpr.CLetIn(na,v,t,t') -> - CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') + CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous], Constrexpr.Default Decl_kinds.Explicit, rt)], - CAst.make @@ Constrexpr.CSort(GType [])) + CAst.make @@ Constrexpr.CSort(UAnonymous {rigid=true})) let do_build_inductive evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) @@ -1369,7 +1369,7 @@ let do_build_inductive (rebuild_return_type returned_types.(i)) in (* We need to lift back our work topconstr but only with all information - We mimick a Set Printing All. + We mimic a Set Printing All. Then save the graphs and reset Printing options to their primitive values *) let rel_arities = Array.mapi rel_arity funsargs in @@ -1438,7 +1438,7 @@ let do_build_inductive (rebuild_return_type returned_types.(i)) in (* We need to lift back our work topconstr but only with all information - We mimick a Set Printing All. + We mimic a Set Printing All. Then save the graphs and reset Printing options to their primitive values *) let rel_arities = Array.mapi rel_arity funsargs in diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 481a8be3ba..24b3690138 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -55,7 +55,7 @@ val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr Glob_term.cases_pattern * Id.Map.key list * Id.t Id.Map.t -(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt +(* [alpha_rt avoid rt] alpha convert [rt] s.t. the result respects barendregt conventions and does not share bound variables with avoid *) val alpha_rt : Id.t list -> glob_constr -> glob_constr diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index ce7d149ae1..241da053b7 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 + 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 ~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 generate_correction_proof_wf f_ref tcc_lemma_ref @@ -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 ~pstate 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,8 +660,8 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive 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 - else pstate, 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 = match recompute_binder_list [fixpoint_expr] with @@ -684,8 +684,8 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive 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 - else pstate, 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) -> 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,9 @@ 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 (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 -> @@ -851,7 +851,7 @@ let make_graph ~pstate (f_ref : GlobRef.t) = end | _ -> raise (UserError (None, str "Not a function reference") ) in - (match Global.body_of_constant_body c_body with + (match Global.body_of_constant_body Library.indirect_accessor c_body with | None -> error "Cannot build a graph over an axiom!" | Some (body, _) -> let env = Global.env () in @@ -902,11 +902,27 @@ 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_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; - pstate) - -let do_generate_principle = do_generate_principle [] warning_error true + expr_list) + +(* *************** 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 acf85f539e..1ba245a45d 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -5,10 +5,12 @@ 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 -> - bool -> +val do_generate_principle : + (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 -> @@ -17,4 +19,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 : GlobRef.t -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 40f66ce5eb..48cf040919 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -115,7 +115,7 @@ let eq = lazy(EConstr.of_constr (coq_constant "eq")) let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) (*****************************************************************) -(* Copy of the standart save mechanism but without the much too *) +(* Copy of the standard save mechanism but without the much too *) (* slow reduction function *) (*****************************************************************) open Entries @@ -357,7 +357,7 @@ let add_Function is_general f = let pr_table env sigma = pr_table env sigma !from_function (*********************************) -(* Debuging *) +(* Debugging *) let functional_induction_rewrite_dependent_proofs = ref true let function_debug = ref false open Goptions diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index edb698280f..03568fc6c7 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -591,7 +591,7 @@ let rec reflexivity_with_destruct_cases g = (* [prove_fun_complete funs graphs schemes lemmas_types_infos i] - is the tactic used to prove completness lemma. + is the tactic used to prove completeness lemma. [funcs], [graphs] [schemes] [lemmas_types_infos] are the mutually recursive functions (resp. definitions of the graphs of the functions, principles and correctness lemma types) to prove correct. @@ -748,7 +748,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let funs = Array.of_list funs and graphs = Array.of_list graphs in let map (c, u) = mkConstU (c, EInstance.make u) in let funs_constr = Array.map map funs in - (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + (* XXX STATE Why do we need this... why is the toplevel protection not enough *) funind_purify (fun () -> let env = Global.env () in @@ -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 @@ -928,7 +928,7 @@ let revert_graph kn post_tac hid g = [hid] is the hypothesis to invert, [fconst] is the function to invert and [f_correct] is the correctness lemma for [fconst]. - The sketch is the follwing~: + The sketch is the following~: \begin{enumerate} \item Transforms the hypothesis [hid] such that its type is now $res\ =\ f\ t_1 \ldots t_n$ (fails if it is not possible) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 1fca132655..e2321d233c 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 @@ -1396,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 + 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 @@ -1413,7 +1410,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 +1428,8 @@ let com_terminate with EmptySubgoals -> (* a non recursive function declared with measure ! *) tcc_lemma_ref := Not_needed; - defined pstate + 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 = @@ -1459,7 +1457,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,14 +1487,12 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation } ) )) pstate in - (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *) -(* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *) - 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 +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 @@ -1584,9 +1580,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num spc () ++ str"is defined" ) ) in - (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + (* 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 a006c2c354..b92ac3a0ec 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -5,15 +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 - +val recursive_definition : + 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 diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index f5098d2a34..0ded60d9c7 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -146,6 +146,23 @@ let discrHyp id = let injection_main with_evars c = elimOnConstrWithHoles (injClause None None) with_evars c +let isInjPat pat = match pat.CAst.v with IntroAction (IntroInjection _) -> Some pat.CAst.loc | _ -> None + +let decode_inj_ipat ?loc = function + (* For the "as [= pat1 ... patn ]" syntax *) + | [{ CAst.v = IntroAction (IntroInjection ipat) }] -> ipat + (* For the "as pat1 ... patn" syntax *) + | ([] | [_]) as ipat -> ipat + | pat1::pat2::_ as ipat -> + (* To be sure that there is no confusion of syntax, we check that no [= ...] occurs + in the non-singleton list of patterns *) + match isInjPat pat1 with + | Some _ -> user_err ?loc:pat2.CAst.loc (str "Unexpected pattern.") + | None -> + match List.map_filter isInjPat ipat with + | loc :: _ -> user_err ?loc (str "Unexpected injection pattern.") + | [] -> ipat + } TACTIC EXTEND injection @@ -158,15 +175,15 @@ TACTIC EXTEND einjection END TACTIC EXTEND injection_as | [ "injection" "as" intropattern_list(ipat)] -> - { injClause None (Some ipat) false None } + { injClause None (Some (decode_inj_ipat ipat)) false None } | [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] -> - { mytclWithHoles (injClause None (Some ipat)) false c } + { mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) false c } END TACTIC EXTEND einjection_as | [ "einjection" "as" intropattern_list(ipat)] -> - { injClause None (Some ipat) true None } + { injClause None (Some (decode_inj_ipat ipat)) true None } | [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> - { mytclWithHoles (injClause None (Some ipat)) true c } + { mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) true c } END TACTIC EXTEND simple_injection | [ "simple" "injection" ] -> { simpleInjClause None false None } @@ -914,10 +931,10 @@ 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 -> 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. *) @@ -946,10 +963,10 @@ 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 -> 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, @@ -1101,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 -> 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..960e5b76f8 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 @@ -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 - 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) ] => +| [ "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 @@ -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 de3a9c9fa9..58c8dabd79 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 (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 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) ] -> +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 } -| ![ proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> +| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> { obligation (num, Some name, None) tac } -| ![ proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> +| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> { obligation (num, None, Some t) tac } -| ![ proof ] [ "Obligation" integer(num) withtac(tac) ] -> +| [ "Obligation" integer(num) withtac(tac) ] -> { obligation (num, None, None) tac } -| ![ proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> +| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> { next_obligation (Some name) tac } -| ![ 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 diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 12b12bc7b0..1a84158df7 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,65 +234,63 @@ 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) ] - (* 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; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(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 - } - | #[ 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 @@ -310,12 +308,6 @@ TACTIC EXTEND setoid_transitivity END VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY -| ![ proof ] [ "Print" "Rewrite" "HintDb" preident(s) ] -> - { (* This command should not use the proof env, keeping previous - behavior as requested in review. *) - fun ~pstate -> - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in - Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s); - pstate } +| [ "Print" "Rewrite" "HintDb" preident(s) ] -> + { Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) } END diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 963b7189f9..7b286e69dc 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -23,14 +23,12 @@ open Tacticals.New open Tactics open Pretype_errors open Typeclasses -open Classes open Constrexpr open Globnames open Evd open Tactypes open Locus open Locusops -open Decl_kinds open Elimschemes open Environ open Termops @@ -44,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. *) @@ -207,7 +205,7 @@ end) = struct let mk_relation env evd a = app_poly env evd relation [| a |] - (** Build an infered signature from constraints on the arguments and expected output + (** Build an inferred signature from constraints on the arguments and expected output relation *) let build_signature evars env m (cstrs : (types * types option) option list) @@ -1791,20 +1789,21 @@ let rec strategy_of_ast = function let mkappc s l = CAst.make @@ CAppExpl ((None,qualid_of_ident (Id.of_string s),None),l) let declare_an_instance n s args = - (((CAst.make @@ Name n),None), Explicit, + (((CAst.make @@ Name n),None), CAst.make @@ CAppExpl ((None, qualid_of_string s,None), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] -let anew_instance ~pstate atts binders instance fields = - let program_mode = atts.program in - new_instance ~pstate ~program_mode atts.polymorphic - binders instance (Some (true, CAst.make @@ CRecord (fields))) - ~global:atts.global ~generalize:false Hints.empty_hint_info +let anew_instance atts binders (name,t) fields = + 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 + () -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 = @@ -1817,44 +1816,44 @@ 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 - | (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) -> () + | (Some lemma1, None, None) -> + declare_instance_refl atts binders a aeq n lemma1 + | (None, Some lemma2, None) -> + declare_instance_sym atts binders a aeq n lemma2 + | (None, None, Some lemma3) -> + declare_instance_trans atts binders a aeq n lemma3 + | (Some lemma1, Some lemma2, None) -> + 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 () = 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 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 () = 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 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 () = 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 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) @@ -1950,18 +1949,18 @@ 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 _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 () = 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 - 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 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 = @@ -1973,58 +1972,63 @@ 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_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 (); - (* 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 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 - 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 - 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 -> - 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 ~ontop:pstate ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in - Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) () + 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 + 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 = - (((CAst.make @@ Name instance_id),None), Explicit, - CAst.make @@ CAppExpl ( - (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), - [cHole; s; m])) + let instance_name = (CAst.make @@ Name instance_id),None in + let instance_t = + CAst.make @@ CAppExpl + ((None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), + [cHole; s; m]) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - let _, pstate = new_instance ~pstate ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance - None - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in - pstate + let _id, pstate = Classes.new_instance_interactive + ~global:atts.global atts.polymorphic + instance_name binders instance_t + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info + in + pstate (* no instance body -> always open proof *) (** Bind to "rewrite" too *) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index a200cb5ced..3ef33c6dc9 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -81,18 +81,36 @@ 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 add_morphism_infer : pstate:Proof_global.t option -> rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t 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 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_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 + -> local_binder_expr list + -> constr_expr + -> constr_expr + -> Id.t + -> Proof_global.t val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 0eb7726a18..8bd69dd4fd 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) | Select (* returns all successes of the first matching branch *) - | Once (* returns the first success in a maching branch + | Once (* returns the first success in a matching branch (not necessarily the first) *) type global_flag = (* [gfail] or [fail] *) | TacGlobal diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index fd303f5d94..f839c3e886 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -24,7 +24,7 @@ type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) | Select (* returns all successes of the first matching branch *) - | Once (* returns the first success in a maching branch + | Once (* returns the first success in a matching branch (not necessarily the first) *) type global_flag = (* [gfail] or [fail] *) | TacGlobal diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 800be2565d..4a0b01bcdc 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -855,7 +855,7 @@ let interp_binding_name ist env sigma = function | NamedHyp id -> (* If a name is bound, it has to be a quantified hypothesis *) (* user has to use other names for variables if these ones clash with *) - (* a name intented to be used as a (non-variable) identifier *) + (* a name intended to be used as a (non-variable) identifier *) try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id @@ -2075,7 +2075,7 @@ let _ = let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in let ist = { lfun; poly; extra; } in let tac = interp_tactic ist tac in - (* EJGA: We sould also pass the proof name if desired, for now + (* EJGA: We should also pass the proof name if desired, for now poly seems like enough to get reasonable behavior in practice *) let name, poly = Id.of_string "ltac_gen", poly in diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 2b5e496168..7783661787 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -128,7 +128,7 @@ module PatternMatching (E:StaticEnvironment) = struct (** To focus on the algorithmic portion of pattern-matching, the bookkeeping is relegated to a monad: the composition of the - bactracking monad of {!IStream.t} with a "writer" effect. *) + backtracking monad of {!IStream.t} with a "writer" effect. *) (* spiwack: as we don't benefit from the various stream optimisations of Haskell, it may be costly to give the monad in direct style such as here. We may want to use some continuation passing style. *) diff --git a/plugins/micromega/DeclConstant.v b/plugins/micromega/DeclConstant.v index 47fcac6481..4e8fe5a8ff 100644 --- a/plugins/micromega/DeclConstant.v +++ b/plugins/micromega/DeclConstant.v @@ -62,6 +62,7 @@ Instance DZO: DeclaredConstant Z0 := {}. Instance DZpos: DeclaredConstant Zpos := {}. Instance DZneg: DeclaredConstant Zneg := {}. Instance DZpow_pos : DeclaredConstant Z.pow_pos := {}. +Instance DZpow : DeclaredConstant Z.pow := {}. Require Import QArith. diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index 36ed0210e3..b20f45af3e 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -925,7 +925,7 @@ Qed. revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. - discriminate. - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. - * injection H as <-. rewrite <- PSubstL1_ok; intuition. + * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition. * now apply IH. Qed. diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 6112eda200..830cbdf7f6 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -55,7 +55,7 @@ Extract Constant Rinv => "fun x -> 1 / x". extraction is only performed as a test in the test suite. *) (*Extraction "micromega.ml" Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula - ZMicromega.cnfZ ZMicromega.bound_problem_fr QMicromega.cnfQ + ZMicromega.cnfZ ZMicromega.Zeval_const ZMicromega.bound_problem_fr QMicromega.cnfQ List.map simpl_cone (*map_cone indexes*) denorm Qpower vm_add normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. diff --git a/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v index e0e2232be5..7759bda7c7 100644 --- a/plugins/micromega/OrderedRing.v +++ b/plugins/micromega/OrderedRing.v @@ -129,7 +129,7 @@ Proof. intros n m H1 H2; rewrite H2 in H1; now apply H1. Qed. -(* Propeties of plus, minus and opp *) +(* Properties of plus, minus and opp *) Theorem Rplus_0_l : forall n : R, 0 + n == n. Proof. diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 60931df517..c5e179fbb8 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -990,7 +990,7 @@ Proof. rewrite IHs. reflexivity. Qed. -(** equality migth be (too) strong *) +(** equality might be (too) strong *) Lemma eval_formulaSC : forall env f, eval_sformula env f = eval_formula env (map_Formula f). Proof. destruct f. diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index ab218a1778..953690c510 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -75,6 +75,21 @@ Fixpoint Zeval_expr (env : PolEnv Z) (e: PExpr Z) : Z := Definition eval_expr := eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x => x) (fun x => x) (pow_N 1 Z.mul). +Fixpoint Zeval_const (e: PExpr Z) : option Z := + match e with + | PEc c => Some c + | PEX _ x => None + | PEadd e1 e2 => map_option2 (fun x y => Some (x + y)) + (Zeval_const e1) (Zeval_const e2) + | PEmul e1 e2 => map_option2 (fun x y => Some (x * y)) + (Zeval_const e1) (Zeval_const e2) + | PEpow e1 n => map_option (fun x => Some (Z.pow x (Z.of_N n))) + (Zeval_const e1) + | PEsub e1 e2 => map_option2 (fun x y => Some (x - y)) + (Zeval_const e1) (Zeval_const e2) + | PEopp e => map_option (fun x => Some (Z.opp x)) (Zeval_const e) + end. + Lemma ZNpower : forall r n, r ^ Z.of_N n = pow_N 1 Z.mul r n. Proof. destruct n. diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index de9dec0f74..48027442b2 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -346,7 +346,9 @@ struct let coq_PsatzC = lazy (constant "PsatzC") let coq_PsatzZ = lazy (constant "PsatzZ") - let coq_GT = lazy (m_constant "GT") + (* let coq_GT = lazy (m_constant "GT")*) + + let coq_DeclaredConstant = lazy (m_constant "DeclaredConstant") let coq_TT = lazy (gen_constant_in_modules "ZMicromega" @@ -462,13 +464,24 @@ struct what to consider as a constant (see [parse_constant]) *) - let is_ground_term env sigma term = - let typ = Retyping.get_type_of env sigma term in - try - ignore (Typeclasses.resolve_one_typeclass env sigma (EConstr.mkApp(Lazy.force coq_GT,[| typ;term|]))) ; - true - with - | Not_found -> false + let is_declared_term env evd t = + match EConstr.kind evd t with + | Const _ | Construct _ -> (* Restrict typeclass resolution to trivial cases *) + begin + let typ = Retyping.get_type_of env evd t in + try + ignore (Typeclasses.resolve_one_typeclass env evd (EConstr.mkApp(Lazy.force coq_DeclaredConstant,[| typ;t|]))) ; true + with Not_found -> false + end + | _ -> false + + let rec is_ground_term env evd term = + match EConstr.kind evd term with + | App(c,args) -> + is_declared_term env evd c && + Array.for_all (is_ground_term env evd) args + | Const _ | Construct _ -> is_declared_term env evd term + | _ -> false let parse_z sigma term = @@ -674,26 +687,28 @@ struct let parse_zop gl (op,args) = let sigma = gl.sigma in - match EConstr.kind sigma op with - | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1)) - | Ind((n,0),_) -> - if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_Z) - then (Mc.OpEq, args.(1), args.(2)) - else raise ParseError - | _ -> failwith "parse_zop" + match args with + | [| a1 ; a2|] -> assoc_const sigma op zop_table, a1, a2 + | [| ty ; a1 ; a2|] -> + if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl ty (Lazy.force coq_Z) + then (Mc.OpEq, args.(1), args.(2)) + else raise ParseError + | _ -> raise ParseError let parse_rop gl (op,args) = let sigma = gl.sigma in - match EConstr.kind sigma op with - | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1)) - | Ind((n,0),_) -> - if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_R) - then (Mc.OpEq, args.(1), args.(2)) - else raise ParseError - | _ -> failwith "parse_zop" + match args with + | [| a1 ; a2|] -> assoc_const sigma op rop_table, a1 , a2 + | [| ty ; a1 ; a2|] -> + if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl ty (Lazy.force coq_R) + then (Mc.OpEq, a1, a2) + else raise ParseError + | _ -> raise ParseError let parse_qop gl (op,args) = - (assoc_const gl.sigma op qop_table, args.(0) , args.(1)) + if Array.length args = 2 + then (assoc_const gl.sigma op qop_table, args.(0) , args.(1)) + else raise ParseError type 'a op = | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr) @@ -804,7 +819,7 @@ struct (op expr1 expr2,env) in try (Mc.PEc (parse_constant gl term) , env) - with ParseError -> + with ParseError -> match EConstr.kind gl.sigma term with | App(t,args) -> ( @@ -820,7 +835,7 @@ struct let (expr,env) = parse_expr env args.(0) in let power = (parse_exp expr args.(1)) in (power , env) - with e when CErrors.noncritical e -> + with ParseError -> (* if the exponent is a variable *) let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env) end @@ -858,19 +873,48 @@ struct coq_Ropp , Opp ; coq_Rpower , Power] - (** [parse_constant parse gl t] returns the reification of term [t]. + let parse_constant parse gl t = parse gl.sigma t + + (** [parse_more_constant parse gl t] returns the reification of term [t]. If [t] is a ground term, then it is first reduced to normal form before using a 'syntactic' parser *) - let parse_constant parse gl t = - if is_ground_term gl.env gl.sigma t - then - parse gl.sigma (Redexpr.cbv_vm gl.env gl.sigma t) - else raise ParseError + let parse_more_constant parse gl t = + try + parse gl t + with ParseError -> + begin + if debug then Feedback.msg_debug Pp.(str "try harder"); + if is_ground_term gl.env gl.sigma t + then parse gl (Redexpr.cbv_vm gl.env gl.sigma t) + else raise ParseError + end let zconstant = parse_constant parse_z let qconstant = parse_constant parse_q let nconstant = parse_constant parse_nat + (** [parse_more_zexpr parse_constant gl] improves the parsing of exponent + which can be arithmetic expressions (without variables). + [parse_constant_expr] returns a constant if the argument is an expression without variables. *) + + let rec parse_zexpr gl = + parse_expr gl + zconstant + (fun expr (x:EConstr.t) -> + let z = parse_zconstant gl x in + match z with + | Mc.Zneg _ -> Mc.PEc Mc.Z0 + | _ -> Mc.PEpow(expr, Mc.Z.to_N z) + ) + zop_spec + and parse_zconstant gl e = + let (e,_) = parse_zexpr gl (Env.empty gl) e in + match Mc.zeval_const e with + | None -> raise ParseError + | Some z -> z + + + (* NB: R is a different story. Because it is axiomatised, reducing would not be effective. Therefore, there is a specific parser for constant over R @@ -905,7 +949,7 @@ struct let b = rconstant args.(1) in f a b with - ParseError -> + ParseError -> match op with | op when EConstr.eq_constr sigma op (Lazy.force coq_Rinv) -> let arg = rconstant args.(0) in @@ -913,12 +957,12 @@ struct then raise ParseError (* This is a division by zero -- no semantics *) else Mc.CInv(arg) | op when EConstr.eq_constr sigma op (Lazy.force coq_Rpower) -> - Mc.CPow(rconstant args.(0) , Mc.Inr (nconstant gl args.(1))) + Mc.CPow(rconstant args.(0) , Mc.Inr (parse_more_constant nconstant gl args.(1))) | op when EConstr.eq_constr sigma op (Lazy.force coq_IQR) -> Mc.CQ (qconstant gl args.(0)) | op when EConstr.eq_constr sigma op (Lazy.force coq_IZR) -> - Mc.CZ (zconstant gl args.(0)) - | _ -> raise ParseError + Mc.CZ (parse_more_constant zconstant gl args.(0)) + | _ -> raise ParseError end | _ -> raise ParseError in @@ -934,14 +978,6 @@ struct res - let parse_zexpr gl = parse_expr gl - zconstant - (fun expr x -> - let exp = (zconstant gl x) in - match exp with - | Mc.Zneg _ -> Mc.PEc Mc.Z0 - | _ -> Mc.PEpow(expr, Mc.Z.to_N exp)) - zop_spec let parse_qexpr gl = parse_expr gl qconstant @@ -952,7 +988,7 @@ struct begin match expr with | Mc.PEc q -> Mc.PEc (Mc.qpower q exp) - | _ -> print_string "parse_qexpr parse error" ; flush stdout ; raise ParseError + | _ -> raise ParseError end | _ -> let exp = Mc.Z.to_N exp in Mc.PEpow(expr,exp)) @@ -1031,14 +1067,16 @@ struct let g,env,tg = xparse_formula env tg b in mkformula_binary mkIff term f g,env,tg | _ -> parse_atom env tg term) - | Prod(typ,a,b) when EConstr.Vars.noccurn sigma 1 b -> + | Prod(typ,a,b) when typ.binder_name = Anonymous || EConstr.Vars.noccurn sigma 1 b -> let f,env,tg = xparse_formula env tg a in let g,env,tg = xparse_formula env tg b in mkformula_binary mkI term f g,env,tg - | _ when EConstr.eq_constr sigma term (Lazy.force coq_True) -> (Mc.TT,env,tg) - | _ when EConstr.eq_constr sigma term (Lazy.force coq_False) -> Mc.(FF,env,tg) - | _ when is_prop term -> Mc.X(term),env,tg - | _ -> raise ParseError + | _ -> if EConstr.eq_constr sigma term (Lazy.force coq_True) + then (Mc.TT,env,tg) + else if EConstr.eq_constr sigma term (Lazy.force coq_False) + then Mc.(FF,env,tg) + else if is_prop term then Mc.X(term),env,tg + else raise ParseError in xparse_formula env tg ((*Reductionops.whd_zeta*) term) @@ -1170,8 +1208,8 @@ let dump_rexpr = lazy (** [make_goal_of_formula depxr vars props form] where - - vars is an environment for the arithmetic variables occuring in form - - props is an environment for the propositions occuring in form + - vars is an environment for the arithmetic variables occurring in form + - props is an environment for the propositions occurring in form @return a goal where all the variables and propositions of the formula are quantified *) @@ -1358,19 +1396,11 @@ let rec parse_hyps gl parse_arith env tg hyps = let (c,env,tg) = parse_formula gl parse_arith env tg t in ((i,c)::lhyps, env,tg) with e when CErrors.noncritical e -> (lhyps,env,tg) - (*(if debug then Printf.printf "parse_arith : %s\n" x);*) - - -(*exception ParseError*) - - let parse_goal gl parse_arith (env:Env.t) hyps term = - (* try*) let (f,env,tg) = parse_formula gl parse_arith env (Tag.from 0) term in let (lhyps,env,tg) = parse_hyps gl parse_arith env tg hyps in (lhyps,f,env) - (* with Failure x -> raise ParseError*) (** * The datastructures that aggregate theory-dependent proof values. @@ -1439,7 +1469,7 @@ let pre_processZ mt f = x <= y or (x and y are incomparable) *) (** - * Instanciate the current Coq goal with a Micromega formula, a varmap, and a + * Instantiate the current Coq goal with a Micromega formula, a varmap, and a * witness. *) @@ -1886,7 +1916,7 @@ let micromega_genr prover tac = ] with - | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") + | ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment") | Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout") | CsdpNotFound -> flush stdout ; Tacticals.New.tclFAIL 0 (Pp.str diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index b34c3b2b7d..a64a5a84b3 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -230,6 +230,13 @@ module Coq_Pos = | XO p -> XO (mul p y) | XH -> y + (** val iter : ('a1 -> 'a1) -> 'a1 -> positive -> 'a1 **) + + let rec iter f x = function + | XI n' -> f (iter f (iter f x n') n') + | XO n' -> iter f (iter f x n') n' + | XH -> f x + (** val size_nat : positive -> nat **) let rec size_nat = function @@ -398,6 +405,18 @@ module Z = | Zpos y' -> Zneg (Coq_Pos.mul x' y') | Zneg y' -> Zpos (Coq_Pos.mul x' y')) + (** val pow_pos : z -> positive -> z **) + + let pow_pos z0 = + Coq_Pos.iter (mul z0) (Zpos XH) + + (** val pow : z -> z -> z **) + + let pow x = function + | Z0 -> Zpos XH + | Zpos p -> pow_pos x p + | Zneg _ -> Z0 + (** val compare : z -> z -> comparison **) let compare x y = @@ -460,6 +479,12 @@ module Z = | O -> Z0 | S n1 -> Zpos (Coq_Pos.of_succ_nat n1) + (** val of_N : n -> z **) + + let of_N = function + | N0 -> Z0 + | Npos p -> Zpos p + (** val pos_div_eucl : positive -> z -> z * z **) let rec pos_div_eucl a b = @@ -1642,6 +1667,21 @@ let rec vm_add default x v = function | XO p -> Branch ((vm_add default p v l), o, r) | XH -> Branch (l, v, r)) +(** val zeval_const : z pExpr -> z option **) + +let rec zeval_const = function +| PEc c -> Some c +| PEX _ -> None +| PEadd (e1, e2) -> + map_option2 (fun x y -> Some (Z.add x y)) (zeval_const e1) (zeval_const e2) +| PEsub (e1, e2) -> + map_option2 (fun x y -> Some (Z.sub x y)) (zeval_const e1) (zeval_const e2) +| PEmul (e1, e2) -> + map_option2 (fun x y -> Some (Z.mul x y)) (zeval_const e1) (zeval_const e2) +| PEopp e0 -> map_option (fun x -> Some (Z.opp x)) (zeval_const e0) +| PEpow (e1, n0) -> + map_option (fun x -> Some (Z.pow x (Z.of_N n0))) (zeval_const e1) + type zWitness = z psatz (** val zWeakChecker : z nFormula list -> z psatz -> bool **) diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli index 5de6caac0b..64cb3a8355 100644 --- a/plugins/micromega/micromega.mli +++ b/plugins/micromega/micromega.mli @@ -86,6 +86,8 @@ module Coq_Pos : val mul : positive -> positive -> positive + val iter : ('a1 -> 'a1) -> 'a1 -> positive -> 'a1 + val size_nat : positive -> nat val compare_cont : comparison -> positive -> positive -> comparison @@ -124,6 +126,10 @@ module Z : val mul : z -> z -> z + val pow_pos : z -> positive -> z + + val pow : z -> z -> z + val compare : z -> z -> comparison val leb : z -> z -> bool @@ -140,6 +146,8 @@ module Z : val of_nat : nat -> z + val of_N : n -> z + val pos_div_eucl : positive -> z -> z * z val div_eucl : z -> z -> z * z @@ -179,20 +187,20 @@ val paddC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol val psubC : ('a1 -> 'a1 -> 'a1) -> 'a1 pol -> 'a1 -> 'a1 pol val paddI : - ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 - pol -> 'a1 pol + ('a1 -> 'a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol + -> 'a1 pol val psubI : ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol val paddX : - 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> - positive -> 'a1 pol -> 'a1 pol + 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> + 'a1 pol -> 'a1 pol val psubX : - 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> - 'a1 pol -> positive -> 'a1 pol -> 'a1 pol + 'a1 -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 + pol -> positive -> 'a1 pol -> 'a1 pol val padd : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol @@ -205,20 +213,19 @@ val pmulC_aux : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol val pmulC : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 - pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol val pmulI : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> - 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 + pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol val pmul : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - 'a1 pol -> 'a1 pol -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 + pol -> 'a1 pol -> 'a1 pol val psquare : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - 'a1 pol -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 + pol -> 'a1 pol type 'c pExpr = | PEc of 'c @@ -232,16 +239,16 @@ type 'c pExpr = val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol val ppow_pos : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 + pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol val ppow_N : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 + pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol val norm_aux : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> - ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 + -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol type ('tA, 'tX, 'aA, 'aF) gFormula = | TT @@ -253,8 +260,7 @@ type ('tA, 'tX, 'aA, 'aF) gFormula = | N of ('tA, 'tX, 'aA, 'aF) gFormula | I of ('tA, 'tX, 'aA, 'aF) gFormula * 'aF option * ('tA, 'tX, 'aA, 'aF) gFormula -val mapX : - ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula +val mapX : ('a2 -> 'a2) -> ('a1, 'a2, 'a3, 'a4) gFormula -> ('a1, 'a2, 'a3, 'a4) gFormula val foldA : ('a5 -> 'a3 -> 'a5) -> ('a1, 'a2, 'a3, 'a4) gFormula -> 'a5 -> 'a5 @@ -278,37 +284,36 @@ val cnf_tt : ('a1, 'a2) cnf val cnf_ff : ('a1, 'a2) cnf val add_term : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> - ('a1, 'a2) clause option + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> ('a1, + 'a2) clause option val or_clause : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) - clause -> ('a1, 'a2) clause option + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) clause -> + ('a1, 'a2) clause option val or_clause_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf - -> ('a1, 'a2) cnf + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1, 'a2) cnf -> + ('a1, 'a2) cnf val or_cnf : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> - ('a1, 'a2) cnf + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, + 'a2) cnf val and_cnf : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf type ('term, 'annot, 'tX, 'aF) tFormula = ('term, 'tX, 'annot, 'aF) gFormula val xcnf : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> - ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, - 'a3) cnf + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> + 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf val radd_term : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> (('a1, 'a2) clause, 'a2 list) sum val ror_clause : - ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause - -> (('a1, 'a2) clause, 'a2 list) sum + ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause -> + (('a1, 'a2) clause, 'a2 list) sum val ror_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause @@ -319,17 +324,16 @@ val ror_cnf : clause list -> ('a1, 'a2) cnf * 'a2 list val rxcnf : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> - ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, - 'a3) cnf * 'a3 list + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> + 'a3 -> ('a2, 'a3) cnf) -> bool -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 + list -val cnf_checker : - (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool +val cnf_checker : (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool val tauto_checker : - ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> - ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) -> ('a1, __, - 'a3, unit0) gFormula -> 'a4 list -> bool + ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> + 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) -> ('a1, __, 'a3, unit0) + gFormula -> 'a4 list -> bool val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool @@ -363,27 +367,27 @@ val map_option : ('a1 -> 'a2 option) -> 'a1 option -> 'a2 option val map_option2 : ('a1 -> 'a2 -> 'a3 option) -> 'a1 option -> 'a2 option -> 'a3 option val pexpr_times_nformula : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - 'a1 polC -> 'a1 nFormula -> 'a1 nFormula option + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 + polC -> 'a1 nFormula -> 'a1 nFormula option val nformula_times_nformula : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 + nFormula -> 'a1 nFormula -> 'a1 nFormula option val nformula_plus_nformula : - 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula - -> 'a1 nFormula option + 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> + 'a1 nFormula option val eval_Psatz : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1 nFormula option + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 + -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1 nFormula option val check_inconsistent : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> bool val check_normalised_formulas : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> - ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 + -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool type op2 = | OpEq @@ -396,8 +400,8 @@ type op2 = type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr } val norm : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> - ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 + -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol val psub0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> @@ -407,20 +411,20 @@ val padd0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol val xnormalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> - ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 + -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list val cnf_normalise : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> - ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 + -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf val xnegate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> - ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 + -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list val cnf_negate : - 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> - ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf + 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 + -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf val xdenorm : positive -> 'a1 pol -> 'a1 pExpr @@ -475,6 +479,8 @@ val singleton : 'a1 -> positive -> 'a1 -> 'a1 t val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t +val zeval_const : z pExpr -> z option + type zWitness = z psatz val zWeakChecker : z nFormula list -> z psatz -> bool @@ -563,12 +569,12 @@ val bound_var : positive -> z formula val mk_eq_pos : positive -> positive -> positive -> z formula val bound_vars : - (positive -> positive -> bool option -> 'a2) -> positive -> Vars.t -> (z formula, - 'a1, 'a2, 'a3) gFormula + (positive -> positive -> bool option -> 'a2) -> positive -> Vars.t -> (z formula, 'a1, + 'a2, 'a3) gFormula val bound_problem_fr : - (positive -> positive -> bool option -> 'a2) -> positive -> (z formula, 'a1, 'a2, - 'a3) gFormula -> (z formula, 'a1, 'a2, 'a3) gFormula + (positive -> positive -> bool option -> 'a2) -> positive -> (z formula, 'a1, 'a2, 'a3) + gFormula -> (z formula, 'a1, 'a2, 'a3) gFormula val zChecker : z nFormula list -> zArithProof -> bool diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 0209030b64..f038f8a71a 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -21,7 +21,7 @@ module type PHashtable = val open_in : string -> 'a t (** [open_in f] rebuilds a table from the records stored in file [f]. - As marshaling is not type-safe, it migth segault. + As marshaling is not type-safe, it might segfault. *) val find : 'a t -> key -> 'a diff --git a/plugins/micromega/persistent_cache.mli b/plugins/micromega/persistent_cache.mli index 4e7a388aaf..d2f3e756a9 100644 --- a/plugins/micromega/persistent_cache.mli +++ b/plugins/micromega/persistent_cache.mli @@ -17,7 +17,7 @@ module type PHashtable = val open_in : string -> 'a t (** [open_in f] rebuilds a table from the records stored in file [f]. - As marshaling is not type-safe, it migth segault. + As marshaling is not type-safe, it might segfault. *) val find : 'a t -> key -> 'a diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml index 6aebc4ca9a..e3a9f6f60f 100644 --- a/plugins/micromega/sos_lib.ml +++ b/plugins/micromega/sos_lib.ml @@ -200,7 +200,7 @@ let is_undefined f = | _ -> false;; (* ------------------------------------------------------------------------- *) -(* Operation analagous to "map" for lists. *) +(* Operation analogous to "map" for lists. *) (* ------------------------------------------------------------------------- *) let mapf = diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 1777418ef6..bece316c7d 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -267,7 +267,7 @@ module PIdeal = Ideal.Make(Poly) open PIdeal (* term to sparse polynomial - varaibles <=np are in the coefficients + variables <=np are in the coefficients *) let term_pol_sparse nvars np t= diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 5db587b9cc..f6ca232c2e 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -357,7 +357,7 @@ let remP v p = moinsP p (multP (coefDom v p) (puisP (x v) (deg v p))) -(* first interger coefficient of p *) +(* first integer coefficient of p *) let rec coef_int_tete p = let v = max_var_pol p in if v>0 @@ -526,7 +526,7 @@ let div_pol_rat p q= (* pseudo division : q = c*x^m+q1 - retruns (r,c,d,s) s.t. c^d*p = s*q + r. + returns (r,c,d,s) s.t. c^d*p = s*q + r. *) let pseudo_div p q x = diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 695f000cb1..23d7b141a4 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -359,7 +359,10 @@ Ltac zify_positive_rel := Ltac zify_positive_op := match goal with - (* Zneg -> -Zpos (except for numbers) *) + (* Z.pow_pos -> Z.pow *) + | H : context [ Z.pow_pos ?a ?b ] |- _ => change (Z.pow_pos a b) with (Z.pow a (Z.pos b)) in H + | |- context [ Z.pow_pos ?a ?b ] => change (Z.pow_pos a b) with (Z.pow a (Z.pos b)) + (* Zneg -> -Zpos (except for numbers) *) | H : context [ Zneg ?a ] |- _ => let isp := isPcst a in match isp with @@ -377,6 +380,10 @@ Ltac zify_positive_op := | H : context [ Zpos (Pos.of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H | |- context [ Zpos (Pos.of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a) + (* Z.power_pos *) + | H : context [ Zpos (Pos.of_succ_nat ?a) ] |- _ => rewrite (Zpos_P_of_succ_nat a) in H + | |- context [ Zpos (Pos.of_succ_nat ?a) ] => rewrite (Zpos_P_of_succ_nat a) + (* Pos.add -> Z.add *) | H : context [ Zpos (?a + ?b) ] |- _ => change (Zpos (a+b)) with (Zpos a + Zpos b) in H | |- context [ Zpos (?a + ?b) ] => change (Zpos (a+b)) with (Zpos a + Zpos b) diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 4886c8b9aa..9be2535a3f 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -105,7 +105,7 @@ Section ZMORPHISM. Proof. constructor. destruct c;intros;try discriminate. - injection H as <-. + injection H as [= <-]. simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial. Qed. diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index f7cb6b688b..c5d396427b 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -894,7 +894,7 @@ Section MakeRingPol. revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. - discriminate. - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. - * injection H as <-. rewrite <- PSubstL1_ok; intuition. + * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition. * now apply IH. Qed. diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/setoid_ring/g_newring.mlg index 6be556b2ae..5dfead2d7e 100644 --- a/plugins/setoid_ring/g_newring.mlg +++ b/plugins/setoid_ring/g_newring.mlg @@ -13,8 +13,6 @@ open Ltac_plugin open Pp open Util -open Libnames -open Printer open Newring_ast open Newring open Stdarg @@ -85,21 +83,10 @@ END VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] -> - { let l = match l with None -> [] | Some l -> l in add_theory id t l } - | ![proof] [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> { - fun ~pstate -> - Feedback.msg_notice (strbrk "The following ring structures have been declared:"); - Spmap.iter (fun fn fi -> - (* We should use the global env here as this shouldn't contain proof - data, however preserving behavior as requested in review. *) - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in - Feedback.msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++ - str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req)) - ) !from_name; - pstate } + { add_theory id t (Option.default [] l) } + | [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> { + print_rings () + } END TACTIC EXTEND ring_lookup @@ -135,20 +122,9 @@ END VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF | [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] -> { let l = match l with None -> [] | Some l -> l in add_field_theory id t l } -| ![proof] [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> { - fun ~pstate -> - Feedback.msg_notice (strbrk "The following field structures have been declared:"); - Spmap.iter (fun fn fi -> - (* We should use the global env here as this shouldn't - contain proof data. *) - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in - Feedback.msg_notice (hov 2 - (Ppconstr.pr_id (Libnames.basename fn)++spc()++ - str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++ - str"and equivalence relation "++ pr_constr_env env sigma fi.field_req)) - ) !field_from_name; - pstate } +| [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> { + print_fields () + } END TACTIC EXTEND field_lookup diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index b02b97f656..8e7b045b8e 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -153,9 +153,11 @@ let decl_constant na univs c = let open Constr in let vars = CVars.universes_of_constr c in let univs = UState.restrict_universe_context univs vars in - let univs = Monomorphic_entry univs in + let () = Declare.declare_universe_context false univs in + let types = (Typeops.infer (Global.env ()) c).uj_type in + let univs = Monomorphic_entry Univ.ContextSet.empty in mkConst(declare_constant (Id.of_string na) - (DefinitionEntry (definition_entry ~opaque:true ~univs c), + (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c), IsProof Lemma)) (* Calling a global tactic *) @@ -327,6 +329,18 @@ module Cmap = Map.Make(Constr) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table" +let print_rings () = + Feedback.msg_notice (strbrk "The following ring structures have been declared:"); + Spmap.iter (fun fn fi -> + let env = Global.env () in + let sigma = Evd.from_env env in + Feedback.msg_notice + (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req)) + ) !from_name + let ring_for_carrier r = Cmap.find r !from_carrier let find_ring_structure env sigma l = @@ -824,6 +838,18 @@ let dest_field env evd th_spec = let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table" let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table" +let print_fields () = + Feedback.msg_notice (strbrk "The following field structures have been declared:"); + Spmap.iter (fun fn fi -> + let env = Global.env () in + let sigma = Evd.from_env env in + Feedback.msg_notice + (hov 2 + (Ppconstr.pr_id (Libnames.basename fn)++spc()++ + str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++ + str"and equivalence relation "++ pr_constr_env env sigma fi.field_req)) + ) !field_from_name + let field_for_carrier r = Cmap.find r !field_from_carrier let find_field_structure env sigma l = diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index fcd04a2e73..3a21a82c5c 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -10,7 +10,6 @@ open Names open EConstr -open Libnames open Constrexpr open Newring_ast @@ -23,7 +22,7 @@ val add_theory : constr_expr -> constr_expr ring_mod list -> unit -val from_name : ring_info Spmap.t ref +val print_rings : unit -> unit val ring_lookup : Geninterp.Val.t -> @@ -35,7 +34,7 @@ val add_field_theory : constr_expr -> constr_expr field_mod list -> unit -val field_from_name : field_info Spmap.t ref +val print_fields : unit -> unit val field_lookup : Geninterp.Val.t -> diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index 49d729bd6c..c5f387b248 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -49,7 +49,7 @@ Require Import ssreflect ssrfun. altP (idP my_formula) but circumventing the dependent index capture issue; destructing boolP my_formula generates two subgoals with - assumtions my_formula and ~~ myformula. As + assumptions my_formula and ~~ myformula. As with altP, my_formula must be an application. \unless C, P <-> we can assume property P when a something that holds under condition C (such as C itself). @@ -64,7 +64,7 @@ Require Import ssreflect ssrfun. := forall b : bool, (P -> b) -> b. This is equivalent to ~ (~ P) when P : Prop. implies P Q == wrapper variant type that coerces to P -> Q and - can be used as a P -> Q view unambigously. + can be used as a P -> Q view unambiguously. Useful to avoid spurious insertion of <-> views when Q is a conjunction of foralls, as in Lemma all_and2 below; conversely, avoids confusion in @@ -1003,7 +1003,7 @@ Proof. by case: a; case: b. Qed. Lemma negb_or (a b : bool) : ~~ (a || b) = ~~ a && ~~ b. Proof. by case: a; case: b. Qed. -(** Pseudo-cancellation -- i.e, absorbtion **) +(** Pseudo-cancellation -- i.e, absorption **) Lemma andbK a b : a && b || a = a. Proof. by case: a; case: b. Qed. Lemma andKb a b : a || b && a = a. Proof. by case: a; case: b. Qed. @@ -1245,7 +1245,7 @@ Notation "[ 'pred' x : T | E1 & E2 ]" := (** Coercions for simpl_pred. As simpl_pred T values are used both applicatively and collectively we need simpl_pred to coerce to both pred T _and_ {pred T}. However it is - undesireable to have two distinct constants for what are essentially identical + undesirable to have two distinct constants for what are essentially identical coercion functions, as this confuses the SSReflect keyed matching algorithm. While the Coq Coercion declarations appear to disallow such Coercion aliasing, it is possible to work around this limitation with a combination of modules @@ -1331,9 +1331,9 @@ Variant mem_pred T := Mem of pred T. Similarly to pred_of_simpl, it will usually not be inserted by type inference, as all mem_pred mp =~= pred_sort ?pT unification problems will be solve by the memPredType instance below; pred_of_mem will however - be used if a mem_pred T is used as a {pred T}, which is desireable as it + be used if a mem_pred T is used as a {pred T}, which is desirable as it will avoid a redundant mem in a collective, e.g., passing (mem A) to a lemma - expection a generic collective predicate p : {pred T} and premise x \in P + exception a generic collective predicate p : {pred T} and premise x \in P will display a subgoal x \in A rathere than x \in mem A. Conversely, pred_of_mem will _not_ if it is used id (mem A) is used applicatively or as a pred T; there the simpl_of_mem coercion defined below @@ -1396,7 +1396,7 @@ Notation "[ 'rel' x y 'in' A & B ]" := Notation "[ 'rel' x y 'in' A | E ]" := [rel x y in A & A | E] : fun_scope. Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] : fun_scope. -(** Aliases of pred T that let us tag intances of simpl_pred as applicative +(** Aliases of pred T that let us tag instances of simpl_pred as applicative or collective, via bespoke coercions. This tagging will give control over the simplification behaviour of inE and othe rewriting lemmas below. For this control to work it is crucial that collective_of_simpl _not_ @@ -1428,7 +1428,7 @@ Implicit Types (mp : mem_pred T). - registered_applicative_pred: this user-facing structure is used to declare values of type pred T meant to be used applicatively. The structure parameter merely displays this same value, and is used to avoid - undesireable, visible occurrence of the structure in the right hand side + undesirable, visible occurrence of the structure in the right hand side of rewrite rules such as app_predE. There is a canonical instance of registered_applicative_pred for values of the applicative_of_simpl coercion, which handles the @@ -1454,7 +1454,7 @@ Implicit Types (mp : mem_pred T). has been fixed earlier by the manifest_mem_pred match. In particular the definition of a predicate using the applicative_pred_of_simpl idiom above will not be expanded - this very case is the reason in_applicative uses - a mem_pred telescope in its left hand side. The more straighforward + a mem_pred telescope in its left hand side. The more straightforward ?x \in applicative_pred_value ?ap (equivalent to in_mem ?x (Mem ?ap)) with ?ap : registered_applicative_pred ?p would set ?p := [pred x | ...] rather than ?p := Apred in the example above. diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 56f17703ff..6c7b4702b6 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -194,8 +194,8 @@ let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) let mkRVar id = DAst.make @@ GRef (VarRef id,None) let mkRltacVar id = DAst.make @@ GVar (id) let mkRCast rc rt = DAst.make @@ GCast (rc, CastConv rt) -let mkRType = DAst.make @@ GSort (GType []) -let mkRProp = DAst.make @@ GSort (GProp) +let mkRType = DAst.make @@ GSort (UAnonymous {rigid=true}) +let mkRProp = DAst.make @@ GSort (UNamed [GProp,0]) let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2) let mkRConstruct c = DAst.make @@ GRef (ConstructRef c,None) let mkRInd mind = DAst.make @@ GRef (IndRef mind,None) @@ -871,8 +871,8 @@ open Constrexpr open Util (** Constructors for constr_expr *) -let mkCProp loc = CAst.make ?loc @@ CSort GProp -let mkCType loc = CAst.make ?loc @@ CSort (GType []) +let mkCProp loc = CAst.make ?loc @@ CSort (UNamed [GProp,0]) +let mkCType loc = CAst.make ?loc @@ CSort (UAnonymous {rigid=true}) let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None) let rec mkCHoles ?loc n = if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) @@ -1119,6 +1119,7 @@ let cleartac clr = check_hyps_uniq [] clr; Tactics.clear (hyps_ids clr) (* XXX the k of the redex should percolate out *) let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = let pat = interp_cpattern gl t None in (* UGLY API *) + let gl = pf_merge_uc_of (fst pat) gl in let cl, env, sigma = Tacmach.pf_concl gl, pf_env gl, project gl in let (c, ucst), cl = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr cl) pat occ 1 @@ -1253,6 +1254,7 @@ let abs_wgen keep_let f gen (gl,args,c) = | _, Some ((x, "@"), Some p) -> let x = hoi_id x in let cp = interp_cpattern gl p None in + let gl = pf_merge_uc_of (fst cp) gl in let (t, ucst), c = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1 with NoMatch -> redex_of_pattern env cp, (EConstr.Unsafe.to_constr c) in @@ -1265,6 +1267,7 @@ let abs_wgen keep_let f gen (gl,args,c) = | _, Some ((x, _), Some p) -> let x = hoi_id x in let cp = interp_cpattern gl p None in + let gl = pf_merge_uc_of (fst cp) gl in let (t, ucst), c = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr c) cp None 1 with NoMatch -> redex_of_pattern env cp, (EConstr.Unsafe.to_constr c) in diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index 5e3e8ce5fb..572d72ccd8 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -132,7 +132,7 @@ Delimit Scope ssripat_scope with ssripat. Make the general "if" into a notation, so that we can override it below. The notations are "only parsing" because the Coq decompiler will not recognize the expansion of the boolean if; using the default printer - avoids a spurrious trailing %%GEN_IF. **) + avoids a spurious trailing %%GEN_IF. **) Declare Scope general_if_scope. Delimit Scope general_if_scope with GEN_IF. @@ -347,10 +347,10 @@ Register protect_term as plugins.ssreflect.protect_term. (** The ssreflect idiom for a non-keyed pattern: - - unkeyed t wiil match any subterm that unifies with t, regardless of + - unkeyed t will match any subterm that unifies with t, regardless of whether it displays the same head symbol as t. - unkeyed t a b will match any application of a term f unifying with t, - to two arguments unifying with with a and b, repectively, regardless of + to two arguments unifying with with a and b, respectively, regardless of apparent head symbols. - unkeyed x where x is a variable will match any subterm with the same type as x (when x would raise the 'indeterminate pattern' error). **) @@ -380,7 +380,7 @@ Notation "=^~ r" := (ssr_converse r) : form_scope. locked_with k t is equal but not convertible to t, much like locked t, but supports explicit tagging with a value k : unit. This is used to mitigate a flaw in the term comparison heuristic of the Coq kernel, - which treats all terms of the form locked t as equal and conpares their + which treats all terms of the form locked t as equal and compares their arguments recursively, leading to an exponential blowup of comparison. For this reason locked_with should be used rather than locked when defining ADT operations. The unlock tactic does not support locked_with @@ -523,7 +523,7 @@ Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2. elim/abstract_context: (pattern) => G defG. vm_compute; rewrite {}defG {G}. Note that vm_cast are not stored in the proof term - for reductions occuring in the context, hence + for reductions occurring in the context, hence set here := pattern; vm_compute in (value of here) blows up at Qed time. **) Lemma abstract_context T (P : T -> Type) x : @@ -637,7 +637,7 @@ Ltac over := later complain that it cannot erase _top_assumption_ after having abstracted the viewed assumption. Making x and y maximal implicits would avoid this and force the intended @Some_inj nat x y _top_assumption_ - interpretation, but is undesireable as it makes it harder to use Some_inj + interpretation, but is undesirable as it makes it harder to use Some_inj with the many SSReflect and MathComp lemmas that have an injectivity premise. Specifying {T : nonPropType} solves this more elegantly, as then (?T : Type) no longer unifies with (Some n = Some 0), which has sort Prop. @@ -655,13 +655,13 @@ Module NonPropType. maybeProp T to tt and use the test_negative instance and set ?r to false. - call_of c r sets up a call to test_of on condition c with expected result r. It has a default instance for its 'callee' projection to Type, which - sets c := maybeProj T and r := false whe unifying with a type T. + sets c := maybeProj T and r := false when unifying with a type T. - type is a telescope on call_of c r, which checks that unifying test_of ?r1 with c indeed sets ?r1 := r; the type structure bundles the 'test' instance and its 'result' value along with its call_of c r projection. The default instance essentially provides eta-expansion for 'type'. This is only essential for the first 'result' projection to bool; using the instance - for other projection merely avoids spurrious delta expansions that would + for other projection merely avoids spurious delta expansions that would spoil the notProp T notation. In detail, unifying T =~= ?S with ?S : nonPropType, i.e., (1) T =~= @callee (@condition (result ?S) (test ?S)) (result ?S) (frame ?S) diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 675e4d2457..3a0868b7e4 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -96,7 +96,7 @@ let subgoals_tys sigma (relctx, concl) = * (occ, c), deps and the pattern inferred from the type of the eliminator * 3. build the new predicate matching the patterns, and the tactic to * generalize the equality in case eqid is not None - * 4. build the tactic handle intructions and clears as required in ipats and + * 4. build the tactic handle instructions and clears as required in ipats and * by eqid *) let get_eq_type gl = @@ -383,15 +383,22 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let c = fire_subst gl (List.assoc (n_elim_args - k - 1) elim_args) in let gl, t = pfe_type_of gl c in let gl, eq = get_eq_type gl in - let gen_eq_tac, gl = + let gen_eq_tac, eq_ty, gl = let refl = EConstr.mkApp (eq, [|t; c; c|]) in let new_concl = EConstr.mkArrow refl Sorts.Relevant (EConstr.Vars.lift 1 (pf_concl orig_gl)) in let new_concl = fire_subst gl new_concl in let erefl, gl = mkRefl t c gl in let erefl = fire_subst gl erefl in - apply_type new_concl [erefl], gl in + let erefl_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl in + let eq_ty = Retyping.get_type_of (pf_env gl) (project gl) erefl_ty in + let gen_eq_tac s = + let open Evd in + let sigma = merge_universe_context s.sigma (evar_universe_context (project gl)) in + apply_type new_concl [erefl] { s with sigma } + in + gen_eq_tac, eq_ty, gl in let rel = k + if c_is_head_p then 1 else 0 in - let src, gl = mkProt EConstr.mkProp EConstr.(mkApp (eq,[|t; c; mkRel rel|])) gl in + let src, gl = mkProt eq_ty EConstr.(mkApp (eq,[|t; c; mkRel rel|])) gl in let concl = EConstr.mkArrow src Sorts.Relevant (EConstr.Vars.lift 1 concl) in let clr = if deps <> [] then clr else [] in concl, gen_eq_tac, clr, gl diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 93c0d5c236..dbb0f25abf 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -128,7 +128,7 @@ let newssrcongrtac arg ist gl = x, re_sig si sigma in let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in let ssr_congr lr = EConstr.mkApp (arr, lr) in - (* here thw two cases: simple equality or arrow *) + (* here the two cases: simple equality or arrow *) let equality, _, eq_args, gl' = let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in pf_saturate gl (EConstr.of_constr eq) 3 in @@ -313,7 +313,7 @@ let rw_progress rhs lhs ise = not (EConstr.eq_constr ise lhs (Evarutil.nf_evar i (* Coq has a more general form of "equation" (any type with a single *) (* constructor with no arguments with_rect_r elimination lemmas). *) (* However there is no clear way of determining the LHS and RHS of *) -(* such a generic Leibnitz equation -- short of inspecting the type *) +(* such a generic Leibniz equation -- short of inspecting the type *) (* of the elimination lemmas. *) let rec strip_prod_assum c = match Constr.kind c with @@ -619,7 +619,11 @@ let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt) with _ when snd mult = May -> fail := true; (project gl, EConstr.mkProp) in let rwtac gl = let rx = Option.map (interp_rpattern gl) grx in + let gl = match rx with + | None -> gl + | Some (s,_) -> pf_merge_uc_of s gl in let t = interp gt gl in + let gl = pf_merge_uc_of (fst t) gl in (match kind with | RWred sim -> simplintac occ rx sim | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 27a558611e..62d344cc02 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -79,7 +79,6 @@ let pr_ssrtacarg env sigma _ _ prt = prt env sigma tacltop } ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } -| [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") } END GRAMMAR EXTEND Gram GLOBAL: ssrtacarg; @@ -88,7 +87,6 @@ END (* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *) ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } -| [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") } END GRAMMAR EXTEND Gram GLOBAL: ssrtac3arg; @@ -204,17 +202,6 @@ ARGUMENT EXTEND ssrhoi_id TYPED AS ssrhoirep PRINTED BY { pr_ssrhoi } | [ ident(id) ] -> { Id (SsrHyp(Loc.tag ~loc id)) } END -{ - -let pr_ssrhyps _ _ _ = pr_hyps - -} - -ARGUMENT EXTEND ssrhyps TYPED AS ssrhyp list PRINTED BY { pr_ssrhyps } - INTERPRETED BY { interp_hyps } - | [ ssrhyp_list(hyps) ] -> { check_hyps_uniq [] hyps; hyps } -END - (** Rewriting direction *) { @@ -310,18 +297,13 @@ GRAMMAR EXTEND Gram END -ARGUMENT EXTEND ssrsimpl TYPED AS ssrsimplrep PRINTED BY { pr_ssrsimpl } -| [ ssrsimpl_ne(sim) ] -> { sim } -| [ ] -> { Nop } -END - { let pr_ssrclear _ _ _ = pr_clear mt } -ARGUMENT EXTEND ssrclear_ne TYPED AS ssrhyps PRINTED BY { pr_ssrclear } +ARGUMENT EXTEND ssrclear_ne TYPED AS ssrhyp list PRINTED BY { pr_ssrclear } | [ "{" ne_ssrhyp_list(clr) "}" ] -> { check_hyps_uniq [] clr; clr } END @@ -1005,7 +987,6 @@ let pr_ssrfwdidx _ _ _ = pr_ssrfwdid (* We use a primitive parser for the head identifier of forward *) (* tactis to avoid syntactic conflicts with basic Coq tactics. *) ARGUMENT EXTEND ssrfwdid TYPED AS ident PRINTED BY { pr_ssrfwdidx } - | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END { @@ -1564,7 +1545,6 @@ let pr_ssrdoarg env sigma prc _ prt (((n, m), tac), clauses) = ARGUMENT EXTEND ssrdoarg TYPED AS (((ssrindex * ssrmmod) * ssrhintarg) * ssrclauses) PRINTED BY { pr_ssrdoarg env sigma } -| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END { @@ -1587,7 +1567,7 @@ let pr_ssrseqarg env sigma _ _ prt = function (* an unindexed tactic. *) ARGUMENT EXTEND ssrseqarg TYPED AS (ssrindex * (ssrhintarg * tactic option)) PRINTED BY { pr_ssrseqarg env sigma } -| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } + END { @@ -1867,7 +1847,6 @@ let pr_ssrseqdir _ _ _ = function } ARGUMENT EXTEND ssrseqdir TYPED AS ssrdir PRINTED BY { pr_ssrseqdir } -| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END TACTIC EXTEND ssrtclseq @@ -2004,7 +1983,6 @@ let pr_ssreqid _ _ _ = pr_eqid (* We must use primitive parsing here to avoid conflicts with the *) (* basic move, case, and elim tactics. *) ARGUMENT EXTEND ssreqid TYPED AS ssripatrep option PRINTED BY { pr_ssreqid } -| [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END { @@ -2326,7 +2304,6 @@ let noruleterm loc = mk_term xNoFlag (mkCProp loc) } ARGUMENT EXTEND ssrrule_ne TYPED AS (ssrrwkind * ssrterm) PRINTED BY { pr_ssrrule } - | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END GRAMMAR EXTEND Gram @@ -2413,7 +2390,6 @@ let pr_ssrrwargs _ _ _ rwargs = pr_list spc pr_rwarg rwargs } ARGUMENT EXTEND ssrrwargs TYPED AS ssrrwarg list PRINTED BY { pr_ssrrwargs } - | [ "YouShouldNotTypeThis" ] -> { anomaly "Grammar placeholder match" } END { diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 08f028465b..8880a6516e 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -566,12 +566,10 @@ let print_view_hints env sigma kind l = } VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY -| ![proof] [ "Print" "Hint" "View" ssrviewpos(i) ] -> +| [ "Print" "Hint" "View" ssrviewpos(i) ] -> { - fun ~pstate -> - (* XXX this is incorrect *) - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in + let env = Global.env () in + let sigma = Evd.from_env env in (match i with | Some k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k) @@ -579,8 +577,7 @@ VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY List.iter (fun k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k)) [ Ssrview.AdaptorDb.Forward; Ssrview.AdaptorDb.Backward; - Ssrview.AdaptorDb.Equivalence ]); - pstate + Ssrview.AdaptorDb.Equivalence ]) } END diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 25975c84e8..6d1d858648 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -143,7 +143,7 @@ val mk_tpattern : type find_P = env -> constr -> int -> k:subst -> constr -(** [conclude ()] asserts that all mentioned ocurrences have been visited. +(** [conclude ()] asserts that all mentioned occurrences have been visited. @return the instance of the pattern, the evarmap after the pattern instantiation, the proof term and the ssrdit stored in the tpattern @raise UserEerror if too many occurrences were specified *) diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index 0f0f3953da..5808385723 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -34,23 +34,8 @@ VERNAC ARGUMENT EXTEND numnotoption END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] ![proof][ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> - { (* It is a bug to use the proof context here, but at the request of - * the reviewers we keep this broken behavior for now. The Global env - * should be used instead, and the `env, sigma` parameteter to the - * numeral notation command removed. - *) - fun ~pstate -> - let sigma, env = match pstate with - | None -> - let env = Global.env () in - let sigma = Evd.from_env env in - sigma, env - | Some pstate -> - Pfedit.get_current_context pstate - in - vernac_numeral_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) o; - pstate } + { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } END diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg index cc8c13a84b..1e06cd8ddb 100644 --- a/plugins/syntax/g_string.mlg +++ b/plugins/syntax/g_string.mlg @@ -19,22 +19,7 @@ open Stdarg } VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] ![proof] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) ] -> - { (* It is a bug to use the proof context here, but at the request of - * the reviewers we keep this broken behavior for now. The Global env - * should be used instead, and the `env, sigma` parameteter to the - * numeral notation command removed. - *) - fun ~pstate -> - let sigma, env = match pstate with - | None -> - let env = Global.env () in - let sigma = Evd.from_env env in - sigma, env - | Some pstate -> - Pfedit.get_current_context pstate - in - vernac_string_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc); - pstate } + { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) } END diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index ec8c2338fb..b0b6fa69bb 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -101,7 +101,9 @@ let type_error_of g ty = str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).") -let vernac_numeral_notation env sigma local ty f g scope opts = +let vernac_numeral_notation local ty f g scope opts = + let env = Global.env () in + let sigma = Evd.from_env env in let dec_ty = locate_decimal () in let z_pos_ty = locate_z () in let int63_ty = locate_int63 () in diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli index b14ed18497..3fc0385f5d 100644 --- a/plugins/syntax/numeral.mli +++ b/plugins/syntax/numeral.mli @@ -14,6 +14,6 @@ open Notation (** * Numeral notation *) -val vernac_numeral_notation : Environ.env -> Evd.evar_map -> locality_flag -> +val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index 5fae696d58..4234cee1bd 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -47,7 +47,9 @@ let type_error_of g ty = (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).") -let vernac_string_notation env sigma local ty f g scope = +let vernac_string_notation local ty f g scope = + let env = Global.env () in + let sigma = Evd.from_env env in let app x y = mkAppC (x,[y]) in let cref q = mkRefC q in let cbyte = cref (q_byte ()) in diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli index e81de603d9..1e25758572 100644 --- a/plugins/syntax/string_notation.mli +++ b/plugins/syntax/string_notation.mli @@ -13,6 +13,6 @@ open Vernacexpr (** * String notation *) -val vernac_string_notation : Environ.env -> Evd.evar_map -> locality_flag -> +val vernac_string_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> unit |