diff options
72 files changed, 1124 insertions, 897 deletions
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index daa76fec46..340b66bbd0 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -133,8 +133,12 @@ in time. the package managers can Cc `@erikmd` to request that he prepare the necessary configuration for the Docker release in [`coqorg/coq`](https://hub.docker.com/r/coqorg/coq) (namely, he'll need to make sure a `coq-bignums` opam package is available in [`extra-dev`](https://github.com/coq/opam-coq-archive/tree/master/extra-dev), respectively [`released`](https://github.com/coq/opam-coq-archive/tree/master/released), so the Docker image gathering `coq` and `coq-bignums` can be built). - [ ] Draft a release on GitHub. -- [ ] Get `@maximedenes` to sign the Windows and MacOS packages and - upload them on GitHub. +- [ ] Sign the Windows and MacOS packages and upload them on GitHub. + + The Windows packages must be signed by the Inria IT security service. They + should be sent as a link to the binary together with its SHA256 hash in a + signed e-mail, via our local contact (currently `@maximedenes`). + + The MacOS packages should be signed by our own certificate, by sending them + to `@maximedenes`. A detailed step-by-step guide can be found [on the wiki](https://github.com/coq/coq/wiki/SigningReleases). - [ ] Prepare a page of news on the website with the link to the GitHub release (see [coq/www#63](https://github.com/coq/www/pull/63)). - [ ] Upload the new version of the reference manual to the website. diff --git a/doc/changelog/03-notations/12163-fix-12159.rst b/doc/changelog/03-notations/12163-fix-12159.rst new file mode 100644 index 0000000000..978ed561dd --- /dev/null +++ b/doc/changelog/03-notations/12163-fix-12159.rst @@ -0,0 +1,11 @@ +- **Fixed:** + Numeral Notations now play better with multiple scopes for the same + inductive type. Previously, when multiple numeral notations were defined + for the same inductive, only the last one was considered for + printing. Now, among the notations that are usable for printing and either + have a scope delimiter or are open, the selection is made according + to the order of open scopes, or according to the last defined + notation if no appropriate scope is open + (`#12163 <https://github.com/coq/coq/pull/12163>`_, + fixes `#12159 <https://github.com/coq/coq/pull/12159>`_, + by Pierre Roux, review by Hugo Herbelin and Jason Gross). diff --git a/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst b/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst new file mode 100644 index 0000000000..37aaf697b5 --- /dev/null +++ b/doc/changelog/10-standard-library/12237-list-more-filter-incl.rst @@ -0,0 +1,4 @@ +- **Added:** + new lemmas in ``List``: ``incl_map``, ``incl_filter``, ``NoDup_filter``, ``incl_Forall_in_iff`` + (`#12237 <https://github.com/coq/coq/pull/12237>`_, + by Olivier Laurent). diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index b94b1fc657..e9e866c5fb 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,6 +1,6 @@ let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in - let scope = DeclareDef.Global Declare.ImportDefaultBehavior in + let scope = Declare.Global Declare.ImportDefaultBehavior in let kind = Decls.(IsDefinition Definition) in - DeclareDef.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl + Declare.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl ~opaque:false ~poly ~types:None ~body sigma diff --git a/interp/constrextern.ml b/interp/constrextern.ml index a37bac3275..d5a5bde616 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -435,13 +435,10 @@ let extern_record_pattern cstrsp args = let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; - let (na,sc,p) = uninterp_prim_token_cases_pattern pat in + let (na,p,key) = uninterp_prim_token_cases_pattern pat scopes in match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> - match availability_of_prim_token p sc scopes with - | None -> raise No_match - | Some key -> let loc = cases_pattern_loc pat in insert_pat_coercion ?loc coercion (insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na) @@ -848,13 +845,11 @@ let same_binder_type ty nal c = (* one with no delimiter if possible) *) let extern_possible_prim_token (custom,scopes) r = - let (sc,n) = uninterp_prim_token r in + let (n,key) = uninterp_prim_token r scopes in match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> - match availability_of_prim_token n sc scopes with - | None -> raise No_match - | Some key -> insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) + insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) let filter_enough_applied nargs l = match nargs with diff --git a/interp/notation.ml b/interp/notation.ml index 0afbb9cd62..7761606f11 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -932,7 +932,7 @@ let prim_token_interp_infos = (* Table from global_reference to backtrack-able informations about prim_token uninterpretation (in particular uninterpreter unique id). *) let prim_token_uninterp_infos = - ref (GlobRef.Map.empty : (scope_name * prim_token_interp_info * bool) GlobRef.Map.t) + ref (GlobRef.Map.empty : ((scope_name * (prim_token_interp_info * bool)) list) GlobRef.Map.t) let hashtbl_check_and_set allow_overwrite uid f h eq = match Hashtbl.find h uid with @@ -968,10 +968,13 @@ let cache_prim_token_interpretation (_,infos) = check_scope ~tolerant:true sc; prim_token_interp_infos := String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos; - List.iter (fun r -> prim_token_uninterp_infos := - GlobRef.Map.add r (sc,ptii,infos.pt_in_match) - !prim_token_uninterp_infos) - infos.pt_refs + let add_uninterp r = + let l = try GlobRef.Map.find r !prim_token_uninterp_infos with Not_found -> [] in + let l = List.remove_assoc_f String.equal sc l in + prim_token_uninterp_infos := + GlobRef.Map.add r ((sc,(ptii,infos.pt_in_match)) :: l) + !prim_token_uninterp_infos in + List.iter add_uninterp infos.pt_refs let subst_prim_token_interpretation (subs,infos) = { infos with @@ -1324,27 +1327,6 @@ let entry_has_ident = function | InCustomEntryLevel (s,n) -> try String.Map.find s !entry_has_ident_map <= n with Not_found -> false -let uninterp_prim_token c = - match glob_prim_constr_key c with - | None -> raise Notation_ops.No_match - | Some r -> - try - let (sc,info,_) = GlobRef.Map.find r !prim_token_uninterp_infos in - let uninterp = match info with - | Uid uid -> Hashtbl.find prim_token_uninterpreters uid - | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o) - | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o) - in - match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with - | None -> raise Notation_ops.No_match - | Some n -> (sc,n) - with Not_found -> raise Notation_ops.No_match - -let uninterp_prim_token_cases_pattern c = - match glob_constr_of_closed_cases_pattern (Global.env()) c with - | exception Not_found -> raise Notation_ops.No_match - | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n) - let availability_of_prim_token n printer_scope local_scopes = let f scope = try @@ -1366,6 +1348,60 @@ let availability_of_prim_token n printer_scope local_scopes = let scopes = make_current_scopes local_scopes in Option.map snd (find_without_delimiters f (NotationInScope printer_scope,None) scopes) +let rec find_uninterpretation need_delim def find = function + | [] -> + List.find_map + (fun (sc,_,_) -> try Some (find need_delim sc) with Not_found -> None) + def + | OpenScopeItem scope :: scopes -> + (try find need_delim scope + with Not_found -> find_uninterpretation need_delim def find scopes) (* TODO: here we should also update the need_delim list with all regular notations in scope [scope] that could shadow a numeral notation *) + | LonelyNotationItem ntn::scopes -> + find_uninterpretation (ntn::need_delim) def find scopes + +let uninterp_prim_token c local_scopes = + match glob_prim_constr_key c with + | None -> raise Notation_ops.No_match + | Some r -> + let uninterp (sc,(info,_)) = + try + let uninterp = match info with + | Uid uid -> Hashtbl.find prim_token_uninterpreters uid + | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o) + | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o) + in + match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with + | None -> None + | Some n -> Some (sc,n) + with Not_found -> None in + let add_key (sc,n) = + Option.map (fun k -> sc,n,k) (availability_of_prim_token n sc local_scopes) in + let l = + try GlobRef.Map.find r !prim_token_uninterp_infos + with Not_found -> raise Notation_ops.No_match in + let l = List.map_filter uninterp l in + let l = List.map_filter add_key l in + let find need_delim sc = + let _,n,k = List.find (fun (sc',_,_) -> String.equal sc' sc) l in + if k <> None then n,k else + let hidden = + List.exists + (fun n' -> notation_eq n' (notation_of_prim_token n)) + need_delim in + if not hidden then n,k else + match (String.Map.find sc !scope_map).delimiters with + | Some k -> n,Some k + | None -> raise Not_found + in + let scopes = make_current_scopes local_scopes in + try find_uninterpretation [] l find scopes + with Not_found -> match l with (_,n,k)::_ -> n,k | [] -> raise Notation_ops.No_match + +let uninterp_prim_token_cases_pattern c local_scopes = + match glob_constr_of_closed_cases_pattern (Global.env()) c with + | exception Not_found -> raise Notation_ops.No_match + | na,c -> let (sc,n) = uninterp_prim_token c local_scopes in (na,sc,n) + (* Miscellaneous *) let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 diff --git a/interp/notation.mli b/interp/notation.mli index 892eba8d11..842f2b1458 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -206,9 +206,9 @@ val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (GlobRef.t -> unit) -> raise [No_match] if no such token *) val uninterp_prim_token : - 'a glob_constr_g -> scope_name * prim_token + 'a glob_constr_g -> subscopes -> prim_token * delimiters option val uninterp_prim_token_cases_pattern : - 'a cases_pattern_g -> Name.t * scope_name * prim_token + 'a cases_pattern_g -> subscopes -> Name.t * prim_token * delimiters option val availability_of_prim_token : prim_token -> scope_name -> subscopes -> delimiters option option diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 3fa376a037..c4036e9677 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -52,6 +52,51 @@ type t = | Float64next_up | Float64next_down +let parse = function + | "int63_head0" -> Int63head0 + | "int63_tail0" -> Int63tail0 + | "int63_add" -> Int63add + | "int63_sub" -> Int63sub + | "int63_mul" -> Int63mul + | "int63_div" -> Int63div + | "int63_mod" -> Int63mod + | "int63_lsr" -> Int63lsr + | "int63_lsl" -> Int63lsl + | "int63_land" -> Int63land + | "int63_lor" -> Int63lor + | "int63_lxor" -> Int63lxor + | "int63_addc" -> Int63addc + | "int63_subc" -> Int63subc + | "int63_addcarryc" -> Int63addCarryC + | "int63_subcarryc" -> Int63subCarryC + | "int63_mulc" -> Int63mulc + | "int63_diveucl" -> Int63diveucl + | "int63_div21" -> Int63div21 + | "int63_addmuldiv" -> Int63addMulDiv + | "int63_eq" -> Int63eq + | "int63_lt" -> Int63lt + | "int63_le" -> Int63le + | "int63_compare" -> Int63compare + | "float64_opp" -> Float64opp + | "float64_abs" -> Float64abs + | "float64_eq" -> Float64eq + | "float64_lt" -> Float64lt + | "float64_le" -> Float64le + | "float64_compare" -> Float64compare + | "float64_classify" -> Float64classify + | "float64_add" -> Float64add + | "float64_sub" -> Float64sub + | "float64_mul" -> Float64mul + | "float64_div" -> Float64div + | "float64_sqrt" -> Float64sqrt + | "float64_of_int63" -> Float64ofInt63 + | "float64_normfr_mantissa" -> Float64normfr_mantissa + | "float64_frshiftexp" -> Float64frshiftexp + | "float64_ldshiftexp" -> Float64ldshiftexp + | "float64_next_up" -> Float64next_up + | "float64_next_down" -> Float64next_down + | _ -> raise Not_found + let equal (p1 : t) (p2 : t) = p1 == p2 @@ -229,3 +274,17 @@ let prim_type_to_string = function let op_or_type_to_string = function | OT_op op -> to_string op | OT_type t -> prim_type_to_string t + +let prim_type_of_string = function + | "int63_type" -> PT_int63 + | "float64_type" -> PT_float64 + | _ -> raise Not_found + +let op_or_type_of_string s = + try OT_type (prim_type_of_string s) + with Not_found -> OT_op (parse s) + +let parse_op_or_type ?loc s = + try op_or_type_of_string s + with Not_found -> + CErrors.user_err ?loc Pp.(str ("Built-in #"^s^" does not exist.")) diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 2a0399f1f7..a5db51111f 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -52,6 +52,10 @@ type t = | Float64next_up | Float64next_down +(** Can raise [Not_found]. + Beware that this is not exactly the reverse of [to_string] below. *) +val parse : string -> t + val equal : t -> t -> bool type arg_kind = @@ -75,6 +79,10 @@ type prim_type = | PT_int63 | PT_float64 +(** Can raise [Not_found] *) +val prim_type_of_string : string -> prim_type +val prim_type_to_string : prim_type -> string + type 'a prim_ind = | PIT_bool : unit prim_ind | PIT_carry : prim_type prim_ind @@ -90,8 +98,13 @@ type op_or_type = | OT_type of prim_type val prim_ind_to_string : 'a prim_ind -> string + +(** Can raise [Not_found] *) +val op_or_type_of_string : string -> op_or_type val op_or_type_to_string : op_or_type -> string +val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type + type ind_or_type = | PITT_ind : 'a prim_ind * 'a -> ind_or_type | PITT_type : prim_type -> ind_or_type diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index c53dcc7edd..608155eb71 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -218,7 +218,7 @@ let build_functional_principle (sigma : Evd.evar_map) old_princ_type sorts funs Declare.build_by_tactic env ~uctx ~poly:false ~typ ftac in (* uctx was ignored before *) - let hook = DeclareDef.Hook.make (hook new_principle_type) in + let hook = Declare.Hook.make (hook new_principle_type) in (body, typ, univs, hook, sigma) let change_property_sort evd toSort princ princName = @@ -318,8 +318,8 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts let uctx = Evd.evar_universe_context sigma in let entry = Declare.definition_entry ~univs ?types body in let (_ : Names.GlobRef.t) = - DeclareDef.declare_entry ~name:new_princ_name ~hook - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + Declare.declare_entry ~name:new_princ_name ~hook + ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~kind:Decls.(IsProof Theorem) ~impargs:[] ~uctx entry in @@ -400,7 +400,7 @@ let register_struct is_rec fixpoint_exprl = Pp.(str "Body of Function must be given") in ComDefinition.do_definition ~name:fname.CAst.v ~poly:false - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~kind:Decls.Definition univs binders None body (Some rtype); let evd, rev_pconstants = List.fold_left @@ -419,7 +419,7 @@ let register_struct is_rec fixpoint_exprl = (None, evd, List.rev rev_pconstants) | _ -> ComFixpoint.do_fixpoint - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false + ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl; let evd, rev_pconstants = List.fold_left diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ffb9a7e69b..5c82ed38bb 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1483,7 +1483,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name let lemma = build_proof env (Evd.from_env env) start_tac end_tac in Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None in - let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in + let info = Lemmas.Info.make ~hook:(Declare.Hook.make hook) () in let lemma = Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type in @@ -1721,7 +1721,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) - let hook {DeclareDef.Hook.S.uctx; _} = + let hook {Declare.Hook.S.uctx; _} = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name Decls.(IsProof Lemma) arg_types term_ref @@ -1767,5 +1767,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls functional_ref (EConstr.of_constr rec_arg_type) relation rec_arg_num term_id using_lemmas (List.length res_vars) evd - (DeclareDef.Hook.make hook)) + (Declare.Hook.make hook)) () diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 5baa23b3e9..aef5f645f4 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -342,7 +342,7 @@ GRAMMAR EXTEND Gram hint: [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; tac = Pltac.tactic -> - { ComHints.HintsExtern (n,c, in_tac tac) } ] ] + { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ] ; operconstr: LEVEL "0" [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3834b21a14..3b8fb48eb0 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1894,10 +1894,10 @@ let declare_projection name instance_id r = in it_mkProd_or_LetIn ccl ctx in let types = Some (it_mkProd_or_LetIn typ ctx) in - let kind, opaque, scope = Decls.(IsDefinition Definition), false, DeclareDef.Global Declare.ImportDefaultBehavior in + let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in let _r : GlobRef.t = - DeclareDef.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma + Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma in () let build_morphism_signature env sigma m = @@ -1961,10 +1961,10 @@ let add_morphism_as_parameter atts m n : unit = let env = Global.env () in let evd = Evd.from_env env in let poly = atts.polymorphic in - let kind, opaque, scope = Decls.(IsAssumption Logical), false, DeclareDef.Global Declare.ImportDefaultBehavior in + let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in let impargs, udecl = [], UState.default_univ_decl in let evd, types = build_morphism_signature env evd m in - let evd, pe = DeclareDef.prepare_parameter ~poly ~udecl ~types evd in + let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in let cst = GlobRef.ConstRef cst in Classes.add_instance @@ -1981,7 +1981,7 @@ let add_morphism_interactive atts m n : Lemmas.t = let poly = atts.polymorphic in let kind = Decls.(IsDefinition Instance) in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in - let hook { DeclareDef.Hook.S.dref; _ } = dref |> function + let hook { Declare.Hook.S.dref; _ } = dref |> function | GlobRef.ConstRef cst -> Classes.add_instance (Classes.mk_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info @@ -1989,7 +1989,7 @@ let add_morphism_interactive atts m n : Lemmas.t = declare_projection n instance_id (GlobRef.ConstRef cst) | _ -> assert false in - let hook = DeclareDef.Hook.make hook in + let hook = Declare.Hook.make hook in let info = Lemmas.Info.make ~hook ~kind () in Flags.silently (fun () -> diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 9910796d9c..e6c59f446d 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -683,6 +683,111 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign = Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign); Mltop.declare_cache_obj obj plugin_name +type (_, 'a) ml_ty_sig = +| MLTyNil : ('a, 'a) ml_ty_sig +| MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig + +let rec ml_sig_len : type r a. (r, a) ml_ty_sig -> int = function +| MLTyNil -> 0 +| MLTyArg sign -> 1 + ml_sig_len sign + +let rec cast_ml : type r a. (r, a) ml_ty_sig -> r -> Geninterp.Val.t list -> a = + fun sign f -> + match sign with + | MLTyNil -> + begin function + | [] -> f + | _ :: _ -> CErrors.anomaly (str "Arity mismatch") + end + | MLTyArg sign -> + function + | [] -> CErrors.anomaly (str "Arity mismatch") + | arg :: args -> cast_ml sign (f arg) args + +let ml_tactic_extend ~plugin ~name ~local ?deprecation sign tac = + let open Tacexpr in + let tac args _ = cast_ml sign tac args in + let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in + let ml = { mltac_name = ml_tactic_name; mltac_index = 0 } in + let len = ml_sig_len sign in + let args = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in + let vars = List.map (fun id -> Name id) args in + let args = List.map (fun id -> Reference (Locus.ArgVar (CAst.make id))) args in + let body = Tacexpr.TacFun (vars, Tacexpr.TacML (CAst.make (ml, args))) in + let id = Names.Id.of_string name in + let obj () = Tacenv.register_ltac true local id body ?deprecation in + let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in + Mltop.declare_cache_obj obj plugin + +module MLName = +struct + open Tacexpr + type t = ml_tactic_name + let compare tac1 tac2 = + let c = String.compare tac1.mltac_tactic tac2.mltac_tactic in + if c = 0 then String.compare tac1.mltac_plugin tac2.mltac_plugin + else c +end + +module MLTacMap = Map.Make(MLName) + +let ml_table : (Geninterp.Val.t list -> Geninterp.Val.t Ftactic.t) MLTacMap.t ref = ref MLTacMap.empty + +type ml_ltac_val = { + tacval_tac : Tacexpr.ml_tactic_name; + tacval_var : Id.t list; +} + +let in_tacval = +(* This is a hack to emulate value-returning ML-implemented tactics in Ltac. + We use a dummy generic argument to work around the limitations of the Ltac + runtime. Indeed, the TacML node needs to return unit values, since it is + considered a "tactic" in the runtime. Changing it to allow arbitrary values + would require to toggle this status, and thus to make it a "value" node. + This would in turn create too much backwards incompatibility. Instead, we + piggy back on the TacGeneric node, which by construction is used to return + values. + + The trick is to represent a n-ary application of a ML function as a generic + argument. We store in the node the name of the tactic and its arity, while + giving canonical names to the bound variables of the closure. This trick is + already performed in several external developments for specific calls, we + make it here generic. The argument should not be used for other purposes, so + we only export the registering functions. + *) + let wit : (Empty.t, ml_ltac_val, Geninterp.Val.t) Genarg.genarg_type = + Genarg.create_arg "ltac:val" + in + (* No need to internalize this ever *) + let intern_fun _ e = Empty.abort e in + let subst_fun s v = v in + let () = Genintern.register_intern0 wit intern_fun in + let () = Genintern.register_subst0 wit subst_fun in + (* No need to register a value tag for it via register_val0 since we will + never access this genarg directly. *) + let interp_fun ist tac = + let args = List.map (fun id -> Id.Map.get id ist.Geninterp.lfun) tac.tacval_var in + let tac = MLTacMap.get tac.tacval_tac !ml_table in + tac args + in + let () = Geninterp.register_interp0 wit interp_fun in + (fun v -> Genarg.in_gen (Genarg.Glbwit wit) v) + + +let ml_val_tactic_extend ~plugin ~name ~local ?deprecation sign tac = + let open Tacexpr in + let tac args = cast_ml sign tac args in + let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in + let len = ml_sig_len sign in + let vars = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in + let body = TacGeneric (in_tacval { tacval_tac = ml_tactic_name; tacval_var = vars }) in + let vars = List.map (fun id -> Name id) vars in + let body = Tacexpr.TacFun (vars, Tacexpr.TacArg (CAst.make body)) in + let id = Names.Id.of_string name in + let obj () = Tacenv.register_ltac true local id body ?deprecation in + let () = assert (not @@ MLTacMap.mem ml_tactic_name !ml_table) in + let () = ml_table := MLTacMap.add ml_tactic_name tac !ml_table in + Mltop.declare_cache_obj obj plugin (** ARGUMENT EXTEND *) diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index ce38431a18..6ee3ce091b 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -69,6 +69,25 @@ val print_ltacs : unit -> unit val print_located_tactic : Libnames.qualid -> unit (** Display the absolute name of a tactic. *) +(** {5 Low-level registering of tactics} *) + +type (_, 'a) ml_ty_sig = +| MLTyNil : ('a, 'a) ml_ty_sig +| MLTyArg : ('r, 'a) ml_ty_sig -> (Geninterp.Val.t -> 'r, 'a) ml_ty_sig + +val ml_tactic_extend : plugin:string -> name:string -> local:locality_flag -> + ?deprecation:Deprecation.t -> ('r, unit Proofview.tactic) ml_ty_sig -> 'r -> unit +(** Helper function to define directly an Ltac function in OCaml without any + associated parsing rule nor further shenanigans. The Ltac function will be + defined as [name] in the Coq file that loads the ML plugin where this + function is called. It will have the arity given by the [ml_ty_sig] + argument. *) + +val ml_val_tactic_extend : plugin:string -> name:string -> local:locality_flag -> + ?deprecation:Deprecation.t -> ('r, Geninterp.Val.t Ftactic.t) ml_ty_sig -> 'r -> unit +(** Same as {!ml_tactic_extend} but the function can return an argument + instead. *) + (** {5 TACTIC EXTEND} *) type _ ty_sig = diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index dda7f0742c..6debc7d9b9 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1895,8 +1895,7 @@ module Value = struct let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in of_tacvalue closure - (** Apply toplevel tactic values *) - let apply (f : value) (args: value list) = + let apply_expr f args = let fold arg (i, vars, lfun) = let id = Id.of_string ("x" ^ string_of_int i) in let x = Reference (ArgVar CAst.(make id)) in @@ -1905,9 +1904,18 @@ module Value = struct let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in let lfun = Id.Map.add (Id.of_string "F") f lfun in let ist = { (default_ist ()) with lfun = lfun; } in - let tac = TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in + ist, TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) + + + (** Apply toplevel tactic values *) + let apply (f : value) (args: value list) = + let ist, tac = apply_expr f args in eval_tactic_ist ist tac + let apply_val (f : value) (args: value list) = + let ist, tac = apply_expr f args in + val_interp ist tac + end (* globalization + interpretation *) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index ce34356a37..cbb17bf0fa 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -29,6 +29,7 @@ sig val of_closure : Geninterp.interp_sign -> glob_tactic_expr -> t val cast : 'a typed_abstract_argument_type -> Geninterp.Val.t -> 'a val apply : t -> t list -> unit Proofview.tactic + val apply_val : t -> t list -> t Ftactic.t end (** Values for interpretation *) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 7e4c4ce5c6..ee2c87d19a 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -128,249 +128,142 @@ let selecti s m = *) module M = struct (** - * Location of the Coq libraries. - *) - - let logic_dir = ["Coq"; "Logic"; "Decidable"] - - let mic_modules = - [ ["Coq"; "Lists"; "List"] - ; ["Coq"; "micromega"; "ZMicromega"] - ; ["Coq"; "micromega"; "Tauto"] - ; ["Coq"; "micromega"; "DeclConstant"] - ; ["Coq"; "micromega"; "RingMicromega"] - ; ["Coq"; "micromega"; "EnvRing"] - ; ["Coq"; "micromega"; "ZMicromega"] - ; ["Coq"; "micromega"; "RMicromega"] - ; ["Coq"; "micromega"; "Tauto"] - ; ["Coq"; "micromega"; "RingMicromega"] - ; ["Coq"; "micromega"; "EnvRing"] - ; ["Coq"; "QArith"; "QArith_base"] - ; ["Coq"; "Reals"; "Rdefinitions"] - ; ["Coq"; "Reals"; "Rpow_def"] - ; ["LRing_normalise"] ] - - [@@@ocaml.warning "-3"] - - let coq_modules = - Coqlib.( - init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules - @ mic_modules) - - let bin_module = [["Coq"; "Numbers"; "BinNums"]] - - let r_modules = - [ ["Coq"; "Reals"; "Rdefinitions"] - ; ["Coq"; "Reals"; "Rpow_def"] - ; ["Coq"; "Reals"; "Raxioms"] - ; ["Coq"; "QArith"; "Qreals"] ] - - let z_modules = [["Coq"; "ZArith"; "BinInt"]] - - (** * Initialization : a large amount of Caml symbols are derived from * ZMicromega.v *) - let gen_constant_in_modules s m n = + let constr_of_ref str = EConstr.of_constr - ( UnivGen.constr_of_monomorphic_global - @@ Coqlib.gen_reference_in_modules s m n ) - - let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules - - [@@@ocaml.warning "+3"] - - let constant = gen_constant_in_modules "ZMicromega" coq_modules - let bin_constant = gen_constant_in_modules "ZMicromega" bin_module - let r_constant = gen_constant_in_modules "ZMicromega" r_modules - let z_constant = gen_constant_in_modules "ZMicromega" z_modules - let m_constant = gen_constant_in_modules "ZMicromega" mic_modules - let coq_and = lazy (init_constant "and") - let coq_or = lazy (init_constant "or") - let coq_not = lazy (init_constant "not") - let coq_iff = lazy (init_constant "iff") - let coq_True = lazy (init_constant "True") - let coq_False = lazy (init_constant "False") - let coq_cons = lazy (constant "cons") - let coq_nil = lazy (constant "nil") - let coq_list = lazy (constant "list") - let coq_O = lazy (init_constant "O") - let coq_S = lazy (init_constant "S") - let coq_nat = lazy (init_constant "nat") - let coq_unit = lazy (init_constant "unit") + (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref str)) + + let coq_and = lazy (constr_of_ref "core.and.type") + let coq_or = lazy (constr_of_ref "core.or.type") + let coq_not = lazy (constr_of_ref "core.not.type") + let coq_iff = lazy (constr_of_ref "core.iff.type") + let coq_True = lazy (constr_of_ref "core.True.type") + let coq_False = lazy (constr_of_ref "core.False.type") + let coq_cons = lazy (constr_of_ref "core.list.cons") + let coq_nil = lazy (constr_of_ref "core.list.nil") + let coq_list = lazy (constr_of_ref "core.list.type") + let coq_O = lazy (constr_of_ref "num.nat.O") + let coq_S = lazy (constr_of_ref "num.nat.S") + let coq_nat = lazy (constr_of_ref "num.nat.type") + let coq_unit = lazy (constr_of_ref "core.unit.type") (* let coq_option = lazy (init_constant "option")*) - let coq_None = lazy (init_constant "None") - let coq_tt = lazy (init_constant "tt") - let coq_Inl = lazy (init_constant "inl") - let coq_Inr = lazy (init_constant "inr") - let coq_N0 = lazy (bin_constant "N0") - let coq_Npos = lazy (bin_constant "Npos") - let coq_xH = lazy (bin_constant "xH") - let coq_xO = lazy (bin_constant "xO") - let coq_xI = lazy (bin_constant "xI") - let coq_Z = lazy (bin_constant "Z") - let coq_ZERO = lazy (bin_constant "Z0") - let coq_POS = lazy (bin_constant "Zpos") - let coq_NEG = lazy (bin_constant "Zneg") - let coq_Q = lazy (constant "Q") - let coq_R = lazy (constant "R") - let coq_Qmake = lazy (constant "Qmake") - let coq_Rcst = lazy (constant "Rcst") - let coq_C0 = lazy (m_constant "C0") - let coq_C1 = lazy (m_constant "C1") - let coq_CQ = lazy (m_constant "CQ") - let coq_CZ = lazy (m_constant "CZ") - let coq_CPlus = lazy (m_constant "CPlus") - let coq_CMinus = lazy (m_constant "CMinus") - let coq_CMult = lazy (m_constant "CMult") - let coq_CPow = lazy (m_constant "CPow") - let coq_CInv = lazy (m_constant "CInv") - let coq_COpp = lazy (m_constant "COpp") - let coq_R0 = lazy (constant "R0") - let coq_R1 = lazy (constant "R1") - let coq_proofTerm = lazy (constant "ZArithProof") - let coq_doneProof = lazy (constant "DoneProof") - let coq_ratProof = lazy (constant "RatProof") - let coq_cutProof = lazy (constant "CutProof") - let coq_enumProof = lazy (constant "EnumProof") - let coq_ExProof = lazy (constant "ExProof") - let coq_Zgt = lazy (z_constant "Z.gt") - let coq_Zge = lazy (z_constant "Z.ge") - let coq_Zle = lazy (z_constant "Z.le") - let coq_Zlt = lazy (z_constant "Z.lt") - let coq_Eq = lazy (init_constant "eq") - let coq_Zplus = lazy (z_constant "Z.add") - let coq_Zminus = lazy (z_constant "Z.sub") - let coq_Zopp = lazy (z_constant "Z.opp") - let coq_Zmult = lazy (z_constant "Z.mul") - let coq_Zpower = lazy (z_constant "Z.pow") - let coq_Qle = lazy (constant "Qle") - let coq_Qlt = lazy (constant "Qlt") - let coq_Qeq = lazy (constant "Qeq") - let coq_Qplus = lazy (constant "Qplus") - let coq_Qminus = lazy (constant "Qminus") - let coq_Qopp = lazy (constant "Qopp") - let coq_Qmult = lazy (constant "Qmult") - let coq_Qpower = lazy (constant "Qpower") - let coq_Rgt = lazy (r_constant "Rgt") - let coq_Rge = lazy (r_constant "Rge") - let coq_Rle = lazy (r_constant "Rle") - let coq_Rlt = lazy (r_constant "Rlt") - let coq_Rplus = lazy (r_constant "Rplus") - let coq_Rminus = lazy (r_constant "Rminus") - let coq_Ropp = lazy (r_constant "Ropp") - let coq_Rmult = lazy (r_constant "Rmult") - let coq_Rinv = lazy (r_constant "Rinv") - let coq_Rpower = lazy (r_constant "pow") - let coq_powerZR = lazy (r_constant "powerRZ") - let coq_IZR = lazy (r_constant "IZR") - let coq_IQR = lazy (r_constant "Q2R") - let coq_PEX = lazy (constant "PEX") - let coq_PEc = lazy (constant "PEc") - let coq_PEadd = lazy (constant "PEadd") - let coq_PEopp = lazy (constant "PEopp") - let coq_PEmul = lazy (constant "PEmul") - let coq_PEsub = lazy (constant "PEsub") - let coq_PEpow = lazy (constant "PEpow") - let coq_PX = lazy (constant "PX") - let coq_Pc = lazy (constant "Pc") - let coq_Pinj = lazy (constant "Pinj") - let coq_OpEq = lazy (constant "OpEq") - let coq_OpNEq = lazy (constant "OpNEq") - let coq_OpLe = lazy (constant "OpLe") - let coq_OpLt = lazy (constant "OpLt") - let coq_OpGe = lazy (constant "OpGe") - let coq_OpGt = lazy (constant "OpGt") - let coq_PsatzIn = lazy (constant "PsatzIn") - let coq_PsatzSquare = lazy (constant "PsatzSquare") - let coq_PsatzMulE = lazy (constant "PsatzMulE") - let coq_PsatzMultC = lazy (constant "PsatzMulC") - let coq_PsatzAdd = lazy (constant "PsatzAdd") - let coq_PsatzC = lazy (constant "PsatzC") - let coq_PsatzZ = lazy (constant "PsatzZ") + let coq_None = lazy (constr_of_ref "core.option.None") + let coq_tt = lazy (constr_of_ref "core.unit.tt") + let coq_Inl = lazy (constr_of_ref "core.sum.inl") + let coq_Inr = lazy (constr_of_ref "core.sum.inr") + let coq_N0 = lazy (constr_of_ref "num.N.N0") + let coq_Npos = lazy (constr_of_ref "num.N.Npos") + let coq_xH = lazy (constr_of_ref "num.pos.xH") + let coq_xO = lazy (constr_of_ref "num.pos.xO") + let coq_xI = lazy (constr_of_ref "num.pos.xI") + let coq_Z = lazy (constr_of_ref "num.Z.type") + let coq_ZERO = lazy (constr_of_ref "num.Z.Z0") + let coq_POS = lazy (constr_of_ref "num.Z.Zpos") + let coq_NEG = lazy (constr_of_ref "num.Z.Zneg") + let coq_Q = lazy (constr_of_ref "rat.Q.type") + let coq_Qmake = lazy (constr_of_ref "rat.Q.Qmake") + let coq_R = lazy (constr_of_ref "reals.R.type") + let coq_Rcst = lazy (constr_of_ref "micromega.Rcst.type") + let coq_C0 = lazy (constr_of_ref "micromega.Rcst.C0") + let coq_C1 = lazy (constr_of_ref "micromega.Rcst.C1") + let coq_CQ = lazy (constr_of_ref "micromega.Rcst.CQ") + let coq_CZ = lazy (constr_of_ref "micromega.Rcst.CZ") + let coq_CPlus = lazy (constr_of_ref "micromega.Rcst.CPlus") + let coq_CMinus = lazy (constr_of_ref "micromega.Rcst.CMinus") + let coq_CMult = lazy (constr_of_ref "micromega.Rcst.CMult") + let coq_CPow = lazy (constr_of_ref "micromega.Rcst.CPow") + let coq_CInv = lazy (constr_of_ref "micromega.Rcst.CInv") + let coq_COpp = lazy (constr_of_ref "micromega.Rcst.COpp") + let coq_R0 = lazy (constr_of_ref "reals.R.R0") + let coq_R1 = lazy (constr_of_ref "reals.R.R1") + let coq_proofTerm = lazy (constr_of_ref "micromega.ZArithProof.type") + let coq_doneProof = lazy (constr_of_ref "micromega.ZArithProof.DoneProof") + let coq_ratProof = lazy (constr_of_ref "micromega.ZArithProof.RatProof") + let coq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof") + let coq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof") + let coq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof") + let coq_Zgt = lazy (constr_of_ref "num.Z.gt") + let coq_Zge = lazy (constr_of_ref "num.Z.ge") + let coq_Zle = lazy (constr_of_ref "num.Z.le") + let coq_Zlt = lazy (constr_of_ref "num.Z.lt") + let coq_Eq = lazy (constr_of_ref "core.eq.type") + let coq_Zplus = lazy (constr_of_ref "num.Z.add") + let coq_Zminus = lazy (constr_of_ref "num.Z.sub") + let coq_Zopp = lazy (constr_of_ref "num.Z.opp") + let coq_Zmult = lazy (constr_of_ref "num.Z.mul") + let coq_Zpower = lazy (constr_of_ref "num.Z.pow") + let coq_Qle = lazy (constr_of_ref "rat.Q.Qle") + let coq_Qlt = lazy (constr_of_ref "rat.Q.Qlt") + let coq_Qeq = lazy (constr_of_ref "rat.Q.Qeq") + let coq_Qplus = lazy (constr_of_ref "rat.Q.Qplus") + let coq_Qminus = lazy (constr_of_ref "rat.Q.Qminus") + let coq_Qopp = lazy (constr_of_ref "rat.Q.Qopp") + let coq_Qmult = lazy (constr_of_ref "rat.Q.Qmult") + let coq_Qpower = lazy (constr_of_ref "rat.Q.Qpower") + let coq_Rgt = lazy (constr_of_ref "reals.R.Rgt") + let coq_Rge = lazy (constr_of_ref "reals.R.Rge") + let coq_Rle = lazy (constr_of_ref "reals.R.Rle") + let coq_Rlt = lazy (constr_of_ref "reals.R.Rlt") + let coq_Rplus = lazy (constr_of_ref "reals.R.Rplus") + let coq_Rminus = lazy (constr_of_ref "reals.R.Rminus") + let coq_Ropp = lazy (constr_of_ref "reals.R.Ropp") + let coq_Rmult = lazy (constr_of_ref "reals.R.Rmult") + let coq_Rinv = lazy (constr_of_ref "reals.R.Rinv") + let coq_Rpower = lazy (constr_of_ref "reals.R.pow") + let coq_powerZR = lazy (constr_of_ref "reals.R.powerRZ") + let coq_IZR = lazy (constr_of_ref "reals.R.IZR") + let coq_IQR = lazy (constr_of_ref "reals.R.Q2R") + let coq_PEX = lazy (constr_of_ref "micromega.PExpr.PEX") + let coq_PEc = lazy (constr_of_ref "micromega.PExpr.PEc") + let coq_PEadd = lazy (constr_of_ref "micromega.PExpr.PEadd") + let coq_PEopp = lazy (constr_of_ref "micromega.PExpr.PEopp") + let coq_PEmul = lazy (constr_of_ref "micromega.PExpr.PEmul") + let coq_PEsub = lazy (constr_of_ref "micromega.PExpr.PEsub") + let coq_PEpow = lazy (constr_of_ref "micromega.PExpr.PEpow") + let coq_PX = lazy (constr_of_ref "micromega.Pol.PX") + let coq_Pc = lazy (constr_of_ref "micromega.Pol.Pc") + let coq_Pinj = lazy (constr_of_ref "micromega.Pol.Pinj") + let coq_OpEq = lazy (constr_of_ref "micromega.Op2.OpEq") + let coq_OpNEq = lazy (constr_of_ref "micromega.Op2.OpNEq") + let coq_OpLe = lazy (constr_of_ref "micromega.Op2.OpLe") + let coq_OpLt = lazy (constr_of_ref "micromega.Op2.OpLt") + let coq_OpGe = lazy (constr_of_ref "micromega.Op2.OpGe") + let coq_OpGt = lazy (constr_of_ref "micromega.Op2.OpGt") + let coq_PsatzIn = lazy (constr_of_ref "micromega.Psatz.PsatzIn") + let coq_PsatzSquare = lazy (constr_of_ref "micromega.Psatz.PsatzSquare") + let coq_PsatzMulE = lazy (constr_of_ref "micromega.Psatz.PsatzMulE") + let coq_PsatzMultC = lazy (constr_of_ref "micromega.Psatz.PsatzMulC") + let coq_PsatzAdd = lazy (constr_of_ref "micromega.Psatz.PsatzAdd") + let coq_PsatzC = lazy (constr_of_ref "micromega.Psatz.PsatzC") + let coq_PsatzZ = lazy (constr_of_ref "micromega.Psatz.PsatzZ") (* let coq_GT = lazy (m_constant "GT")*) - let coq_DeclaredConstant = lazy (m_constant "DeclaredConstant") - - let coq_TT = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "TT") - - let coq_FF = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "FF") - - let coq_And = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "Cj") + let coq_DeclaredConstant = + lazy (constr_of_ref "micromega.DeclaredConstant.type") - let coq_Or = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "D") - - let coq_Neg = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "N") - - let coq_Atom = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "A") - - let coq_X = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "X") - - let coq_Impl = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "I") - - let coq_Formula = - lazy - (gen_constant_in_modules "ZMicromega" - [["Coq"; "micromega"; "Tauto"]; ["Tauto"]] - "BFormula") + let coq_TT = lazy (constr_of_ref "micromega.GFormula.TT") + let coq_FF = lazy (constr_of_ref "micromega.GFormula.FF") + let coq_And = lazy (constr_of_ref "micromega.GFormula.Cj") + let coq_Or = lazy (constr_of_ref "micromega.GFormula.D") + let coq_Neg = lazy (constr_of_ref "micromega.GFormula.N") + let coq_Atom = lazy (constr_of_ref "micromega.GFormula.A") + let coq_X = lazy (constr_of_ref "micromega.GFormula.X") + let coq_Impl = lazy (constr_of_ref "micromega.GFormula.I") + let coq_Formula = lazy (constr_of_ref "micromega.BFormula.type") (** * Initialization : a few Caml symbols are derived from other libraries; * QMicromega, ZArithRing, RingMicromega. *) - let coq_QWitness = - lazy - (gen_constant_in_modules "QMicromega" - [["Coq"; "micromega"; "QMicromega"]] - "QWitness") - - let coq_Build = - lazy - (gen_constant_in_modules "RingMicromega" - [["Coq"; "micromega"; "RingMicromega"]; ["RingMicromega"]] - "Build_Formula") - - let coq_Cstr = - lazy - (gen_constant_in_modules "RingMicromega" - [["Coq"; "micromega"; "RingMicromega"]; ["RingMicromega"]] - "Formula") + let coq_QWitness = lazy (constr_of_ref "micromega.QWitness.type") + let coq_Build = lazy (constr_of_ref "micromega.Formula.Build_Formula") + let coq_Cstr = lazy (constr_of_ref "micromega.Formula.type") (** * Parsing and dumping : transformation functions between Caml and Coq @@ -1318,29 +1211,10 @@ end open M -let coq_Branch = - lazy - (gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "Branch") - -let coq_Elt = - lazy - (gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "Elt") - -let coq_Empty = - lazy - (gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "Empty") - -let coq_VarMap = - lazy - (gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "t") +let coq_Branch = lazy (constr_of_ref "micromega.VarMap.Branch") +let coq_Elt = lazy (constr_of_ref "micromega.VarMap.Elt") +let coq_Empty = lazy (constr_of_ref "micromega.VarMap.Empty") +let coq_VarMap = lazy (constr_of_ref "micromega.VarMap.type") let rec dump_varmap typ m = match m with @@ -1900,13 +1774,7 @@ let micromega_order_changer cert env ff = [ ( "__ff" , ff , EConstr.mkApp (Lazy.force coq_Formula, [|formula_typ|]) ) - ; ( "__varmap" - , vm - , EConstr.mkApp - ( gen_constant_in_modules "VarMap" - [["Coq"; "micromega"; "VarMap"]; ["VarMap"]] - "t" - , [|typ|] ) ) + ; ("__varmap", vm, EConstr.mkApp (Lazy.force coq_VarMap, [|typ|])) ; ("__wit", cert, cert_typ) ] (Tacmach.New.pf_concl gl)) (* Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)*) diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 0307728819..60af804c1b 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -349,8 +349,8 @@ let interp_index ist gl idx = begin match Tacinterp.Value.to_constr v with | Some c -> let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in - begin match Notation.uninterp_prim_token rc with - | _, Constrexpr.Numeral n when NumTok.Signed.is_int n -> + begin match Notation.uninterp_prim_token rc (None, []) with + | Constrexpr.Numeral n, _ when NumTok.Signed.is_int n -> int_of_string (NumTok.Signed.to_string n) | _ -> raise Not_found end diff --git a/test-suite/output/bug_12159.out b/test-suite/output/bug_12159.out new file mode 100644 index 0000000000..7f47c47e32 --- /dev/null +++ b/test-suite/output/bug_12159.out @@ -0,0 +1,28 @@ +f 1%B + : unit +f 0 + : unit +1%B + : unit +0 + : unit +1%B + : unit +1 + : unit +1 + : unit +0 + : unit +1 + : unit +0%A + : unit +1 + : unit +0%A + : unit +0 + : unit +0 + : unit diff --git a/test-suite/output/bug_12159.v b/test-suite/output/bug_12159.v new file mode 100644 index 0000000000..91d66f7f4c --- /dev/null +++ b/test-suite/output/bug_12159.v @@ -0,0 +1,39 @@ +Declare Scope A. +Declare Scope B. +Delimit Scope A with A. +Delimit Scope B with B. +Definition to_unit (v : Decimal.uint) : option unit + := match Nat.of_uint v with O => Some tt | _ => None end. +Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0. +Definition of_unit' (v : unit) : Decimal.uint := Nat.to_uint 1. +Numeral Notation unit to_unit of_unit : A. +Numeral Notation unit to_unit of_unit' : B. +Definition f x : unit := x. +Check f tt. +Arguments f x%A. +Check f tt. +Check tt. +Open Scope A. +Check tt. +Close Scope A. +Check tt. +Open Scope B. +Check tt. +Undelimit Scope B. +Check tt. +Open Scope A. +Check tt. +Close Scope A. +Check tt. +Close Scope B. +Check tt. +Open Scope B. +Check tt. +Notation "1" := true. +Check tt. +Open Scope A. +Check tt. +Declare Scope C. +Notation "0" := false : C. +Open Scope C. +Check tt. (* gives 0 but should now be 0%A *) diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 0f2717beef..9f77221d5a 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -26,6 +26,8 @@ Inductive Empty_set : Set :=. Inductive unit : Set := tt : unit. +Register unit as core.unit.type. +Register tt as core.unit.tt. (********************************************************************) (** * The boolean datatype *) @@ -198,6 +200,10 @@ Notation "x + y" := (sum x y) : type_scope. Arguments inl {A B} _ , [A] B _. Arguments inr {A B} _ , A [B] _. +Register sum as core.sum.type. +Register inl as core.sum.inl. +Register inr as core.sum.inr. + (** [prod A B], written [A * B], is the product of [A] and [B]; the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 638e8e8308..c3c69f46f3 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -517,18 +517,20 @@ Section Elts. exists (a::l1); exists l2; simpl; split; now f_equal. Qed. - Lemma nth_ext : forall l l' d, length l = length l' -> - (forall n, nth n l d = nth n l' d) -> l = l'. + Lemma nth_ext : forall l l' d d', length l = length l' -> + (forall n, n < length l -> nth n l d = nth n l' d') -> l = l'. Proof. - induction l; intros l' d Hlen Hnth; destruct l' as [| b l']. + induction l; intros l' d d' Hlen Hnth; destruct l' as [| b l']. - reflexivity. - inversion Hlen. - inversion Hlen. - change a with (nth 0 (a :: l) d). - change b with (nth 0 (b :: l') d). + change b with (nth 0 (b :: l') d'). rewrite Hnth; f_equal. - apply IHl with d; [ now inversion Hlen | ]. - intros n; apply (Hnth (S n)). + + apply IHl with d d'; [ now inversion Hlen | ]. + intros n Hlen'; apply (Hnth (S n)). + now simpl; apply lt_n_S. + + simpl; apply Nat.lt_0_succ. Qed. (** Results about [nth_error] *) @@ -2008,6 +2010,9 @@ Section SetIncl. now apply incl_cons_inv in Hin. Qed. + Lemma incl_filter f l : incl (filter f l) l. + Proof. intros x Hin; now apply filter_In in Hin. Qed. + Lemma remove_incl (eq_dec : forall x y : A, {x = y} + {x <> y}) : forall l1 l2 x, incl l1 l2 -> incl (remove eq_dec x l1) (remove eq_dec x l2). Proof. @@ -2018,8 +2023,15 @@ Section SetIncl. End SetIncl. +Lemma incl_map A B (f : A -> B) l1 l2 : incl l1 l2 -> incl (map f l1) (map f l2). +Proof. + intros Hincl x Hinx. + destruct (proj1 (in_map_iff _ _ _) Hinx) as [y [<- Hiny]]. + apply in_map; intuition. +Qed. + Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons - incl_app: datatypes. + incl_app incl_map: datatypes. (**************************************) @@ -2412,6 +2424,15 @@ Section ReDun. now apply Hnin, in_rev. Qed. + Lemma NoDup_filter f l : NoDup l -> NoDup (filter f l). + Proof. + induction l; simpl; intros Hnd; auto. + apply NoDup_cons_iff in Hnd. + destruct (f a); [ | intuition ]. + apply NoDup_cons_iff; split; intuition. + apply filter_In in H; intuition. + Qed. + (** Effective computation of a list without duplicates *) Hypothesis decA: forall x y : A, {x = y} + {x <> y}. @@ -2947,6 +2968,10 @@ Section Exists_Forall. now apply neg_Forall_Exists_neg. Defined. + Lemma incl_Forall_in_iff l l' : + incl l l' <-> Forall (fun x => In x l') l. + Proof. now rewrite Forall_forall; split. Qed. + End Exists_Forall. Hint Constructors Exists : core. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index b65cb294aa..2c112c3469 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -135,29 +135,29 @@ Register Inline subcarry. Definition addc_def x y := let r := x + y in if r < x then C1 r else C0 r. -(* the same but direct implementation for effeciancy *) +(* the same but direct implementation for efficiency *) Primitive addc := #int63_addc. Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope. Definition addcarryc_def x y := let r := addcarry x y in if r <= x then C1 r else C0 r. -(* the same but direct implementation for effeciancy *) +(* the same but direct implementation for efficiency *) Primitive addcarryc := #int63_addcarryc. Definition subc_def x y := if y <= x then C0 (x - y) else C1 (x - y). -(* the same but direct implementation for effeciancy *) +(* the same but direct implementation for efficiency *) Primitive subc := #int63_subc. Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope. Definition subcarryc_def x y := if y < x then C0 (x - y - 1) else C1 (x - y - 1). -(* the same but direct implementation for effeciancy *) +(* the same but direct implementation for efficiency *) Primitive subcarryc := #int63_subcarryc. Definition diveucl_def x y := (x/y, x\%y). -(* the same but direct implementation for effeciancy *) +(* the same but direct implementation for efficiency *) Primitive diveucl := #int63_diveucl. Primitive diveucl_21 := #int63_div21. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index bd5225d9ef..74cdd1797c 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -22,6 +22,10 @@ Declare Scope Q_scope. Delimit Scope Q_scope with Q. Bind Scope Q_scope with Q. Arguments Qmake _%Z _%positive. + +Register Q as rat.Q.type. +Register Qmake as rat.Q.Qmake. + Open Scope Q_scope. Ltac simpl_mult := rewrite ?Pos2Z.inj_mul. @@ -101,6 +105,10 @@ Notation "x > y" := (Qlt y x)(only parsing) : Q_scope. Notation "x >= y" := (Qle y x)(only parsing) : Q_scope. Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope. +Register Qeq as rat.Q.Qeq. +Register Qle as rat.Q.Qle. +Register Qlt as rat.Q.Qlt. + (** injection from Z is injective. *) Lemma inject_Z_injective (a b: Z): inject_Z a == inject_Z b <-> a = b. @@ -278,6 +286,11 @@ Infix "*" := Qmult : Q_scope. Notation "/ x" := (Qinv x) : Q_scope. Infix "/" := Qdiv : Q_scope. +Register Qplus as rat.Q.Qplus. +Register Qminus as rat.Q.Qminus. +Register Qopp as rat.Q.Qopp. +Register Qmult as rat.Q.Qmult. + (** A light notation for [Zpos] *) Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z (Zpos b). @@ -1053,6 +1066,8 @@ Definition Qpower (q:Q) (z:Z) := Notation " q ^ z " := (Qpower q z) : Q_scope. +Register Qpower as rat.Q.Qpower. + Instance Qpower_comp : Proper (Qeq==>eq==>Qeq) Qpower. Proof. intros x x' Hx y y' Hy. rewrite <- Hy; clear y' Hy. diff --git a/theories/Reals/Rregisternames.v b/theories/Reals/Rregisternames.v index f09edef600..8b078f2cf3 100644 --- a/theories/Reals/Rregisternames.v +++ b/theories/Reals/Rregisternames.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Reals. +Require Import Raxioms Rfunctions Qreals. (*****************************************************************) (** Register names for use in plugins *) @@ -18,6 +18,9 @@ Register R as reals.R.type. Register R0 as reals.R.R0. Register R1 as reals.R.R1. Register Rle as reals.R.Rle. +Register Rgt as reals.R.Rgt. +Register Rlt as reals.R.Rlt. +Register Rge as reals.R.Rge. Register Rplus as reals.R.Rplus. Register Ropp as reals.R.Ropp. Register Rminus as reals.R.Rminus. @@ -26,5 +29,6 @@ Register Rinv as reals.R.Rinv. Register Rdiv as reals.R.Rdiv. Register IZR as reals.R.IZR. Register Rabs as reals.R.Rabs. -Register sqrt as reals.R.sqrt. Register powerRZ as reals.R.powerRZ. +Register pow as reals.R.pow. +Register Qreals.Q2R as reals.R.Q2R. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 0b3656f586..78b26c83ea 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -44,6 +44,7 @@ Register succ as num.Z.succ. Register pred as num.Z.pred. Register sub as num.Z.sub. Register mul as num.Z.mul. +Register pow as num.Z.pow. Register of_nat as num.Z.of_nat. (** When including property functors, only inline t eq zero one two *) diff --git a/theories/micromega/DeclConstant.v b/theories/micromega/DeclConstant.v index bd8490d796..2e50481b13 100644 --- a/theories/micromega/DeclConstant.v +++ b/theories/micromega/DeclConstant.v @@ -35,6 +35,7 @@ Require Import List. (** Ground terms (see [GT] below) are built inductively from declared constants. *) Class DeclaredConstant {T : Type} (F : T). +Register DeclaredConstant as micromega.DeclaredConstant.type. Class GT {T : Type} (F : T). diff --git a/theories/micromega/EnvRing.v b/theories/micromega/EnvRing.v index 28c7e8c554..7bef11e89a 100644 --- a/theories/micromega/EnvRing.v +++ b/theories/micromega/EnvRing.v @@ -31,6 +31,14 @@ Inductive PExpr {C} : Type := | PEpow : PExpr -> N -> PExpr. Arguments PExpr : clear implicits. +Register PEc as micromega.PExpr.PEc. +Register PEX as micromega.PExpr.PEX. +Register PEadd as micromega.PExpr.PEadd. +Register PEsub as micromega.PExpr.PEsub. +Register PEmul as micromega.PExpr.PEmul. +Register PEopp as micromega.PExpr.PEopp. +Register PEpow as micromega.PExpr.PEpow. + (* Definition of multivariable polynomials with coefficients in C : Type [Pol] represents [X1 ... Xn]. The representation is Horner's where a [n] variable polynomial @@ -60,6 +68,10 @@ Inductive Pol {C} : Type := | PX : Pol -> positive -> Pol -> Pol. Arguments Pol : clear implicits. +Register Pc as micromega.Pol.Pc. +Register Pinj as micromega.Pol.Pinj. +Register PX as micromega.Pol.PX. + Section MakeRingPol. (* Ring elements *) diff --git a/theories/micromega/Lra.v b/theories/micromega/Lra.v index 22cef50e0d..5c8cece845 100644 --- a/theories/micromega/Lra.v +++ b/theories/micromega/Lra.v @@ -20,6 +20,7 @@ Require Import Rdefinitions. Require Import RingMicromega. Require Import VarMap. Require Coq.micromega.Tauto. +Require Import Rregisternames. Declare ML Module "micromega_plugin". Ltac rchange := diff --git a/theories/micromega/QMicromega.v b/theories/micromega/QMicromega.v index e28de1a620..1fbc5a648a 100644 --- a/theories/micromega/QMicromega.v +++ b/theories/micromega/QMicromega.v @@ -154,6 +154,9 @@ Qed. Definition QWitness := Psatz Q. +Register QWitness as micromega.QWitness.type. + + Definition QWeakChecker := check_normalised_formulas 0 1 Qplus Qmult Qeq_bool Qle_bool. Require Import List. diff --git a/theories/micromega/RMicromega.v b/theories/micromega/RMicromega.v index a67c273c7f..fd8903eac9 100644 --- a/theories/micromega/RMicromega.v +++ b/theories/micromega/RMicromega.v @@ -150,7 +150,17 @@ Inductive Rcst := | CInv (r : Rcst) | COpp (r : Rcst). - +Register Rcst as micromega.Rcst.type. +Register C0 as micromega.Rcst.C0. +Register C1 as micromega.Rcst.C1. +Register CQ as micromega.Rcst.CQ. +Register CZ as micromega.Rcst.CZ. +Register CPlus as micromega.Rcst.CPlus. +Register CMinus as micromega.Rcst.CMinus. +Register CMult as micromega.Rcst.CMult. +Register CPow as micromega.Rcst.CPow. +Register CInv as micromega.Rcst.CInv. +Register COpp as micromega.Rcst.COpp. Definition z_of_exp (z : Z + nat) := match z with diff --git a/theories/micromega/RingMicromega.v b/theories/micromega/RingMicromega.v index 04de9509ac..fb7fbcf80b 100644 --- a/theories/micromega/RingMicromega.v +++ b/theories/micromega/RingMicromega.v @@ -298,6 +298,15 @@ Inductive Psatz : Type := | PsatzC : C -> Psatz | PsatzZ : Psatz. +Register PsatzIn as micromega.Psatz.PsatzIn. +Register PsatzSquare as micromega.Psatz.PsatzSquare. +Register PsatzMulC as micromega.Psatz.PsatzMulC. +Register PsatzMulE as micromega.Psatz.PsatzMulE. +Register PsatzAdd as micromega.Psatz.PsatzAdd. +Register PsatzC as micromega.Psatz.PsatzC. +Register PsatzZ as micromega.Psatz.PsatzZ. + + (** Given a list [l] of NFormula and an extended polynomial expression [e], if [eval_Psatz l e] succeeds (= Some f) then [f] is a logic consequence of the conjunction of the formulae in l. @@ -672,6 +681,13 @@ Inductive Op2 : Set := (* binary relations *) | OpLt | OpGt. +Register OpEq as micromega.Op2.OpEq. +Register OpNEq as micromega.Op2.OpNEq. +Register OpLe as micromega.Op2.OpLe. +Register OpGe as micromega.Op2.OpGe. +Register OpLt as micromega.Op2.OpLt. +Register OpGt as micromega.Op2.OpGt. + Definition eval_op2 (o : Op2) : R -> R -> Prop := match o with | OpEq => req @@ -686,12 +702,15 @@ Definition eval_pexpr : PolEnv -> PExpr C -> R := PEeval rplus rtimes rminus ropp phi pow_phi rpow. #[universes(template)] -Record Formula (T:Type) : Type := { +Record Formula (T:Type) : Type := Build_Formula{ Flhs : PExpr T; Fop : Op2; Frhs : PExpr T }. +Register Formula as micromega.Formula.type. +Register Build_Formula as micromega.Formula.Build_Formula. + Definition eval_formula (env : PolEnv) (f : Formula C) : Prop := let (lhs, op, rhs) := f in (eval_op2 op) (eval_pexpr env lhs) (eval_pexpr env rhs). diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v index a3e3cc3e9d..6e89089355 100644 --- a/theories/micromega/Tauto.v +++ b/theories/micromega/Tauto.v @@ -37,6 +37,16 @@ Section S. | N : GFormula -> GFormula | I : GFormula -> option AF -> GFormula -> GFormula. + Register TT as micromega.GFormula.TT. + Register FF as micromega.GFormula.FF. + Register X as micromega.GFormula.X. + Register A as micromega.GFormula.A. + Register Cj as micromega.GFormula.Cj. + Register D as micromega.GFormula.D. + Register N as micromega.GFormula.N. + Register I as micromega.GFormula.I. + + Section MAPX. Variable F : TX -> TX. @@ -137,6 +147,8 @@ End S. (** Typical boolean formulae *) Definition BFormula (A : Type) := @GFormula A Prop unit unit. +Register BFormula as micromega.BFormula.type. + Section MAPATOMS. Context {TA TA':Type}. Context {TX : Type}. diff --git a/theories/micromega/VarMap.v b/theories/micromega/VarMap.v index c2472f6303..e28c27f400 100644 --- a/theories/micromega/VarMap.v +++ b/theories/micromega/VarMap.v @@ -33,6 +33,11 @@ Inductive t {A} : Type := | Branch : t -> A -> t -> t . Arguments t : clear implicits. +Register Branch as micromega.VarMap.Branch. +Register Elt as micromega.VarMap.Elt. +Register Empty as micromega.VarMap.Empty. +Register t as micromega.VarMap.type. + Section MakeVarMap. Variable A : Type. diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v index efb263faf3..bff9671fee 100644 --- a/theories/micromega/ZMicromega.v +++ b/theories/micromega/ZMicromega.v @@ -564,10 +564,14 @@ Inductive ZArithProof := . (*| SplitProof : PolC Z -> ZArithProof -> ZArithProof -> ZArithProof.*) +Register ZArithProof as micromega.ZArithProof.type. +Register DoneProof as micromega.ZArithProof.DoneProof. +Register RatProof as micromega.ZArithProof.RatProof. +Register CutProof as micromega.ZArithProof.CutProof. +Register EnumProof as micromega.ZArithProof.EnumProof. +Register ExProof as micromega.ZArithProof.ExProof. -(* n/d <= x -> d*x - n >= 0 *) - (* In order to compute the 'cut', we need to express a polynomial P as a * Q + b. - b is the constant diff --git a/vernac/classes.ml b/vernac/classes.ml index eb735b7cdf..55af2e1a7d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -313,8 +313,8 @@ let instance_hook info global ?hook cst = let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in - let scope = DeclareDef.Global Declare.ImportDefaultBehavior in - let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs + let scope = Declare.Global Declare.ImportDefaultBehavior in + let kn = Declare.declare_definition ~name ~kind ~scope ~impargs ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in instance_hook info global ?hook kn @@ -325,7 +325,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst in let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma, entry = DeclareDef.prepare_parameter ~poly sigma ~udecl ~types:termtype in + let sigma, entry = Declare.prepare_parameter ~poly sigma ~udecl ~types:termtype in let cst = Declare.declare_constant ~name ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); @@ -334,7 +334,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst instance_hook pri global cst let declare_instance_program env sigma ~global ~poly name pri impargs udecl term termtype = - let hook { DeclareDef.Hook.S.scope; dref; _ } = + let hook { Declare.Hook.S.scope; dref; _ } = let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in let pri = intern_info pri in let env = Global.env () in @@ -342,9 +342,9 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term declare_instance env sigma (Some pri) (not global) (GlobRef.ConstRef cst) in let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in - let hook = DeclareDef.Hook.make hook in + let hook = Declare.Hook.make hook in let uctx = Evd.evar_universe_context sigma in - let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in + let scope, kind = Declare.Global Declare.ImportDefaultBehavior, Decls.Instance in let _ : DeclareObl.progress = Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls in () @@ -357,7 +357,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in let kind = Decls.(IsDefinition Instance) in - let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in + let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in let info = Lemmas.Info.make ~hook ~kind () in (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails! This is due to a bug in proof_global :( *) diff --git a/vernac/classes.mli b/vernac/classes.mli index f410cddfef..1b6deb3b28 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -22,7 +22,7 @@ val declare_instance : ?warn:bool -> env -> Evd.evar_map -> Does nothing — or emit a “not-a-class” warning if the [warn] argument is set — when said type is not a registered type class. *) -val existing_instance : bool -> qualid -> ComHints.hint_info_expr option -> unit +val existing_instance : bool -> qualid -> Vernacexpr.hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) val new_instance_interactive @@ -34,7 +34,7 @@ val new_instance_interactive -> ?generalize:bool -> ?tac:unit Proofview.tactic -> ?hook:(GlobRef.t -> unit) - -> ComHints.hint_info_expr + -> Vernacexpr.hint_info_expr -> (bool * constr_expr) option -> Id.t * Lemmas.t @@ -47,7 +47,7 @@ val new_instance -> (bool * constr_expr) -> ?generalize:bool -> ?hook:(GlobRef.t -> unit) - -> ComHints.hint_info_expr + -> Vernacexpr.hint_info_expr -> Id.t val new_instance_program @@ -59,7 +59,7 @@ val new_instance_program -> (bool * constr_expr) option -> ?generalize:bool -> ?hook:(GlobRef.t -> unit) - -> ComHints.hint_info_expr + -> Vernacexpr.hint_info_expr -> Id.t val declare_new_instance @@ -69,7 +69,7 @@ val declare_new_instance -> ident_decl -> local_binder_expr list -> constr_expr - -> ComHints.hint_info_expr + -> Vernacexpr.hint_info_expr -> unit (** {6 Low level interface used by Add Morphism, do not use } *) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 776ffd6b9f..023d76ce3b 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -87,8 +87,7 @@ let context_set_of_entry = function | Monomorphic_entry uctx -> uctx let declare_assumptions ~poly ~scope ~kind univs nl l = - let open DeclareDef in - let () = match scope with + let () = let open Declare in match scope with | Discharge -> (* declare universes separately for variables *) DeclareUctx.declare_universe_context ~poly (context_set_of_entry (fst univs)) @@ -100,10 +99,10 @@ let declare_assumptions ~poly ~scope ~kind univs nl l = let univs,subst' = List.fold_left_map (fun univs id -> let refu = match scope with - | Discharge -> + | Declare.Discharge -> declare_variable is_coe ~kind typ imps Glob_term.Explicit id; GlobRef.VarRef id.CAst.v, Univ.Instance.empty - | Global local -> + | Declare.Global local -> declare_axiom is_coe ~local ~poly ~kind typ univs imps nl id in next_univs univs, (id.CAst.v, Constr.mkRef refu)) @@ -130,7 +129,7 @@ let process_assumptions_udecls ~scope l = udecl, id | (_, ([], _))::_ | [] -> assert false in - let open DeclareDef in + let open Declare in let () = match scope, udecl with | Discharge, Some _ -> let loc = first_id.CAst.loc in @@ -208,7 +207,7 @@ let context_insection sigma ~poly ctx = let uctx = Evd.evar_universe_context sigma in let kind = Decls.(IsDefinition Definition) in let _ : GlobRef.t = - DeclareDef.declare_entry ~name ~scope:DeclareDef.Discharge + Declare.declare_entry ~name ~scope:Declare.Discharge ~kind ~impargs:[] ~uctx entry in () diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 4b953c8869..989015a9f3 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -17,7 +17,7 @@ open Constrexpr val do_assumptions : program_mode:bool -> poly:bool - -> scope:DeclareDef.locality + -> scope:Declare.locality -> kind:Decls.assumption_object_kind -> Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml index 4a8e217fc1..d6be02245c 100644 --- a/vernac/comCoercion.ml +++ b/vernac/comCoercion.ml @@ -352,8 +352,8 @@ let try_add_new_identity_coercion id ~local ~poly ~source ~target = let try_add_new_coercion_with_source ref ~local ~poly ~source = try_add_new_coercion_core ref ~local poly (Some source) None false -let add_coercion_hook poly { DeclareDef.Hook.S.scope; dref; _ } = - let open DeclareDef in +let add_coercion_hook poly { Declare.Hook.S.scope; dref; _ } = + let open Declare in let local = match scope with | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *) | Global ImportNeedQualified -> true @@ -363,10 +363,10 @@ let add_coercion_hook poly { DeclareDef.Hook.S.scope; dref; _ } = let msg = Nametab.pr_global_env Id.Set.empty dref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg -let add_coercion_hook ~poly = DeclareDef.Hook.make (add_coercion_hook poly) +let add_coercion_hook ~poly = Declare.Hook.make (add_coercion_hook poly) -let add_subclass_hook ~poly { DeclareDef.Hook.S.scope; dref; _ } = - let open DeclareDef in +let add_subclass_hook ~poly { Declare.Hook.S.scope; dref; _ } = + let open Declare in let stre = match scope with | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *) | Global ImportNeedQualified -> true @@ -375,4 +375,4 @@ let add_subclass_hook ~poly { DeclareDef.Hook.S.scope; dref; _ } = let cl = class_of_global dref in try_add_new_coercion_subclass cl ~local:stre ~poly -let add_subclass_hook ~poly = DeclareDef.Hook.make (add_subclass_hook ~poly) +let add_subclass_hook ~poly = Declare.Hook.make (add_subclass_hook ~poly) diff --git a/vernac/comCoercion.mli b/vernac/comCoercion.mli index 3b44bdaf8a..dee693232f 100644 --- a/vernac/comCoercion.mli +++ b/vernac/comCoercion.mli @@ -46,8 +46,8 @@ val try_add_new_identity_coercion -> local:bool -> poly:bool -> source:cl_typ -> target:cl_typ -> unit -val add_coercion_hook : poly:bool -> DeclareDef.Hook.t +val add_coercion_hook : poly:bool -> Declare.Hook.t -val add_subclass_hook : poly:bool -> DeclareDef.Hook.t +val add_subclass_hook : poly:bool -> Declare.Hook.t val class_of_global : GlobRef.t -> cl_typ diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 66d5a4f7f5..95f3955309 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -117,7 +117,7 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = in let kind = Decls.IsDefinition kind in let _ : Names.GlobRef.t = - DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs + Declare.declare_definition ~name ~scope ~kind ?hook ~impargs ~opaque:false ~poly evd ~udecl ~types ~body in () @@ -126,7 +126,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let term, ty, uctx, obls = DeclareDef.prepare_obligation ~name ~poly ~body ~types ~udecl evd in + let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in let _ : DeclareObl.progress = Obligations.add_definition ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 337da22018..2e8fe16252 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -15,9 +15,9 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition - : ?hook:DeclareDef.Hook.t + : ?hook:Declare.Hook.t -> name:Id.t - -> scope:DeclareDef.locality + -> scope:Declare.locality -> poly:bool -> kind:Decls.definition_object_kind -> universe_decl_expr option @@ -28,9 +28,9 @@ val do_definition -> unit val do_definition_program - : ?hook:DeclareDef.Hook.t + : ?hook:Declare.Hook.t -> name:Id.t - -> scope:DeclareDef.locality + -> scope:Declare.locality -> poly:bool -> kind:Decls.definition_object_kind -> universe_decl_expr option diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index d3c1d2e767..80ca85e9a6 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -257,7 +257,7 @@ let build_recthms ~indexes fixnames fixtypes fiximps = in let thms = List.map3 (fun name typ (ctx,impargs,_) -> - { DeclareDef.Recthm.name + { Declare.Recthm.name ; typ ; args = List.map Context.Rel.Declaration.get_name ctx ; impargs}) @@ -284,7 +284,7 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in let fix_kind = Decls.IsDefinition fix_kind in let _ : GlobRef.t list = - DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx + Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration fixitems in diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index dcb61d38d9..62a9d10bae 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -16,16 +16,16 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint_interactive : - scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t + scope:Declare.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t val do_fixpoint : - scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit + scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint_interactive : - scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t + scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t val do_cofixpoint : - scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit + scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit (************************************************************************) (** Internal API *) diff --git a/vernac/comHints.ml b/vernac/comHints.ml index 5a48e9c16c..2fd6fe2b29 100644 --- a/vernac/comHints.ml +++ b/vernac/comHints.ml @@ -13,23 +13,6 @@ open Util (** (Partial) implementation of the [Hint] command; some more functionality still lives in tactics/hints.ml *) -type hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen - -type reference_or_constr = - | HintsReference of Libnames.qualid - | HintsConstr of Constrexpr.constr_expr - -type hints_expr = - | HintsResolve of (hint_info_expr * bool * reference_or_constr) list - | HintsResolveIFF of bool * Libnames.qualid list * int option - | HintsImmediate of reference_or_constr list - | HintsUnfold of Libnames.qualid list - | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool - | HintsMode of Libnames.qualid * Hints.hint_mode list - | HintsConstructors of Libnames.qualid list - | HintsExtern of - int * Constrexpr.constr_expr option * Genarg.raw_generic_argument - let project_hint ~poly pri l2r r = let open EConstr in let open Coqlib in @@ -108,6 +91,7 @@ let interp_hints ~poly h = let fr r = Tacred.evaluable_of_global_reference env (fref r) in let fi c = let open Hints in + let open Vernacexpr in match c with | HintsReference c -> let gr = Smartlocate.global_with_alias c in @@ -126,15 +110,14 @@ let interp_hints ~poly h = in (info, poly, b, path, gr) in - let ft = - let open Hints in - function + let open Hints in + let open Vernacexpr in + let ft = function | HintsVariables -> HintsVariables | HintsConstants -> HintsConstants | HintsReferences lhints -> HintsReferences (List.map fr lhints) in let fp = Constrintern.intern_constr_pattern (Global.env ()) in - let open Hints in match h with | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) | HintsResolveIFF (l2r, lc, n) -> diff --git a/vernac/comHints.mli b/vernac/comHints.mli index 77fbef5387..20894eecf1 100644 --- a/vernac/comHints.mli +++ b/vernac/comHints.mli @@ -8,22 +8,4 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Typeclasses - -type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen - -type reference_or_constr = - | HintsReference of Libnames.qualid - | HintsConstr of Constrexpr.constr_expr - -type hints_expr = - | HintsResolve of (hint_info_expr * bool * reference_or_constr) list - | HintsResolveIFF of bool * Libnames.qualid list * int option - | HintsImmediate of reference_or_constr list - | HintsUnfold of Libnames.qualid list - | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool - | HintsMode of Libnames.qualid * Hints.hint_mode list - | HintsConstructors of Libnames.qualid list - | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument - -val interp_hints : poly:bool -> hints_expr -> Hints.hints_entry +val interp_hints : poly:bool -> Vernacexpr.hints_expr -> Hints.hints_entry diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index bf38088f71..4e9e24b119 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -230,7 +230,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = let name = add_suffix recname "_func" in (* XXX: Mutating the evar_map in the hook! *) (* XXX: Likely the sigma is out of date when the hook is called .... *) - let hook sigma { DeclareDef.Hook.S.dref; _ } = + let hook sigma { Declare.Hook.S.dref; _ } = let sigma, h_body = Evarutil.new_global sigma dref in let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in let ty = it_mkProd_or_LetIn top_arity binders_rel in @@ -248,13 +248,13 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = hook, name, typ else let typ = it_mkProd_or_LetIn top_arity binders_rel in - let hook sigma { DeclareDef.Hook.S.dref; _ } = + let hook sigma { Declare.Hook.S.dref; _ } = if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false dref impls in hook, recname, typ in (* XXX: Capturing sigma here... bad bad *) - let hook = DeclareDef.Hook.make (hook sigma) in + let hook = Declare.Hook.make (hook sigma) in RetrieveObl.check_evars env sigma; let evars, _, evars_def, evars_typ = RetrieveObl.retrieve_obligations env recname sigma 0 def typ @@ -290,7 +290,7 @@ let do_program_recursive ~scope ~poly fixkind fixl = let evars, _, def, typ = RetrieveObl.retrieve_obligations env name evm (List.length rec_sign) def typ in - ({ DeclareDef.Recthm.name; typ; impargs; args = [] }, def, evars) + ({ Declare.Recthm.name; typ; impargs; args = [] }, def, evars) in let (fixnames,fixrs,fixdefs,fixtypes) = fix in let fiximps = List.map pi2 info in diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli index 6851c9f69e..8b1fa6c202 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -14,8 +14,8 @@ open Vernacexpr val do_fixpoint : (* When [false], assume guarded. *) - scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit + scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint : (* When [false], assume guarded. *) - scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit + scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit diff --git a/vernac/declare.ml b/vernac/declare.ml index f4636c5724..c3f95c5297 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -16,7 +16,7 @@ open Names open Safe_typing module NamedDecl = Context.Named.Declaration -type opacity_flag = Opaque | Transparent +type opacity_flag = Vernacexpr.opacity_flag = Opaque | Transparent type t = { endline_tactic : Genarg.glob_generic_argument option @@ -120,17 +120,6 @@ let get_open_goals ps = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + List.length shelf -(* object_kind , id *) -exception AlreadyDeclared of (string option * Id.t) - -let _ = CErrors.register_handler (function - | AlreadyDeclared (kind, id) -> - Some - (seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind - ; Id.print id; str " already exists."]) - | _ -> - None) - type import_status = ImportDefaultBehavior | ImportNeedQualified (** Declaration of constants and parameters *) @@ -267,7 +256,7 @@ type constant_obj = { let load_constant i ((sp,kn), obj) = if Nametab.exists_cci sp then - raise (AlreadyDeclared (None, Libnames.basename sp)); + raise (DeclareUniv.AlreadyDeclared (None, Libnames.basename sp)); let con = Global.constant_of_delta_kn kn in Nametab.push (Nametab.Until i) sp (GlobRef.ConstRef con); Dumpglob.add_constant_kind con obj.cst_kind @@ -287,7 +276,7 @@ let exists_name id = let check_exists id = if exists_name id then - raise (AlreadyDeclared (None, id)) + raise (DeclareUniv.AlreadyDeclared (None, id)) let cache_constant ((sp,kn), obj) = (* Invariant: the constant must exist in the logical environment *) @@ -495,6 +484,17 @@ let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = let () = register_constant kn kind local in kn +let get_cd_fix_exn = function + | DefinitionEntry de -> + Future.fix_exn_of de.proof_entry_body + | _ -> fun x -> x + +let declare_constant ?local ~name ~kind cd = + try declare_constant ?local ~name ~kind cd + with exn -> + let exn = Exninfo.capture exn in + Exninfo.iraise (get_cd_fix_exn cd exn) + let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de = let kn, eff = let de = @@ -537,7 +537,7 @@ let inVariable v = Libobject.Dyn.Easy.inj v objVariable let declare_variable ~name ~kind d = (* Variables are distinguished by only short names *) if Decls.variable_exists name then - raise (AlreadyDeclared (None, name)); + raise (DeclareUniv.AlreadyDeclared (None, name)); let impl,opaque = match d with (* Fails if not well-typed *) | SectionLocalAssum {typ;impl} -> @@ -620,8 +620,6 @@ module Internal = struct let set_opacity ~opaque entry = { entry with proof_entry_opaque = opaque } - let get_fix_exn entry = Future.fix_exn_of entry.proof_entry_body - let rec decompose len c t accu = let open Constr in let open Context.Rel.Declaration in @@ -877,3 +875,181 @@ let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme let _ = Abstract.declare_abstract := declare_abstract let declare_universe_context = DeclareUctx.declare_universe_context + +type locality = Discharge | Global of import_status + +(* Hooks naturally belong here as they apply to both definitions and lemmas *) +module Hook = struct + module S = struct + type t = + { uctx : UState.t + (** [ustate]: universe constraints obtained when the term was closed *) + ; obls : (Names.Id.t * Constr.t) list + (** [(n1,t1),...(nm,tm)]: association list between obligation + name and the corresponding defined term (might be a constant, + but also an arbitrary term in the Expand case of obligations) *) + ; scope : locality + (** [locality]: Locality of the original declaration *) + ; dref : Names.GlobRef.t + (** [ref]: identifier of the original declaration *) + } + end + + type t = (S.t -> unit) CEphemeron.key + + let make hook = CEphemeron.create hook + + let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook + +end + +(* Locality stuff *) +let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry = + let should_suggest = entry.proof_entry_opaque && + Option.is_empty entry.proof_entry_secctx in + let ubind = UState.universe_binders uctx in + let dref = match scope with + | Discharge -> + let () = declare_variable ~name ~kind (SectionLocalDef entry) in + if should_suggest then Proof_using.suggest_variable (Global.env ()) name; + Names.GlobRef.VarRef name + | Global local -> + let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in + let gr = Names.GlobRef.ConstRef kn in + if should_suggest then Proof_using.suggest_constant (Global.env ()) kn; + let () = DeclareUniv.declare_univ_binders gr ubind in + gr + in + let () = Impargs.maybe_declare_manual_implicits false dref impargs in + let () = definition_message name in + Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook; + dref + +let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = + match possible_indexes with + | Some possible_indexes -> + let env = Global.env() in + let indexes = Pretyping.search_guard env possible_indexes rec_declaration in + let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in + let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in + vars, fixdecls, Some indexes + | None -> + let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixitems in + let vars = Vars.universes_of_constr (List.hd fixdecls) in + vars, fixdecls, None + +module Recthm = struct + type t = + { name : Names.Id.t + (** Name of theorem *) + ; typ : Constr.t + (** Type of theorem *) + ; args : Names.Name.t list + (** Names to pre-introduce *) + ; impargs : Impargs.manual_implicits + (** Explicitily declared implicit arguments *) + } +end + +let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = + let vars, fixdecls, indexes = + mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in + let uctx, univs = + (* XXX: Obligations don't do this, this seems like a bug? *) + if restrict_ucontext + then + let uctx = UState.restrict uctx vars in + let univs = UState.check_univ_decl ~poly uctx udecl in + uctx, univs + else + let univs = UState.univ_entry ~poly uctx in + uctx, univs + in + let csts = CList.map2 + (fun Recthm.{ name; typ; impargs } body -> + let entry = definition_entry ~opaque ~types:typ ~univs body in + declare_entry ~name ~scope ~kind ~impargs ~uctx entry) + fixitems fixdecls + in + let isfix = Option.has_some possible_indexes in + let fixnames = List.map (fun { Recthm.name } -> name) fixitems in + recursive_message isfix indexes fixnames; + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; + csts + +let warn_let_as_axiom = + CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" + Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ + spc () ++ strbrk "declared as an axiom.") + +let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe = + let local = match scope with + | Discharge -> warn_let_as_axiom name; ImportNeedQualified + | Global local -> local + in + let kind = Decls.(IsAssumption Conjectural) in + let decl = ParameterEntry pe in + let kn = declare_constant ~name ~local ~kind decl in + let dref = Names.GlobRef.ConstRef kn in + let () = Impargs.maybe_declare_manual_implicits false dref impargs in + let () = assumption_message name in + let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in + let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in + dref + +let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = + try declare_assumption ~name ~scope ~hook ~impargs ~uctx pe + with exn -> + let exn = Exninfo.capture exn in + let exn = Option.cata (fun fix -> fix exn) exn fix_exn in + Exninfo.iraise exn + +(* Preparing proof entries *) + +let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma = + let env = Global.env () in + Pretyping.check_evars_are_solved ~program_mode:false env sigma; + let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true + sigma (fun nf -> nf body, Option.map nf types) + in + let univs = Evd.check_univ_decl ~poly sigma udecl in + let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in + let uctx = Evd.evar_universe_context sigma in + entry, uctx + +let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook + ?obls ~poly ?inline ~types ~body ?fix_exn sigma = + let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in + declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry + +let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = + let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false + sigma (fun nf -> nf body, Option.map nf types) + in + let univs = Evd.check_univ_decl ~poly sigma udecl in + let ce = definition_entry ?opaque ?inline ?types ~univs body in + let env = Global.env () in + let (c,ctx), sideff = Future.force ce.proof_entry_body in + assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private); + assert(Univ.ContextSet.is_empty ctx); + RetrieveObl.check_evars env sigma; + let c = EConstr.of_constr c in + let typ = match ce.proof_entry_type with + | Some t -> EConstr.of_constr t + | None -> Retyping.get_type_of env sigma c + in + let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in + let uctx = Evd.evar_universe_context sigma in + c, cty, uctx, obls + +let prepare_parameter ~poly ~udecl ~types sigma = + let env = Global.env () in + Pretyping.check_evars_are_solved ~program_mode:false env sigma; + let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:true + sigma (fun nf -> nf types) + in + let univs = Evd.check_univ_decl ~poly sigma udecl in + sigma, (None(*proof using*), (typ, univs), None(*inline*)) + +(* Compat: will remove *) +exception AlreadyDeclared = DeclareUniv.AlreadyDeclared diff --git a/vernac/declare.mli b/vernac/declare.mli index a297f25868..340c035d1d 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -69,7 +69,7 @@ module Proof : sig end -type opacity_flag = Opaque | Transparent +type opacity_flag = Vernacexpr.opacity_flag = Opaque | Transparent (** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of name [name] with goals [goals] (a list of pairs of environment and @@ -194,14 +194,9 @@ val inline_private_constants val definition_message : Id.t -> unit val assumption_message : Id.t -> unit val fixpoint_message : int array option -> Id.t list -> unit -val recursive_message : bool (** true = fixpoint *) -> - int array option -> Id.t list -> unit val check_exists : Id.t -> unit -(* Used outside this module only in indschemes *) -exception AlreadyDeclared of (string option * Id.t) - (** {6 For legacy support, do not use} *) module Internal : sig @@ -211,10 +206,6 @@ module Internal : sig (* Overriding opacity is indeed really hacky *) val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry - (* TODO: This is only used in DeclareDef to forward the fix to - hooks, should eventually go away *) - val get_fix_exn : 'a proof_entry -> Future.fix_exn - val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list type constant_obj @@ -282,3 +273,127 @@ val build_constant_by_tactic : val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit [@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"] + +type locality = Discharge | Global of import_status + +(** Declaration hooks *) +module Hook : sig + type t + + (** Hooks allow users of the API to perform arbitrary actions at + proof/definition saving time. For example, to register a constant + as a Coercion, perform some cleanup, update the search database, + etc... *) + module S : sig + type t = + { uctx : UState.t + (** [ustate]: universe constraints obtained when the term was closed *) + ; obls : (Id.t * Constr.t) list + (** [(n1,t1),...(nm,tm)]: association list between obligation + name and the corresponding defined term (might be a constant, + but also an arbitrary term in the Expand case of obligations) *) + ; scope : locality + (** [scope]: Locality of the original declaration *) + ; dref : GlobRef.t + (** [dref]: identifier of the original declaration *) + } + end + + val make : (S.t -> unit) -> t + val call : ?hook:t -> S.t -> unit +end + +(** Declare an interactively-defined constant *) +val declare_entry + : name:Id.t + -> scope:locality + -> kind:Decls.logical_kind + -> ?hook:Hook.t + -> ?obls:(Id.t * Constr.t) list + -> impargs:Impargs.manual_implicits + -> uctx:UState.t + -> Evd.side_effects proof_entry + -> GlobRef.t + +(** Declares a non-interactive constant; [body] and [types] will be + normalized w.r.t. the passed [evar_map] [sigma]. Universes should + be handled properly, including minimization and restriction. Note + that [sigma] is checked for unresolved evars, thus you should be + careful not to submit open terms or evar maps with stale, + unresolved existentials *) +val declare_definition + : name:Id.t + -> scope:locality + -> kind:Decls.logical_kind + -> opaque:bool + -> impargs:Impargs.manual_implicits + -> udecl:UState.universe_decl + -> ?hook:Hook.t + -> ?obls:(Id.t * Constr.t) list + -> poly:bool + -> ?inline:bool + -> types:EConstr.t option + -> body:EConstr.t + -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) + -> Evd.evar_map + -> GlobRef.t + +val declare_assumption + : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) + -> name:Id.t + -> scope:locality + -> hook:Hook.t option + -> impargs:Impargs.manual_implicits + -> uctx:UState.t + -> Entries.parameter_entry + -> GlobRef.t + +module Recthm : sig + type t = + { name : Id.t + (** Name of theorem *) + ; typ : Constr.t + (** Type of theorem *) + ; args : Name.t list + (** Names to pre-introduce *) + ; impargs : Impargs.manual_implicits + (** Explicitily declared implicit arguments *) + } +end + +val declare_mutually_recursive + : opaque:bool + -> scope:locality + -> kind:Decls.logical_kind + -> poly:bool + -> uctx:UState.t + -> udecl:UState.universe_decl + -> ntns:Vernacexpr.decl_notation list + -> rec_declaration:Constr.rec_declaration + -> possible_indexes:int list list option + -> ?restrict_ucontext:bool + (** XXX: restrict_ucontext should be always true, this seems like a + bug in obligations, so this parameter should go away *) + -> Recthm.t list + -> Names.GlobRef.t list + +val prepare_obligation + : ?opaque:bool + -> ?inline:bool + -> name:Id.t + -> poly:bool + -> udecl:UState.universe_decl + -> types:EConstr.t option + -> body:EConstr.t + -> Evd.evar_map + -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info + +val prepare_parameter + : poly:bool + -> udecl:UState.universe_decl + -> types:EConstr.types + -> Evd.evar_map + -> Evd.evar_map * Entries.parameter_entry + +(* Compat: will remove *) +exception AlreadyDeclared of (string option * Names.Id.t) diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 1809c2bc91..83bb1dae71 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -1,193 +1,9 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Declare - -type locality = Discharge | Global of Declare.import_status - -(* Hooks naturally belong here as they apply to both definitions and lemmas *) -module Hook = struct - module S = struct - type t = - { uctx : UState.t - (** [ustate]: universe constraints obtained when the term was closed *) - ; obls : (Names.Id.t * Constr.t) list - (** [(n1,t1),...(nm,tm)]: association list between obligation - name and the corresponding defined term (might be a constant, - but also an arbitrary term in the Expand case of obligations) *) - ; scope : locality - (** [locality]: Locality of the original declaration *) - ; dref : Names.GlobRef.t - (** [ref]: identifier of the original declaration *) - } - end - - type t = (S.t -> unit) CEphemeron.key - - let make hook = CEphemeron.create hook - - let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook - -end - -(* Locality stuff *) -let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry = - let should_suggest = entry.Declare.proof_entry_opaque && - Option.is_empty entry.Declare.proof_entry_secctx in - let ubind = UState.universe_binders uctx in - let dref = match scope with - | Discharge -> - let () = declare_variable ~name ~kind (SectionLocalDef entry) in - if should_suggest then Proof_using.suggest_variable (Global.env ()) name; - Names.GlobRef.VarRef name - | Global local -> - let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in - let gr = Names.GlobRef.ConstRef kn in - if should_suggest then Proof_using.suggest_constant (Global.env ()) kn; - let () = DeclareUniv.declare_univ_binders gr ubind in - gr - in - let () = Impargs.maybe_declare_manual_implicits false dref impargs in - let () = definition_message name in - Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook; - dref - -let declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry = - try declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry - with exn -> - let exn = Exninfo.capture exn in - let fix_exn = Declare.Internal.get_fix_exn entry in - Exninfo.iraise (fix_exn exn) - -let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = - match possible_indexes with - | Some possible_indexes -> - let env = Global.env() in - let indexes = Pretyping.search_guard env possible_indexes rec_declaration in - let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in - let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in - vars, fixdecls, Some indexes - | None -> - let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixitems in - let vars = Vars.universes_of_constr (List.hd fixdecls) in - vars, fixdecls, None - -module Recthm = struct - type t = - { name : Names.Id.t - (** Name of theorem *) - ; typ : Constr.t - (** Type of theorem *) - ; args : Names.Name.t list - (** Names to pre-introduce *) - ; impargs : Impargs.manual_implicits - (** Explicitily declared implicit arguments *) - } -end - -let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = - let vars, fixdecls, indexes = - mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in - let uctx, univs = - (* XXX: Obligations don't do this, this seems like a bug? *) - if restrict_ucontext - then - let uctx = UState.restrict uctx vars in - let univs = UState.check_univ_decl ~poly uctx udecl in - uctx, univs - else - let univs = UState.univ_entry ~poly uctx in - uctx, univs - in - let csts = CList.map2 - (fun Recthm.{ name; typ; impargs } body -> - let entry = Declare.definition_entry ~opaque ~types:typ ~univs body in - declare_entry ~name ~scope ~kind ~impargs ~uctx entry) - fixitems fixdecls - in - let isfix = Option.has_some possible_indexes in - let fixnames = List.map (fun { Recthm.name } -> name) fixitems in - Declare.recursive_message isfix indexes fixnames; - List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; - csts - -let warn_let_as_axiom = - CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" - Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ - spc () ++ strbrk "declared as an axiom.") - -let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe = - let local = match scope with - | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified - | Global local -> local - in - let kind = Decls.(IsAssumption Conjectural) in - let decl = Declare.ParameterEntry pe in - let kn = Declare.declare_constant ~name ~local ~kind decl in - let dref = Names.GlobRef.ConstRef kn in - let () = Impargs.maybe_declare_manual_implicits false dref impargs in - let () = Declare.assumption_message name in - let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in - let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in - dref - -let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = - try declare_assumption ~name ~scope ~hook ~impargs ~uctx pe - with exn -> - let exn = Exninfo.capture exn in - let exn = Option.cata (fun fix -> fix exn) exn fix_exn in - Exninfo.iraise exn - -(* Preparing proof entries *) - -let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma = - let env = Global.env () in - Pretyping.check_evars_are_solved ~program_mode:false env sigma; - let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true - sigma (fun nf -> nf body, Option.map nf types) - in - let univs = Evd.check_univ_decl ~poly sigma udecl in - let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in - let uctx = Evd.evar_universe_context sigma in - entry, uctx - -let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook - ?obls ~poly ?inline ~types ~body ?fix_exn sigma = - let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in - declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry - -let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = - let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false - sigma (fun nf -> nf body, Option.map nf types) - in - let univs = Evd.check_univ_decl ~poly sigma udecl in - let ce = definition_entry ?opaque ?inline ?types ~univs body in - let env = Global.env () in - let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in - assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private); - assert(Univ.ContextSet.is_empty ctx); - RetrieveObl.check_evars env sigma; - let c = EConstr.of_constr c in - let typ = match ce.Declare.proof_entry_type with - | Some t -> EConstr.of_constr t - | None -> Retyping.get_type_of env sigma c - in - let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in - let uctx = Evd.evar_universe_context sigma in - c, cty, uctx, obls - -let prepare_parameter ~poly ~udecl ~types sigma = - let env = Global.env () in - Pretyping.check_evars_are_solved ~program_mode:false env sigma; - let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:true - sigma (fun nf -> nf types) - in - let univs = Evd.check_univ_decl ~poly sigma udecl in - sigma, (None(*proof using*), (typ, univs), None(*inline*)) +type locality = Declare.locality = + | Discharge [@ocaml.deprecated "Use [Declare.Discharge]"] + | Global of Declare.import_status [@ocaml.deprecated "Use [Declare.Global]"] +[@@ocaml.deprecated "Use [Declare.locality]"] + +let declare_definition = Declare.declare_definition +[@@ocaml.deprecated "Use [Declare.declare_definition]"] +module Hook = Declare.Hook +[@@ocaml.deprecated "Use [Declare.Hook]"] diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli deleted file mode 100644 index 3bc1e25f19..0000000000 --- a/vernac/declareDef.mli +++ /dev/null @@ -1,132 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Names - -type locality = Discharge | Global of Declare.import_status - -(** Declaration hooks *) -module Hook : sig - type t - - (** Hooks allow users of the API to perform arbitrary actions at - proof/definition saving time. For example, to register a constant - as a Coercion, perform some cleanup, update the search database, - etc... *) - module S : sig - type t = - { uctx : UState.t - (** [ustate]: universe constraints obtained when the term was closed *) - ; obls : (Id.t * Constr.t) list - (** [(n1,t1),...(nm,tm)]: association list between obligation - name and the corresponding defined term (might be a constant, - but also an arbitrary term in the Expand case of obligations) *) - ; scope : locality - (** [scope]: Locality of the original declaration *) - ; dref : GlobRef.t - (** [dref]: identifier of the original declaration *) - } - end - - val make : (S.t -> unit) -> t - val call : ?hook:t -> S.t -> unit -end - -(** Declare an interactively-defined constant *) -val declare_entry - : name:Id.t - -> scope:locality - -> kind:Decls.logical_kind - -> ?hook:Hook.t - -> ?obls:(Id.t * Constr.t) list - -> impargs:Impargs.manual_implicits - -> uctx:UState.t - -> Evd.side_effects Declare.proof_entry - -> GlobRef.t - -(** Declares a non-interactive constant; [body] and [types] will be - normalized w.r.t. the passed [evar_map] [sigma]. Universes should - be handled properly, including minimization and restriction. Note - that [sigma] is checked for unresolved evars, thus you should be - careful not to submit open terms or evar maps with stale, - unresolved existentials *) -val declare_definition - : name:Id.t - -> scope:locality - -> kind:Decls.logical_kind - -> opaque:bool - -> impargs:Impargs.manual_implicits - -> udecl:UState.universe_decl - -> ?hook:Hook.t - -> ?obls:(Id.t * Constr.t) list - -> poly:bool - -> ?inline:bool - -> types:EConstr.t option - -> body:EConstr.t - -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) - -> Evd.evar_map - -> GlobRef.t - -val declare_assumption - : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) - -> name:Id.t - -> scope:locality - -> hook:Hook.t option - -> impargs:Impargs.manual_implicits - -> uctx:UState.t - -> Entries.parameter_entry - -> GlobRef.t - -module Recthm : sig - type t = - { name : Id.t - (** Name of theorem *) - ; typ : Constr.t - (** Type of theorem *) - ; args : Name.t list - (** Names to pre-introduce *) - ; impargs : Impargs.manual_implicits - (** Explicitily declared implicit arguments *) - } -end - -val declare_mutually_recursive - : opaque:bool - -> scope:locality - -> kind:Decls.logical_kind - -> poly:bool - -> uctx:UState.t - -> udecl:UState.universe_decl - -> ntns:Vernacexpr.decl_notation list - -> rec_declaration:Constr.rec_declaration - -> possible_indexes:int list list option - -> ?restrict_ucontext:bool - (** XXX: restrict_ucontext should be always true, this seems like a - bug in obligations, so this parameter should go away *) - -> Recthm.t list - -> Names.GlobRef.t list - -val prepare_obligation - : ?opaque:bool - -> ?inline:bool - -> name:Id.t - -> poly:bool - -> udecl:UState.universe_decl - -> types:EConstr.t option - -> body:EConstr.t - -> Evd.evar_map - -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info - -val prepare_parameter - : poly:bool - -> udecl:UState.universe_decl - -> types:EConstr.types - -> Evd.evar_map - -> Evd.evar_map * Entries.parameter_entry diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index bba3687256..ab11472dec 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -55,10 +55,10 @@ module ProgramDecl = struct ; prg_implicits : Impargs.manual_implicits ; prg_notations : Vernacexpr.decl_notation list ; prg_poly : bool - ; prg_scope : DeclareDef.locality + ; prg_scope : Declare.locality ; prg_kind : Decls.definition_object_kind ; prg_reduce : constr -> constr - ; prg_hook : DeclareDef.Hook.t option + ; prg_hook : Declare.Hook.t option ; prg_opaque : bool } @@ -373,7 +373,7 @@ let declare_definition prg = (* XXX: This is doing normalization twice *) let () = progmap_remove prg in let kn = - DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls + Declare.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma in kn @@ -426,7 +426,7 @@ let declare_mutual_definition l = let fixdefs, fixrs, fixtypes, fixitems = List.fold_right2 (fun (d,r,typ,impargs) name (a1,a2,a3,a4) -> d :: a1, r :: a2, typ :: a3, - DeclareDef.Recthm.{ name; typ; impargs; args = [] } :: a4 + Declare.Recthm.{ name; typ; impargs; args = [] } :: a4 ) defs first.prg_deps ([],[],[],[]) in let fixkind = Option.get first.prg_fixkind in @@ -446,13 +446,13 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let udecl = UState.default_univ_decl in let kns = - DeclareDef.declare_mutually_recursive ~scope ~opaque ~kind + Declare.declare_mutually_recursive ~scope ~opaque ~kind ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly ~restrict_ucontext:false fixitems in (* Only for the first constant *) let dref = List.hd kns in - DeclareDef.Hook.(call ?hook:first.prg_hook { S.uctx = first.prg_ctx; obls; scope; dref }); + Declare.Hook.(call ?hook:first.prg_hook { S.uctx = first.prg_ctx; obls; scope; dref }); List.iter progmap_remove l; dref @@ -556,7 +556,7 @@ let obligation_terminator entries uctx { name; num; auto } = (* Similar to the terminator but for interactive paths, as the terminator is only called in interactive proof mode *) -let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } = +let obligation_hook prg obl num auto { Declare.Hook.S.uctx = ctx'; dref; _ } = let { obls; remaining=rem } = prg.prg_obligations in let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in let transparent = evaluable_constant cst (Global.env ()) in diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index 16c0413caf..03f0a57bcb 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -52,22 +52,22 @@ module ProgramDecl : sig ; prg_implicits : Impargs.manual_implicits ; prg_notations : Vernacexpr.decl_notation list ; prg_poly : bool - ; prg_scope : DeclareDef.locality + ; prg_scope : Declare.locality ; prg_kind : Decls.definition_object_kind ; prg_reduce : constr -> constr - ; prg_hook : DeclareDef.Hook.t option + ; prg_hook : Declare.Hook.t option ; prg_opaque : bool } val make : ?opaque:bool - -> ?hook:DeclareDef.Hook.t + -> ?hook:Declare.Hook.t -> Names.Id.t -> udecl:UState.universe_decl -> uctx:UState.t -> impargs:Impargs.manual_implicits -> poly:bool - -> scope:DeclareDef.locality + -> scope:Declare.locality -> kind:Decls.definition_object_kind -> Constr.constr option -> Constr.types @@ -126,7 +126,7 @@ val obligation_hook -> Obligation.t -> Int.t -> (Names.Id.t option -> Int.Set.t -> 'a option -> 'b) - -> DeclareDef.Hook.S.t + -> Declare.Hook.S.t -> unit (** [obligation_hook] part 2 of saving an obligation, non-interactive mode *) diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml index 89f3503f4d..1705915e70 100644 --- a/vernac/declareUniv.ml +++ b/vernac/declareUniv.ml @@ -10,6 +10,17 @@ open Names +(* object_kind , id *) +exception AlreadyDeclared of (string option * Id.t) + +let _ = CErrors.register_handler (function + | AlreadyDeclared (kind, id) -> + Some + Pp.(seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind + ; Id.print id; str " already exists."]) + | _ -> + None) + type universe_source = | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *) | QualifiedUniv of Id.t (* global universe introduced by some global value *) @@ -19,7 +30,7 @@ type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list let check_exists_universe sp = if Nametab.exists_universe sp then - raise (Declare.AlreadyDeclared (Some "Universe", Libnames.basename sp)) + raise (AlreadyDeclared (Some "Universe", Libnames.basename sp)) else () let qualify_univ i dp src id = diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli index 51f3f5e0fb..e4d1d5dc65 100644 --- a/vernac/declareUniv.mli +++ b/vernac/declareUniv.mli @@ -10,6 +10,9 @@ open Names +(* object_kind , id *) +exception AlreadyDeclared of (string option * Id.t) + (** Global universe contexts, names and constraints *) val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index e84fce5504..058fa691ee 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -14,7 +14,6 @@ open Glob_term open Constrexpr open Vernacexpr open Hints -open ComHints open Pcoq open Pcoq.Prim diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 13145d3757..3cb10364b5 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -68,6 +68,11 @@ let make_bullet s = let add_control_flag ~loc ~flag { CAst.v = cmd } = CAst.make ~loc { cmd with control = flag :: cmd.control } +let test_hash_ident = + let open Pcoq.Lookahead in + to_entry "test_hash_ident" begin + lk_kw "#" >> lk_ident >> check_no_space + end } GRAMMAR EXTEND Gram @@ -226,63 +231,9 @@ GRAMMAR EXTEND Gram | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> { VernacConstraint l } ] ] ; - - register_token: - [ [ r = register_prim_token -> { CPrimitives.OT_op r } - | r = register_type_token -> { CPrimitives.OT_type r } ] ] - ; - - register_type_token: - [ [ "#int63_type" -> { CPrimitives.PT_int63 } - | "#float64_type" -> { CPrimitives.PT_float64 } ] ] - ; - - register_prim_token: - [ [ "#int63_head0" -> { CPrimitives.Int63head0 } - | "#int63_tail0" -> { CPrimitives.Int63tail0 } - | "#int63_add" -> { CPrimitives.Int63add } - | "#int63_sub" -> { CPrimitives.Int63sub } - | "#int63_mul" -> { CPrimitives.Int63mul } - | "#int63_div" -> { CPrimitives.Int63div } - | "#int63_mod" -> { CPrimitives.Int63mod } - | "#int63_lsr" -> { CPrimitives.Int63lsr } - | "#int63_lsl" -> { CPrimitives.Int63lsl } - | "#int63_land" -> { CPrimitives.Int63land } - | "#int63_lor" -> { CPrimitives.Int63lor } - | "#int63_lxor" -> { CPrimitives.Int63lxor } - | "#int63_addc" -> { CPrimitives.Int63addc } - | "#int63_subc" -> { CPrimitives.Int63subc } - | "#int63_addcarryc" -> { CPrimitives.Int63addCarryC } - | "#int63_subcarryc" -> { CPrimitives.Int63subCarryC } - | "#int63_mulc" -> { CPrimitives.Int63mulc } - | "#int63_diveucl" -> { CPrimitives.Int63diveucl } - | "#int63_div21" -> { CPrimitives.Int63div21 } - | "#int63_addmuldiv" -> { CPrimitives.Int63addMulDiv } - | "#int63_eq" -> { CPrimitives.Int63eq } - | "#int63_lt" -> { CPrimitives.Int63lt } - | "#int63_le" -> { CPrimitives.Int63le } - | "#int63_compare" -> { CPrimitives.Int63compare } - | "#float64_opp" -> { CPrimitives.Float64opp } - | "#float64_abs" -> { CPrimitives.Float64abs } - | "#float64_eq" -> { CPrimitives.Float64eq } - | "#float64_lt" -> { CPrimitives.Float64lt } - | "#float64_le" -> { CPrimitives.Float64le } - | "#float64_compare" -> { CPrimitives.Float64compare } - | "#float64_classify" -> { CPrimitives.Float64classify } - | "#float64_add" -> { CPrimitives.Float64add } - | "#float64_sub" -> { CPrimitives.Float64sub } - | "#float64_mul" -> { CPrimitives.Float64mul } - | "#float64_div" -> { CPrimitives.Float64div } - | "#float64_sqrt" -> { CPrimitives.Float64sqrt } - | "#float64_of_int63" -> { CPrimitives.Float64ofInt63 } - | "#float64_normfr_mantissa" -> { CPrimitives.Float64normfr_mantissa } - | "#float64_frshiftexp" -> { CPrimitives.Float64frshiftexp } - | "#float64_ldshiftexp" -> { CPrimitives.Float64ldshiftexp } - | "#float64_next_up" -> { CPrimitives.Float64next_up } - | "#float64_next_down" -> { CPrimitives.Float64next_down } - ] ] - ; - + register_token: + [ [ test_hash_ident; "#"; r = IDENT -> { CPrimitives.parse_op_or_type ~loc r } ] ] + ; thm_token: [ [ "Theorem" -> { Theorem } | IDENT "Lemma" -> { Lemma } diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 6ffa88874b..356ccef06b 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -142,7 +142,7 @@ let try_declare_scheme what f internal names kn = | UndefinedCst s -> alarm what internal (strbrk "Required constant " ++ str s ++ str " undefined.") - | AlreadyDeclared (kind, id) as exn -> + | DeclareUniv.AlreadyDeclared (kind, id) as exn -> let msg = CErrors.print exn in alarm what internal msg | DecidabilityMutualNotSupported -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index b13e5bf653..838496c595 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -39,17 +39,17 @@ end module Info = struct type t = - { hook : DeclareDef.Hook.t option + { hook : Declare.Hook.t option ; proof_ending : Proof_ending.t CEphemeron.key (* This could be improved and the CEphemeron removed *) - ; scope : DeclareDef.locality + ; scope : Declare.locality ; kind : Decls.logical_kind (* thms and compute guard are specific only to start_lemma_with_initialization + regular terminator *) - ; thms : DeclareDef.Recthm.t list + ; thms : Declare.Recthm.t list ; compute_guard : lemma_possible_guards } - let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) + let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Declare.Global Declare.ImportDefaultBehavior) ?(kind=Decls.(IsProof Lemma)) () = { hook ; compute_guard = [] @@ -98,7 +98,7 @@ let initialize_named_context_for_proof () = let add_first_thm ~info ~name ~typ ~impargs = let thms = - { DeclareDef.Recthm.name + { Declare.Recthm.name ; impargs ; typ = EConstr.Unsafe.to_constr typ ; args = [] } :: info.Info.thms @@ -128,7 +128,7 @@ let start_dependent_lemma ~name ~poly let rec_tac_initializer finite guard thms snl = if finite then - match List.map (fun { DeclareDef.Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with + match List.map (fun { Declare.Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else @@ -136,12 +136,12 @@ let rec_tac_initializer finite guard thms snl = let nl = match snl with | None -> List.map succ (List.map List.last guard) | Some nl -> nl - in match List.map2 (fun { DeclareDef.Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with + in match List.map2 (fun { Declare.Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl = - let intro_tac { DeclareDef.Recthm.args; _ } = Tactics.auto_intros_tac args in + let intro_tac { Declare.Recthm.args; _ } = Tactics.auto_intros_tac args in let init_tac, compute_guard = match recguard with | Some (finite,guard,init_terms) -> let rec_tac = rec_tac_initializer finite guard thms snl in @@ -161,7 +161,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua intro_tac (List.hd thms), [] in match thms with | [] -> CErrors.anomaly (Pp.str "No proof to start.") - | { DeclareDef.Recthm.name; typ; impargs; _} :: thms -> + | { Declare.Recthm.name; typ; impargs; _} :: thms -> let info = Info.{ hook ; compute_guard @@ -200,7 +200,7 @@ module MutualEntry : sig end = struct - (* XXX: Refactor this with the code in [DeclareDef.declare_mutdef] *) + (* XXX: Refactor this with the code in [Declare.declare_mutdef] *) let guess_decreasing env possible_indexes ((body, ctx), eff) = let open Constr in match Constr.kind body with @@ -220,7 +220,7 @@ end = struct Pp.(str "Not a proof by induction: " ++ Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".") - let declare_mutdef ~uctx ~info pe i DeclareDef.Recthm.{ name; impargs; typ; _} = + let declare_mutdef ~uctx ~info pe i Declare.Recthm.{ name; impargs; typ; _} = let { Info.hook; scope; kind; compute_guard; _ } = info in (* if i = 0 , we don't touch the type; this is for compat but not clear it is the right thing to do. @@ -238,7 +238,7 @@ end = struct Declare.Internal.map_entry_body pe ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in - DeclareDef.declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe + Declare.declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe let declare_mutdef ~info ~uctx const = let pe = match info.Info.compute_guard with @@ -256,8 +256,8 @@ end = struct let declare_variable ~info ~uctx pe = let { Info.scope; hook } = info in List.map_i ( - fun i { DeclareDef.Recthm.name; typ; impargs } -> - DeclareDef.declare_assumption ~name ~scope ~hook ~impargs ~uctx pe + fun i { Declare.Recthm.name; typ; impargs } -> + Declare.declare_assumption ~name ~scope ~hook ~impargs ~uctx pe ) 0 info.Info.thms end @@ -395,8 +395,8 @@ let process_idopt_for_save ~idopt info = (* Save foo was used; we override the info in the first theorem *) let thms = match info.Info.thms, CEphemeron.default info.Info.proof_ending Proof_ending.Regular with - | [ { DeclareDef.Recthm.name; _} as decl ], Proof_ending.Regular -> - [ { decl with DeclareDef.Recthm.name = save_name } ] + | [ { Declare.Recthm.name; _} as decl ], Proof_ending.Regular -> + [ { decl with Declare.Recthm.name = save_name } ] | _ -> err_save_forbidden_in_place_of_qed () in { info with Info.thms } diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index bd2e87ac3a..b1462f1ce5 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -49,11 +49,11 @@ module Info : sig type t val make - : ?hook: DeclareDef.Hook.t + : ?hook: Declare.Hook.t (** Callback to be executed at the end of the proof *) -> ?proof_ending : Proof_ending.t (** Info for special constants *) - -> ?scope : DeclareDef.locality + -> ?scope : Declare.locality (** locality *) -> ?kind:Decls.logical_kind (** Theorem, etc... *) @@ -85,14 +85,14 @@ type lemma_possible_guards = int list list (** Pretty much internal, used by the Lemma / Fixpoint vernaculars *) val start_lemma_with_initialization - : ?hook:DeclareDef.Hook.t + : ?hook:Declare.Hook.t -> poly:bool - -> scope:DeclareDef.locality + -> scope:Declare.locality -> kind:Decls.logical_kind -> udecl:UState.universe_decl -> Evd.evar_map -> (bool * lemma_possible_guards * Constr.t option list option) option - -> DeclareDef.Recthm.t list + -> Declare.Recthm.t list -> int list option -> t diff --git a/vernac/locality.ml b/vernac/locality.ml index 9e784c8bb3..f62eed5e41 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -34,7 +34,7 @@ let warn_local_declaration = strbrk "available without qualification when imported.") let enforce_locality_exp locality_flag discharge = - let open DeclareDef in + let open Declare in let open Vernacexpr in match locality_flag, discharge with | Some b, NoDischarge -> Global (importability_of_bool b) diff --git a/vernac/locality.mli b/vernac/locality.mli index 26149cb394..bf65579efd 100644 --- a/vernac/locality.mli +++ b/vernac/locality.mli @@ -20,7 +20,7 @@ val make_locality : bool option -> bool val make_non_locality : bool option -> bool -val enforce_locality_exp : bool option -> Vernacexpr.discharge -> DeclareDef.locality +val enforce_locality_exp : bool option -> Vernacexpr.discharge -> Declare.locality val enforce_locality : bool option -> bool (** For commands whose default is to not discharge but to export: diff --git a/vernac/obligations.ml b/vernac/obligations.ml index bed593234b..5e746afc74 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -162,13 +162,13 @@ let rec solve_obligation prg num tac = ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining)); in let obl = subst_deps_obl obls obl in - let scope = DeclareDef.(Global Declare.ImportNeedQualified) in + let scope = Declare.(Global Declare.ImportNeedQualified) in let kind = kind_of_obligation (snd obl.obl_status) in let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n oblset tac = auto_solve_obligations n ~oblset tac in let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in - let hook = DeclareDef.Hook.make (DeclareObl.obligation_hook prg obl num auto) in + let hook = Declare.Hook.make (DeclareObl.obligation_hook prg obl num auto) in let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in let poly = prg.prg_poly in let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in @@ -309,7 +309,7 @@ let show_term n = ++ Printer.pr_constr_env env sigma prg.prg_body) let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl) - ?(impargs=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic + ?(impargs=[]) ~poly ?(scope=Declare.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic ?(reduce=reduce) ?hook ?(opaque = false) obls = let info = Id.print name ++ str " has type-checked" in let prg = ProgramDecl.make ~opaque name ~udecl term t ~uctx [] None [] obls ~impargs ~poly ~scope ~kind reduce ?hook in @@ -328,11 +328,11 @@ let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl) | _ -> res) let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic - ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce) + ~poly ?(scope=Declare.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce) ?hook ?(opaque = false) notations fixkind = - let deps = List.map (fun ({ DeclareDef.Recthm.name; _ }, _, _) -> name) l in + let deps = List.map (fun ({ Declare.Recthm.name; _ }, _, _) -> name) l in List.iter - (fun ({ DeclareDef.Recthm.name; typ; impargs; _ }, b, obls) -> + (fun ({ Declare.Recthm.name; typ; impargs; _ }, b, obls) -> let prg = ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps (Some fixkind) notations obls ~impargs ~poly ~scope ~kind reduce ?hook in progmap_add name (CEphemeron.create prg)) l; diff --git a/vernac/obligations.mli b/vernac/obligations.mli index f42d199e18..89ed4c3498 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -77,11 +77,11 @@ val add_definition : -> ?udecl:UState.universe_decl (** Universe binders and constraints *) -> ?impargs:Impargs.manual_implicits -> poly:bool - -> ?scope:DeclareDef.locality + -> ?scope:Declare.locality -> ?kind:Decls.definition_object_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(constr -> constr) - -> ?hook:DeclareDef.Hook.t + -> ?hook:Declare.Hook.t -> ?opaque:bool -> RetrieveObl.obligation_info -> DeclareObl.progress @@ -91,15 +91,15 @@ val add_definition : (** Start a [Program Fixpoint] declaration, similar to the above, except it takes a list now. *) val add_mutual_definitions : - (DeclareDef.Recthm.t * Constr.t * RetrieveObl.obligation_info) list + (Declare.Recthm.t * Constr.t * RetrieveObl.obligation_info) list -> uctx:UState.t -> ?udecl:UState.universe_decl (** Universe binders and constraints *) -> ?tactic:unit Proofview.tactic -> poly:bool - -> ?scope:DeclareDef.locality + -> ?scope:Declare.locality -> ?kind:Decls.definition_object_kind -> ?reduce:(constr -> constr) - -> ?hook:DeclareDef.Hook.t + -> ?hook:Declare.Hook.t -> ?opaque:bool -> Vernacexpr.decl_notation list -> DeclareObl.fixpoint_kind diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f1aae239aa..b97cdfa51c 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -185,7 +185,7 @@ open Pputils | [] -> mt() | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z - let pr_reference_or_constr pr_c = let open ComHints in function + let pr_reference_or_constr pr_c = function | HintsReference r -> pr_qualid r | HintsConstr c -> pr_c c @@ -202,7 +202,6 @@ open Pputils let opth = pr_opt_hintbases db in let pph = let open Hints in - let open ComHints in match h with | HintsResolve l -> keyword "Resolve " ++ prlist_with_sep sep @@ -792,7 +791,6 @@ let string_of_definition_object_kind = let open Decls in function return (keyword "Admitted") | VernacEndProof (Proved (opac,o)) -> return ( - let open Declare in match o with | None -> (match opac with | Transparent -> keyword "Defined" diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index 2b6beaf2e3..1718024edd 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -28,7 +28,7 @@ module Vernac_ : val command_entry : vernac_expr Entry.t val main_entry : vernac_control option Entry.t val red_expr : raw_red_expr Entry.t - val hint_info : ComHints.hint_info_expr Entry.t + val hint_info : hint_info_expr Entry.t end (* To be removed when the parser is made functional wrt the tactic diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 6d5d16d94a..618a61f487 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -9,16 +9,15 @@ Himsg Locality Egramml Vernacextend -Declare -ComHints Ppvernac Proof_using Egramcoq Metasyntax DeclareUniv RetrieveObl -DeclareDef +Declare DeclareObl +ComHints Canonical RecLemmas Library @@ -48,3 +47,4 @@ Vernacstate Vernacinterp Proof_global Pfedit +DeclareDef diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index df94f69cf6..aac0b54ed4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -460,7 +460,7 @@ let vernac_custom_entry ~module_local s = let check_name_freshness locality {CAst.loc;v=id} : unit = (* We check existence here: it's a bit late at Qed time *) if Nametab.exists_cci (Lib.make_path id) || Termops.is_section_variable id || - locality <> DeclareDef.Discharge && Nametab.exists_cci (Lib.make_path_except_section id) + locality <> Declare.Discharge && Nametab.exists_cci (Lib.make_path_except_section id) then user_err ?loc (Id.print id ++ str " already exists.") @@ -504,7 +504,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in let evd = Evd.minimize_universes evd in let thms = List.map (fun (name, (typ, (args, impargs))) -> - { DeclareDef.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in + { Declare.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in let () = let open UState in if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then @@ -521,13 +521,13 @@ let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in | Coercion -> Some (ComCoercion.add_coercion_hook ~poly) | CanonicalStructure -> - Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) + Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) | SubClass -> Some (ComCoercion.add_subclass_hook ~poly) | Definition when canonical_instance -> - Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) + Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref))) | Let when canonical_instance -> - Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref))) + Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref))) | _ -> None let default_thm_id = Id.of_string "Unnamed_thm" @@ -542,7 +542,7 @@ let vernac_definition_name lid local = CAst.make ?loc (fresh_name_for_anonymous_theorem ()) | { v = Name.Name n; loc } -> CAst.make ?loc n in let () = - let open DeclareDef in + let open Declare in match local with | Discharge -> Dumpglob.dump_definition lid true "var" | Global _ -> Dumpglob.dump_definition lid false "def" @@ -603,8 +603,8 @@ let vernac_assumption ~atts discharge kind l nl = if Dumpglob.dump () then List.iter (fun (lid, _) -> match scope with - | DeclareDef.Global _ -> Dumpglob.dump_definition lid false "ax" - | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l; + | Declare.Global _ -> Dumpglob.dump_definition lid false "ax" + | Declare.Discharge -> Dumpglob.dump_definition lid true "var") idl) l; ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l let is_polymorphic_inductive_cumulativity = diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index b65a0da1cc..b622fd9801 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -195,10 +195,12 @@ type syntax_modifier = | SetOnlyPrinting | SetFormat of string * lstring +type opacity_flag = Opaque | Transparent + type proof_end = | Admitted (* name in `Save ident` when closing goal *) - | Proved of Declare.opacity_flag * lident option + | Proved of opacity_flag * lident option type scheme = | InductionScheme of bool * qualid or_by_notation * sort_expr @@ -286,6 +288,22 @@ type extend_name = type discharge = DoDischarge | NoDischarge +type hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen + +type reference_or_constr = + | HintsReference of Libnames.qualid + | HintsConstr of Constrexpr.constr_expr + +type hints_expr = + | HintsResolve of (hint_info_expr * bool * reference_or_constr) list + | HintsResolveIFF of bool * Libnames.qualid list * int option + | HintsImmediate of reference_or_constr list + | HintsUnfold of Libnames.qualid list + | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool + | HintsMode of Libnames.qualid * Hints.hint_mode list + | HintsConstructors of Libnames.qualid list + | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument + type nonrec vernac_expr = | VernacLoad of verbose_flag * string @@ -336,18 +354,18 @@ type nonrec vernac_expr = local_binder_expr list * (* binders *) constr_expr * (* type *) (bool * constr_expr) option * (* body (bool=true when using {}) *) - ComHints.hint_info_expr + hint_info_expr | VernacDeclareInstance of ident_decl * (* name *) local_binder_expr list * (* binders *) constr_expr * (* type *) - ComHints.hint_info_expr + hint_info_expr | VernacContext of local_binder_expr list | VernacExistingInstance of - (qualid * ComHints.hint_info_expr) list (* instances names, priorities and patterns *) + (qualid * hint_info_expr) list (* instances names, priorities and patterns *) | VernacExistingClass of qualid (* inductive or definition name *) @@ -387,7 +405,7 @@ type nonrec vernac_expr = (* Commands *) | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * qualid list - | VernacHints of string list * ComHints.hints_expr + | VernacHints of string list * hints_expr | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * onlyparsing_flag |