diff options
100 files changed, 2023 insertions, 790 deletions
@@ -65,6 +65,33 @@ Standard Library - Added `Ndigits.N2Bv_sized`, and proved some lemmas about it. +- The scopes `int_scope` and `uint_scope` have been renamed to + `dec_int_scope` and `dec_uint_scope`, to clash less with ssreflect + and other packages. They are still delimited by `%int` and `%uint`. + +- Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`, + and `int31` are no longer available merely by `Require`ing the files + that define the inductives. You must `Import` `Coq.Strings.String`, + `Coq.Strings.Ascii`, `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`, + `Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and + `Coq.Numbers.Cyclic.Int31.Int31`, respectively, to be able to use + these notations. Note that passing `-compat 8.8` or issuing + `Require Import Coq.Compat.Coq88` will make these notations + available. Users wishing to port their developments automatically + may download `fix.py` from + <https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169> + and run a command like `while true; do make -Okj 2>&1 | + /path/to/fix.py; done` and get a cup of coffee. (This command must + be manually interrupted once the build finishes all the way though. + Note also that this method is not fail-proof; you may have to adjust + some scopes if you were relying on string notations not being + available even when `string_scope` was open.) + +- Numeral syntax for `nat` is no longer available without loading the + entire prelude (`Require Import Coq.Init.Prelude`). This only + impacts users running Coq without the init library (`-nois` or + `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`. + Tools - Coq_makefile lets one override or extend the following variables from @@ -98,6 +125,8 @@ Vernacular Commands overwritting the opacity set of the hint database. - Added generic syntax for “attributes”, as in: `#[local] Lemma foo : bar.` +- Added the `Numeral Notation` command for registering decimal numeral + notations for custom types - The `Set SsrHave NoTCResolution` command no longer has special global scope. If you want the previous behavior, use `Global Set SsrHave NoTCResolution`. diff --git a/Makefile.common b/Makefile.common index 772561bd70..09457ced7b 100644 --- a/Makefile.common +++ b/Makefile.common @@ -140,13 +140,12 @@ FOCMO:=plugins/firstorder/ground_plugin.cmo CCCMO:=plugins/cc/cc_plugin.cmo BTAUTOCMO:=plugins/btauto/btauto_plugin.cmo RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo -NATSYNTAXCMO:=plugins/syntax/nat_syntax_plugin.cmo -OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \ - positive_syntax_plugin.cmo n_syntax_plugin.cmo \ - z_syntax_plugin.cmo r_syntax_plugin.cmo \ +SYNTAXCMO:=$(addprefix plugins/syntax/, \ + r_syntax_plugin.cmo \ int31_syntax_plugin.cmo \ ascii_syntax_plugin.cmo \ - string_syntax_plugin.cmo ) + string_syntax_plugin.cmo \ + numeral_notation_plugin.cmo) DERIVECMO:=plugins/derive/derive_plugin.cmo LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo @@ -156,7 +155,7 @@ PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \ $(QUOTECMO) $(RINGCMO) \ $(EXTRACTIONCMO) \ $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ - $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \ + $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \ $(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO) ifeq ($(HASNATDYNLINK)-$(BEST),false-opt) diff --git a/Makefile.dev b/Makefile.dev index 68e96a57b7..7fc1076a8f 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -91,7 +91,7 @@ endif coqlight: theories-light tools coqbinaries -states: camldevfiles theories/Init/Prelude.vo +states: theories/Init/Prelude.vo miniopt: $(COQTOPEXE) pluginsopt minibyte: $(COQTOPBYTE) pluginsbyte diff --git a/checker/cic.mli b/checker/cic.mli index df747692a4..17259bb438 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -220,6 +220,7 @@ type typing_flags = { points are assumed to be total. *) check_universes : bool; (** If [false] universe constraints are not checked *) conv_oracle : oracle; (** Unfolding strategies for conversion *) + share_reduction : bool; (** Use by-need reduction algorithm *) } type constant_body = { diff --git a/checker/values.ml b/checker/values.ml index e68cd18b87..e1b5a949ac 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -15,7 +15,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 064cd8d9651d37aebf77fb638b889cad checker/cic.mli +MD5 f7b267579138eabf86a74d6f2a7ed794 checker/cic.mli *) @@ -226,7 +226,7 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|] + v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool|] let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 60108cda4f..8a49b97dac 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1448,10 +1448,10 @@ function make_addons { export CI_BRANCH="" export CI_PULL_REQUEST="" fi - . /build/ci-basic-overlay.sh for overlay in /build/user-overlays/*.sh; do . "$overlay" done + . /build/ci-basic-overlay.sh for addon in $COQ_ADDONS; do "make_addon_$addon" diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 3536cc70b2..7af648f0a6 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -37,12 +37,12 @@ ls "$COQBIN" # Where we download and build external developments CI_BUILD_DIR="$PWD/_build_ci" -# shellcheck source=ci-basic-overlay.sh -. "${ci_dir}/ci-basic-overlay.sh" for overlay in "${ci_dir}"/user-overlays/*.sh; do # shellcheck source=/dev/null . "${overlay}" done +# shellcheck source=ci-basic-overlay.sh +. "${ci_dir}/ci-basic-overlay.sh" # [git_download project] will download [project] and unpack it # in [$CI_BUILD_DIR/project] if the folder does not exist already; diff --git a/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh new file mode 100644 index 0000000000..575df07425 --- /dev/null +++ b/dev/ci/user-overlays/07085-ppedrot-pure-sharing-flag.sh @@ -0,0 +1,8 @@ +_OVERLAY_BRANCH=pure-sharing-flag + +if [ "$CI_PULL_REQUEST" = "7085" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + mtac2_CI_BRANCH="$_OVERLAY_BRANCH" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + +fi diff --git a/dev/ci/user-overlays/jasongross-numeral-notation-4.sh b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh new file mode 100644 index 0000000000..76aa37d380 --- /dev/null +++ b/dev/ci/user-overlays/jasongross-numeral-notation-4.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "8064" ] || [ "$CI_BRANCH" = "numeral-notation-4" ]; then + HoTT_CI_REF=fix-for-numeral-notations + HoTT_CI_GITURL=https://github.com/JasonGross/HoTT + HoTT_CI_ARCHIVEURL=${HoTT_CI_GITURL}/archive +fi diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 5089a1b3e3..b46382dbbf 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1372,6 +1372,154 @@ Abbreviations denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. + +Numeral notations +----------------- + +.. cmd:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope. + + This command allows the user to customize the way numeral literals + are parsed and printed. + + The token :n:`@ident__1` should be the name of an inductive type, + while :n:`@ident__2` and :n:`@ident__3` should be the names of the + parsing and printing functions, respectively. The parsing function + :n:`@ident__2` should have one of the following types: + + * :n:`Decimal.int -> @ident__1` + * :n:`Decimal.int -> option @ident__1` + * :n:`Decimal.uint -> @ident__1` + * :n:`Decimal.uint -> option @ident__1` + * :n:`Z -> @ident__1` + * :n:`Z -> option @ident__1` + + And the printing function :n:`@ident__3` should have one of the + following types: + + * :n:`@ident__1 -> Decimal.int` + * :n:`@ident__1 -> option Decimal.int` + * :n:`@ident__1 -> Decimal.uint` + * :n:`@ident__1 -> option Decimal.uint` + * :n:`@ident__1 -> Z` + * :n:`@ident__1 -> option Z` + + When parsing, the application of the parsing function + :n:`@ident__2` to the number will be fully reduced, and universes + of the resulting term will be refreshed. + + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num). + + When a literal larger than :token:`num` is parsed, a warning + message about possible stack overflow, resulting from evaluating + :n:`@ident__2`, will be displayed. + + .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (abstract after @num). + + When a literal :g:`m` larger than :token:`num` is parsed, the + result will be :n:`(@ident__2 m)`, without reduction of this + application to a normal form. Here :g:`m` will be a + :g:`Decimal.int` or :g:`Decimal.uint` or :g:`Z`, depending on the + type of the parsing function :n:`@ident__2`. This allows for a + more compact representation of literals in types such as :g:`nat`, + and limits parse failures due to stack overflow. Note that a + warning will be emitted when an integer larger than :token:`num` + is parsed. Note that :n:`(abstract after @num)` has no effect + when :n:`@ident__2` lands in an :g:`option` type. + + .. exn:: Cannot interpret this number as a value of type @type + + The numeral notation registered for :token:`type` does not support + the given numeral. This error is given when the interpretation + function returns :g:`None`, or if the interpretation is registered + for only non-negative integers, and the given numeral is negative. + + .. exn:: @ident should go from Decimal.int to @type or (option @type). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + + The parsing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. + + .. exn:: @ident should go from @type to Decimal.int or (option Decimal.int). Instead of Decimal.int, the types Decimal.uint or Z could be used{? (require BinNums first)}. + + The printing function given to the :cmd:`Numeral Notation` + vernacular is not of the right type. + + .. exn:: @type is not an inductive type. + + Numeral notations can only be declared for inductive types with no + arguments. + + .. exn:: Unexpected term @term while parsing a numeral notation. + + Parsing functions must always return ground terms, made up of + applications of constructors and inductive types. Parsing + functions may not return terms containing axioms, bare + (co)fixpoints, lambdas, etc. + + .. exn:: Unexpected non-option term @term while parsing a numeral notation. + + Parsing functions expected to return an :g:`option` must always + return a concrete :g:`Some` or :g:`None` when applied to a + concrete numeral expressed as a decimal. They may not return + opaque constants. + + .. exn:: Cannot interpret in @scope because @ident could not be found in the current environment. + + The inductive type used to register the numeral notation is no + longer available in the environment. Most likely, this is because + the numeral notation was declared inside a functor for an + inductive type inside the functor. This use case is not currently + supported. + + Alternatively, you might be trying to use a primitive token + notation from a plugin which forgot to specify which module you + must :g:`Require` for access to that notation. + + .. exn:: Syntax error: [prim:reference] expected after 'Notation' (in [vernac:command]). + + The type passed to :cmd:`Numeral Notation` must be a single + identifier. + + .. exn:: Syntax error: [prim:reference] expected after [prim:reference] (in [vernac:command]). + + Both functions passed to :cmd:`Numeral Notation` must be single + identifiers. + + .. exn:: The reference @ident was not found in the current environment. + + Identifiers passed to :cmd:`Numeral Notation` must exist in the + global environment. + + .. exn:: @ident is bound to a notation that does not denote a reference. + + Identifiers passed to :cmd:`Numeral Notation` must be global + references, or notations which denote to single identifiers. + + .. warn:: Stack overflow or segmentation fault happens when working with large numbers in @type (threshold may vary depending on your system limits and on the command executed). + + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(warning after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + + .. warn:: To avoid stack overflow, large numbers in @type are interpreted as applications of @ident__2. + + When a :cmd:`Numeral Notation` is registered in the current scope + with :n:`(abstract after @num)`, this warning is emitted when + parsing a numeral greater than or equal to :token:`num`. + Typically, this indicates that the fully computed representation + of numerals can be so large that non-tail-recursive OCaml + functions run out of stack space when trying to walk them. + + For example + + .. coqtop:: all + + Check 90000. + + .. warn:: The 'abstract after' directive has no effect when the parsing function (@ident__2) targets an option type. + + As noted above, the :n:`(abstract after @num)` directive has no + effect when :n:`@ident__2` lands in an :g:`option` type. + .. _TacticNotation: Tactic Notations diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index f448248468..0fa42cadad 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -226,6 +226,7 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/BinNums.v theories/Numbers/NumPrelude.v theories/Numbers/NaryFunctions.v + theories/Numbers/AltBinNotations.v theories/Numbers/DecimalFacts.v theories/Numbers/DecimalNat.v theories/Numbers/DecimalPos.v diff --git a/engine/evd.ml b/engine/evd.ml index d1c7fef738..9f976b57dd 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -774,7 +774,7 @@ let universe_subst evd = UState.subst evd.universes let merge_context_set ?loc ?(sideff=false) rigid evd ctx' = - {evd with universes = UState.merge ?loc sideff rigid evd.universes ctx'} + {evd with universes = UState.merge ?loc ~sideff ~extend:true rigid evd.universes ctx'} let merge_universe_subst evd subst = {evd with universes = UState.merge_subst evd.universes subst } diff --git a/engine/uState.ml b/engine/uState.ml index 0791e4c277..29cb3c9bcc 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -430,10 +430,17 @@ let univ_rigid = UnivRigid let univ_flexible = UnivFlexible false let univ_flexible_alg = UnivFlexible true -let merge ?loc sideff rigid uctx ctx' = +(** ~sideff indicates that it is ok to redeclare a universe. + ~extend also merges the universe context in the local constraint structures + and not only in the graph. This depends if the + context we merge comes from a side effect that is already inlined + or defined separately. In the later case, there is no extension, + see [emit_side_effects] for example. *) +let merge ?loc ~sideff ~extend rigid uctx ctx' = let open Univ in let levels = ContextSet.levels ctx' in - let uctx = if sideff then uctx else + let uctx = + if not extend then uctx else match rigid with | UnivRigid -> uctx | UnivFlexible b -> @@ -448,9 +455,8 @@ let merge ?loc sideff rigid uctx ctx' = else { uctx with uctx_univ_variables = uvars' } in let uctx_local = - if sideff then uctx.uctx_local - else ContextSet.append ctx' uctx.uctx_local - in + if not extend then uctx.uctx_local + else ContextSet.append ctx' uctx.uctx_local in let declare g = LSet.fold (fun u g -> try UGraph.add_universe u false g @@ -479,7 +485,7 @@ let merge_subst uctx s = let emit_side_effects eff u = let uctxs = Safe_typing.universes_of_private eff in - List.fold_left (merge true univ_rigid) u uctxs + List.fold_left (merge ~sideff:true ~extend:false univ_rigid) u uctxs let new_univ_variable ?loc rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = @@ -668,7 +674,7 @@ let update_sigma_env uctx env = { uctx with uctx_initial_universes = univs; uctx_universes = univs } in - merge true univ_rigid eunivs eunivs.uctx_local + merge ~sideff:true ~extend:false univ_rigid eunivs eunivs.uctx_local let pr_weak prl {uctx_weak_constraints=weak} = let open Pp in diff --git a/engine/uState.mli b/engine/uState.mli index a59e61b894..f833508ebf 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -103,7 +103,7 @@ val univ_rigid : rigid val univ_flexible : rigid val univ_flexible_alg : rigid -val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t +val merge : ?loc:Loc.t -> sideff:bool -> extend:bool -> rigid -> t -> Univ.ContextSet.t -> t val merge_subst : t -> UnivSubst.universe_opt_subst -> t val emit_side_effects : Safe_typing.private_constants -> t -> t diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 009894fddb..ddc0a5c000 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -531,18 +531,7 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = else try if !Flags.raw_print || !print_no_symbol then raise No_match; - let (sc,p) = uninterp_prim_token_ind_pattern ind args 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 -> - insert_pat_coercion coercion (insert_pat_delimiters (CAst.make @@ CPatPrim p) key) - with No_match -> - try - if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation_ind_pattern allscopes vars ind args + extern_notation_ind_pattern allscopes vars ind args (uninterp_ind_pattern_notations ind) with No_match -> let c = extern_reference vars (IndRef ind) in diff --git a/interp/declare.ml b/interp/declare.ml index 2b2ca36edc..a82e6b35a6 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -150,8 +150,8 @@ let register_side_effect (c, role) = ignore(add_leaf id o); update_tables c; match role with - | Safe_typing.Subproof -> () - | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|] + | Subproof -> () + | Schema (ind, kind) -> !declare_scheme kind [|ind,c|] let declare_constant_common id cst = let o = inConstant cst in diff --git a/interp/notation.ml b/interp/notation.ml index 625d072b9f..55ead946cb 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -266,16 +266,14 @@ let keymap_find key map = (* Scopes table : interpretation -> scope_name *) let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) -let prim_token_key_table = ref (KeyMap.empty : (string * (any_glob_constr -> prim_token option) * bool) KeyMap.t) - let glob_prim_constr_key c = match DAst.get c with - | GRef (ref, _) -> RefKey (canonical_gr ref) + | GRef (ref, _) -> Some (canonical_gr ref) | GApp (c, _) -> begin match DAst.get c with - | GRef (ref, _) -> RefKey (canonical_gr ref) - | _ -> Oth + | GRef (ref, _) -> Some (canonical_gr ref) + | _ -> None end - | _ -> Oth + | _ -> None let glob_constr_keys c = match DAst.get c with | GApp (c, _) -> @@ -303,77 +301,189 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) (* Interpreting numbers (not in summary because functional objects) *) type required_module = full_path * string list +type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign -type 'a prim_token_interpreter = - ?loc:Loc.t -> 'a -> glob_constr +type prim_token_uid = string -type cases_pattern_status = bool (* true = use prim token in patterns *) +type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr +type 'a prim_token_uninterpreter = any_glob_constr -> 'a option -type 'a prim_token_uninterpreter = - glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status +type 'a prim_token_interpretation = + 'a prim_token_interpreter * 'a prim_token_uninterpreter -type internal_prim_token_interpreter = - ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr) +module InnerPrimToken = struct -let prim_token_interpreter_tab = - (Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t) + type interpreter = + | RawNumInterp of (?loc:Loc.t -> rawnum -> glob_constr) + | BigNumInterp of (?loc:Loc.t -> Bigint.bigint -> glob_constr) + | StringInterp of (?loc:Loc.t -> string -> glob_constr) -let add_prim_token_interpreter sc interp = - try - let cont = Hashtbl.find prim_token_interpreter_tab sc in - Hashtbl.replace prim_token_interpreter_tab sc (interp cont) - with Not_found -> - let cont = (fun ?loc _p -> raise Not_found) in - Hashtbl.add prim_token_interpreter_tab sc (interp cont) + let interp_eq f f' = match f,f' with + | RawNumInterp f, RawNumInterp f' -> f == f' + | BigNumInterp f, BigNumInterp f' -> f == f' + | StringInterp f, StringInterp f' -> f == f' + | _ -> false -let declare_prim_token_interpreter sc interp (patl,uninterp,b) = - declare_scope sc; - add_prim_token_interpreter sc interp; - List.iter (fun pat -> - prim_token_key_table := KeyMap.add - (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table) - patl + let ofNumeral n s = + if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) -let mkNumeral n = - if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true) - else Numeral (Bigint.to_string (Bigint.neg n), false) + let do_interp ?loc interp primtok = + match primtok, interp with + | Numeral (n,s), RawNumInterp interp -> interp ?loc (n,s) + | Numeral (n,s), BigNumInterp interp -> interp ?loc (ofNumeral n s) + | String s, StringInterp interp -> interp ?loc s + | _ -> raise Not_found -let ofNumeral n s = - if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) + type uninterpreter = + | RawNumUninterp of (any_glob_constr -> rawnum option) + | BigNumUninterp of (any_glob_constr -> Bigint.bigint option) + | StringUninterp of (any_glob_constr -> string option) -let mkString = function -| None -> None -| Some s -> if Unicode.is_utf8 s then Some (String s) else None + let uninterp_eq f f' = match f,f' with + | RawNumUninterp f, RawNumUninterp f' -> f == f' + | BigNumUninterp f, BigNumUninterp f' -> f == f' + | StringUninterp f, StringUninterp f' -> f == f' + | _ -> false -let delay dir int ?loc x = (dir, (fun () -> int ?loc x)) + let mkNumeral n = + if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true) + else Numeral (Bigint.to_string (Bigint.neg n), false) -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign + let mkString = function + | None -> None + | Some s -> if Unicode.is_utf8 s then Some (String s) else None + + let do_uninterp uninterp g = match uninterp with + | RawNumUninterp u -> Option.map (fun (n,s) -> Numeral (n,s)) (u g) + | BigNumUninterp u -> Option.map mkNumeral (u g) + | StringUninterp u -> mkString (u g) + +end + +(* The following two tables of (un)interpreters will *not* be synchronized. + But their indexes will be checked to be unique *) +let prim_token_interpreters = + (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.interpreter) Hashtbl.t) + +let prim_token_uninterpreters = + (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t) + +(* Table from scope_name to backtrack-able informations about interpreters + (in particular interpreter unique id). *) +let prim_token_interp_infos = + ref (String.Map.empty : (required_module * prim_token_uid) String.Map.t) + +(* Table from global_reference to backtrack-able informations about + prim_token uninterpretation (in particular uninterpreter unique id). *) +let prim_token_uninterp_infos = + ref (Refmap.empty : (scope_name * prim_token_uid * bool) Refmap.t) + +let hashtbl_check_and_set allow_overwrite uid f h eq = + match Hashtbl.find h uid with + | exception Not_found -> Hashtbl.add h uid f + | _ when allow_overwrite -> Hashtbl.add h uid f + | g when eq f g -> () + | _ -> + user_err ~hdr:"prim_token_interpreter" + (str "Unique identifier " ++ str uid ++ + str " already used to register a numeral or string (un)interpreter.") + +let register_gen_interpretation allow_overwrite uid (interp, uninterp) = + hashtbl_check_and_set + allow_overwrite uid interp prim_token_interpreters InnerPrimToken.interp_eq; + hashtbl_check_and_set + allow_overwrite uid uninterp prim_token_uninterpreters InnerPrimToken.uninterp_eq + +let register_rawnumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid + (InnerPrimToken.RawNumInterp interp, InnerPrimToken.RawNumUninterp uninterp) + +let register_bignumeral_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid + (InnerPrimToken.BigNumInterp interp, InnerPrimToken.BigNumUninterp uninterp) + +let register_string_interpretation ?(allow_overwrite=false) uid (interp, uninterp) = + register_gen_interpretation allow_overwrite uid + (InnerPrimToken.StringInterp interp, InnerPrimToken.StringUninterp uninterp) + +type prim_token_infos = { + pt_local : bool; (** Is this interpretation local? *) + pt_scope : scope_name; (** Concerned scope *) + pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) + pt_required : required_module; (** Module that should be loaded first *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) + pt_in_match : bool (** Is this prim token legal in match patterns ? *) +} + +let cache_prim_token_interpretation (_,infos) = + let sc = infos.pt_scope in + let uid = infos.pt_uid in + declare_scope sc; + prim_token_interp_infos := + String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos; + List.iter (fun r -> prim_token_uninterp_infos := + Refmap.add r (sc,uid,infos.pt_in_match) + !prim_token_uninterp_infos) + infos.pt_refs + +let subst_prim_token_interpretation (subs,infos) = + { infos with + pt_refs = List.map (subst_global_reference subs) infos.pt_refs } + +let classify_prim_token_interpretation infos = + if infos.pt_local then Dispose else Substitute infos + +let inPrimTokenInterp : prim_token_infos -> obj = + declare_object {(default_object "PRIM-TOKEN-INTERP") with + open_function = (fun i o -> if Int.equal i 1 then cache_prim_token_interpretation o); + cache_function = cache_prim_token_interpretation; + subst_function = subst_prim_token_interpretation; + classify_function = classify_prim_token_interpretation} + +let enable_prim_token_interpretation infos = + Lib.add_anonymous_leaf (inPrimTokenInterp infos) + +(** Compatibility. + Avoid the next two functions, they will now store unnecessary + objects in the library segment. Instead, combine + [register_*_interpretation] and [enable_prim_token_interpretation] + (the latter inside a [Mltop.declare_cache_obj]). +*) + +let fresh_string_of = + let count = ref 0 in + fun root -> count := !count+1; (string_of_int !count)^"_"^root + +let declare_numeral_interpreter ?(local=false) sc dir interp (patl,uninterp,b) = + let uid = fresh_string_of sc in + register_bignumeral_interpretation uid (interp,uninterp); + enable_prim_token_interpretation + { pt_local = local; + pt_scope = sc; + pt_uid = uid; + pt_required = dir; + pt_refs = List.map_filter glob_prim_constr_key patl; + pt_in_match = b } +let declare_string_interpreter ?(local=false) sc dir interp (patl,uninterp,b) = + let uid = fresh_string_of sc in + register_string_interpretation uid (interp,uninterp); + enable_prim_token_interpretation + { pt_local = local; + pt_scope = sc; + pt_uid = uid; + pt_required = dir; + pt_refs = List.map_filter glob_prim_constr_key patl; + pt_in_match = b } -let declare_rawnumeral_interpreter sc dir interp (patl,uninterp,inpat) = - declare_prim_token_interpreter sc - (fun cont ?loc -> function Numeral (n,s) -> delay dir interp ?loc (n,s) - | p -> cont ?loc p) - (patl, (fun r -> match uninterp r with - | None -> None - | Some (n,s) -> Some (Numeral (n,s))), inpat) - -let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) = - let interp' ?loc (n,s) = interp ?loc (ofNumeral n s) in - declare_prim_token_interpreter sc - (fun cont ?loc -> function Numeral (n,s) -> delay dir interp' ?loc (n,s) - | p -> cont ?loc p) - (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat) - -let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = - declare_prim_token_interpreter sc - (fun cont ?loc -> function String s -> delay dir interp ?loc s | p -> cont ?loc p) - (patl, (fun r -> mkString (uninterp r)), inpat) let check_required_module ?loc sc (sp,d) = try let _ = Nametab.global_of_path sp in () with Not_found -> - user_err ?loc ~hdr:"prim_token_interpreter" - (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") + match d with + | [] -> user_err ?loc ~hdr:"prim_token_interpreter" + (str "Cannot interpret in " ++ str sc ++ str " because " ++ pr_path sp ++ str " could not be found in the current environment.") + | _ -> user_err ?loc ~hdr:"prim_token_interpreter" + (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".") (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) @@ -476,9 +586,10 @@ let find_prim_token check_allowed ?loc p sc = pat, df with Not_found -> (* Try for a primitive numerical notation *) - let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc ?loc p in + let (spdir,uid) = String.Map.find sc !prim_token_interp_infos in check_required_module ?loc sc spdir; - let pat = interp () in + let interp = Hashtbl.find prim_token_interpreters uid in + let pat = InnerPrimToken.do_interp ?loc interp p in check_allowed pat; pat, ((dirpath (fst spdir),DirPath.empty),"") @@ -649,43 +760,34 @@ let entry_has_ident = function try String.Map.find s !entry_has_ident_map <= n with Not_found -> false let uninterp_prim_token c = - try - let (sc,numpr,_) = - KeyMap.find (glob_prim_constr_key c) !prim_token_key_table in - match numpr (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_ind_pattern ind args = - let ref = IndRef ind in - try - let k = RefKey (canonical_gr ref) in - let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in - if not b then raise Notation_ops.No_match; - let args' = List.map - (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in - let ref = DAst.make @@ GRef (ref,None) in - match numpr (AnyGlobConstr (DAst.make @@ GApp (ref,args'))) with - | None -> raise Notation_ops.No_match - | Some n -> (sc,n) - with Not_found -> raise Notation_ops.No_match + match glob_prim_constr_key c with + | None -> raise Notation_ops.No_match + | Some r -> + try + let (sc,uid,_) = Refmap.find r !prim_token_uninterp_infos in + let uninterp = Hashtbl.find prim_token_uninterpreters uid 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 = - try - let k = cases_pattern_key c in - let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in - if not b then raise Notation_ops.No_match; - let na,c = glob_constr_of_closed_cases_pattern c in - match numpr (AnyGlobConstr c) with - | None -> raise Notation_ops.No_match - | Some n -> (na,sc,n) - with Not_found -> raise Notation_ops.No_match + match glob_constr_of_closed_cases_pattern 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 ignore ((Hashtbl.find prim_token_interpreter_tab scope) n); true - with Not_found -> false in + try + let uid = snd (String.Map.find scope !prim_token_interp_infos) in + let interp = Hashtbl.find prim_token_interpreters uid in + let open InnerPrimToken in + match n, interp with + | Numeral _, (RawNumInterp _ | BigNumInterp _) -> true + | String _, StringInterp _ -> true + | _ -> false + with Not_found -> false + in let scopes = make_current_scopes local_scopes in Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes) @@ -1206,16 +1308,19 @@ let pr_visibility prglob = function let freeze _ = (!scope_map, !scope_stack, !arguments_scope, !delimiters_map, !notations_key_table, !scope_class_map, + !prim_token_interp_infos, !prim_token_uninterp_infos, !entry_coercion_map, !entry_has_global_map, !entry_has_ident_map) -let unfreeze (scm,scs,asc,dlm,fkm,clsc,coe,globs,ids) = +let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = scope_map := scm; scope_stack := scs; delimiters_map := dlm; arguments_scope := asc; notations_key_table := fkm; scope_class_map := clsc; + prim_token_interp_infos := ptii; + prim_token_uninterp_infos := ptui; entry_coercion_map := coe; entry_has_global_map := globs; entry_has_ident_map := ids @@ -1224,7 +1329,9 @@ let init () = init_scope_map (); delimiters_map := String.Map.empty; notations_key_table := KeyMap.empty; - scope_class_map := initial_scope_class_map + scope_class_map := initial_scope_class_map; + prim_token_interp_infos := String.Map.empty; + prim_token_uninterp_infos := Refmap.empty let _ = Summary.declare_summary "symbols" diff --git a/interp/notation.mli b/interp/notation.mli index c921606484..e5478eff48 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Bigint open Names open Libnames open Constrexpr @@ -75,24 +74,62 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name type notation_location = (DirPath.t * DirPath.t) * string type required_module = full_path * string list -type cases_pattern_status = bool (** true = use prim token in patterns *) +type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign -type 'a prim_token_interpreter = - ?loc:Loc.t -> 'a -> glob_constr +(** The unique id string below will be used to refer to a particular + registered interpreter/uninterpreter of numeral or string notation. + Using the same uid for different (un)interpreters will fail. + If at most one interpretation of prim token is used per scope, + then the scope name could be used as unique id. *) -type 'a prim_token_uninterpreter = - glob_constr list * (any_glob_constr -> 'a option) * cases_pattern_status +type prim_token_uid = string -type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign +type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> glob_constr +type 'a prim_token_uninterpreter = any_glob_constr -> 'a option + +type 'a prim_token_interpretation = + 'a prim_token_interpreter * 'a prim_token_uninterpreter + +val register_rawnumeral_interpretation : + ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit + +val register_bignumeral_interpretation : + ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit + +val register_string_interpretation : + ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit + +type prim_token_infos = { + pt_local : bool; (** Is this interpretation local? *) + pt_scope : scope_name; (** Concerned scope *) + pt_uid : prim_token_uid; (** Unique id "pointing" to (un)interp functions *) + pt_required : required_module; (** Module that should be loaded first *) + pt_refs : GlobRef.t list; (** Entry points during uninterpretation *) + pt_in_match : bool (** Is this prim token legal in match patterns ? *) +} + +(** Note: most of the time, the [pt_refs] field above will contain + inductive constructors (e.g. O and S for nat). But it could also be + injection functions such as IZR for reals. *) + +(** Activate a prim token interpretation whose unique id and functions + have already been registered. *) -val declare_rawnumeral_interpreter : scope_name -> required_module -> - rawnum prim_token_interpreter -> rawnum prim_token_uninterpreter -> unit +val enable_prim_token_interpretation : prim_token_infos -> unit -val declare_numeral_interpreter : scope_name -> required_module -> - bigint prim_token_interpreter -> bigint prim_token_uninterpreter -> unit +(** Compatibility. + Avoid the next two functions, they will now store unnecessary + objects in the library segment. Instead, combine + [register_*_interpretation] and [enable_prim_token_interpretation] + (the latter inside a [Mltop.declare_cache_obj]). +*) -val declare_string_interpreter : scope_name -> required_module -> - string prim_token_interpreter -> string prim_token_uninterpreter -> unit +val declare_numeral_interpreter : ?local:bool -> scope_name -> required_module -> + Bigint.bigint prim_token_interpreter -> + glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit +val declare_string_interpreter : ?local:bool -> scope_name -> required_module -> + string prim_token_interpreter -> + glob_constr list * string prim_token_uninterpreter * bool -> unit (** Return the [term]/[cases_pattern] bound to a primitive token in a given scope context*) @@ -110,8 +147,6 @@ val uninterp_prim_token : 'a glob_constr_g -> scope_name * prim_token val uninterp_prim_token_cases_pattern : 'a cases_pattern_g -> Name.t * scope_name * prim_token -val uninterp_prim_token_ind_pattern : - inductive -> cases_pattern list -> scope_name * prim_token val availability_of_prim_token : prim_token -> scope_name -> subscopes -> delimiters option option diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index ac4c6c52c6..fd9394025a 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -31,7 +31,6 @@ open Environ open Esubst let stats = ref false -let share = ref true (* Profiling *) let beta = ref 0 @@ -266,6 +265,7 @@ type 'a infos_cache = { i_env : env; i_sigma : existential -> constr option; i_rels : (Constr.rel_declaration * lazy_val) Range.t; + i_share : bool; } and 'a infos = { @@ -313,12 +313,13 @@ let ref_value_cache ({i_cache = cache} as infos) tab ref = let evar_value cache ev = cache.i_sigma ev -let create mk_cl flgs env evars = +let create ~repr ~share flgs env evars = let cache = - { i_repr = mk_cl; + { i_repr = repr; i_env = env; i_sigma = evars; i_rels = env.env_rel_context.env_rel_map; + i_share = share; } in { i_flags = flgs; i_cache = cache } @@ -384,8 +385,8 @@ let mk_red f = {norm=Red;term=f} (* Could issue a warning if no is still Red, pointing out that we loose sharing. *) -let update v1 no t = - if !share then +let update ~share v1 no t = + if share then (v1.norm <- no; v1.term <- t; v1) @@ -498,14 +499,16 @@ let compact_stack head stk = (* Be sure to create a new cell otherwise sharing would be lost by the update operation *) let h' = lft_fconstr depth head in - let _ = update m h'.norm h'.term in + (** The stack contains [Zupdate] marks only if in sharing mode *) + let _ = update ~share:true m h'.norm h'.term in strip_rec depth s | stk -> zshift depth stk in strip_rec 0 stk (* Put an update mark in the stack, only if needed *) -let zupdate m s = - if !share && begin match m.norm with Red -> true | _ -> false end +let zupdate info m s = + let share = info.i_cache.i_share in + if share && begin match m.norm with Red -> true | _ -> false end then let s' = compact_stack m s in let _ = m.term <- FLOCKED in @@ -698,7 +701,8 @@ let rec zip m stk = | Zshift(n)::s -> zip (lift_fconstr n m) s | Zupdate(rf)::s -> - zip (update rf m.norm m.term) s + (** The stack contains [Zupdate] marks only if in sharing mode *) + zip (update ~share:true rf m.norm m.term) s let fapp_stack (m,stk) = zip m stk @@ -718,7 +722,8 @@ let strip_update_shift_app_red head stk = strip_rec (Zapp args :: rstk) {norm=h.norm;term=FApp(h,args)} depth s | Zupdate(m)::s -> - strip_rec rstk (update m h.norm h.term) depth s + (** The stack contains [Zupdate] marks only if in sharing mode *) + strip_rec rstk (update ~share:true m h.norm h.term) depth s | stk -> (depth,List.rev rstk, stk) in strip_rec [] head 0 stk @@ -743,7 +748,8 @@ let get_nth_arg head n stk = List.rev (if Int.equal n 0 then rstk else (Zapp bef :: rstk)) in (Some (stk', args.(n)), append_stack aft s') | Zupdate(m)::s -> - strip_rec rstk (update m h.norm h.term) n s + (** The stack contains [Zupdate] mark only if in sharing mode *) + strip_rec rstk (update ~share:true m h.norm h.term) n s | s -> (None, List.rev rstk @ s) in strip_rec [] head n stk @@ -752,7 +758,8 @@ let get_nth_arg head n stk = let rec get_args n tys f e stk = match stk with Zupdate r :: s -> - let _hd = update r Cstr (FLambda(n,tys,f,e)) in + (** The stack contains [Zupdate] mark only if in sharing mode *) + let _hd = update ~share:true r Cstr (FLambda(n,tys,f,e)) in get_args n tys f e s | Zshift k :: s -> get_args n tys f (subs_shft (k,e)) s @@ -889,10 +896,10 @@ let unfold_projection info p = let rec knh info m stk = match m.term with | FLIFT(k,a) -> knh info a (zshift k stk) - | FCLOS(t,e) -> knht info e t (zupdate m stk) + | FCLOS(t,e) -> knht info e t (zupdate info m stk) | FLOCKED -> assert false - | FApp(a,b) -> knh info a (append_stack b (zupdate m stk)) - | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate m stk) + | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk)) + | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk) | FFix(((ri,n),(_,_,_)),_) -> (match get_nth_arg m ri.(n) stk with (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk') @@ -901,7 +908,7 @@ let rec knh info m stk = | FProj (p,c) -> (match unfold_projection info p with | None -> (m, stk) - | Some s -> knh info c (s :: zupdate m stk)) + | Some s -> knh info c (s :: zupdate info m stk)) (* cases where knh stops *) | (FFlex _|FLetIn _|FConstruct _|FEvar _| @@ -1019,10 +1026,11 @@ let rec zip_term zfun m stk = 2- tries to rebuild the term. If a closure still has to be computed, calls itself recursively. *) let rec kl info tab m = + let share = info.i_cache.i_share in if is_val m then (incr prune; term_of_fconstr m) else let (nm,s) = kni info tab m [] in - let () = if !share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *) + let () = if share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *) zip_term (kl info tab) (norm_head info tab nm) s (* no redex: go up for atoms and already normalized terms, go down @@ -1078,14 +1086,15 @@ let whd_stack infos tab m stk = match m.norm with knh infos m stk | Red | Cstr -> let k = kni infos tab m stk in - let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *) + let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k (* cache of constants: the body is computed only when needed. *) type clos_infos = fconstr infos let create_clos_infos ?(evars=fun _ -> None) flgs env = - create (fun _ _ c -> inject c) flgs env evars + let share = (Environ.typing_flags env).Declarations.share_reduction in + create ~share ~repr:(fun _ _ c -> inject c) flgs env evars let create_tab () = KeyTable.create 17 diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 1e3e7b48ac..6121b3a1ec 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -15,7 +15,6 @@ open Esubst (** Flags for profiling reductions. *) val stats : bool ref -val share : bool ref val with_stats: 'a Lazy.t -> 'a @@ -106,8 +105,13 @@ type 'a infos = { i_cache : 'a infos_cache } val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option -val create: ('a infos -> 'a infos_tab -> constr -> 'a) -> reds -> env -> - (existential -> constr option) -> 'a infos +val create: + repr:('a infos -> 'a infos_tab -> constr -> 'a) -> + share:bool -> + reds -> + env -> + (existential -> constr option) -> + 'a infos val create_tab : unit -> 'a infos_tab val evar_value : 'a infos_cache -> existential -> constr option diff --git a/kernel/cooking.ml b/kernel/cooking.ml index c06358054e..657478a106 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -24,6 +24,7 @@ open Declarations open Univ module NamedDecl = Context.Named.Declaration +module RelDecl = Context.Rel.Declaration (*s Cooking the constants. *) @@ -140,11 +141,31 @@ let expmod_constr cache modlist c = if is_empty_modlist modlist then c else substrec c -let abstract_constant_type = - List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c) +(** Transforms a named context into a rel context. Also returns the list of + variables [id1 ... idn] that need to be replaced by [Rel 1 ... Rel n] to + abstract a term that lived in that context. *) +let abstract_context hyps = + let fold decl (ctx, subst) = + let id, decl = match decl with + | NamedDecl.LocalDef (id, b, t) -> + let b = Vars.subst_vars subst b in + let t = Vars.subst_vars subst t in + id, RelDecl.LocalDef (Name id, b, t) + | NamedDecl.LocalAssum (id, t) -> + let t = Vars.subst_vars subst t in + id, RelDecl.LocalAssum (Name id, t) + in + (decl :: ctx, id :: subst) + in + Context.Named.fold_outside fold hyps ~init:([], []) + +let abstract_constant_type t (hyps, subst) = + let t = Vars.subst_vars subst t in + List.fold_left (fun c d -> mkProd_wo_LetIn d c) t hyps -let abstract_constant_body = - List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c) +let abstract_constant_body c (hyps, subst) = + let c = Vars.subst_vars subst c in + it_mkLambda_or_LetIn c hyps type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool @@ -173,6 +194,7 @@ let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c = let cache = RefTable.create 13 in let expmod = expmod_constr_subst cache modlist subst in let hyps = Context.Named.map expmod vars in + let hyps = abstract_context hyps in abstract_constant_body (expmod c) hyps let lift_univs cb subst auctx0 = @@ -207,12 +229,13 @@ let cook_constant ~hcons { from = cb; info } = let abstract, usubst, abs_ctx = abstract in let usubst, univs = lift_univs cb usubst abs_ctx in let expmod = expmod_constr_subst cache modlist usubst in - let hyps = Context.Named.map expmod abstract in + let hyps0 = Context.Named.map expmod abstract in + let hyps = abstract_context hyps0 in let map c = let c = abstract_constant_body (expmod c) hyps in if hcons then Constr.hcons c else c in - let body = on_body modlist (hyps, usubst, abs_ctx) + let body = on_body modlist (hyps0, usubst, abs_ctx) map cb.const_body in @@ -220,7 +243,7 @@ let cook_constant ~hcons { from = cb; info } = Context.Named.fold_outside (fun decl hyps -> List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) hyps) - hyps ~init:cb.const_hyps in + hyps0 ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in { cook_body = body; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 0811eb72fd..1d49550442 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -65,6 +65,7 @@ type typing_flags = { points are assumed to be total. *) check_universes : bool; (** If [false] universe constraints are not checked *) conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *) + share_reduction : bool; (** Use by-need reduction algorithm *) } (* some contraints are in constant_constraints, some other may be in diff --git a/kernel/declareops.ml b/kernel/declareops.ml index bbe4bc0dcb..51ec3defb3 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -21,6 +21,7 @@ let safe_flags oracle = { check_guarded = true; check_universes = true; conv_oracle = oracle; + share_reduction = true; } (** {6 Arities } *) @@ -305,13 +306,6 @@ let hcons_mind mib = mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; mind_universes = hcons_mind_universes mib.mind_universes } -(** {6 Stm machinery } *) - -let string_of_side_effect { Entries.eff } = match eff with - | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.Constant.to_string c ^ ")" - | Entries.SEscheme (cl,_) -> - "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.Constant.to_string c) cl) ^ ")" - (** Hashconsing of modules *) let hcons_functorize hty he hself f = match f with diff --git a/kernel/declareops.mli b/kernel/declareops.mli index f91e69807f..35490ceef9 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -11,7 +11,6 @@ open Declarations open Mod_subst open Univ -open Entries (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -39,10 +38,6 @@ val constant_is_polymorphic : constant_body -> bool val is_opaque : constant_body -> bool -(** Side effects *) - -val string_of_side_effect : side_effect -> string - (** {6 Inductive types} *) val eq_recarg : recarg -> recarg -> bool diff --git a/kernel/entries.ml b/kernel/entries.ml index 40873bea76..94248ad26b 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -120,11 +120,14 @@ type seff_env = Same as the constant_body's but not in an ephemeron *) | `Opaque of Constr.t * Univ.ContextSet.t ] -type side_eff = - | SEsubproof of Constant.t * Declarations.constant_body * seff_env - | SEscheme of (inductive * Constant.t * Declarations.constant_body * seff_env) list * string - -type side_effect = { - from_env : Declarations.structure_body CEphemeron.key; - eff : side_eff; +(** Not used by the kernel. *) +type side_effect_role = + | Subproof + | Schema of inductive * string + +type side_eff = { + seff_constant : Constant.t; + seff_body : Declarations.constant_body; + seff_env : seff_env; + seff_role : side_effect_role; } diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index cc35a70cbf..ad10c86945 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1067,12 +1067,11 @@ let ml_of_instance instance u = let tyn = fresh_lname Anonymous in let i = push_symbol (SymbMeta mv) in MLapp(MLprimitive Mk_meta, [|get_meta_code i; MLlocal tyn|]) - | Levar(evk,ty,args) -> - let tyn = fresh_lname Anonymous in + | Levar(evk, args) -> let i = push_symbol (SymbEvar evk) in + (** Arguments are *not* reversed in evar instances in native compilation *) let args = MLarray(Array.map (ml_of_lam env l) args) in - MLlet(tyn, ml_of_lam env l ty, - MLapp(MLprimitive Mk_evar, [|get_evar_code i;MLlocal tyn; args|])) + MLapp(MLprimitive Mk_evar, [|get_evar_code i; args|]) | Lprod(dom,codom) -> let dom = ml_of_lam env l dom in let codom = ml_of_lam env l codom in @@ -1749,7 +1748,7 @@ let pp_mllam fmt l = | Mk_cofix(start) -> Format.fprintf fmt "mk_cofix_accu %i" start | Mk_rel i -> Format.fprintf fmt "mk_rel_accu %i" i | Mk_var id -> - Format.fprintf fmt "mk_var_accu (Names.id_of_string \"%s\")" (string_of_id id) + Format.fprintf fmt "mk_var_accu (Names.Id.of_string \"%s\")" (string_of_id id) | Mk_proj -> Format.fprintf fmt "mk_proj_accu" | Is_int -> Format.fprintf fmt "is_int" | Cast_accu -> Format.fprintf fmt "cast_accu" diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 931b8bbc86..c75dde843e 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -64,7 +64,7 @@ and conv_atom env pb lvl a1 a2 cu = match a1, a2 with | Ameta (m1,_), Ameta (m2,_) -> if Int.equal m1 m2 then cu else raise NotConvertible - | Aevar (ev1,_,args1), Aevar (ev2,_,args2) -> + | Aevar (ev1, args1), Aevar (ev2, args2) -> if Evar.equal ev1 ev2 then Array.fold_right2 (conv_val env CONV lvl) args1 args2 cu else raise NotConvertible diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 5075bd3d14..2d8e2ba2f0 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -25,7 +25,7 @@ and lambda = | Lrel of Name.t * int | Lvar of Id.t | Lmeta of metavariable * lambda (* type *) - | Levar of Evar.t * lambda (* type *) * lambda array (* arguments *) + | Levar of Evar.t * lambda array (* arguments *) | Lprod of lambda * lambda | Llam of Name.t array * lambda | Llet of Name.t * lambda * lambda diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index cec0ee57d5..122fe95df4 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -23,7 +23,6 @@ exception NotClosed type evars = { evars_val : existential -> constr option; - evars_typ : existential -> types; evars_metas : metavariable -> types } (*s Constructors *) @@ -88,7 +87,7 @@ let get_const_prefix env c = let rec map_lam_with_binders g f n lam = match lam with | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ - | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> lam + | Lconstruct _ | Llazy | Lforce | Lmeta _ -> lam | Lprod(dom,codom) -> let dom' = f n dom in let codom' = f n codom in @@ -139,6 +138,9 @@ let rec map_lam_with_binders g f n lam = | Luint u -> let u' = map_uint g f n u in if u == u' then lam else Luint u' + | Levar (evk, args) -> + let args' = Array.Smart.map (f n) args in + if args == args' then lam else Levar (evk, args') and map_uint g f n u = match u with @@ -386,13 +388,10 @@ let is_lazy env prefix t = let evar_value sigma ev = sigma.evars_val ev -let evar_type sigma ev = sigma.evars_typ ev - let meta_type sigma mv = sigma.evars_metas mv let empty_evars = { evars_val = (fun _ -> None); - evars_typ = (fun _ -> assert false); evars_metas = (fun _ -> assert false) } let empty_ids = [||] @@ -420,9 +419,8 @@ let rec lambda_of_constr cache env sigma c = | Evar (evk,args as ev) -> (match evar_value sigma ev with | None -> - let ty = evar_type sigma ev in let args = Array.map (lambda_of_constr cache env sigma) args in - Levar(evk, lambda_of_constr cache env sigma ty, args) + Levar(evk, args) | Some t -> lambda_of_constr cache env sigma t) | Cast (c, _, _) -> lambda_of_constr cache env sigma c diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index efe1700cd7..7b20258929 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -15,7 +15,6 @@ open Nativeinstr (** This file defines the lambda code generation phase of the native compiler *) type evars = { evars_val : existential -> constr option; - evars_typ : existential -> types; evars_metas : metavariable -> types } val empty_evars : evars diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 91f6add1c3..3bf23f1468 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -63,7 +63,7 @@ type atom = | Acofixe of t array * t array * int * t | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t - | Aevar of Evar.t * t * t array + | Aevar of Evar.t * t array | Aproj of (inductive * int) * accumulator let accumulate_tag = 0 @@ -135,8 +135,8 @@ let mk_prod_accu s dom codom = let mk_meta_accu mv ty = mk_accu (Ameta (mv,ty)) -let mk_evar_accu ev ty args = - mk_accu (Aevar (ev,ty,args)) +let mk_evar_accu ev args = + mk_accu (Aevar (ev, args)) let mk_proj_accu kn c = mk_accu (Aproj (kn,c)) diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 6bbf15160c..10689941e8 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -53,7 +53,7 @@ type atom = | Acofixe of t array * t array * int * t | Aprod of Name.t * t * (t -> t) | Ameta of metavariable * t - | Aevar of Evar.t * t (* type *) * t array (* arguments *) + | Aevar of Evar.t * t array (* arguments *) | Aproj of (inductive * int) * accumulator (* Constructors *) @@ -70,7 +70,7 @@ val mk_prod_accu : Name.t -> t -> t -> t val mk_fix_accu : rec_pos -> int -> t array -> t array -> t val mk_cofix_accu : int -> t array -> t array -> t val mk_meta_accu : metavariable -> t -val mk_evar_accu : Evar.t -> t -> t array -> t +val mk_evar_accu : Evar.t -> t array -> t val mk_proj_accu : (inductive * int) -> accumulator -> t val upd_cofix : t -> t -> unit val force_cofix : t -> t diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f87ec9e023..6c87ff570f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -210,13 +210,8 @@ let get_opaque_body env cbo = (Opaqueproof.force_proof (Environ.opaque_tables env) opaque, Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) -type private_constant = Entries.side_effect type private_constants = Term_typing.side_effects -type private_constant_role = Term_typing.side_effect_role = - | Subproof - | Schema of inductive * string - let empty_private_constants = Term_typing.empty_seff let add_private = Term_typing.add_seff let concat_private = Term_typing.concat_seff @@ -225,44 +220,38 @@ let inline_private_constants_in_constr = Term_typing.inline_side_effects let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects let side_effects_of_private_constants = Term_typing.uniq_seff +let make_eff env cst r = + let open Entries in + let cbo = Environ.lookup_constant cst env.env in + { + seff_constant = cst; + seff_body = cbo; + seff_env = get_opaque_body env.env cbo; + seff_role = r; + } + let private_con_of_con env c = - let cbo = Environ.lookup_constant c env.env in - { Entries.from_env = CEphemeron.create env.revstruct; - Entries.eff = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) } + let open Entries in + let eff = [make_eff env c Subproof] in + add_private env.revstruct eff empty_private_constants let private_con_of_scheme ~kind env cl = - { Entries.from_env = CEphemeron.create env.revstruct; - Entries.eff = Entries.SEscheme( - List.map (fun (i,c) -> - let cbo = Environ.lookup_constant c env.env in - i, c, cbo, get_opaque_body env.env cbo) cl, - kind) } + let open Entries in + let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in + add_private env.revstruct eff empty_private_constants let universes_of_private eff = - let open Declarations in - List.fold_left - (fun acc { Entries.eff } -> - match eff with - | Entries.SEscheme (l,s) -> - List.fold_left - (fun acc (_,_,cb,c) -> - let acc = match c with - | `Nothing -> acc - | `Opaque (_, ctx) -> ctx :: acc - in - match cb.const_universes with - | Monomorphic_const ctx -> - ctx :: acc - | Polymorphic_const _ -> acc - ) - acc l - | Entries.SEsubproof (c, cb, e) -> - match cb.const_universes with - | Monomorphic_const ctx -> - ctx :: acc - | Polymorphic_const _ -> acc - ) - [] (Term_typing.uniq_seff eff) + let open Entries in + let fold acc eff = + let acc = match eff.seff_env with + | `Nothing -> acc + | `Opaque (_, ctx) -> ctx :: acc + in + match eff.seff_body.const_universes with + | Monomorphic_const ctx -> ctx :: acc + | Polymorphic_const _ -> acc + in + List.fold_left fold [] (Term_typing.uniq_seff eff) let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env @@ -489,7 +478,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - Constant.t * private_constant_role + Constant.t * Entries.side_effect_role let add_constant_aux no_section senv (kn, cb) = let l = pi3 (Constant.repr3 kn) in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index aca77ccd13..502e2970a1 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -41,29 +41,20 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment (** {6 Stm machinery } *) -type private_constant type private_constants -type private_constant_role = - | Subproof - | Schema of inductive * string - val side_effects_of_private_constants : - private_constants -> Entries.side_effect list + private_constants -> Entries.side_eff list (** Return the list of individual side-effects in the order of their creation. *) val empty_private_constants : private_constants -val add_private : private_constant -> private_constants -> private_constants -(** Add a constant to a list of private constants. The former must be more - recent than all constants appearing in the latter, i.e. one should not - create a dependency cycle. *) val concat_private : private_constants -> private_constants -> private_constants (** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in [e1] must be more recent than those of [e2]. *) -val private_con_of_con : safe_environment -> Constant.t -> private_constant -val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constant +val private_con_of_con : safe_environment -> Constant.t -> private_constants +val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constants val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output val inline_private_constants_in_constr : @@ -105,7 +96,7 @@ type global_declaration = | GlobalRecipe of Cooking.recipe type exported_private_constant = - Constant.t * private_constant_role + Constant.t * Entries.side_effect_role val export_private_constants : in_section:bool -> private_constants Entries.definition_entry -> diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 1f7ee145a2..43351737e5 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -27,16 +27,10 @@ module NamedDecl = Context.Named.Declaration (* Insertion of constants and parameters in environment. *) -let equal_eff e1 e2 = - let open Entries in - match e1, e2 with - | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } -> - Names.Constant.equal c1 c2 - | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } -> - CList.for_all2eq - (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2) - cl1 cl2 - | _ -> false +type side_effect = { + from_env : Declarations.structure_body CEphemeron.key; + eff : side_eff list; +} module SideEffects : sig @@ -48,17 +42,11 @@ sig end = struct -let compare_seff e1 e2 = match e1, e2 with -| SEsubproof (c1, _, _), SEsubproof (c2, _, _) -> Constant.CanOrd.compare c1 c2 -| SEscheme (cl1, _), SEscheme (cl2, _) -> - let cmp (_, c1, _, _) (_, c2, _, _) = Constant.CanOrd.compare c1 c2 in - CList.compare cmp cl1 cl2 -| SEsubproof _, SEscheme _ -> -1 -| SEscheme _, SEsubproof _ -> 1 - module SeffOrd = struct type t = side_effect -let compare e1 e2 = compare_seff e1.eff e2.eff +let compare e1 e2 = + let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in + List.compare cmp e1.eff e2.eff end module SeffSet = Set.Make(SeffOrd) @@ -83,10 +71,14 @@ type _ trust = | SideEffects : structure_body -> side_effects trust let uniq_seff_rev = SideEffects.repr -let uniq_seff l = List.rev (SideEffects.repr l) +let uniq_seff l = + let ans = List.rev (SideEffects.repr l) in + List.map_append (fun { eff } -> eff) ans let empty_seff = SideEffects.empty -let add_seff = SideEffects.add +let add_seff mb eff effs = + let from_env = CEphemeron.create mb in + SideEffects.add { eff; from_env } effs let concat_seff = SideEffects.concat let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff @@ -94,11 +86,8 @@ let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff let inline_side_effects env body ctx side_eff = (** First step: remove the constants that are still in the environment *) let filter { eff = se; from_env = mb } = - let cbl = match se with - | SEsubproof (c, cb, b) -> [c, cb, b] - | SEscheme (cl,_) -> - List.map (fun (_, c, cb, b) -> c, cb, b) cl - in + let map e = (e.seff_constant, e.seff_body, e.seff_env) in + let cbl = List.map map se in let not_exists (c,_,_) = try ignore(Environ.lookup_constant c env); false with Not_found -> true in @@ -468,58 +457,50 @@ let constant_entry_of_side_effect cb u = const_entry_inline_code = cb.const_inline_code } ;; -let turn_direct (kn,cb,u,r as orig) = - match cb.const_body, u with - | OpaqueDef _, `Opaque (b,c) -> - let pt = Future.from_val (b,c) in - kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r - | _ -> orig -;; - -type side_effect_role = - | Subproof - | Schema of inductive * string +let turn_direct orig = + let cb = orig.seff_body in + if Declareops.is_opaque cb then + let p = match orig.seff_env with + | `Opaque (b, c) -> (b, c) + | _ -> assert false + in + let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in + let cb = { cb with const_body } in + { orig with seff_body = cb } + else orig type exported_side_effect = Constant.t * constant_body * side_effect_role +let export_eff eff = + (eff.seff_constant, eff.seff_body, eff.seff_role) + let export_side_effects mb env c = let { const_entry_body = body } = c in let _, eff = Future.force body in let ce = { c with const_entry_body = Future.chain body (fun (b_ctx, _) -> b_ctx, ()) } in - let not_exists (c,_,_,_) = - try ignore(Environ.lookup_constant c env); false + let not_exists e = + try ignore(Environ.lookup_constant e.seff_constant env); false with Not_found -> true in let aux (acc,sl) { eff = se; from_env = mb } = - let cbl = match se with - | SEsubproof (c,cb,b) -> [c,cb,b,Subproof] - | SEscheme (cl,k) -> - List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in - let cbl = List.filter not_exists cbl in - if cbl = [] then acc, sl + let cbl = List.filter not_exists se in + if List.is_empty cbl then acc, sl else cbl :: acc, (mb,List.length cbl) :: sl in let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in let trusted = check_signatures mb signatures in - let push_seff env = function - | kn, cb, `Nothing, _ -> - begin - let env = Environ.add_constant kn cb env in - match cb.const_universes with - | Monomorphic_const ctx -> - Environ.push_context_set ~strict:true ctx env - | Polymorphic_const _ -> env - end - | kn, cb, `Opaque(_, ctx), _ -> - begin - let env = Environ.add_constant kn cb env in - match cb.const_universes with - | Monomorphic_const cstctx -> - let env = Environ.push_context_set ~strict:true cstctx env in - Environ.push_context_set ~strict:true ctx env - | Polymorphic_const _ -> env - end + let push_seff env eff = + let { seff_constant = kn; seff_body = cb } = eff in + let env = Environ.add_constant kn cb env in + match cb.const_universes with + | Polymorphic_const _ -> env + | Monomorphic_const ctx -> + let ctx = match eff.seff_env with + | `Nothing -> ctx + | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx + in + Environ.push_context_set ~strict:true ctx env in let rec translate_seff sl seff acc env = match seff with @@ -527,18 +508,22 @@ let export_side_effects mb env c = | cbs :: rest -> if Int.equal sl 0 then let env, cbs = - List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> + List.fold_left (fun (env,cbs) eff -> + let { seff_constant = kn; seff_body = ocb; seff_env = u } = eff in let ce = constant_entry_of_side_effect ocb u in let cb = translate_constant Pure env kn ce in - (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) + let eff = { eff with + seff_body = cb; + seff_env = `Nothing; + } in + (push_seff env eff, export_eff eff :: cbs)) (env,[]) cbs in translate_seff 0 rest (cbs @ acc) env else let cbs_len = List.length cbs in let cbs = List.map turn_direct cbs in let env = List.fold_left push_seff env cbs in - let ecbs = List.map (fun (kn,cb,u,r) -> - kn, cb, r) cbs in + let ecbs = List.map export_eff cbs in translate_seff (sl - cbs_len) rest (ecbs @ acc) env in translate_seff trusted seff [] env diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 6a0ff072f5..b05e05e4dc 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -38,24 +38,18 @@ val inline_entry_side_effects : yet type checked proof. *) val empty_seff : side_effects -val add_seff : side_effect -> side_effects -> side_effects +val add_seff : Declarations.structure_body -> Entries.side_eff list -> side_effects -> side_effects val concat_seff : side_effects -> side_effects -> side_effects (** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in [e1] must be more recent than those of [e2]. *) -val uniq_seff : side_effects -> side_effect list +val uniq_seff : side_effects -> side_eff list (** Return the list of individual side-effects in the order of their creation. *) -val equal_eff : side_effect -> side_effect -> bool - val translate_constant : 'a trust -> env -> Constant.t -> 'a constant_entry -> constant_body -type side_effect_role = - | Subproof - | Schema of inductive * string - type exported_side_effect = Constant.t * constant_body * side_effect_role diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 1c323e3ea2..60293fe864 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -62,6 +62,7 @@ type ('constr, 'types) ptype_error = | IllTypedRecBody of int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array | UnsatisfiedConstraints of Univ.Constraint.t + | UndeclaredUniverse of Univ.Level.t type type_error = (constr, types) ptype_error @@ -125,3 +126,6 @@ let error_elim_explain kp ki = let error_unsatisfied_constraints env c = raise (TypeError (env, UnsatisfiedConstraints c)) + +let error_undeclared_universe env l = + raise (TypeError (env, UndeclaredUniverse l)) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 20bf300ac3..9c6ef64b50 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -63,6 +63,7 @@ type ('constr, 'types) ptype_error = | IllTypedRecBody of int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array | UnsatisfiedConstraints of Univ.Constraint.t + | UndeclaredUniverse of Univ.Level.t type type_error = (constr, types) ptype_error @@ -108,3 +109,5 @@ val error_ill_typed_rec_body : val error_elim_explain : Sorts.family -> Sorts.family -> arity_error val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a + +val error_undeclared_universe : env -> Univ.Level.t -> 'a diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 7f36f3813f..25c1cbff3a 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -431,7 +431,28 @@ and execute_recdef env (names,lar,vdef) i = and execute_array env = Array.map (execute env) (* Derived functions *) + +let universe_levels_of_constr env c = + let rec aux s c = + match kind c with + | Const (c, u) -> + LSet.fold LSet.add (Instance.levels u) s + | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> + LSet.fold LSet.add (Instance.levels u) s + | Sort u when not (Sorts.is_small u) -> + let u = Sorts.univ_of_sort u in + LSet.fold LSet.add (Universe.levels u) s + | _ -> Constr.fold aux s c + in aux LSet.empty c + +let check_wellformed_universes env c = + let univs = universe_levels_of_constr env c in + try UGraph.check_declared_universes (universes env) univs + with UGraph.UndeclaredLevel u -> + error_undeclared_universe env u + let infer env constr = + let () = check_wellformed_universes env constr in let t = execute env constr in make_judge constr t @@ -449,11 +470,13 @@ let type_judgment env {uj_val=c; uj_type=t} = {utj_val = c; utj_type = s } let infer_type env constr = + let () = check_wellformed_universes env constr in let t = execute env constr in let s = check_type env constr t in {utj_val = constr; utj_type = s} let infer_v env cv = + let () = Array.iter (check_wellformed_universes env) cv in let jv = execute_array env cv in make_judgev cv jv @@ -461,9 +484,11 @@ let infer_v env cv = let infer_local_decl env id = function | Entries.LocalDefEntry c -> + let () = check_wellformed_universes env c in let t = execute env c in RelDecl.LocalDef (Name id, c, t) | Entries.LocalAssumEntry c -> + let () = check_wellformed_universes env c in let t = execute env c in RelDecl.LocalAssum (Name id, check_assumption env c t) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index bc624ba56d..95d71965df 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -529,6 +529,11 @@ let add_universe vlev strict g = let add_universe_unconstrained vlev g = fst (add_universe_gen vlev g) +exception UndeclaredLevel of Univ.Level.t +let check_declared_universes g us = + let check l = if not (UMap.mem l g.entries) then raise (UndeclaredLevel l) in + Univ.LSet.iter check us + exception Found_explanation of explanation let get_explanation strict u v g = diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 8c2d877b0b..752bf76270 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -55,6 +55,12 @@ val add_universe : Level.t -> bool -> t -> t (** Add a universe without (Prop,Set) <= u *) val add_universe_unconstrained : Level.t -> t -> t +(** Check that the universe levels are declared. Otherwise + @raise UndeclaredLevel l for the first undeclared level found. *) +exception UndeclaredLevel of Univ.Level.t + +val check_declared_universes : t -> Univ.LSet.t -> unit + (** {6 Pretty-printing of universes. } *) val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t diff --git a/library/global.ml b/library/global.ml index dcb20a280e..e833f71142 100644 --- a/library/global.ml +++ b/library/global.ml @@ -90,6 +90,7 @@ let push_context b c = globalize0 (Safe_typing.push_context b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) +let typing_flags () = Environ.typing_flags (env ()) let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) @@ -278,3 +279,9 @@ let register_inline c = globalize0 (Safe_typing.register_inline c) let set_strategy k l = GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l) +let set_reduction_sharing b = + let env = safe_env () in + let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in + let flags = { flags with Declarations.share_reduction = b } in + let env = Safe_typing.set_typing_flags flags env in + GlobalSafeEnv.set_safe_env env diff --git a/library/global.mli b/library/global.mli index b2a191ceeb..2819c187ed 100644 --- a/library/global.mli +++ b/library/global.mli @@ -30,6 +30,7 @@ val named_context : unit -> Constr.named_context (** Changing the (im)predicativity of the system *) val set_engagement : Declarations.engagement -> unit val set_typing_flags : Declarations.typing_flags -> unit +val typing_flags : unit -> Declarations.typing_flags (** Variables, Local definitions, constants, inductive types *) @@ -155,6 +156,8 @@ val register_inline : Constant.t -> unit val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit +val set_reduction_sharing : bool -> unit + (* Modifies the global state, registering new universes *) val current_modpath : unit -> ModPath.t diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 49e1cd7ec9..7cb5af787b 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -249,7 +249,7 @@ GRAMMAR EXTEND Gram record_field_declaration: [ [ id = global; bl = binders; ":="; c = lconstr -> - { (id, mkCLambdaN ~loc bl c) } ] ] + { (id, if bl = [] then c else mkCLambdaN ~loc bl c) } ] ] ; binder_constr: [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" -> diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml index c36b3b17bf..5cc1292c92 100644 --- a/parsing/notgram_ops.ml +++ b/parsing/notgram_ops.ml @@ -19,8 +19,10 @@ open Notation_gram let notation_level_map = Summary.ref ~name:"notation_level_map" NotationMap.empty let declare_notation_level ?(onlyprint=false) ntn level = - if NotationMap.mem ntn !notation_level_map then - anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level."); + try + let (level,onlyprint) = NotationMap.find ntn !notation_level_map in + if not onlyprint then anomaly (str "Notation " ++ pr_notation ntn ++ str " is already assigned a level.") + with Not_found -> notation_level_map := NotationMap.add ntn (level,onlyprint) !notation_level_map let level_of_notation ?(onlyprint=false) ntn = diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index dbbdbfa396..d779951180 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -52,8 +52,11 @@ let () = (* Rewriting orientation *) -let _ = Metasyntax.add_token_obj "<-" -let _ = Metasyntax.add_token_obj "->" +let _ = + Mltop.declare_cache_obj + (fun () -> Metasyntax.add_token_obj "<-"; + Metasyntax.add_token_obj "->") + "ltac_plugin" let pr_orient _prc _prlc _prt = function | true -> Pp.mt () diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 0bb9ccb1d8..1f2c722b34 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -144,7 +144,7 @@ let add ~deprecation kn b t = mactab := KNmap.add kn entry !mactab let replace kn path t = - let (path, _, _) = KerName.repr path in + let path = KerName.modpath path in let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in mactab := KNmap.modify kn entry !mactab diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 46fde41150..1dbacf0ff7 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -379,8 +379,9 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr = let ctx, last = EConstr.decompose_prod_assum sigma concl in let args = match EConstr.kind_of_type sigma last with | Term.AtomicType (hd, args) -> - assert(Ssrcommon.is_protect hd env sigma); - args + if Ssrcommon.is_protect hd env sigma then args + else Ssrcommon.errorstrm + (Pp.str "Too many names in intro pattern") | _ -> assert false in let case = args.(Array.length args-1) in if not(EConstr.Vars.closed0 sigma case) diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 47a59ba631..5e36fbeb81 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -83,8 +83,18 @@ let make_ascii_string n = let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r) +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + let _ = - Notation.declare_string_interpreter "char_scope" - (ascii_path,ascii_module) - interp_ascii_string - ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true) + let sc = "char_scope" in + register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = sc; + pt_uid = sc; + pt_required = (ascii_path,ascii_module); + pt_refs = [static_glob_Ascii]; + pt_in_match = true } diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4 new file mode 100644 index 0000000000..ec14df3baa --- /dev/null +++ b/plugins/syntax/g_numeral.ml4 @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +DECLARE PLUGIN "numeral_notation_plugin" + +open Numeral +open Pp +open Names +open Vernacinterp +open Ltac_plugin +open Stdarg +open Pcoq.Prim + +let pr_numnot_option _ _ _ = function + | Nop -> mt () + | Warning n -> str "(warning after " ++ str n ++ str ")" + | Abstract n -> str "(abstract after " ++ str n ++ str ")" + +ARGUMENT EXTEND numnotoption + PRINTED BY pr_numnot_option +| [ ] -> [ Nop ] +| [ "(" "warning" "after" bigint(waft) ")" ] -> [ Warning waft ] +| [ "(" "abstract" "after" bigint(n) ")" ] -> [ Abstract n ] +END + +VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF + | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) numnotoption(o) ] -> + [ vernac_numeral_notation (Locality.make_module_locality atts.locality) ty f g (Id.to_string sc) o ] +END diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml index f10f98e23b..d3ffe936a9 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -96,10 +96,19 @@ let uninterp_int31 (AnyGlobConstr i) = with Non_closed -> None +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + (* Actually declares the interpreter for int31 *) -let _ = Notation.declare_numeral_interpreter int31_scope - (int31_path, int31_module) - interp_int31 - ([DAst.make (GRef (int31_construct, None))], - uninterp_int31, - true) + +let _ = + register_bignumeral_interpretation int31_scope (interp_int31,uninterp_int31); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = int31_scope; + pt_uid = int31_scope; + pt_required = (int31_path,int31_module); + pt_refs = [int31_construct]; + pt_in_match = true } diff --git a/plugins/syntax/n_syntax.ml b/plugins/syntax/n_syntax.ml deleted file mode 100644 index 0e202be47f..0000000000 --- a/plugins/syntax/n_syntax.ml +++ /dev/null @@ -1,81 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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 Pp -open CErrors -open Names -open Bigint -open Positive_syntax_plugin.Positive_syntax - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "n_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -(**********************************************************************) -(* Parsing N via scopes *) -(**********************************************************************) - -open Globnames -open Glob_term - -let binnums = ["Coq";"Numbers";"BinNums"] - -let make_dir l = DirPath.make (List.rev_map Id.of_string l) -let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) - -(* TODO: temporary hack *) -let make_kn dir id = Globnames.encode_mind dir id - -let n_kn = make_kn (make_dir binnums) (Id.of_string "N") -let glob_n = IndRef (n_kn,0) -let path_of_N0 = ((n_kn,0),1) -let path_of_Npos = ((n_kn,0),2) -let glob_N0 = ConstructRef path_of_N0 -let glob_Npos = ConstructRef path_of_Npos - -let n_path = make_path binnums "N" - -let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@ - if not (Bigint.equal n zero) then - GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n]) - else - GRef(glob_N0, None) - -let error_negative ?loc = - user_err ?loc ~hdr:"interp_N" (str "No negative numbers in type \"N\".") - -let n_of_int ?loc n = - if is_pos_or_zero n then n_of_binnat ?loc true n - else error_negative ?loc - -(**********************************************************************) -(* Printing N via scopes *) -(**********************************************************************) - -let bignat_of_n n = DAst.with_val (function - | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a - | GRef (a,_) when GlobRef.equal a glob_N0 -> Bigint.zero - | _ -> raise Non_closed_number - ) n - -let uninterp_n (AnyGlobConstr p) = - try Some (bignat_of_n p) - with Non_closed_number -> None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for N *) - -let _ = Notation.declare_numeral_interpreter "N_scope" - (n_path,binnums) - n_of_int - ([DAst.make @@ GRef (glob_N0, None); - DAst.make @@ GRef (glob_Npos, None)], - uninterp_n, - true) diff --git a/plugins/syntax/n_syntax_plugin.mlpack b/plugins/syntax/n_syntax_plugin.mlpack deleted file mode 100644 index 4c56645f07..0000000000 --- a/plugins/syntax/n_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -N_syntax diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml deleted file mode 100644 index e158e0b516..0000000000 --- a/plugins/syntax/nat_syntax.ml +++ /dev/null @@ -1,85 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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) *) -(************************************************************************) - - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "nat_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -(* This file defines the printer for natural numbers in [nat] *) - -(*i*) -open Pp -open CErrors -open Names -open Glob_term -open Bigint -open Coqlib -(*i*) - -(**********************************************************************) -(* Parsing via scopes *) -(* For example, (nat_of_string "3") is <<(S (S (S O)))>> *) - -let threshold = of_int 5000 - -let warn_large_nat = - CWarnings.create ~name:"large-nat" ~category:"numbers" - (fun () -> strbrk "Stack overflow or segmentation fault happens when " ++ - strbrk "working with large numbers in nat (observed threshold " ++ - strbrk "may vary from 5000 to 70000 depending on your system " ++ - strbrk "limits and on the command executed).") - -let nat_of_int ?loc n = - if is_pos_or_zero n then begin - if less_than threshold n then warn_large_nat (); - let ref_O = DAst.make ?loc @@ GRef (glob_O, None) in - let ref_S = DAst.make ?loc @@ GRef (glob_S, None) in - let rec mk_nat acc n = - if n <> zero then - mk_nat (DAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n) - else - acc - in - mk_nat ref_O n - end - else - user_err ?loc ~hdr:"nat_of_int" - (str "Cannot interpret a negative number as a number of type nat") - -(************************************************************************) -(* Printing via scopes *) - -exception Non_closed_number - -let rec int_of_nat x = DAst.with_val (function - | GApp (r, [a]) -> - begin match DAst.get r with - | GRef (s,_) when GlobRef.equal s glob_S -> add_1 (int_of_nat a) - | _ -> raise Non_closed_number - end - | GRef (z,_) when GlobRef.equal z glob_O -> zero - | _ -> raise Non_closed_number - ) x - -let uninterp_nat (AnyGlobConstr p) = - try - Some (int_of_nat p) - with - Non_closed_number -> None - -(************************************************************************) -(* Declare the primitive parsers and printers *) - -let _ = - Notation.declare_numeral_interpreter "nat_scope" - (nat_path,datatypes_module_name) - nat_of_int - ([DAst.make @@ GRef (glob_S,None); DAst.make @@ GRef (glob_O,None)], uninterp_nat, true) diff --git a/plugins/syntax/nat_syntax_plugin.mlpack b/plugins/syntax/nat_syntax_plugin.mlpack deleted file mode 100644 index 39bdd62f47..0000000000 --- a/plugins/syntax/nat_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Nat_syntax diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml new file mode 100644 index 0000000000..fee93593d0 --- /dev/null +++ b/plugins/syntax/numeral.ml @@ -0,0 +1,478 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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 Pp +open Util +open Names +open Libnames +open Globnames +open Constrexpr +open Constrexpr_ops +open Constr + +(** * Numeral notation *) + +(** Reduction + + The constr [c] below isn't necessarily well-typed, since we + built it via an [mkApp] of a conversion function on a term + that starts with the right constructor but might be partially + applied. + + At least [c] is known to be evar-free, since it comes from + our own ad-hoc [constr_of_glob] or from conversions such + as [coqint_of_rawnum]. +*) + +let eval_constr env sigma (c : Constr.t) = + let c = EConstr.of_constr c in + let sigma,t = Typing.type_of env sigma c in + let c' = Vnorm.cbv_vm env sigma c t in + EConstr.Unsafe.to_constr c' + +(* For testing with "compute" instead of "vm_compute" : +let eval_constr env sigma (c : Constr.t) = + let c = EConstr.of_constr c in + let c' = Tacred.compute env sigma c in + EConstr.Unsafe.to_constr c' +*) + +let eval_constr_app env sigma c1 c2 = + eval_constr env sigma (mkApp (c1,[| c2 |])) + +exception NotANumber + +let warn_large_num = + CWarnings.create ~name:"large-number" ~category:"numbers" + (fun ty -> + strbrk "Stack overflow or segmentation fault happens when " ++ + strbrk "working with large numbers in " ++ pr_qualid ty ++ + strbrk " (threshold may vary depending" ++ + strbrk " on your system limits and on the command executed).") + +let warn_abstract_large_num = + CWarnings.create ~name:"abstract-large-number" ~category:"numbers" + (fun (ty,f) -> + strbrk "To avoid stack overflow, large numbers in " ++ + pr_qualid ty ++ strbrk " are interpreted as applications of " ++ + Printer.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".") + +let warn_abstract_large_num_no_op = + CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers" + (fun f -> + strbrk "The 'abstract after' directive has no effect when " ++ + strbrk "the parsing function (" ++ + Printer.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++ + strbrk "option type.") + +(** Comparing two raw numbers (base 10, big-endian, non-negative). + A bit nasty, but not critical: only used to decide when a + number is considered as large (see warnings above). *) + +exception Comp of int + +let rec rawnum_compare s s' = + let l = String.length s and l' = String.length s' in + if l < l' then - rawnum_compare s' s + else + let d = l-l' in + try + for i = 0 to d-1 do if s.[i] != '0' then raise (Comp 1) done; + for i = d to l-1 do + let c = Pervasives.compare s.[i] s'.[i-d] in + if c != 0 then raise (Comp c) + done; + 0 + with Comp c -> c + +(***********************************************************************) + +(** ** Conversion between Coq [Decimal.int] and internal raw string *) + +type int_ty = + { uint : Names.inductive; + int : Names.inductive } + +(** Decimal.Nil has index 1, then Decimal.D0 has index 2 .. Decimal.D9 is 11 *) + +let digit_of_char c = + assert ('0' <= c && c <= '9'); + Char.code c - Char.code '0' + 2 + +let char_of_digit n = + assert (2<=n && n<=11); + Char.chr (n-2 + Char.code '0') + +let coquint_of_rawnum uint str = + let nil = mkConstruct (uint,1) in + let rec do_chars s i acc = + if i < 0 then acc + else + let dg = mkConstruct (uint, digit_of_char s.[i]) in + do_chars s (i-1) (mkApp(dg,[|acc|])) + in + do_chars str (String.length str - 1) nil + +let coqint_of_rawnum inds (str,sign) = + let uint = coquint_of_rawnum inds.uint str in + mkApp (mkConstruct (inds.int, if sign then 1 else 2), [|uint|]) + +let rawnum_of_coquint c = + let rec of_uint_loop c buf = + match Constr.kind c with + | Construct ((_,1), _) (* Nil *) -> () + | App (c, [|a|]) -> + (match Constr.kind c with + | Construct ((_,n), _) (* D0 to D9 *) -> + let () = Buffer.add_char buf (char_of_digit n) in + of_uint_loop a buf + | _ -> raise NotANumber) + | _ -> raise NotANumber + in + let buf = Buffer.create 64 in + let () = of_uint_loop c buf in + if Int.equal (Buffer.length buf) 0 then + (* To avoid ambiguities between Nil and (D0 Nil), we choose + to not display Nil alone as "0" *) + raise NotANumber + else Buffer.contents buf + +let rawnum_of_coqint c = + match Constr.kind c with + | App (c,[|c'|]) -> + (match Constr.kind c with + | Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true) + | Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false) + | _ -> raise NotANumber) + | _ -> raise NotANumber + + +(***********************************************************************) + +(** ** Conversion between Coq [Z] and internal bigint *) + +type z_pos_ty = + { z_ty : Names.inductive; + pos_ty : Names.inductive } + +(** First, [positive] from/to bigint *) + +let rec pos_of_bigint posty n = + match Bigint.div2_with_rest n with + | (q, false) -> + let c = mkConstruct (posty, 2) in (* xO *) + mkApp (c, [| pos_of_bigint posty q |]) + | (q, true) when not (Bigint.equal q Bigint.zero) -> + let c = mkConstruct (posty, 1) in (* xI *) + mkApp (c, [| pos_of_bigint posty q |]) + | (q, true) -> + mkConstruct (posty, 3) (* xH *) + +let rec bigint_of_pos c = match Constr.kind c with + | Construct ((_, 3), _) -> (* xH *) Bigint.one + | App (c, [| d |]) -> + begin match Constr.kind c with + | Construct ((_, n), _) -> + begin match n with + | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d)) + | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d) + | n -> assert false (* no other constructor of type positive *) + end + | x -> raise NotANumber + end + | x -> raise NotANumber + +(** Now, [Z] from/to bigint *) + +let z_of_bigint { z_ty; pos_ty } n = + if Bigint.equal n Bigint.zero then + mkConstruct (z_ty, 1) (* Z0 *) + else + let (s, n) = + if Bigint.is_pos_or_zero n then (2, n) (* Zpos *) + else (3, Bigint.neg n) (* Zneg *) + in + let c = mkConstruct (z_ty, s) in + mkApp (c, [| pos_of_bigint pos_ty n |]) + +let bigint_of_z z = match Constr.kind z with + | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero + | App (c, [| d |]) -> + begin match Constr.kind c with + | Construct ((_, n), _) -> + begin match n with + | 2 -> (* Zpos *) bigint_of_pos d + | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d) + | n -> assert false (* no other constructor of type Z *) + end + | _ -> raise NotANumber + end + | _ -> raise NotANumber + +(** The uninterp function below work at the level of [glob_constr] + which is too low for us here. So here's a crude conversion back + to [constr] for the subset that concerns us. *) + +let rec constr_of_glob env sigma g = match DAst.get g with + | Glob_term.GRef (ConstructRef c, _) -> + let sigma,c = Evd.fresh_constructor_instance env sigma c in + sigma,mkConstructU c + | Glob_term.GApp (gc, gcl) -> + let sigma,c = constr_of_glob env sigma gc in + let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in + sigma,mkApp (c, Array.of_list cl) + | _ -> + raise NotANumber + +let rec glob_of_constr ?loc c = match Constr.kind c with + | App (c, ca) -> + let c = glob_of_constr ?loc c in + let cel = List.map (glob_of_constr ?loc) (Array.to_list ca) in + DAst.make ?loc (Glob_term.GApp (c, cel)) + | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None)) + | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None)) + | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None)) + | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None)) + | _ -> let (sigma, env) = Pfedit.get_current_context () in + CErrors.user_err ?loc + (strbrk "Unexpected term " ++ + Printer.pr_constr_env env sigma c ++ + strbrk " while parsing a numeral notation.") + +let no_such_number ?loc ty = + CErrors.user_err ?loc + (str "Cannot interpret this number as a value of type " ++ + pr_qualid ty) + +let interp_option ty ?loc c = + match Constr.kind c with + | App (_Some, [| _; c |]) -> glob_of_constr ?loc c + | App (_None, [| _ |]) -> no_such_number ?loc ty + | x -> let (sigma, env) = Pfedit.get_current_context () in + CErrors.user_err ?loc + (strbrk "Unexpected non-option term " ++ + Printer.pr_constr_env env sigma c ++ + strbrk " while parsing a numeral notation.") + +let uninterp_option c = + match Constr.kind c with + | App (_Some, [| _; x |]) -> x + | _ -> raise NotANumber + +let big2raw n = + if Bigint.is_pos_or_zero n then (Bigint.to_string n, true) + else (Bigint.to_string (Bigint.neg n), false) + +let raw2big (n,s) = + if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n) + +type target_kind = + | Int of int_ty (* Coq.Init.Decimal.int + uint *) + | UInt of Names.inductive (* Coq.Init.Decimal.uint *) + | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) + +type option_kind = Option | Direct +type conversion_kind = target_kind * option_kind + +type numnot_option = + | Nop + | Warning of raw_natural_number + | Abstract of raw_natural_number + +type numeral_notation_obj = + { to_kind : conversion_kind; + to_ty : GlobRef.t; + of_kind : conversion_kind; + of_ty : GlobRef.t; + num_ty : Libnames.qualid; (* for warnings / error messages *) + warning : numnot_option } + +let interp o ?loc n = + begin match o.warning with + | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 -> + warn_large_num o.num_ty + | _ -> () + end; + let c = match fst o.to_kind with + | Int int_ty -> coqint_of_rawnum int_ty n + | UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n) + | UInt _ (* n <= 0 *) -> no_such_number ?loc o.num_ty + | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n) + in + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in + let to_ty = EConstr.Unsafe.to_constr to_ty in + match o.warning, snd o.to_kind with + | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 -> + warn_abstract_large_num (o.num_ty,o.to_ty); + glob_of_constr ?loc (mkApp (to_ty,[|c|])) + | _ -> + let res = eval_constr_app env sigma to_ty c in + match snd o.to_kind with + | Direct -> glob_of_constr ?loc res + | Option -> interp_option o.num_ty ?loc res + +let uninterp o (Glob_term.AnyGlobConstr n) = + let env = Global.env () in + let sigma = Evd.from_env env in + let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in + let of_ty = EConstr.Unsafe.to_constr of_ty in + try + let sigma,n = constr_of_glob env sigma n in + let c = eval_constr_app env sigma of_ty n in + let c = if snd o.of_kind == Direct then c else uninterp_option c in + match fst o.of_kind with + | Int _ -> Some (rawnum_of_coqint c) + | UInt _ -> Some (rawnum_of_coquint c, true) + | Z _ -> Some (big2raw (bigint_of_z c)) + with + | Type_errors.TypeError _ | Pretype_errors.PretypeError _ -> None (* cf. eval_constr_app *) + | NotANumber -> None (* all other functions except big2raw *) + +(* Here we only register the interp and uninterp functions + for a particular Numeral Notation (determined by a unique + string). The actual activation of the notation will be done + later (cf. Notation.enable_prim_token_interpretation). + This registration of interp/uninterp must be added in the + libstack, otherwise this won't work through a Require. *) + +let load_numeral_notation _ (_, (uid,opts)) = + Notation.register_rawnumeral_interpretation + ~allow_overwrite:true uid (interp opts, uninterp opts) + +let cache_numeral_notation x = load_numeral_notation 1 x + +(* TODO: substitution ? + TODO: uid pas stable par substitution dans opts + *) + +let inNumeralNotation : string * numeral_notation_obj -> Libobject.obj = + Libobject.declare_object { + (Libobject.default_object "NUMERAL NOTATION") with + Libobject.cache_function = cache_numeral_notation; + Libobject.load_function = load_numeral_notation } + +let get_constructors ind = + let mib,oib = Global.lookup_inductive ind in + let mc = oib.Declarations.mind_consnames in + Array.to_list + (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc) + +let q_z = qualid_of_string "Coq.Numbers.BinNums.Z" +let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive" +let q_int = qualid_of_string "Coq.Init.Decimal.int" +let q_uint = qualid_of_string "Coq.Init.Decimal.uint" +let q_option = qualid_of_string "Coq.Init.Datatypes.option" + +let unsafe_locate_ind q = + match Nametab.locate q with + | IndRef i -> i + | _ -> raise Not_found + +let locate_ind q = + try unsafe_locate_ind q + with Not_found -> Nametab.error_global_not_found q + +let locate_z () = + try + Some { z_ty = unsafe_locate_ind q_z; + pos_ty = unsafe_locate_ind q_positive } + with Not_found -> None + +let locate_int () = + { uint = locate_ind q_uint; + int = locate_ind q_int } + +let has_type f ty = + let (sigma, env) = Pfedit.get_current_context () in + let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in + try let _ = Constrintern.interp_constr env sigma c in true + with Pretype_errors.PretypeError _ -> false + +let type_error_to f ty loadZ = + CErrors.user_err + (pr_qualid f ++ str " should go from Decimal.int to " ++ + pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ + fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ + (if loadZ then str " (require BinNums first)." else str ".")) + +let type_error_of g ty loadZ = + CErrors.user_err + (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ + str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ + str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ + (if loadZ then str " (require BinNums first)." else str ".")) + +let vernac_numeral_notation local ty f g scope opts = + let int_ty = locate_int () in + let z_pos_ty = locate_z () in + let tyc = Smartlocate.global_inductive_with_alias ty in + let to_ty = Smartlocate.global_with_alias f in + let of_ty = Smartlocate.global_with_alias g in + let cty = mkRefC ty in + let app x y = mkAppC (x,[y]) in + let cref q = mkRefC q in + let arrow x y = + mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) + in + let cZ = cref q_z in + let cint = cref q_int in + let cuint = cref q_uint in + let coption = cref q_option in + let opt r = app coption r in + let constructors = get_constructors tyc in + (* Check the type of f *) + let to_kind = + if has_type f (arrow cint cty) then Int int_ty, Direct + else if has_type f (arrow cint (opt cty)) then Int int_ty, Option + else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct + else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option + else + match z_pos_ty with + | Some z_pos_ty -> + if has_type f (arrow cZ cty) then Z z_pos_ty, Direct + else if has_type f (arrow cZ (opt cty)) then Z z_pos_ty, Option + else type_error_to f ty false + | None -> type_error_to f ty true + in + (* Check the type of g *) + let of_kind = + if has_type g (arrow cty cint) then Int int_ty, Direct + else if has_type g (arrow cty (opt cint)) then Int int_ty, Option + else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct + else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option + else + match z_pos_ty with + | Some z_pos_ty -> + if has_type g (arrow cty cZ) then Z z_pos_ty, Direct + else if has_type g (arrow cty (opt cZ)) then Z z_pos_ty, Option + else type_error_of g ty false + | None -> type_error_of g ty true + in + let o = { to_kind; to_ty; of_kind; of_ty; + num_ty = ty; + warning = opts } + in + (match opts, to_kind with + | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty + | _ -> ()); + (* TODO: un hash suffit-il ? *) + let uid = Marshal.to_string o [] in + let i = Notation.( + { pt_local = local; + pt_scope = scope; + pt_uid = uid; + pt_required = Nametab.path_of_global (IndRef tyc),[]; + pt_refs = constructors; + pt_in_match = true }) + in + Lib.add_anonymous_leaf (inNumeralNotation (uid,o)); + Notation.enable_prim_token_interpretation i diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli new file mode 100644 index 0000000000..83ede6f48f --- /dev/null +++ b/plugins/syntax/numeral.mli @@ -0,0 +1,22 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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 Libnames +open Constrexpr +open Vernacexpr + +(** * Numeral notation *) + +type numnot_option = + | Nop + | Warning of raw_natural_number + | Abstract of raw_natural_number + +val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit diff --git a/plugins/syntax/numeral_notation_plugin.mlpack b/plugins/syntax/numeral_notation_plugin.mlpack new file mode 100644 index 0000000000..f4d9cae3ff --- /dev/null +++ b/plugins/syntax/numeral_notation_plugin.mlpack @@ -0,0 +1,2 @@ +Numeral +G_numeral diff --git a/plugins/syntax/positive_syntax.ml b/plugins/syntax/positive_syntax.ml deleted file mode 100644 index 0c82e47445..0000000000 --- a/plugins/syntax/positive_syntax.ml +++ /dev/null @@ -1,101 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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 Pp -open CErrors -open Util -open Names -open Bigint - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "positive_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -exception Non_closed_number - -(**********************************************************************) -(* Parsing positive via scopes *) -(**********************************************************************) - -open Globnames -open Glob_term - -let binnums = ["Coq";"Numbers";"BinNums"] - -let make_dir l = DirPath.make (List.rev_map Id.of_string l) -let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) - -let positive_path = make_path binnums "positive" - -(* TODO: temporary hack *) -let make_kn dir id = Globnames.encode_mind dir id - -let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive") -let glob_positive = IndRef (positive_kn,0) -let path_of_xI = ((positive_kn,0),1) -let path_of_xO = ((positive_kn,0),2) -let path_of_xH = ((positive_kn,0),3) -let glob_xI = ConstructRef path_of_xI -let glob_xO = ConstructRef path_of_xO -let glob_xH = ConstructRef path_of_xH - -let pos_of_bignat ?loc x = - let ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in - let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in - let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in - let rec pos_of x = - match div2_with_rest x with - | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q]) - | (q,true) -> ref_xH - in - pos_of x - -let error_non_positive ?loc = - user_err ?loc ~hdr:"interp_positive" - (str "Only strictly positive numbers in type \"positive\".") - -let interp_positive ?loc n = - if is_strictly_pos n then pos_of_bignat ?loc n - else error_non_positive ?loc - -(**********************************************************************) -(* Printing positive via scopes *) -(**********************************************************************) - -let is_gr c gr = match DAst.get c with -| GRef (r, _) -> GlobRef.equal r gr -| _ -> false - -let rec bignat_of_pos x = DAst.with_val (function - | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) - | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one - | _ -> raise Non_closed_number - ) x - -let uninterp_positive (AnyGlobConstr p) = - try - Some (bignat_of_pos p) - with Non_closed_number -> - None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for positive *) -(************************************************************************) - -let _ = Notation.declare_numeral_interpreter "positive_scope" - (positive_path,binnums) - interp_positive - ([DAst.make @@ GRef (glob_xI, None); - DAst.make @@ GRef (glob_xO, None); - DAst.make @@ GRef (glob_xH, None)], - uninterp_positive, - true) diff --git a/plugins/syntax/positive_syntax_plugin.mlpack b/plugins/syntax/positive_syntax_plugin.mlpack deleted file mode 100644 index ac8f3c425c..0000000000 --- a/plugins/syntax/positive_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Positive_syntax diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 94aa143350..04946c158b 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -131,9 +131,19 @@ let uninterp_r (AnyGlobConstr p) = with Non_closed_number -> None -let _ = Notation.declare_numeral_interpreter "R_scope" - (r_path,["Coq";"Reals";"Rdefinitions"]) - r_of_int - ([DAst.make @@ GRef (glob_IZR, None)], - uninterp_r, - false) +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + +let r_scope = "R_scope" + +let _ = + register_bignumeral_interpretation r_scope (r_of_int,uninterp_r); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = r_scope; + pt_uid = r_scope; + pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]); + pt_refs = [glob_IZR]; + pt_in_match = false } diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index c22869f4d6..640bcfde91 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -64,10 +64,18 @@ let uninterp_string (AnyGlobConstr r) = with Non_closed_string -> None +open Notation + +let at_declare_ml_module f x = + Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name + let _ = - Notation.declare_string_interpreter "string_scope" - (string_path,["Coq";"Strings";"String"]) - interp_string - ([DAst.make @@ GRef (static_glob_String,None); - DAst.make @@ GRef (static_glob_EmptyString,None)], - uninterp_string, true) + let sc = "string_scope" in + register_string_interpretation sc (interp_string,uninterp_string); + at_declare_ml_module enable_prim_token_interpretation + { pt_local = false; + pt_scope = sc; + pt_uid = sc; + pt_required = (string_path,["Coq";"Strings";"String"]); + pt_refs = [static_glob_String; static_glob_EmptyString]; + pt_in_match = true } diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml deleted file mode 100644 index 2534162e36..0000000000 --- a/plugins/syntax/z_syntax.ml +++ /dev/null @@ -1,78 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \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 -open Bigint -open Positive_syntax_plugin.Positive_syntax - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "z_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -(**********************************************************************) -(* Parsing Z via scopes *) -(**********************************************************************) - -open Globnames -open Glob_term - -let binnums = ["Coq";"Numbers";"BinNums"] - -let make_dir l = DirPath.make (List.rev_map Id.of_string l) -let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) - -(* TODO: temporary hack *) -let make_kn dir id = Globnames.encode_mind dir id - -let z_path = make_path binnums "Z" -let z_kn = make_kn (make_dir binnums) (Id.of_string "Z") -let glob_z = IndRef (z_kn,0) -let path_of_ZERO = ((z_kn,0),1) -let path_of_POS = ((z_kn,0),2) -let path_of_NEG = ((z_kn,0),3) -let glob_ZERO = ConstructRef path_of_ZERO -let glob_POS = ConstructRef path_of_POS -let glob_NEG = ConstructRef path_of_NEG - -let z_of_int ?loc n = - if not (Bigint.equal n zero) then - let sgn, n = - if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in - DAst.make ?loc @@ GApp(DAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n]) - else - DAst.make ?loc @@ GRef(glob_ZERO, None) - -(**********************************************************************) -(* Printing Z via scopes *) -(**********************************************************************) - -let bigint_of_z z = DAst.with_val (function - | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a - | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) - | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero - | _ -> raise Non_closed_number - ) z - -let uninterp_z (AnyGlobConstr p) = - try - Some (bigint_of_z p) - with Non_closed_number -> None - -(************************************************************************) -(* Declaring interpreters and uninterpreters for Z *) - -let _ = Notation.declare_numeral_interpreter "Z_scope" - (z_path,binnums) - z_of_int - ([DAst.make @@ GRef (glob_ZERO, None); - DAst.make @@ GRef (glob_POS, None); - DAst.make @@ GRef (glob_NEG, None)], - uninterp_z, - true) diff --git a/plugins/syntax/z_syntax_plugin.mlpack b/plugins/syntax/z_syntax_plugin.mlpack deleted file mode 100644 index 411260c04c..0000000000 --- a/plugins/syntax/z_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -Z_syntax diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index da6e26cc4b..fc24e9b3a9 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -455,7 +455,8 @@ let cbv_norm infos constr = (* constant bodies are normalized at the first expansion *) let create_cbv_infos flgs env sigma = let infos = create - (fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c) + ~share:true (** Not used by cbv *) + ~repr:(fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c) flgs env (Reductionops.safe_evar_value sigma) in diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 5df41ef76a..246acfc92e 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -354,9 +354,8 @@ and nf_atom_type env sigma atom = let env = push_rel (LocalAssum (n,dom)) env in let codom,s2 = nf_type_sort env sigma (codom vn) in mkProd(n,dom,codom), Typeops.type_of_product env n s1 s2 - | Aevar(evk,ty,args) -> - let ty = nf_type env sigma ty in - nf_evar env sigma evk ty args + | Aevar(evk,args) -> + nf_evar env sigma evk args | Ameta(mv,ty) -> let ty = nf_type env sigma ty in mkMeta mv, ty @@ -398,22 +397,27 @@ and nf_predicate env sigma ind mip params v pT = mkLambda(name,dom,body) | _ -> nf_type env sigma v -and nf_evar env sigma evk ty args = +and nf_evar env sigma evk args = let evi = try Evd.find sigma evk with Not_found -> assert false in let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in + let ty = EConstr.Unsafe.to_constr @@ Evd.evar_concl evi in if List.is_empty hyps then begin assert (Int.equal (Array.length args) 0); mkEvar (evk, [||]), ty end else + (** Let-bound arguments are present in the evar arguments but not in the + type, so we turn the let into a product. *) + let hyps = Context.Named.drop_bodies hyps in let fold accu d = Term.mkNamedProd_or_LetIn d accu in let t = List.fold_left fold ty hyps in let ty, args = nf_args env sigma args t in - mkEvar (evk, Array.of_list args), ty + (** nf_args takes arguments in the reverse order but produces them in the + correct one, so we have to reverse them again for the evar node *) + mkEvar (evk, Array.rev_of_list args), ty let evars_of_evar_map sigma = { Nativelambda.evars_val = Evd.existential_opt_value0 sigma; - Nativelambda.evars_typ = Evd.existential_type0 sigma; Nativelambda.evars_metas = Evd.meta_type0 sigma } (* fork perf process, return profiler's process id *) diff --git a/proofs/refine.ml b/proofs/refine.ml index b64e7a2e5e..198e057ebc 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -49,20 +49,14 @@ let (pr_constrv,pr_constr) = (* Get the side-effect's constant declarations to update the monad's * environmnent *) -let add_if_undefined kn cb env = - try ignore(Environ.lookup_constant kn env); env - with Not_found -> Environ.add_constant kn cb env +let add_if_undefined env eff = + let open Entries in + try ignore(Environ.lookup_constant eff.seff_constant env); env + with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env (* Add the side effects to the monad's environment, if not already done. *) -let add_side_effect env = function - | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> - add_if_undefined kn cb env - | { Entries.eff = Entries.SEscheme (l,_) } -> - List.fold_left (fun env (_,kn,cb,eff_env) -> - add_if_undefined kn cb env) env l - -let add_side_effects env effects = - List.fold_left (fun env eff -> add_side_effect env eff) env effects +let add_side_effects env eff = + List.fold_left add_if_undefined env eff let generic_refine ~typecheck f gl = let sigma = Proofview.Goal.sigma gl in diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 21520f5d2b..e4013152e6 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -154,7 +154,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = | None -> add_suffix mib.mind_packets.(i).mind_typename suff in let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in declare_scheme kind [|ind,const|]; - const, Safe_typing.add_private + const, Safe_typing.concat_private (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff let define_individual_scheme kind mode names (mind,i as ind) = @@ -174,7 +174,7 @@ let define_mutual_scheme_base kind suff f mode names mind = let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; consts, - Safe_typing.add_private + Safe_typing.concat_private (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) (Array.to_list schemes)) eff @@ -187,7 +187,7 @@ let define_mutual_scheme kind mode names mind = let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in - s, Safe_typing.add_private + s, Safe_typing.concat_private (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind, s]) Safe_typing.empty_private_constants diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2a8ebe08ca..2d02c3ca6e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5007,7 +5007,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let evd = Evd.set_universe_context evd ectx in let open Safe_typing in let eff = private_con_of_con (Global.safe_env ()) cst in - let effs = add_private eff + let effs = concat_private eff Entries.(snd (Future.force const.const_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 117d6523a8..f8cedfff6e 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -23,7 +23,9 @@ Module Export Datatypes. Set Implicit Arguments. Notation nat := Coq.Init.Datatypes.nat. +Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. +Notation two := (S (S O)). Record prod (A B : Type) := pair { fst : A ; snd : B }. @@ -159,7 +161,7 @@ End Adjointify. (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), @@ -220,12 +222,12 @@ Section ORecursion. Definition O_indpaths {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o to O P == h o to O P) : g == h - := (fst (snd (extendable_to_O O 2) g h) p).1. + := (fst (snd (extendable_to_O O two) g h) p).1. Definition O_indpaths_beta {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o (to O P) == h o (to O P)) (x : P) : O_indpaths g h p (to O P x) = p x - := (fst (snd (extendable_to_O O 2) g h) p).2 x. + := (fst (snd (extendable_to_O O two) g h) p).2 x. End ORecursion. diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v index c3e0da1117..fd2380a070 100644 --- a/test-suite/bugs/closed/4533.v +++ b/test-suite/bugs/closed/4533.v @@ -17,7 +17,10 @@ Notation "A -> B" := (forall (_ : A), B) : type_scope. Module Export Datatypes. Set Implicit Arguments. Notation nat := Coq.Init.Datatypes.nat. + Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. + Notation one := (S O). + Notation two := (S one). Record prod (A B : Type) := pair { fst : A ; snd : B }. Notation "x * y" := (prod x y) : type_scope. Delimit Scope nat_scope with nat. @@ -109,7 +112,7 @@ Fixpoint ExtendableAlong@{i j k l} (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), @@ -160,17 +163,17 @@ Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses). Definition O_rec {P Q : Type} {Q_inO : In O Q} (f : P -> Q) : O P -> Q - := (fst (extendable_to_O O 1%nat) f).1. + := (fst (extendable_to_O O one) f).1. Definition O_rec_beta {P Q : Type} {Q_inO : In O Q} (f : P -> Q) (x : P) : O_rec f (to O P x) = f x - := (fst (extendable_to_O O 1%nat) f).2 x. + := (fst (extendable_to_O O one) f).2 x. Definition O_indpaths {P Q : Type} {Q_inO : In O Q} (g h : O P -> Q) (p : g o to O P == h o to O P) : g == h - := (fst (snd (extendable_to_O O 2) g h) p).1. + := (fst (snd (extendable_to_O O two) g h) p).1. End ORecursion. diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 4ad53bc629..13c47edc8f 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -19,6 +19,7 @@ Inductive sum (A B : Type) : Type := | inl : A -> sum A B | inr : B -> sum A B. Notation nat := Coq.Init.Datatypes.nat. +Notation O := Coq.Init.Datatypes.O. Notation S := Coq.Init.Datatypes.S. Notation "x + y" := (sum x y) : type_scope. @@ -449,7 +450,7 @@ Section Extensions. (n : nat) {A : Type@{i}} {B : Type@{j}} (f : A -> B) (C : B -> Type@{k}) : Type@{l} := match n with - | 0 => Unit@{l} + | O => Unit@{l} | S n => (forall (g : forall a, C (f a)), ExtensionAlong@{i j k l l} f C g) * forall (h k : forall b, C b), diff --git a/test-suite/bugs/closed/7867.v b/test-suite/bugs/closed/7867.v new file mode 100644 index 0000000000..d0c7902756 --- /dev/null +++ b/test-suite/bugs/closed/7867.v @@ -0,0 +1,4 @@ +(* Was a printer anomaly due to an internal lambda with no binders *) + +Class class := { foo : nat }. +Fail Instance : class := { foo := 0 ; bar := 0 }. diff --git a/test-suite/bugs/closed/7900.v b/test-suite/bugs/closed/7900.v new file mode 100644 index 0000000000..583ef0ef3b --- /dev/null +++ b/test-suite/bugs/closed/7900.v @@ -0,0 +1,53 @@ +Require Import Coq.Program.Program. +(* Set Universe Polymorphism. *) +Set Printing Universes. + +Axiom ALL : forall {T:Prop}, T. + +Inductive Expr : Set := E (a : Expr). + +Parameter Value : Set. + +Fixpoint eval (e: Expr): Value := + match e with + | E a => eval a + end. + +Class Quote (n: Value) : Set := + { quote: Expr + ; eval_quote: eval quote = n }. + +Program Definition quote_mult n + `{!Quote n} : Quote n := + {| quote := E (quote (n:=n)) |}. + +Set Printing Universes. +Next Obligation. +Proof. + Show Universes. + destruct Quote0 as [q eq]. + Show Universes. + rewrite <- eq. + clear n eq. + Show Universes. + apply ALL. + Show Universes. +Qed. +Print quote_mult_obligation_1. +(* quote_mult_obligation_1@{} = +let Top_internal_eq_rew_dep := + fun (A : Type@{Coq.Init.Logic.8}) (x : A) (P : forall a : A, x = a -> Type@{Top.5} (* <- XXX *)) + (f : P x eq_refl) (y : A) (e : x = y) => + match e as e0 in (_ = y0) return (P y0 e0) with + | eq_refl => f + end in +fun (n : Value) (Quote0 : Quote n) => +match Quote0 as q return (eval quote = n) with +| {| quote := q; eval_quote := eq0 |} => + Top_internal_eq_rew_dep Value (eval q) (fun (n0 : Value) (eq1 : eval q = n0) => eval quote = n0) + ALL n eq0 +end + : forall (n : Value) (Quote0 : Quote n), eval (E quote) = n + +quote_mult_obligation_1 is universe polymorphic +*) diff --git a/test-suite/bugs/closed/8106.v b/test-suite/bugs/closed/8106.v new file mode 100644 index 0000000000..a711c5adef --- /dev/null +++ b/test-suite/bugs/closed/8106.v @@ -0,0 +1,4 @@ +(* Was raising an anomaly "already assigned a level" on the second line *) + +Notation "c1 ; c2" := (c1 + c2) (only printing, at level 76, right associativity, c1 at level 76, c2 at level 76). +Notation "c1 ; c2" := (c1 + c2) (only parsing, at level 76, right associativity, c2 at level 76). diff --git a/test-suite/bugs/closed/8121.v b/test-suite/bugs/closed/8121.v new file mode 100644 index 0000000000..99267612ca --- /dev/null +++ b/test-suite/bugs/closed/8121.v @@ -0,0 +1,46 @@ +Require Import Coq.Strings.String. + +Section T. + Eval native_compute in let x := tt in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Eval native_compute in let _ := Set in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Eval native_compute in let _ := Prop in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End T. + +Section U0. + Let n : unit := tt. + Eval native_compute in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. native_compute. Abort. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End U0. + +Section S0. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval native_compute in _. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. native_compute. Abort. +(* Error: Anomaly "Uncaught exception Constr.DestKO." Please report at http://coq.inria.fr/bugs/. *) +End S0. + +Class T := { }. +Section S1. + Context {p : T}. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval native_compute in _. +(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *) + Goal exists tt : unit, tt = tt. eexists. native_compute. Abort. +(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *) +End S1. + +Class M := { m : Type }. +Section S2. + Context {p : M}. + Let LF : string := String (Coq.Strings.Ascii.Ascii false true false true false false false false) "". + Eval native_compute in _. +(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *) + Goal exists tt : unit, tt = tt. eexists. native_compute. Abort. +(* Error: Anomaly "File "pretyping/vnorm.ml", line 60, characters 9-15: Assertion failed." *) +End S2. diff --git a/test-suite/interactive/PrimNotation.v b/test-suite/interactive/PrimNotation.v new file mode 100644 index 0000000000..07986b0df3 --- /dev/null +++ b/test-suite/interactive/PrimNotation.v @@ -0,0 +1,64 @@ +(* Until recently, the Notation.declare_numeral_notation wasn't synchronized + w.r.t. backtracking. This should be ok now. + This test is pretty artificial (we must declare Z_scope for this to work). +*) + +Delimit Scope Z_scope with Z. +Open Scope Z_scope. +Check let v := 0 in v : nat. +(* let v := 0 in v : nat : nat *) +Require BinInt. +Check let v := 0 in v : BinNums.Z. +(* let v := 0 in v : BinNums.Z : BinNums.Z *) +Back 2. +Check let v := 0 in v : nat. +(* Expected answer: let v := 0 in v : nat : nat *) +(* Used to fail with: +Error: Cannot interpret in Z_scope without requiring first module BinNums. +*) + +Local Set Universe Polymorphism. +Delimit Scope punit_scope with punit. +Delimit Scope pcunit_scope with pcunit. +Delimit Scope int_scope with int. +Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int : int_scope. +Module A. + NonCumulative Inductive punit@{u} : Type@{u} := ptt. + Cumulative Inductive pcunit@{u} : Type@{u} := pctt. + Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. + Definition to_pcunit : Decimal.int -> option pcunit + := fun v => match v with 0%int => Some pctt | _ => None end. + Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. + Definition of_pcunit : pcunit -> Decimal.uint := fun _ => Nat.to_uint 0. + Numeral Notation punit to_punit of_punit : punit_scope. + Check let v := 0%punit in v : punit. + Back 2. + Numeral Notation pcunit to_pcunit of_pcunit : punit_scope. + Check let v := 0%punit in v : pcunit. +End A. +Reset A. +Local Unset Universe Polymorphism. +Module A. + Inductive punit : Set := ptt. + Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. + Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. + Numeral Notation punit to_punit of_punit : punit_scope. + Check let v := 0%punit in v : punit. +End A. +Local Set Universe Polymorphism. +Inductive punit@{u} : Type@{u} := ptt. +Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. +Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. +Numeral Notation punit to_punit of_punit : punit_scope. +Check let v := 0%punit in v : punit. +Back 6. (* check backtracking of registering universe polymorphic constants *) +Local Unset Universe Polymorphism. +Inductive punit : Set := ptt. +Definition to_punit : Decimal.int -> option punit + := fun v => match v with 0%int => Some ptt | _ => None end. +Definition of_punit : punit -> Decimal.uint := fun _ => Nat.to_uint 0. +Numeral Notation punit to_punit of_punit : punit_scope. +Check let v := 0%punit in v : punit. diff --git a/test-suite/success/ssr_delayed_clear_rename.v b/test-suite/ssr/delayed_clear_rename.v index 951e5aff79..951e5aff79 100644 --- a/test-suite/success/ssr_delayed_clear_rename.v +++ b/test-suite/ssr/delayed_clear_rename.v diff --git a/test-suite/ssr/ssr_rew_illtyped.v b/test-suite/ssr/rewrite_illtyped.v index 7358068c8d..7358068c8d 100644 --- a/test-suite/ssr/ssr_rew_illtyped.v +++ b/test-suite/ssr/rewrite_illtyped.v diff --git a/test-suite/success/Compat88.v b/test-suite/success/Compat88.v new file mode 100644 index 0000000000..e2045900d5 --- /dev/null +++ b/test-suite/success/Compat88.v @@ -0,0 +1,18 @@ +(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(** Check that various syntax usage is available without importing + relevant files. *) +Require Coq.Strings.Ascii Coq.Strings.String. +Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef. +Require Coq.Reals.Rdefinitions. +Require Coq.Numbers.Cyclic.Int31.Cyclic31. + +Require Import Coq.Compat.Coq88. (* XXX FIXME Should not need [Require], see https://github.com/coq/coq/issues/8311 *) + +Check String.String "a" String.EmptyString. +Check String.eqb "a" "a". +Check Nat.eqb 1 1. +Check BinNat.N.eqb 1 1. +Check BinInt.Z.eqb 1 1. +Check BinPos.Pos.eqb 1 1. +Check Rdefinitions.Rplus 1 1. +Check Int31.iszero 1. diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v new file mode 100644 index 0000000000..47ef381270 --- /dev/null +++ b/test-suite/success/NumeralNotations.v @@ -0,0 +1,302 @@ +(* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *) + +(* https://github.com/coq/coq/pull/8064#discussion_r202497516 *) +Module Test1. + Axiom hold : forall {A B C}, A -> B -> C. + Definition opaque3 (x : Decimal.int) : Decimal.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). + Numeral Notation Decimal.int opaque3 opaque3 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Fail Check 1%opaque. +End Test1. + +(* https://github.com/coq/coq/pull/8064#discussion_r202497990 *) +Module Test2. + Axiom opaque4 : option Decimal.int. + Definition opaque6 (x : Decimal.int) : option Decimal.int := opaque4. + Numeral Notation Decimal.int opaque6 opaque6 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Open Scope opaque_scope. + Fail Check 1%opaque. +End Test2. + +Module Test3. + Inductive silly := SILLY (v : Decimal.uint) (f : forall A, A -> A). + Definition to_silly (v : Decimal.uint) := SILLY v (fun _ x => x). + Definition of_silly (v : silly) := match v with SILLY v _ => v end. + Numeral Notation silly to_silly of_silly : silly_scope. + Delimit Scope silly_scope with silly. + Fail Check 1%silly. +End Test3. + + +Module Test4. + Polymorphic NonCumulative Inductive punit := ptt. + Polymorphic Definition pto_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. + Polymorphic Definition pto_punit_all (v : Decimal.uint) : punit := ptt. + Polymorphic Definition pof_punit (v : punit) : Decimal.uint := Nat.to_uint 0. + Definition to_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. + Definition of_punit (v : punit) : Decimal.uint := Nat.to_uint 0. + Polymorphic Definition pto_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end. + Polymorphic Definition pof_unit (v : unit) : Decimal.uint := Nat.to_uint 0. + 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. + Numeral Notation punit to_punit of_punit : pto. + Numeral Notation punit pto_punit of_punit : ppo. + Numeral Notation punit to_punit pof_punit : ptp. + Numeral Notation punit pto_punit pof_punit : ppp. + Numeral Notation unit to_unit of_unit : uto. + Delimit Scope pto with pto. + Delimit Scope ppo with ppo. + Delimit Scope ptp with ptp. + Delimit Scope ppp with ppp. + Delimit Scope uto with uto. + Check let v := 0%pto in v : punit. + Check let v := 0%ppo in v : punit. + Check let v := 0%ptp in v : punit. + Check let v := 0%ppp in v : punit. + Check let v := 0%uto in v : unit. + Fail Check 1%uto. + Fail Check (-1)%uto. + Numeral Notation unit pto_unit of_unit : upo. + Numeral Notation unit to_unit pof_unit : utp. + Numeral Notation unit pto_unit pof_unit : upp. + Delimit Scope upo with upo. + Delimit Scope utp with utp. + Delimit Scope upp with upp. + Check let v := 0%upo in v : unit. + Check let v := 0%utp in v : unit. + Check let v := 0%upp in v : unit. + + Polymorphic Definition pto_punits := pto_punit_all@{Set}. + Polymorphic Definition pof_punits := pof_punit@{Set}. + Numeral Notation punit pto_punits pof_punits : ppps (abstract after 1). + Delimit Scope ppps with ppps. + Universe u. + Constraint Set < u. + Check let v := 0%ppps in v : punit@{u}. (* Check that universes are refreshed *) + Fail Check let v := 1%ppps in v : punit@{u}. (* Note that universes are not refreshed here *) +End Test4. + +Module Test5. + Check S. (* At one point gave Error: Anomaly "Uncaught exception Pretype_errors.PretypeError(_, _, _)." Please report at http://coq.inria.fr/bugs/. *) +End Test5. + +Module Test6. + (* Check that numeral notations on enormous terms don't take forever to print/parse *) + (* Ackerman definition from https://stackoverflow.com/a/10303475/377022 *) + Fixpoint ack (n m : nat) : nat := + match n with + | O => S m + | S p => let fix ackn (m : nat) := + match m with + | O => ack p 1 + | S q => ack p (ackn q) + end + in ackn m + end. + + Timeout 1 Check (S (ack 4 4)). (* should be instantaneous *) + + Local Set Primitive Projections. + Record > wnat := wrap { unwrap :> nat }. + Definition to_uint (x : wnat) : Decimal.uint := Nat.to_uint x. + Definition of_uint (x : Decimal.uint) : wnat := Nat.of_uint x. + Module Export Scopes. + Delimit Scope wnat_scope with wnat. + End Scopes. + Module Export Notations. + Export Scopes. + Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). + End Notations. + Check let v := 0%wnat in v : wnat. + Check wrap O. + Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *) +End Test6. + +Module Test6_2. + Import Test6.Scopes. + Check Test6.wrap 0. + Import Test6.Notations. + Check let v := 0%wnat in v : Test6.wnat. +End Test6_2. + +Module Test7. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Decimal.uint }. + Delimit Scope wuint_scope with wuint. + Numeral Notation wuint wrap unwrap : wuint_scope. + Check let v := 0%wuint in v : wuint. + Check let v := 1%wuint in v : wuint. +End Test7. + +Module Test8. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Decimal.uint }. + Delimit Scope wuint8_scope with wuint8. + Delimit Scope wuint8'_scope with wuint8'. + Section with_var. + Context (dummy : unit). + Definition wrap' := let __ := dummy in wrap. + Definition unwrap' := let __ := dummy in unwrap. + Numeral Notation wuint wrap' unwrap' : wuint8_scope. + Check let v := 0%wuint8 in v : wuint. + End with_var. + Check let v := 0%wuint8 in v : nat. + Fail Check let v := 0%wuint8 in v : wuint. + Compute wrap (Nat.to_uint 0). + + Notation wrap'' := wrap. + Notation unwrap'' := unwrap. + Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope. + Check let v := 0%wuint8' in v : wuint. +End Test8. + +Module Test9. + Delimit Scope wuint9_scope with wuint9. + Delimit Scope wuint9'_scope with wuint9'. + Section with_let. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Decimal.uint }. + Let wrap' := wrap. + Let unwrap' := unwrap. + Local Notation wrap'' := wrap. + Local Notation unwrap'' := unwrap. + Numeral Notation wuint wrap' unwrap' : wuint9_scope. + Check let v := 0%wuint9 in v : wuint. + Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope. + Check let v := 0%wuint9' in v : wuint. + End with_let. + Check let v := 0%wuint9 in v : nat. + Fail Check let v := 0%wuint9 in v : wuint. +End Test9. + +Module Test10. + (* Test that it is only a warning to add abstract after to an optional parsing function *) + Definition to_uint (v : unit) := Nat.to_uint 0. + Definition of_uint (v : Decimal.uint) := match Nat.of_uint v with O => Some tt | _ => None end. + Definition of_any_uint (v : Decimal.uint) := tt. + Delimit Scope unit_scope with unit. + Delimit Scope unit2_scope with unit2. + Numeral Notation unit of_uint to_uint : unit_scope (abstract after 1). + Local Set Warnings Append "+abstract-large-number-no-op". + (* Check that there is actually a warning here *) + Fail Numeral Notation unit of_uint to_uint : unit2_scope (abstract after 1). + (* Check that there is no warning here *) + Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1). +End Test10. + +Module Test11. + (* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *) + Inductive unit11 := tt11. + Delimit Scope unit11_scope with unit11. + Goal True. + evar (to_uint : unit11 -> Decimal.uint). + evar (of_uint : Decimal.uint -> unit11). + Fail Numeral Notation unit11 of_uint to_uint : uint11_scope. + exact I. + Unshelve. + all: solve [ constructor ]. + Qed. +End Test11. + +Module Test12. + (* Test for numeral notations on context variables *) + Delimit Scope test12_scope with test12. + Section test12. + Context (to_uint : unit -> Decimal.uint) (of_uint : Decimal.uint -> unit). + + Numeral Notation unit of_uint to_uint : test12_scope. + Check let v := 1%test12 in v : unit. + End test12. +End Test12. + +Module Test13. + (* Test for numeral notations on notations which do not denote references *) + Delimit Scope test13_scope with test13. + Delimit Scope test13'_scope with test13'. + Delimit Scope test13''_scope with test13''. + Definition to_uint (x y : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Definition to_uint_good := to_uint tt. + Notation to_uint' := (to_uint tt). + Notation to_uint'' := (to_uint _). + Numeral Notation unit of_uint to_uint_good : test13_scope. + Check let v := 0%test13 in v : unit. + Fail Numeral Notation unit of_uint to_uint' : test13'_scope. + Fail Check let v := 0%test13' in v : unit. + Fail Numeral Notation unit of_uint to_uint'' : test13''_scope. + Fail Check let v := 0%test13'' in v : unit. +End Test13. + +Module Test14. + (* Test that numeral notations follow [Import], not [Require], and + also test that [Local Numeral Notation]s do not escape modules + nor sections. *) + Delimit Scope test14_scope with test14. + Delimit Scope test14'_scope with test14'. + Delimit Scope test14''_scope with test14''. + Delimit Scope test14'''_scope with test14'''. + Module Inner. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Local Numeral Notation unit of_uint to_uint : test14_scope. + Global Numeral Notation unit of_uint to_uint : test14'_scope. + Check let v := 0%test14 in v : unit. + Check let v := 0%test14' in v : unit. + End Inner. + Fail Check let v := 0%test14 in v : unit. + Fail Check let v := 0%test14' in v : unit. + Import Inner. + Fail Check let v := 0%test14 in v : unit. + Check let v := 0%test14' in v : unit. + Section InnerSection. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Local Numeral Notation unit of_uint to_uint : test14''_scope. + Fail Global Numeral Notation unit of_uint to_uint : test14'''_scope. + Check let v := 0%test14'' in v : unit. + Fail Check let v := 0%test14''' in v : unit. + End InnerSection. + Fail Check let v := 0%test14'' in v : unit. + Fail Check let v := 0%test14''' in v : unit. +End Test14. + +Module Test15. + (** Test module include *) + Delimit Scope test15_scope with test15. + Module Inner. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Numeral Notation unit of_uint to_uint : test15_scope. + Check let v := 0%test15 in v : unit. + End Inner. + Module Inner2. + Include Inner. + Check let v := 0%test15 in v : unit. + End Inner2. + Import Inner Inner2. + Check let v := 0%test15 in v : unit. +End Test15. + +Module Test16. + (** Test functors *) + Delimit Scope test16_scope with test16. + Module Type A. + Axiom T : Set. + Axiom t : T. + End A. + Module F (a : A). + Inductive Foo := foo (_ : a.T). + Definition to_uint (x : Foo) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : Foo := foo a.t. + Global Numeral Notation Foo of_uint to_uint : test16_scope. + Check let v := 0%test16 in v : Foo. + End F. + Module a <: A. + Definition T : Set := unit. + Definition t : T := tt. + End a. + Module Import f := F a. + (** Ideally this should work, but it should definitely not anomaly *) + Fail Check let v := 0%test16 in v : Foo. +End Test16. diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v index 4142af05d2..578425bfb5 100644 --- a/theories/Compat/Coq88.v +++ b/theories/Compat/Coq88.v @@ -9,3 +9,17 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.8 *) +(** In Coq 8.9, prim token notations follow [Import] rather than + [Require]. So we make all of the relevant notations accessible in + compatibility mode. *) +Require Coq.Strings.Ascii Coq.Strings.String. +Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef. +Require Coq.Reals.Rdefinitions. +Require Coq.Numbers.Cyclic.Int31.Int31. +Declare ML Module "string_syntax_plugin". +Declare ML Module "ascii_syntax_plugin". +Declare ML Module "r_syntax_plugin". +Declare ML Module "int31_syntax_plugin". +Numeral Notation BinNums.Z BinIntDef.Z.of_int BinIntDef.Z.to_int : Z_scope. +Numeral Notation BinNums.positive BinPosDef.Pos.of_int BinPosDef.Pos.to_int : positive_scope. +Numeral Notation BinNums.N BinNatDef.N.of_int BinNatDef.N.to_int : N_scope. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 05b741f0ac..1e6843d511 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -12,7 +12,6 @@ Set Implicit Arguments. Require Import Notations. Require Import Logic. -Declare ML Module "nat_syntax_plugin". (********************************************************************) (** * Datatypes with zero and one element *) diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 57163b1b07..1ff00ec11c 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -42,10 +42,10 @@ Notation zero := (D0 Nil). Inductive int := Pos (d:uint) | Neg (d:uint). -Delimit Scope uint_scope with uint. -Bind Scope uint_scope with uint. -Delimit Scope int_scope with int. -Bind Scope int_scope with int. +Delimit Scope dec_uint_scope with uint. +Bind Scope dec_uint_scope with uint. +Delimit Scope dec_int_scope with int. +Bind Scope dec_int_scope with int. (** This representation favors simplicity over canonicity. For normalizing numbers, we need to remove head zero digits, @@ -161,3 +161,9 @@ with succ_double d := end. End Little. + +(** Pseudo-conversion functions used when declaring + Numeral Notations on [uint] and [int]. *) + +Definition uint_of_uint (i:uint) := i. +Definition int_of_int (i:int) := i. diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index ad1bc717c4..eb4ba0e5e6 100644 --- a/theories/Init/Nat.v +++ b/theories/Init/Nat.v @@ -24,6 +24,10 @@ Definition t := nat. (** ** Constants *) +Local Notation "0" := O. +Local Notation "1" := (S O). +Local Notation "2" := (S (S O)). + Definition zero := 0. Definition one := 1. Definition two := 2. diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index d5322d0945..65e5e76a22 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -31,6 +31,7 @@ Require Import Logic. Require Coq.Init.Nat. Open Scope nat_scope. +Local Notation "0" := O. Definition eq_S := f_equal S. Definition f_equal_nat := f_equal (A:=nat). diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 802f18c0f2..6d98bcb34a 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -19,9 +19,24 @@ Require Export Peano. Require Export Coq.Init.Wf. Require Export Coq.Init.Tactics. Require Export Coq.Init.Tauto. -(* Initially available plugins - (+ nat_syntax_plugin loaded in Datatypes) *) +(* Some initially available plugins. See also: + - ltac_plugin (in Notations) + - tauto_plugin (in Tauto). +*) Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". +Declare ML Module "numeral_notation_plugin". + +(* Parsing / printing of decimal numbers *) +Arguments Nat.of_uint d%dec_uint_scope. +Arguments Nat.of_int d%dec_int_scope. +Numeral Notation Decimal.uint Decimal.uint_of_uint Decimal.uint_of_uint + : dec_uint_scope. +Numeral Notation Decimal.int Decimal.int_of_int Decimal.int_of_int + : dec_int_scope. + +(* Parsing / printing of [nat] numbers *) +Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5000). + (* Default substrings not considered by queries like SearchAbout *) Add Search Blacklist "_subproof" "_subterm" "Private_". diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 5d3ec5abc7..bd27f94abd 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -930,6 +930,8 @@ Bind Scope N_scope with N.t N. (** Exportation of notations *) +Numeral Notation N N.of_uint N.to_uint : N_scope. + Infix "+" := N.add : N_scope. Infix "-" := N.sub : N_scope. Infix "*" := N.mul : N_scope. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 5de75537cb..be12fffaaf 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -13,6 +13,10 @@ Require Import BinPos. Local Open Scope N_scope. +Local Notation "0" := N0. +Local Notation "1" := (Npos 1). +Local Notation "2" := (Npos 2). + (**********************************************************************) (** * Binary natural numbers, definitions of operations *) (**********************************************************************) @@ -398,4 +402,9 @@ Definition to_uint n := Definition to_int n := Decimal.Pos (to_uint n). +Numeral Notation N of_uint to_uint : N_scope. + End N. + +(** Re-export the notation for those who just [Import NatIntDef] *) +Numeral Notation N N.of_uint N.to_uint : N_scope. diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v new file mode 100644 index 0000000000..c7e3999691 --- /dev/null +++ b/theories/Numbers/AltBinNotations.v @@ -0,0 +1,69 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \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) *) +(************************************************************************) + +(** * Alternative Binary Numeral Notations *) + +(** Faster but less safe parsers and printers of [positive], [N], [Z]. *) + +(** By default, literals in types [positive], [N], [Z] are parsed and + printed via the [Numeral Notation] command, by conversion from/to + the [Decimal.int] representation. When working with numbers with + thousands of digits and more, conversion from/to [Decimal.int] can + become significantly slow. If that becomes a problem for your + development, this file provides some alternative [Numeral + Notation] commmands that use [Z] as bridge type. To enable these + commands, just be sure to [Require] this file after other files + defining numeral notations. + + Note: up to Coq 8.8, literals in types [positive], [N], [Z] were + parsed and printed using a native ML library of arbitrary + precision integers named bigint.ml. From 8.9, the default is to + parse and print using a Coq library converting sequences of + digits, hence reducing the amount of ML code to trust. But this + method is slower. This file then gives access to the legacy + method, trading efficiency against a larger ML trust base relying + on bigint.ml. *) + +Require Import BinNums. + +(** [positive] *) + +Definition pos_of_z z := + match z with + | Zpos p => Some p + | _ => None + end. + +Definition pos_to_z p := Zpos p. + +Numeral Notation positive pos_of_z pos_to_z : positive_scope. + +(** [N] *) + +Definition n_of_z z := + match z with + | Z0 => Some N0 + | Zpos p => Some (Npos p) + | Zneg _ => None + end. + +Definition n_to_z n := + match n with + | N0 => Z0 + | Npos p => Zpos p + end. + +Numeral Notation N n_of_z n_to_z : N_scope. + +(** [Z] *) + +Definition z_of_z (z:Z) := z. + +Numeral Notation Z z_of_z z_of_z : Z_scope. diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index d5eb4f2681..3ba9d1f5ed 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -12,15 +12,11 @@ Set Implicit Arguments. -Declare ML Module "positive_syntax_plugin". -Declare ML Module "n_syntax_plugin". -Declare ML Module "z_syntax_plugin". - (** [positive] is a datatype representing the strictly positive integers in a binary way. Starting from 1 (represented by [xH]), one can add a new least significant digit via [xO] (digit 0) or [xI] (digit 1). - Numbers in [positive] can also be denoted using a decimal notation; - e.g. [6%positive] abbreviates [xO (xI xH)] *) + Numbers in [positive] will also be denoted using a decimal notation; + e.g. [6%positive] will abbreviate [xO (xI xH)] *) Inductive positive : Set := | xI : positive -> positive @@ -34,8 +30,8 @@ Arguments xI _%positive. (** [N] is a datatype representing natural numbers in a binary way, by extending the [positive] datatype with a zero. - Numbers in [N] can also be denoted using a decimal notation; - e.g. [6%N] abbreviates [Npos (xO (xI xH))] *) + Numbers in [N] will also be denoted using a decimal notation; + e.g. [6%N] will abbreviate [Npos (xO (xI xH))] *) Inductive N : Set := | N0 : N @@ -49,8 +45,8 @@ Arguments Npos _%positive. An integer is either zero or a strictly positive number (coded as a [positive]) or a strictly negative number (whose opposite is stored as a [positive] value). - Numbers in [Z] can also be denoted using a decimal notation; - e.g. [(-6)%Z] abbreviates [Zneg (xO (xI xH))] *) + Numbers in [Z] will also be denoted using a decimal notation; + e.g. [(-6)%Z] will abbreviate [Zneg (xO (xI xH))] *) Inductive Z : Set := | Z0 : Z diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index bd4f0279d4..ec480bb1eb 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -23,8 +23,6 @@ Require Import Zpow_facts. Require Import CyclicAxioms. Require Import ROmega. -Declare ML Module "int31_syntax_plugin". - Local Open Scope nat_scope. Local Open Scope int31_scope. @@ -128,7 +126,7 @@ Section Basics. Lemma nshiftl_S_tail : forall n x, nshiftl x (S n) = nshiftl (shiftl x) n. - Proof. + Proof. intros n; elim n; simpl; intros; now f_equal. Qed. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 9f8da831d8..39af62c32f 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -15,6 +15,8 @@ Require Import Wf_nat. Require Export ZArith. Require Export DoubleType. +Declare ML Module "int31_syntax_plugin". + (** * 31-bit integers *) (** This file contains basic definitions of a 31-bit integer diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 000d895e10..dcaae1606d 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -1871,6 +1871,8 @@ Bind Scope positive_scope with Pos.t positive. (** Exportation of notations *) +Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. + Infix "+" := Pos.add : positive_scope. Infix "-" := Pos.sub : positive_scope. Infix "*" := Pos.mul : positive_scope. diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 070314746a..7f30733559 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -26,6 +26,8 @@ Require Export BinNums. for the number 6 (which is 110 in binary notation). *) +Local Notation "1" := xH. + Notation "p ~ 1" := (xI p) (at level 7, left associativity, format "p '~' '1'") : positive_scope. Notation "p ~ 0" := (xO p) @@ -325,14 +327,14 @@ Definition sqrtrem_step (f g:positive->positive) p := let r' := g (f r) in if s' <=? r' then (s~1, sub_mask r' s') else (s~0, IsPos r') - | (s,_) => (s~0, sub_mask (g (f 1)) 4) + | (s,_) => (s~0, sub_mask (g (f 1)) 1~0~0) end. Fixpoint sqrtrem p : positive * mask := match p with | 1 => (1,IsNul) - | 2 => (1,IsPos 1) - | 3 => (1,IsPos 2) + | 1~0 => (1,IsPos 1) + | 1~1 => (1,IsPos 1~0) | p~0~0 => sqrtrem_step xO xO (sqrtrem p) | p~0~1 => sqrtrem_step xO xI (sqrtrem p) | p~1~0 => sqrtrem_step xI xO (sqrtrem p) @@ -614,4 +616,9 @@ Definition to_uint p := Decimal.rev (to_little_uint p). Definition to_int n := Decimal.Pos (to_uint n). +Numeral Notation positive of_int to_uint : positive_scope. + End Pos. + +(** Re-export the notation for those who just [Import BinPosDef] *) +Numeral Notation positive Pos.of_int Pos.to_uint : positive_scope. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index cf7397b57e..a11d491a8b 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1248,6 +1248,8 @@ Bind Scope Z_scope with Z.t Z. (** Re-export Notations *) +Numeral Notation Z Z.of_int Z.to_int : Z_scope. + Infix "+" := Z.add : Z_scope. Notation "- x" := (Z.opp x) : Z_scope. Infix "-" := Z.sub : Z_scope. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index db4de0b90c..8cb62622db 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -14,6 +14,10 @@ Require Import BinPos BinNat. Local Open Scope Z_scope. +Local Notation "0" := Z0. +Local Notation "1" := (Zpos 1). +Local Notation "2" := (Zpos 2). + (***********************************************************) (** * Binary Integers, Definitions of Operations *) (***********************************************************) @@ -53,7 +57,7 @@ Definition succ_double x := Definition pred_double x := match x with - | 0 => -1 + | 0 => neg 1 | neg p => neg p~1 | pos p => pos (Pos.pred_double p) end. @@ -104,7 +108,7 @@ Definition succ x := x + 1. (** ** Predecessor *) -Definition pred x := x + -1. +Definition pred x := x + neg 1. (** ** Subtraction *) @@ -171,7 +175,7 @@ Definition sgn z := match z with | 0 => 0 | pos p => 1 - | neg p => -1 + | neg p => neg 1 end. (** Boolean equality and comparisons *) @@ -635,4 +639,9 @@ Definition lxor a b := | neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b)) end. +Numeral Notation Z of_int to_int : Z_scope. + End Z. + +(** Re-export the notation for those who just [Import BinIntDef] *) +Numeral Notation Z Z.of_int Z.to_int : Z_scope. diff --git a/vernac/himsg.ml b/vernac/himsg.ml index b9c47ff475..a4650cfd92 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -679,6 +679,11 @@ let explain_unsatisfied_constraints env sigma cst = Univ.pr_constraints (Termops.pr_evd_level sigma) cst ++ spc () ++ str "(maybe a bugged tactic)." +let explain_undeclared_universe env sigma l = + strbrk "Undeclared universe: " ++ + Termops.pr_evd_level sigma l ++ + spc () ++ str "(maybe a bugged tactic)." + let explain_type_error env sigma err = let env = make_all_name_different env sigma in match err with @@ -716,6 +721,8 @@ let explain_type_error env sigma err = explain_wrong_case_info env ind ci | UnsatisfiedConstraints cst -> explain_unsatisfied_constraints env sigma cst + | UndeclaredUniverse l -> + explain_undeclared_universe env sigma l let pr_position (cl,pos) = let clpos = match cl with @@ -1299,6 +1306,7 @@ let map_ptype_error f = function | IllTypedRecBody (n, na, jv, t) -> IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t) | UnsatisfiedConstraints g -> UnsatisfiedConstraints g +| UndeclaredUniverse l -> UndeclaredUniverse l let explain_reduction_tactic_error = function | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index ce74f2344a..880a11becd 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -71,17 +71,13 @@ let adjust_guardness_conditions const = function List.interval 0 (List.length ((lam_assum c)))) lemma_guard (Array.to_list fixdefs) in *) - let add c cb e = - let exists c e = - try ignore(Environ.lookup_constant c e); true - with Not_found -> false in - if exists c e then e else Environ.add_constant c cb e in - let env = List.fold_left (fun env { eff } -> - match eff with - | SEsubproof (c, cb,_) -> add c cb env - | SEscheme (l,_) -> - List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) - env (Safe_typing.side_effects_of_private_constants eff) in + let fold env eff = + try + let _ = Environ.lookup_constant eff.seff_constant env in + env + with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env + in + let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in let indexes = search_guard env possible_indexes fixdecls in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 5258ab2ea4..e1c9712135 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1505,8 +1505,8 @@ let _ = { optdepr = false; optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; - optread = (fun () -> !CClosure.share); - optwrite = (fun b -> CClosure.share := b) } + optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction); + optwrite = (fun b -> Global.set_reduction_sharing b) } let _ = declare_bool_option |