diff options
147 files changed, 2584 insertions, 1055 deletions
diff --git a/.gitignore b/.gitignore index aab1d1ede7..7d05a12cfe 100644 --- a/.gitignore +++ b/.gitignore @@ -152,6 +152,7 @@ plugins/ssr/ssrvernac.ml kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h +kernel/byterun/coq_arity.h kernel/genOpcodeFiles.exe kernel/vmopcodes.ml kernel/uint63.ml diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 6a8217674a..14bf263251 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -260,7 +260,7 @@ before_script: stage: stage-1 interruptible: true variables: - PLATFORM: "https://github.com/coq/platform/archive/master.zip" + PLATFORM: "https://github.com/coq/platform/archive/dev-ci.zip" artifacts: name: "$CI_JOB_NAME" paths: diff --git a/META.coq.in b/META.coq.in index 7a9818da08..39e35561ff 100644 --- a/META.coq.in +++ b/META.coq.in @@ -500,21 +500,6 @@ package "plugins" ( plugin(native) = "r_syntax_plugin.cmxs" ) - package "int63syntax" ( - - description = "Coq int63syntax plugin" - version = "8.14" - - requires = "" - directory = "syntax" - - archive(byte) = "int63_syntax_plugin.cmo" - archive(native) = "int63_syntax_plugin.cmx" - - plugin(byte) = "int63_syntax_plugin.cmo" - plugin(native) = "int63_syntax_plugin.cmxs" - ) - package "string_notation" ( description = "Coq string_notation plugin" diff --git a/Makefile.build b/Makefile.build index b307bde5df..d619fd3c85 100644 --- a/Makefile.build +++ b/Makefile.build @@ -367,6 +367,10 @@ kernel/byterun/coq_jumptbl.h: kernel/genOpcodeFiles.exe $(SHOW)'WRITE $@' $(HIDE)$< jump > $@ +kernel/byterun/coq_arity.h: kernel/genOpcodeFiles.exe + $(SHOW)'WRITE $@' + $(HIDE)$< arity > $@ + kernel/vmopcodes.ml: kernel/genOpcodeFiles.exe $(SHOW)'WRITE $@' $(HIDE)$< copml > $@ diff --git a/Makefile.common b/Makefile.common index 415454df79..dc40413078 100644 --- a/Makefile.common +++ b/Makefile.common @@ -149,7 +149,6 @@ CCCMO:=plugins/cc/cc_plugin.cmo BTAUTOCMO:=plugins/btauto/btauto_plugin.cmo RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo SYNTAXCMO:=$(addprefix plugins/syntax/, \ - int63_syntax_plugin.cmo \ float_syntax_plugin.cmo \ number_string_notation_plugin.cmo) DERIVECMO:=plugins/derive/derive_plugin.cmo diff --git a/Makefile.make b/Makefile.make index 2f6781439c..5e45e71c8c 100644 --- a/Makefile.make +++ b/Makefile.make @@ -109,7 +109,7 @@ GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml no GENMLGFILES:= $(MLGFILES:.mlg=.ml) GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/vmopcodes.ml kernel/uint63.ml kernel/float64.ml GENMLIFILES:=$(GRAMMLIFILES) -GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h +GENHFILES:=$(addprefix kernel/byterun/, coq_instruct.h coq_jumptbl.h coq_arity.h) GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) kernel/genOpcodeFiles.exe COQ_EXPORTED += GRAMFILES GRAMMLFILES GRAMMLIFILES GENMLFILES GENHFILES GENFILES @@ -274,7 +274,7 @@ depclean: find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} + cacheclean: - find theories test-suite -name '.*.aux' -exec rm -f {} + + find theories user-contrib test-suite -name '.*.aux' -exec rm -f {} + cleanconfig: rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist @@ -282,12 +282,12 @@ cleanconfig: distclean: clean cleanconfig cacheclean timingclean voclean: - find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.glob' -o -name "*.cmxs" \ + find theories plugins user-contrib test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.glob' -o -name "*.cmxs" \ -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} + - find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} + + find theories plugins user-contrib test-suite -name .coq-native -empty -exec rm -rf {} + timingclean: - find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' \ + find theories plugins user-contrib test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' \ -o -name "*.v.after-timing" -o -name "*.v.timing.diff" -o -name "time-of-build.log" \ -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \ -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} + @@ -65,12 +65,9 @@ environment for semi-interactive development of machine-checked proofs. [coqorg-badge]: https://images.microbadger.com/badges/version/coqorg/coq.svg [coqorg-link]: https://github.com/coq-community/docker-coq/wiki#docker-coq-images "coqorg/coq:latest" -Download the pre-built packages of the [latest release][] for Windows and macOS; -read the [help page][opam-using] on how to install Coq with OPAM; -or refer to the [`INSTALL.md`](INSTALL.md) file for the procedure to install from source. - -[latest release]: https://github.com/coq/coq/releases/latest -[opam-using]: https://coq.inria.fr/opam/www/using.html +Please see https://coq.inria.fr/download. +Information on how to build and install from sources can be found in +[`INSTALL.md`](INSTALL.md). ## Documentation diff --git a/checker/check.ml b/checker/check.ml index 1ff1425dea..587bb90d43 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -149,7 +149,7 @@ let remove_load_path dir = load_paths := List.filter2 (fun p d -> p <> dir) physical logical let add_load_path (phys_path,coq_path) = - if !Flags.debug then + if CDebug.(get_flag misc) then Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ str phys_path); let phys_path = CUnix.canonical_path_name phys_path in diff --git a/checker/checker.ml b/checker/checker.ml index bdfc5f07be..ba5e3c6d1a 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -48,19 +48,17 @@ let path_of_string s = let ( / ) = Filename.concat -let get_version_date () = +let get_version () = try let ch = open_in (Envars.coqlib () / "revision") in let ver = input_line ch in let rev = input_line ch in let () = close_in ch in - (ver,rev) - with _ -> (Coq_config.version,Coq_config.date) + Printf.sprintf "%s (%s)" ver rev + with _ -> Coq_config.version let print_header () = - let (ver,rev) = (get_version_date ()) in - Printf.printf "Welcome to Chicken %s (%s)\n" ver rev; - flush stdout + Printf.printf "Welcome to Chicken %s\n%!" (get_version ()) (* Adding files to Coq loadpath *) @@ -132,8 +130,6 @@ let init_load_path () = includes := [] -let set_debug () = Flags.debug := true - let impredicative_set = ref Declarations.PredicativeSet let set_impredicative_set () = impredicative_set := Declarations.ImpredicativeSet @@ -170,9 +166,7 @@ let compile_files senv = ~check:(List.rev !compile_list) let version () = - Printf.printf "The Coq Proof Checker, version %s (%s)\n" - Coq_config.version Coq_config.date; - Printf.printf "compiled on %s\n" Coq_config.compile_date; + Printf.printf "The Coq Proof Checker, version %s\n" Coq_config.version; exit 0 (* print the usage of coqtop (or coqc) on channel co *) @@ -222,7 +216,7 @@ let guill s = str "\"" ++ str s ++ str "\"" let where = function | None -> mt () | Some s -> - if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) + if CDebug.(get_flag misc) then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) let explain_exn = function | Stream.Failure -> @@ -251,7 +245,7 @@ let explain_exn = function hov 0 (fnl () ++ str "User interrupt.") | Univ.UniverseInconsistency i -> let msg = - if !Flags.debug then + if CDebug.(get_flag misc) then str "." ++ spc() ++ Univ.explain_universe_inconsistency Univ.Level.pr i else @@ -339,7 +333,7 @@ let parse_args argv = | ("-Q"|"-R") :: d :: p :: rem -> set_include d p;parse rem | ("-Q"|"-R") :: ([] | [_]) -> usage () - | "-debug" :: rem -> set_debug (); parse rem + | "-debug" :: rem -> CDebug.set_debug_all true; parse rem | "-where" :: _ -> Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); @@ -377,7 +371,7 @@ let init_with_argv argv = try parse_args argv; CWarnings.set_flags ("+"^Typeops.warn_bad_relevance_name); - if !Flags.debug then Printexc.record_backtrace true; + if CDebug.(get_flag misc) then Printexc.record_backtrace true; Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x)); Flags.if_verbose print_header (); init_load_path (); @@ -392,7 +386,7 @@ let run senv = let senv = compile_files senv in flush_all(); senv with e -> - if !Flags.debug then Printexc.print_backtrace stderr; + if CDebug.(get_flag misc) then Printexc.print_backtrace stderr; fatal_error (explain_exn e) (is_anomaly e) let start () = diff --git a/checker/values.ml b/checker/values.ml index 907f9f7e32..f7a367b986 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -240,7 +240,7 @@ let v_template_universes = v_tuple "template_universes" [|List(Opt v_level);v_context_set|] let v_primitive = - v_enum "primitive" 50 (* Number of "Primitive" in Int63.v and PrimFloat.v *) + v_enum "primitive" 54 (* Number of constructors of the CPrimitives.t type *) let v_cst_def = v_sum "constant_def" 0 diff --git a/config/coq_config.mli b/config/coq_config.mli index 809fa3d758..035574475d 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -33,8 +33,6 @@ val arch_is_win32 : bool val version : string (* version number of Coq *) val caml_version : string (* OCaml version used to compile Coq *) val caml_version_nums : int list (* OCaml version used to compile Coq by components *) -val date : string (* release date *) -val compile_date : string (* compile date *) val vo_version : int32 val state_magic_number : int diff --git a/configure.ml b/configure.ml index 40d77ed109..7814204e42 100644 --- a/configure.ml +++ b/configure.ml @@ -196,31 +196,6 @@ let which prog = let program_in_path prog = try let _ = which prog in true with Not_found -> false -let build_date = - try - float_of_string (Sys.getenv "SOURCE_DATE_EPOCH") - with - Not_found -> Unix.time () - -(** * Date *) - -(** The short one is displayed when starting coqtop, - The long one is used as compile date *) - -let months = - [| "January";"February";"March";"April";"May";"June"; - "July";"August";"September";"October";"November";"December" |] - -let get_date () = - let now = Unix.gmtime build_date in - let year = 1900+now.Unix.tm_year in - let month = months.(now.Unix.tm_mon) in - sprintf "%s %d" month year, - sprintf "%s %d %d %d:%02d:%02d" (String.sub month 0 3) now.Unix.tm_mday year - now.Unix.tm_hour now.Unix.tm_min now.Unix.tm_sec - -let short_date, full_date = get_date () - (** * Command-line parsing *) type ide = Opt | Byte | No @@ -1096,8 +1071,6 @@ let write_configml f = pr_s "version" coq_version; pr_s "caml_version" caml_version; pr_li "caml_version_nums" caml_version_nums; - pr_s "date" short_date; - pr_s "compile_date" full_date; pr_s "arch" arch; pr_b "arch_is_win32" arch_is_win32; pr_s "exec_extension" exe; diff --git a/dev/ci/user-overlays/13202-SkySkimmer-debug-infra.sh b/dev/ci/user-overlays/13202-SkySkimmer-debug-infra.sh new file mode 100644 index 0000000000..d80363c49f --- /dev/null +++ b/dev/ci/user-overlays/13202-SkySkimmer-debug-infra.sh @@ -0,0 +1 @@ +overlay elpi https://github.com/SkySkimmer/coq-elpi debug-infra 13202 diff --git a/dev/top_printers.mli b/dev/top_printers.mli index e8ed6c709e..b4b24d743a 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -165,6 +165,7 @@ val ppobj : Libobject.obj -> unit (* Some super raw printers *) val cast_kind_display : Constr.cast_kind -> string val constr_display : Constr.constr -> unit +val econstr_display : EConstr.constr -> unit val print_pure_constr : Constr.types -> unit val print_pure_econstr : EConstr.types -> unit diff --git a/doc/changelog/01-kernel/13853-delay-native.rst b/doc/changelog/01-kernel/13853-delay-native.rst new file mode 100644 index 0000000000..59bf960a0f --- /dev/null +++ b/doc/changelog/01-kernel/13853-delay-native.rst @@ -0,0 +1,6 @@ +- **Changed:** + Native-code libraries used by :tacn:`native_compute` are now delayed + until an actual call to the :tacn:`native_compute` machinery is + performed. This should make Coq more responsive on some systems + (`#13853 <https://github.com/coq/coq/pull/13853>`_, fixes `#13849 + <https://github.com/coq/coq/issues/13849>`_, by Guillaume Melquiond). diff --git a/doc/changelog/07-vernac-commands-and-options/13202-debug-infra.rst b/doc/changelog/07-vernac-commands-and-options/13202-debug-infra.rst new file mode 100644 index 0000000000..cd1ac3a35a --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/13202-debug-infra.rst @@ -0,0 +1,19 @@ +- **Added:** + :opt:`Debug` to control debug messages, functioning similarly to the warning system + (`#13202 <https://github.com/coq/coq/pull/13202>`_, + by Maxime Dénès and Gaëtan Gilbert). + The following flags have been converted (such that ``Set Flag`` becomes ``Set Debug "flag"``): + + - ``Debug Unification`` to ``unification`` + + - ``Debug HO Unification`` to ``ho-unification`` + + - ``Debug Tactic Unification`` to ``tactic-unification`` + + - ``Congruence Verbose`` to ``congruence`` + + - ``Debug Cbv`` to ``cbv`` + + - ``Debug RAKAM`` to ``RAKAM`` + + - ``Debug Ssreflect`` to ``ssreflect`` diff --git a/doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst b/doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst new file mode 100644 index 0000000000..e48b772f01 --- /dev/null +++ b/doc/changelog/08-cli-tools/13876-coqc+no_multiple_files.rst @@ -0,0 +1,6 @@ +- **Changed:** + `coqc` now enforces that at most a single `.v` file can be passed in + the command line. Support for multiple `.v` files in the form of + `coqc f1.v f2.v` didn't properly work in 8.13, tho it was accepted. + (`#13876 <https://github.com/coq/coq/pull/13876>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/10-standard-library/13080-ascii.rst b/doc/changelog/10-standard-library/13080-ascii.rst new file mode 100644 index 0000000000..167002283e --- /dev/null +++ b/doc/changelog/10-standard-library/13080-ascii.rst @@ -0,0 +1,4 @@ +- **Added:** + ``leb`` and ``ltb`` functions for ``ascii`` + (`#13080 <https://github.com/coq/coq/pull/13080>`_, + by Yishuai Li). diff --git a/doc/changelog/10-standard-library/13559-primitive_integers.rst b/doc/changelog/10-standard-library/13559-primitive_integers.rst new file mode 100644 index 0000000000..c3cad79bd2 --- /dev/null +++ b/doc/changelog/10-standard-library/13559-primitive_integers.rst @@ -0,0 +1,5 @@ +- **Added:** + Library for signed primitive integers, Sint63. The following operations were added to the kernel: division, remainder, comparison functions, and arithmetic shift right. Everything else works the same for signed and unsigned ints. + (`#13559 <https://github.com/coq/coq/pull/13559>`_, + fixes `#12109 <https://github.com/coq/coq/issues/12109>`_, + by Ana Borges, Guillaume Melquiond and Pierre Roux). diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst index 4505fc4b4d..7211d00dd0 100644 --- a/doc/sphinx/language/core/primitive.rst +++ b/doc/sphinx/language/core/primitive.rst @@ -8,15 +8,20 @@ Primitive Integers The language of terms features 63-bit machine integers as values. The type of such a value is *axiomatized*; it is declared through the following sentence -(excerpt from the :g:`Int63` module): +(excerpt from the :g:`PrimInt63` module): .. coqdoc:: Primitive int := #int63_type. -This type is equipped with a few operators, that must be similarly declared. -For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function, -declared and specified as follows: +This type can be understood as representing either unsigned or signed integers, +depending on which module is imported or, more generally, which scope is open. +:g:`Int63` and :g:`int63_scope` refer to the unsigned version, while :g:`Sint63` +and :g:`sint63_scope` refer to the signed one. + +The :g:`PrimInt63` module declares the available operators for this type. +For instance, equality of two unsigned primitive integers can be determined using +the :g:`Int63.eqb` function, declared and specified as follows: .. coqdoc:: @@ -25,7 +30,9 @@ declared and specified as follows: Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. -The complete set of such operators can be obtained looking at the :g:`Int63` module. +The complete set of such operators can be found in the :g:`PrimInt63` module. +The specifications and notations are in the :g:`Int63` and :g:`Sint63` +modules. These primitive declarations are regular axioms. As such, they must be trusted and are listed by the :g:`Print Assumptions` command, as in the following example. diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index dcc60195ed..e7237cf7eb 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -248,7 +248,7 @@ right arrow, or ``\>=`` for a greater than or equal sign. A larger number of latex tokens are supported by default. The full list is available here: -https://github.com/coq/coq/blob/master/ide/default_bindings_src.ml +https://github.com/coq/coq/blob/master/ide/coqide/default_bindings_src.ml Custom bindings may be added, as explained further on. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 665bae7077..071fcbee11 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -675,10 +675,10 @@ Applying theorems :tacn:`notypeclasses refine`: it performs type checking without resolution of typeclasses, does not perform beta reductions or shelve the subgoals. - .. flag:: Debug Unification - - Enables printing traces of unification steps used during - elaboration/typechecking and the :tacn:`refine` tactic. + :opt:`Debug` ``"unification"`` enables printing traces of + unification steps used during elaboration/typechecking and the + :tacn:`refine` tactic. ``"ho-unification"`` prints information + about higher order heuristics. .. tacn:: apply @term :name: apply @@ -1040,10 +1040,9 @@ Applying theorems when the instantiation of a variable cannot be found (cf. :tacn:`eapply` and :tacn:`apply`). -.. flag:: Debug Tactic Unification - - Enables printing traces of unification steps in tactic unification. - Tactic unification is used in tactics such as :tacn:`apply` and :tacn:`rewrite`. +:opt:`Debug` ``"tactic-unification"`` enables printing traces of +unification steps in tactic unification. Tactic unification is used in +tactics such as :tacn:`apply` and :tacn:`rewrite`. .. _managingthelocalcontext: diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 8db16fff69..37d605360d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -865,6 +865,14 @@ Controlling display interpreted from left to right, so in case of an overlap, the flags on the right have higher priority, meaning that `A,-A` is equivalent to `-A`. +.. opt:: Debug "{+, {? - } @ident }" + + Configures the display of debug messages. Each :n:`@ident` enables debug messages + for that component, while :n:`-@ident` disables messages for the component. + ``all`` activates or deactivates all other components. ``backtrace`` controls printing of + error backtraces. + + :cmd:`Test` `Debug` displays the list of components and their enabled/disabled state. .. opt:: Printing Width @natural This command sets which left-aligned part of the width of the screen is used diff --git a/doc/sphinx/proofs/automatic-tactics/logic.rst b/doc/sphinx/proofs/automatic-tactics/logic.rst index 5aaded2726..3f1f5d46c5 100644 --- a/doc/sphinx/proofs/automatic-tactics/logic.rst +++ b/doc/sphinx/proofs/automatic-tactics/logic.rst @@ -194,9 +194,7 @@ Solvers for logic and equality additional arguments can be given to congruence by filling in the holes in the terms given in the error message, using the `with` clause. - .. flag:: Congruence Verbose - - Makes :tacn:`congruence` print debug information. + :opt:`Debug` ``"congruence"`` makes :tacn:`congruence` print debug information. .. tacn:: btauto diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index bfaf746a06..4f937ad727 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -559,9 +559,7 @@ the conversion in hypotheses :n:`{+ @ident}`. on the profile file to see the results. Consult the ``perf`` documentation for more details. -.. flag:: Debug Cbv - - This flag makes :tacn:`cbv` (and its derivative :tacn:`compute`) print + :opt:`Debug` ``"Cbv"`` makes :tacn:`cbv` (and its derivative :tacn:`compute`) print information about the constants it encounters and the unfolding decisions it makes. @@ -659,10 +657,8 @@ the conversion in hypotheses :n:`{+ @ident}`. This applies :tacn:`simpl` only to the :n:`{+ @natural}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). -.. flag:: Debug RAKAM - - This flag makes :tacn:`cbn` print various debugging information. - ``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. +:opt:`Debug` ``"RAKAM"`` makes :tacn:`cbn` print various debugging information. +``RAKAM`` is the Refolding Algebraic Krivine Abstract Machine. .. tacn:: unfold @qualid :name: unfold diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 609884ce1d..03571ad680 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1741,6 +1741,12 @@ Number notations sorts, primitive integers, primitive floats, primitive arrays and type constants for primitive types) will be considered for printing. + .. note:: + For example, :n:`@qualid__type` can be :n:`PrimInt63.int`, + in which case :n:`@qualid__print` takes :n:`PrimInt63.int_wrapper` as input + instead of :n:`PrimInt63.int`. See below for an + :ref:`example <example-number-notation-primitive-int>`. + .. _number-string-via: :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]` @@ -2066,6 +2072,23 @@ The following errors apply to both string and number notations: Check 3. +.. _example-number-notation-primitive-int: + +.. example:: Number Notation for primitive integers + + This shows the use of the primitive + integers :n:`PrimInt63.int` as :n:`@qualid__type`. It is the way + parsing and printing of primitive integers are actually implemented + in `PrimInt63.v`. + + .. coqtop:: in reset + + Require Import Int63. + Definition parser (x : pos_neg_int63) : option int := + match x with Pos p => Some p | Neg _ => None end. + Definition printer (x : int_wrapper) : pos_neg_int63 := Pos (int_wrap x). + Number Notation int parser printer : int63_scope. + .. _example-number-notation-non-inductive: .. example:: Number Notation for a non inductive type diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index cbe526be68..27eb64a83b 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -286,6 +286,7 @@ through the <tt>Require Import</tt> command.</p> theories/Numbers/Cyclic/Int63/Cyclic63.v theories/Numbers/Cyclic/Int63/PrimInt63.v theories/Numbers/Cyclic/Int63/Int63.v + theories/Numbers/Cyclic/Int63/Sint63.v theories/Numbers/Cyclic/Int63/Ring63.v theories/Numbers/Cyclic/ZModulo/ZModulo.v </dd> diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 0d038e9a67..162d189136 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -365,6 +365,8 @@ val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Cons val of_case_invert : Constr.case_invert -> case_invert +val of_constr_array : Constr.t array -> t array + (** {5 Unsafe operations} *) module Unsafe : diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index b8228df2aa..20e9f0134f 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -13,13 +13,9 @@ open Preferences let ideslave_coqtop_flags = ref None -(** * Version and date *) +(** * Version *) -let get_version_date () = - let date = - if Glib.Utf8.validate Coq_config.date - then Coq_config.date - else "<date not printable>" in +let get_version () = try (* the following makes sense only when running with local layout *) let coqroot = Filename.concat @@ -29,21 +25,20 @@ let get_version_date () = let ch = open_in (Filename.concat coqroot "revision") in let ver = input_line ch in let rev = input_line ch in - (ver,rev) - with _ -> (Coq_config.version,date) + close_in ch; + Printf.sprintf "%s (%s)" ver rev + with _ -> Coq_config.version let short_version () = - let (ver,date) = get_version_date () in - Printf.sprintf "The Coq Proof Assistant, version %s (%s)\n" ver date + Printf.sprintf "The Coq Proof Assistant, version %s\n" (get_version ()) let version () = - let (ver,date) = get_version_date () in Printf.sprintf - "The Coq Proof Assistant, version %s (%s)\ + "The Coq Proof Assistant, version %s\ \nArchitecture %s running %s operating system\ \nGtk version is %s\ \nThis is %s \n" - ver date + (get_version ()) Coq_config.arch Sys.os_type (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z) (Filename.basename Sys.executable_name) diff --git a/ide/coqide/coqide.ml b/ide/coqide/coqide.ml index e066fc6292..3fbfbd66d3 100644 --- a/ide/coqide/coqide.ml +++ b/ide/coqide/coqide.ml @@ -1374,8 +1374,7 @@ let main files = let read_coqide_args argv = let set_debug () = Minilib.debug := true; - Flags.debug := true; - Exninfo.record_backtrace true + CDebug.set_debug_all true in let rec filter_coqtop coqtop project_files bindings_files out = function |"-unicode-bindings" :: sfilenames :: args -> diff --git a/ide/coqide/coqide_main.ml b/ide/coqide/coqide_main.ml index 0812e00960..a178e72806 100644 --- a/ide/coqide/coqide_main.ml +++ b/ide/coqide/coqide_main.ml @@ -35,7 +35,7 @@ let catch_gtk_messages () = let () = GToolbox.message_box ~title:"Error" (header ^ msg) in Coqide.crash_save 1 |`ERROR -> - if !Flags.debug then GToolbox.message_box ~title:"Error" (header ^ msg) + if CDebug.(get_flag misc) then GToolbox.message_box ~title:"Error" (header ^ msg) else Printf.eprintf "%s\n" (header ^ msg) |`DEBUG -> Minilib.log msg |level when Sys.os_type = "Win32" -> Minilib.log ~level msg diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index b42c705add..a6a7f7d742 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -35,11 +35,11 @@ let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s let pr_error s = pr_with_pid s let pr_debug s = - if !Flags.debug then pr_with_pid s + if CDebug.(get_flag misc) then pr_with_pid s let pr_debug_call q = - if !Flags.debug then pr_with_pid ("<-- " ^ Xmlprotocol.pr_call q) + if CDebug.(get_flag misc) then pr_with_pid ("<-- " ^ Xmlprotocol.pr_call q) let pr_debug_answer q r = - if !Flags.debug then pr_with_pid ("--> " ^ Xmlprotocol.pr_full_value q r) + if CDebug.(get_flag misc) then pr_with_pid ("--> " ^ Xmlprotocol.pr_full_value q r) (** Categories of commands *) @@ -397,8 +397,8 @@ let set_options options = let about () = { Interface.coqtop_version = Coq_config.version; Interface.protocol_version = Xmlprotocol.protocol_version; - Interface.release_date = Coq_config.date; - Interface.compile_date = Coq_config.compile_date; + Interface.release_date = "n/a"; + Interface.compile_date = "n/a"; } let handle_exn (e, info) = diff --git a/ide/coqide/microPG.ml b/ide/coqide/microPG.ml index 5a4871b70a..9908703cea 100644 --- a/ide/coqide/microPG.ml +++ b/ide/coqide/microPG.ml @@ -15,7 +15,7 @@ open GdkKeysyms open Printf let eprintf x = - if !Flags.debug then Printf.eprintf x else Printf.ifprintf stderr x + if CDebug.(get_flag misc) then Printf.eprintf x else Printf.ifprintf stderr x type gui = { notebook : session Wg_Notebook.typed_notebook; diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8138b4c6d9..4fb7861ca6 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -969,7 +969,13 @@ let rec extern inctx ?impargs scopes vars r = with No_match -> extern inctx scopes vars r') | None -> - try extern_notations inctx scopes vars None r + let r' = match DAst.get r with + | GInt i when Coqlib.has_ref "num.int63.wrap_int" -> + let wrap = Coqlib.lib_ref "num.int63.wrap_int" in + DAst.make (GApp (DAst.make (GRef (wrap, None)), [r])) + | _ -> r in + + try extern_notations inctx scopes vars None r' with No_match -> let loc = r.CAst.loc in @@ -1123,7 +1129,7 @@ let rec extern inctx ?impargs scopes vars r = | GInt i -> extern_prim_token_delimiter_if_required - (Number (NumTok.Signed.of_int_string (Uint63.to_string i))) + (Number NumTok.(Signed.of_bigint CHex (Z.of_int64 (Uint63.to_int64 i)))) "int63" "int63_scope" (snd scopes) | GFloat f -> extern_float f (snd scopes) diff --git a/interp/notation.ml b/interp/notation.ml index d6002d71b5..ed605c994d 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -548,11 +548,14 @@ type number_ty = hexadecimal : Names.inductive; number : Names.inductive } +type pos_neg_int63_ty = + { pos_neg_int63_ty : Names.inductive } + type target_kind = | Int of int_ty (* Coq.Init.Number.int + uint *) | UInt of int_ty (* Coq.Init.Number.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) - | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *) + | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *) | Number of number_ty (* Coq.Init.Number.number + uint + int *) | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *) | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *) @@ -1038,12 +1041,22 @@ let error_negative ?loc = let error_overflow ?loc n = CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Z.to_string n)) -let interp_int63 ?loc n = +let error_underflow ?loc n = + CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "underflow in int63 literal: " ++ str (Z.to_string n)) + +let coqpos_neg_int63_of_bigint ?loc ind (sign,n) = + let uint = int63_of_pos_bigint ?loc n in + let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in + mkApp (mkConstruct (ind, pos_neg), [|uint|]) + +let interp_int63 ?loc ind n = + let sign = if Z.(compare n zero >= 0) then SPlus else SMinus in + let n = Z.abs n in if Z.(leq zero n) then if Z.(lt n (pow z_two 63)) - then int63_of_pos_bigint ?loc n - else error_overflow ?loc n + then coqpos_neg_int63_of_bigint ?loc ind (sign,n) + else match sign with SPlus -> error_overflow ?loc n | SMinus -> error_underflow ?loc n else error_negative ?loc let bigint_of_int63 c = @@ -1051,6 +1064,15 @@ let bigint_of_int63 c = | Int i -> Z.of_int64 (Uint63.to_int64 i) | _ -> raise NotAValidPrimToken +let bigint_of_coqpos_neg_int63 c = + match Constr.kind c with + | App (c,[|c'|]) -> + (match Constr.kind c with + | Construct ((_,1), _) (* Pos *) -> bigint_of_int63 c' + | Construct ((_,2), _) (* Neg *) -> Z.neg (bigint_of_int63 c') + | _ -> raise NotAValidPrimToken) + | _ -> raise NotAValidPrimToken + let interp o ?loc n = begin match o.warning, n with | Warning threshold, n when NumTok.Signed.is_bigger_int_than n threshold -> @@ -1070,9 +1092,9 @@ let interp o ?loc n = with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name) | Z z_pos_ty, Some n -> z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n) - | Int63, Some n -> - interp_int63 ?loc (NumTok.SignedNat.to_bigint n) - | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63), _ -> + | Int63 pos_neg_int63_ty, Some n -> + interp_int63 ?loc pos_neg_int63_ty.pos_neg_int63_ty (NumTok.SignedNat.to_bigint n) + | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63 _), _ -> no_such_prim_token "number" ?loc o.ty_name | Number number_ty, _ -> coqnumber_of_rawnum number_ty n | Decimal number_ty, _ -> @@ -1100,7 +1122,7 @@ let uninterp o n = | (Int _, c) -> NumTok.Signed.of_int (rawnum_of_coqint c) | (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c) | (Z _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_z c) - | (Int63, c) -> NumTok.Signed.of_bigint CDec (bigint_of_int63 c) + | (Int63 _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_coqpos_neg_int63 c) | (Number _, c) -> rawnum_of_coqnumber c | (DecimalInt _, c) -> NumTok.Signed.of_int (decimal_rawnum_of_coqint c) | (DecimalUInt _, c) -> NumTok.Signed.of_nat (decimal_rawnum_of_coquint c) diff --git a/interp/notation.mli b/interp/notation.mli index 97955bf92e..77f245ae77 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -137,11 +137,14 @@ type number_ty = hexadecimal : Names.inductive; number : Names.inductive } +type pos_neg_int63_ty = + { pos_neg_int63_ty : Names.inductive } + type target_kind = | Int of int_ty (* Coq.Init.Number.int + uint *) | UInt of int_ty (* Coq.Init.Number.uint *) | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *) - | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *) + | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *) | Number of number_ty (* Coq.Init.Number.number + uint + int *) | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *) | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *) diff --git a/interp/numTok.ml b/interp/numTok.ml index 124a6cd249..12ef33717a 100644 --- a/interp/numTok.ml +++ b/interp/numTok.ml @@ -85,7 +85,7 @@ struct let string_of_nonneg_bigint c n = match c with | CDec -> Z.format "%d" n - | CHex -> Z.format "0x%x" n + | CHex -> Z.format "%#x" n let of_bigint c n = let sign, n = if Int.equal (-1) (Z.sign n) then (SMinus, Z.neg n) else (SPlus, n) in (sign, string_of_nonneg_bigint c n) diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 2c0b580e24..20890a28dc 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -21,70 +21,12 @@ #include <caml/alloc.h> #include <caml/memory.h> #include "coq_instruct.h" +#include "coq_arity.h" #include "coq_fix_code.h" #ifdef THREADED_CODE char ** coq_instr_table; char * coq_instr_base; -int arity[STOP+1]; - -void init_arity () { - /* instruction with zero operand */ - arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]= - arity[ACC6]=arity[ACC7]= - arity[PUSH]=arity[PUSHACC1]= - arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]= - arity[PUSHACC6]=arity[PUSHACC7]= - arity[ENVACC0]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]= - arity[PUSHENVACC0]=arity[PUSHENVACC1]=arity[PUSHENVACC2]=arity[PUSHENVACC3]= - arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[APPLY4]=arity[RESTART]= - arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE1]= - arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE1]= - arity[GETFIELD0]=arity[GETFIELD1]= - arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= - arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= - arity[ACCUMULATE]=arity[STOP]= - 0; - /* instruction with one operand */ - arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= - arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]= - arity[APPTERM3]=arity[RETURN]=arity[GRAB]=arity[OFFSETCLOSURE]= - arity[PUSHOFFSETCLOSURE]=arity[GETGLOBAL]=arity[PUSHGETGLOBAL]= - arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]= - arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]= - arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]= - arity[BRANCH]=arity[ENSURESTACKCAPACITY]= - arity[CHECKADDINT63]=arity[CHECKADDCINT63]=arity[CHECKADDCARRYCINT63]= - arity[CHECKSUBINT63]=arity[CHECKSUBCINT63]=arity[CHECKSUBCARRYCINT63]= - arity[CHECKMULINT63]=arity[CHECKMULCINT63]= - arity[CHECKDIVINT63]=arity[CHECKMODINT63]=arity[CHECKDIVEUCLINT63]= - arity[CHECKDIV21INT63]= - arity[CHECKLXORINT63]=arity[CHECKLORINT63]=arity[CHECKLANDINT63]= - arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]= - arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]= - arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]= - arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]= - arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]= - arity[CHECKCLASSIFYFLOAT]= - arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]= - arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]= - arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]= - arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]= - arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]= - arity[CHECKNEXTUPFLOATINPLACE]=arity[CHECKNEXTDOWNFLOATINPLACE]= - 1; - /* instruction with two operands */ - arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= - arity[CHECKCAMLCALL1]=arity[CHECKCAMLCALL2_1]= - arity[CHECKCAMLCALL2]=arity[CHECKCAMLCALL3_1]= - arity[PROJ]= - 2; - /* instruction with four operands */ - arity[MAKESWITCHBLOCK]=4; - /* instruction with arbitrary operands */ - arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0; -} - #endif /* THREADED_CODE */ @@ -166,9 +108,7 @@ value coq_tcode_of_code (value code) { opcode_t instr; COPY32(&instr,p); p++; - if (instr < 0 || instr > STOP){ - instr = STOP; - }; + if (instr < 0 || instr > STOP) abort(); *q++ = VALINSTR(instr); if (instr == SWITCH) { uint32_t i, sizes, const_size, block_size; @@ -185,8 +125,9 @@ value coq_tcode_of_code (value code) { q++; for(i=1; i<n; i++) { COPY32(q,p); p++; q++; }; } else { - uint32_t i, ar; + int i, ar; ar = arity[instr]; + if (ar < 0) abort(); for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; }; } } diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h index 5a233e6178..916d9753a4 100644 --- a/kernel/byterun/coq_fix_code.h +++ b/kernel/byterun/coq_fix_code.h @@ -18,7 +18,6 @@ void * coq_stat_alloc (asize_t sz); #ifdef THREADED_CODE extern char ** coq_instr_table; extern char * coq_instr_base; -void init_arity(); #define VALINSTR(instr) ((opcode_t)(coq_instr_table[instr] - coq_instr_base)) #else #define VALINSTR(instr) instr diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a9ea6d9f46..704eb1ef98 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -547,7 +547,7 @@ value coq_interprete CHECK_STACK(0); /* We also check for signals */ #if OCAML_VERSION >= 41000 - { + if (caml_something_to_do) { value res = caml_process_pending_actions_exn(); if (Is_exception_result(res)) { /* If there is an asynchronous exception, we reset the vm */ @@ -1426,6 +1426,41 @@ value coq_interprete Next; } + Instruct(CHECKDIVSINT63) { + print_instr("CHEKDIVSINT63"); + CheckInt2(); + int b; + Uint63_eq0(b, *sp); + if (b) { + accu = *sp++; + } + else { + Uint63_eqm1(b, *sp); + if (b) { + Uint63_neg(accu); + sp++; + } + else { + Uint63_divs(accu, *sp++); + } + } + Next; + } + + Instruct(CHECKMODSINT63) { + print_instr("CHEKMODSINT63"); + CheckInt2(); + int b; + Uint63_eq0(b, *sp); + if (b) { + accu = *sp++; + } + else { + Uint63_mods(accu,*sp++); + } + Next; + } + Instruct (CHECKDIV21INT63) { print_instr("DIV21INT63"); CheckInt3(); @@ -1473,6 +1508,13 @@ value coq_interprete Next; } + Instruct(CHECKASRINT63) { + print_instr("CHECKASRINT63"); + CheckInt2(); + Uint63_asr(accu,*sp++); + Next; + } + Instruct (CHECKADDMULDIVINT63) { print_instr("CHECKADDMULDIVINT63"); CheckInt3(); @@ -1508,6 +1550,24 @@ value coq_interprete Next; } + Instruct (CHECKLTSINT63) { + print_instr("CHECKLTSINT63"); + CheckInt2(); + int b; + Uint63_lts(b,accu,*sp++); + accu = b ? coq_true : coq_false; + Next; + } + + Instruct (CHECKLESINT63) { + print_instr("CHECKLESINT63"); + CheckInt2(); + int b; + Uint63_les(b,accu,*sp++); + accu = b ? coq_true : coq_false; + Next; + } + Instruct (CHECKCOMPAREINT63) { /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */ /* assumes Inductive _ : _ := Eq | Lt | Gt */ @@ -1526,6 +1586,24 @@ value coq_interprete Next; } + Instruct (CHECKCOMPARESINT63) { + /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */ + /* assumes Inductive _ : _ := Eq | Lt | Gt */ + print_instr("CHECKCOMPARESINT63"); + CheckInt2(); + int b; + Uint63_eq(b, accu, *sp); + if (b) { + accu = coq_Eq; + sp++; + } + else { + Uint63_lts(b, accu, *sp++); + accu = b ? coq_Lt : coq_Gt; + } + Next; + } + Instruct (CHECKHEAD0INT63) { print_instr("CHECKHEAD0INT63"); CheckInt1(); diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index fe076f8f04..a55ff57c8d 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -100,9 +100,6 @@ value init_coq_vm(value unit) /* ML */ fprintf(stderr,"already open \n");fflush(stderr);} else { drawinstr=0; -#ifdef THREADED_CODE - init_arity(); -#endif /* THREADED_CODE */ /* Allocate the table of global and the stack */ init_coq_stack(); /* Initialing the interpreter */ diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index dd9b9e55be..693716ee90 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -96,7 +96,10 @@ value uint63_##name##_ml(value x, value y, value z) { \ accu = uint63_return_value__; \ }while(0) +DECLARE_NULLOP(zero) DECLARE_NULLOP(one) +DECLARE_UNOP(neg) +#define Uint63_neg(x) CALL_UNOP(neg, x) DECLARE_BINOP(add) #define Uint63_add(x, y) CALL_BINOP(add, x, y) DECLARE_BINOP(addcarry) @@ -105,28 +108,40 @@ DECLARE_TEROP(addmuldiv) #define Uint63_addmuldiv(x, y, z) CALL_TEROP(addmuldiv, x, y, z) DECLARE_BINOP(div) #define Uint63_div(x, y) CALL_BINOP(div, x, y) +DECLARE_BINOP(divs) +#define Uint63_divs(x, y) CALL_BINOP(divs, x, y) DECLARE_BINOP(eq) #define Uint63_eq(r, x, y) CALL_RELATION(r, eq, x, y) DECLARE_UNOP(eq0) #define Uint63_eq0(r, x) CALL_PREDICATE(r, eq0, x) +DECLARE_UNOP(eqm1) +#define Uint63_eqm1(r, x) CALL_PREDICATE(r, eqm1, x) DECLARE_UNOP(head0) #define Uint63_head0(x) CALL_UNOP(head0, x) DECLARE_BINOP(land) #define Uint63_land(x, y) CALL_BINOP(land, x, y) DECLARE_BINOP(leq) #define Uint63_leq(r, x, y) CALL_RELATION(r, leq, x, y) +DECLARE_BINOP(les) +#define Uint63_les(r, x, y) CALL_RELATION(r, les, x, y) DECLARE_BINOP(lor) #define Uint63_lor(x, y) CALL_BINOP(lor, x, y) DECLARE_BINOP(lsl) #define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y) DECLARE_BINOP(lsr) #define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y) +DECLARE_BINOP(asr) +#define Uint63_asr(x, y) CALL_BINOP(asr, x, y) DECLARE_BINOP(lt) #define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y) +DECLARE_BINOP(lts) +#define Uint63_lts(r, x, y) CALL_RELATION(r, lts, x, y) DECLARE_BINOP(lxor) #define Uint63_lxor(x, y) CALL_BINOP(lxor, x, y) DECLARE_BINOP(mod) #define Uint63_mod(x, y) CALL_BINOP(mod, x, y) +DECLARE_BINOP(mods) +#define Uint63_mods(x, y) CALL_BINOP(mods, x, y) DECLARE_BINOP(mul) #define Uint63_mul(x, y) CALL_BINOP(mul, x, y) DECLARE_BINOP(sub) diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 731ae8f46e..da9ae7f147 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -12,21 +12,28 @@ #define uint_of_value(val) (((uint64_t)(val)) >> 1) #define uint63_of_value(val) ((uint64_t)(val) >> 1) +#define int63_of_value(val) ((int64_t)(val) >> 1) /* 2^63 * y + x as a value */ //#define Val_intint(x,y) ((value)(((uint64_t)(x)) << 1 + ((uint64_t)(y) << 64))) -#define uint63_zero ((value) 1) /* 2*0 + 1 */ +#define uint63_zero() ((value) 1) /* 2*0 + 1 */ #define uint63_one() ((value) 3) /* 2*1 + 1 */ #define uint63_eq(x,y) ((x) == (y)) #define Uint63_eq(r,x,y) ((r) = uint63_eq(x,y)) #define Uint63_eq0(r,x) ((r) = ((x) == (uint64_t)1)) +#define Uint63_eqm1(r,x) ((r) = ((x) == (uint64_t)(int64_t)(-1))) #define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y)) #define Uint63_lt(r,x,y) ((r) = uint63_lt(x,y)) #define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y)) #define Uint63_leq(r,x,y) ((r) = uint63_leq(x,y)) +#define uint63_lts(x,y) ((int64_t) (x) < (int64_t) (y)) +#define Uint63_lts(r,x,y) ((r) = uint63_lts(x,y)) +#define uint63_les(x,y) ((int64_t) (x) <= (int64_t) (y)) +#define Uint63_les(r,x,y) ((r) = uint63_les(x,y)) +#define Uint63_neg(x) (accu = (value)(2 - (uint64_t) x)) #define Uint63_add(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) - 1)) #define Uint63_addcarry(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) + 1)) #define Uint63_sub(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) + 1)) @@ -34,6 +41,8 @@ #define Uint63_mul(x,y) (accu = Val_long(uint63_of_value(x) * uint63_of_value(y))) #define Uint63_div(x,y) (accu = Val_long(uint63_of_value(x) / uint63_of_value(y))) #define Uint63_mod(x,y) (accu = Val_long(uint63_of_value(x) % uint63_of_value(y))) +#define Uint63_divs(x,y) (accu = Val_long(int63_of_value(x) / int63_of_value(y))) +#define Uint63_mods(x,y) (accu = Val_long(int63_of_value(x) % int63_of_value(y))) #define Uint63_lxor(x,y) (accu = (value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1)) #define Uint63_lor(x,y) (accu = (value)((uint64_t)(x) | (uint64_t)(y))) @@ -46,14 +55,21 @@ if (uint63_lsl_y__ < (uint64_t) 127) \ accu = (value)((((uint64_t)(x)-1) << uint63_of_value(uint63_lsl_y__)) | 1); \ else \ - accu = uint63_zero; \ + accu = uint63_zero(); \ }while(0) #define Uint63_lsr(x,y) do{ \ value uint63_lsl_y__ = (y); \ if (uint63_lsl_y__ < (uint64_t) 127) \ accu = (value)(((uint64_t)(x) >> uint63_of_value(uint63_lsl_y__)) | 1); \ else \ - accu = uint63_zero; \ + accu = uint63_zero(); \ + }while(0) +#define Uint63_asr(x,y) do{ \ + value uint63_asr_y__ = (y); \ + if (uint63_asr_y__ < (uint64_t) 127) \ + accu = (value)(((int64_t)(x) >> uint63_of_value(uint63_asr_y__)) | 1); \ + else \ + accu = uint63_zero(); \ }while(0) /* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */ diff --git a/kernel/byterun/dune b/kernel/byterun/dune index d3e2a2fa7f..a2484f79a7 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -14,3 +14,7 @@ (rule (targets coq_jumptbl.h) (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump)))) + +(rule + (targets coq_arity.h) + (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe arity)))) diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 5cd91b4e74..6ef0e9fa15 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -8,6 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(* Note: don't forget to update v_primitive in checker/values.ml if the *) +(* number of primitives is changed. *) + open Univ type t = @@ -18,8 +21,11 @@ type t = | Int63mul | Int63div | Int63mod + | Int63divs + | Int63mods | Int63lsr | Int63lsl + | Int63asr | Int63land | Int63lor | Int63lxor @@ -34,7 +40,10 @@ type t = | Int63eq | Int63lt | Int63le + | Int63lts + | Int63les | Int63compare + | Int63compares | Float64opp | Float64abs | Float64eq @@ -68,8 +77,11 @@ let parse = function | "int63_mul" -> Int63mul | "int63_div" -> Int63div | "int63_mod" -> Int63mod + | "int63_divs" -> Int63divs + | "int63_mods" -> Int63mods | "int63_lsr" -> Int63lsr | "int63_lsl" -> Int63lsl + | "int63_asr" -> Int63asr | "int63_land" -> Int63land | "int63_lor" -> Int63lor | "int63_lxor" -> Int63lxor @@ -84,7 +96,10 @@ let parse = function | "int63_eq" -> Int63eq | "int63_lt" -> Int63lt | "int63_le" -> Int63le + | "int63_lts" -> Int63lts + | "int63_les" -> Int63les | "int63_compare" -> Int63compare + | "int63_compares" -> Int63compares | "float64_opp" -> Float64opp | "float64_abs" -> Float64abs | "float64_eq" -> Float64eq @@ -163,6 +178,12 @@ let hash = function | Arrayset -> 46 | Arraycopy -> 47 | Arraylength -> 48 + | Int63lts -> 49 + | Int63les -> 50 + | Int63divs -> 51 + | Int63mods -> 52 + | Int63asr -> 53 + | Int63compares -> 54 (* Should match names in nativevalues.ml *) let to_string = function @@ -173,8 +194,11 @@ let to_string = function | Int63mul -> "mul" | Int63div -> "div" | Int63mod -> "rem" + | Int63divs -> "divs" + | Int63mods -> "rems" | Int63lsr -> "l_sr" | Int63lsl -> "l_sl" + | Int63asr -> "a_sr" | Int63land -> "l_and" | Int63lor -> "l_or" | Int63lxor -> "l_xor" @@ -189,7 +213,10 @@ let to_string = function | Int63eq -> "eq" | Int63lt -> "lt" | Int63le -> "le" + | Int63lts -> "lts" + | Int63les -> "les" | Int63compare -> "compare" + | Int63compares -> "compares" | Float64opp -> "fopp" | Float64abs -> "fabs" | Float64eq -> "feq" @@ -271,14 +298,15 @@ let types = | Int63head0 | Int63tail0 -> [int_ty; int_ty] | Int63add | Int63sub | Int63mul | Int63div | Int63mod - | Int63lsr | Int63lsl + | Int63divs | Int63mods + | Int63lsr | Int63lsl | Int63asr | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty] | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC -> [int_ty; int_ty; PITT_ind (PIT_carry, int_ty)] | Int63mulc | Int63diveucl -> [int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))] - | Int63eq | Int63lt | Int63le -> [int_ty; int_ty; PITT_ind (PIT_bool, ())] - | Int63compare -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())] + | Int63eq | Int63lt | Int63le | Int63lts | Int63les -> [int_ty; int_ty; PITT_ind (PIT_bool, ())] + | Int63compare | Int63compares -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())] | Int63div21 -> [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))] | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty] @@ -314,8 +342,11 @@ let params = function | Int63mul | Int63div | Int63mod + | Int63divs + | Int63mods | Int63lsr | Int63lsl + | Int63asr | Int63land | Int63lor | Int63lxor @@ -330,7 +361,10 @@ let params = function | Int63eq | Int63lt | Int63le + | Int63lts + | Int63les | Int63compare + | Int63compares | Float64opp | Float64abs | Float64eq @@ -367,8 +401,11 @@ let univs = function | Int63mul | Int63div | Int63mod + | Int63divs + | Int63mods | Int63lsr | Int63lsl + | Int63asr | Int63land | Int63lor | Int63lxor @@ -383,7 +420,10 @@ let univs = function | Int63eq | Int63lt | Int63le + | Int63lts + | Int63les | Int63compare + | Int63compares | Float64opp | Float64abs | Float64eq diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 0db643faf4..de90179726 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -16,8 +16,11 @@ type t = | Int63mul | Int63div | Int63mod + | Int63divs + | Int63mods | Int63lsr | Int63lsl + | Int63asr | Int63land | Int63lor | Int63lxor @@ -32,7 +35,10 @@ type t = | Int63eq | Int63lt | Int63le + | Int63lts + | Int63les | Int63compare + | Int63compares | Float64opp | Float64abs | Float64eq diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index 0e1cd0c56a..20220dd9d2 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -10,192 +10,201 @@ (** List of opcodes. - It is used to generate the [coq_instruct.h], [coq_jumptbl.h] and - [vmopcodes.ml] files. + It is used to generate the files [coq_instruct.h], [coq_jumptbl.h], + [coq_arity.h], and [vmopcodes.ml]. - If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c - with the arity of the instruction and maybe coq_tcode_of_code. + [STOP] needs to be the last opcode. + + Arity -1 designates opcodes that need special handling in [coq_fix_code.c]. *) let opcodes = [| - "ACC0"; - "ACC1"; - "ACC2"; - "ACC3"; - "ACC4"; - "ACC5"; - "ACC6"; - "ACC7"; - "ACC"; - "PUSH"; - "PUSHACC1"; - "PUSHACC2"; - "PUSHACC3"; - "PUSHACC4"; - "PUSHACC5"; - "PUSHACC6"; - "PUSHACC7"; - "PUSHACC"; - "POP"; - "ENVACC0"; - "ENVACC1"; - "ENVACC2"; - "ENVACC3"; - "ENVACC"; - "PUSHENVACC0"; - "PUSHENVACC1"; - "PUSHENVACC2"; - "PUSHENVACC3"; - "PUSHENVACC"; - "PUSH_RETADDR"; - "APPLY"; - "APPLY1"; - "APPLY2"; - "APPLY3"; - "APPLY4"; - "APPTERM"; - "APPTERM1"; - "APPTERM2"; - "APPTERM3"; - "RETURN"; - "RESTART"; - "GRAB"; - "GRABREC"; - "CLOSURE"; - "CLOSUREREC"; - "CLOSURECOFIX"; - "OFFSETCLOSURE0"; - "OFFSETCLOSURE1"; - "OFFSETCLOSURE"; - "PUSHOFFSETCLOSURE0"; - "PUSHOFFSETCLOSURE1"; - "PUSHOFFSETCLOSURE"; - "GETGLOBAL"; - "PUSHGETGLOBAL"; - "MAKEBLOCK"; - "MAKEBLOCK1"; - "MAKEBLOCK2"; - "MAKEBLOCK3"; - "MAKEBLOCK4"; - "SWITCH"; - "PUSHFIELDS"; - "GETFIELD0"; - "GETFIELD1"; - "GETFIELD"; - "SETFIELD"; - "PROJ"; - "ENSURESTACKCAPACITY"; - "CONST0"; - "CONST1"; - "CONST2"; - "CONST3"; - "CONSTINT"; - "PUSHCONST0"; - "PUSHCONST1"; - "PUSHCONST2"; - "PUSHCONST3"; - "PUSHCONSTINT"; - "ACCUMULATE"; - "MAKESWITCHBLOCK"; - "MAKEACCU"; - "BRANCH"; - "CHECKADDINT63"; - "CHECKADDCINT63"; - "CHECKADDCARRYCINT63"; - "CHECKSUBINT63"; - "CHECKSUBCINT63"; - "CHECKSUBCARRYCINT63"; - "CHECKMULINT63"; - "CHECKMULCINT63"; - "CHECKDIVINT63"; - "CHECKMODINT63"; - "CHECKDIVEUCLINT63"; - "CHECKDIV21INT63"; - "CHECKLXORINT63"; - "CHECKLORINT63"; - "CHECKLANDINT63"; - "CHECKLSLINT63"; - "CHECKLSRINT63"; - "CHECKADDMULDIVINT63"; - "CHECKEQINT63"; - "CHECKLTINT63"; - "CHECKLEINT63"; - "CHECKCOMPAREINT63"; - "CHECKHEAD0INT63"; - "CHECKTAIL0INT63"; - "CHECKOPPFLOAT"; - "CHECKABSFLOAT"; - "CHECKEQFLOAT"; - "CHECKLTFLOAT"; - "CHECKLEFLOAT"; - "CHECKCOMPAREFLOAT"; - "CHECKCLASSIFYFLOAT"; - "CHECKADDFLOAT"; - "CHECKSUBFLOAT"; - "CHECKMULFLOAT"; - "CHECKDIVFLOAT"; - "CHECKSQRTFLOAT"; - "CHECKFLOATOFINT63"; - "CHECKFLOATNORMFRMANTISSA"; - "CHECKFRSHIFTEXP"; - "CHECKLDSHIFTEXP"; - "CHECKNEXTUPFLOAT"; - "CHECKNEXTDOWNFLOAT"; - "CHECKNEXTUPFLOATINPLACE"; - "CHECKNEXTDOWNFLOATINPLACE"; - "CHECKCAMLCALL2_1"; - "CHECKCAMLCALL1"; - "CHECKCAMLCALL2"; - "CHECKCAMLCALL3_1"; - "STOP" + "ACC0", 0; + "ACC1", 0; + "ACC2", 0; + "ACC3", 0; + "ACC4", 0; + "ACC5", 0; + "ACC6", 0; + "ACC7", 0; + "ACC", 1; + "PUSH", 0; + "PUSHACC1", 0; + "PUSHACC2", 0; + "PUSHACC3", 0; + "PUSHACC4", 0; + "PUSHACC5", 0; + "PUSHACC6", 0; + "PUSHACC7", 0; + "PUSHACC", 1; + "POP", 1; + "ENVACC0", 0; + "ENVACC1", 0; + "ENVACC2", 0; + "ENVACC3", 0; + "ENVACC", 1; + "PUSHENVACC0", 0; + "PUSHENVACC1", 0; + "PUSHENVACC2", 0; + "PUSHENVACC3", 0; + "PUSHENVACC", 1; + "PUSH_RETADDR", 1; + "APPLY", 1; + "APPLY1", 0; + "APPLY2", 0; + "APPLY3", 0; + "APPLY4", 0; + "APPTERM", 2; + "APPTERM1", 1; + "APPTERM2", 1; + "APPTERM3", 1; + "RETURN", 1; + "RESTART", 0; + "GRAB", 1; + "GRABREC", 1; + "CLOSURE", 2; + "CLOSUREREC", -1; + "CLOSURECOFIX", -1; + "OFFSETCLOSURE0", 0; + "OFFSETCLOSURE1", 0; + "OFFSETCLOSURE", 1; + "PUSHOFFSETCLOSURE0", 0; + "PUSHOFFSETCLOSURE1", 0; + "PUSHOFFSETCLOSURE", 1; + "GETGLOBAL", 1; + "PUSHGETGLOBAL", 1; + "MAKEBLOCK", 2; + "MAKEBLOCK1", 1; + "MAKEBLOCK2", 1; + "MAKEBLOCK3", 1; + "MAKEBLOCK4", 1; + "SWITCH", -1; + "PUSHFIELDS", 1; + "GETFIELD0", 0; + "GETFIELD1", 0; + "GETFIELD", 1; + "SETFIELD", 1; + "PROJ", 2; + "ENSURESTACKCAPACITY", 1; + "CONST0", 0; + "CONST1", 0; + "CONST2", 0; + "CONST3", 0; + "CONSTINT", 1; + "PUSHCONST0", 0; + "PUSHCONST1", 0; + "PUSHCONST2", 0; + "PUSHCONST3", 0; + "PUSHCONSTINT", 1; + "ACCUMULATE", 0; + "MAKESWITCHBLOCK", 4; + "MAKEACCU", 1; + "BRANCH", 1; + "CHECKADDINT63", 1; + "CHECKADDCINT63", 1; + "CHECKADDCARRYCINT63", 1; + "CHECKSUBINT63", 1; + "CHECKSUBCINT63", 1; + "CHECKSUBCARRYCINT63", 1; + "CHECKMULINT63", 1; + "CHECKMULCINT63", 1; + "CHECKDIVINT63", 1; + "CHECKMODINT63", 1; + "CHECKDIVSINT63", 1; + "CHECKMODSINT63", 1; + "CHECKDIVEUCLINT63", 1; + "CHECKDIV21INT63", 1; + "CHECKLXORINT63", 1; + "CHECKLORINT63", 1; + "CHECKLANDINT63", 1; + "CHECKLSLINT63", 1; + "CHECKLSRINT63", 1; + "CHECKASRINT63", 1; + "CHECKADDMULDIVINT63", 1; + "CHECKEQINT63", 1; + "CHECKLTINT63", 1; + "CHECKLEINT63", 1; + "CHECKLTSINT63", 1; + "CHECKLESINT63", 1; + "CHECKCOMPAREINT63", 1; + "CHECKCOMPARESINT63", 1; + "CHECKHEAD0INT63", 1; + "CHECKTAIL0INT63", 1; + "CHECKOPPFLOAT", 1; + "CHECKABSFLOAT", 1; + "CHECKEQFLOAT", 1; + "CHECKLTFLOAT", 1; + "CHECKLEFLOAT", 1; + "CHECKCOMPAREFLOAT", 1; + "CHECKCLASSIFYFLOAT", 1; + "CHECKADDFLOAT", 1; + "CHECKSUBFLOAT", 1; + "CHECKMULFLOAT", 1; + "CHECKDIVFLOAT", 1; + "CHECKSQRTFLOAT", 1; + "CHECKFLOATOFINT63", 1; + "CHECKFLOATNORMFRMANTISSA", 1; + "CHECKFRSHIFTEXP", 1; + "CHECKLDSHIFTEXP", 1; + "CHECKNEXTUPFLOAT", 1; + "CHECKNEXTDOWNFLOAT", 1; + "CHECKNEXTUPFLOATINPLACE", 1; + "CHECKNEXTDOWNFLOATINPLACE", 1; + "CHECKCAMLCALL2_1", 2; + "CHECKCAMLCALL1", 2; + "CHECKCAMLCALL2", 2; + "CHECKCAMLCALL3_1", 2; + "STOP", 0 |] let pp_c_comment fmt = - Format.fprintf fmt "/* %a */" + Format.fprintf fmt "/* %s */" let pp_ocaml_comment fmt = - Format.fprintf fmt "(* %a *)" + Format.fprintf fmt "(* %s *)" let pp_header isOcaml fmt = Format.fprintf fmt "%a" - (fun fmt -> - (if isOcaml then pp_ocaml_comment else pp_c_comment) fmt - Format.pp_print_string) + (if isOcaml then pp_ocaml_comment else pp_c_comment) "DO NOT EDIT: automatically generated by kernel/genOpcodeFiles.ml" -let pp_with_commas fmt k = - Array.iteri (fun n s -> - Format.fprintf fmt " %a%s@." - k s - (if n + 1 < Array.length opcodes - then "," else "") - ) opcodes - let pp_coq_instruct_h fmt = - let line = Format.fprintf fmt "%s@." in pp_header false fmt; - line "#pragma once"; - line "enum instructions {"; - pp_with_commas fmt Format.pp_print_string; - line "};" + Format.fprintf fmt "#pragma once@.enum instructions {@."; + Array.iter (fun (name, _) -> + Format.fprintf fmt " %s,@." name + ) opcodes; + Format.fprintf fmt "};@." let pp_coq_jumptbl_h fmt = - pp_with_commas fmt (fun fmt -> Format.fprintf fmt "&&coq_lbl_%s") + pp_header false fmt; + Array.iter (fun (name, _) -> + Format.fprintf fmt " &&coq_lbl_%s,@." name + ) opcodes + +let pp_coq_arity_h fmt = + pp_header false fmt; + Format.fprintf fmt "static signed char arity[] = {@."; + Array.iter (fun (_, arity) -> + Format.fprintf fmt " %d,@." arity + ) opcodes; + Format.fprintf fmt "};@." let pp_vmopcodes_ml fmt = pp_header true fmt; Array.iteri (fun n s -> Format.fprintf fmt "let op%s = %d@.@." s n - ) opcodes + ) (Array.map fst opcodes) let usage () = - Format.eprintf "usage: %s [enum|jump|copml]@." Sys.argv.(0); + Format.eprintf "usage: %s [enum|jump|arity|copml]@." Sys.argv.(0); exit 1 let main () = match Sys.argv.(1) with | "enum" -> pp_coq_instruct_h Format.std_formatter | "jump" -> pp_coq_jumptbl_h Format.std_formatter + | "arity" -> pp_coq_arity_h Format.std_formatter | "copml" -> pp_vmopcodes_ml Format.std_formatter | _ -> usage () | exception Invalid_argument _ -> usage () diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index c19b883e3d..d517d215ed 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -24,6 +24,11 @@ open Environ compiler. mllambda represents a fragment of ML, and can easily be printed to OCaml code. *) +let debug_native_flag, debug_native_compiler = CDebug.create_full ~name:"native-compiler" () + +let keep_debug_files () = + CDebug.get_flag debug_native_flag + (** Local names **) (* The first component is there for debugging purposes only *) @@ -1939,7 +1944,7 @@ let compile_constant env sigma con cb = | Def t -> let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in - if !Flags.debug then Feedback.msg_debug (Pp.str "Generated lambda code"); + debug_native_compiler (fun () -> Pp.str "Generated lambda code"); let is_lazy = is_lazy t in let code = if is_lazy then mk_lazy code else code in let l = Constant.label con in @@ -1950,11 +1955,11 @@ let compile_constant env sigma con cb = let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in (auxdefs,mkMLlam [|univ|] code) in - if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code"); + debug_native_compiler (fun () -> Pp.str "Generated mllambda code"); let code = optimize_stk (Glet(Gconstant ("", con),code)::auxdefs) in - if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code"); + debug_native_compiler (fun () -> Pp.str "Optimized mllambda code"); code | _ -> let i = push_symbol (SymbConst con) in diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index aab6e1d4a0..90525a19b2 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -21,6 +21,10 @@ to OCaml code. *) type mllambda type global +val debug_native_compiler : CDebug.t + +val keep_debug_files : unit -> bool + val pp_global : Format.formatter -> global -> unit val mk_open : string -> global @@ -59,6 +63,8 @@ val empty_updates : code_location_updates val register_native_file : string -> unit +val is_loaded_native_file : string -> bool + val compile_constant_field : env -> string -> Constant.t -> global list -> 'a constant_body -> global list diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index d77ee759c6..f0ae5e2fbf 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Nativelib open Reduction open Util open Nativevalues @@ -151,22 +150,25 @@ let warn_no_native_compiler = strbrk " falling back to VM conversion test.") let native_conv_gen pb sigma env univs t1 t2 = - if not (typing_flags env).Declarations.enable_native_compiler then begin - warn_no_native_compiler (); - Vconv.vm_conv_gen pb env univs t1 t2 - end - else - let ml_filename, prefix = get_ml_filename () in + Nativelib.link_libraries (); + let ml_filename, prefix = Nativelib.get_ml_filename () in let code, upds = mk_conv_code env sigma prefix t1 t2 in - let fn = compile ml_filename code ~profile:false in - if !Flags.debug then Feedback.msg_debug (Pp.str "Running test..."); + let fn = Nativelib.compile ml_filename code ~profile:false in + debug_native_compiler (fun () -> Pp.str "Running test..."); let t0 = Sys.time () in - call_linker ~fatal:true ~prefix fn (Some upds); + let (rt1, rt2) = Nativelib.execute_library ~prefix fn upds in let t1 = Sys.time () in let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in - if !Flags.debug then Feedback.msg_debug (Pp.str time_info); + debug_native_compiler (fun () -> Pp.str time_info); (* TODO change 0 when we can have de Bruijn *) - fst (conv_val env pb 0 !rt1 !rt2 univs) + fst (conv_val env pb 0 rt1 rt2 univs) + +let native_conv_gen pb sigma env univs t1 t2 = + if not (typing_flags env).Declarations.enable_native_compiler then begin + warn_no_native_compiler (); + Vconv.vm_conv_gen pb env univs t1 t2 + end + else native_conv_gen pb sigma env univs t1 t2 (* Wrapper for [native_conv] above *) let native_conv cv_pb sigma env t1 t2 = diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 1e1085d5ff..73567e34cf 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -38,7 +38,7 @@ let ( / ) = Filename.concat let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "") let () = at_exit (fun () -> - if not !Flags.debug && Lazy.is_val my_temp_dir then + if not (keep_debug_files ()) && Lazy.is_val my_temp_dir then try let d = Lazy.force my_temp_dir in Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d); @@ -129,7 +129,7 @@ let call_compiler ?profile:(profile=false) ml_filename = ::"-w"::"a" ::include_dirs) @ ["-impl"; ml_filename] in - if !Flags.debug then Feedback.msg_debug (Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args))); + debug_native_compiler (fun () -> Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args))); try let res = CUnix.sys_command (Envars.ocamlfind ()) args in match res with @@ -142,7 +142,7 @@ let call_compiler ?profile:(profile=false) ml_filename = let compile fn code ~profile:profile = write_ml_code fn code; let r = call_compiler ~profile fn in - if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn; + if (not (keep_debug_files ())) && Sys.file_exists fn then Sys.remove fn; r type native_library = Nativecode.global list * Nativevalues.symbols @@ -160,34 +160,43 @@ let compile_library (code, symb) fn = let fn = dirname / basename in write_ml_code fn ~header code; let _ = call_compiler fn in - if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn + if (not (keep_debug_files ())) && Sys.file_exists fn then Sys.remove fn -(* call_linker links dynamically the code for constants in environment or a *) -(* conversion test. *) -let call_linker ?(fatal=true) ~prefix f upds = +let execute_library ~prefix f upds = rt1 := dummy_value (); rt2 := dummy_value (); if not (Sys.file_exists f) then - begin - let msg = "Cannot find native compiler file " ^ f in - if fatal then CErrors.user_err Pp.(str msg) - else if !Flags.debug then Feedback.msg_debug (Pp.str msg) - end - else - (try - if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; - register_native_file prefix - with Dynlink.Error _ as exn -> - let exn = Exninfo.capture exn in - if fatal then Exninfo.iraise exn - else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); - match upds with Some upds -> update_locations upds | _ -> () - -let link_library ~prefix ~dirname ~basename = + CErrors.user_err Pp.(str "Cannot find native compiler file " ++ str f); + if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; + register_native_file prefix; + update_locations upds; + (!rt1, !rt2) + +let link_library dirname prefix = + let basename = Dynlink.adapt_filename (prefix ^ "cmo") in (* We try both [output_dir] and [.coq-native], unfortunately from [Require] we don't know if we are loading a library in the build dir or in the installed layout *) let install_location = dirname / dft_output_dir / basename in let build_location = dirname / !output_dir / basename in let f = if Sys.file_exists build_location then build_location else install_location in - call_linker ~fatal:false ~prefix f None + try + if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; + register_native_file prefix + with + | Dynlink.Error _ as exn -> + debug_native_compiler (fun () -> CErrors.iprint (Exninfo.capture exn)) + +let delayed_link = ref [] + +let link_libraries () = + let delayed = List.rev !delayed_link in + delayed_link := []; + List.iter (fun (dirname, libname) -> + let prefix = mod_uid_of_dirpath libname ^ "." in + if not (Nativecode.is_loaded_native_file prefix) then + link_library dirname prefix + ) delayed + +let enable_library dirname libname = + delayed_link := (dirname, libname) :: !delayed_link diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 0c0fe3acc9..ba04c28ab0 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -7,7 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Nativecode (** This file provides facilities to access OCaml compiler and dynamic linker, used by the native compiler. *) @@ -25,7 +24,7 @@ val get_ml_filename : unit -> string * string (** [compile file code ~profile] will compile native [code] to [file], and return the name of the object file; this name depends on whether are in byte mode or not; file is expected to be .ml file *) -val compile : string -> global list -> profile:bool -> string +val compile : string -> Nativecode.global list -> profile:bool -> string type native_library = Nativecode.global list * Nativevalues.symbols @@ -33,18 +32,19 @@ type native_library = Nativecode.global list * Nativevalues.symbols but will perform some extra tweaks to handle [code] as a Coq lib. *) val compile_library : native_library -> string -> unit -val call_linker - : ?fatal:bool - -> prefix:string - -> string - -> code_location_updates option - -> unit +(** [execute_library file upds] dynamically loads library [file], + updates the library locations [upds], and returns the values stored + in [rt1] and [rt2] *) +val execute_library : + prefix:string -> string -> Nativecode.code_location_updates -> + Nativevalues.t * Nativevalues.t -val link_library - : prefix:string - -> dirname:string - -> basename:string - -> unit +(** [enable_library] marks the given library for dynamic loading + the next time [link_libraries] is called. *) +val enable_library : string -> Names.DirPath.t -> unit +val link_libraries : unit -> unit + +(* used for communication with the loaded libraries *) val rt1 : Nativevalues.t ref val rt2 : Nativevalues.t ref diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index c95880dc36..2e27fe071e 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -28,35 +28,35 @@ and translate_field prefix mp env acc (l,x) = match x with | SFBconst cb -> let con = Constant.make2 mp l in - (if !Flags.debug then + (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in - Feedback.msg_debug (Pp.str msg)); + Pp.str msg)); compile_constant_field env prefix con acc cb | SFBmind mb -> - (if !Flags.debug then + (debug_native_compiler (fun () -> let id = mb.mind_packets.(0).mind_typename in let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in - Feedback.msg_debug (Pp.str msg)); + Pp.str msg)); compile_mind_field mp l acc mb | SFBmodule md -> let mp = md.mod_mp in - (if !Flags.debug then + (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling module %s..." (ModPath.to_string mp) in - Feedback.msg_debug (Pp.str msg)); + Pp.str msg)); translate_mod prefix mp env md.mod_type acc | SFBmodtype mdtyp -> let mp = mdtyp.mod_mp in - (if !Flags.debug then + (debug_native_compiler (fun () -> let msg = Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp) in - Feedback.msg_debug (Pp.str msg)); + Pp.str msg)); translate_mod prefix mp env mdtyp.mod_type acc let dump_library mp dp env mod_expr = - if !Flags.debug then Feedback.msg_debug (Pp.str "Compiling library..."); + debug_native_compiler (fun () -> Pp.str "Compiling library..."); match mod_expr with | NoFunctor struc -> let env = add_structure mp struc empty_delta_resolver env in diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index bd6241ae67..c986cb473d 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -333,6 +333,22 @@ let rem accu x y = if is_int x && is_int y then no_check_rem x y else accu x y +let no_check_divs x y = + mk_uint (Uint63.divs (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let divs accu x y = + if is_int x && is_int y then no_check_divs x y + else accu x y + +let no_check_rems x y = + mk_uint (Uint63.rems (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let rems accu x y = + if is_int x && is_int y then no_check_rems x y + else accu x y + let no_check_l_sr x y = mk_uint (Uint63.l_sr (to_uint x) (to_uint y)) [@@ocaml.inline always] @@ -349,6 +365,14 @@ let l_sl accu x y = if is_int x && is_int y then no_check_l_sl x y else accu x y +let no_check_a_sr x y = + mk_uint (Uint63.a_sr (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let a_sr accu x y = + if is_int x && is_int y then no_check_a_sr x y + else accu x y + let no_check_l_and x y = mk_uint (Uint63.l_and (to_uint x) (to_uint y)) [@@ocaml.inline always] @@ -502,6 +526,22 @@ let le accu x y = if is_int x && is_int y then no_check_le x y else accu x y +let no_check_lts x y = + mk_bool (Uint63.lts (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let lts accu x y = + if is_int x && is_int y then no_check_lts x y + else accu x y + +let no_check_les x y = + mk_bool (Uint63.les (to_uint x) (to_uint y)) +[@@ocaml.inline always] + +let les accu x y = + if is_int x && is_int y then no_check_les x y + else accu x y + let no_check_compare x y = match Uint63.compare (to_uint x) (to_uint y) with | x when x < 0 -> (Obj.magic CmpLt:t) @@ -512,6 +552,16 @@ let compare accu x y = if is_int x && is_int y then no_check_compare x y else accu x y +let no_check_compares x y = + match Uint63.compares (to_uint x) (to_uint y) with + | x when x < 0 -> (Obj.magic CmpLt:t) + | 0 -> (Obj.magic CmpEq:t) + | _ -> (Obj.magic CmpGt:t) + +let compares accu x y = + if is_int x && is_int y then no_check_compares x y + else accu x y + let print x = Printf.fprintf stderr "%s" (Uint63.to_string (to_uint x)); flush stderr; diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index b9b75a9d7c..98cf4219a0 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -158,9 +158,12 @@ val sub : t -> t -> t -> t val mul : t -> t -> t -> t val div : t -> t -> t -> t val rem : t -> t -> t -> t +val divs : t -> t -> t -> t +val rems : t -> t -> t -> t val l_sr : t -> t -> t -> t val l_sl : t -> t -> t -> t +val a_sr : t -> t -> t -> t val l_and : t -> t -> t -> t val l_xor : t -> t -> t -> t val l_or : t -> t -> t -> t @@ -179,7 +182,10 @@ val addMulDiv : t -> t -> t -> t -> t val eq : t -> t -> t -> t val lt : t -> t -> t -> t val le : t -> t -> t -> t +val lts : t -> t -> t -> t +val les : t -> t -> t -> t val compare : t -> t -> t -> t +val compares : t -> t -> t -> t val print : t -> t @@ -205,12 +211,21 @@ val no_check_div : t -> t -> t val no_check_rem : t -> t -> t [@@ocaml.inline always] +val no_check_divs : t -> t -> t +[@@ocaml.inline always] + +val no_check_rems : t -> t -> t +[@@ocaml.inline always] + val no_check_l_sr : t -> t -> t [@@ocaml.inline always] val no_check_l_sl : t -> t -> t [@@ocaml.inline always] +val no_check_a_sr : t -> t -> t +[@@ocaml.inline always] + val no_check_l_and : t -> t -> t [@@ocaml.inline always] @@ -253,8 +268,16 @@ val no_check_lt : t -> t -> t val no_check_le : t -> t -> t [@@ocaml.inline always] +val no_check_lts : t -> t -> t +[@@ocaml.inline always] + +val no_check_les : t -> t -> t +[@@ocaml.inline always] + val no_check_compare : t -> t -> t +val no_check_compares : t -> t -> t + (** Support for machine floating point values *) val is_float : t -> bool diff --git a/kernel/primred.ml b/kernel/primred.ml index f0b4d6d362..23b7e13ab8 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -223,10 +223,16 @@ struct let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.div i1 i2) | Int63mod -> let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.rem i1 i2) + | Int63divs -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.divs i1 i2) + | Int63mods -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.rems i1 i2) | Int63lsr -> let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_sr i1 i2) | Int63lsl -> let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_sl i1 i2) + | Int63asr -> + let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.a_sr i1 i2) | Int63land -> let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_and i1 i2) | Int63lor -> @@ -276,6 +282,12 @@ struct | Int63le -> let i1, i2 = get_int2 evd args in E.mkBool env (Uint63.le i1 i2) + | Int63lts -> + let i1, i2 = get_int2 evd args in + E.mkBool env (Uint63.lts i1 i2) + | Int63les -> + let i1, i2 = get_int2 evd args in + E.mkBool env (Uint63.les i1 i2) | Int63compare -> let i1, i2 = get_int2 evd args in begin match Uint63.compare i1 i2 with @@ -283,6 +295,13 @@ struct | 0 -> E.mkEq env | _ -> E.mkGt env end + | Int63compares -> + let i1, i2 = get_int2 evd args in + begin match Uint63.compares i1 i2 with + | x when x < 0 -> E.mkLt env + | 0 -> E.mkEq env + | _ -> E.mkGt env + end | Float64opp -> let f = get_float1 evd args in E.mkFloat env (Float64.opp f) | Float64abs -> diff --git a/kernel/uint63.mli b/kernel/uint63.mli index 6b2519918a..ff8d1eefb7 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -48,6 +48,7 @@ val l_xor : t -> t -> t val l_or : t -> t -> t (* Arithmetic operations *) +val a_sr : t -> t -> t val add : t -> t -> t val sub : t -> t -> t val mul : t -> t -> t @@ -56,6 +57,10 @@ val rem : t -> t -> t val diveucl : t -> t -> t * t + (* Signed arithmetic opeartions *) +val divs : t -> t -> t +val rems : t -> t -> t + (* Specific arithmetic operations *) val mulc : t -> t -> t * t val addmuldiv : t -> t -> t -> t @@ -71,6 +76,11 @@ val equal : t -> t -> bool val le : t -> t -> bool val compare : t -> t -> int + (* signed comparision *) +val lts : t -> t -> bool +val les : t -> t -> bool +val compares : t -> t -> int + (* head and tail *) val head0 : t -> t val tail0 : t -> t diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index 4f2cbc4262..9c8401105e 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -52,6 +52,15 @@ let lt x y = let le x y = Int64.compare x y <= 0 + (* signed comparison *) +(* We shift the arguments by 1 to the left so that the top-most bit is interpreted as a sign *) +(* The zero at the end doesn't change the order (it is stable by multiplication by 2) *) +let lts x y = + Int64.(compare (shift_left x 1) (shift_left y 1)) < 0 + +let les x y = + Int64.(compare (shift_left x 1) (shift_left y 1)) <= 0 + (* logical shift *) let l_sl x y = if le 0L y && lt y 63L then mask63 (Int64.shift_left x (Int64.to_int y)) else 0L @@ -59,6 +68,12 @@ let l_sl x y = let l_sr x y = if le 0L y && lt y 63L then Int64.shift_right x (Int64.to_int y) else 0L + (* arithmetic shift (for sint63) *) +let a_sr x y = + if les 0L y && lts y 63L then + mask63 (Int64.shift_right (Int64.shift_left x 1) ((Int64.to_int y) + 1)) + else 0L + let l_and x y = Int64.logand x y let l_or x y = Int64.logor x y let l_xor x y = Int64.logxor x y @@ -86,6 +101,15 @@ let rem x y = let diveucl x y = (div x y, rem x y) + (* signed division *) +let divs x y = + if y = 0L then 0L else mask63 Int64.(div (shift_left x 1) (shift_left y 1)) + + (* signed modulo *) +let rems x y = + if y = 0L then 0L else + Int64.shift_right_logical (Int64.(rem (shift_left x 1) (shift_left y 1))) 1 + let addmuldiv p x y = l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p)) @@ -139,6 +163,8 @@ let equal (x : t) y = x = y let compare x y = Int64.compare x y +let compares x y = Int64.(compare (shift_left x 1) (shift_left y 1)) + (* Number of leading zeroes *) let head0 x = let r = ref 0 in @@ -198,22 +224,30 @@ let () = Callback.register "uint63 addcarry" addcarry; Callback.register "uint63 addmuldiv" addmuldiv; Callback.register "uint63 div" div; + Callback.register "uint63 divs" divs; Callback.register "uint63 div21_ml" div21; Callback.register "uint63 eq" equal; Callback.register "uint63 eq0" (equal Int64.zero); + Callback.register "uint63 eqm1" (equal (sub zero one)); Callback.register "uint63 head0" head0; Callback.register "uint63 land" l_and; Callback.register "uint63 leq" le; + Callback.register "uint63 les" les; Callback.register "uint63 lor" l_or; Callback.register "uint63 lsl" l_sl; Callback.register "uint63 lsr" l_sr; + Callback.register "uint63 asr" a_sr; Callback.register "uint63 lt" lt; + Callback.register "uint63 lts" lts; Callback.register "uint63 lxor" l_xor; Callback.register "uint63 mod" rem; + Callback.register "uint63 mods" rems; Callback.register "uint63 mul" mul; Callback.register "uint63 mulc_ml" mulc; + Callback.register "uint63 zero" zero; Callback.register "uint63 one" one; Callback.register "uint63 sub" sub; + Callback.register "uint63 neg" (sub zero); Callback.register "uint63 subcarry" subcarry; Callback.register "uint63 tail0" tail0; Callback.register "uint63 of_float" of_float; diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml index 8d052d6593..d017dafd3c 100644 --- a/kernel/uint63_63.ml +++ b/kernel/uint63_63.ml @@ -53,6 +53,10 @@ let l_sl x y = let l_sr x y = if 0 <= y && y < 63 then x lsr y else 0 + (* arithmetic shift (for sint63) *) +let a_sr x y = + if 0 <= y && y < 63 then x asr y else 0 + let l_and x y = x land y [@@ocaml.inline always] @@ -84,6 +88,14 @@ let rem (x : int) (y : int) = let diveucl x y = (div x y, rem x y) + (* signed division *) +let divs (x : int) (y : int) = + if y = 0 then 0 else x / y + + (* modulo *) +let rems (x : int) (y : int) = + if y = 0 then 0 else x mod y + let addmuldiv p x y = l_or (l_sl x p) (l_sr y (uint_size - p)) @@ -96,6 +108,15 @@ let le (x : int) (y : int) = (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000) [@@ocaml.inline always] + (* signed comparison *) +let lts (x : int) (y : int) = + x < y +[@@ocaml.inline always] + +let les (x : int) (y : int) = + x <= y +[@@ocaml.inline always] + let to_int_min n m = if lt n m then n else m [@@ocaml.inline always] @@ -175,9 +196,10 @@ let equal (x : int) (y : int) = x = y let compare (x:int) (y:int) = let x = x lxor 0x4000000000000000 in let y = y lxor 0x4000000000000000 in - if x > y then 1 - else if y > x then -1 - else 0 + Int.compare x y + +let compares (x : int) (y : int) = + Int.compare x y (* head tail *) diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index d3af8bf09b..caa263432e 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -226,8 +226,11 @@ let check_prim_op = function | Int63mul -> opCHECKMULINT63 | Int63div -> opCHECKDIVINT63 | Int63mod -> opCHECKMODINT63 + | Int63divs -> opCHECKDIVSINT63 + | Int63mods -> opCHECKMODSINT63 | Int63lsr -> opCHECKLSRINT63 | Int63lsl -> opCHECKLSLINT63 + | Int63asr -> opCHECKASRINT63 | Int63land -> opCHECKLANDINT63 | Int63lor -> opCHECKLORINT63 | Int63lxor -> opCHECKLXORINT63 @@ -242,7 +245,10 @@ let check_prim_op = function | Int63eq -> opCHECKEQINT63 | Int63lt -> opCHECKLTINT63 | Int63le -> opCHECKLEINT63 + | Int63lts -> opCHECKLTSINT63 + | Int63les -> opCHECKLESINT63 | Int63compare -> opCHECKCOMPAREINT63 + | Int63compares -> opCHECKCOMPARESINT63 | Float64opp -> opCHECKOPPFLOAT | Float64abs -> opCHECKABSFLOAT | Float64eq -> opCHECKEQFLOAT diff --git a/lib/cDebug.ml b/lib/cDebug.ml new file mode 100644 index 0000000000..efa7365b91 --- /dev/null +++ b/lib/cDebug.ml @@ -0,0 +1,92 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type flag = bool ref + +type t = (unit -> Pp.t) -> unit + +let debug = ref CString.Map.empty + +(* Used to remember level of Set Debug "all" for debugs created by + plugins dynlinked after the Set *) +let all_flag = ref false + +let set_debug_backtrace b = + Exninfo.record_backtrace b + +let set_debug_all b = + set_debug_backtrace b; + CString.Map.iter (fun _ flag -> flag := b) !debug; + all_flag := b + +let create_full ~name () = + let anomaly pp = CErrors.anomaly ~label:"CDebug.create" pp in + let () = match name with + | "all"|"backtrace" -> anomaly Pp.(str"The debug name \""++str name++str"\" is reserved.") + | _ -> + if CString.Map.mem name !debug then + anomaly Pp.(str "The debug name \"" ++ str name ++ str "\" is already used.") + in + let pp x = + Feedback.msg_debug Pp.(str "[" ++ str name ++ str "] " ++ x) + in + let flag = ref !all_flag in + debug := CString.Map.add name flag !debug; + let pp x = + if !flag + then pp (x ()) + in + flag, pp + +let create ~name () = + snd (create_full ~name ()) + +let get_flag flag = !flag + +let warn_unknown_debug = CWarnings.create ~name:"unknown-debug-flag" ~category:"option" + Pp.(fun name -> str "There is no debug flag \"" ++ str name ++ str "\".") + +let get_flags () = + let pp_flag name flag = if flag then name else "-"^name in + let flags = + CString.Map.fold + (fun name v acc -> pp_flag name !v :: acc) + !debug [] + in + let all = pp_flag "all" !all_flag in + let bt = pp_flag "backtrace" (Printexc.backtrace_status()) in + String.concat "," (all::bt::flags) + +exception Error + +let parse_flags s = + let parse_flag s = + if CString.is_empty s then raise Error + else if s.[0] = '-' + then String.sub s 1 (String.length s - 1), false + else s, true + in + try + Some (CList.map parse_flag @@ String.split_on_char ',' s) + with Error -> None + +let set_flags s = match parse_flags s with + | None -> CErrors.user_err Pp.(str "Syntax error in debug flags.") + | Some flags -> + let set_one_flag (name,b) = match name with + | "all" -> set_debug_all b + | "backtrace" -> set_debug_backtrace b + | _ -> match CString.Map.find_opt name !debug with + | None -> warn_unknown_debug name + | Some flag -> flag := b + in + List.iter set_one_flag flags + +let misc, pp_misc = create_full ~name:"misc" () diff --git a/lib/cDebug.mli b/lib/cDebug.mli new file mode 100644 index 0000000000..846c4b493b --- /dev/null +++ b/lib/cDebug.mli @@ -0,0 +1,50 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +type flag + +type t = (unit -> Pp.t) -> unit + +(** Creates a debug component, which may be used to print debug + messages. + + A debug component is named by the string [name]. It is either + active or inactive. + + The special component ["all"] may be used to control all components. + + There is also a special component ["backtrace"] to control + backtrace recording. +*) +val create : name:string -> unit -> t + +(** Useful when interacting with a component from code, typically when + doing something more complicated than printing. + + Note that the printer function prints some metadata compared to + [ fun pp -> if get_flag flag then Feedback.msg_debug (pp ()) ] + *) +val create_full : name:string -> unit -> flag * t + +val get_flag : flag -> bool + +(** [get_flags] and [set_flags] use the user syntax: a comma separated + list of activated "component" and "-component"s. [get_flags] starts + with "all" or "-all" and lists all components after it (even if redundant). *) +val get_flags : unit -> string + +(** Components not mentioned are not affected (use the "all" component + at the start if you want to reset everything). *) +val set_flags : string -> unit + +val set_debug_all : bool -> unit + +val misc : flag +val pp_misc : t diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 760c07783b..1baedb64c9 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -30,6 +30,7 @@ let anomaly ?loc ?info ?label pp = let info = Option.cata (Loc.add_loc info) info loc in Exninfo.iraise (Anomaly (label, pp), info) +(* TODO remove the option *) exception UserError of string option * Pp.t (* User errors *) let user_err ?loc ?info ?hdr strm = @@ -46,7 +47,7 @@ exception Timeout = Control.Timeout let where = function | None -> mt () | Some s -> - if !Flags.debug then str "in " ++ str s ++ str ":" ++ spc () else mt () + str "in " ++ str s ++ str ":" ++ spc () let raw_anomaly e = match e with | Anomaly (s, pps) -> @@ -133,7 +134,7 @@ let print_no_report e = iprint_no_report (e, Exninfo.info e) let _ = register_handler begin function | UserError(s, pps) -> - Some (where s ++ pps) + Some pps | _ -> None end diff --git a/lib/flags.ml b/lib/flags.ml index 83733cf00d..57e879add7 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -46,7 +46,6 @@ let async_proofs_is_worker () = !async_proofs_worker_id <> "master" let load_vos_libraries = ref false -let debug = ref false let xml_debug = ref false let in_debugger = ref false diff --git a/lib/flags.mli b/lib/flags.mli index ebd23a4d20..e10e2c8cb8 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -40,7 +40,6 @@ val async_proofs_is_worker : unit -> bool val load_vos_libraries : bool ref (** Debug flags *) -val debug : bool ref val xml_debug : bool ref val in_debugger : bool ref val in_toplevel : bool ref diff --git a/lib/lib.mllib b/lib/lib.mllib index 4e08e87084..bbc9966498 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -10,6 +10,7 @@ Loc Feedback CErrors CWarnings +CDebug AcyclicGraph Rtree diff --git a/lib/spawn.ml b/lib/spawn.ml index 2fe7b31d04..27b4387b61 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -13,7 +13,7 @@ let prefer_sock = Sys.os_type = "Win32" let accept_timeout = 10.0 let pr_err s = Printf.eprintf "(Spawn ,%d) %s\n%!" (Unix.getpid ()) s -let prerr_endline s = if !Flags.debug then begin pr_err s end else () +let prerr_endline s = if CDebug.(get_flag misc) then begin pr_err s end else () type req = ReqDie | Hello of int * int diff --git a/library/nametab.ml b/library/nametab.ml index e94b696b60..bd96446f1c 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -574,7 +574,7 @@ let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) with Not_found as exn -> let exn, info = Exninfo.capture exn in - if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); + if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str "pr_global_env not found"); Exninfo.iraise (exn, info) let global_inductive qid = diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 129b220680..6617f4726e 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -19,20 +19,12 @@ open Sorts open Constr open Context open Vars -open Goptions open Tacmach open Util let init_size=5 -let cc_verbose= - declare_bool_option_and_ref - ~depr:false - ~key:["Congruence";"Verbose"] - ~value:false - -let debug x = - if cc_verbose () then Feedback.msg_debug (x ()) +let debug_congruence = CDebug.create ~name:"congruence" () (* Signature table *) @@ -576,7 +568,7 @@ let add_inst state (inst,int_subst) = Control.check_for_interrupt (); if state.rew_depth > 0 then if is_redundant state inst.qe_hyp_id int_subst then - debug (fun () -> str "discarding redundant (dis)equality") + debug_congruence (fun () -> str "discarding redundant (dis)equality") else begin Identhash.add state.q_history inst.qe_hyp_id int_subst; @@ -591,7 +583,7 @@ let add_inst state (inst,int_subst) = state.rew_depth<-pred state.rew_depth; if inst.qe_pol then begin - debug (fun () -> + debug_congruence (fun () -> (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++ (str " [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++ pr_term state.env state.sigma s ++ str " == " ++ pr_term state.env state.sigma t ++ str "]")); @@ -599,7 +591,7 @@ let add_inst state (inst,int_subst) = end else begin - debug (fun () -> + debug_congruence (fun () -> (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++ (str " [" ++ Printer.pr_econstr_env state.env state.sigma (EConstr.of_constr prf) ++ str " : " ++ pr_term state.env state.sigma s ++ str " <> " ++ pr_term state.env state.sigma t ++ str "]")); @@ -630,7 +622,7 @@ let join_path uf i j= min_path (down_path uf i [],down_path uf j []) let union state i1 i2 eq= - debug (fun () -> str "Linking " ++ pr_idx_term state.env state.sigma state.uf i1 ++ + debug_congruence (fun () -> str "Linking " ++ pr_idx_term state.env state.sigma state.uf i1 ++ str " and " ++ pr_idx_term state.env state.sigma state.uf i2 ++ str "."); let r1= get_representative state.uf i1 and r2= get_representative state.uf i2 in @@ -670,7 +662,7 @@ let union state i1 i2 eq= | _,_ -> () let merge eq state = (* merge and no-merge *) - debug + debug_congruence (fun () -> str "Merging " ++ pr_idx_term state.env state.sigma state.uf eq.lhs ++ str " and " ++ pr_idx_term state.env state.sigma state.uf eq.rhs ++ str "."); let uf=state.uf in @@ -683,7 +675,7 @@ let merge eq state = (* merge and no-merge *) union state j i (swap eq) let update t state = (* update 1 and 2 *) - debug + debug_congruence (fun () -> str "Updating term " ++ pr_idx_term state.env state.sigma state.uf t ++ str "."); let (i,j) as sign = signature state.uf t in let (u,v) = subterms state.uf t in @@ -745,7 +737,7 @@ let process_constructor_mark t i rep pac state = end let process_mark t m state = - debug + debug_congruence (fun () -> str "Processing mark for term " ++ pr_idx_term state.env state.sigma state.uf t ++ str "."); let i=find state.uf t in let rep=get_representative state.uf i in @@ -766,7 +758,7 @@ let check_disequalities state = if Int.equal (find uf dis.lhs) (find uf dis.rhs) then (str "Yes", Some dis) else (str "No", check_aux q) in - let _ = debug + let _ = debug_congruence (fun () -> str "Checking if " ++ pr_idx_term state.env state.sigma state.uf dis.lhs ++ str " = " ++ pr_idx_term state.env state.sigma state.uf dis.rhs ++ str " ... " ++ info) in ans @@ -953,7 +945,7 @@ let find_instances state = let pb_stack= init_pb_stack state in let res =ref [] in let _ = - debug (fun () -> str "Running E-matching algorithm ... "); + debug_congruence (fun () -> str "Running E-matching algorithm ... "); try while true do Control.check_for_interrupt (); @@ -964,7 +956,7 @@ let find_instances state = !res let rec execute first_run state = - debug (fun () -> str "Executing ... "); + debug_congruence (fun () -> str "Executing ... "); try while Control.check_for_interrupt (); @@ -974,7 +966,7 @@ let rec execute first_run state = None -> if not(Int.Set.is_empty state.pa_classes) then begin - debug (fun () -> str "First run was incomplete, completing ... "); + debug_congruence (fun () -> str "First run was incomplete, completing ... "); complete state; execute false state end @@ -989,12 +981,12 @@ let rec execute first_run state = end else begin - debug (fun () -> str "Out of instances ... "); + debug_congruence (fun () -> str "Out of instances ... "); None end else begin - debug (fun () -> str "Out of depth ... "); + debug_congruence (fun () -> str "Out of depth ... "); None end | Some dis -> Some diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 3270f74479..047756deef 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -121,7 +121,7 @@ val term_equal : term -> term -> bool val constr_of_term : term -> constr -val debug : (unit -> Pp.t) -> unit +val debug_congruence : CDebug.t val forest : state -> forest diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index 53d8c5bdd9..e7e0822916 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -95,13 +95,13 @@ let pinject p c n a = p_rule=Inject(p,c,n,a)} let rec equal_proof env sigma uf i j= - debug (fun () -> str "equal_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); + debug_congruence (fun () -> str "equal_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); if i=j then prefl (term uf i) else let (li,lj)=join_path uf i j in ptrans (path_proof env sigma uf i li) (psym (path_proof env sigma uf j lj)) and edge_proof env sigma uf ((i,j),eq)= - debug (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); + debug_congruence (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); let pi=equal_proof env sigma uf i eq.lhs in let pj=psym (equal_proof env sigma uf j eq.rhs) in let pij= @@ -117,7 +117,7 @@ and edge_proof env sigma uf ((i,j),eq)= ptrans (ptrans pi pij) pj and constr_proof env sigma uf i ipac= - debug (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20)); + debug_congruence (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20)); let t=find_oldest_pac uf i ipac in let eq_it=equal_proof env sigma uf i t in if ipac.args=[] then @@ -130,20 +130,20 @@ and constr_proof env sigma uf i ipac= ptrans eq_it (pcongr p (prefl targ)) and path_proof env sigma uf i l= - debug (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++ + debug_congruence (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++ (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}"); match l with | [] -> prefl (term uf i) | x::q->ptrans (path_proof env sigma uf (snd (fst x)) q) (edge_proof env sigma uf x) and congr_proof env sigma uf i j= - debug (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); + debug_congruence (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); let (i1,i2) = subterms uf i and (j1,j2) = subterms uf j in pcongr (equal_proof env sigma uf i1 j1) (equal_proof env sigma uf i2 j2) and ind_proof env sigma uf i ipac j jpac= - debug (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); + debug_congruence (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j); let p=equal_proof env sigma uf i j and p1=constr_proof env sigma uf i ipac and p2=constr_proof env sigma uf j jpac in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 72f77508d8..341fde7b77 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -420,16 +420,16 @@ let cc_tactic depth additionnal_terms = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in Coqlib.(check_required_library logic_module_name); - let _ = debug (fun () -> Pp.str "Reading goal ...") in + let _ = debug_congruence (fun () -> Pp.str "Reading goal ...") in let state = make_prb gl depth additionnal_terms in - let _ = debug (fun () -> Pp.str "Problem built, solving ...") in + let _ = debug_congruence (fun () -> Pp.str "Problem built, solving ...") in let sol = execute true state in - let _ = debug (fun () -> Pp.str "Computation completed.") in + let _ = debug_congruence (fun () -> Pp.str "Computation completed.") in let uf=forest state in match sol with None -> Tacticals.New.tclFAIL 0 (str "congruence failed") | Some reason -> - debug (fun () -> Pp.str "Goal solved, generating proof ..."); + debug_congruence (fun () -> Pp.str "Goal solved, generating proof ..."); match reason with Discrimination (i,ipac,j,jpac) -> let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index d1403558ad..61966b60c0 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -14,7 +14,7 @@ open Pp open Lazy module NamedDecl = Context.Named.Declaration -let debug = false +let debug_zify = CDebug.create ~name:"zify" () (* The following [constr] are necessary for constructing the proof terms *) @@ -805,12 +805,11 @@ let pp_prf prf = let interp_prf evd inj source prf = let t, prf' = interp_prf evd inj source prf in - if debug then - Feedback.msg_debug + debug_zify (fun () -> Pp.( str "interp_prf " ++ gl_pr_constr inj.EInjT.inj ++ str " " ++ gl_pr_constr source ++ str " = " ++ gl_pr_constr t ++ str " by " - ++ gl_pr_constr prf' ++ str " from " ++ pp_prf prf ++ fnl ()); + ++ gl_pr_constr prf' ++ str " from " ++ pp_prf prf ++ fnl ())); (t, prf') let mkvar evd inj e = @@ -888,13 +887,12 @@ let app_unop evd src unop arg prf = let app_unop evd src unop arg prf = let res = app_unop evd src unop arg prf in - if debug then - Feedback.msg_debug + debug_zify (fun () -> Pp.( str "\napp_unop " ++ pp_prf evd unop.EUnOpT.inj1_t arg prf ++ str " => " - ++ pp_prf evd unop.EUnOpT.inj2_t src res); + ++ pp_prf evd unop.EUnOpT.inj2_t src res)); res let app_binop evd src binop arg1 prf1 arg2 prf2 = @@ -1066,8 +1064,7 @@ let match_operator env evd hd args (t, d) = let pp_trans_expr env evd e res = let {deriv = inj} = get_injection env evd e.typ in - if debug then - Feedback.msg_debug Pp.(str "\ntrans_expr " ++ pp_prf evd inj e.constr res); + debug_zify (fun () -> Pp.(str "\ntrans_expr " ++ pp_prf evd inj e.constr res)); res let declared_term env evd hd args = @@ -1187,7 +1184,7 @@ let trans_binrel evd src rop a1 prf1 a2 prf2 = let trans_binrel evd src rop a1 prf1 a2 prf2 = let res = trans_binrel evd src rop a1 prf1 a2 prf2 in - if debug then Feedback.msg_debug Pp.(str "\ntrans_binrel " ++ pp_prfp res); + debug_zify (fun () -> Pp.(str "\ntrans_binrel " ++ pp_prfp res)); res let mkprf t p = @@ -1199,11 +1196,10 @@ let mkprf t p = let mkprf t p = let t', p = mkprf t p in - if debug then - Feedback.msg_debug + debug_zify (fun () -> Pp.( str "mkprf " ++ gl_pr_constr t ++ str " <-> " ++ gl_pr_constr t' - ++ str " by " ++ gl_pr_constr p); + ++ str " by " ++ gl_pr_constr p)); (t', p) let trans_bin_prop op_constr op_iff t1 p1 t2 p2 = @@ -1221,7 +1217,7 @@ let trans_bin_prop op_constr op_iff t1 p1 t2 p2 = let trans_bin_prop op_constr op_iff t1 p1 t2 p2 = let prf = trans_bin_prop op_constr op_iff t1 p1 t2 p2 in - if debug then Feedback.msg_debug (pp_prfp prf); + debug_zify (fun () -> pp_prfp prf); prf let trans_un_prop op_constr op_iff p1 prf1 = @@ -1285,8 +1281,7 @@ let trans_hyps env evd l = [] l let trans_hyp h t0 prfp = - if debug then - Feedback.msg_debug Pp.(str "trans_hyp: " ++ pp_prfp prfp ++ fnl ()); + debug_zify (fun () -> Pp.(str "trans_hyp: " ++ pp_prfp prfp ++ fnl ())); match prfp with | IProof -> Tacticals.New.tclIDTAC (* Should detect before *) | CProof t' -> @@ -1313,8 +1308,7 @@ let trans_hyp h t0 prfp = (tclTHEN (Tactics.clear [h]) (Tactics.rename_hyp [(h', h)]))))) let trans_concl prfp = - if debug then - Feedback.msg_debug Pp.(str "trans_concl: " ++ pp_prfp prfp ++ fnl ()); + debug_zify (fun () -> Pp.(str "trans_concl: " ++ pp_prfp prfp ++ fnl ())); match prfp with | IProof -> Tacticals.New.tclIDTAC | CProof t -> diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml index 1caa042db6..19bdcbac58 100644 --- a/plugins/nsatz/utile.ml +++ b/plugins/nsatz/utile.ml @@ -1,9 +1,9 @@ (* Printing *) let pr x = - if !Flags.debug then (Format.printf "@[%s@]" x; flush(stdout);)else () + if CDebug.(get_flag misc) then (Format.printf "@[%s@]" x; flush(stdout);)else () let prt0 s = () (* print_string s;flush(stdout)*) -let sinfo s = if !Flags.debug then Feedback.msg_debug (Pp.str s) -let info s = if !Flags.debug then Feedback.msg_debug (Pp.str (s ())) +let sinfo s = if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str s) +let info s = if CDebug.(get_flag misc) then Feedback.msg_debug (Pp.str (s ())) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 4d57abb465..41fd96ccb5 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -252,7 +252,7 @@ let interp_refine ist gl rc = in let sigma, c = Pretyping.understand_ltac flags (pf_env gl) (project gl) vars kind rc in (* ppdebug(lazy(str"sigma@interp_refine=" ++ pr_evar_map None sigma)); *) - ppdebug(lazy(str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c)); + debug_ssr (fun () -> str"c@interp_refine=" ++ Printer.pr_econstr_env (pf_env gl) sigma c); (sigma, (sigma, c)) @@ -1207,7 +1207,7 @@ let gentac gen = Proofview.V82.tactic begin fun gl -> (* ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *) let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux gl false gen in - ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c)); + debug_ssr (fun () -> str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c); let gl = pf_merge_uc ucst gl in if conv then tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl)) (old_cleartac clr) gl diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 582c45cde1..78a59abda9 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -126,17 +126,17 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = fun (oc, orig_clr, occ, c_gen) -> pfLIFT begin fun gl -> let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in - ppdebug(lazy(Pp.str(if is_case then "==CASE==" else "==ELIM=="))); + debug_ssr (fun () -> (Pp.str(if is_case then "==CASE==" else "==ELIM=="))); let fire_subst gl t = Reductionops.nf_evar (project gl) t in let is_undef_pat = function | sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t) | _ -> false in let match_pat env p occ h cl = let sigma0 = project orig_gl in - ppdebug(lazy Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p)); + debug_ssr (fun () -> Pp.(str"matching: " ++ pr_occ occ ++ pp_pattern env p)); let (c,ucst), cl = fill_occ_pattern ~raise_NoMatch:true env sigma0 (EConstr.Unsafe.to_constr cl) p occ h in - ppdebug(lazy Pp.(str" got: " ++ pr_constr_env env sigma0 c)); + debug_ssr (fun () -> Pp.(str" got: " ++ pr_constr_env env sigma0 c)); c, EConstr.of_constr cl, ucst in let mkTpat gl t = (* takes a term, refreshes it and makes a T pattern *) let n, t, _, ucst = pf_abs_evars orig_gl (project gl, fire_subst gl t) in @@ -212,10 +212,10 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let renamed_tys = Array.mapi (fun j (ctx, cty) -> let t = Term.it_mkProd_or_LetIn cty ctx in - ppdebug(lazy Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t)); + debug_ssr (fun () -> Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t)); let t = Arguments_renaming.rename_type t (GlobRef.ConstructRef((kn,i),j+1)) in - ppdebug(lazy Pp.(str"Done Search " ++ Printer.pr_constr_env env (project gl) t)); + debug_ssr (fun () -> Pp.(str"Done Search " ++ Printer.pr_constr_env env (project gl) t)); t) tys in @@ -241,8 +241,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = in let () = let sigma = project gl in - ppdebug(lazy Pp.(str"elim= "++ pr_econstr_pat env sigma elim)); - ppdebug(lazy Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in + debug_ssr (fun () -> Pp.(str"elim= "++ pr_econstr_pat env sigma elim)); + debug_ssr (fun () -> Pp.(str"elimty= "++ pr_econstr_pat env sigma elimty)) in let open EConstr in let inf_deps_r = match kind_of_type (project gl) elimty with | AtomicType (_, args) -> List.rev (Array.to_list args) @@ -301,7 +301,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = | Some (c, _, _,gl) -> Some(true, gl) | None -> None in first [try_c_last_arg;try_c_last_pattern] in - ppdebug(lazy Pp.(str"c_is_head_p= " ++ bool c_is_head_p)); + debug_ssr (fun () -> Pp.(str"c_is_head_p= " ++ bool c_is_head_p)); let gl, predty = pfe_type_of gl pred in (* Patterns for the inductive types indexes to be bound in pred are computed * looking at the ones provided by the user and the inferred ones looking at @@ -321,7 +321,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = loop (patterns @ [i, p, inf_t, occ]) (clr_t @ clr) (i+1) (deps, inf_deps) | [], c :: inf_deps -> - ppdebug(lazy Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c)); + debug_ssr (fun () -> Pp.(str"adding inf pattern " ++ pr_econstr_pat env (project gl) c)); loop (patterns @ [i, mkTpat gl c, c, allocc]) clr (i+1) ([], inf_deps) | _::_, [] -> errorstrm Pp.(str "Too many dependent abstractions") in @@ -337,8 +337,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = loop [] orig_clr (List.length head_p+1) (List.rev deps, inf_deps_r) in head_p @ patterns, Util.List.uniquize clr, gl in - ppdebug(lazy Pp.(pp_concat (str"patterns=") (List.map pp_pat patterns))); - ppdebug(lazy Pp.(pp_concat (str"inf. patterns=") (List.map (pp_inf_pat gl) patterns))); + debug_ssr (fun () -> Pp.(pp_concat (str"patterns=") (List.map pp_pat patterns))); + debug_ssr (fun () -> Pp.(pp_concat (str"inf. patterns=") (List.map (pp_inf_pat gl) patterns))); (* Predicate generation, and (if necessary) tactic to generalize the * equation asked by the user *) let elim_pred, gen_eq_tac, clr, gl = @@ -348,7 +348,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let match_or_postpone (cl, gl, post) (h, p, inf_t, occ) = let p = unif_redex gl p inf_t in if is_undef_pat p then - let () = ppdebug(lazy Pp.(str"postponing " ++ pp_pattern env p)) in + let () = debug_ssr (fun () -> Pp.(str"postponing " ++ pp_pattern env p)) in cl, gl, post @ [h, p, inf_t, occ] else try let c, cl, ucst = match_pat env p occ h cl in @@ -420,8 +420,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = else gl, concl in concl, gen_eq_tac, clr, gl in let gl, pty = pf_e_type_of gl elim_pred in - ppdebug(lazy Pp.(str"elim_pred=" ++ pp_term gl elim_pred)); - ppdebug(lazy Pp.(str"elim_pred_ty=" ++ pp_term gl pty)); + debug_ssr (fun () -> Pp.(str"elim_pred=" ++ pp_term gl elim_pred)); + debug_ssr (fun () -> Pp.(str"elim_pred_ty=" ++ pp_term gl pty)); let gl = pf_unify_HO gl pred elim_pred in let elim = fire_subst gl elim in let gl = pf_resolve_typeclasses ~where:elim ~fail:false gl in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 0008d31ffd..92a481dd18 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -76,7 +76,7 @@ let simpltac s = Proofview.Goal.enter (fun _ -> simpltac s) (** The "congr" tactic *) let interp_congrarg_at ist gl n rf ty m = - ppdebug(lazy Pp.(str"===interp_congrarg_at===")); + debug_ssr (fun () -> Pp.(str"===interp_congrarg_at===")); let congrn, _ = mkSsrRRef "nary_congruence" in let args1 = mkRnat n :: mkRHoles n @ [ty] in let args2 = mkRHoles (3 * n) in @@ -84,7 +84,7 @@ let interp_congrarg_at ist gl n rf ty m = if i + n > m then None else try let rt = mkRApp congrn (args1 @ mkRApp rf (mkRHoles i) :: args2) in - ppdebug(lazy Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) (project gl) rt)); + debug_ssr (fun () -> Pp.(str"rt=" ++ Printer.pr_glob_constr_env (pf_env gl) (project gl) rt)); Some (interp_refine ist gl rt) with _ -> loop (i + 1) in loop 0 @@ -92,8 +92,8 @@ let interp_congrarg_at ist gl n rf ty m = let pattern_id = mk_internal_id "pattern value" let congrtac ((n, t), ty) ist gl = - ppdebug(lazy (Pp.str"===congr===")); - ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl))); + debug_ssr (fun () -> (Pp.str"===congr===")); + debug_ssr (fun () -> Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (Tacmach.pf_concl gl))); let sigma, _ as it = interp_term (pf_env gl) (project gl) ist t in let gl = pf_merge_uc_of sigma gl in let _, f, _, _ucst = pf_abs_evars gl it in @@ -124,8 +124,8 @@ let newssrcongrtac arg ist = Proofview.Goal.enter_one ~__LOC__ begin fun _g -> (Ssrcommon.tacMK_SSR_CONST "ssr_congr_arrow") end >>= fun arr -> Proofview.V82.tactic begin fun gl -> - ppdebug(lazy Pp.(str"===newcongr===")); - ppdebug(lazy Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl))); + debug_ssr (fun () -> Pp.(str"===newcongr===")); + debug_ssr (fun () -> Pp.(str"concl=" ++ Printer.pr_econstr_env (pf_env gl) (project gl) (pf_concl gl))); (* utils *) let fs gl t = Reductionops.nf_evar (project gl) t in let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl = @@ -385,8 +385,8 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_ | Pretype_errors.PretypeError (env, sigma, te) -> raise (PRtype_error (Some (env, sigma, te))) | e when CErrors.noncritical e -> raise (PRtype_error None) in - ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof)); - ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); + debug_ssr (fun () -> Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof)); + debug_ssr (fun () -> Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty)); try Proofview.V82.of_tactic (refine_with ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof)) gl with e when CErrors.noncritical e -> @@ -435,12 +435,12 @@ let rwcltac ?under ?map_redex cl rdx dir sr = let sigma0 = Evd.set_universe_context sigma0 ucst in let rdxt = Retyping.get_type_of env (fst sr) rdx in (* ppdebug(lazy(str"sigma@rwcltac=" ++ pr_evar_map None (fst sr))); *) - ppdebug(lazy Pp.(str"r@rwcltac=" ++ pr_econstr_env env sigma0 (snd sr))); + debug_ssr (fun () -> Pp.(str"r@rwcltac=" ++ pr_econstr_env env sigma0 (snd sr))); let cvtac, rwtac, sigma0 = if EConstr.Vars.closed0 sigma0 r' then let sigma, c, c_eq = fst sr, snd sr, Coqlib.(lib_ref "core.eq.type") in let sigma, c_ty = Typing.type_of env sigma c in - ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); + debug_ssr (fun () -> Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty)); let open EConstr in match kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq -> @@ -521,7 +521,7 @@ let rwprocess_rule env dir rule = let t = if red = 1 then Tacred.hnf_constr env sigma t0 else Reductionops.whd_betaiotazeta env sigma t0 in - ppdebug(lazy Pp.(str"rewrule="++pr_econstr_pat env sigma t)); + debug_ssr (fun () -> Pp.(str"rewrule="++pr_econstr_pat env sigma t)); match EConstr.kind sigma t with | Prod (_, xt, at) -> let sigma = Evd.create_evar_defs sigma in diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index f2c7f495b3..bc46c23761 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -296,8 +296,8 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave = | Some id -> if pats = [] then Tacticals.New.tclIDTAC else let args = Array.of_list args in - ppdebug(lazy(str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args)))); - ppdebug(lazy(str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct)); + debug_ssr (fun () -> str"specialized="++ pr_econstr_env (pf_env gl) (project gl) EConstr.(mkApp (mkVar id,args))); + debug_ssr (fun () -> str"specialized_ty="++ pr_econstr_env (pf_env gl) (project gl) ct); Tacticals.New.tclTHENS (basecuttac "ssr_have" ct) [Tactics.apply EConstr.(mkApp (mkVar id,args)); Tacticals.New.tclIDTAC] in "ssr_have", @@ -395,7 +395,7 @@ let intro_lock ipats = Array.length args = 3 && is_app_evar sigma args.(2) -> protect_subgoal env sigma hd args | _ -> - ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t)); + debug_ssr (fun () -> Pp.(str"under: stop:" ++ pr_econstr_env env sigma t)); Proofview.tclUNIT () end) @@ -468,13 +468,13 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint = | Some l -> [IPatCase(Regular [l;[]])] in let map_redex env evar_map ~before:_ ~after:t = - ppdebug(lazy Pp.(str"under vars: " ++ prlist Names.Name.print varnames)); + debug_ssr (fun () -> Pp.(str"under vars: " ++ prlist Names.Name.print varnames)); let evar_map, ty = Typing.type_of env evar_map t in let new_t = (* pretty-rename the bound variables *) try begin match EConstr.destApp evar_map t with (f, ar) -> let lam = Array.last ar in - ppdebug(lazy Pp.(str"under: mapping:" ++ + debug_ssr(fun () -> Pp.(str"under: mapping:" ++ pr_econstr_env env evar_map lam)); let new_lam = pretty_rename evar_map lam varnames in let new_ar, len1 = Array.copy ar, pred (Array.length ar) in @@ -482,10 +482,10 @@ let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint = EConstr.mkApp (f, new_ar) end with | DestKO -> - ppdebug(lazy Pp.(str"under: cannot pretty-rename bound variables with destApp")); + debug_ssr (fun () -> Pp.(str"under: cannot pretty-rename bound variables with destApp")); t in - ppdebug(lazy Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t)); + debug_ssr (fun () -> Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t)); evar_map, new_t in let undertacs = diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 1e940b5ad3..f8abed5482 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -324,7 +324,7 @@ end `tac`, where k is the size of `seeds` *) let tclSEED_SUBGOALS seeds tac = tclTHENin tac (fun i n -> - Ssrprinters.ppdebug (lazy Pp.(str"seeding")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"seeding")); (* eg [case: (H _ : nat)] generates 3 goals: - 1 for _ - 2 for the nat constructors *) @@ -416,11 +416,11 @@ let tclMK_ABSTRACT_VARS ids = (* Debugging *) let tclLOG p t = tclUNIT () >>= begin fun () -> - Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ pr_ipatop p)); + Ssrprinters.debug_ssr (fun () -> Pp.(str "exec: " ++ pr_ipatop p)); tclUNIT () end <*> Goal.enter begin fun g -> - Ssrprinters.ppdebug (lazy Pp.(str" on state:" ++ spc () ++ + Ssrprinters.debug_ssr (fun () -> Pp.(str" on state:" ++ spc () ++ isPRINT g ++ str" goal:" ++ spc () ++ Printer.pr_goal (Goal.print g))); tclUNIT () @@ -429,7 +429,7 @@ let tclLOG p t = t p >>= fun ret -> Goal.enter begin fun g -> - Ssrprinters.ppdebug (lazy Pp.(str "done: " ++ isPRINT g)); + Ssrprinters.debug_ssr (fun () -> Pp.(str "done: " ++ isPRINT g)); tclUNIT () end >>= fun () -> tclUNIT ret @@ -579,10 +579,10 @@ let tclCompileIPats l = elab l ;; let tclCompileIPats l = - Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats input: " ++ + Ssrprinters.debug_ssr (fun () -> Pp.(str "tclCompileIPats input: " ++ prlist_with_sep spc Ssrprinters.pr_ipat l)); let ops = tclCompileIPats l in - Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats output: " ++ + Ssrprinters.debug_ssr (fun () -> Pp.(str "tclCompileIPats output: " ++ prlist_with_sep spc pr_ipatop ops)); ops @@ -597,11 +597,11 @@ let main ?eqtac ~first_case_is_dispatch iops = end (* }}} *) let tclIPAT_EQ eqtac ip = - Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); + Ssrprinters.debug_ssr (fun () -> Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); IpatMachine.(main ~eqtac ~first_case_is_dispatch:true (tclCompileIPats ip)) let tclIPATssr ip = - Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); + Ssrprinters.debug_ssr (fun () -> Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); IpatMachine.(main ~first_case_is_dispatch:true (tclCompileIPats ip)) let tclCompileIPats = IpatMachine.tclCompileIPats diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 6ed68094dc..434568b554 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -15,7 +15,6 @@ open Names open Printer open Tacmach -open Ssrmatching_plugin open Ssrast let pr_spc () = str " " @@ -121,15 +120,4 @@ and pr_block = function (Prefix id) -> str"^" ++ Id.print id | (SuffixId id) -> str"^~" ++ Id.print id | (SuffixNum n) -> str"^~" ++ int n -(* 0 cost pp function. Active only if Debug Ssreflect is Set *) -let ppdebug_ref = ref (fun _ -> ()) -let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s) -let () = - Goptions.(declare_bool_option - { optkey = ["Debug";"Ssreflect"]; - optdepr = false; - optread = (fun _ -> !ppdebug_ref == ssr_pp); - optwrite = (fun b -> - Ssrmatching.debug b; - if b then ppdebug_ref := ssr_pp else ppdebug_ref := fun _ -> ()) }) -let ppdebug s = !ppdebug_ref s +let debug_ssr = CDebug.create ~name:"ssreflect" () diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 21fb28038a..994577a0c9 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -51,5 +51,4 @@ val pr_guarded : val pr_occ : ssrocc -> Pp.t -val ppdebug : Pp.t Lazy.t -> unit - +val debug_ssr : CDebug.t diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 97926753f5..b3a9e71a3f 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -194,17 +194,17 @@ let mkGApp f args = let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal -> let env = Goal.env goal in let sigma = Goal.sigma goal in - Ssrprinters.ppdebug (lazy + Ssrprinters.debug_ssr (fun () -> Pp.(str"interp-in: " ++ Printer.pr_glob_constr_env env sigma glob)); try let sigma,term = Tacinterp.interp_open_constr ist env sigma (glob,None) in - Ssrprinters.ppdebug (lazy + Ssrprinters.debug_ssr (fun () -> Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term)); tclUNIT (env,sigma,term) with e -> (* XXX this is another catch all! *) let e, info = Exninfo.capture e in - Ssrprinters.ppdebug (lazy + Ssrprinters.debug_ssr (fun () -> Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env sigma glob)); tclZERO ~info e end @@ -217,7 +217,7 @@ end let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t let tclADD_CLEAR_IF_ID (env, ist, t) x = - Ssrprinters.ppdebug (lazy + Ssrprinters.debug_ssr (fun () -> Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t)); let hd, args = EConstr.decompose_app ist t in match EConstr.kind ist hd with @@ -269,11 +269,11 @@ let interp_view ~clear_if_id ist v p = let p_id = DAst.make p_id in match DAst.get v with | Glob_term.GApp (hd, rargs) when is_specialize hd -> - Ssrprinters.ppdebug (lazy Pp.(str "specialize")); + Ssrprinters.debug_ssr (fun () -> Pp.(str "specialize")); interp_glob ist (mkGApp p_id rargs) >>= tclKeepOpenConstr >>= tclPAIR [] | _ -> - Ssrprinters.ppdebug (lazy Pp.(str "view")); + Ssrprinters.debug_ssr (fun () -> Pp.(str "view")); (* We find out how to build (v p) eventually using an adaptor *) let adaptors = AdaptorDb.(get Forward) in Proofview.tclORELSE @@ -324,7 +324,7 @@ Goal.enter_one ~__LOC__ begin fun g -> let rigid = rigid_of und0 in let n, p, to_prune, _ucst = pf_abs_evars2 s0 rigid (sigma, p) in let p = if simple_types then pf_abs_cterm s0 n p else p in - Ssrprinters.ppdebug (lazy Pp.(str"view@finalized: " ++ + Ssrprinters.debug_ssr (fun () -> Pp.(str"view@finalized: " ++ Printer.pr_econstr_env env sigma p)); let sigma = List.fold_left Evd.remove sigma to_prune in Unsafe.tclEVARS sigma <*> @@ -349,26 +349,26 @@ let rec apply_all_views_aux ~clear_if_id vs finalization conclusion s0 = pose_proof name p <*> conclusion ~to_clear:name) <*> tclUNIT false) | v :: vs -> - Ssrprinters.ppdebug (lazy Pp.(str"piling...")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"piling...")); is_tac_in_term ~extra_scope:"ssripat" v >>= function | `Term v -> - Ssrprinters.ppdebug (lazy Pp.(str"..a term")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"..a term")); pile_up_view ~clear_if_id v <*> apply_all_views_aux ~clear_if_id vs finalization conclusion s0 | `Tac tac -> - Ssrprinters.ppdebug (lazy Pp.(str"..a tactic")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"..a tactic")); finalization s0 (fun name p -> (match p with | None -> tclUNIT () | Some p -> pose_proof name p) <*> Tacinterp.eval_tactic tac <*> if vs = [] then begin - Ssrprinters.ppdebug (lazy Pp.(str"..was the last view")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"..was the last view")); conclusion ~to_clear:name <*> tclUNIT true end else Tactics.clear name <*> tclINDEPENDENTL begin - Ssrprinters.ppdebug (lazy Pp.(str"..was NOT the last view")); + Ssrprinters.debug_ssr (fun () -> Pp.(str"..was NOT the last view")); Ssrcommon.tacSIGMA >>= apply_all_views_aux ~clear_if_id vs finalization conclusion end >>= reduce_or) diff --git a/plugins/syntax/dune b/plugins/syntax/dune index f930fc265a..ba53a439a0 100644 --- a/plugins/syntax/dune +++ b/plugins/syntax/dune @@ -6,13 +6,6 @@ (libraries coq.vernac)) (library - (name int63_syntax_plugin) - (public_name coq.plugins.int63_syntax) - (synopsis "Coq syntax plugin: int63") - (modules int63_syntax) - (libraries coq.vernac)) - -(library (name float_syntax_plugin) (public_name coq.plugins.float_syntax) (synopsis "Coq syntax plugin: float") diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml deleted file mode 100644 index 110b26581f..0000000000 --- a/plugins/syntax/int63_syntax.ml +++ /dev/null @@ -1,58 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "int63_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -(* digit-based syntax for int63 *) - -open Names -open Libnames - -(*** Constants for locating int63 constructors ***) - -let q_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.int" -let q_id_int63 = qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.id_int" - -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) - -(* int63 stuff *) -let int63_module = ["Coq"; "Numbers"; "Cyclic"; "Int63"; "PrimInt63"] -let int63_path = make_path int63_module "int" -let int63_scope = "int63_scope" - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -(* Actually declares the interpreter for int63 *) - -let _ = - let open Notation in - at_declare_ml_module - (fun () -> - let id_int63 = Nametab.locate q_id_int63 in - let o = { to_kind = Int63, Direct; - to_ty = id_int63; - to_post = [||]; - of_kind = Int63, Direct; - of_ty = id_int63; - ty_name = q_int63; - warning = Nop } in - enable_prim_token_interpretation - { pt_local = false; - pt_scope = int63_scope; - pt_interp_info = NumberNotation o; - pt_required = (int63_path, int63_module); - pt_refs = []; - pt_in_match = false }) - () diff --git a/plugins/syntax/number.ml b/plugins/syntax/number.ml index 0e7640f430..80c11dc0d4 100644 --- a/plugins/syntax/number.ml +++ b/plugins/syntax/number.ml @@ -106,10 +106,12 @@ let locate_number () = let locate_int63 () = let int63n = "num.int63.type" in - if Coqlib.has_ref int63n + let pos_neg_int63n = "num.int63.pos_neg_int63" in + if Coqlib.has_ref int63n && Coqlib.has_ref pos_neg_int63n then - let q_int63 = qualid_of_ref int63n in - Some (mkRefC q_int63) + let q_pos_neg_int63 = qualid_of_ref pos_neg_int63n in + Some ({pos_neg_int63_ty = unsafe_locate_ind q_pos_neg_int63}, + mkRefC q_pos_neg_int63) else None let has_type env sigma f ty = @@ -121,13 +123,13 @@ let type_error_to f ty = CErrors.user_err (pr_qualid f ++ str " should go from Number.int to " ++ pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ - fnl () ++ str "Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first).") + fnl () ++ str "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first).") let type_error_of g ty = CErrors.user_err (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ str " to Number.int or (option Number.int)." ++ fnl () ++ - str "Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first).") + str "Instead of Number.int, the types Number.uint or Z or PrimInt63.pos_neg_int63 or Number.number could be used (you may need to require BinNums or Number or PrimInt63 first).") let warn_deprecated_decimal = CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated" @@ -381,22 +383,37 @@ let elaborate_to_post_via env sigma ty_name ty_ind l = let pt_refs = List.map (fun (_, cnst, _) -> cnst) (to_post.(0)) in to_post, pt_refs -let locate_global_inductive allow_params qid = - let locate_param_inductive qid = +type target_type = + | TargetInd of (inductive * GlobRef.t option list) + | TargetPrim of required_module + +let locate_global_inductive_with_params allow_params qid = + if not allow_params then raise Not_found else match Nametab.locate_extended qid with | Globnames.TrueGlobal _ -> raise Not_found | Globnames.SynDef kn -> match Syntax_def.search_syntactic_definition kn with - | [], Notation_term.(NApp (NRef (GlobRef.IndRef i,None), l)) when allow_params -> + | [], Notation_term.(NApp (NRef (GlobRef.IndRef i,None), l)) -> i, List.map (function | Notation_term.NRef (r,None) -> Some r | Notation_term.NHole _ -> None | _ -> raise Not_found) l - | _ -> raise Not_found in - try locate_param_inductive qid + | _ -> raise Not_found + +let locate_global_inductive allow_params qid = + try locate_global_inductive_with_params allow_params qid with Not_found -> Smartlocate.global_inductive_with_alias qid, [] +let locate_global_inductive_or_int63 allow_params qid = + try TargetInd (locate_global_inductive_with_params allow_params qid) + with Not_found -> + let int63n = "num.int63.type" in + if allow_params && Coqlib.has_ref int63n + && GlobRef.equal (Smartlocate.global_with_alias qid) (Coqlib.lib_ref int63n) + then TargetPrim (Nametab.path_of_global (Coqlib.lib_ref int63n), []) + else TargetInd (Smartlocate.global_inductive_with_alias qid, []) + let vernac_number_notation local ty f g opts scope = let rec parse_opts = function | [] -> None, Nop @@ -421,7 +438,7 @@ let vernac_number_notation local ty f g opts scope = let ty_name = ty in let ty, via = match via with None -> ty, via | Some (ty', a) -> ty', Some (ty, a) in - let tyc, params = locate_global_inductive (via = None) ty in + let tyc_params = locate_global_inductive_or_int63 (via = None) 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 @@ -451,11 +468,14 @@ let vernac_number_notation local ty f g opts scope = | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ (opt cty)) -> Z z_pos_ty, Option | _ -> match int63_ty with - | Some cint63 when has_type env sigma f (arrow cint63 cty) -> Int63, Direct - | Some cint63 when has_type env sigma f (arrow cint63 (opt cty)) -> Int63, Option + | Some (pos_neg_int63_ty, cint63) when has_type env sigma f (arrow cint63 cty) -> Int63 pos_neg_int63_ty, Direct + | Some (pos_neg_int63_ty, cint63) when has_type env sigma f (arrow cint63 (opt cty)) -> Int63 pos_neg_int63_ty, Option | _ -> type_error_to f ty in (* Check the type of g *) + let cty = match tyc_params with + | TargetPrim _ -> mkRefC (qualid_of_string "Coq.Numbers.Cyclic.Int63.PrimInt63.int_wrapper") + | TargetInd _ -> cty in let of_kind = match num_ty with | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct @@ -476,8 +496,8 @@ let vernac_number_notation local ty f g opts scope = | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty (opt cZ)) -> Z z_pos_ty, Option | _ -> match int63_ty with - | Some cint63 when has_type env sigma g (arrow cty cint63) -> Int63, Direct - | Some cint63 when has_type env sigma g (arrow cty (opt cint63)) -> Int63, Option + | Some (pos_neg_int63_ty, cint63) when has_type env sigma g (arrow cty cint63) -> Int63 pos_neg_int63_ty, Direct + | Some (pos_neg_int63_ty, cint63) when has_type env sigma g (arrow cty (opt cint63)) -> Int63 pos_neg_int63_ty, Option | _ -> type_error_of g ty in (match to_kind, of_kind with @@ -485,9 +505,14 @@ let vernac_number_notation local ty f g opts scope = | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) -> warn_deprecated_decimal () | _ -> ()); - let to_post, pt_refs = match via with - | None -> elaborate_to_post_params env sigma tyc params - | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in + let to_post, pt_required, pt_refs = match tyc_params with + | TargetPrim path -> [||], path, [Coqlib.lib_ref "num.int63.wrap_int"] + | TargetInd (tyc, params) -> + let to_post, pt_refs = + match via with + | None -> elaborate_to_post_params env sigma tyc params + | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in + to_post, (Nametab.path_of_global (GlobRef.IndRef tyc), []), pt_refs in let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name; warning = opts } in @@ -498,7 +523,7 @@ let vernac_number_notation local ty f g opts scope = { pt_local = local; pt_scope = scope; pt_interp_info = NumberNotation o; - pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; + pt_required; pt_refs; pt_in_match = true } in diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 7930c3d634..02fb347d08 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -201,10 +201,7 @@ let cofixp_reducible flgs _ stk = else false -let get_debug_cbv = Goptions.declare_bool_option_and_ref - ~depr:false - ~value:false - ~key:["Debug";"Cbv"] +let debug_cbv = CDebug.create ~name:"Cbv" () (* Reduction of primitives *) @@ -525,7 +522,7 @@ and norm_head_ref k info env stack normt t = if red_set_ref info.reds normt then match cbv_value_cache info normt with | Declarations.Def body -> - if get_debug_cbv () then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); + debug_cbv (fun () -> Pp.(str "Unfolding " ++ debug_pr_key normt)); strip_appl (shift_value k body) stack | Declarations.Primitive op -> let c = match normt with @@ -534,11 +531,11 @@ and norm_head_ref k info env stack normt t = in (PRIMITIVE(op,c,[||]),stack) | Declarations.OpaqueDef _ | Declarations.Undef _ -> - if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); + debug_cbv (fun () -> Pp.(str "Not unfolding " ++ debug_pr_key normt)); (VAL(0,make_constr_ref k normt t),stack) else begin - if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); + debug_cbv (fun () -> Pp.(str "Not unfolding " ++ debug_pr_key normt)); (VAL(0,make_constr_ref k normt t),stack) end diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 990e84e5a7..e1d6fff3e4 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -47,17 +47,9 @@ let default_flags env = let ts = default_transparent_state env in default_flags_of ts -let debug_unification = - Goptions.declare_bool_option_and_ref - ~depr:false - ~key:["Debug";"Unification"] - ~value:false - -let debug_ho_unification = - Goptions.declare_bool_option_and_ref - ~depr:false - ~key:["Debug";"HO";"Unification"] - ~value:false +let debug_unification = CDebug.create ~name:"unification" () + +let debug_ho_unification = CDebug.create ~name:"ho-unification" () (*******************************************) (* Functions to deal with impossible cases *) @@ -808,9 +800,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) - let () = if debug_unification () then - let open Pp in - Feedback.msg_debug (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in + let () = debug_unification (fun () -> Pp.(v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ()))) in match (flex_kind_of_term flags env evd term1 sk1, flex_kind_of_term flags env evd term2 sk2) with | Flexible (sp1,al1), Flexible (sp2,al2) -> @@ -1288,17 +1278,17 @@ let apply_on_subterm env evd fixed f test c t = (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t else - (if debug_ho_unification () then - Feedback.msg_debug Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t); + (debug_ho_unification (fun () -> + Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t)); let b, evd = try test env !evdref k c t with e when CErrors.noncritical e -> assert false in - if b then (if debug_ho_unification () then Feedback.msg_debug (Pp.str "succeeded"); + if b then (debug_ho_unification (fun () -> Pp.str "succeeded"); let evd', fixed, t' = f !evdref !fixedref k t in fixedref := fixed; evdref := evd'; t') else ( - if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed"); + debug_ho_unification (fun () -> Pp.str "failed"); map_constr_with_binders_left_to_right env !evdref (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t)) @@ -1404,9 +1394,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let env_evar = evar_filtered_env env_rhs evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in - if debug_ho_unification () then - (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs); - Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar)); + debug_ho_unification (fun () -> + Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs ++ fnl () ++ + str"env evars: " ++ Termops.Internal.print_env env_evar)); let args = List.map (nf_evar evd) args in let argsubst = List.map2 (fun decl c -> (NamedDecl.get_id decl, c)) ctxt args in let instance = evar_identity_subst evi in @@ -1439,17 +1429,17 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let rec set_holes env_rhs evd fixed rhs = function | (id,idty,c,cty,evsref,filter,occs)::subst -> let c = nf_evar evd c in - if debug_ho_unification () then - Feedback.msg_debug Pp.(str"set holes for: " ++ + debug_ho_unification (fun () -> + Pp.(str"set holes for: " ++ prc env_rhs evd (mkVar id.binder_name) ++ spc () ++ prc env_rhs evd c ++ str" in " ++ - prc env_rhs evd rhs); + prc env_rhs evd rhs)); let occ = ref 1 in let set_var evd fixed k inst = let oc = !occ in - if debug_ho_unification () then - (Feedback.msg_debug Pp.(str"Found one occurrence"); - Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs evd c)); + debug_ho_unification (fun () -> + Pp.(str"Found one occurrence" ++ fnl () ++ + str"cty: " ++ prc env_rhs evd c)); incr occ; match occs with | AtOccurrences occs -> @@ -1458,10 +1448,10 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = | Unspecified prefer_abstraction -> let evd, fixed, evty = set_holes env_rhs evd fixed cty subst in let evty = nf_evar evd evty in - if debug_ho_unification () then - Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++ - str" of type: " ++ prc env_evar evd evty ++ - str " for " ++ prc env_rhs evd c); + debug_ho_unification (fun () -> + Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++ + str" of type: " ++ prc env_evar evd evty ++ + str " for " ++ prc env_rhs evd c)); let instance = Filter.filter_list filter instance in (* Allow any type lower than the variable's type as the abstracted subterm might have a smaller type, which could be @@ -1477,8 +1467,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = evd, fixed, mkEvar (evk, instance) in let evd, fixed, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in - if debug_ho_unification () then - Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs evd rhs'); + debug_ho_unification (fun () -> + Pp.(str"abstracted: " ++ prc env_rhs evd rhs')); let () = check_selected_occs env_rhs evd c !occ occs in let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in set_holes env_rhs' evd fixed rhs' subst @@ -1491,9 +1481,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = (* Thin evars making the term typable in env_evar *) let evd, rhs' = thin_evars env_evar evd ctxt rhs' in (* We instantiate the evars of which the value is forced by typing *) - if debug_ho_unification () then - (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs'); - Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); + debug_ho_unification (fun () -> + Pp.(str"solve_evars on: " ++ prc env_evar evd rhs' ++ fnl () ++ + str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); let evd,rhs' = try !solve_evars env_evar evd rhs' with e when Pretype_errors.precatchable_exception e -> @@ -1501,18 +1491,18 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = raise (TypingFailed evd) in let rhs' = nf_evar evd rhs' in (* We instantiate the evars of which the value is forced by typing *) - if debug_ho_unification () then - (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs'); - Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); + debug_ho_unification (fun () -> + Pp.(str"after solve_evars: " ++ prc env_evar evd rhs' ++ fnl () ++ + str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); let rec abstract_free_holes evd = function | (id,idty,c,cty,evsref,_,_)::l -> let id = id.binder_name in let c = nf_evar evd c in - if debug_ho_unification () then - Feedback.msg_debug Pp.(str"abstracting: " ++ - prc env_rhs evd (mkVar id) ++ spc () ++ - prc env_rhs evd c); + debug_ho_unification (fun () -> + Pp.(str"abstracting: " ++ + prc env_rhs evd (mkVar id) ++ spc () ++ + prc env_rhs evd c)); let rec force_instantiation evd = function | (evk,evty,inst,abstract)::evs -> let evk = Option.default evk (Evarutil.advance evd evk) in @@ -1541,14 +1531,14 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = with IllTypedInstance _ (* from instantiate_evar *) | TypingFailed _ -> user_err (Pp.str "Cannot find an instance.") else - ((if debug_ho_unification () then + ((debug_ho_unification (fun () -> let evi = Evd.find evd evk in let env = Evd.evar_env env_rhs evi in - Feedback.msg_debug Pp.(str"evar is defined: " ++ + Pp.(str"evar is defined: " ++ int (Evar.repr evk) ++ spc () ++ prc env evd (match evar_body evi with Evar_defined c -> c | Evar_empty -> assert false))); - evd) + evd)) in force_instantiation evd evs | [] -> abstract_free_holes evd l in force_instantiation evd !evsref @@ -1556,27 +1546,27 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = if Evd.is_defined evd evk then (* Can happen due to dependencies: instantiating evars in the arguments of evk might instantiate evk itself. *) - (if debug_ho_unification () then + (debug_ho_unification (fun () -> begin let evi = Evd.find evd evk in let evenv = evar_env env_rhs evi in let body = match evar_body evi with Evar_empty -> assert false | Evar_defined c -> c in - Feedback.msg_debug Pp.(str"evar was defined already as: " ++ prc evenv evd body) - end; + Pp.(str"evar was defined already as: " ++ prc evenv evd body) + end); evd) else try let evi = Evd.find_undefined evd evk in let evenv = evar_env env_rhs evi in let rhs' = nf_evar evd rhs' in - if debug_ho_unification () then - Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++ - prc evenv evd rhs'); + debug_ho_unification (fun () -> + Pp.(str"abstracted type before second solve_evars: " ++ + prc evenv evd rhs')); (* solve_evars is not commuting with nf_evar, because restricting an evar might provide a more specific type. *) let evd, _ = !solve_evars evenv evd rhs' in - if debug_ho_unification () then - Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs')); + debug_ho_unification (fun () -> + Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs'))); let flags = default_flags_of TransparentState.full in Evarsolve.instantiate_evar evar_unify flags env_rhs evd evk rhs' with IllTypedInstance _ -> raise (TypingFailed evd) @@ -1629,11 +1619,10 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in - let () = if debug_unification () then - let open Pp in - Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++ + let () = debug_unification (fun () -> + Pp.(v 0 (str "Heuristic:" ++ spc () ++ Termops.Internal.print_constr_env env evd t1 ++ cut () ++ - Termops.Internal.print_constr_env env evd t2 ++ cut ())) in + Termops.Internal.print_constr_env env evd t2 ++ cut ()))) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in match EConstr.kind evd term1, EConstr.kind evd term2 with | Evar (evk1,args1), (Rel _|Var _) when app_empty diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index d02b015604..2e678f5700 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -347,37 +347,50 @@ let make_case_invert env (IndType (((ind,u),params),indices)) ci = then CaseInvert {indices=Array.of_list indices} else NoInvert +let make_project env sigma ind pred c branches ps = + let open EConstr in + assert(Array.length branches == 1); + let na, ty, t = destLambda sigma pred in + let () = + let mib, _ = Inductive.lookup_mind_specif env ind in + if (* dependent *) not (Vars.noccurn sigma 1 t) && + not (has_dependent_elim mib) then + user_err ~hdr:"make_case_or_project" + Pp.(str"Dependent case analysis not allowed" ++ + str" on inductive type " ++ Termops.Internal.print_constr_env env sigma (mkInd ind)) + in + let branch = branches.(0) in + let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in + let n, len, ctx = + List.fold_right + (fun decl (i, j, ctx) -> + match decl with + | LocalAssum (na, ty) -> + let t = mkProj (Projection.make ps.(i) true, mkRel j) in + (i + 1, j + 1, LocalDef (na, t, Vars.liftn 1 j ty) :: ctx) + | LocalDef (na, b, ty) -> + (i, j + 1, LocalDef (na, Vars.liftn 1 j b, Vars.liftn 1 j ty) :: ctx)) + ctx (0, 1, []) + in + mkLetIn (na, c, ty, it_mkLambda_or_LetIn (Vars.liftn 1 (Array.length ps + 1) br) ctx) + +let simple_make_case_or_project env sigma ci pred invert c branches = + let open EConstr in + let ind = ci.ci_ind in + let projs = get_projections env ind in + match projs with + | None -> mkCase (EConstr.contract_case env sigma (ci, pred, invert, c, branches)) + | Some ps -> make_project env sigma ind pred c branches ps + let make_case_or_project env sigma indt ci pred c branches = let open EConstr in let IndType (((ind,_),_),_) = indt in let projs = get_projections env ind in match projs with - | None -> (mkCase (EConstr.contract_case env sigma (ci, pred, make_case_invert env indt ci, c, branches))) - | Some ps -> - assert(Array.length branches == 1); - let na, ty, t = destLambda sigma pred in - let () = - let mib, _ = Inductive.lookup_mind_specif env ind in - if (* dependent *) not (Vars.noccurn sigma 1 t) && - not (has_dependent_elim mib) then - user_err ~hdr:"make_case_or_project" - Pp.(str"Dependent case analysis not allowed" ++ - str" on inductive type " ++ Termops.Internal.print_constr_env env sigma (mkInd ind)) - in - let branch = branches.(0) in - let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in - let n, len, ctx = - List.fold_right - (fun decl (i, j, ctx) -> - match decl with - | LocalAssum (na, ty) -> - let t = mkProj (Projection.make ps.(i) true, mkRel j) in - (i + 1, j + 1, LocalDef (na, t, Vars.liftn 1 j ty) :: ctx) - | LocalDef (na, b, ty) -> - (i, j + 1, LocalDef (na, Vars.liftn 1 j b, Vars.liftn 1 j ty) :: ctx)) - ctx (0, 1, []) - in - mkLetIn (na, c, ty, it_mkLambda_or_LetIn (Vars.liftn 1 (Array.length ps + 1) br) ctx) + | None -> + let invert = make_case_invert env indt ci in + mkCase (EConstr.contract_case env sigma (ci, pred, invert, c, branches)) + | Some ps -> make_project env sigma ind pred c branches ps (* substitution in a signature *) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 8e83814fa0..59ef8e08e3 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -212,6 +212,12 @@ val make_case_or_project : env -> evar_map -> inductive_type -> case_info -> (* pred *) EConstr.constr -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr +(** Sometimes [make_case_or_project] is nicer to call with a pre-built + [case_invert] than [inductive_type]. *) +val simple_make_case_or_project : + env -> evar_map -> case_info -> + (* pred *) EConstr.constr -> EConstr.case_invert -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr + val make_case_invert : env -> inductive_type -> case_info -> EConstr.case_invert diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 92e412a537..2c107502f4 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -469,15 +469,15 @@ let start_profiler_linux profile_fn = Unix.stdin dev_null dev_null in (* doesn't seem to be a way to test whether process creation succeeded *) - if !Flags.debug then - Feedback.msg_debug (Pp.str (Format.sprintf "Native compute profiler started, pid = %d, output to: %s" profiler_pid profile_fn)); + debug_native_compiler (fun () -> + Pp.str (Format.sprintf "Native compute profiler started, pid = %d, output to: %s" profiler_pid profile_fn)); Some profiler_pid (* kill profiler via SIGINT *) let stop_profiler_linux m_pid = match m_pid with | Some pid -> ( - let _ = if !Flags.debug then Feedback.msg_debug (Pp.str "Stopping native code profiler") in + let _ = debug_native_compiler (fun () -> Pp.str "Stopping native code profiler") in try Unix.kill pid Sys.sigint; let _ = Unix.waitpid [] pid in () @@ -502,15 +502,9 @@ let stop_profiler m_pid = | _ -> () let native_norm env sigma c ty = + Nativelib.link_libraries (); let c = EConstr.Unsafe.to_constr c in let ty = EConstr.Unsafe.to_constr ty in - if not (Flags.get_native_compiler ()) then - user_err Pp.(str "Native_compute reduction has been disabled.") - else - (* - Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1); - Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2); - *) let profile = get_profiling_enabled () in let print_timing = get_timing_enabled () in let ml_filename, prefix = Nativelib.get_ml_filename () in @@ -526,17 +520,22 @@ let native_norm env sigma c ty = if print_timing then Feedback.msg_info (Pp.str time_info); let profiler_pid = if profile then start_profiler () else None in let t0 = Unix.gettimeofday () in - Nativelib.call_linker ~fatal:true ~prefix fn (Some upd); + let (rt1, _) = Nativelib.execute_library ~prefix fn upd in let t1 = Unix.gettimeofday () in if profile then stop_profiler profiler_pid; let time_info = Format.sprintf "native_compute: Evaluation done in %.5f" (t1 -. t0) in if print_timing then Feedback.msg_info (Pp.str time_info); - let res = nf_val env sigma !Nativelib.rt1 ty in + let res = nf_val env sigma rt1 ty in let t2 = Unix.gettimeofday () in let time_info = Format.sprintf "native_compute: Reification done in %.5f" (t2 -. t1) in if print_timing then Feedback.msg_info (Pp.str time_info); EConstr.of_constr res +let native_norm env sigma c ty = + if not (Flags.get_native_compiler ()) then + user_err Pp.(str "Native_compute reduction has been disabled."); + native_norm env sigma c ty + let native_conv_generic pb sigma t = Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 54a47a252d..4083d3bc23 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -686,11 +686,7 @@ module CredNative = RedNative(CNativeEntries) contract_* in any case . *) -let debug_RAKAM = - Goptions.declare_bool_option_and_ref - ~depr:false - ~key:["Debug";"RAKAM"] - ~value:false +let debug_RAKAM = CDebug.create ~name:"RAKAM" () let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) = let args = Stack.tail ci.ci_npar args in @@ -709,18 +705,18 @@ let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) = let rec whd_state_gen flags env sigma = let open Context.Named.Declaration in let rec whrec (x, stack) : state = - let () = if debug_RAKAM () then + let () = let open Pp in let pr c = Termops.Internal.print_constr_env env sigma c in - Feedback.msg_debug + debug_RAKAM (fun () -> (h (str "<<" ++ pr x ++ str "|" ++ cut () ++ Stack.pr pr stack ++ - str ">>")) + str ">>"))) in let c0 = EConstr.kind sigma x in let fold () = - let () = if debug_RAKAM () then - let open Pp in Feedback.msg_debug (str "<><><><><>") in + let () = debug_RAKAM (fun () -> + let open Pp in str "<><><><><>") in ((EConstr.of_kind c0, stack)) in match c0 with diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 41d16f1c3c..09bcc860d0 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -19,7 +19,7 @@ open Environ exception Elimconst -val debug_RAKAM : unit -> bool +val debug_RAKAM : CDebug.t module CredNative : Primred.RedNative with type elem = EConstr.t and type args = EConstr.t array and type evd = Evd.evar_map diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 83e46e3295..df0f49a033 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -49,11 +49,7 @@ let is_keyed_unification = ~key:["Keyed";"Unification"] ~value:false -let debug_unification = - Goptions.declare_bool_option_and_ref - ~depr:false - ~key:["Debug";"Tactic";"Unification"] - ~value:false +let debug_tactic_unification = CDebug.create ~name:"tactic-unification" () (** Making this unification algorithm correct w.r.t. the evar-map abstraction breaks too much stuff. So we redefine incorrect functions here. *) @@ -713,8 +709,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e let cM = Evarutil.whd_head_evar sigma curm and cN = Evarutil.whd_head_evar sigma curn in let () = - if debug_unification () then - Feedback.msg_debug ( + debug_tactic_unification (fun () -> Termops.Internal.print_constr_env curenv sigma cM ++ str" ~= " ++ Termops.Internal.print_constr_env curenv sigma cN) in @@ -1138,7 +1133,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e else error_cannot_unify (fst curenvnb) sigma (cM,cN) in - if debug_unification () then Feedback.msg_debug (str "Starting unification"); + debug_tactic_unification (fun () -> str "Starting unification"); let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in try let res = @@ -1165,11 +1160,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e let a = match res with | Some sigma -> sigma, ms, es | None -> unirec_rec (env,0) cv_pb opt subst (fst m) (fst n) in - if debug_unification () then Feedback.msg_debug (str "Leaving unification with success"); + debug_tactic_unification (fun () -> str "Leaving unification with success"); a with e -> let e = Exninfo.capture e in - if debug_unification () then Feedback.msg_debug (str "Leaving unification with failure"); + debug_tactic_unification (fun () -> str "Leaving unification with failure"); Exninfo.iraise e let unify_0 env sigma pb flags c1 c2 = diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 4c4c26f47e..dd80ff21aa 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -13,7 +13,7 @@ open Pp open Util let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp -let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else () +let stm_prerr_endline s = if CDebug.(get_flag misc) then begin stm_pr_err (str s) end else () type cancel_switch = bool ref let async_proofs_flags_for_workers = ref [] diff --git a/stm/spawned.ml b/stm/spawned.ml index 5cc8be78f5..ee9c8e9942 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -11,7 +11,7 @@ open Spawn let pr_err s = Printf.eprintf "(Spawned,%d) %s\n%!" (Unix.getpid ()) s -let prerr_endline s = if !Flags.debug then begin pr_err s end else () +let prerr_endline s = if CDebug.(get_flag misc) then begin pr_err s end else () type chandescr = AnonPipe | Socket of string * int * int diff --git a/stm/stm.ml b/stm/stm.ml index 7de109e596..5ed6adbd63 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -9,7 +9,7 @@ (************************************************************************) (* enable in case of stm problems *) -(* let stm_debug () = !Flags.debug *) +(* let stm_debug () = CDebug.(get_flag misc) *) let stm_debug = ref false let stm_pr_err s = Format.eprintf "%s] %s\n%!" (Spawned.process_id ()) s @@ -18,7 +18,7 @@ let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.p let stm_prerr_endline s = if !stm_debug then begin stm_pr_err (s ()) end else () let stm_pperr_endline s = if !stm_debug then begin stm_pp_err (s ()) end else () -let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () +let stm_prerr_debug s = if CDebug.(get_flag misc) then begin stm_pr_err (s ()) end else () open Pp open CErrors @@ -785,7 +785,7 @@ end = struct (* {{{ *) end let print ?(now=false) () = - if !Flags.debug then NB.command ~now (print_dag !vcs) + if CDebug.(get_flag misc) then NB.command ~now (print_dag !vcs) let backup () = !vcs let restore v = vcs := v @@ -1533,7 +1533,7 @@ end = struct (* {{{ *) when is_tac expr && Vernacstate.Stm.same_env o n -> (* A pure tactic *) Some (id, `ProofOnly (prev, Vernacstate.Stm.pstate n)) | Some _, Some s -> - if !Flags.debug then msg_debug (Pp.str "STM: sending back a fat state"); + if CDebug.(get_flag misc) then msg_debug (Pp.str "STM: sending back a fat state"); Some (id, `Full s) | _, Some s -> Some (id, `Full s) in let rec aux seen = function diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index 56d88e6bd6..8be73ca028 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -22,14 +22,6 @@ let error_missing_arg s = exit 1 (******************************************************************************) -(* Imperative effects! This must be fixed at some point. *) -(******************************************************************************) - -let set_debug () = - let () = Exninfo.record_backtrace true in - Flags.debug := true - -(******************************************************************************) type native_compiler = Coq_config.native_compiler = NativeOff | NativeOn of { ondemand : bool } @@ -168,6 +160,9 @@ let add_load_vernacular opts verb s = let add_set_option opts opt_name value = { opts with pre = { opts.pre with injections = OptionInjection (opt_name, value) :: opts.pre.injections }} +let add_set_debug opts flags = + add_set_option opts ["Debug"] (OptionAppend flags) + (** Options for proof general *) let set_emacs opts = let opts = add_set_option opts Printer.print_goal_tag_opt_name (OptionSet None) in @@ -382,10 +377,15 @@ let parse_args ~usage ~init arglist : t * string list = (* Options with zero arg *) |"-test-mode" -> Vernacinterp.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval - |"-bt" -> Exninfo.record_backtrace true; oval + |"-bt" -> add_set_debug oval "backtrace" |"-config"|"--config" -> set_query oval PrintConfig - |"-debug" -> set_debug (); oval - |"-xml-debug" -> Flags.xml_debug := true; set_debug (); oval + + |"-debug" -> add_set_debug oval "all" + |"-d" | "-D" -> add_set_debug oval (next()) + + (* -xml-debug implies -debug. TODO don't be imperative here. *) + |"-xml-debug" -> Flags.xml_debug := true; add_set_debug oval "all" + |"-diffs" -> add_set_option oval Proof_diffs.opt_name @@ OptionSet (Some (next ())) |"-emacs" -> set_emacs oval diff --git a/sysinit/usage.ml b/sysinit/usage.ml index 763cd54137..d00b916f23 100644 --- a/sysinit/usage.ml +++ b/sysinit/usage.ml @@ -9,9 +9,8 @@ (************************************************************************) let version () = - Printf.printf "The Coq Proof Assistant, version %s (%s)\n" - Coq_config.version Coq_config.date; - Printf.printf "compiled on %s with OCaml %s\n" Coq_config.compile_date Coq_config.caml_version + Printf.printf "The Coq Proof Assistant, version %s\n" Coq_config.version; + Printf.printf "compiled with OCaml %s\n" Coq_config.caml_version let machine_readable_version () = Printf.printf "%s %s\n" diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 6fb6cff04f..167f7d4026 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -562,19 +562,18 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let open Context.Named.Declaration in let open ReductionBehaviour in let rec whrec cst_l (x, stack) = - let () = if debug_RAKAM () then + let () = debug_RAKAM (fun () -> let open Pp in let pr c = Termops.Internal.print_constr_env env sigma c in - Feedback.msg_debug (h (str "<<" ++ pr x ++ str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++ str "|" ++ cut () ++ Stack.pr pr stack ++ - str ">>")) + str ">>"))) in let c0 = EConstr.kind sigma x in let fold () = - let () = if debug_RAKAM () then - let open Pp in Feedback.msg_debug (str "<><><><><>") in + let () = debug_RAKAM (fun () -> + Pp.(str "<><><><><>")) in ((EConstr.of_kind c0, stack),cst_l) in match c0 with diff --git a/test-suite/bugs/closed/PLACEHOLDER.v b/test-suite/bugs/closed/PLACEHOLDER.v deleted file mode 100644 index e69de29bb2..0000000000 --- a/test-suite/bugs/closed/PLACEHOLDER.v +++ /dev/null diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v index 9aefb10172..62d39619b0 100644 --- a/test-suite/bugs/closed/bug_4836.v +++ b/test-suite/bugs/closed/bug_4836.v @@ -1 +1 @@ -(* -*- coq-prog-args: ("bugs/closed/PLACEHOLDER.v") -*- *) +(* Placeholder file for directory / file test *) diff --git a/test-suite/output/DebugFlags.out b/test-suite/output/DebugFlags.out new file mode 100644 index 0000000000..0385413937 --- /dev/null +++ b/test-suite/output/DebugFlags.out @@ -0,0 +1,44 @@ +File "stdin", line 1, characters 0-16: +Warning: There is no debug flag "cbn". [unknown-debug-flag,option] +Debug: [RAKAM] <<forall A : Type, A -> A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<forall A : Type, A -> A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<?A -> ?A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<?A -> ?A -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> nat|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> Prop|>> +Debug: [RAKAM] <><><><><> +Debug: [RAKAM] <<nat -> Prop|>> +Debug: [RAKAM] <><><><><> +2 + 3 = 0 + : Prop diff --git a/test-suite/output/DebugFlags.v b/test-suite/output/DebugFlags.v new file mode 100644 index 0000000000..32c0f2d24b --- /dev/null +++ b/test-suite/output/DebugFlags.v @@ -0,0 +1,5 @@ +Set Debug "cbn". + +Set Debug "RAKAM". + +Check 2 + 3 = 0. diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out index 7ca4de1e46..96af456891 100644 --- a/test-suite/output/Int63Syntax.out +++ b/test-suite/output/Int63Syntax.out @@ -15,9 +15,9 @@ 427 : int The command has indeed failed with message: -Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int +Cannot interpret this number as a value of type int The command has indeed failed with message: -Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int +Cannot interpret this number as a value of type int 0 : int 0 @@ -33,9 +33,11 @@ The reference x was not found in the current environment. add 2 2 : int The command has indeed failed with message: -int63 are only non-negative numbers. +Cannot interpret this number as a value of type int The command has indeed failed with message: overflow in int63 literal: 9223372036854775808 +0x1 + : int 2 : nat 2%int63 diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v index 50910264f2..be0ee701af 100644 --- a/test-suite/output/Int63Syntax.v +++ b/test-suite/output/Int63Syntax.v @@ -20,6 +20,11 @@ Fail Check 0x. Check (PrimInt63.add 2 2). Fail Check -1. Fail Check 9223372036854775808. + +Set Printing All. +Check 1%int63. +Unset Printing All. + Open Scope nat_scope. Check 2. (* : nat *) Check 2%int63. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 3477a293e3..0b18981f4e 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -77,18 +77,18 @@ fun x : nat => [x] : nat -> nat ∀ x : nat, x = x : Prop -File "stdin", line 184, characters 0-160: +File "stdin", line 187, characters 0-160: Warning: Notation "∀ _ .. _ , _" was already defined with a different format in scope type_scope. [notation-incompatible-format,parsing] ∀x : nat,x = x : Prop -File "stdin", line 197, characters 0-60: +File "stdin", line 200, characters 0-60: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 201, characters 0-64: +File "stdin", line 204, characters 0-64: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 206, characters 0-62: +File "stdin", line 209, characters 0-62: Warning: Lonely notation "_ %%%% _" was already defined with a different format. [notation-incompatible-format,parsing] 3 %% 4 @@ -97,10 +97,10 @@ format. [notation-incompatible-format,parsing] : nat 3 %% 4 : nat -File "stdin", line 234, characters 0-61: +File "stdin", line 237, characters 0-61: Warning: The format modifier is irrelevant for only parsing rules. [irrelevant-format-only-parsing,parsing] -File "stdin", line 238, characters 0-63: +File "stdin", line 241, characters 0-63: Warning: The only parsing modifier has no effect in Reserved Notation. [irrelevant-reserved-notation-only-parsing,parsing] fun x : nat => U (S x) @@ -111,7 +111,7 @@ fun x : nat => V x : forall x : nat, nat * (?T -> ?T) where ?T : [x : nat x0 : ?T |- Type] (x0 cannot be used) -File "stdin", line 255, characters 0-30: +File "stdin", line 258, characters 0-30: Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing] 0 :=: 0 : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index ebad12af88..a5ec92fe3c 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -103,7 +103,10 @@ Module NumberNotations. Delimit Scope test17_scope with test17. Local Set Primitive Projections. Record myint63 := of_int { to_int : int }. - Number Notation myint63 of_int to_int : test17_scope. + Definition parse x := + match x with Pos x => Some (of_int x) | Neg _ => None end. + Definition print x := Pos (to_int x). + Number Notation myint63 parse print : test17_scope. Check let v := 0%test17 in v : myint63. End Test17. End NumberNotations. diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out index 60682edec8..df9b39389c 100644 --- a/test-suite/output/NumberNotations.out +++ b/test-suite/output/NumberNotations.out @@ -260,28 +260,28 @@ The command has indeed failed with message: add is not a constructor of an inductive type. The command has indeed failed with message: Missing mapping for constructor Iempty. -File "stdin", line 574, characters 56-61: +File "stdin", line 577, characters 56-61: Warning: Type of I'sum seems incompatible with the type of sum. Expected type is: (I' -> I' -> I') instead of (I -> I' -> I'). This might yield ill typed terms when using the notation. [via-type-mismatch,numbers] -File "stdin", line 579, characters 32-33: +File "stdin", line 582, characters 32-33: Warning: I was already mapped to Set, mapping it also to nat might yield ill typed terms when using the notation. [via-type-remapping,numbers] -File "stdin", line 579, characters 37-42: +File "stdin", line 582, characters 37-42: Warning: Type of Iunit seems incompatible with the type of O. Expected type is: I instead of I. This might yield ill typed terms when using the notation. [via-type-mismatch,numbers] The command has indeed failed with message: 'via' and 'abstract' cannot be used together. -File "stdin", line 659, characters 21-23: +File "stdin", line 662, characters 21-23: Warning: Type of I1 seems incompatible with the type of Fin.F1. Expected type is: (nat -> I) instead of I. This might yield ill typed terms when using the notation. [via-type-mismatch,numbers] -File "stdin", line 659, characters 35-37: +File "stdin", line 662, characters 35-37: Warning: Type of IS seems incompatible with the type of Fin.FS. Expected type is: (nat -> I -> I) instead of (I -> I). This might yield ill typed terms when using the notation. diff --git a/test-suite/output/NumberNotations.v b/test-suite/output/NumberNotations.v index 718da13500..85400c2fd4 100644 --- a/test-suite/output/NumberNotations.v +++ b/test-suite/output/NumberNotations.v @@ -328,7 +328,10 @@ Module Test17. Delimit Scope test17_scope with test17. Local Set Primitive Projections. Record myint63 := of_int { to_int : int }. - Number Notation myint63 of_int to_int : test17_scope. + Definition parse x := + match x with Pos x => Some (of_int x) | Neg _ => None end. + Definition print x := Pos (to_int x). + Number Notation myint63 parse print : test17_scope. Check let v := 0%test17 in v : myint63. End Test17. diff --git a/test-suite/output/Sint63Syntax.out b/test-suite/output/Sint63Syntax.out new file mode 100644 index 0000000000..db14658307 --- /dev/null +++ b/test-suite/output/Sint63Syntax.out @@ -0,0 +1,66 @@ +2%sint63 + : int +2 + : int +-3 + : int +4611686018427387903 + : int +-4611686018427387904 + : int +427 + : int +427 + : int +427 + : int +427 + : int +427 + : int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +0 + : int +0 + : int +The command has indeed failed with message: +The reference xg was not found in the current environment. +The command has indeed failed with message: +The reference xG was not found in the current environment. +The command has indeed failed with message: +The reference x1 was not found in the current environment. +The command has indeed failed with message: +The reference x was not found in the current environment. +2 + 2 + : int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +The command has indeed failed with message: +Cannot interpret this number as a value of type int +0x1%int63 + : int +0x7fffffffffffffff%int63 + : int +2 + : nat +2%sint63 + : int +t = 2%si63 + : int +t = 2%si63 + : int +2 + : nat +2 + : int +(2 + 2)%sint63 + : int +2 + 2 + : int + = 4 + : int + = 37151199385380486 + : int diff --git a/test-suite/output/Sint63Syntax.v b/test-suite/output/Sint63Syntax.v new file mode 100644 index 0000000000..b9ed596537 --- /dev/null +++ b/test-suite/output/Sint63Syntax.v @@ -0,0 +1,49 @@ +Require Import Sint63. + +Check 2%sint63. +Open Scope sint63_scope. +Check 2. +Check -3. +Check 4611686018427387903. +Check -4611686018427387904. +Check 0x1ab. +Check 0X1ab. +Check 0x1Ab. +Check 0x1aB. +Check 0x1AB. +Fail Check 0x1ap5. (* exponents not implemented (yet?) *) +Fail Check 0x1aP5. +Check 0x0. +Check 0x000. +Fail Check 0xg. +Fail Check 0xG. +Fail Check 00x1. +Fail Check 0x. +Check (PrimInt63.add 2 2). +Fail Check 4611686018427387904. +Fail Check -4611686018427387905. + +Set Printing All. +Check 1%sint63. +Check (-1)%sint63. +Unset Printing All. + +Open Scope nat_scope. +Check 2. (* : nat *) +Check 2%sint63. +Delimit Scope sint63_scope with si63. +Definition t := 2%sint63. +Print t. +Delimit Scope nat_scope with sint63. +Print t. +Check 2. +Close Scope nat_scope. +Check 2. +Close Scope sint63_scope. +Delimit Scope sint63_scope with sint63. + +Check (2 + 2)%sint63. +Open Scope sint63_scope. +Check (2+2). +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. diff --git a/test-suite/primitive/sint63/add.v b/test-suite/primitive/sint63/add.v new file mode 100644 index 0000000000..dcafd64181 --- /dev/null +++ b/test-suite/primitive/sint63/add.v @@ -0,0 +1,25 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 2 + 3 = 5). +Check (eq_refl 5 <: 2 + 3 = 5). +Check (eq_refl 5 <<: 2 + 3 = 5). +Definition compute1 := Eval compute in 2 + 3. +Check (eq_refl compute1 : 5 = 5). + +Check (eq_refl : 4611686018427387903 + 1 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <: + 4611686018427387903 + 1 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <<: + 4611686018427387903 + 1 = -4611686018427387904). +Definition compute2 := Eval compute in 4611686018427387903 + 1. +Check (eq_refl compute2 : -4611686018427387904 = -4611686018427387904). + +Check (eq_refl : 2 - 3 = -1). +Check (eq_refl (-1) <: 2 - 3 = -1). +Check (eq_refl (-1) <<: 2 - 3 = -1). +Definition compute3 := Eval compute in 2 - 3. +Check (eq_refl compute3 : -1 = -1). diff --git a/test-suite/primitive/sint63/asr.v b/test-suite/primitive/sint63/asr.v new file mode 100644 index 0000000000..4524ae4e6f --- /dev/null +++ b/test-suite/primitive/sint63/asr.v @@ -0,0 +1,41 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : (-2305843009213693952) >> 61 = -1). +Check (eq_refl (-1) <: (-2305843009213693952) >> 61 = -1). +Check (eq_refl (-1) <<: (-2305843009213693952) >> 61 = -1). +Definition compute1 := Eval compute in (-2305843009213693952) >> 61. +Check (eq_refl compute1 : -1 = -1). + +Check (eq_refl : 2305843009213693952 >> 62 = 0). +Check (eq_refl 0 <: 2305843009213693952 >> 62 = 0). +Check (eq_refl 0 <<: 2305843009213693952 >> 62 = 0). +Definition compute2 := Eval compute in 2305843009213693952 >> 62. +Check (eq_refl compute2 : 0 = 0). + +Check (eq_refl : 4611686018427387903 >> 63 = 0). +Check (eq_refl 0 <: 4611686018427387903 >> 63 = 0). +Check (eq_refl 0 <<: 4611686018427387903 >> 63 = 0). +Definition compute3 := Eval compute in 4611686018427387903 >> 63. +Check (eq_refl compute3 : 0 = 0). + +Check (eq_refl : (-1) >> 1 = -1). +Check (eq_refl (-1) <: (-1) >> 1 = -1). +Check (eq_refl (-1) <<: (-1) >> 1 = -1). +Definition compute4 := Eval compute in (-1) >> 1. +Check (eq_refl compute4 : -1 = -1). + +Check (eq_refl : (-1) >> (-1) = 0). +Check (eq_refl 0 <: (-1) >> (-1) = 0). +Check (eq_refl 0 <<: (-1) >> (-1) = 0). +Definition compute5 := Eval compute in (-1) >> (-1). +Check (eq_refl compute5 : 0 = 0). + +Check (eq_refl : 73 >> (-2) = 0). +Check (eq_refl 0 <: 73 >> (-2) = 0). +Check (eq_refl 0 <<: 73 >> (-2) = 0). +Definition compute6 := Eval compute in 73 >> (-2). +Check (eq_refl compute6 : 0 = 0). diff --git a/test-suite/primitive/sint63/compare.v b/test-suite/primitive/sint63/compare.v new file mode 100644 index 0000000000..7a9882f1c8 --- /dev/null +++ b/test-suite/primitive/sint63/compare.v @@ -0,0 +1,36 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 1 ?= 1 = Eq). +Check (eq_refl Eq <: 1 ?= 1 = Eq). +Check (eq_refl Eq <<: 1 ?= 1 = Eq). +Definition compute1 := Eval compute in 1 ?= 1. +Check (eq_refl compute1 : Eq = Eq). + +Check (eq_refl : 1 ?= 2 = Lt). +Check (eq_refl Lt <: 1 ?= 2 = Lt). +Check (eq_refl Lt <<: 1 ?= 2 = Lt). +Definition compute2 := Eval compute in 1 ?= 2. +Check (eq_refl compute2 : Lt = Lt). + +Check (eq_refl : 4611686018427387903 ?= 0 = Gt). +Check (eq_refl Gt <: 4611686018427387903 ?= 0 = Gt). +Check (eq_refl Gt <<: 4611686018427387903 ?= 0 = Gt). +Definition compute3 := Eval compute in 4611686018427387903 ?= 0. +Check (eq_refl compute3 : Gt = Gt). + +Check (eq_refl : -1 ?= 1 = Lt). +Check (eq_refl Lt <: -1 ?= 1 = Lt). +Check (eq_refl Lt <<: -1 ?= 1 = Lt). +Definition compute4 := Eval compute in -1 ?= 1. +Check (eq_refl compute4 : Lt = Lt). + +Check (eq_refl : 4611686018427387903 ?= -4611686018427387904 = Gt). +Check (eq_refl Gt <: 4611686018427387903 ?= -4611686018427387904 = Gt). +Check (eq_refl Gt <<: 4611686018427387903 ?= -4611686018427387904 = Gt). +Definition compute5 := + Eval compute in 4611686018427387903 ?= -4611686018427387904. +Check (eq_refl compute5 : Gt = Gt). diff --git a/test-suite/primitive/sint63/div.v b/test-suite/primitive/sint63/div.v new file mode 100644 index 0000000000..9da628ce1e --- /dev/null +++ b/test-suite/primitive/sint63/div.v @@ -0,0 +1,61 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 6 / 3 = 2). +Check (eq_refl 2 <: 6 / 3 = 2). +Check (eq_refl 2 <<: 6 / 3 = 2). +Definition compute1 := Eval compute in 6 / 3. +Check (eq_refl compute1 : 2 = 2). + +Check (eq_refl : -6 / 3 = -2). +Check (eq_refl (-2) <: -6 / 3 = -2). +Check (eq_refl (-2) <<: -6 / 3 = -2). +Definition compute2 := Eval compute in -6 / 3. +Check (eq_refl compute2 : -2 = -2). + +Check (eq_refl : 6 / -3 = -2). +Check (eq_refl (-2) <: 6 / -3 = -2). +Check (eq_refl (-2) <<: 6 / -3 = -2). +Definition compute3 := Eval compute in 6 / -3. +Check (eq_refl compute3 : -2 = -2). + +Check (eq_refl : -6 / -3 = 2). +Check (eq_refl 2 <: -6 / -3 = 2). +Check (eq_refl 2 <<: -6 / -3 = 2). +Definition compute4 := Eval compute in -6 / -3. +Check (eq_refl compute4 : 2 = 2). + +Check (eq_refl : 3 / 2 = 1). +Check (eq_refl 1 <: 3 / 2 = 1). +Check (eq_refl 1 <<: 3 / 2 = 1). +Definition compute5 := Eval compute in 3 / 2. +Check (eq_refl compute5 : 1 = 1). + +Check (eq_refl : -3 / 2 = -1). +Check (eq_refl (-1) <: -3 / 2 = -1). +Check (eq_refl (-1) <<: -3 / 2 = -1). +Definition compute6 := Eval compute in -3 / 2. +Check (eq_refl compute6 : -1 = -1). + +Check (eq_refl : 3 / -2 = -1). +Check (eq_refl (-1) <: 3 / -2 = -1). +Check (eq_refl (-1) <<: 3 / -2 = -1). +Definition compute7 := Eval compute in 3 / -2. +Check (eq_refl compute7 : -1 = -1). + +Check (eq_refl : -3 / -2 = 1). +Check (eq_refl 1 <: -3 / -2 = 1). +Check (eq_refl 1 <<: -3 / -2 = 1). +Definition compute8 := Eval compute in -3 / -2. +Check (eq_refl compute8 : 1 = 1). + +Check (eq_refl : -4611686018427387904 / -1 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <: + -4611686018427387904 / -1 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <<: + -4611686018427387904 / -1 = -4611686018427387904). +Definition compute9 := Eval compute in -4611686018427387904 / -1. +Check (eq_refl compute9 : -4611686018427387904 = -4611686018427387904). diff --git a/test-suite/primitive/sint63/eqb.v b/test-suite/primitive/sint63/eqb.v new file mode 100644 index 0000000000..4d365acf54 --- /dev/null +++ b/test-suite/primitive/sint63/eqb.v @@ -0,0 +1,17 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 1 =? 1 = true). +Check (eq_refl true <: 1 =? 1 = true). +Check (eq_refl true <<: 1 =? 1 = true). +Definition compute1 := Eval compute in 1 =? 1. +Check (eq_refl compute1 : true = true). + +Check (eq_refl : 4611686018427387903 =? 0 = false). +Check (eq_refl false <: 4611686018427387903 =? 0 = false). +Check (eq_refl false <<: 4611686018427387903 =? 0 = false). +Definition compute2 := Eval compute in 4611686018427387903 =? 0. +Check (eq_refl compute2 : false = false). diff --git a/test-suite/primitive/sint63/isint.v b/test-suite/primitive/sint63/isint.v new file mode 100644 index 0000000000..f1c9c2cfd1 --- /dev/null +++ b/test-suite/primitive/sint63/isint.v @@ -0,0 +1,50 @@ +(* This file tests the check that arithmetic operations use to know if their +arguments are ground. The various test cases correspond to possible +optimizations of these tests made by the compiler. *) +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Section test. + +Variable m n : int. + +Check (eq_refl : (fun x => x + 3) m = m + 3). +Check (eq_refl (m + 3) <: (fun x => x + 3) m = m + 3). +Check (eq_refl (m + 3) <<: (fun x => x + 3) m = m + 3). +Definition compute1 := Eval compute in (fun x => x + 3) m. +Check (eq_refl compute1 : m + 3 = m + 3). + +Check (eq_refl : (fun x => 3 + x) m = 3 + m). +Check (eq_refl (3 + m) <: (fun x => 3 + x) m = 3 + m). +Check (eq_refl (3 + m) <<: (fun x => 3 + x) m = 3 + m). +Definition compute2 := Eval compute in (fun x => 3 + x) m. +Check (eq_refl compute2 : 3 + m = 3 + m). + +Check (eq_refl : (fun x y => x + y) m n = m + n). +Check (eq_refl (m + n) <: (fun x y => x + y) m n = m + n). +Check (eq_refl (m + n) <<: (fun x y => x + y) m n = m + n). +Definition compute3 := Eval compute in (fun x y => x + y) m n. +Check (eq_refl compute3 : m + n = m + n). + +Check (eq_refl : (fun x y => x + y) 2 3 = 5). +Check (eq_refl 5 <: (fun x y => x + y) 2 3 = 5). +Check (eq_refl 5 <<: (fun x y => x + y) 2 3 = 5). +Definition compute4 := Eval compute in (fun x y => x + y) 2 3. +Check (eq_refl compute4 : 5 = 5). + +Check (eq_refl : (fun x => x + x) m = m + m). +Check (eq_refl (m + m) <: (fun x => x + x) m = m + m). +Check (eq_refl (m + m) <<: (fun x => x + x) m = m + m). +Definition compute5 := Eval compute in (fun x => x + x) m. +Check (eq_refl compute5 : m + m = m + m). + +Check (eq_refl : (fun x => x + x) 2 = 4). +Check (eq_refl 4 <: (fun x => x + x) 2 = 4). +Check (eq_refl 4 <<: (fun x => x + x) 2 = 4). +Definition compute6 := Eval compute in (fun x => x + x) 2. +Check (eq_refl compute6 : 4 = 4). + +End test. diff --git a/test-suite/primitive/sint63/leb.v b/test-suite/primitive/sint63/leb.v new file mode 100644 index 0000000000..dbe958e41d --- /dev/null +++ b/test-suite/primitive/sint63/leb.v @@ -0,0 +1,29 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 1 <=? 1 = true). +Check (eq_refl true <: 1 <=? 1 = true). +Check (eq_refl true <<: 1 <=? 1 = true). +Definition compute1 := Eval compute in 1 <=? 1. +Check (eq_refl compute1 : true = true). + +Check (eq_refl : 1 <=? 2 = true). +Check (eq_refl true <: 1 <=? 2 = true). +Check (eq_refl true <<: 1 <=? 2 = true). +Definition compute2 := Eval compute in 1 <=? 2. +Check (eq_refl compute2 : true = true). + +Check (eq_refl : 4611686018427387903 <=? 0 = false). +Check (eq_refl false <: 4611686018427387903 <=? 0 = false). +Check (eq_refl false <<: 4611686018427387903 <=? 0 = false). +Definition compute3 := Eval compute in 4611686018427387903 <=? 0. +Check (eq_refl compute3 : false = false). + +Check (eq_refl : 1 <=? -1 = false). +Check (eq_refl false <: 1 <=? -1 = false). +Check (eq_refl false <<: 1 <=? -1 = false). +Definition compute4 := Eval compute in 1 <=? -1. +Check (eq_refl compute4 : false = false). diff --git a/test-suite/primitive/sint63/lsl.v b/test-suite/primitive/sint63/lsl.v new file mode 100644 index 0000000000..082c42979a --- /dev/null +++ b/test-suite/primitive/sint63/lsl.v @@ -0,0 +1,43 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 3 << 61 = -2305843009213693952). +Check (eq_refl (-2305843009213693952) <: 3 << 61 = -2305843009213693952). +Check (eq_refl (-2305843009213693952) <<: 3 << 61 = -2305843009213693952). +Definition compute1 := Eval compute in 3 << 61. +Check (eq_refl compute1 : -2305843009213693952 = -2305843009213693952). + +Check (eq_refl : 2 << 62 = 0). +Check (eq_refl 0 <: 2 << 62 = 0). +Check (eq_refl 0 <<: 2 << 62 = 0). +Definition compute2 := Eval compute in 2 << 62. +Check (eq_refl compute2 : 0 = 0). + +Check (eq_refl : 4611686018427387903 << 63 = 0). +Check (eq_refl 0 <: 4611686018427387903 << 63 = 0). +Check (eq_refl 0 <<: 4611686018427387903 << 63 = 0). +Definition compute3 := Eval compute in 4611686018427387903 << 63. +Check (eq_refl compute3 : 0 = 0). + +Check (eq_refl : 4611686018427387903 << 62 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <: + 4611686018427387903 << 62 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <<: + 4611686018427387903 << 62 = -4611686018427387904). +Definition compute4 := Eval compute in 4611686018427387903 << 62. +Check (eq_refl compute4 : -4611686018427387904 = -4611686018427387904). + +Check (eq_refl : 1 << 62 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <: 1 << 62 = -4611686018427387904). +Check (eq_refl (-4611686018427387904) <<: 1 << 62 = -4611686018427387904). +Definition compute5 := Eval compute in 1 << 62. +Check (eq_refl compute5 : -4611686018427387904 = -4611686018427387904). + +Check (eq_refl : -1 << 1 = -2). +Check (eq_refl (-2) <: -1 << 1 = -2). +Check (eq_refl (-2) <<: -1 << 1 = -2). +Definition compute6 := Eval compute in -1 << 1. +Check (eq_refl compute6 : -2 = -2). diff --git a/test-suite/primitive/sint63/ltb.v b/test-suite/primitive/sint63/ltb.v new file mode 100644 index 0000000000..aa72e1d377 --- /dev/null +++ b/test-suite/primitive/sint63/ltb.v @@ -0,0 +1,29 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 1 <? 1 = false). +Check (eq_refl false <: 1 <? 1 = false). +Check (eq_refl false <<: 1 <? 1 = false). +Definition compute1 := Eval compute in 1 <? 1. +Check (eq_refl compute1 : false = false). + +Check (eq_refl : 1 <? 2 = true). +Check (eq_refl true <: 1 <? 2 = true). +Check (eq_refl true <<: 1 <? 2 = true). +Definition compute2 := Eval compute in 1 <? 2. +Check (eq_refl compute2 : true = true). + +Check (eq_refl : 4611686018427387903 <? 0 = false). +Check (eq_refl false <: 4611686018427387903 <? 0 = false). +Check (eq_refl false <<: 4611686018427387903 <? 0 = false). +Definition compute3 := Eval compute in 4611686018427387903 <? 0. +Check (eq_refl compute3 : false = false). + +Check (eq_refl : 1 <? -1 = false). +Check (eq_refl false <: 1 <? -1 = false). +Check (eq_refl false <<: 1 <? -1 = false). +Definition compute4 := Eval compute in 1 <? -1. +Check (eq_refl compute4 : false = false). diff --git a/test-suite/primitive/sint63/mod.v b/test-suite/primitive/sint63/mod.v new file mode 100644 index 0000000000..a4872b45f3 --- /dev/null +++ b/test-suite/primitive/sint63/mod.v @@ -0,0 +1,53 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 6 mod 3 = 0). +Check (eq_refl 0 <: 6 mod 3 = 0). +Check (eq_refl 0 <<: 6 mod 3 = 0). +Definition compute1 := Eval compute in 6 mod 3. +Check (eq_refl compute1 : 0 = 0). + +Check (eq_refl : -6 mod 3 = 0). +Check (eq_refl 0 <: -6 mod 3 = 0). +Check (eq_refl 0 <<: -6 mod 3 = 0). +Definition compute2 := Eval compute in -6 mod 3. +Check (eq_refl compute2 : 0 = 0). + +Check (eq_refl : 6 mod -3 = 0). +Check (eq_refl 0 <: 6 mod -3 = 0). +Check (eq_refl 0 <<: 6 mod -3 = 0). +Definition compute3 := Eval compute in 6 mod -3. +Check (eq_refl compute3 : 0 = 0). + +Check (eq_refl : -6 mod -3 = 0). +Check (eq_refl 0 <: -6 mod -3 = 0). +Check (eq_refl 0 <<: -6 mod -3 = 0). +Definition compute4 := Eval compute in -6 mod -3. +Check (eq_refl compute4 : 0 = 0). + +Check (eq_refl : 5 mod 3 = 2). +Check (eq_refl 2 <: 5 mod 3 = 2). +Check (eq_refl 2 <<: 5 mod 3 = 2). +Definition compute5 := Eval compute in 5 mod 3. +Check (eq_refl compute5 : 2 = 2). + +Check (eq_refl : -5 mod 3 = -2). +Check (eq_refl (-2) <: -5 mod 3 = -2). +Check (eq_refl (-2) <<: -5 mod 3 = -2). +Definition compute6 := Eval compute in -5 mod 3. +Check (eq_refl compute6 : -2 = -2). + +Check (eq_refl : 5 mod -3 = 2). +Check (eq_refl 2 <: 5 mod -3 = 2). +Check (eq_refl 2 <<: 5 mod -3 = 2). +Definition compute7 := Eval compute in 5 mod -3. +Check (eq_refl compute7 : 2 = 2). + +Check (eq_refl : -5 mod -3 = -2). +Check (eq_refl (-2) <: -5 mod -3 = -2). +Check (eq_refl (-2) <<: -5 mod -3 = -2). +Definition compute8 := Eval compute in -5 mod -3. +Check (eq_refl compute8 : -2 = -2). diff --git a/test-suite/primitive/sint63/mul.v b/test-suite/primitive/sint63/mul.v new file mode 100644 index 0000000000..f72f643083 --- /dev/null +++ b/test-suite/primitive/sint63/mul.v @@ -0,0 +1,35 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 2 * 3 = 6). +Check (eq_refl 6 <: 2 * 3 = 6). +Check (eq_refl 6 <<: 2 * 3 = 6). +Definition compute1 := Eval compute in 2 * 3. +Check (eq_refl compute1 : 6 = 6). + +Check (eq_refl : -2 * 3 = -6). +Check (eq_refl (-6) <: -2 * 3 = -6). +Check (eq_refl (-6) <<: -2 * 3 = -6). +Definition compute2 := Eval compute in -2 * 3. +Check (eq_refl compute2 : -6 = -6). + +Check (eq_refl : 2 * -3 = -6). +Check (eq_refl (-6) <: 2 * -3 = -6). +Check (eq_refl (-6) <<: 2 * -3 = -6). +Definition compute3 := Eval compute in 2 * -3. +Check (eq_refl compute3 : -6 = -6). + +Check (eq_refl : -2 * -3 = 6). +Check (eq_refl 6 <: -2 * -3 = 6). +Check (eq_refl 6 <<: -2 * -3 = 6). +Definition compute4 := Eval compute in -2 * -3. +Check (eq_refl compute4 : 6 = 6). + +Check (eq_refl : 4611686018427387903 * 2 = -2). +Check (eq_refl (-2) <: 4611686018427387903 * 2 = -2). +Check (eq_refl (-2) <<: 4611686018427387903 * 2 = -2). +Definition compute5 := Eval compute in 4611686018427387903 * 2. +Check (eq_refl compute5 : -2 = -2). diff --git a/test-suite/primitive/sint63/signed.v b/test-suite/primitive/sint63/signed.v new file mode 100644 index 0000000000..d8333a8efb --- /dev/null +++ b/test-suite/primitive/sint63/signed.v @@ -0,0 +1,18 @@ +(* This file checks that operations over sint63 are signed. *) +Require Import Sint63. + +Open Scope sint63_scope. + +(* (0-1) must be negative 1 and not the maximum integer value *) + +Check (eq_refl : 1/(0-1) = -1). +Check (eq_refl (-1) <: 1/(0-1) = -1). +Check (eq_refl (-1) <<: 1/(0-1) = -1). +Definition compute1 := Eval compute in 1/(0-1). +Check (eq_refl compute1 : -1 = -1). + +Check (eq_refl : 3 mod (0-1) = 0). +Check (eq_refl 0 <: 3 mod (0-1) = 0). +Check (eq_refl 0 <<: 3 mod (0-1) = 0). +Definition compute2 := Eval compute in 3 mod (0-1). +Check (eq_refl compute2 : 0 = 0). diff --git a/test-suite/primitive/sint63/sub.v b/test-suite/primitive/sint63/sub.v new file mode 100644 index 0000000000..8504177286 --- /dev/null +++ b/test-suite/primitive/sint63/sub.v @@ -0,0 +1,25 @@ +Require Import Sint63. + +Set Implicit Arguments. + +Open Scope sint63_scope. + +Check (eq_refl : 3 - 2 = 1). +Check (eq_refl 1 <: 3 - 2 = 1). +Check (eq_refl 1 <<: 3 - 2 = 1). +Definition compute1 := Eval compute in 3 - 2. +Check (eq_refl compute1 : 1 = 1). + +Check (eq_refl : 0 - 1 = -1). +Check (eq_refl (-1) <: 0 - 1 = -1). +Check (eq_refl (-1) <<: 0 - 1 = -1). +Definition compute2 := Eval compute in 0 - 1. +Check (eq_refl compute2 : -1 = -1). + +Check (eq_refl : -4611686018427387904 - 1 = 4611686018427387903). +Check (eq_refl 4611686018427387903 <: + -4611686018427387904 - 1 = 4611686018427387903). +Check (eq_refl 4611686018427387903 <<: + -4611686018427387904 - 1 = 4611686018427387903). +Definition compute3 := Eval compute in -4611686018427387904 - 1. +Check (eq_refl compute3 : 4611686018427387903 = 4611686018427387903). diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 7bb725538b..a3ebe67325 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -205,6 +205,7 @@ Qed. Corollary to_Z_bounded : forall x, (0 <= φ x < wB)%Z. Proof. apply to_Z_rec_bounded. Qed. + (* =================================================== *) Local Open Scope Z_scope. (* General arithmetic results *) @@ -1904,6 +1905,22 @@ Qed. Lemma lxor0_r i : i lxor 0 = i. Proof. rewrite lxorC; exact (lxor0 i). Qed. +Lemma opp_to_Z_opp (x : int) : + φ x mod wB <> 0 -> + (- φ (- x)) mod wB = (φ x) mod wB. +Proof. + intros neqx0. + rewrite opp_spec. + rewrite (Z_mod_nz_opp_full (φ x%int63)) by assumption. + rewrite (Z.mod_small (φ x%int63)) by apply to_Z_bounded. + rewrite <- Z.add_opp_l. + rewrite Z.opp_add_distr, Z.opp_involutive. + replace (- wB) with (-1 * wB) by easy. + rewrite Z_mod_plus by easy. + now rewrite Z.mod_small by apply to_Z_bounded. +Qed. + + Module Export Int63Notations. Local Open Scope int63_scope. #[deprecated(since="8.13",note="use infix mod instead")] diff --git a/theories/Numbers/Cyclic/Int63/PrimInt63.v b/theories/Numbers/Cyclic/Int63/PrimInt63.v index 64c1b862c7..98127ef0ac 100644 --- a/theories/Numbers/Cyclic/Int63/PrimInt63.v +++ b/theories/Numbers/Cyclic/Int63/PrimInt63.v @@ -17,11 +17,21 @@ Register comparison as kernel.ind_cmp. Primitive int := #int63_type. Register int as num.int63.type. +Variant pos_neg_int63 := Pos (d:int) | Neg (d:int). +Register pos_neg_int63 as num.int63.pos_neg_int63. Declare Scope int63_scope. Definition id_int : int -> int := fun x => x. -Declare ML Module "int63_syntax_plugin". - -Module Export Int63NotationsInternalA. +Record int_wrapper := wrap_int {int_wrap : int}. +Register wrap_int as num.int63.wrap_int. +Definition printer (x : int_wrapper) : pos_neg_int63 := Pos (int_wrap x). +Definition parser (x : pos_neg_int63) : option int := + match x with + | Pos p => Some p + | Neg _ => None + end. +Number Notation int parser printer : int63_scope. + +Module Import Int63NotationsInternalA. Delimit Scope int63_scope with int63. Bind Scope int63_scope with int. End Int63NotationsInternalA. @@ -37,6 +47,9 @@ Primitive lor := #int63_lor. Primitive lxor := #int63_lxor. + +Primitive asr := #int63_asr. + (* Arithmetic modulo operations *) Primitive add := #int63_add. @@ -50,6 +63,10 @@ Primitive div := #int63_div. Primitive mod := #int63_mod. +Primitive divs := #int63_divs. + +Primitive mods := #int63_mods. + (* Comparisons *) Primitive eqb := #int63_eq. @@ -57,6 +74,10 @@ Primitive ltb := #int63_lt. Primitive leb := #int63_le. +Primitive ltsb := #int63_lts. + +Primitive lesb := #int63_les. + (** Exact arithmetic operations *) Primitive addc := #int63_addc. @@ -76,7 +97,13 @@ Primitive addmuldiv := #int63_addmuldiv. (** Comparison *) Primitive compare := #int63_compare. +Primitive compares := #int63_compares. + (** Exotic operations *) Primitive head0 := #int63_head0. Primitive tail0 := #int63_tail0. + +Module Export PrimInt63Notations. + Export Int63NotationsInternalA. +End PrimInt63Notations. diff --git a/theories/Numbers/Cyclic/Int63/Sint63.v b/theories/Numbers/Cyclic/Int63/Sint63.v new file mode 100644 index 0000000000..c0239ae3db --- /dev/null +++ b/theories/Numbers/Cyclic/Int63/Sint63.v @@ -0,0 +1,407 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import ZArith. +Import Znumtheory. +Require Export Int63. +Require Import Lia. + +Declare Scope sint63_scope. +Definition printer (x : int_wrapper) : pos_neg_int63 := + if (int_wrap x <? 4611686018427387904)%int63 then (* 2^62 *) + Pos (int_wrap x) + else + Neg ((int_wrap x) lxor max_int + 1)%int63. +Definition parser (x : pos_neg_int63) : option int := + match x with + | Pos p => if (p <? 4611686018427387904)%int63 then Some p else None + | Neg n => if (n <=? 4611686018427387904)%int63 + then Some ((n - 1) lxor max_int)%int63 else None + end. +Number Notation int parser printer : sint63_scope. + + +Module Import Sint63NotationsInternalA. +Delimit Scope sint63_scope with sint63. +Bind Scope sint63_scope with int. +End Sint63NotationsInternalA. + + +Module Import Sint63NotationsInternalB. +Infix "<<" := Int63.lsl (at level 30, no associativity) : sint63_scope. +(* TODO do we want >> to be asr or lsr? And is there a notation for the other one? *) +Infix ">>" := asr (at level 30, no associativity) : sint63_scope. +Infix "land" := Int63.land (at level 40, left associativity) : sint63_scope. +Infix "lor" := Int63.lor (at level 40, left associativity) : sint63_scope. +Infix "lxor" := Int63.lxor (at level 40, left associativity) : sint63_scope. +Infix "+" := Int63.add : sint63_scope. +Infix "-" := Int63.sub : sint63_scope. +Infix "*" := Int63.mul : sint63_scope. +Infix "/" := divs : sint63_scope. +Infix "mod" := mods (at level 40, no associativity) : sint63_scope. +Infix "=?" := Int63.eqb (at level 70, no associativity) : sint63_scope. +Infix "<?" := ltsb (at level 70, no associativity) : sint63_scope. +Infix "<=?" := lesb (at level 70, no associativity) : sint63_scope. +Infix "≤?" := lesb (at level 70, no associativity) : sint63_scope. +Notation "- x" := (opp x) : sint63_scope. +Notation "n ?= m" := (compares n m) (at level 70, no associativity) : sint63_scope. +End Sint63NotationsInternalB. + +Definition min_int := Eval vm_compute in (lsl 1 62). +Definition max_int := Eval vm_compute in (min_int - 1)%sint63. + +(** Translation to and from Z *) +Definition to_Z (i:int) := + if (i <? min_int)%int63 then + φ i%int63 + else + (- φ (- i)%int63)%Z. + +Lemma to_Z_0 : to_Z 0 = 0. +Proof. easy. Qed. + +Lemma to_Z_min : to_Z min_int = - (wB / 2). +Proof. easy. Qed. + +Lemma to_Z_max : to_Z max_int = wB / 2 - 1. +Proof. easy. Qed. + +Lemma to_Z_bounded : forall x, (to_Z min_int <= to_Z x <= to_Z max_int)%Z. +Proof. + intros x; unfold to_Z. + case ltbP; [> lia | intros _]. + case (ltbP max_int); [> intros _ | now intros H; exfalso; apply H]. + rewrite opp_spec. + rewrite Z_mod_nz_opp_full by easy. + rewrite Z.mod_small by apply Int63.to_Z_bounded. + case ltbP. + - intros ltxmin; split. + + now transitivity 0%Z; [>| now apply Int63.to_Z_bounded]. + + replace (φ min_int%int63) with (φ max_int%int63 + 1)%Z in ltxmin. + * lia. + * now compute. + - rewrite Z.nlt_ge; intros leminx. + rewrite opp_spec. + rewrite Z_mod_nz_opp_full. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + split. + * rewrite <- Z.opp_le_mono. + now rewrite <- Z.sub_le_mono_l. + * transitivity 0%Z; [>| now apply Int63.to_Z_bounded]. + rewrite Z.opp_nonpos_nonneg. + apply Zle_minus_le_0. + apply Z.lt_le_incl. + now apply Int63.to_Z_bounded. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + now intros eqx0; rewrite eqx0 in leminx. +Qed. + +Lemma of_to_Z : forall x, of_Z (to_Z x) = x. +Proof. + unfold to_Z, of_Z. + intros x. + generalize (Int63.to_Z_bounded x). + case ltbP. + - intros ltxmin [leq0x _]. + generalize (Int63.of_to_Z x). + destruct (φ x%int63). + + now intros <-. + + now intros <-; unfold Int63.of_Z. + + now intros _. + - intros nltxmin leq0xltwB. + rewrite (opp_spec x). + rewrite Z_mod_nz_opp_full. + + rewrite Zmod_small by easy. + destruct (wB - φ x%int63) eqn: iswbmx. + * lia. + * simpl. + apply to_Z_inj. + rewrite opp_spec. + generalize (of_Z_spec (Z.pos p)). + simpl Int63.of_Z; intros ->. + rewrite <- iswbmx. + rewrite <- Z.sub_0_l. + rewrite <- (Zmod_0_l wB). + rewrite <- Zminus_mod. + replace (0 - _) with (φ x%int63 - wB) by ring. + rewrite <- Zminus_mod_idemp_r. + rewrite Z_mod_same_full. + rewrite Z.sub_0_r. + now rewrite Z.mod_small. + * lia. + + rewrite Z.mod_small by easy. + intros eqx0; revert nltxmin; rewrite eqx0. + now compute. +Qed. + +Lemma to_Z_inj (x y : int) : to_Z x = to_Z y -> x = y. +Proof. exact (fun e => can_inj of_to_Z e). Qed. + +Lemma to_Z_mod_Int63to_Z (x : int) : to_Z x mod wB = φ x%int63. +Proof. + unfold to_Z. + case ltbP; [> now rewrite Z.mod_small by now apply Int63.to_Z_bounded |]. + rewrite Z.nlt_ge; intros gexmin. + rewrite opp_to_Z_opp; rewrite Z.mod_small by now apply Int63.to_Z_bounded. + - easy. + - now intros neqx0; rewrite neqx0 in gexmin. +Qed. + + +(** Centered modulo *) +Definition cmod (x d : Z) : Z := + (x + d / 2) mod d - (d / 2). + +Lemma cmod_mod (x d : Z) : + cmod (x mod d) d = cmod x d. +Proof. + now unfold cmod; rewrite Zplus_mod_idemp_l. +Qed. + +Lemma cmod_small (x d : Z) : + - (d / 2) <= x < d / 2 -> cmod x d = x. +Proof. + intros bound. + unfold cmod. + rewrite Zmod_small; [> lia |]. + split; [> lia |]. + rewrite Z.lt_add_lt_sub_r. + apply (Z.lt_le_trans _ (d / 2)); [> easy |]. + now rewrite <- Z.le_add_le_sub_r, Z.add_diag, Z.mul_div_le. +Qed. + +Lemma to_Z_cmodwB (x : int) : + to_Z x = cmod (φ x%int63) wB. +Proof. + unfold to_Z, cmod. + case ltbP; change φ (min_int)%int63 with (wB / 2). + - intros ltxmin. + rewrite Z.mod_small; [> lia |]. + split. + + now apply Z.add_nonneg_nonneg; try apply Int63.to_Z_bounded. + + change wB with (wB / 2 + wB / 2) at 2; lia. + - rewrite Z.nlt_ge; intros gexmin. + rewrite Int63.opp_spec. + rewrite Z_mod_nz_opp_full. + + rewrite Z.mod_small by apply Int63.to_Z_bounded. + rewrite <- (Z_mod_plus_full _ (-1)). + change (-1 * wB) with (- (wB / 2) - wB / 2). + rewrite <- Z.add_assoc, Zplus_minus. + rewrite Z.mod_small. + * change wB with (wB / 2 + wB / 2) at 1; lia. + * split; [> lia |]. + apply Z.lt_sub_lt_add_r. + transitivity wB; [>| easy]. + now apply Int63.to_Z_bounded. + + rewrite Z.mod_small by now apply Int63.to_Z_bounded. + now intros not0; rewrite not0 in gexmin. +Qed. + +Lemma of_Z_spec (z : Z) : to_Z (of_Z z) = cmod z wB. +Proof. now rewrite to_Z_cmodwB, Int63.of_Z_spec, cmod_mod. Qed. + +Lemma of_Z_cmod (z : Z) : of_Z (cmod z wB) = of_Z z. +Proof. now rewrite <- of_Z_spec, of_to_Z. Qed. + +Lemma is_int (z : Z) : + to_Z min_int <= z <= to_Z max_int -> + z = to_Z (of_Z z). +Proof. + rewrite to_Z_min, to_Z_max. + intros bound; rewrite of_Z_spec, cmod_small; lia. +Qed. + +(** Specification of operations that differ on signed and unsigned ints *) + +Axiom asr_spec : forall x p, to_Z (x >> p) = (to_Z x) / 2 ^ (to_Z p). + +Axiom div_spec : forall x y, + to_Z x <> to_Z min_int \/ to_Z y <> (-1)%Z -> + to_Z (x / y) = Z.quot (to_Z x) (to_Z y). + +Axiom mod_spec : forall x y, to_Z (x mod y) = Z.rem (to_Z x) (to_Z y). + +Axiom ltb_spec : forall x y, (x <? y)%sint63 = true <-> to_Z x < to_Z y. + +Axiom leb_spec : forall x y, (x <=? y)%sint63 = true <-> to_Z x <= to_Z y. + +Axiom compare_spec : forall x y, (x ?= y)%sint63 = (to_Z x ?= to_Z y). + +(** Specification of operations that coincide on signed and unsigned ints *) + +Lemma add_spec (x y : int) : + to_Z (x + y)%sint63 = cmod (to_Z x + to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.add_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Z.add_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma sub_spec (x y : int) : + to_Z (x - y)%sint63 = cmod (to_Z x - to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.sub_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Zminus_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma mul_spec (x y : int) : + to_Z (x * y)%sint63 = cmod (to_Z x * to_Z y) wB. +Proof. + rewrite to_Z_cmodwB, Int63.mul_spec. + rewrite <- 2!to_Z_mod_Int63to_Z, <- Zmult_mod by easy. + now rewrite cmod_mod. +Qed. + +Lemma succ_spec (x : int) : + to_Z (succ x)%sint63 = cmod (to_Z x + 1) wB. +Proof. now unfold succ; rewrite add_spec. Qed. + +Lemma pred_spec (x : int) : + to_Z (pred x)%sint63 = cmod (to_Z x - 1) wB. +Proof. now unfold pred; rewrite sub_spec. Qed. + +Lemma opp_spec (x : int) : + to_Z (- x)%sint63 = cmod (- to_Z x) wB. +Proof. + rewrite to_Z_cmodwB, Int63.opp_spec. + rewrite <- Z.sub_0_l, <- to_Z_mod_Int63to_Z, Zminus_mod_idemp_r. + now rewrite cmod_mod. +Qed. + +(** Behaviour when there is no under or overflow *) + +Lemma add_bounded (x y : int) : + to_Z min_int <= to_Z x + to_Z y <= to_Z max_int -> + to_Z (x + y) = to_Z x + to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite add_spec, cmod_small; [>| lia]. +Qed. + +Lemma sub_bounded (x y : int) : + to_Z min_int <= to_Z x - to_Z y <= to_Z max_int -> + to_Z (x - y) = to_Z x - to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite sub_spec, cmod_small; [>| lia]. +Qed. + +Lemma mul_bounded (x y : int) : + to_Z min_int <= to_Z x * to_Z y <= to_Z max_int -> + to_Z (x * y) = to_Z x * to_Z y. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite mul_spec, cmod_small; [>| lia]. +Qed. + +Lemma succ_bounded (x : int) : + to_Z min_int <= to_Z x + 1 <= to_Z max_int -> + to_Z (succ x) = to_Z x + 1. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite succ_spec, cmod_small; [>| lia]. +Qed. + +Lemma pred_bounded (x : int) : + to_Z min_int <= to_Z x - 1 <= to_Z max_int -> + to_Z (pred x) = to_Z x - 1. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite pred_spec, cmod_small; [>| lia]. +Qed. + +Lemma opp_bounded (x : int) : + to_Z min_int <= - to_Z x <= to_Z max_int -> + to_Z (- x) = - to_Z x. +Proof. + rewrite to_Z_min, to_Z_max; intros bound. + now rewrite opp_spec, cmod_small; [>| lia]. +Qed. + +(** Relationship with of_Z *) + +Lemma add_of_Z (x y : int) : + (x + y)%sint63 = of_Z (to_Z x + to_Z y). +Proof. now rewrite <- of_Z_cmod, <- add_spec, of_to_Z. Qed. + +Lemma sub_of_Z (x y : int) : + (x - y)%sint63 = of_Z (to_Z x - to_Z y). +Proof. now rewrite <- of_Z_cmod, <- sub_spec, of_to_Z. Qed. + +Lemma mul_of_Z (x y : int) : + (x * y)%sint63 = of_Z (to_Z x * to_Z y). +Proof. now rewrite <- of_Z_cmod, <- mul_spec, of_to_Z. Qed. + +Lemma succ_of_Z (x : int) : + (succ x)%sint63 = of_Z (to_Z x + 1). +Proof. now rewrite <- of_Z_cmod, <- succ_spec, of_to_Z. Qed. + +Lemma pred_of_Z (x : int) : + (pred x)%sint63 = of_Z (to_Z x - 1). +Proof. now rewrite <- of_Z_cmod, <- pred_spec, of_to_Z. Qed. + +Lemma opp_of_Z (x : int) : + (- x)%sint63 = of_Z (- to_Z x). +Proof. now rewrite <- of_Z_cmod, <- opp_spec, of_to_Z. Qed. + +(** Comparison *) +Import Bool. + +Lemma eqbP x y : reflect (to_Z x = to_Z y) (x =? y)%sint63. +Proof. + apply iff_reflect; rewrite Int63.eqb_spec. + now split; [> apply to_Z_inj | apply f_equal]. +Qed. + +Lemma ltbP x y : reflect (to_Z x < to_Z y) (x <? y)%sint63. +Proof. now apply iff_reflect; symmetry; apply ltb_spec. Qed. + +Lemma lebP x y : reflect (to_Z x <= to_Z y) (x ≤? y)%sint63. +Proof. now apply iff_reflect; symmetry; apply leb_spec. Qed. + +(** ASR *) +Lemma asr_0 (i : int) : (0 >> i)%sint63 = 0%sint63. +Proof. now apply to_Z_inj; rewrite asr_spec. Qed. + +Lemma asr_0_r (i : int) : (i >> 0)%sint63 = i. +Proof. now apply to_Z_inj; rewrite asr_spec, Zdiv_1_r. Qed. + +Lemma asr_neg_r (i n : int) : to_Z n < 0 -> (i >> n)%sint63 = 0%sint63. +Proof. + intros ltn0. + apply to_Z_inj. + rewrite asr_spec, Z.pow_neg_r by assumption. + now rewrite Zdiv_0_r. +Qed. + +Lemma asr_1 (n : int) : (1 >> n)%sint63 = (n =? 0)%sint63. +Proof. + apply to_Z_inj; rewrite asr_spec. + case eqbP; [> now intros -> | intros neqn0]. + case (lebP 0 n). + - intros le0n. + apply Z.div_1_l; apply Z.pow_gt_1; [> easy |]. + rewrite to_Z_0 in *; lia. + - rewrite Z.nle_gt; intros ltn0. + now rewrite Z.pow_neg_r. +Qed. + +Notation asr := asr (only parsing). +Notation div := divs (only parsing). +Notation rem := mods (only parsing). +Notation ltb := ltsb (only parsing). +Notation leb := lesb (only parsing). +Notation compare := compares (only parsing). + +Module Export Sint63Notations. + Export Sint63NotationsInternalA. + Export Sint63NotationsInternalB. +End Sint63Notations. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 06b02ab211..37d30a282c 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -173,6 +173,14 @@ Proof. apply N_ascii_bounded. Qed. +Definition ltb (a b : ascii) : bool := + (N_of_ascii a <? N_of_ascii b)%N. + +Definition leb (a b : ascii) : bool := + (N_of_ascii a <=? N_of_ascii b)%N. + +Infix "<?" := ltb : char_scope. +Infix "<=?" := leb : char_scope. (** * Concrete syntax *) diff --git a/theories/dune b/theories/dune index 18e000cfe1..90e9522b7b 100644 --- a/theories/dune +++ b/theories/dune @@ -15,7 +15,6 @@ coq.plugins.firstorder coq.plugins.number_string_notation - coq.plugins.int63_syntax coq.plugins.float_syntax coq.plugins.btauto diff --git a/theories/extraction/ExtrOCamlInt63.v b/theories/extraction/ExtrOCamlInt63.v index 7f7b4af98d..1949a1a9d8 100644 --- a/theories/extraction/ExtrOCamlInt63.v +++ b/theories/extraction/ExtrOCamlInt63.v @@ -10,7 +10,7 @@ (** Extraction to OCaml of native 63-bit machine integers. *) -From Coq Require Int63 Extraction. +From Coq Require Int63 Sint63 Extraction. (** Basic data types used by some primitive operators. *) @@ -26,6 +26,7 @@ Extraction Inline Int63.int. Extract Constant Int63.lsl => "Uint63.l_sl". Extract Constant Int63.lsr => "Uint63.l_sr". +Extract Constant Sint63.asr => "Uint63.a_sr". Extract Constant Int63.land => "Uint63.l_and". Extract Constant Int63.lor => "Uint63.l_or". Extract Constant Int63.lxor => "Uint63.l_xor". @@ -36,10 +37,15 @@ Extract Constant Int63.mul => "Uint63.mul". Extract Constant Int63.mulc => "Uint63.mulc". Extract Constant Int63.div => "Uint63.div". Extract Constant Int63.mod => "Uint63.rem". +Extract Constant Sint63.div => "Uint63.divs". +Extract Constant Sint63.rem => "Uint63.rems". + Extract Constant Int63.eqb => "Uint63.equal". Extract Constant Int63.ltb => "Uint63.lt". Extract Constant Int63.leb => "Uint63.le". +Extract Constant Sint63.ltb => "Uint63.lts". +Extract Constant Sint63.leb => "Uint63.les". Extract Constant Int63.addc => "Uint63.addc". Extract Constant Int63.addcarryc => "Uint63.addcarryc". @@ -51,6 +57,7 @@ Extract Constant Int63.diveucl_21 => "Uint63.div21". Extract Constant Int63.addmuldiv => "Uint63.addmuldiv". Extract Constant Int63.compare => "Uint63.compare". +Extract Constant Sint63.compare => "Uint63.compares". Extract Constant Int63.head0 => "Uint63.head0". Extract Constant Int63.tail0 => "Uint63.tail0". diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 6ebf9b71d6..b8d5032373 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -87,8 +87,7 @@ let obsolete s = course). *) let banner () = - eprintf "This is coqdoc version %s, compiled on %s\n" - Coq_config.version Coq_config.compile_date; + eprintf "This is coqdoc version %s\n" Coq_config.version; flush stderr let target_full_name f = diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index ca09bad441..041097d2d3 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -216,9 +216,8 @@ let compile_file opts stm_opts copts injections (f_in, echo) = else compile opts stm_opts copts injections ~echo ~f_in ~f_out -let compile_files (opts, stm_opts) copts injections = - let compile_list = copts.compile_list in - List.iter (compile_file opts stm_opts copts injections) compile_list +let compile_file opts stm_opts copts injections = + Option.iter (compile_file opts stm_opts copts injections) copts.compile_file (******************************************************************************) (* VIO Dispatching *) diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli index 9f3783f32e..e9e83af3ad 100644 --- a/toplevel/ccompile.mli +++ b/toplevel/ccompile.mli @@ -12,8 +12,8 @@ the init (rc) file *) val load_init_vernaculars : Coqargs.t -> state:Vernac.State.t-> Vernac.State.t -(** [compile_files opts] compile files specified in [opts] *) -val compile_files : Coqargs.t * Stm.AsyncOpts.stm_opt -> Coqcargs.t -> Coqargs.injection_command list -> unit +(** [compile_file opts] compile file specified in [opts] *) +val compile_file : Coqargs.t -> Stm.AsyncOpts.stm_opt -> Coqcargs.t -> Coqargs.injection_command list -> unit (** [do_vio opts] process [.vio] files in [opts] *) val do_vio : Coqargs.t -> Coqcargs.t -> Coqargs.injection_command list -> unit diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index a403640149..b7af66b2ee 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -44,7 +44,7 @@ coqc specific options:\ let coqc_main ((copts,_),stm_opts) injections ~opts = Topfmt.(in_phase ~phase:CompilationPhase) - Ccompile.compile_files (opts,stm_opts) copts injections; + Ccompile.compile_file opts stm_opts copts injections; (* Careful this will modify the load-path and state so after this point some stuff may not be safe anymore. *) diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index f84d73ed17..efd8a79e18 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -13,7 +13,7 @@ type compilation_mode = BuildVo | BuildVio | Vio2Vo | BuildVos | BuildVok type t = { compilation_mode : compilation_mode - ; compile_list: (string * bool) list (* bool is verbosity *) + ; compile_file: (string * bool) option (* bool is verbosity *) ; compilation_output_name : string option ; vio_checking : bool @@ -32,7 +32,7 @@ type t = let default = { compilation_mode = BuildVo - ; compile_list = [] + ; compile_file = None ; compilation_output_name = None ; vio_checking = false @@ -62,17 +62,13 @@ let error_missing_arg s = prerr_endline "See -help for the syntax of supported options"; exit 1 -let check_compilation_output_name_consistency args = - match args.compilation_output_name, args.compile_list with - | Some _, _::_::_ -> - prerr_endline ("Error: option -o is not valid when more than one"); - prerr_endline ("file have to be compiled") - | _ -> () +let arg_error msg = CErrors.user_err msg let is_dash_argument s = String.length s > 0 && s.[0] = '-' let add_compile ?echo copts s = - if is_dash_argument s then (prerr_endline ("Unknown option " ^ s); exit 1); + if is_dash_argument s then + arg_error Pp.(str "Unknown option " ++ str s); (* make the file name explicit; needed not to break up Coq loadpath stuff. *) let echo = Option.default copts.echo echo in let s = @@ -81,7 +77,14 @@ let add_compile ?echo copts s = then concat current_dir_name s else s in - { copts with compile_list = (s,echo) :: copts.compile_list } + { copts with compile_file = Some (s,echo) } + +let add_compile ?echo copts v_file = + match copts.compile_file with + | Some _ -> + arg_error Pp.(str "More than one file to compile: " ++ str v_file) + | None -> + add_compile ?echo copts v_file let add_vio_task opts f = { opts with vio_tasks = f :: opts.vio_tasks } @@ -230,14 +233,12 @@ let parse arglist : t = try let opts, extra = parse default in let args = List.fold_left add_compile opts extra in - check_compilation_output_name_consistency args; args with any -> fatal_error any let parse args = let opts = parse args in { opts with - compile_list = List.rev opts.compile_list - ; vio_tasks = List.rev opts.vio_tasks + vio_tasks = List.rev opts.vio_tasks ; vio_files = List.rev opts.vio_files } diff --git a/toplevel/coqcargs.mli b/toplevel/coqcargs.mli index 905250e363..96895568ea 100644 --- a/toplevel/coqcargs.mli +++ b/toplevel/coqcargs.mli @@ -27,7 +27,7 @@ type compilation_mode = BuildVo | BuildVio | Vio2Vo | BuildVos | BuildVok type t = { compilation_mode : compilation_mode - ; compile_list: (string * bool) list (* bool is verbosity *) + ; compile_file: (string * bool) option (* bool is verbosity *) ; compilation_output_name : string option ; vio_checking : bool diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 32e942f0d0..bb44d9cdee 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -18,19 +18,17 @@ let () = at_exit flush_all let ( / ) = Filename.concat -let get_version_date () = +let get_version () = try let ch = open_in (Envars.coqlib () / "revision") in let ver = input_line ch in let rev = input_line ch in let () = close_in ch in - (ver,rev) - with e when CErrors.noncritical e -> - (Coq_config.version,Coq_config.date) + Printf.sprintf "%s (%s)" ver rev + with _ -> Coq_config.version let print_header () = - let (ver,rev) = get_version_date () in - Feedback.msg_info (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")"); + Feedback.msg_info (str "Welcome to Coq " ++ str (get_version ())); flush_all () diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index cc59a96834..f600432c80 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -193,48 +193,48 @@ let build_beq_scheme mode kn = let create_input c = let myArrow u v = mkArrow u Sorts.Relevant (lift 1 v) and eqName = function - | Name s -> Id.of_string ("eq_"^(Id.to_string s)) - | Anonymous -> Id.of_string "eq_A" + | Name s -> Id.of_string ("eq_"^(Id.to_string s)) + | Anonymous -> Id.of_string "eq_A" in let ext_rel_list = Context.Rel.to_extended_list mkRel 0 lnamesparrec in - let lift_cnt = ref 0 in - let eqs_typ = List.map (fun aa -> - let a = lift !lift_cnt aa in - incr lift_cnt; - myArrow a (myArrow a (bb ())) - ) ext_rel_list in - - let eq_input = List.fold_left2 - ( fun a b decl -> (* mkLambda(n,b,a) ) *) - (* here I leave the Naming thingy so that the type of + let lift_cnt = ref 0 in + let eqs_typ = List.map (fun aa -> + let a = lift !lift_cnt aa in + incr lift_cnt; + myArrow a (myArrow a (bb ())) + ) ext_rel_list in + + let eq_input = List.fold_left2 + ( fun a b decl -> (* mkLambda(n,b,a) ) *) + (* here I leave the Naming thingy so that the type of the function is more readable for the user *) - mkNamedLambda (map_annot eqName (RelDecl.get_annot decl)) b a ) - c (List.rev eqs_typ) lnamesparrec - in - List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *) - (* Same here , hoping the auto renaming will do something good ;) *) - let x = map_annot - (function Name s -> s | Anonymous -> Id.of_string "A") - (RelDecl.get_annot decl) - in - mkNamedLambda x (RelDecl.get_type decl) a) eq_input lnamesparrec - in - let make_one_eq cur = - let u = Univ.Instance.empty in - let ind = (kn,cur),u (* FIXME *) in - (* current inductive we are working on *) - let cur_packet = mib.mind_packets.(snd (fst ind)) in - (* Inductive toto : [rettyp] := *) - let rettyp = Inductive.type_of_inductive ((mib,cur_packet),u) in - (* split rettyp in a list without the non rec params and the last -> + mkNamedLambda (map_annot eqName (RelDecl.get_annot decl)) b a ) + c (List.rev eqs_typ) lnamesparrec + in + List.fold_left (fun a decl ->(* mkLambda(n,t,a)) eq_input rel_list *) + (* Same here , hoping the auto renaming will do something good ;) *) + let x = map_annot + (function Name s -> s | Anonymous -> Id.of_string "A") + (RelDecl.get_annot decl) + in + mkNamedLambda x (RelDecl.get_type decl) a) eq_input lnamesparrec + in + let make_one_eq cur = + let u = Univ.Instance.empty in + let ind = (kn,cur),u (* FIXME *) in + (* current inductive we are working on *) + let cur_packet = mib.mind_packets.(snd (fst ind)) in + (* Inductive toto : [rettyp] := *) + let rettyp = Inductive.type_of_inductive ((mib,cur_packet),u) in + (* split rettyp in a list without the non rec params and the last -> e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *) - let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in + let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in (* give a type A, this function tries to find the equality on A declared previously *) (* nlist = the number of args (A , B , ... ) eqA = the de Bruijn index of the first eq param ndx = how much to translate due to the 2nd Case - *) + *) let compute_A_equality rel_list nlist eqA ndx t = let lifti = ndx in let rec aux c = @@ -243,47 +243,47 @@ let build_beq_scheme mode kn = match Constr.kind c with | Rel x -> mkRel (x-nlist+ndx) | Var x -> - (* Support for working in a context with "eq_x : x -> x -> bool" *) - let eid = Id.of_string ("eq_"^(Id.to_string x)) in - let () = - try ignore (Environ.lookup_named eid env) - with Not_found -> raise (ParameterWithoutEquality (GlobRef.VarRef x)) - in - mkVar eid + (* Support for working in a context with "eq_x : x -> x -> bool" *) + let eid = Id.of_string ("eq_"^(Id.to_string x)) in + let () = + try ignore (Environ.lookup_named eid env) + with Not_found -> raise (ParameterWithoutEquality (GlobRef.VarRef x)) + in + mkVar eid | Cast (x,_,_) -> aux (Term.applist (x,a)) | App _ -> assert false | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> - if Environ.QMutInd.equal env kn kn' then mkRel(eqA-nlist-i+nb_ind-1) - else begin - try - let eq = match lookup_scheme (!beq_scheme_kind_aux()) ind' with - | Some c -> mkConst c - | None -> assert false - in - let eqa = Array.of_list @@ List.map aux a in - let args = - Array.append - (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in - if Int.equal (Array.length args) 0 then eq - else mkApp (eq, args) - with Not_found -> raise(EqNotFound (ind', fst ind)) - end + if Environ.QMutInd.equal env kn kn' then mkRel(eqA-nlist-i+nb_ind-1) + else begin + try + let eq = match lookup_scheme (!beq_scheme_kind_aux()) ind' with + | Some c -> mkConst c + | None -> assert false + in + let eqa = Array.of_list @@ List.map aux a in + let args = + Array.append + (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in + if Int.equal (Array.length args) 0 then eq + else mkApp (eq, args) + with Not_found -> raise(EqNotFound (ind', fst ind)) + end | Sort _ -> raise InductiveWithSort | Prod _ -> raise InductiveWithProduct | Lambda _-> raise (EqUnknown "abstraction") | LetIn _ -> raise (EqUnknown "let-in") | Const (kn, u) -> - (match Environ.constant_opt_value_in env (kn, u) with - | Some c -> aux (Term.applist (c,a)) - | None -> - (* Support for working in a context with "eq_x : x -> x -> bool" *) - (* Needs Hints, see test suite *) - let eq_lbl = Label.make ("eq_" ^ Label.to_string (Constant.label kn)) in - let kneq = Constant.change_label kn eq_lbl in - if Environ.mem_constant kneq env then - let _ = Environ.constant_opt_value_in env (kneq, u) in - Term.applist (mkConst kneq,a) - else raise (ParameterWithoutEquality (GlobRef.ConstRef kn))) + (match Environ.constant_opt_value_in env (kn, u) with + | Some c -> aux (Term.applist (c,a)) + | None -> + (* Support for working in a context with "eq_x : x -> x -> bool" *) + (* Needs Hints, see test suite *) + let eq_lbl = Label.make ("eq_" ^ Label.to_string (Constant.label kn)) in + let kneq = Constant.change_label kn eq_lbl in + if Environ.mem_constant kneq env then + let _ = Environ.constant_opt_value_in env (kneq, u) in + Term.applist (mkConst kneq,a) + else raise (ParameterWithoutEquality (GlobRef.ConstRef kn))) | Proj _ -> raise (EqUnknown "projection") | Construct _ -> raise (EqUnknown "constructor") | Case _ -> raise (EqUnknown "match") @@ -293,100 +293,112 @@ let build_beq_scheme mode kn = | Evar _ -> raise (EqUnknown "existential variable") | Int _ -> raise (EqUnknown "int") | Float _ -> raise (EqUnknown "float") - | Array _ -> raise (EqUnknown "array") - in + | Array _ -> raise (EqUnknown "array") + in aux t - in - (* construct the predicate for the Case part*) - let do_predicate rel_list n = - List.fold_left (fun a b -> mkLambda(make_annot Anonymous Sorts.Relevant,b,a)) - (mkLambda (make_annot Anonymous Sorts.Relevant, - mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1), - (bb ()))) - (List.rev rettyp_l) in - (* make_one_eq *) - (* do the [| C1 ... => match Y with ... end + in + (* construct the predicate for the Case part*) + let do_predicate rel_list n = + List.fold_left (fun a b -> mkLambda(make_annot Anonymous Sorts.Relevant,b,a)) + (mkLambda (make_annot Anonymous Sorts.Relevant, + mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1), + (bb ()))) + (List.rev rettyp_l) in + (* make_one_eq *) + (* do the [| C1 ... => match Y with ... end ... Cn => match Y with ... end |] part *) let rci = Sorts.Relevant in (* TODO relevance *) let ci = make_case_info env (fst ind) rci MatchStyle in - let constrs n = get_constructors env (make_ind_family (ind, - Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt)) in + let constrs n = + let params = Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt in + get_constructors env (make_ind_family (ind, params)) + in let constrsi = constrs (3+nparrec) in let n = Array.length constrsi in - let ar = Array.make n (ff ()) in - for i=0 to n-1 do - let nb_cstr_args = List.length constrsi.(i).cs_args in - let ar2 = Array.make n (ff ()) in - let constrsj = constrs (3+nparrec+nb_cstr_args) in - for j=0 to n-1 do - if Int.equal i j then - ar2.(j) <- let cc = (match nb_cstr_args with - | 0 -> tt () - | _ -> let eqs = Array.make nb_cstr_args (tt ()) in - for ndx = 0 to nb_cstr_args-1 do - let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in - let eqA = compute_A_equality rel_list - nparrec - (nparrec+3+2*nb_cstr_args) - (nb_cstr_args+ndx+1) - cc - in - Array.set eqs ndx - (mkApp (eqA, - [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|] - )) - done; - Array.fold_left - (fun a b -> mkApp (andb(),[|b;a|])) - (eqs.(0)) - (Array.sub eqs 1 (nb_cstr_args - 1)) - ) - in - (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) cc - (constrsj.(j).cs_args) - ) - else ar2.(j) <- (List.fold_left (fun a decl -> - mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) (ff ()) (constrsj.(j).cs_args) ) - done; - - ar.(i) <- (List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) - (mkCase (Inductive.contract_case env ((ci,do_predicate rel_list nb_cstr_args, - NoInvert, mkVar (Id.of_string "Y") ,ar2)))) - (constrsi.(i).cs_args)) - done; - mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1)) ( - mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2)) ( - mkCase (Inductive.contract_case env (ci, do_predicate rel_list 0,NoInvert,mkVar (Id.of_string "X"),ar)))) - in (* build_beq_scheme *) - let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and - types = Array.make nb_ind mkSet and - cores = Array.make nb_ind mkSet in - let u = Univ.Instance.empty in - for i=0 to (nb_ind-1) do - names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant; - types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0) Sorts.Relevant - (mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ())); - let c = make_one_eq i in - cores.(i) <- c; - done; - (Array.init nb_ind (fun i -> - let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in - if not (Sorts.family_leq InSet kelim) then - raise (NonSingletonProp (kn,i)); - let fix = match mib.mind_finite with - | CoFinite -> - raise NoDecidabilityCoInductive; - | Finite -> - mkFix (((Array.make nb_ind 0),i),(names,types,cores)) - | BiFinite -> - (* If the inductive type is not recursive, the fixpoint is + let ar = Array.init n (fun i -> + let nb_cstr_args = List.length constrsi.(i).cs_args in + let constrsj = constrs (3+nparrec+nb_cstr_args) in + let ar2 = Array.init n (fun j -> + if Int.equal i j then + let cc = match nb_cstr_args with + | 0 -> tt () + | _ -> + let eqs = Array.init nb_cstr_args (fun ndx -> + let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in + let eqA = compute_A_equality rel_list + nparrec + (nparrec+3+2*nb_cstr_args) + (nb_cstr_args+ndx+1) + cc + in + mkApp (eqA, [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|])) + in + Array.fold_left + (fun a b -> mkApp (andb(),[|b;a|])) + eqs.(0) + (Array.sub eqs 1 (nb_cstr_args - 1)) + in + List.fold_left (fun a decl -> + mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) + cc + constrsj.(j).cs_args + else + List.fold_left (fun a decl -> + mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) + (ff ()) + (constrsj.(j).cs_args)) + in + let pred = EConstr.of_constr (do_predicate rel_list nb_cstr_args) in + let case = + simple_make_case_or_project env (Evd.from_env env) + ci pred NoInvert (EConstr.mkVar (Id.of_string "Y")) + (EConstr.of_constr_array ar2) + in + List.fold_left (fun a decl -> mkLambda (RelDecl.get_annot decl, RelDecl.get_type decl, a)) + (EConstr.Unsafe.to_constr case) + (constrsi.(i).cs_args)) + in + let pred = EConstr.of_constr (do_predicate rel_list 0) in + let case = + simple_make_case_or_project env (Evd.from_env env) + ci pred NoInvert (EConstr.mkVar (Id.of_string "X")) + (EConstr.of_constr_array ar) + in + mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1)) ( + mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2)) ( + (EConstr.Unsafe.to_constr case))) + in (* build_beq_scheme *) + + let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and + types = Array.make nb_ind mkSet and + cores = Array.make nb_ind mkSet in + let u = Univ.Instance.empty in + for i=0 to (nb_ind-1) do + names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant; + types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0) Sorts.Relevant + (mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ())); + let c = make_one_eq i in + cores.(i) <- c; + done; + let res = Array.init nb_ind (fun i -> + let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in + if not (Sorts.family_leq InSet kelim) then + raise (NonSingletonProp (kn,i)); + let fix = match mib.mind_finite with + | CoFinite -> + raise NoDecidabilityCoInductive; + | Finite -> + mkFix (((Array.make nb_ind 0),i),(names,types,cores)) + | BiFinite -> + (* If the inductive type is not recursive, the fixpoint is not used, so let's replace it with garbage *) - let subst = List.init nb_ind (fun _ -> mkProp) in - Vars.substl subst cores.(i) - in - create_input fix), - UState.from_env (Global.env ())) + let subst = List.init nb_ind (fun _ -> mkProp) in + Vars.substl subst cores.(i) + in + create_input fix) + in + res, UState.from_env (Global.env ()) let beq_scheme_kind = declare_mutual_scheme_object "_beq" diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index b3ffb864f2..2e48313630 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -111,6 +111,10 @@ let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt = let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in evd, (c, tyopt), imps +let definition_using env evd ~body ~types ~using = + let terms = Option.List.cons types [body] in + Option.map (fun using -> Proof_using.definition_using env evd ~using ~terms) using + let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl red_option c ctypopt = let program_mode = false in let env = Global.env() in @@ -120,11 +124,7 @@ let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl r let evd, (body, types), impargs = interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt in - let using = using |> Option.map (fun expr -> - let terms = body :: match types with Some x -> [x] | None -> [] in - let l = Proof_using.process_expr (Global.env()) evd expr terms in - Names.Id.Set.(List.fold_right add l empty)) - in + let using = definition_using env evd ~body ~types ~using in let kind = Decls.IsDefinition kind in let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly ?typing_flags () in @@ -141,11 +141,7 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ?typing_flags ~kind ?usin let evd, (body, types), impargs = interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt in - let using = using |> Option.map (fun expr -> - let terms = body :: match types with Some x -> [x] | None -> [] in - let l = Proof_using.process_expr (Global.env()) evd expr terms in - Names.Id.Set.(List.fold_right add l empty)) - in + let using = definition_using env evd ~body ~types ~using in let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in let pm, _ = let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 0cf0b07822..0f817ffbd1 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -259,13 +259,10 @@ let build_recthms ~indexes ?using fixnames fixtypes fiximps = in let thms = List.map3 (fun name typ (ctx,impargs,_) -> - let using = using |> Option.map (fun expr -> - let terms = [EConstr.of_constr typ] in - let env = Global.env() in - let sigma = Evd.from_env env in - let l = Proof_using.process_expr env sigma expr terms in - Names.Id.Set.(List.fold_right add l empty)) - in + let env = Global.env() in + let evd = Evd.from_env env in + let terms = [EConstr.of_constr typ] in + let using = Option.map (fun using -> Proof_using.definition_using env evd ~using ~terms) using in let args = List.map Context.Rel.Declaration.get_name ctx in Declare.CInfo.make ~name ~typ ~args ~impargs ?using () ) fixnames fixtypes fiximps diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 3c4a651cf5..0651f3330e 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -259,10 +259,9 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?typing_flags ?using r let evars, _, evars_def, evars_typ = RetrieveObl.retrieve_obligations env recname sigma 0 def typ in - let using = using |> Option.map (fun expr -> + let using = let terms = List.map EConstr.of_constr [evars_def; evars_typ] in - let l = Proof_using.process_expr env sigma expr terms in - Names.Id.Set.(List.fold_right add l empty)) + Option.map (fun using -> Proof_using.definition_using env sigma ~using ~terms) using in let uctx = Evd.evar_universe_context sigma in let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in @@ -294,11 +293,8 @@ let do_program_recursive ~pm ~scope ~poly ?typing_flags ?using fixkind fixl = let evd = nf_evar_map_undefined evd in let collect_evars name def typ impargs = (* Generalize by the recursive prototypes *) - let using = using |> Option.map (fun expr -> - let terms = [def; typ] in - let l = Proof_using.process_expr env evd expr terms in - Names.Id.Set.(List.fold_right add l empty)) - in + let terms = [def; typ] in + let using = Option.map (fun using -> Proof_using.definition_using env evd ~using ~terms) using in let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in let evm = collect_evars_of_term evd def typ in diff --git a/vernac/declare.ml b/vernac/declare.ml index 48aa329e5e..607ba18a95 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -57,7 +57,7 @@ module CInfo = struct (** Names to pre-introduce *) ; impargs : Impargs.manual_implicits (** Explicitily declared implicit arguments *) - ; using : Names.Id.Set.t option + ; using : Proof_using.t option (** Explicit declaration of section variables used by the constant *) } @@ -1478,11 +1478,10 @@ let start_mutual_with_initialization ~info ~cinfo ~mutual_info sigma snl = let get_used_variables pf = pf.using let get_universe_decl pf = pf.pinfo.Proof_info.info.Info.udecl -let set_used_variables ps l = +let set_used_variables ps ~using = let open Context.Named.Declaration in let env = Global.env () in - let ids = List.fold_right Id.Set.add l Id.Set.empty in - let ctx = Environ.keep_hyps env ids in + let ctx = Environ.keep_hyps env using in let ctx_set = List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in let vars_of = Environ.global_vars_set in diff --git a/vernac/declare.mli b/vernac/declare.mli index 37a61cc4f0..81558e6f6b 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -79,7 +79,7 @@ module CInfo : sig -> typ:'constr -> ?args:Name.t list -> ?impargs:Impargs.manual_implicits - -> ?using:Names.Id.Set.t + -> ?using:Proof_using.t -> unit -> 'constr t @@ -244,7 +244,7 @@ module Proof : sig (** Sets the section variables assumed by the proof, returns its closure * (w.r.t. type dependencies and let-ins covered by it) *) - val set_used_variables : t -> Names.Id.t list -> Constr.named_context * t + val set_used_variables : t -> using:Proof_using.t -> Constr.named_context * t (** Gets the set of variables declared to be used by the proof. None means no "Proof using" or #[using] was given *) diff --git a/vernac/library.ml b/vernac/library.ml index 8a9b1fd68d..cc9e3c3c44 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -155,17 +155,13 @@ let library_is_loaded dir = let register_loaded_library m = let libname = m.libsum_name in - let link () = - let dirname = Filename.dirname (library_full_filename libname) in - let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in - let f = prefix ^ "cmo" in - let f = Dynlink.adapt_filename f in - Nativelib.link_library ~prefix ~dirname ~basename:f - in let rec aux = function | [] -> - let () = if Flags.get_native_compiler () then link () in - [libname] + if Flags.get_native_compiler () then begin + let dirname = Filename.dirname (library_full_filename libname) in + Nativelib.enable_library dirname libname + end; + [libname] | m'::_ as l when DirPath.equal m' libname -> l | m'::l' -> m' :: aux l' in libraries_loaded_list := aux !libraries_loaded_list; diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index bdb0cabacf..01e7b7cc3d 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -64,6 +64,12 @@ let process_expr env sigma e ty = let s = Id.Set.union v_ty (process_expr env sigma e v_ty) in Id.Set.elements s +type t = Names.Id.Set.t + +let definition_using env evd ~using ~terms = + let l = process_expr env evd using terms in + Names.Id.Set.(List.fold_right add l empty) + let name_set id expr = known_names := (id,expr) :: !known_names let minimize_hyps env ids = @@ -91,13 +97,14 @@ let remove_ids_and_lets env s ids = let record_proof_using expr = Aux_file.record_in_aux "suggest_proof_using" expr +let debug_proof_using = CDebug.create ~name:"proof-using" () + (* Variables in [skip] come from after the definition, so don't count for "All". Used in the variable case since the env contains the variable itself. *) let suggest_common env ppid used ids_typ skip = let module S = Id.Set in let open Pp in - let print x = Feedback.msg_debug x in let pr_set parens s = let wrap ppcmds = if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")" @@ -111,13 +118,13 @@ let suggest_common env ppid used ids_typ skip = in let all = S.diff all skip in let fwd_typ = close_fwd env (Evd.from_env env) ids_typ in - if !Flags.debug then begin - print (str "All " ++ pr_set false all); - print (str "Type " ++ pr_set false ids_typ); - print (str "needed " ++ pr_set false needed); - print (str "all_needed " ++ pr_set false all_needed); - print (str "Type* " ++ pr_set false fwd_typ); - end; + let () = debug_proof_using (fun () -> + str "All " ++ pr_set false all ++ fnl() ++ + str "Type " ++ pr_set false ids_typ ++ fnl() ++ + str "needed " ++ pr_set false needed ++ fnl() ++ + str "all_needed " ++ pr_set false all_needed ++ fnl() ++ + str "Type* " ++ pr_set false fwd_typ) + in let valid_exprs = ref [] in let valid e = valid_exprs := e :: !valid_exprs in if S.is_empty needed then valid (str "Type"); diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli index 93dbd33ae4..60db4d60e6 100644 --- a/vernac/proof_using.mli +++ b/vernac/proof_using.mli @@ -10,10 +10,17 @@ (** Utility code for section variables handling in Proof using... *) -val process_expr : - Environ.env -> Evd.evar_map -> - Vernacexpr.section_subset_expr -> EConstr.types list -> - Names.Id.t list +(** At some point it would be good to make this abstract *) +type t = Names.Id.Set.t + +(** Process a [using] expression in definitions to provide the list of + used terms *) +val definition_using + : Environ.env + -> Evd.evar_map + -> using:Vernacexpr.section_subset_expr + -> terms:EConstr.constr list + -> t val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 42ba63903d..38ca836b32 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -563,19 +563,19 @@ let program_inference_hook env sigma ev = user_err Pp.(str "The statement obligations could not be resolved \ automatically, write a statement definition first.") -let vernac_set_used_variables ~pstate e : Declare.Proof.t = +let vernac_set_used_variables ~pstate using : Declare.Proof.t = let env = Global.env () in let sigma, _ = Declare.Proof.get_current_context pstate in let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in - let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in - let l = Proof_using.process_expr env sigma e tys in + let terms = List.map snd (initial_goals (Declare.Proof.get pstate)) in + let using = Proof_using.definition_using env sigma ~using ~terms in let vars = Environ.named_context env in - List.iter (fun id -> - if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then - user_err ~hdr:"vernac_set_used_variables" - (str "Unknown variable: " ++ Id.print id)) - l; - let _, pstate = Declare.Proof.set_used_variables pstate l in + Names.Id.Set.iter (fun id -> + if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then + user_err ~hdr:"vernac_set_used_variables" + (str "Unknown variable: " ++ Id.print id)) + using; + let _, pstate = Declare.Proof.set_used_variables pstate ~using in pstate let vernac_set_used_variables_opt ?using pstate = @@ -1645,6 +1645,13 @@ let () = optwrite = CWarnings.set_flags } let () = + declare_string_option + { optdepr = false; + optkey = ["Debug"]; + optread = CDebug.get_flags; + optwrite = CDebug.set_flags } + +let () = declare_bool_option { optdepr = false; optkey = ["Guard"; "Checking"]; @@ -1710,9 +1717,9 @@ let vernac_set_append_option ~locality key s = let vernac_set_option ~locality table v = match v with | OptionSetString s -> - (* We make a special case for warnings because appending is their - natural semantics *) - if CString.List.equal table ["Warnings"] then + (* We make a special case for warnings and debug flags because appending is + their natural semantics *) + if CString.List.equal table ["Warnings"] || CString.List.equal table ["Debug"] then vernac_set_append_option ~locality table s else let (last, prefix) = List.sep_last table in |