diff options
94 files changed, 1730 insertions, 1588 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 68bb24ac77..8b79dbf810 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -697,6 +697,7 @@ library:ci-verdi-raft: library:ci-vst: extends: .ci-template-flambda + allow_failure: true # Plugins are by definition the projects that depend on Coq's ML API diff --git a/Makefile.build b/Makefile.build index 9e0a402730..2bb32dc6c2 100644 --- a/Makefile.build +++ b/Makefile.build @@ -570,8 +570,8 @@ bin/votour.byte: $(VOTOURCMO) $(LIBCOQRUN) ########################################################################### CSDPCERTCMO:=clib/clib.cma $(addprefix plugins/micromega/, \ - micromega.cmo mutils.cmo \ - sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) + micromega.cmo numCompat.cmo mutils.cmo \ + sos_types.cmo sos_lib.cmo sos.cmo csdpcert.cmo ) $(CSDPCERT): $(call bestobj, $(CSDPCERTCMO)) $(SHOW)'OCAMLBEST -o $@' diff --git a/Makefile.doc b/Makefile.doc index 1249555cd7..5aa1ae9850 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -38,10 +38,11 @@ SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(WIN_CURDIR)" else SPHINXENV:=COQBIN="$(CURDIR)/bin/" COQLIB="$(CURDIR)" endif -SPHINXOPTS= -j4 SPHINXWARNERROR ?= 1 ifeq ($(SPHINXWARNERROR),1) -SPHINXOPTS += -W +SPHINXOPTS= -W +else +SPHINXOPTS= endif SPHINXBUILD= sphinx-build SPHINXBUILDDIR= doc/sphinx/_build diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 62e732ce69..c4c6d9bb4f 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -20,7 +20,7 @@ exception InductiveMismatch of MutInd.t * string let check mind field b = if not b then raise (InductiveMismatch (mind,field)) -let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = +let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = let open Entries in let nparams = List.length mb.mind_params_ctxt in (* include letins *) let mind_entry_record = match mb.mind_record with @@ -33,39 +33,27 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = inductive types. The set of monomorphic constraints is already part of the graph at that point, but we need to emulate a broken bound variable mechanism for template inductive types. *) - let fold accu ind = match ind.mind_arity with - | RegularArity _ -> accu - | TemplateArity ar -> - match accu with - | None -> Some ar.template_context - | Some ctx -> - (* Ensure that all template contexts agree. This is enforced by the - kernel. *) - let () = check mind "mind_arity" (ContextSet.equal ctx ar.template_context) in - Some ctx - in - let univs = match Array.fold_left fold None mb.mind_packets with + let univs = match mb.mind_template with | None -> ContextSet.empty - | Some ctx -> ctx + | Some ctx -> ctx.template_context in Monomorphic_entry univs | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx) in let mind_entry_inds = Array.map_to_list (fun ind -> - let mind_entry_arity, mind_entry_template = match ind.mind_arity with + let mind_entry_arity = match ind.mind_arity with | RegularArity ar -> let ctx, arity = Term.decompose_prod_n_assum nparams ar.mind_user_arity in ignore ctx; (* we will check that the produced user_arity is equal to the input *) - arity, false + arity | TemplateArity ar -> let ctx = ind.mind_arity_ctxt in let ctx = List.firstn (List.length ctx - nparams) ctx in - Term.mkArity (ctx, Sorts.sort_of_univ ar.template_level), true + Term.mkArity (ctx, Sorts.sort_of_univ ar.template_level) in { mind_entry_typename = ind.mind_typename; mind_entry_arity; - mind_entry_template; mind_entry_consnames = Array.to_list ind.mind_consnames; mind_entry_lc = Array.map_to_list (fun c -> let ctx, c = Term.decompose_prod_n_assum nparams c in @@ -75,12 +63,19 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry = }) mb.mind_packets in + let check_template ind = match ind.mind_arity with + | RegularArity _ -> false + | TemplateArity _ -> true + in + let mind_entry_template = Array.exists check_template mb.mind_packets in + let () = if mind_entry_template then assert (Array.for_all check_template mb.mind_packets) in { mind_entry_record; mind_entry_finite = mb.mind_finite; mind_entry_params = mb.mind_params_ctxt; mind_entry_inds; mind_entry_universes; + mind_entry_template; mind_entry_cumulative= Option.has_some mb.mind_variance; mind_entry_private = mb.mind_private; } @@ -89,13 +84,18 @@ let check_arity env ar1 ar2 = match ar1, ar2 with | RegularArity ar, RegularArity {mind_user_arity;mind_sort} -> Constr.equal ar.mind_user_arity mind_user_arity && Sorts.equal ar.mind_sort mind_sort - | TemplateArity ar, TemplateArity {template_param_levels;template_level;template_context} -> - List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels && - ContextSet.equal template_context ar.template_context && + | TemplateArity ar, TemplateArity {template_level} -> UGraph.check_leq (universes env) template_level ar.template_level (* template_level is inferred by indtypes, so functor application can produce a smaller one *) | (RegularArity _ | TemplateArity _), _ -> assert false +let check_template ar1 ar2 = match ar1, ar2 with +| None, None -> true +| Some ar, Some {template_context; template_param_levels} -> + List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels && + ContextSet.equal template_context ar.template_context +| None, Some _ | Some _, None -> false + let check_kelim k1 k2 = Sorts.family_leq k1 k2 (* Use [eq_ind_chk] because when we rebuild the recargs we have lost @@ -157,10 +157,10 @@ let check_same_record r1 r2 = match r1, r2 with | (NotRecord | FakeRecord | PrimRecord _), _ -> false let check_inductive env mind mb = - let entry = to_entry mind mb in + let entry = to_entry mb in let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps; mind_nparams; mind_nparams_rec; mind_params_ctxt; - mind_universes; mind_variance; mind_sec_variance; + mind_universes; mind_template; mind_variance; mind_sec_variance; mind_private; mind_typing_flags; } = (* Locally set typing flags for further typechecking *) @@ -191,6 +191,7 @@ let check_inductive env mind mb = check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt); ignore mind_universes; (* Indtypes did the necessary checking *) + check "mind_template" (check_template mb.mind_template mind_template); check "mind_variance" (Option.equal (Array.equal Univ.Variance.equal) mb.mind_variance mind_variance); check "mind_sec_variance" (Option.is_empty mind_sec_variance); diff --git a/checker/checkTypes.mli b/checker/checkTypes.mli index ac9ea2fb31..9ef6ff017c 100644 --- a/checker/checkTypes.mli +++ b/checker/checkTypes.mli @@ -17,4 +17,4 @@ open Environ (*s Typing functions (not yet tagged as safe) *) val check_polymorphic_arity : - env -> rel_context -> template_arity -> unit + env -> rel_context -> template_universes -> unit diff --git a/checker/values.ml b/checker/values.ml index ed730cff8e..cba96e6636 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -227,8 +227,11 @@ let v_oracle = v_pred v_cst; |] -let v_pol_arity = - v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ;v_context_set|] +let v_template_arity = + v_tuple "template_arity" [|v_univ|] + +let v_template_universes = + v_tuple "template_universes" [|List(Opt v_level);v_context_set|] let v_primitive = v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *) @@ -265,7 +268,7 @@ let v_mono_ind_arity = v_tuple "monomorphic_inductive_arity" [|v_constr;v_sort|] let v_ind_arity = v_sum "inductive_arity" 0 - [|[|v_mono_ind_arity|];[|v_pol_arity|]|] + [|[|v_mono_ind_arity|];[|v_template_arity|]|] let v_one_ind = v_tuple "one_inductive_body" [|v_id; @@ -301,6 +304,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body" Int; v_rctxt; v_univs; (* universes *) + Opt v_template_universes; Opt (Array v_variance); Opt (Array v_variance); Opt v_bool; diff --git a/clib/cStack.ml b/clib/cStack.ml deleted file mode 100644 index 0432e29fad..0000000000 --- a/clib/cStack.ml +++ /dev/null @@ -1,44 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -exception Empty = Stack.Empty - -type 'a t = { - mutable stack : 'a list; -} - -let create () = { stack = [] } - -let push x s = s.stack <- x :: s.stack - -let pop = function - | { stack = [] } -> raise Stack.Empty - | { stack = x::xs } as s -> s.stack <- xs; x - -let top = function - | { stack = [] } -> raise Stack.Empty - | { stack = x::_ } -> x - -let to_list { stack = s } = s - -let find f s = List.find f (to_list s) - -let find_map f s = CList.find_map f s.stack - -let fold_until f accu s = CList.fold_left_until f accu s.stack - -let is_empty { stack = s } = s = [] - -let iter f { stack = s } = List.iter f s - -let clear s = s.stack <- [] - -let length { stack = s } = List.length s - diff --git a/clib/cStack.mli b/clib/cStack.mli deleted file mode 100644 index de802160e7..0000000000 --- a/clib/cStack.mli +++ /dev/null @@ -1,58 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Extended interface for OCaml stacks. *) - -type 'a t - -exception Empty -(** Alias for Stack.Empty. *) - -val create : unit -> 'a t -(** Create an empty stack. *) - -val push : 'a -> 'a t -> unit -(** Add an element to a stack. *) - -val find : ('a -> bool) -> 'a t -> 'a -(** Find the first element satisfying the predicate. - @raise Not_found it there is none. *) - -val is_empty : 'a t -> bool -(** Whether a stack is empty. *) - -val iter : ('a -> unit) -> 'a t -> unit -(** Iterate a function over elements, from the last added one. *) - -val clear : 'a t -> unit -(** Empty a stack. *) - -val length : 'a t -> int -(** Length of a stack. *) - -val pop : 'a t -> 'a -(** Remove and returns the first element of the stack. - @raise Empty if empty. *) - -val top : 'a t -> 'a -(** Remove the first element of the stack without modifying it. - @raise Empty if empty. *) - -val to_list : 'a t -> 'a list -(** Convert to a list. *) - -val find_map : ('a -> 'b option) -> 'a t -> 'b -(** Find the first element that returns [Some _]. - @raise Not_found it there is none. *) - -val fold_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a t -> 'c -(** Like CList.fold_left_until. - The stack is traversed from the top and is not altered. *) - diff --git a/clib/clib.mllib b/clib/clib.mllib index 5a2c9a9ce9..be3b5971be 100644 --- a/clib/clib.mllib +++ b/clib/clib.mllib @@ -9,7 +9,6 @@ CSet CMap CList CString -CStack Int Range @@ -33,7 +32,6 @@ Unionfind Dyn Store Exninfo -Backtrace IStream Terminal Monad diff --git a/default.nix b/default.nix index ae6a8d06e5..841bccb129 100644 --- a/default.nix +++ b/default.nix @@ -22,7 +22,7 @@ # a symlink to where Coq was installed. { pkgs ? import ./dev/nixpkgs.nix {} -, ocamlPackages ? pkgs.ocamlPackages +, ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_09 , buildIde ? true , buildDoc ? true , doInstallCheck ? true diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 7aa265cf90..f0dbe485f7 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -19,7 +19,7 @@ then elif [ -d "$PWD/_build/install/default/" ]; then # Dune build - export OCAMLPATH="$PWD/_build/install/default/lib/" + export OCAMLPATH="$PWD/_build/install/default/lib/:$OCAMLPATH" export COQBIN="$PWD/_build/install/default/bin" export COQLIB="$PWD/_build/install/default/lib/coq" CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" diff --git a/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh b/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh new file mode 100644 index 0000000000..f8871ae158 --- /dev/null +++ b/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh @@ -0,0 +1,18 @@ +if [ "$CI_PULL_REQUEST" = "11764" ] || [ "$CI_BRANCH" = "simplify-template" ]; then + + elpi_CI_REF="simplify-template" + elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi + + equations_CI_REF="simplify-template" + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + paramcoq_CI_REF="simplify-template" + paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq + + mtac2_CI_REF="simplify-template" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + + rewriter_CI_REF="simplify-template" + rewriter_CI_GITURL=https://github.com/ppedrot/rewriter + +fi diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index 54baaee1fe..b8a696ef21 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/8da81465c19fca393a3b17004c743e4d82a98e4f.tar.gz"; - sha256 = "1f3s27nrssfk413pszjhbs70wpap43bbjx2pf4zq5x2c1kd72l6y"; + url = "https://github.com/NixOS/nixpkgs/archive/34e41a91547e342f6fbc901929134b34000297eb.tar.gz"; + sha256 = "0mlqxim36xg8aj4r35mpcgqg27wy1dbbim9l1cpjl24hcy96v48w"; }) diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 89b4bda71a..0802b5d0b4 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -3,8 +3,8 @@ ============================= .. - README.rst is auto-generated from README.template.rst and the coqrst docs; - use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. + README.rst is auto-generated from README.template.rst and the coqrst/*.py files + (in particular coqdomain.py). Use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_. @@ -97,7 +97,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica ``.. cmd::`` :black_nib: A Coq command. Example:: - .. cmd:: Infix @string := @term1_extended {? ( {+, @syntax_modifier } ) } {? : @ident } + .. cmd:: Infix @string := @one_term {? ( {+, @syntax_modifier } ) } {? : @ident } This command is equivalent to :n:`…`. diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index c5e0007e78..5762967c36 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -3,8 +3,8 @@ ============================= .. - README.rst is auto-generated from README.template.rst and the coqrst docs; - use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. + README.rst is auto-generated from README.template.rst and the coqrst/*.py files + (in particular coqdomain.py). Use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_. diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 94ab6e789c..315c9d4a80 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -713,48 +713,119 @@ Definitions ~~~~~~~~~~~ The generalized rewriting tactic is based on a set of strategies that can be -combined to obtain custom rewriting procedures. Its set of strategies is based +combined to create custom rewriting procedures. Its set of strategies is based on the programmable rewriting strategies with generic traversals by Visser et al. :cite:`Luttik97specificationof` :cite:`Visser98`, which formed the core of the Stratego transformation language :cite:`Visser01`. Rewriting strategies -are applied using the tactic :n:`rewrite_strat @strategy` where :token:`strategy` is a -strategy expression. Strategies are defined inductively as described by the -following grammar: - -.. productionlist:: coq - strategy : `qualid` (lemma, left to right) - : <- `qualid` (lemma, right to left) - : fail (failure) - : id (identity) - : refl (reflexivity) - : progress `strategy` (progress) - : try `strategy` (try catch) - : `strategy` ; `strategy` (composition) - : choice `strategy` `strategy` (left_biased_choice) - : repeat `strategy` (one or more) - : any `strategy` (zero or more) - : subterm `strategy` (one subterm) - : subterms `strategy` (all subterms) - : innermost `strategy` (innermost first) - : outermost `strategy` (outermost first) - : bottomup `strategy` (bottom-up) - : topdown `strategy` (top-down) - : hints `ident` (apply hints from hint database) - : terms `term` ... `term` (any of the terms) - : eval `red_expr` (apply reduction) - : fold `term` (unify) - : ( `strategy` ) - -Actually a few of these are defined in term of the others using a +are applied using the tactic :n:`rewrite_strat @rewstrategy`. + +.. insertprodn rewstrategy rewstrategy + +.. prodn:: + rewstrategy ::= @one_term + | <- @one_term + | fail + | id + | refl + | progress @rewstrategy + | try @rewstrategy + | @rewstrategy ; @rewstrategy + | choice @rewstrategy @rewstrategy + | repeat @rewstrategy + | any @rewstrategy + | subterm @rewstrategy + | subterms @rewstrategy + | innermost @rewstrategy + | outermost @rewstrategy + | bottomup @rewstrategy + | topdown @rewstrategy + | hints @ident + | terms {* @one_term } + | eval @red_expr + | fold @one_term + | ( @rewstrategy ) + | old_hints @ident + +:n:`@one_term` + lemma, left to right + +:n:`<- @one_term` + lemma, right to left + +:n:`fail` + failure + +:n:`id` + identity + +:n:`refl` + reflexivity + +:n:`progress @rewstrategy` + progress + +:n:`try @rewstrategy` + try catch + +:n:`@rewstrategy ; @rewstrategy` + composition + +:n:`choice @rewstrategy @rewstrategy` + left_biased_choice + +:n:`repeat @rewstrategy` + one or more + +:n:`any @rewstrategy` + zero or more + +:n:`subterm @rewstrategy` + one subterm + +:n:`subterms @rewstrategy` + all subterms + +:n:`innermost @rewstrategy` + innermost first + +:n:`outermost @rewstrategy` + outermost first + +:n:`bottomup @rewstrategy` + bottom-up + +:n:`topdown @rewstrategy` + top-down + +:n:`hints @ident` + apply hints from hint database + +:n:`terms {* @one_term }` + any of the terms + +:n:`eval @red_expr` + apply reduction + +:n:`fold @term` + unify + +:n:`( @rewstrategy )` + to be documented + +:n:`old_hints @ident` + to be documented + + +A few of these are defined in terms of the others using a primitive fixpoint operator: -- :n:`try @strategy := choice @strategy id` -- :n:`any @strategy := fix @ident. try (@strategy ; @ident)` -- :n:`repeat @strategy := @strategy; any @strategy` -- :n:`bottomup @strategy := fix @ident. (choice (progress (subterms @ident)) @strategy) ; try @ident` -- :n:`topdown @strategy := fix @ident. (choice @strategy (progress (subterms @ident))) ; try @ident` -- :n:`innermost @strategy := fix @ident. (choice (subterm @ident) @strategy)` -- :n:`outermost @strategy := fix @ident. (choice @strategy (subterm @ident))` +- :n:`try @rewstrategy := choice @rewstrategy id` +- :n:`any @rewstrategy := fix @ident. try (@rewstrategy ; @ident)` +- :n:`repeat @rewstrategy := @rewstrategy; any @rewstrategy` +- :n:`bottomup @rewstrategy := fix @ident. (choice (progress (subterms @ident)) @rewstrategy) ; try @ident` +- :n:`topdown @rewstrategy := fix @ident. (choice @rewstrategy (progress (subterms @ident))) ; try @ident` +- :n:`innermost @rewstrategy := fix @ident. (choice (subterm @ident) @rewstrategy)` +- :n:`outermost @rewstrategy := fix @ident. (choice @rewstrategy (subterm @ident))` The basic control strategy semantics are straightforward: strategies are applied to subterms of the term to rewrite, starting from the root @@ -764,18 +835,18 @@ hand-side. Composition can be used to continue rewriting on the current subterm. The ``fail`` strategy always fails while the identity strategy succeeds without making progress. The reflexivity strategy succeeds, making progress using a reflexivity proof of rewriting. -``progress`` tests progress of the argument :token:`strategy` and fails if no +``progress`` tests progress of the argument :n:`@rewstrategy` and fails if no progress was made, while ``try`` always succeeds, catching failures. ``choice`` is left-biased: it will launch the first strategy and fall back on the second one in case of failure. One can iterate a strategy at least 1 time using ``repeat`` and at least 0 times using ``any``. -The ``subterm`` and ``subterms`` strategies apply their argument :token:`strategy` to +The ``subterm`` and ``subterms`` strategies apply their argument :n:`@rewstrategy` to respectively one or all subterms of the current term under consideration, left-to-right. ``subterm`` stops at the first subterm for -which :token:`strategy` made progress. The composite strategies ``innermost`` and ``outermost`` +which :n:`@rewstrategy` made progress. The composite strategies ``innermost`` and ``outermost`` perform a single innermost or outermost rewrite using their argument -:token:`strategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many +:n:`@rewstrategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many rewritings as possible, starting from the bottom or the top of the term. @@ -793,7 +864,7 @@ Usage ~~~~~ -.. tacn:: rewrite_strat @strategy {? in @ident } +.. tacn:: rewrite_strat @rewstrategy {? in @ident } :name: rewrite_strat Rewrite using the strategy s in hypothesis ident or the conclusion. diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index b007509b2e..1f33775a01 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -37,12 +37,13 @@ In addition to these user-defined classes, we have two built-in classes: * ``Funclass``, the class of functions; its objects are all the terms with a functional type, i.e. of form :g:`forall x:A,B`. -Formally, the syntax of classes is defined as: + .. insertprodn class class + + .. prodn:: + class ::= Funclass + | Sortclass + | @smart_qualid -.. productionlist:: - class: `qualid` - : Sortclass - : Funclass Coercions @@ -186,37 +187,12 @@ Declaring Coercions This defines :token:`ident` just like :n:`Let @ident := @term {? @type }`, and then declares :token:`ident` as a coercion between it source and its target. -Assumptions can be declared as coercions at declaration time. -This extends the grammar of assumptions from -Figure :ref:`vernacular` as follows: - -.. - FIXME: - \comindex{Variable \mbox{\rm (and coercions)}} - \comindex{Axiom \mbox{\rm (and coercions)}} - \comindex{Parameter \mbox{\rm (and coercions)}} - \comindex{Hypothesis \mbox{\rm (and coercions)}} - -.. productionlist:: - assumption : `assumption_token` `assums` . - assums : `simple_assums` - : (`simple_assums`) ... (`simple_assums`) - simple_assums : `ident` ... `ident` :[>] `term` - -If the extra ``>`` is present before the type of some assumptions, these -assumptions are declared as coercions. - -Similarly, constructors of inductive types can be declared as coercions at -definition time of the inductive type. This extends and modifies the -grammar of inductive types from Figure :ref:`vernacular` as follows: - -.. - FIXME: - \comindex{Inductive \mbox{\rm (and coercions)}} - \comindex{CoInductive \mbox{\rm (and coercions)}} - -Especially, if the extra ``>`` is present in a constructor -declaration, this constructor is declared as a coercion. +Some objects can be declared as coercions when they are defined. +This applies to :ref:`assumptions<gallina-assumptions>` and +constructors of :ref:`inductive types and record fields<gallina-inductive-definitions>`. +Use :n:`:>` instead of :n:`:` before the +:n:`@type` of the assumption to do so. See :n:`@of_type`. + .. cmd:: Identity Coercion @ident : @class >-> @class diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 1098aa75da..76174e32b5 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -300,70 +300,79 @@ following property: The syntax for adding a new ring is -.. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )} - - The :token:`ident` is not relevant. It is used just for error messages. The - :token:`term` is a proof that the ring signature satisfies the (semi-)ring +.. cmd:: Add Ring @ident : @one_term {? ( {+, @ring_mod } ) } + + .. insertprodn ring_mod ring_mod + + .. prodn:: + ring_mod ::= decidable @one_term + | abstract + | morphism @one_term + | constants [ @ltac_expr ] + | preprocess [ @ltac_expr ] + | postprocess [ @ltac_expr ] + | setoid @one_term @one_term + | sign @one_term + | power @one_term [ {+ @qualid } ] + | power_tac @one_term [ @ltac_expr ] + | div @one_term + | closed [ {+ @qualid } ] + + The :n:`@ident` is used only for error messages. The + :n:`@one_term` is a proof that the ring signature satisfies the (semi-)ring axioms. The optional list of modifiers is used to tailor the behavior - of the tactic. The following list describes their syntax and effects: - - .. productionlist:: coq - ring_mod : abstract | decidable `term` | morphism `term` - : setoid `term` `term` - : constants [ `tactic` ] - : preprocess [ `tactic` ] - : postprocess [ `tactic` ] - : power_tac `term` [ `tactic` ] - : sign `term` - : div `term` - - abstract + of the tactic. Here are their effects: + + :n:`abstract` declares the ring as abstract. This is the default. - decidable :n:`@term` + :n:`decidable @one_term` declares the ring as computational. The expression - :n:`@term` is the correctness proof of an equality test ``?=!`` + :n:`@one_term` is the correctness proof of an equality test ``?=!`` (which should be evaluable). Its type should be of the form ``forall x y, x ?=! y = true → x == y``. - morphism :n:`@term` + :n:`morphism @one_term` declares the ring as a customized one. The expression - :n:`@term` is a proof that there exists a morphism between a set of + :n:`@one_term` is a proof that there exists a morphism between a set of coefficient and the ring carrier (see ``Ring_theory.ring_morph`` and ``Ring_theory.semi_morph``). - setoid :n:`@term` :n:`@term` + :n:`setoid @one_term @one_term` forces the use of given setoid. The first - :n:`@term` is a proof that the equality is indeed a setoid (see - ``Setoid.Setoid_Theory``), and the second :n:`@term` a proof that the + :n:`@one_term` is a proof that the equality is indeed a setoid (see + ``Setoid.Setoid_Theory``), and the second a proof that the ring operations are morphisms (see ``Ring_theory.ring_eq_ext`` and ``Ring_theory.sring_eq_ext``). This modifier needs not be used if the setoid and morphisms have been declared. - constants [ :n:`@tactic` ] - specifies a tactic expression :n:`@tactic` that, given a + :n:`constants [ @ltac_expr ]` + specifies a tactic expression :n:`@ltac_expr` that, given a term, returns either an object of the coefficient set that is mapped to the expression via the morphism, or returns ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1 to their counterpart in the coefficient set. This is generally not desirable for non trivial computational rings. - preprocess [ :n:`@tactic` ] - specifies a tactic :n:`@tactic` that is applied as a + :n:`preprocess [ @ltac_expr ]` + specifies a tactic :n:`@ltac_expr` that is applied as a preliminary step for :tacn:`ring` and :tacn:`ring_simplify`. It can be used to transform a goal so that it is better recognized. For instance, ``S n`` can be changed to ``plus 1 n``. - postprocess [ :n:`@tactic` ] - specifies a tactic :n:`@tactic` that is applied as a final + :n:`postprocess [ @ltac_expr ]` + specifies a tactic :n:`@ltac_expr` that is applied as a final step for :tacn:`ring_simplify`. For instance, it can be used to undo modifications of the preprocessor. - power_tac :n:`@term` [ :n:`@tactic` ] + :n:`power @one_term [ {+ @qualid } ]` + to be documented + + :n:`power_tac @one_term @ltac_expr ]` allows :tacn:`ring` and :tacn:`ring_simplify` to recognize power expressions with a constant positive integer exponent (example: - :math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies + :math:`x^2` ). The term :n:`@one_term` is a proof that a given power function satisfies the specification of a power function (term has to be a proof of ``Ring_theory.power_theory``) and :n:`@tactic` specifies a tactic expression that, given a term, “abstracts” it into an object of type |N| whose @@ -374,22 +383,25 @@ The syntax for adding a new ring is and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic does not recognize power expressions as ring expressions. - sign :n:`@term` + :n:`sign @one_term` allows :tacn:`ring_simplify` to use a minus operation when outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The term :token:`term` is a proof that a given sign function indicates expressions that are signed (:token:`term` has to be a proof of ``Ring_theory.get_sign``). See ``plugins/setoid_ring/InitialRing.v`` for examples of sign function. - div :n:`@term` + :n:`div @one_term` allows :tacn:`ring` and :tacn:`ring_simplify` to use monomials with - coefficients other than 1 in the rewriting. The term :n:`@term` is a proof + coefficients other than 1 in the rewriting. The term :n:`@one_term` is a proof that a given division function satisfies the specification of an - euclidean division function (:n:`@term` has to be a proof of + euclidean division function (:n:`@one_term` has to be a proof of ``Ring_theory.div_theory``). For example, this function is called when trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See ``plugins/setoid_ring/InitialRing.v`` for examples of div function. + :n:`closed [ {+ @qualid } ]` + to be documented + Error messages: .. exn:: Bad ring structure. @@ -653,24 +665,27 @@ zero for the correctness of the algorithm. The syntax for adding a new field is -.. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )} +.. cmd:: Add Field @ident : @one_term {? ( {+, @field_mod } ) } - The :n:`@ident` is not relevant. It is used just for error - messages. :n:`@term` is a proof that the field signature satisfies the + .. insertprodn field_mod field_mod + + .. prodn:: + field_mod ::= @ring_mod + | completeness @one_term + + The :n:`@ident` is used only for error + messages. :n:`@one_term` is a proof that the field signature satisfies the (semi-)field axioms. The optional list of modifiers is used to tailor the behavior of the tactic. - .. productionlist:: coq - field_mod : `ring_mod` | completeness `term` - Since field tactics are built upon ``ring`` - tactics, all modifiers of the ``Add Ring`` apply. There is only one + tactics, all modifiers of :cmd:`Add Ring` apply. There is only one specific modifier: - completeness :n:`@term` + completeness :n:`@one_term` allows the field tactic to prove automatically that the image of nonzero coefficients are mapped to nonzero - elements of the field. :n:`@term` is a proof of + elements of the field. :n:`@one_term` is a proof of :g:`forall x y, [x] == [y] -> x ?=! y = true`, which is the completeness of equality on coefficients w.r.t. the field equality. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index c069782add..0e326f45d2 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -372,16 +372,11 @@ to universes and explicitly instantiate polymorphic definitions. universe quantification will be discharged on each section definition independently. -.. cmd:: Constraint @universe_constraint - Polymorphic Constraint @universe_constraint +.. cmd:: Constraint @univ_constraint + Polymorphic Constraint @univ_constraint This command declares a new constraint between named universes. - .. productionlist:: coq - universe_constraint : `qualid` < `qualid` - : `qualid` <= `qualid` - : `qualid` = `qualid` - If consistent, the constraint is then enforced in the global environment. Like :cmd:`Universe`, it can be used with the ``Polymorphic`` prefix in sections only to declare constraints diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 22102aa3ab..d864f8549d 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -183,9 +183,9 @@ todo_include_todos = False nitpicky = True nitpick_ignore = [ ('token', token) for token in [ + 'assums', 'binders', 'collection', - 'command', 'definition', 'dirpath', 'inductive', @@ -194,7 +194,6 @@ nitpick_ignore = [ ('token', token) for token in [ 'module', 'simple_tactic', 'symbol', - 'tactic', 'term_pattern', 'term_pattern_string', 'toplevel_selector', diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index e12ff1ba98..4f0cf5f815 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -158,6 +158,8 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. | @term1 arg ::= ( @ident := @term ) | @term1 + one_term ::= @term1 + | @ @qualid {? @univ_annot } term1 ::= @term_projection | @term0 % @ident | @term0 @@ -175,6 +177,13 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. | ltac : ( @ltac_expr ) field_def ::= @qualid {* @binder } := @term +.. note:: + + Many commands and tactics use :n:`@one_term` rather than :n:`@term`. + The former need to be enclosed in parentheses unless they're very + simple, such as a single identifier. This avoids confusing a space-separated + list of terms with a :n:`@term1` applied to a list of arguments. + .. _types: Types @@ -591,17 +600,15 @@ Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`). Recursive and co-recursive functions: fix and cofix --------------------------------------------------- -.. insertprodn term_fix term1_extended +.. insertprodn term_fix fixannot .. prodn:: term_fix ::= let fix @fix_body in @term | fix @fix_body {? {+ with @fix_body } for @ident } fix_body ::= @ident {* @binder } {? @fixannot } {? : @type } := @term fixannot ::= %{ struct @ident %} - | %{ wf @term1_extended @ident %} - | %{ measure @term1_extended {? @ident } {? @term1_extended } %} - term1_extended ::= @term1 - | @ @qualid {? @univ_annot } + | %{ wf @one_term @ident %} + | %{ measure @one_term {? @ident } {? @one_term } %} The expression ":n:`fix @ident__1 @binder__1 : @type__1 := @term__1 with … with @ident__n @binder__n : @type__n := @term__n for @ident__i`" denotes the @@ -1472,11 +1479,11 @@ Computations | vm_compute {? @ref_or_pattern_occ } | native_compute {? @ref_or_pattern_occ } | unfold {+, @unfold_occ } - | fold {+ @term1_extended } + | fold {+ @one_term } | pattern {+, @pattern_occ } | @ident - delta_flag ::= {? - } [ {+ @smart_global } ] - smart_global ::= @qualid + delta_flag ::= {? - } [ {+ @smart_qualid } ] + smart_qualid ::= @qualid | @by_notation by_notation ::= @string {? % @ident } strategy_flag ::= {+ @red_flags } @@ -1488,16 +1495,16 @@ Computations | cofix | zeta | delta {? @delta_flag } - ref_or_pattern_occ ::= @smart_global {? at @occs_nums } - | @term1_extended {? at @occs_nums } + ref_or_pattern_occ ::= @smart_qualid {? at @occs_nums } + | @one_term {? at @occs_nums } occs_nums ::= {+ @num_or_var } | - @num_or_var {* @int_or_var } num_or_var ::= @num | @ident int_or_var ::= @int | @ident - unfold_occ ::= @smart_global {? at @occs_nums } - pattern_occ ::= @term1_extended {? at @occs_nums } + unfold_occ ::= @smart_qualid {? at @occs_nums } + pattern_occ ::= @one_term {? at @occs_nums } See :ref:`Conversion-rules`. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 179dff9959..514353e39b 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -505,34 +505,41 @@ Building a |Coq| project with Dune .. note:: + Dune's Coq support is still experimental; we strongly recommend + using Dune 2.3 or later. + +.. note:: + The canonical documentation for the Coq Dune extension is maintained upstream; please refer to the `Dune manual - <https://dune.readthedocs.io/>`_ for up-to-date information. + <https://dune.readthedocs.io/>`_ for up-to-date information. This + documentation is up to date for Dune 2.3. Building a Coq project with Dune requires setting up a Dune project for your files. This involves adding a ``dune-project`` and -``pkg.opam`` file to the root (``pkg.opam`` can be empty), and then -providing ``dune`` files in the directories your ``.v`` files are -placed. For the experimental version "0.1" of the Coq Dune language, -|Coq| library stanzas look like: +``pkg.opam`` file to the root (``pkg.opam`` can be empty or generated +by Dune itself), and then providing ``dune`` files in the directories +your ``.v`` files are placed. For the experimental version "0.1" of +the Coq Dune language, |Coq| library stanzas look like: .. code:: scheme - (coqlib + (coq.theory (name <module_prefix>) - (public_name <package.lib_name>) + (package <opam_package>) (synopsis <text>) (modules <ordered_set_lang>) (libraries <ocaml_libraries>) (flags <coq_flags>)) This stanza will build all `.v` files in the given directory, wrapping -the library under ``<module_prefix>``. If you declare a -``<package.lib_name>`` a ``.install`` file for the library will be -generated; the optional ``<modules>`` field allows you to filter -the list of modules, and ``<libraries>`` allows to depend on ML -plugins. For the moment, Dune relies on Coq's standard mechanisms -(such as ``COQPATH``) to locate installed Coq libraries. +the library under ``<module_prefix>``. If you declare an +``<opam_package>``, an ``.install`` file for the library will be +generated; the optional ``(modules <ordered_set_lang>)`` field allows +you to filter the list of modules, and ``(libraries +<ocaml_libraries>)`` allows the Coq theory depend on ML plugins. For +the moment, Dune relies on Coq's standard mechanisms (such as +``COQPATH``) to locate installed Coq libraries. By default Dune will skip ``.v`` files present in subdirectories. In order to enable the usual recursive organization of Coq projects add @@ -565,9 +572,9 @@ of your project. .. code:: scheme - (coqlib + (coq.theory (name Equations) ; -R flag - (public_name equations.Equations) + (package equations) (synopsis "Equations Plugin") (libraries coq.plugins.extraction equations.plugin) (modules :standard \ IdDec NoCycle)) ; exclude some modules that don't build diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 2bfd810ea1..4f2f74aae4 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -72,7 +72,7 @@ specified, the default selector is used. .. _bindingslist: Bindings list -~~~~~~~~~~~~~~~~~~~ +~~~~~~~~~~~~~ Tactics that take a term as an argument may also support a bindings list to instantiate some parameters of the term by name or position. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index fd95a5cef4..669975ba7e 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -947,7 +947,7 @@ notations are given below. The optional :production:`scope` is described in .. prodn:: decl_notations ::= where @decl_notation {* and @decl_notation } - decl_notation ::= @string := @term1_extended [(only parsing)] {? : @ident } + decl_notation ::= @string := @one_term {? ( only parsing ) } {? : @ident } .. note:: No typing of the denoted expression is performed at definition time. Type checking is done only at the time of use of the notation. @@ -1194,7 +1194,7 @@ Binding arguments of a constant to an interpretation scope Binding types of arguments to an interpretation scope +++++++++++++++++++++++++++++++++++++++++++++++++++++ -.. cmd:: Bind Scope @scope with @qualid +.. cmd:: Bind Scope @ident with {+ @class } When an interpretation scope is naturally associated to a type (e.g. the scope of operations on the natural numbers), it may be convenient to bind it diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index d6ecf311f1..4d5c837e5c 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -294,7 +294,7 @@ class VernacObject(NotationObject): Example:: - .. cmd:: Infix @string := @term1_extended {? ( {+, @syntax_modifier } ) } {? : @ident } + .. cmd:: Infix @string := @one_term {? ( {+, @syntax_modifier } ) } {? : @ident } This command is equivalent to :n:`…`. """ diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 3524d77380..7a165988a6 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -57,14 +57,15 @@ DELETE: [ | check_for_coloneq | local_test_lpar_id_colon | lookup_at_as_comma -| only_starredidentrefs +| test_only_starredidentrefs | test_bracket_ident | test_lpar_id_colon | test_lpar_id_coloneq (* todo: grammar seems incorrect, repeats the "(" IDENT ":=" *) | test_lpar_id_rpar | test_lpar_idnum_coloneq -| test_nospace_pipe_closedcurly | test_show_goal +| test_name_colon +| test_pipe_closedcurly | ensure_fixannot (* SSR *) @@ -332,8 +333,8 @@ typeclass_constraint: [ | EDIT ADD_OPT "!" operconstr200 | REPLACE "{" name "}" ":" [ "!" | ] operconstr200 | WITH "{" name "}" ":" OPT "!" operconstr200 -| REPLACE name_colon [ "!" | ] operconstr200 -| WITH name_colon OPT "!" operconstr200 +| REPLACE name ":" [ "!" | ] operconstr200 +| WITH name ":" OPT "!" operconstr200 ] (* ?? From the grammar, Prim.name seems to be only "_" but ident is also accepted "*) @@ -409,19 +410,6 @@ DELETE: [ | cumulativity_token ] -opt_coercion: [ -| OPTINREF -] - -opt_constructors_or_fields: [ -| OPTINREF -] - -SPLICE: [ -| opt_coercion -| opt_constructors_or_fields -] - constructor_list_or_record_decl: [ | OPTINREF ] @@ -433,11 +421,6 @@ record_fields: [ | DELETE (* empty *) ] -decl_notation: [ -| REPLACE "where" LIST1 one_decl_notation SEP decl_sep -| WITH "where" one_decl_notation LIST0 ( decl_sep one_decl_notation ) -] - assumptions_token: [ | DELETENT ] @@ -767,13 +750,13 @@ vernacular: [ ] rec_definition: [ -| REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation -| WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation +| REPLACE ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations +| WITH ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations ] corec_definition: [ -| REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation -| WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation +| REPLACE ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations +| WITH ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations ] type_cstr: [ @@ -782,13 +765,9 @@ type_cstr: [ | OPTINREF ] -decl_notation: [ -| OPTINREF -] - inductive_definition: [ -| REPLACE OPT ">" ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] OPT ( ":=" OPT constructor_list_or_record_decl ) OPT decl_notation -| WITH OPT ">" ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] OPT ( ":=" OPT constructor_list_or_record_decl ) OPT decl_notation +| REPLACE opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations +| WITH opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" type ] opt_constructors_or_fields decl_notations ] constructor_list_or_record_decl: [ @@ -807,6 +786,31 @@ record_binder: [ | DELETE name ] +in_clause: [ +| DELETE in_clause' +| REPLACE LIST0 hypident_occ SEP "," "|-" concl_occ +| WITH LIST0 hypident_occ SEP "," OPT ( "|-" concl_occ ) +| DELETE LIST0 hypident_occ SEP "," +] + +concl_occ: [ +| OPTINREF +] + +opt_coercion: [ +| OPTINREF +] + +opt_constructors_or_fields: [ +| OPTINREF +] + +decl_notations: [ +| REPLACE "where" LIST1 decl_notation SEP decl_sep +| WITH "where" decl_notation LIST0 (decl_sep decl_notation ) +| OPTINREF +] + SPLICE: [ | noedit_mode | command_entry @@ -941,11 +945,12 @@ SPLICE: [ | record_fields | constructor_type | record_binder +| opt_coercion +| opt_constructors_or_fields ] (* end SPLICE *) RENAME: [ | clause clause_dft_concl -| in_clause' in_clause | tactic3 ltac_expr3 (* todo: can't figure out how this gets mapped by coqpp *) | tactic1 ltac_expr1 (* todo: can't figure out how this gets mapped by coqpp *) @@ -980,7 +985,7 @@ RENAME: [ | nat_or_var num_or_var | fix_decl fix_body | cofix_decl cofix_body -| constr term1_extended +| constr one_term | appl_arg arg | rec_definition fix_definition | corec_definition cofix_definition @@ -988,12 +993,12 @@ RENAME: [ | univ_instance univ_annot | simple_assum_coe assumpt | of_type_with_opt_coercion of_type -| decl_notation decl_notations -| one_decl_notation decl_notation | attribute attr | attribute_value attr_value | constructor_list_or_record_decl constructors_or_record | record_binder_body field_body +| class_rawexpr class +| smart_global smart_qualid ] diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 5fcb56f5f2..366b70a1f7 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -1717,7 +1717,7 @@ let process_rst g file args seen tac_prods cmd_prods = else begin let line3 = getline() in if not (Str.string_match dir_regex line3 0) || (Str.matched_group 2 line3) <> "prodn::" then - error "%s line %d: expecting 'prodn' after 'insertprodn'\n" file !linenum + error "%s line %d: expecting '.. prodn::' after 'insertprodn'\n" file !linenum else begin let indent = Str.matched_group 1 line3 in let rec skip_to_end () = diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 529d81e424..6897437457 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -152,7 +152,7 @@ binder_constr: [ ] appl_arg: [ -| lpar_id_coloneq lconstr ")" +| test_lpar_id_coloneq "(" ident ":=" lconstr ")" | operconstr9 ] @@ -335,7 +335,7 @@ closed_binder: [ typeclass_constraint: [ | "!" operconstr200 | "{" name "}" ":" [ "!" | ] operconstr200 -| name_colon [ "!" | ] operconstr200 +| test_name_colon name ":" [ "!" | ] operconstr200 | operconstr200 ] @@ -449,7 +449,7 @@ bigint: [ ] bar_cbrace: [ -| test_nospace_pipe_closedcurly "|" "}" +| test_pipe_closedcurly "|" "}" ] vernac_toplevel: [ @@ -511,8 +511,8 @@ command: [ | "Load" [ "Verbose" | ] [ ne_string | IDENT ] | "Declare" "ML" "Module" LIST1 ne_string | "Locate" locatable -| "Add" "LoadPath" ne_string as_dirpath -| "Add" "Rec" "LoadPath" ne_string as_dirpath +| "Add" "LoadPath" ne_string "as" dirpath +| "Add" "Rec" "LoadPath" ne_string "as" dirpath | "Remove" "LoadPath" ne_string | "Type" lconstr | "Print" printable @@ -522,7 +522,6 @@ command: [ | "Print" "Namespace" dirpath | "Inspect" natural | "Add" "ML" "Path" ne_string -| "Add" "Rec" "ML" "Path" ne_string | "Set" option_table option_setting | "Unset" option_table | "Print" "Table" option_table @@ -655,6 +654,7 @@ command: [ | "Add" "CstOp" constr (* micromega plugin *) | "Add" "BinRel" constr (* micromega plugin *) | "Add" "PropOp" constr (* micromega plugin *) +| "Add" "PropBinOp" constr (* micromega plugin *) | "Add" "PropUOp" constr (* micromega plugin *) | "Add" "Spec" constr (* micromega plugin *) | "Add" "BinOpSpec" constr (* micromega plugin *) @@ -924,16 +924,16 @@ reduce: [ | ] -one_decl_notation: [ -| ne_lstring ":=" constr OPT [ ":" IDENT ] +decl_notation: [ +| ne_lstring ":=" constr only_parsing OPT [ ":" IDENT ] ] decl_sep: [ | "and" ] -decl_notation: [ -| "where" LIST1 one_decl_notation SEP decl_sep +decl_notations: [ +| "where" LIST1 decl_notation SEP decl_sep | ] @@ -943,7 +943,7 @@ opt_constructors_or_fields: [ ] inductive_definition: [ -| opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notation +| opt_coercion ident_decl binders OPT [ "|" binders ] OPT [ ":" lconstr ] opt_constructors_or_fields decl_notations ] constructor_list_or_record_decl: [ @@ -961,11 +961,11 @@ opt_coercion: [ ] rec_definition: [ -| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notation +| ident_decl binders_fixannot type_cstr OPT [ ":=" lconstr ] decl_notations ] corec_definition: [ -| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notation +| ident_decl binders type_cstr OPT [ ":=" lconstr ] decl_notations ] scheme: [ @@ -982,7 +982,7 @@ scheme_kind: [ ] record_field: [ -| LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notation +| LIST0 quoted_attributes record_binder OPT [ "|" natural ] decl_notations ] record_fields: [ @@ -1148,7 +1148,7 @@ module_type: [ ] section_subset_expr: [ -| only_starredidentrefs LIST0 starredidentref +| test_only_starredidentrefs LIST0 starredidentref | ssexpr35 ] @@ -1172,8 +1172,8 @@ ssexpr50: [ ssexpr0: [ | starredidentref -| "(" only_starredidentrefs LIST0 starredidentref ")" -| "(" only_starredidentrefs LIST0 starredidentref ")" "*" +| "(" test_only_starredidentrefs LIST0 starredidentref ")" +| "(" test_only_starredidentrefs LIST0 starredidentref ")" "*" | "(" ssexpr35 ")" | "(" ssexpr35 ")" "*" ] @@ -1331,10 +1331,6 @@ option_table: [ | LIST1 IDENT ] -as_dirpath: [ -| OPT [ "as" dirpath ] -] - ne_in_or_out_modules: [ | "inside" LIST1 global | "outside" LIST1 global @@ -1684,6 +1680,8 @@ simple_tactic: [ | "eenough" test_lpar_id_colon "(" identref ":" lconstr ")" by_tactic | "assert" constr as_ipat by_tactic | "eassert" constr as_ipat by_tactic +| "pose" "proof" test_lpar_id_coloneq "(" identref ":=" lconstr ")" +| "epose" "proof" test_lpar_id_coloneq "(" identref ":=" lconstr ")" | "pose" "proof" lconstr as_ipat | "epose" "proof" lconstr as_ipat | "enough" constr as_ipat by_tactic @@ -1740,10 +1738,11 @@ simple_tactic: [ | "psatz_R" tactic (* micromega plugin *) | "psatz_Q" int_or_var tactic (* micromega plugin *) | "psatz_Q" tactic (* micromega plugin *) -| "zify_iter_specs" tactic (* micromega plugin *) +| "zify_iter_specs" (* micromega plugin *) | "zify_op" (* micromega plugin *) | "zify_saturate" (* micromega plugin *) | "zify_iter_let" tactic (* micromega plugin *) +| "zify_elim_let" (* micromega plugin *) | "nsatz_compute" constr (* nsatz plugin *) | "omega" (* omega plugin *) | "rtauto" diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 908e3ccd51..f26a174722 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -58,6 +58,11 @@ arg: [ | term1 ] +one_term: [ +| term1 +| "@" qualid OPT univ_annot +] + term1: [ | term_projection | term0 "%" ident @@ -238,13 +243,8 @@ fix_body: [ fixannot: [ | "{" "struct" ident "}" -| "{" "wf" term1_extended ident "}" -| "{" "measure" term1_extended OPT ident OPT term1_extended "}" -] - -term1_extended: [ -| term1 -| "@" qualid OPT univ_annot +| "{" "wf" one_term ident "}" +| "{" "measure" one_term OPT ident OPT one_term "}" ] term_cofix: [ @@ -400,7 +400,7 @@ decl_notations: [ ] decl_notation: [ -| string ":=" term1_extended OPT [ ":" ident ] +| string ":=" one_term OPT ( "(" "only" "parsing" ")" ) OPT [ ":" ident ] ] register_token: [ @@ -484,16 +484,16 @@ red_expr: [ | "vm_compute" OPT ref_or_pattern_occ | "native_compute" OPT ref_or_pattern_occ | "unfold" LIST1 unfold_occ SEP "," -| "fold" LIST1 term1_extended +| "fold" LIST1 one_term | "pattern" LIST1 pattern_occ SEP "," | ident ] delta_flag: [ -| OPT "-" "[" LIST1 smart_global "]" +| OPT "-" "[" LIST1 smart_qualid "]" ] -smart_global: [ +smart_qualid: [ | qualid | by_notation ] @@ -518,8 +518,8 @@ red_flags: [ ] ref_or_pattern_occ: [ -| smart_global OPT ( "at" occs_nums ) -| term1_extended OPT ( "at" occs_nums ) +| smart_qualid OPT ( "at" occs_nums ) +| one_term OPT ( "at" occs_nums ) ] occs_nums: [ @@ -538,11 +538,11 @@ int_or_var: [ ] unfold_occ: [ -| smart_global OPT ( "at" occs_nums ) +| smart_qualid OPT ( "at" occs_nums ) ] pattern_occ: [ -| term1_extended OPT ( "at" occs_nums ) +| one_term OPT ( "at" occs_nums ) ] finite_token: [ @@ -587,11 +587,11 @@ scheme: [ ] scheme_kind: [ -| "Induction" "for" smart_global "Sort" sort_family -| "Minimality" "for" smart_global "Sort" sort_family -| "Elimination" "for" smart_global "Sort" sort_family -| "Case" "for" smart_global "Sort" sort_family -| "Equality" "for" smart_global +| "Induction" "for" smart_qualid "Sort" sort_family +| "Minimality" "for" smart_qualid "Sort" sort_family +| "Elimination" "for" smart_qualid "Sort" sort_family +| "Case" "for" smart_qualid "Sort" sort_family +| "Equality" "for" smart_qualid ] sort_family: [ @@ -615,21 +615,21 @@ gallina_ext: [ | "Export" LIST1 qualid | "Include" module_type_inl LIST0 ( "<+" module_expr_inl ) | "Include" "Type" module_type_inl LIST0 ( "<+" module_type_inl ) -| "Transparent" LIST1 smart_global -| "Opaque" LIST1 smart_global -| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ] +| "Transparent" LIST1 smart_qualid +| "Opaque" LIST1 smart_qualid +| "Strategy" LIST1 [ strategy_level "[" LIST1 smart_qualid "]" ] | "Canonical" OPT "Structure" qualid OPT [ OPT univ_decl def_body ] | "Canonical" OPT "Structure" by_notation | "Coercion" qualid OPT univ_decl def_body -| "Identity" "Coercion" ident ":" class_rawexpr ">->" class_rawexpr -| "Coercion" qualid ":" class_rawexpr ">->" class_rawexpr -| "Coercion" by_notation ":" class_rawexpr ">->" class_rawexpr +| "Identity" "Coercion" ident ":" class ">->" class +| "Coercion" qualid ":" class ">->" class +| "Coercion" by_notation ":" class ">->" class | "Context" LIST1 binder | "Instance" instance_name ":" term hint_info [ ":=" "{" [ LIST1 field_def SEP ";" | ] "}" | ":=" term | ] | "Existing" "Instance" qualid hint_info | "Existing" "Instances" LIST1 qualid OPT [ "|" num ] | "Existing" "Class" qualid -| "Arguments" smart_global LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ] +| "Arguments" smart_qualid LIST0 argument_spec_block LIST0 [ "," LIST0 more_implicits_block ] OPT [ ":" LIST1 arguments_modifier SEP "," ] | "Implicit" "Type" reserv_list | "Implicit" "Types" reserv_list | "Generalizable" [ "All" "Variables" | "No" "Variables" | [ "Variable" | "Variables" ] LIST1 ident ] @@ -643,14 +643,8 @@ option_setting: [ | string ] -class_rawexpr: [ -| "Funclass" -| "Sortclass" -| smart_global -] - hint_info: [ -| "|" OPT num OPT term1_extended +| "|" OPT num OPT one_term | ] @@ -780,11 +774,11 @@ command: [ | "Load" [ "Verbose" | ] [ string | ident ] | "Declare" "ML" "Module" LIST1 string | "Locate" locatable -| "Add" "LoadPath" string as_dirpath -| "Add" "Rec" "LoadPath" string as_dirpath +| "Add" "LoadPath" string "as" dirpath +| "Add" "Rec" "LoadPath" string "as" dirpath | "Remove" "LoadPath" string | "Type" term -| "Print" "Term" smart_global OPT ( "@{" LIST0 name "}" ) +| "Print" "Term" smart_qualid OPT ( "@{" LIST0 name "}" ) | "Print" "All" | "Print" "Section" qualid | "Print" "Grammar" ident @@ -798,36 +792,35 @@ command: [ | "Print" "Graph" | "Print" "Classes" | "Print" "TypeClasses" -| "Print" "Instances" smart_global +| "Print" "Instances" smart_qualid | "Print" "Coercions" -| "Print" "Coercion" "Paths" class_rawexpr class_rawexpr -| "Print" "Canonical" "Projections" LIST0 smart_global +| "Print" "Coercion" "Paths" class class +| "Print" "Canonical" "Projections" LIST0 smart_qualid | "Print" "Typing" "Flags" | "Print" "Tables" | "Print" "Options" | "Print" "Hint" -| "Print" "Hint" smart_global +| "Print" "Hint" smart_qualid | "Print" "Hint" "*" | "Print" "HintDb" ident | "Print" "Scopes" | "Print" "Scope" ident | "Print" "Visibility" OPT ident -| "Print" "Implicit" smart_global +| "Print" "Implicit" smart_qualid | "Print" OPT "Sorted" "Universes" OPT ( "Subgraph" "(" LIST0 qualid ")" ) OPT string -| "Print" "Assumptions" smart_global -| "Print" "Opaque" "Dependencies" smart_global -| "Print" "Transparent" "Dependencies" smart_global -| "Print" "All" "Dependencies" smart_global -| "Print" "Strategy" smart_global +| "Print" "Assumptions" smart_qualid +| "Print" "Opaque" "Dependencies" smart_qualid +| "Print" "Transparent" "Dependencies" smart_qualid +| "Print" "All" "Dependencies" smart_qualid +| "Print" "Strategy" smart_qualid | "Print" "Strategies" | "Print" "Registered" -| "Print" smart_global OPT ( "@{" LIST0 name "}" ) +| "Print" smart_qualid OPT ( "@{" LIST0 name "}" ) | "Print" "Module" "Type" qualid | "Print" "Module" qualid | "Print" "Namespace" dirpath | "Inspect" num | "Add" "ML" "Path" string -| "Add" "Rec" "ML" "Path" string | "Set" LIST1 ident option_setting | "Unset" LIST1 ident | "Print" "Table" LIST1 ident @@ -849,7 +842,7 @@ command: [ | "Debug" "Off" | "Declare" "Reduction" ident ":=" red_expr | "Declare" "Custom" "Entry" ident -| "Derive" ident "SuchThat" term1_extended "As" ident (* derive plugin *) +| "Derive" ident "SuchThat" one_term "As" ident (* derive plugin *) | "Proof" | "Proof" "Mode" string | "Proof" term @@ -907,31 +900,31 @@ command: [ | "Obligations" | "Preterm" "of" ident | "Preterm" -| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident -| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident -| "Add" "Relation" term1_extended term1_extended "as" ident -| "Add" "Relation" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident -| "Add" "Relation" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Relation" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Relation" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "reflexivity" "proved" "by" term1_extended "symmetry" "proved" "by" term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Parametric" "Relation" LIST0 binder ":" term1_extended term1_extended "transitivity" "proved" "by" term1_extended "as" ident -| "Add" "Setoid" term1_extended term1_extended term1_extended "as" ident -| "Add" "Parametric" "Setoid" LIST0 binder ":" term1_extended term1_extended term1_extended "as" ident -| "Add" "Morphism" term1_extended ":" ident -| "Declare" "Morphism" term1_extended ":" ident -| "Add" "Morphism" term1_extended "with" "signature" term "as" ident -| "Add" "Parametric" "Morphism" LIST0 binder ":" term1_extended "with" "signature" term "as" ident +| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "as" ident +| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "as" ident +| "Add" "Relation" one_term one_term "as" ident +| "Add" "Relation" one_term one_term "symmetry" "proved" "by" one_term "as" ident +| "Add" "Relation" one_term one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Relation" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Relation" one_term one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "symmetry" "proved" "by" one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "reflexivity" "proved" "by" one_term "symmetry" "proved" "by" one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Parametric" "Relation" LIST0 binder ":" one_term one_term "transitivity" "proved" "by" one_term "as" ident +| "Add" "Setoid" one_term one_term one_term "as" ident +| "Add" "Parametric" "Setoid" LIST0 binder ":" one_term one_term one_term "as" ident +| "Add" "Morphism" one_term ":" ident +| "Declare" "Morphism" one_term ":" ident +| "Add" "Morphism" one_term "with" "signature" term "as" ident +| "Add" "Parametric" "Morphism" LIST0 binder ":" one_term "with" "signature" term "as" ident | "Grab" "Existential" "Variables" | "Unshelve" -| "Declare" "Equivalent" "Keys" term1_extended term1_extended +| "Declare" "Equivalent" "Keys" one_term one_term | "Print" "Equivalent" "Keys" | "Optimize" "Proof" | "Optimize" "Heap" @@ -940,24 +933,25 @@ command: [ | "Show" "Ltac" "Profile" "CutOff" int | "Show" "Ltac" "Profile" string | "Show" "Lia" "Profile" (* micromega plugin *) -| "Add" "InjTyp" term1_extended (* micromega plugin *) -| "Add" "BinOp" term1_extended (* micromega plugin *) -| "Add" "UnOp" term1_extended (* micromega plugin *) -| "Add" "CstOp" term1_extended (* micromega plugin *) -| "Add" "BinRel" term1_extended (* micromega plugin *) -| "Add" "PropOp" term1_extended (* micromega plugin *) -| "Add" "PropUOp" term1_extended (* micromega plugin *) -| "Add" "Spec" term1_extended (* micromega plugin *) -| "Add" "BinOpSpec" term1_extended (* micromega plugin *) -| "Add" "UnOpSpec" term1_extended (* micromega plugin *) -| "Add" "Saturate" term1_extended (* micromega plugin *) +| "Add" "InjTyp" one_term (* micromega plugin *) +| "Add" "BinOp" one_term (* micromega plugin *) +| "Add" "UnOp" one_term (* micromega plugin *) +| "Add" "CstOp" one_term (* micromega plugin *) +| "Add" "BinRel" one_term (* micromega plugin *) +| "Add" "PropOp" one_term (* micromega plugin *) +| "Add" "PropBinOp" one_term (* micromega plugin *) +| "Add" "PropUOp" one_term (* micromega plugin *) +| "Add" "Spec" one_term (* micromega plugin *) +| "Add" "BinOpSpec" one_term (* micromega plugin *) +| "Add" "UnOpSpec" one_term (* micromega plugin *) +| "Add" "Saturate" one_term (* micromega plugin *) | "Show" "Zify" "InjTyp" (* micromega plugin *) | "Show" "Zify" "BinOp" (* micromega plugin *) | "Show" "Zify" "UnOp" (* micromega plugin *) | "Show" "Zify" "CstOp" (* micromega plugin *) | "Show" "Zify" "BinRel" (* micromega plugin *) | "Show" "Zify" "Spec" (* micromega plugin *) -| "Add" "Ring" ident ":" term1_extended OPT ( "(" LIST1 ring_mod SEP "," ")" ) (* setoid_ring plugin *) +| "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" ) (* setoid_ring plugin *) | "Hint" "Cut" "[" hints_path "]" opthints | "Typeclasses" "Transparent" LIST0 qualid | "Typeclasses" "Opaque" LIST0 qualid @@ -996,20 +990,20 @@ command: [ | "Show" "Extraction" (* extraction plugin *) | "Functional" "Case" fun_scheme_arg (* funind plugin *) | "Generate" "graph" "for" qualid (* funind plugin *) -| "Hint" "Rewrite" orient LIST1 term1_extended ":" LIST0 ident -| "Hint" "Rewrite" orient LIST1 term1_extended "using" ltac_expr ":" LIST0 ident -| "Hint" "Rewrite" orient LIST1 term1_extended -| "Hint" "Rewrite" orient LIST1 term1_extended "using" ltac_expr -| "Derive" "Inversion_clear" ident "with" term1_extended "Sort" sort_family -| "Derive" "Inversion_clear" ident "with" term1_extended -| "Derive" "Inversion" ident "with" term1_extended "Sort" sort_family -| "Derive" "Inversion" ident "with" term1_extended -| "Derive" "Dependent" "Inversion" ident "with" term1_extended "Sort" sort_family -| "Derive" "Dependent" "Inversion_clear" ident "with" term1_extended "Sort" sort_family -| "Declare" "Left" "Step" term1_extended -| "Declare" "Right" "Step" term1_extended +| "Hint" "Rewrite" orient LIST1 one_term ":" LIST0 ident +| "Hint" "Rewrite" orient LIST1 one_term "using" ltac_expr ":" LIST0 ident +| "Hint" "Rewrite" orient LIST1 one_term +| "Hint" "Rewrite" orient LIST1 one_term "using" ltac_expr +| "Derive" "Inversion_clear" ident "with" one_term "Sort" sort_family +| "Derive" "Inversion_clear" ident "with" one_term +| "Derive" "Inversion" ident "with" one_term "Sort" sort_family +| "Derive" "Inversion" ident "with" one_term +| "Derive" "Dependent" "Inversion" ident "with" one_term "Sort" sort_family +| "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family +| "Declare" "Left" "Step" one_term +| "Declare" "Right" "Step" one_term | "Print" "Rings" (* setoid_ring plugin *) -| "Add" "Field" ident ":" term1_extended OPT ( "(" LIST1 field_mod SEP "," ")" ) (* setoid_ring plugin *) +| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* setoid_ring plugin *) | "Print" "Fields" (* setoid_ring plugin *) | "Numeral" "Notation" qualid qualid qualid ":" ident OPT numnotoption | "String" "Notation" qualid qualid qualid ":" ident @@ -1059,8 +1053,8 @@ dirpath: [ ] locatable: [ -| smart_global -| "Term" smart_global +| smart_qualid +| "Term" smart_qualid | "File" string | "Library" qualid | "Module" qualid @@ -1071,19 +1065,15 @@ option_ref_value: [ | string ] -as_dirpath: [ -| OPT [ "as" dirpath ] -] - comment: [ -| term1_extended +| one_term | string | num ] reference_or_constr: [ | qualid -| term1_extended +| one_term ] hint: [ @@ -1100,7 +1090,7 @@ hint: [ | "Mode" qualid LIST1 [ "+" | "!" | "-" ] | "Unfold" LIST1 qualid | "Constructors" LIST1 qualid -| "Extern" num OPT term1_extended "=>" ltac_expr +| "Extern" num OPT one_term "=>" ltac_expr ] constr_body: [ @@ -1157,23 +1147,23 @@ fun_scheme_arg: [ ] ring_mod: [ -| "decidable" term1_extended (* setoid_ring plugin *) +| "decidable" one_term (* setoid_ring plugin *) | "abstract" (* setoid_ring plugin *) -| "morphism" term1_extended (* setoid_ring plugin *) +| "morphism" one_term (* setoid_ring plugin *) | "constants" "[" ltac_expr "]" (* setoid_ring plugin *) -| "closed" "[" LIST1 qualid "]" (* setoid_ring plugin *) | "preprocess" "[" ltac_expr "]" (* setoid_ring plugin *) | "postprocess" "[" ltac_expr "]" (* setoid_ring plugin *) -| "setoid" term1_extended term1_extended (* setoid_ring plugin *) -| "sign" term1_extended (* setoid_ring plugin *) -| "power" term1_extended "[" LIST1 qualid "]" (* setoid_ring plugin *) -| "power_tac" term1_extended "[" ltac_expr "]" (* setoid_ring plugin *) -| "div" term1_extended (* setoid_ring plugin *) +| "setoid" one_term one_term (* setoid_ring plugin *) +| "sign" one_term (* setoid_ring plugin *) +| "power" one_term "[" LIST1 qualid "]" (* setoid_ring plugin *) +| "power_tac" one_term "[" ltac_expr "]" (* setoid_ring plugin *) +| "div" one_term (* setoid_ring plugin *) +| "closed" "[" LIST1 qualid "]" (* setoid_ring plugin *) ] field_mod: [ | ring_mod (* setoid_ring plugin *) -| "completeness" term1_extended (* setoid_ring plugin *) +| "completeness" one_term (* setoid_ring plugin *) ] debug: [ @@ -1216,15 +1206,21 @@ query_command: [ | "Eval" red_expr "in" term "." | "Compute" term "." | "Check" term "." -| "About" smart_global OPT ( "@{" LIST0 name "}" ) "." -| "SearchHead" term1_extended in_or_out_modules "." -| "SearchPattern" term1_extended in_or_out_modules "." -| "SearchRewrite" term1_extended in_or_out_modules "." +| "About" smart_qualid OPT ( "@{" LIST0 name "}" ) "." +| "SearchHead" one_term in_or_out_modules "." +| "SearchPattern" one_term in_or_out_modules "." +| "SearchRewrite" one_term in_or_out_modules "." | "Search" searchabout_query searchabout_queries "." | "SearchAbout" searchabout_query searchabout_queries "." | "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "." ] +class: [ +| "Funclass" +| "Sortclass" +| smart_qualid +] + ne_in_or_out_modules: [ | "inside" LIST1 qualid | "outside" LIST1 qualid @@ -1242,7 +1238,7 @@ positive_search_mark: [ searchabout_query: [ | positive_search_mark string OPT ( "%" ident ) -| positive_search_mark term1_extended +| positive_search_mark one_term ] searchabout_queries: [ @@ -1256,10 +1252,10 @@ syntax: [ | "Close" "Scope" ident | "Delimit" "Scope" ident "with" ident | "Undelimit" "Scope" ident -| "Bind" "Scope" ident "with" LIST1 class_rawexpr -| "Infix" string ":=" term1_extended OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ] -| "Notation" ident LIST0 ident ":=" term1_extended OPT ( "(" "only" "parsing" ")" ) -| "Notation" string ":=" term1_extended OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ] +| "Bind" "Scope" ident "with" LIST1 class +| "Infix" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ] +| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" ) +| "Notation" string ":=" one_term OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] OPT [ ":" ident ] | "Format" "Notation" string string string | "Reserved" "Infix" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] | "Reserved" "Notation" string OPT [ "(" LIST1 syntax_modifier SEP "," ")" ] @@ -1314,17 +1310,17 @@ at_level_opt: [ simple_tactic: [ | "reflexivity" -| "exact" term1_extended +| "exact" one_term | "assumption" | "etransitivity" -| "cut" term1_extended -| "exact_no_check" term1_extended -| "vm_cast_no_check" term1_extended -| "native_cast_no_check" term1_extended -| "casetype" term1_extended -| "elimtype" term1_extended -| "lapply" term1_extended -| "transitivity" term1_extended +| "cut" one_term +| "exact_no_check" one_term +| "vm_cast_no_check" one_term +| "native_cast_no_check" one_term +| "casetype" one_term +| "elimtype" one_term +| "lapply" one_term +| "transitivity" one_term | "left" | "eleft" | "left" "with" bindings @@ -1377,11 +1373,11 @@ simple_tactic: [ | "clear" LIST0 ident | "clear" "-" LIST1 ident | "clearbody" LIST1 ident -| "generalize" "dependent" term1_extended -| "replace" term1_extended "with" term1_extended clause_dft_concl by_arg_tac -| "replace" "->" term1_extended clause_dft_concl -| "replace" "<-" term1_extended clause_dft_concl -| "replace" term1_extended clause_dft_concl +| "generalize" "dependent" one_term +| "replace" one_term "with" one_term clause_dft_concl by_arg_tac +| "replace" "->" one_term clause_dft_concl +| "replace" "<-" one_term clause_dft_concl +| "replace" one_term clause_dft_concl | "simplify_eq" | "simplify_eq" destruction_arg | "esimplify_eq" @@ -1400,64 +1396,64 @@ simple_tactic: [ | "einjection" destruction_arg "as" LIST0 simple_intropattern | "simple" "injection" | "simple" "injection" destruction_arg -| "dependent" "rewrite" orient term1_extended -| "dependent" "rewrite" orient term1_extended "in" ident -| "cutrewrite" orient term1_extended -| "cutrewrite" orient term1_extended "in" ident -| "decompose" "sum" term1_extended -| "decompose" "record" term1_extended -| "absurd" term1_extended +| "dependent" "rewrite" orient one_term +| "dependent" "rewrite" orient one_term "in" ident +| "cutrewrite" orient one_term +| "cutrewrite" orient one_term "in" ident +| "decompose" "sum" one_term +| "decompose" "record" one_term +| "absurd" one_term | "contradiction" OPT constr_with_bindings | "autorewrite" "with" LIST1 ident clause_dft_concl | "autorewrite" "with" LIST1 ident clause_dft_concl "using" ltac_expr | "autorewrite" "*" "with" LIST1 ident clause_dft_concl | "autorewrite" "*" "with" LIST1 ident clause_dft_concl "using" ltac_expr -| "rewrite" "*" orient term1_extended "in" ident "at" occurrences by_arg_tac -| "rewrite" "*" orient term1_extended "at" occurrences "in" ident by_arg_tac -| "rewrite" "*" orient term1_extended "in" ident by_arg_tac -| "rewrite" "*" orient term1_extended "at" occurrences by_arg_tac -| "rewrite" "*" orient term1_extended by_arg_tac -| "refine" term1_extended -| "simple" "refine" term1_extended -| "notypeclasses" "refine" term1_extended -| "simple" "notypeclasses" "refine" term1_extended +| "rewrite" "*" orient one_term "in" ident "at" occurrences by_arg_tac +| "rewrite" "*" orient one_term "at" occurrences "in" ident by_arg_tac +| "rewrite" "*" orient one_term "in" ident by_arg_tac +| "rewrite" "*" orient one_term "at" occurrences by_arg_tac +| "rewrite" "*" orient one_term by_arg_tac +| "refine" one_term +| "simple" "refine" one_term +| "notypeclasses" "refine" one_term +| "simple" "notypeclasses" "refine" one_term | "solve_constraints" | "subst" LIST1 ident | "subst" | "simple" "subst" | "evar" "(" ident ":" term ")" -| "evar" term1_extended +| "evar" one_term | "instantiate" "(" ident ":=" term ")" | "instantiate" "(" int ":=" term ")" hloc | "instantiate" -| "stepl" term1_extended "by" ltac_expr -| "stepl" term1_extended -| "stepr" term1_extended "by" ltac_expr -| "stepr" term1_extended +| "stepl" one_term "by" ltac_expr +| "stepl" one_term +| "stepr" one_term "by" ltac_expr +| "stepr" one_term | "generalize_eqs" ident | "dependent" "generalize_eqs" ident | "generalize_eqs_vars" ident | "dependent" "generalize_eqs_vars" ident | "specialize_eqs" ident -| "hresolve_core" "(" ident ":=" term1_extended ")" "at" int_or_var "in" term1_extended -| "hresolve_core" "(" ident ":=" term1_extended ")" "in" term1_extended +| "hresolve_core" "(" ident ":=" one_term ")" "at" int_or_var "in" one_term +| "hresolve_core" "(" ident ":=" one_term ")" "in" one_term | "hget_evar" int_or_var | "destauto" | "destauto" "in" ident | "transparent_abstract" ltac_expr3 | "transparent_abstract" ltac_expr3 "using" ident -| "constr_eq" term1_extended term1_extended -| "constr_eq_strict" term1_extended term1_extended -| "constr_eq_nounivs" term1_extended term1_extended -| "is_evar" term1_extended -| "has_evar" term1_extended -| "is_var" term1_extended -| "is_fix" term1_extended -| "is_cofix" term1_extended -| "is_ind" term1_extended -| "is_constructor" term1_extended -| "is_proj" term1_extended -| "is_const" term1_extended +| "constr_eq" one_term one_term +| "constr_eq_strict" one_term one_term +| "constr_eq_nounivs" one_term one_term +| "is_evar" one_term +| "has_evar" one_term +| "is_var" one_term +| "is_fix" one_term +| "is_cofix" one_term +| "is_ind" one_term +| "is_constructor" one_term +| "is_proj" one_term +| "is_const" one_term | "shelve" | "shelve_unifiable" | "unshelve" ltac_expr1 @@ -1466,7 +1462,7 @@ simple_tactic: [ | "swap" int_or_var int_or_var | "revgoals" | "guard" int_or_var comparison int_or_var -| "decompose" "[" LIST1 term1_extended "]" term1_extended +| "decompose" "[" LIST1 one_term "]" one_term | "optimize_heap" | "start" "ltac" "profiling" | "stop" "ltac" "profiling" @@ -1478,14 +1474,14 @@ simple_tactic: [ | "finish_timing" OPT string | "finish_timing" "(" string ")" OPT string | "eassumption" -| "eexact" term1_extended +| "eexact" one_term | "trivial" auto_using hintbases | "info_trivial" auto_using hintbases | "debug" "trivial" auto_using hintbases | "auto" OPT int_or_var auto_using hintbases | "info_auto" OPT int_or_var auto_using hintbases | "debug" "auto" OPT int_or_var auto_using hintbases -| "prolog" "[" LIST0 term1_extended "]" int_or_var +| "prolog" "[" LIST0 one_term "]" int_or_var | "eauto" OPT int_or_var OPT int_or_var auto_using hintbases | "new" "auto" OPT int_or_var auto_using hintbases | "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases @@ -1494,17 +1490,17 @@ simple_tactic: [ | "autounfold" hintbases clause_dft_concl | "autounfold_one" hintbases "in" ident | "autounfold_one" hintbases -| "unify" term1_extended term1_extended -| "unify" term1_extended term1_extended "with" ident -| "convert_concl_no_check" term1_extended +| "unify" one_term one_term +| "unify" one_term one_term "with" ident +| "convert_concl_no_check" one_term | "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 ident | "typeclasses" "eauto" OPT int_or_var "with" LIST1 ident | "typeclasses" "eauto" OPT int_or_var -| "head_of_constr" ident term1_extended -| "not_evar" term1_extended -| "is_ground" term1_extended -| "autoapply" term1_extended "using" ident -| "autoapply" term1_extended "with" ident +| "head_of_constr" ident one_term +| "not_evar" one_term +| "is_ground" one_term +| "autoapply" one_term "using" ident +| "autoapply" one_term "with" ident | "progress_evars" ltac_expr | "rewrite_strat" rewstrategy | "rewrite_db" ident "in" ident @@ -1518,10 +1514,10 @@ simple_tactic: [ | "setoid_symmetry" | "setoid_symmetry" "in" ident | "setoid_reflexivity" -| "setoid_transitivity" term1_extended +| "setoid_transitivity" one_term | "setoid_etransitivity" | "decide" "equality" -| "compare" term1_extended term1_extended +| "compare" one_term one_term | "rewrite_strat" rewstrategy "in" ident | "intros" intropattern_list_opt | "eintros" intropattern_list_opt @@ -1536,41 +1532,43 @@ simple_tactic: [ | "fix" ident num "with" LIST1 fixdecl | "cofix" ident "with" LIST1 cofixdecl | "pose" bindings_with_parameters -| "pose" term1_extended as_name +| "pose" one_term as_name | "epose" bindings_with_parameters -| "epose" term1_extended as_name +| "epose" one_term as_name | "set" bindings_with_parameters clause_dft_concl -| "set" term1_extended as_name clause_dft_concl +| "set" one_term as_name clause_dft_concl | "eset" bindings_with_parameters clause_dft_concl -| "eset" term1_extended as_name clause_dft_concl -| "remember" term1_extended as_name eqn_ipat clause_dft_all -| "eremember" term1_extended as_name eqn_ipat clause_dft_all +| "eset" one_term as_name clause_dft_concl +| "remember" one_term as_name eqn_ipat clause_dft_all +| "eremember" one_term as_name eqn_ipat clause_dft_all | "assert" "(" ident ":=" term ")" | "eassert" "(" ident ":=" term ")" | "assert" "(" ident ":" term ")" by_tactic | "eassert" "(" ident ":" term ")" by_tactic | "enough" "(" ident ":" term ")" by_tactic | "eenough" "(" ident ":" term ")" by_tactic -| "assert" term1_extended as_ipat by_tactic -| "eassert" term1_extended as_ipat by_tactic +| "assert" one_term as_ipat by_tactic +| "eassert" one_term as_ipat by_tactic +| "pose" "proof" "(" ident ":=" term ")" +| "epose" "proof" "(" ident ":=" term ")" | "pose" "proof" term as_ipat | "epose" "proof" term as_ipat -| "enough" term1_extended as_ipat by_tactic -| "eenough" term1_extended as_ipat by_tactic -| "generalize" term1_extended -| "generalize" term1_extended LIST1 term1_extended -| "generalize" term1_extended OPT ( "at" occs_nums ) as_name LIST0 [ "," pattern_occ as_name ] +| "enough" one_term as_ipat by_tactic +| "eenough" one_term as_ipat by_tactic +| "generalize" one_term +| "generalize" one_term LIST1 one_term +| "generalize" one_term OPT ( "at" occs_nums ) as_name LIST0 [ "," pattern_occ as_name ] | "induction" induction_clause_list | "einduction" induction_clause_list | "destruct" induction_clause_list | "edestruct" induction_clause_list | "rewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic | "erewrite" LIST1 oriented_rewriter SEP "," clause_dft_concl by_tactic -| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" term1_extended ] +| "dependent" [ "simple" "inversion" | "inversion" | "inversion_clear" ] quantified_hypothesis as_or_and_ipat OPT [ "with" one_term ] | "simple" "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list | "inversion" quantified_hypothesis as_or_and_ipat in_hyp_list | "inversion_clear" quantified_hypothesis as_or_and_ipat in_hyp_list -| "inversion" quantified_hypothesis "using" term1_extended in_hyp_list +| "inversion" quantified_hypothesis "using" one_term in_hyp_list | "red" clause_dft_concl | "hnf" clause_dft_concl | "simpl" OPT delta_flag OPT ref_or_pattern_occ clause_dft_concl @@ -1581,7 +1579,7 @@ simple_tactic: [ | "vm_compute" OPT ref_or_pattern_occ clause_dft_concl | "native_compute" OPT ref_or_pattern_occ clause_dft_concl | "unfold" LIST1 unfold_occ SEP "," clause_dft_concl -| "fold" LIST1 term1_extended clause_dft_concl +| "fold" LIST1 one_term clause_dft_concl | "pattern" LIST1 pattern_occ SEP "," clause_dft_concl | "change" conversion clause_dft_concl | "change_no_check" conversion clause_dft_concl @@ -1589,16 +1587,16 @@ simple_tactic: [ | "rtauto" | "congruence" | "congruence" int -| "congruence" "with" LIST1 term1_extended -| "congruence" int "with" LIST1 term1_extended +| "congruence" "with" LIST1 one_term +| "congruence" int "with" LIST1 one_term | "f_equal" | "firstorder" OPT ltac_expr firstorder_using | "firstorder" OPT ltac_expr "with" LIST1 ident | "firstorder" OPT ltac_expr firstorder_using "with" LIST1 ident | "gintuition" OPT ltac_expr | "functional" "inversion" quantified_hypothesis OPT qualid (* funind plugin *) -| "functional" "induction" LIST1 term1_extended fun_ind_using with_names (* funind plugin *) -| "soft" "functional" "induction" LIST1 term1_extended fun_ind_using with_names (* funind plugin *) +| "functional" "induction" LIST1 one_term fun_ind_using with_names (* funind plugin *) +| "soft" "functional" "induction" LIST1 one_term fun_ind_using with_names (* funind plugin *) | "psatz_Z" int_or_var ltac_expr (* micromega plugin *) | "psatz_Z" ltac_expr (* micromega plugin *) | "xlia" ltac_expr (* micromega plugin *) @@ -1614,16 +1612,17 @@ simple_tactic: [ | "psatz_R" ltac_expr (* micromega plugin *) | "psatz_Q" int_or_var ltac_expr (* micromega plugin *) | "psatz_Q" ltac_expr (* micromega plugin *) -| "zify_iter_specs" ltac_expr (* micromega plugin *) +| "zify_iter_specs" (* micromega plugin *) | "zify_op" (* micromega plugin *) | "zify_saturate" (* micromega plugin *) | "zify_iter_let" ltac_expr (* micromega plugin *) -| "nsatz_compute" term1_extended (* nsatz plugin *) +| "zify_elim_let" (* micromega plugin *) +| "nsatz_compute" one_term (* nsatz plugin *) | "omega" (* omega plugin *) | "protect_fv" string "in" ident (* setoid_ring plugin *) | "protect_fv" string (* setoid_ring plugin *) -| "ring_lookup" ltac_expr0 "[" LIST0 term1_extended "]" LIST1 term1_extended (* setoid_ring plugin *) -| "field_lookup" ltac_expr "[" LIST0 term1_extended "]" LIST1 term1_extended (* setoid_ring plugin *) +| "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* setoid_ring plugin *) +| "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* setoid_ring plugin *) ] hloc: [ @@ -1646,11 +1645,23 @@ by_arg_tac: [ ] in_clause: [ -| in_clause +| LIST0 hypident_occ SEP "," OPT ( "|-" OPT concl_occ ) +| "*" "|-" OPT concl_occ | "*" OPT ( "at" occs_nums ) -| "*" "|-" concl_occ -| LIST0 hypident_occ SEP "," "|-" concl_occ -| LIST0 hypident_occ SEP "," +] + +concl_occ: [ +| "*" OPT ( "at" occs_nums ) +] + +hypident_occ: [ +| hypident OPT ( "at" occs_nums ) +] + +hypident: [ +| ident +| "(" "type" "of" ident ")" +| "(" "value" "of" ident ")" ] as_ipat: [ @@ -1707,7 +1718,7 @@ induction_clause_list: [ ] auto_using: [ -| "using" LIST1 term1_extended SEP "," +| "using" LIST1 one_term SEP "," | ] @@ -1762,7 +1773,7 @@ simple_binding: [ bindings: [ | LIST1 simple_binding -| LIST1 term1_extended +| LIST1 one_term ] comparison: [ @@ -1783,16 +1794,6 @@ bindings_with_parameters: [ | "(" ident LIST0 simple_binder ":=" term ")" ] -hypident: [ -| ident -| "(" "type" "of" ident ")" -| "(" "value" "of" ident ")" -] - -hypident_occ: [ -| hypident OPT ( "at" occs_nums ) -] - clause_dft_concl: [ | "in" in_clause | OPT ( "at" occs_nums ) @@ -1810,11 +1811,6 @@ opt_clause: [ | ] -concl_occ: [ -| "*" OPT ( "at" occs_nums ) -| -] - in_hyp_list: [ | "in" LIST1 ident | @@ -1844,7 +1840,7 @@ cofixdecl: [ ] constr_with_bindings: [ -| term1_extended with_bindings +| one_term with_bindings ] with_bindings: [ @@ -1869,9 +1865,9 @@ quantified_hypothesis: [ ] conversion: [ -| term1_extended -| term1_extended "with" term1_extended -| term1_extended "at" occs_nums "with" term1_extended +| one_term +| one_term "with" one_term +| one_term "at" occs_nums "with" one_term ] firstorder_using: [ @@ -1897,29 +1893,29 @@ occurrences: [ ] rewstrategy: [ -| term1_extended -| "<-" term1_extended -| "subterms" rewstrategy -| "subterm" rewstrategy -| "innermost" rewstrategy -| "outermost" rewstrategy -| "bottomup" rewstrategy -| "topdown" rewstrategy -| "id" +| one_term +| "<-" one_term | "fail" +| "id" | "refl" | "progress" rewstrategy | "try" rewstrategy -| "any" rewstrategy -| "repeat" rewstrategy | rewstrategy ";" rewstrategy -| "(" rewstrategy ")" | "choice" rewstrategy rewstrategy -| "old_hints" ident +| "repeat" rewstrategy +| "any" rewstrategy +| "subterm" rewstrategy +| "subterms" rewstrategy +| "innermost" rewstrategy +| "outermost" rewstrategy +| "bottomup" rewstrategy +| "topdown" rewstrategy | "hints" ident -| "terms" LIST0 term1_extended +| "terms" LIST0 one_term | "eval" red_expr -| "fold" term1_extended +| "fold" one_term +| "(" rewstrategy ")" +| "old_hints" ident ] ltac_expr: [ @@ -2037,7 +2033,7 @@ tactic_arg: [ | "context" ident "[" term "]" | "type" "of" term | "fresh" LIST0 fresh_id -| "type_term" term1_extended +| "type_term" one_term | "numgoals" ] @@ -2,7 +2,7 @@ (env (dev (flags :standard -rectypes -w -9-27+40+60 \ -short-paths)) (release (flags :standard -rectypes) - (ocamlopt_flags -O3 -unbox-closures)) + (ocamlopt_flags :standard -O3 -unbox-closures)) (ireport (flags :standard -rectypes -w -9-27-40+60) (ocamlopt_flags :standard -O3 -unbox-closures -inlining-report))) diff --git a/ide/coqide.ml b/ide/coqide.ml index 61e95c21b1..553b834a37 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -244,6 +244,13 @@ let close_and_quit () = List.iter (fun sn -> Coq.close_coqtop sn.coqtop) notebook#pages; exit 0 +(* Work around a deadlock due to OCaml exit cleanup. The standard [exit] + function calls [flush_all], which can block if one of the opened channels is + not valid anymore. We do not register [at_exit] functions in CoqIDE, so + instead of flushing we simply die as gracefully as possible in the function + below. *) +external sys_exit : int -> 'a = "caml_sys_exit" + let crash_save exitcode = Minilib.log "Starting emergency save of buffers in .crashcoqide files"; let idx = @@ -263,7 +270,7 @@ let crash_save exitcode = in List.iter save_session notebook#pages; Minilib.log "End emergency save"; - exit exitcode + sys_exit exitcode end diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 31dd26d2ba..13ee353c6b 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -295,20 +295,14 @@ let abstract_projection ~params expmod hyps t = t let cook_one_ind ~ntypes - (section_decls,_ as hyps) expmod mip = + hyps expmod mip = let mind_arity = match mip.mind_arity with | RegularArity {mind_user_arity=arity;mind_sort=sort} -> let arity = abstract_as_type (expmod arity) hyps in let sort = destSort (expmod (mkSort sort)) in RegularArity {mind_user_arity=arity; mind_sort=sort} - | TemplateArity {template_param_levels=levels;template_level;template_context} -> - let sec_levels = CList.map_filter (fun d -> - if RelDecl.is_local_assum d then Some None - else None) - section_decls - in - let levels = List.rev_append sec_levels levels in - TemplateArity {template_param_levels=levels;template_level;template_context} + | TemplateArity {template_level} -> + TemplateArity {template_level} in let mind_arity_ctxt = let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in @@ -386,6 +380,17 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib = in Some (Array.append newvariance variance), Some sec_variance in + let mind_template = match mib.mind_template with + | None -> None + | Some {template_param_levels=levels; template_context} -> + let sec_levels = CList.map_filter (fun d -> + if RelDecl.is_local_assum d then Some None + else None) + section_decls + in + let levels = List.rev_append sec_levels levels in + Some {template_param_levels=levels; template_context} + in { mind_packets; mind_record; @@ -396,6 +401,7 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib = mind_nparams_rec = mib.mind_nparams_rec + nnewparams; mind_params_ctxt; mind_universes; + mind_template; mind_variance; mind_sec_variance; mind_private = mib.mind_private; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index ac130d018d..11a07ee5cf 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -30,8 +30,11 @@ type engagement = set_predicativity *) type template_arity = { - template_param_levels : Univ.Level.t option list; template_level : Univ.Universe.t; +} + +type template_universes = { + template_param_levels : Univ.Level.t option list; template_context : Univ.ContextSet.t; } @@ -218,6 +221,8 @@ type mutual_inductive_body = { mind_universes : universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) + mind_template : template_universes option; + mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *) mind_sec_variance : Univ.Variance.t array option; diff --git a/kernel/declareops.ml b/kernel/declareops.ml index a3adac7a11..a1122d1279 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -46,9 +46,10 @@ let map_decl_arity f g = function | TemplateArity a -> TemplateArity (g a) let hcons_template_arity ar = + { template_level = Univ.hcons_univ ar.template_level; } + +let hcons_template_universe ar = { template_param_levels = ar.template_param_levels; - (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *) - template_level = Univ.hcons_univ ar.template_level; template_context = Univ.hcons_universe_context_set ar.template_context } let universes_context = function @@ -247,6 +248,7 @@ let subst_mind_body sub mib = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ; mind_universes = mib.mind_universes; + mind_template = mib.mind_template; mind_variance = mib.mind_variance; mind_sec_variance = mib.mind_sec_variance; mind_private = mib.mind_private; @@ -323,6 +325,7 @@ let hcons_mind mib = { mib with mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; + mind_template = Option.Smart.map hcons_template_universe mib.mind_template; mind_universes = hcons_universes mib.mind_universes } (** Hashconsing of modules *) diff --git a/kernel/entries.ml b/kernel/entries.ml index 8d930b521c..983fa822e9 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -37,7 +37,6 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1]; type one_inductive_entry = { mind_entry_typename : Id.t; mind_entry_arity : constr; - mind_entry_template : bool; (* Use template polymorphism *) mind_entry_consnames : Id.t list; mind_entry_lc : constr list } @@ -50,6 +49,7 @@ type mutual_inductive_entry = { mind_entry_params : Constr.rel_context; mind_entry_inds : one_inductive_entry list; mind_entry_universes : universes_entry; + mind_entry_template : bool; (* Use template polymorphism *) mind_entry_cumulative : bool; (* universe constraints and the constraints for subtyping of inductive types in the block. *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 501ac99ff3..1b5a77cc96 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -590,11 +590,11 @@ let template_polymorphic_ind (mind,i) env = | TemplateArity _ -> true | RegularArity _ -> false -let template_polymorphic_variables (mind,i) env = - match (lookup_mind mind env).mind_packets.(i).mind_arity with - | TemplateArity { Declarations.template_param_levels = l; _ } -> +let template_polymorphic_variables (mind, _) env = + match (lookup_mind mind env).mind_template with + | Some { Declarations.template_param_levels = l; _ } -> List.map_filter (fun level -> level) l - | RegularArity _ -> [] + | None -> [] let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index cc15109f06..d5aadd0c02 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -101,10 +101,10 @@ let check_indices_matter env_params info indices = else check_context_univs ~ctor:false env_params info indices (* env_ar contains the inductives before the current ones in the block, and no parameters *) -let check_arity env_params env_ar ind = +let check_arity ~template env_params env_ar ind = let {utj_val=arity;utj_type=_} = Typeops.infer_type env_params ind.mind_entry_arity in let indices, ind_sort = Reduction.dest_arity env_params arity in - let ind_min_univ = if ind.mind_entry_template then Some Universe.type0m else None in + let ind_min_univ = if template then Some Universe.type0m else None in let univ_info = { ind_squashed=false; ind_has_relevant_arg=false; @@ -200,28 +200,88 @@ let unbounded_from_below u cstrs = let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl = let check_level l = Univ.LSet.mem l (Univ.ContextSet.levels uctx) && + (let () = assert (not @@ Univ.Level.is_small l) in true) && unbounded_from_below l (Univ.ContextSet.constraints uctx) && not (Univ.LSet.mem l ctor_levels) in let univs = Univ.Universe.levels concl in - let univs = - Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs - in + let univs = Univ.LSet.filter (fun l -> check_level l) univs in let fold acc = function | (LocalAssum (_, p)) -> (let c = Term.strip_prod_assum p in match kind c with | Sort (Type u) -> (match Univ.Universe.level u with - | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None + | Some l -> if Univ.LSet.mem l univs then Some l else None | None -> None) | _ -> None) :: acc | LocalDef _ -> acc in let params = List.fold_left fold [] paramsctxt in - params, univs + if Universe.is_type0m concl then Some (univs, params) + else if not @@ Univ.LSet.is_empty univs then Some (univs, params) + else None + +let get_param_levels ctx params arity splayed_lc = + let min_univ = match arity with + | RegularArity _ -> + CErrors.user_err + Pp.(strbrk "Ill-formed template mutual inductive declaration: all types must be template.") + | TemplateArity ar -> ar.template_level + in + let ctor_levels = + let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in + let param_levels = + List.fold_left (fun levels d -> match d with + | LocalAssum _ -> levels + | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) + Univ.LSet.empty params + in + Array.fold_left + (fun levels (d,c) -> + let levels = + List.fold_left (fun levels d -> + Context.Rel.Declaration.fold_constr add_levels d levels) + levels d + in + add_levels c levels) + param_levels + splayed_lc + in + match template_polymorphic_univs ~ctor_levels ctx params min_univ with + | None -> + CErrors.user_err + Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") + | Some (_, param_levels) -> + param_levels + +let get_template univs params data = + let ctx = match univs with + | Monomorphic ctx -> ctx + | Polymorphic _ -> + CErrors.anomaly ~label:"polymorphic_template_ind" + Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in + (* For each type in the block, compute potential template parameters *) + let params = List.map (fun ((arity, _), (_, splayed_lc), _) -> get_param_levels ctx params arity splayed_lc) data in + (* Pick the lower bound of template parameters. Note that in particular, if + one of the the inductive types from the block is Prop-valued, then no + parameters are template. *) + let fold min params = + let map u v = match u, v with + | (None, _) | (_, None) -> None + | Some u, Some v -> + let () = assert (Univ.Level.equal u v) in + Some u + in + List.map2 map min params + in + let params = match params with + | [] -> assert false + | hd :: rem -> List.fold_left fold hd rem + in + { template_param_levels = params; template_context = ctx } -let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = +let abstract_packets usubst ((arity,lc),(indices,splayed_lc),univ_info) = if not (Universe.Set.is_empty univ_info.missing) then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ))); let arity = Vars.subst_univs_level_constr usubst arity in @@ -237,40 +297,7 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i let arity = match univ_info.ind_min_univ with | None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ} - | Some min_univ -> - let ctx = match univs with - | Monomorphic ctx -> ctx - | Polymorphic _ -> - CErrors.anomaly ~label:"polymorphic_template_ind" - Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in - let ctor_levels = - let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in - let param_levels = - List.fold_left (fun levels d -> match d with - | LocalAssum _ -> levels - | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) - Univ.LSet.empty params - in - Array.fold_left - (fun levels (d,c) -> - let levels = - List.fold_left (fun levels d -> - Context.Rel.Declaration.fold_constr add_levels d levels) - levels d - in - add_levels c levels) - param_levels - splayed_lc - in - let param_levels, concl_levels = - template_polymorphic_univs ~ctor_levels ctx params min_univ - in - if List.for_all (fun x -> Option.is_empty x) param_levels - && Univ.LSet.is_empty concl_levels then - CErrors.user_err - Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") - else - TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx } + | Some min_univ -> TemplateArity { template_level = min_univ; } in let kelim = allowed_sorts univ_info in @@ -285,7 +312,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = mind_check_names mie; assert (List.is_empty (Environ.rel_context env)); - let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in + let has_template_poly = mie.mind_entry_template in (* universes *) let env_univs = @@ -306,7 +333,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = let env_params, params = Typeops.check_context env_univs mie.mind_entry_params in (* Arities *) - let env_ar, data = List.fold_left_map (check_arity env_params) env_univs mie.mind_entry_inds in + let env_ar, data = List.fold_left_map (check_arity ~template:has_template_poly env_params) env_univs mie.mind_entry_inds in let env_ar_par = push_rel_context params env_ar in (* Constructors *) @@ -352,7 +379,14 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in let params = Vars.subst_univs_level_context usubst params in - let data = List.map (abstract_packets univs usubst params) data in + let data = List.map (abstract_packets usubst) data in + let template = + let check ((arity, _), _, _) = match arity with + | TemplateArity _ -> true + | RegularArity _ -> false + in + if List.exists check data then Some (get_template univs params data) else None + in let env_ar_par = let ctx = Environ.rel_context env_ar_par in @@ -361,4 +395,4 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = Environ.push_rel_context ctx env in - env_ar_par, univs, variance, record, params, Array.of_list data + env_ar_par, univs, template, variance, record, params, Array.of_list data diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 723ba5459e..babb82c39e 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -29,6 +29,7 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option -> mutual_inductive_entry -> env * universes + * template_universes option * Univ.Variance.t array option * Names.Id.t array option option * Constr.rel_context @@ -44,4 +45,4 @@ val template_polymorphic_univs : Univ.ContextSet.t -> Constr.rel_context -> Univ.Universe.t -> - Univ.Level.t option list * Univ.LSet.t + (Univ.LSet.t * Univ.Level.t option list) option diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b6b8e5265c..58e5e76b61 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -466,7 +466,7 @@ let compute_projections (kn, i as ind) mib = Array.of_list (List.rev rs), Array.of_list (List.rev pbs) -let build_inductive env ~sec_univs names prv univs variance +let build_inductive env ~sec_univs names prv univs template variance paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) @@ -538,6 +538,7 @@ let build_inductive env ~sec_univs names prv univs variance mind_params_ctxt = paramsctxt; mind_packets = packets; mind_universes = univs; + mind_template = template; mind_variance = variance; mind_sec_variance = sec_variance; mind_private = prv; @@ -562,7 +563,7 @@ let build_inductive env ~sec_univs names prv univs variance let check_inductive env ~sec_univs kn mie = (* First type-check the inductive definition *) - let (env_ar_par, univs, variance, record, paramsctxt, inds) = + let (env_ar_par, univs, template, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env ~sec_univs mie in (* Then check positivity conditions *) @@ -575,6 +576,6 @@ let check_inductive env ~sec_univs kn mie = (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds) in (* Build the inductive packets *) - build_inductive env ~sec_univs names mie.mind_entry_private univs variance + build_inductive env ~sec_univs names mie.mind_entry_private univs template variance paramsctxt kn record mie.mind_entry_finite inds nmr recargs diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 1be86f2bf8..6325779675 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -185,8 +185,8 @@ let make_subst = exception SingletonInductiveBecomesProp of Id.t -let instantiate_universes ctx ar args = - let subst = make_subst (ctx,ar.template_param_levels,args) in +let instantiate_universes ctx (templ, ar) args = + let subst = make_subst (ctx,templ.template_param_levels,args) in let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) @@ -215,8 +215,12 @@ let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> + let templ = match mib.mind_template with + | None -> assert false + | Some t -> t + in let ctx = List.rev mip.mind_arity_ctxt in - let ctx,s = instantiate_universes ctx ar paramtyps in + let ctx,s = instantiate_universes ctx (templ, ar) paramtyps in (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. the situation where a non-Prop singleton inductive becomes Prop when applied to Prop params *) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index b690fe1157..90571844b9 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -123,9 +123,6 @@ exception SingletonInductiveBecomesProp of Id.t val max_inductive_sort : Sorts.t array -> Universe.t -val instantiate_universes : Constr.rel_context -> - template_arity -> param_univs -> Constr.rel_context * Sorts.t - (** {6 Debug} *) type size = Large | Strict diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 535b7de121..a37d04d82c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1303,12 +1303,7 @@ let start_library dir senv = required = senv.required } let export ?except ~output_native_objects senv dir = - let senv = - try join_safe_environment ?except senv - with e -> - let e = Exninfo.capture e in - CErrors.user_err ~hdr:"export" (CErrors.iprint e) - in + let senv = join_safe_environment ?except senv in assert(senv.future_cst = []); let () = check_current_library dir senv in let mp = senv.modpath in diff --git a/lib/control.ml b/lib/control.ml index e67e88ee95..1898eab89e 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -75,8 +75,8 @@ let windows_timeout n f x e = if not !exited then begin killed := true; raise Sys.Break end else raise e | e -> - let () = killed := true in let e = Exninfo.capture e in + let () = killed := true in Exninfo.iraise e type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } @@ -201,11 +201,7 @@ let pp_with ft pp = pp_cmd s; pp_close_tag ft () [@warning "-3"] in - try pp_cmd pp - with reraise -> - let reraise = Exninfo.capture reraise in - let () = Format.pp_print_flush ft () in - Exninfo.iraise reraise + pp_cmd pp (* If mixing some output and a goal display, please use msg_warning, so that interfaces (proofgeneral for example) can easily dispatch diff --git a/lib/util.ml b/lib/util.ml index e2447b005e..ae8119ced0 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -82,10 +82,6 @@ module Set = CSet module Map = CMap -(* Stacks *) - -module Stack = CStack - (* Matrices *) let matrix_transpose mat = diff --git a/lib/util.mli b/lib/util.mli index 1417d6dfcb..be0cc11763 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -76,10 +76,6 @@ module Set : module type of CSet module Map : module type of CMap -(** {6 Stacks.} *) - -module Stack : module type of CStack - (** {6 Streams. } *) val stream_nth : int -> 'a Stream.t -> 'a diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 3dc934b426..b0b74f4558 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util open Constr open Names @@ -156,102 +155,6 @@ val subterms : forest -> int -> int * int val join_path : forest -> int -> int -> ((int * int) * equality) list * ((int * int) * equality) list -val make_fun_table : state -> Int.Set.t PafMap.t - -val do_match : state -> - (quant_eq * int array) list ref -> matching_problem Stack.t -> unit - -val init_pb_stack : state -> matching_problem Stack.t - -val paf_of_patt : int Termhash.t -> ccpattern -> pa_fun - -val find_instances : state -> (quant_eq * int array) list - val execute : bool -> state -> explanation option val pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t - -val empty_forest: unit -> forest - - - - - - - - - - -(*type pa_constructor - - -module PacMap:CSig.MapS with type key=pa_constructor - -type term = - Symb of Term.constr - | Eps - | Appli of term * term - | Constructor of Names.constructor*int*int - -type rule = - Congruence - | Axiom of Names.Id.t - | Injection of int*int*int*int - -type equality = - {lhs : int; - rhs : int; - rule : rule} - -module ST : -sig - type t - val empty : unit -> t - val enter : int -> int * int -> t -> unit - val query : int * int -> t -> int - val delete : int -> t -> unit - val delete_list : int list -> t -> unit -end - -module UF : -sig - type t - exception Discriminable of int * int * int * int * t - val empty : unit -> t - val find : t -> int -> int - val size : t -> int -> int - val get_constructor : t -> int -> Names.constructor - val pac_arity : t -> int -> int * int -> int - val mem_node_pac : t -> int -> int * int -> int - val add_pacs : t -> int -> pa_constructor PacMap.t -> - int list * equality list - val term : t -> int -> term - val subterms : t -> int -> int * int - val add : t -> term -> int - val union : t -> int -> int -> equality -> int list * equality list - val join_path : t -> int -> int -> - ((int*int)*equality) list* - ((int*int)*equality) list -end - - -val combine_rec : UF.t -> int list -> equality list -val process_rec : UF.t -> equality list -> int list - -val cc : UF.t -> unit - -val make_uf : - (Names.Id.t * (term * term)) list -> UF.t - -val add_one_diseq : UF.t -> (term * term) -> int * int - -val add_disaxioms : - UF.t -> (Names.Id.t * (term * term)) list -> - (Names.Id.t * (int * int)) list - -val check_equal : UF.t -> int * int -> bool - -val find_contradiction : UF.t -> - (Names.Id.t * (int * int)) list -> - (Names.Id.t * (int * int)) -*) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 45fafd2872..7d87fc0220 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -92,18 +92,14 @@ let list_union_eq eq_fun l1 l2 = let list_add_set_eq eq_fun x l = if List.exists (eq_fun x) l then l else x::l -[@@@ocaml.warning "-3"] -let coq_constant s = - UnivGen.constr_of_monomorphic_global @@ - Coqlib.gen_reference_in_modules "RecursiveDefinition" - Coqlib.init_modules s;; +let coq_constant s = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref s;; let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in Nametab.locate (make_qualid dp (Id.of_string s)) -let eq = lazy(EConstr.of_constr (coq_constant "eq")) -let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl")) +let eq = lazy(EConstr.of_constr (coq_constant "core.eq.type")) +let refl_equal = lazy(EConstr.of_constr (coq_constant "core.eq.refl")) let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () @@ -369,10 +365,10 @@ let do_observe_tac s tac g = ignore(Stack.pop debug_queue); v with reraise -> - let reraise = CErrors.push reraise in + let reraise = Exninfo.capture reraise in if not (Stack.is_empty debug_queue) then print_debug_queue true (fst reraise); - Util.iraise reraise + Exninfo.iraise reraise let observe_tac s tac g = if do_observe () @@ -447,14 +443,11 @@ let h_intros l = let h_id = Id.of_string "h" let hrec_id = Id.of_string "hrec" -let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded") -let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") -let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") - -[@@@ocaml.warning "-3"] -let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ - Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof" -[@@@ocaml.warning "+3"] +let well_founded = function () -> EConstr.of_constr (coq_constant "core.wf.well_founded") +let acc_rel = function () -> EConstr.of_constr (coq_constant "core.wf.acc") +let acc_inv_id = function () -> EConstr.of_constr (coq_constant "core.wf.acc_inv") + +let well_founded_ltof () = EConstr.of_constr (coq_constant "num.nat.well_founded_ltof") let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f7f8004998..9fa0ec8c08 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -47,18 +47,12 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) -[@@@ocaml.warning "-3"] -let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ - Coqlib.find_reference "RecursiveDefinition" m s - -let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"] -let arith_Lt = ["Coq"; "Arith";"Lt"] +let coq_constant s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ + Coqlib.lib_ref s let coq_init_constant s = - EConstr.of_constr ( - UnivGen.constr_of_monomorphic_global @@ - Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) -[@@@ocaml.warning "+3"] + EConstr.of_constr(UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref s) +;; let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in @@ -122,26 +116,26 @@ let v_id = Id.of_string "v" let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; -let lt = function () -> (coq_init_constant "lt") -[@@@ocaml.warning "-3"] -let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") -let ex = function () -> (coq_init_constant "ex") -let nat = function () -> (coq_init_constant "nat") +let lt = function () -> (coq_init_constant "num.nat.lt") +let le = function () -> Coqlib.lib_ref "num.nat.le" + +let ex = function () -> (coq_init_constant "core.ex.type") +let nat = function () -> (coq_init_constant "num.nat.type") let iter_ref () = try find_reference ["Recdef"] "iter" with Not_found -> user_err Pp.(str "module Recdef not loaded") let iter_rd = function () -> (constr_of_monomorphic_global (delayed_force iter_ref)) -let eq = function () -> (coq_init_constant "eq") +let eq = function () -> (coq_init_constant "core.eq.type") let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") -let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm") -let le_trans = function () -> (coq_constant arith_Nat "le_trans") -let le_lt_trans = function () -> (coq_constant arith_Nat "le_lt_trans") -let lt_S_n = function () -> (coq_constant arith_Lt "lt_S_n") -let le_n = function () -> (coq_init_constant "le_n") +let le_lt_n_Sm = function () -> (coq_constant "num.nat.le_lt_n_Sm") +let le_trans = function () -> (coq_constant "num.nat.le_trans") +let le_lt_trans = function () -> (coq_constant "num.nat.le_lt_trans") +let lt_S_n = function () -> (coq_constant "num.nat.lt_S_n") +let le_n = function () -> (coq_init_constant "num.nat.le_n") let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig") -let coq_O = function () -> (coq_init_constant "O") -let coq_S = function () -> (coq_init_constant "S") -let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r") +let coq_O = function () -> (coq_init_constant "num.nat.O") +let coq_S = function () -> (coq_init_constant"num.nat.S") +let lt_n_O = function () -> (coq_constant "num.nat.nlt_0_r") let max_ref = function () -> (find_reference ["Recdef"] "max") let max_constr = function () -> EConstr.of_constr (constr_of_monomorphic_global (delayed_force max_ref)) @@ -817,7 +811,7 @@ let rec prove_le g = | App (c, [| x0 ; _ |]) -> EConstr.isVar sigma x0 && Id.equal (destVar sigma x0) (destVar sigma x) && - EConstr.is_global sigma (le ()) c + EConstr.isRefX sigma (le ()) c | _ -> false in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in @@ -1194,7 +1188,7 @@ let get_current_subgoals_types pstate = exception EmptySubgoals let build_and_l sigma l = let and_constr = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in - let conj_constr = Coqlib.build_coq_conj () in + let conj_constr = Coqlib.lib_ref "core.and.conj" in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in let rec is_well_founded t = diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index e946ffd8bc..c788c7f147 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -19,12 +19,13 @@ let debug = false -open Big_int -open Num open Polynomial module Mc = Micromega module Ml2C = Mutils.CamlToCoq module C2Ml = Mutils.CoqToCaml +open NumCompat +open Q.Notations +open Mutils let use_simplex = ref true @@ -32,11 +33,9 @@ type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown type zres = (Mc.zArithProof, int * Mc.z list) res type qres = (Mc.q Mc.psatz, int * Mc.q list) res -open Mutils - type 'a number_spec = - { bigint_to_number : big_int -> 'a - ; number_to_num : 'a -> num + { bigint_to_number : Z.t -> 'a + ; number_to_num : 'a -> Q.t ; zero : 'a ; unit : 'a ; mult : 'a -> 'a -> 'a @@ -44,7 +43,7 @@ type 'a number_spec = let z_spec = { bigint_to_number = Ml2C.bigint - ; number_to_num = (fun x -> Big_int (C2Ml.z_big_int x)) + ; number_to_num = (fun x -> Q.of_bigint (C2Ml.z_big_int x)) ; zero = Mc.Z0 ; unit = Mc.Zpos Mc.XH ; mult = Mc.Z.mul @@ -124,17 +123,16 @@ let constrain_variable v l = let coeffs = List.fold_left (fun acc p -> Vect.get v p.coeffs :: acc) [] l in { coeffs = Vect.from_list - (Big_int zero_big_int :: Big_int zero_big_int :: List.rev coeffs) + (Q.of_bigint Z.zero :: Q.of_bigint Z.zero :: List.rev coeffs) ; op = Eq - ; cst = Big_int zero_big_int } + ; cst = Q.of_bigint Z.zero } let constrain_constant l = - let coeffs = List.fold_left (fun acc p -> minus_num p.cst :: acc) [] l in + let coeffs = List.fold_left (fun acc p -> Q.neg p.cst :: acc) [] l in { coeffs = - Vect.from_list - (Big_int zero_big_int :: Big_int unit_big_int :: List.rev coeffs) + Vect.from_list (Q.of_bigint Z.zero :: Q.of_bigint Z.one :: List.rev coeffs) ; op = Eq - ; cst = Big_int zero_big_int } + ; cst = Q.of_bigint Z.zero } let positivity l = let rec xpositivity i l = @@ -144,16 +142,16 @@ let positivity l = match c.op with | Eq -> xpositivity (i + 1) l | _ -> - { coeffs = Vect.update (i + 1) (fun _ -> Int 1) Vect.null + { coeffs = Vect.update (i + 1) (fun _ -> Q.one) Vect.null ; op = Ge - ; cst = Int 0 } + ; cst = Q.zero } :: xpositivity (i + 1) l ) in xpositivity 1 l let cstr_of_poly (p, o) = let c, l = Vect.decomp_cst p in - {coeffs = l; op = o; cst = minus_num c} + {coeffs = l; op = o; cst = Q.neg c} let variables_of_cstr c = Vect.variables c.coeffs @@ -175,25 +173,23 @@ let build_dual_linear_system l = let strict = { coeffs = Vect.from_list - ( Big_int zero_big_int :: Big_int unit_big_int + ( Q.of_bigint Z.zero :: Q.of_bigint Z.one :: List.map (fun c -> - if is_strict c then Big_int unit_big_int - else Big_int zero_big_int) + if is_strict c then Q.of_bigint Z.one else Q.of_bigint Z.zero) l ) ; op = Ge - ; cst = Big_int unit_big_int } + ; cst = Q.of_bigint Z.one } in (* Add the positivity constraint *) - { coeffs = Vect.from_list [Big_int zero_big_int; Big_int unit_big_int] + { coeffs = Vect.from_list [Q.of_bigint Z.zero; Q.of_bigint Z.one] ; op = Ge - ; cst = Big_int zero_big_int } + ; cst = Q.of_bigint Z.zero } :: ((strict :: positivity l) @ (c :: s0)) -open Util - (** [direct_linear_prover l] does not handle strict inegalities *) let fourier_linear_prover l = + let open Util in match Mfourier.Fourier.find_point l with | Inr prf -> if debug then Printf.printf "AProof : %a\n" Mfourier.pp_proof prf; @@ -211,6 +207,7 @@ let direct_linear_prover l = else fourier_linear_prover l let find_point l = + let open Util in if !use_simplex then Simplex.find_point l else match Mfourier.Fourier.find_point l with @@ -237,8 +234,8 @@ let dual_raw_certificate l = match Vect.choose cert with | None -> failwith "dual_raw_certificate: empty_certificate" | Some _ -> - (*Some (rats_to_ints (Vect.to_list (Vect.decr_var 2 (Vect.set 1 (Int 0) cert))))*) - Some (Vect.normalise (Vect.decr_var 2 (Vect.set 1 (Int 0) cert))) ) + (*Some (rats_to_ints (Vect.to_list (Vect.decr_var 2 (Vect.set 1 Q.zero cert))))*) + Some (Vect.normalise (Vect.decr_var 2 (Vect.set 1 Q.zero cert))) ) (* should not use rats_to_ints *) with x when CErrors.noncritical x -> if debug then ( @@ -306,14 +303,14 @@ exception FoundProof of ProofFormat.prf_rule let check_int_sat (cstr, prf) = let {coeffs; op; cst} = cstr in match Vect.choose coeffs with - | None -> if eval_op op (Int 0) cst then Tauto else Unsat prf + | None -> if eval_op op Q.zero cst then Tauto else Unsat prf | _ -> ( let gcdi = Vect.gcd coeffs in - let gcd = Big_int gcdi in - if eq_num gcd (Int 1) then Normalise (cstr, prf) - else if Int.equal (sign_num (mod_num cst gcd)) 0 then begin + let gcd = Q.of_bigint gcdi in + if gcd =/ Q.one then Normalise (cstr, prf) + else if Int.equal (Q.sign (Q.mod_ cst gcd)) 0 then begin (* We can really normalise *) - assert (sign_num gcd >= 1); + assert (Q.sign gcd >= 1); let cstr = {coeffs = Vect.div gcd coeffs; op; cst = cst // gcd} in Normalise (cstr, ProofFormat.Gcd (gcdi, prf)) (* Normalise(cstr,CutPrf prf)*) @@ -323,7 +320,7 @@ let check_int_sat (cstr, prf) = | Eq -> Unsat (ProofFormat.CutPrf prf) | Ge -> let cstr = - {coeffs = Vect.div gcd coeffs; op; cst = ceiling_num (cst // gcd)} + {coeffs = Vect.div gcd coeffs; op; cst = Q.ceiling (cst // gcd)} in Cut (cstr, ProofFormat.CutPrf prf) | Gt -> failwith "check_sat : Unexpected operator" ) @@ -351,7 +348,7 @@ let is_linear_for v pc = *) let is_linear_substitution sys ((p, o), prf) = - let pred v = v =/ Int 1 || v =/ Int (-1) in + let pred v = v =/ Q.one || v =/ Q.neg_one in match o with | Eq -> ( match @@ -521,28 +518,31 @@ open Sos_types let rec scale_term t = match t with - | Zero -> (unit_big_int, Zero) - | Const n -> (denominator n, Const (Big_int (numerator n))) - | Var n -> (unit_big_int, Var n) + | Zero -> (Z.one, Zero) + | Const n -> (Q.den n, Const (Q.of_bigint (Q.num n))) + | Var n -> (Z.one, Var n) | Opp t -> let s, t = scale_term t in (s, Opp t) | Add (t1, t2) -> let s1, y1 = scale_term t1 and s2, y2 = scale_term t2 in - let g = gcd_big_int s1 s2 in - let s1' = div_big_int s1 g in - let s2' = div_big_int s2 g in - let e = mult_big_int g (mult_big_int s1' s2') in - if Int.equal (compare_big_int e unit_big_int) 0 then - (unit_big_int, Add (y1, y2)) - else (e, Add (Mul (Const (Big_int s2'), y1), Mul (Const (Big_int s1'), y2))) + let g = Z.gcd s1 s2 in + let s1' = Z.div s1 g in + let s2' = Z.div s2 g in + let e = Z.mul g (Z.mul s1' s2') in + if Int.equal (Z.compare e Z.one) 0 then (Z.one, Add (y1, y2)) + else + ( e + , Add + (Mul (Const (Q.of_bigint s2'), y1), Mul (Const (Q.of_bigint s1'), y2)) + ) | Sub _ -> failwith "scale term: not implemented" | Mul (y, z) -> let s1, y1 = scale_term y and s2, y2 = scale_term z in - (mult_big_int s1 s2, Mul (y1, y2)) + (Z.mul s1 s2, Mul (y1, y2)) | Pow (t, n) -> let s, t = scale_term t in - (power_big_int_positive_int s n, Pow (t, n)) + (Z.power_int s n, Pow (t, n)) let scale_term t = let s, t' = scale_term t in @@ -550,37 +550,38 @@ let scale_term t = let rec scale_certificate pos = match pos with - | Axiom_eq i -> (unit_big_int, Axiom_eq i) - | Axiom_le i -> (unit_big_int, Axiom_le i) - | Axiom_lt i -> (unit_big_int, Axiom_lt i) - | Monoid l -> (unit_big_int, Monoid l) - | Rational_eq n -> (denominator n, Rational_eq (Big_int (numerator n))) - | Rational_le n -> (denominator n, Rational_le (Big_int (numerator n))) - | Rational_lt n -> (denominator n, Rational_lt (Big_int (numerator n))) + | Axiom_eq i -> (Z.one, Axiom_eq i) + | Axiom_le i -> (Z.one, Axiom_le i) + | Axiom_lt i -> (Z.one, Axiom_lt i) + | Monoid l -> (Z.one, Monoid l) + | Rational_eq n -> (Q.den n, Rational_eq (Q.of_bigint (Q.num n))) + | Rational_le n -> (Q.den n, Rational_le (Q.of_bigint (Q.num n))) + | Rational_lt n -> (Q.den n, Rational_lt (Q.of_bigint (Q.num n))) | Square t -> let s, t' = scale_term t in - (mult_big_int s s, Square t') + (Z.mul s s, Square t') | Eqmul (t, y) -> let s1, y1 = scale_term t and s2, y2 = scale_certificate y in - (mult_big_int s1 s2, Eqmul (y1, y2)) + (Z.mul s1 s2, Eqmul (y1, y2)) | Sum (y, z) -> let s1, y1 = scale_certificate y and s2, y2 = scale_certificate z in - let g = gcd_big_int s1 s2 in - let s1' = div_big_int s1 g in - let s2' = div_big_int s2 g in - ( mult_big_int g (mult_big_int s1' s2') + let g = Z.gcd s1 s2 in + let s1' = Z.div s1 g in + let s2' = Z.div s2 g in + ( Z.mul g (Z.mul s1' s2') , Sum - ( Product (Rational_le (Big_int s2'), y1) - , Product (Rational_le (Big_int s1'), y2) ) ) + ( Product (Rational_le (Q.of_bigint s2'), y1) + , Product (Rational_le (Q.of_bigint s1'), y2) ) ) | Product (y, z) -> let s1, y1 = scale_certificate y and s2, y2 = scale_certificate z in - (mult_big_int s1 s2, Product (y1, y2)) + (Z.mul s1 s2, Product (y1, y2)) +module Z_ = Z open Micromega let rec term_to_q_expr = function | Const n -> PEc (Ml2C.q n) - | Zero -> PEc (Ml2C.q (Int 0)) + | Zero -> PEc (Ml2C.q Q.zero) | Var s -> PEX (Ml2C.index (int_of_string (String.sub s 1 (String.length s - 1)))) | Mul (p1, p2) -> PEmul (term_to_q_expr p1, term_to_q_expr p2) @@ -590,8 +591,8 @@ let rec term_to_q_expr = function | Sub (t1, t2) -> PEsub (term_to_q_expr t1, term_to_q_expr t2) let term_to_q_pol e = - Mc.norm_aux (Ml2C.q (Int 0)) (Ml2C.q (Int 1)) Mc.qplus Mc.qmult Mc.qminus - Mc.qopp Mc.qeq_bool (term_to_q_expr e) + Mc.norm_aux (Ml2C.q Q.zero) (Ml2C.q Q.one) Mc.qplus Mc.qmult Mc.qminus Mc.qopp + Mc.qeq_bool (term_to_q_expr e) let rec product l = match l with @@ -606,7 +607,7 @@ let q_cert_of_pos pos = | Axiom_lt i -> Mc.PsatzIn (Ml2C.nat i) | Monoid l -> product l | Rational_eq n | Rational_le n | Rational_lt n -> - if Int.equal (compare_num n (Int 0)) 0 then Mc.PsatzZ + if Int.equal (Q.compare n Q.zero) 0 then Mc.PsatzZ else Mc.PsatzC (Ml2C.q n) | Square t -> Mc.PsatzSquare (term_to_q_pol t) | Eqmul (t, y) -> Mc.PsatzMulC (term_to_q_pol t, _cert_of_pos y) @@ -616,7 +617,7 @@ let q_cert_of_pos pos = simplify_cone q_spec (_cert_of_pos pos) let rec term_to_z_expr = function - | Const n -> PEc (Ml2C.bigint (big_int_of_num n)) + | Const n -> PEc (Ml2C.bigint (Q.to_bigint n)) | Zero -> PEc Z0 | Var s -> PEX (Ml2C.index (int_of_string (String.sub s 1 (String.length s - 1)))) @@ -638,11 +639,11 @@ let z_cert_of_pos pos = | Axiom_lt i -> Mc.PsatzIn (Ml2C.nat i) | Monoid l -> product l | Rational_eq n | Rational_le n | Rational_lt n -> - if Int.equal (compare_num n (Int 0)) 0 then Mc.PsatzZ - else Mc.PsatzC (Ml2C.bigint (big_int_of_num n)) + if Int.equal (Q.compare n Q.zero) 0 then Mc.PsatzZ + else Mc.PsatzC (Ml2C.bigint (Q.to_bigint n)) | Square t -> Mc.PsatzSquare (term_to_z_pol t) | Eqmul (t, y) -> - let is_unit = match t with Const n -> n =/ Int 1 | _ -> false in + let is_unit = match t with Const n -> n =/ Q.one | _ -> false in if is_unit then _cert_of_pos y else Mc.PsatzMulC (term_to_z_pol t, _cert_of_pos y) | Sum (y, z) -> Mc.PsatzAdd (_cert_of_pos y, _cert_of_pos z) @@ -655,8 +656,6 @@ open Mutils Given a constraint, all the coefficients are always integers. *) -open Num -open Big_int open Polynomial type prf_sys = (cstr * ProofFormat.prf_rule) list @@ -674,19 +673,18 @@ let pivot v (c1, p1) (c2, p2) = (ProofFormat.mul_cst_proof cv1 p1) (ProofFormat.mul_cst_proof cv2 p2) ) in - match (Vect.get v v1, Vect.get v v2) with - | Int 0, _ | _, Int 0 -> None - | a, b -> - if Int.equal (sign_num a * sign_num b) (-1) then - let cv1 = abs_num b and cv2 = abs_num a in - Some (xpivot cv1 cv2) - else if op1 == Eq then - let cv1 = minus_num (b */ Int (sign_num a)) and cv2 = abs_num a in - Some (xpivot cv1 cv2) - else if op2 == Eq then - let cv1 = abs_num b and cv2 = minus_num (a */ Int (sign_num b)) in - Some (xpivot cv1 cv2) - else None + let a, b = (Vect.get v v1, Vect.get v v2) in + if a =/ Q.zero || b =/ Q.zero then None + else if Int.equal (Q.sign a * Q.sign b) (-1) then + let cv1 = Q.abs b and cv2 = Q.abs a in + Some (xpivot cv1 cv2) + else if op1 == Eq then + let cv1 = Q.neg (b */ Q.of_int (Q.sign a)) and cv2 = Q.abs a in + Some (xpivot cv1 cv2) + else if op2 == Eq then + let cv1 = Q.abs b and cv2 = Q.neg (a */ Q.of_int (Q.sign b)) in + Some (xpivot cv1 cv2) + else None (* op2 could be Eq ... this might happen *) @@ -705,21 +703,17 @@ let simpl_sys sys = Source: http://en.wikipedia.org/wiki/Extended_Euclidean_algorithm *) let rec ext_gcd a b = - if Int.equal (sign_big_int b) 0 then (unit_big_int, zero_big_int) + if Int.equal (Z_.sign b) 0 then (Z_.one, Z_.zero) else - let q, r = quomod_big_int a b in + let q, r = Z_.quomod a b in let s, t = ext_gcd b r in - (t, sub_big_int s (mult_big_int q t)) + (t, Z_.sub s (Z_.mul q t)) let extract_coprime (c1, p1) (c2, p2) = if c1.op == Eq && c2.op == Eq then Vect.exists2 (fun n1 n2 -> - Int.equal - (compare_big_int - (gcd_big_int (numerator n1) (numerator n2)) - unit_big_int) - 0) + Int.equal (Z_.compare (Z_.gcd (Q.num n1) (Q.num n2)) Z_.one) 0) c1.coeffs c2.coeffs else None @@ -742,8 +736,8 @@ let reduce_coprime psys = match oeq with | None -> None (* Nothing to do *) | Some ((v, n1, n2), (c1, p1), (c2, p2)) -> - let l1, l2 = ext_gcd (numerator n1) (numerator n2) in - let l1' = Big_int l1 and l2' = Big_int l2 in + let l1, l2 = ext_gcd (Q.num n1) (Q.num n2) in + let l1' = Q.of_bigint l1 and l2' = Q.of_bigint l2 in let cstr = { coeffs = Vect.add (Vect.mul l1' c1.coeffs) (Vect.mul l2' c2.coeffs) ; op = Eq @@ -761,7 +755,7 @@ let reduce_unary psys = let is_unary_equation (cstr, prf) = if cstr.op == Eq then Vect.find - (fun v n -> if n =/ Int 1 || n =/ Int (-1) then Some v else None) + (fun v n -> if n =/ Q.one || n =/ Q.neg_one then Some v else None) cstr.coeffs else None in @@ -775,13 +769,12 @@ let reduce_var_change psys = match Vect.choose vect with | None -> None | Some (x, v, vect) -> ( - let v = numerator v in + let v = Q.num v in match Vect.find (fun x' v' -> - let v' = numerator v' in - if eq_big_int (gcd_big_int v v') unit_big_int then Some (x', v') - else None) + let v' = Q.num v' in + if Z_.equal (Z_.gcd v v') Z_.one then Some (x', v') else None) vect with | Some (x', v') -> Some ((x, v), (x', v')) @@ -795,12 +788,12 @@ let reduce_var_change psys = | None -> None | Some (((x, v), (x', v')), (c, p)) -> let l1, l2 = ext_gcd v v' in - let l1, l2 = (Big_int l1, Big_int l2) in + let l1, l2 = (Q.of_bigint l1, Q.of_bigint l2) in let pivot_eq (c', p') = let {coeffs; op; cst} = c' in let vx = Vect.get x coeffs in let vx' = Vect.get x' coeffs in - let m = minus_num ((vx */ l1) +/ (vx' */ l2)) in + let m = Q.neg ((vx */ l1) +/ (vx' */ l2)) in Some ( { coeffs = Vect.add (Vect.mul m c.coeffs) coeffs ; op @@ -818,7 +811,7 @@ let reduction_equations psys = (** [get_bound sys] returns upon success an interval (lb,e,ub) with proofs *) let get_bound sys = let is_small (v, i) = - match Itv.range i with None -> false | Some i -> i <=/ Int 1 + match Itv.range i with None -> false | Some i -> i <=/ Q.one in let select_best (x1, i1) (x2, i2) = if Itv.smaller_itv i1 i2 then (x1, i1) else (x2, i2) @@ -858,18 +851,20 @@ let get_bound sys = in match smallest_interval with | Some (lb, e, ub) -> ( - let lbn, lbd = (sub_big_int (numerator lb) unit_big_int, denominator lb) in - let ubn, ubd = (add_big_int unit_big_int (numerator ub), denominator ub) in + let lbn, lbd = (Z_.sub (Q.num lb) Z_.one, Q.den lb) in + let ubn, ubd = (Z_.add Z_.one (Q.num ub), Q.den ub) in (* x <= ub -> x > ub *) match ( direct_linear_prover - ( {coeffs = Vect.mul (Big_int ubd) e; op = Ge; cst = Big_int ubn} + ( { coeffs = Vect.mul (Q.of_bigint ubd) e + ; op = Ge + ; cst = Q.of_bigint ubn } :: sys ) , (* lb <= x -> lb > x *) direct_linear_prover - ( { coeffs = Vect.mul (minus_num (Big_int lbd)) e + ( { coeffs = Vect.mul (Q.neg (Q.of_bigint lbd)) e ; op = Ge - ; cst = minus_num (Big_int lbn) } + ; cst = Q.neg (Q.of_bigint lbn) } :: sys ) ) with | Some cub, Some clb -> @@ -879,7 +874,7 @@ let get_bound sys = let check_sys sys = List.for_all - (fun (c, p) -> Vect.for_all (fun _ n -> sign_num n <> 0) c.coeffs) + (fun (c, p) -> Vect.for_all (fun _ n -> Q.sign n <> 0) c.coeffs) sys open ProofFormat @@ -896,8 +891,8 @@ let xlia (can_enum : bool) reduction_equations sys = | Some (prf1, (lb, e, ub), prf2) -> ( if debug then Printf.printf "Found interval: %a in [%s;%s] -> " Vect.pp e - (string_of_num lb) (string_of_num ub); - match start_enum id e (ceiling_num lb) (floor_num ub) sys with + (Q.to_string lb) (Q.to_string ub); + match start_enum id e (Q.ceiling lb) (Q.floor ub) sys with | Prf prfl -> Prf (ProofFormat.Enum @@ -916,7 +911,7 @@ let xlia (can_enum : bool) reduction_equations sys = match aux_lia (id + 1) ((eq, ProofFormat.Def id) :: sys) with | Unknown | Model _ -> Unknown | Prf prf -> ( - match start_enum id e (clb +/ Int 1) cub sys with + match start_enum id e (clb +/ Q.one) cub sys with | Prf l -> Prf (prf :: l) | _ -> Unknown ) and aux_lia (id : int) (sys : prf_sys) = @@ -964,7 +959,7 @@ let xlia (can_enum : bool) reduction_equations sys = if Mc.zChecker sys' prf then Some prf else raise Certificate.BadCertificate with Failure s -> (Printf.printf "%s" s ; Some prf) - *) + *) Prf prf let xlia_simplex env red sys = diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 4b656f8e61..c3f59b4208 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -518,7 +518,7 @@ module M = struct | Mc.Zneg p -> EConstr.mkApp (Lazy.force coq_NEG, [|dump_positive p|]) let pp_z o x = - Printf.fprintf o "%s" (Big_int.string_of_big_int (CoqToCaml.z_big_int x)) + Printf.fprintf o "%s" (NumCompat.Z.to_string (CoqToCaml.z_big_int x)) let dump_q q = EConstr.mkApp @@ -636,14 +636,14 @@ module M = struct in pp_pol o e - (* let pp_clause pp_c o (f: 'cst clause) = - List.iter (fun ((p,_),(t,_)) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c) p Tag.pp t) f *) + (* let pp_clause pp_c o (f: 'cst clause) = + List.iter (fun ((p,_),(t,_)) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c) p Tag.pp t) f *) let pp_clause_tag o (f : 'cst clause) = List.iter (fun ((p, _), (t, _)) -> Printf.fprintf o "(_ @%a)" Tag.pp t) f - (* let pp_cnf pp_c o (f:'cst cnf) = - List.iter (fun l -> Printf.fprintf o "[%a]" (pp_clause pp_c) l) f *) + (* let pp_cnf pp_c o (f:'cst cnf) = + List.iter (fun l -> Printf.fprintf o "[%a]" (pp_clause pp_c) l) f *) let pp_cnf_tag o (f : 'cst cnf) = List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause_tag l) f @@ -819,16 +819,16 @@ module M = struct let elements env = env.vars - (* let string_of_env gl env = - let rec string_of_env i env acc = - match env with - | [] -> acc - | e::env -> string_of_env (i+1) env - (IMap.add i - (Pp.string_of_ppcmds - (Printer.pr_econstr_env gl.env gl.sigma e)) acc) in - string_of_env 1 env IMap.empty - *) + (* let string_of_env gl env = + let rec string_of_env i env acc = + match env with + | [] -> acc + | e::env -> string_of_env (i+1) env + (IMap.add i + (Pp.string_of_ppcmds + (Printer.pr_econstr_env gl.env gl.sigma e)) acc) in + string_of_env 1 env IMap.empty + *) let pp gl env = let ppl = List.mapi @@ -951,7 +951,7 @@ module M = struct (* NB: R is a different story. Because it is axiomatised, reducing would not be effective. Therefore, there is a specific parser for constant over R - *) + *) let rconst_assoc = [ (coq_Rplus, fun x y -> Mc.CPlus (x, y)) @@ -1613,14 +1613,14 @@ let compact_proofs (cnf_ff : 'cst cnf) res (cnf_ff' : 'cst cnf) = in List.assoc formula new_cl in - (* if debug then - begin - Printf.printf "\ncompact_proof : %a %a %a" - (pp_ml_list prover.pp_f) (List.map fst old_cl) - prover.pp_prf prf - (pp_ml_list prover.pp_f) (List.map fst new_cl) ; - flush stdout - end ; *) + (* if debug then + begin + Printf.printf "\ncompact_proof : %a %a %a" + (pp_ml_list prover.pp_f) (List.map fst old_cl) + prover.pp_prf prf + (pp_ml_list prover.pp_f) (List.map fst new_cl) ; + flush stdout + end ; *) let res = try prover.compact prf remap with x when CErrors.noncritical x -> ( @@ -1790,14 +1790,14 @@ let micromega_tauto pre_process cnf spec prover env flush stdout end; (* Even if it does not work, this does not mean it is not provable - -- the prover is REALLY incomplete *) + -- the prover is REALLY incomplete *) (* if debug then - begin - (* recompute the proofs *) - match witness_list_tags prover cnf_ff' with - | None -> failwith "abstraction is wrong" - | Some res -> () - end ; *) + begin + (* recompute the proofs *) + match witness_list_tags prover cnf_ff' with + | None -> failwith "abstraction is wrong" + | Some res -> () + end ; *) let res' = compact_proofs cnf_ff res cnf_ff' in let ff', res', ids = (ff', res', Mc.ids_of_formula ff') in let res' = dump_list spec.proof_typ spec.dump_proof res' in @@ -2009,7 +2009,7 @@ let micromega_genr prover tac = let goal_vars = List.map (fun (_, i) -> List.nth env (i - 1)) vars in let arith_args = goal_props @ goal_vars in let kill_arith = Tacticals.New.tclTHEN tac_arith tac in - (* Tacticals.New.tclTHEN + (* Tacticals.New.tclTHEN (Tactics.keep []) (Tactics.tclABSTRACT None*) Tacticals.New.tclTHENS diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml index 90dd81adf4..a636fb0bdf 100644 --- a/plugins/micromega/csdpcert.ml +++ b/plugins/micromega/csdpcert.ml @@ -14,7 +14,7 @@ (* *) (************************************************************************) -open Num +open NumCompat open Sos open Sos_types open Sos_lib @@ -96,7 +96,7 @@ let real_nonlinear_prover d l = | Axiom_lt i -> poly_mul p y | Axiom_eq i -> poly_mul (poly_pow p 2) y | _ -> failwith "monoids") - m (poly_const (Int 1)) + m (poly_const Q.one) , List.map snd m )) (sets_of_list neq) in @@ -127,7 +127,7 @@ let real_nonlinear_prover d l = match List.map (function Axiom_eq i -> i | _ -> failwith "error") neq with - | [] -> Rational_lt (Int 1) + | [] -> Rational_lt Q.one | l -> Monoid l in List.fold_right (fun x y -> Product (x, y)) lt sq @@ -146,7 +146,7 @@ let real_nonlinear_prover d l = let pure_sos l = let l = List.map (fun (e, o) -> (Mc.denorm e, o)) l in (* If there is no strict inequality, - I should nonetheless be able to try something - over Z > is equivalent to -1 >= *) + I should nonetheless be able to try something - over Z > is equivalent to -1 >= *) try let l = List.combine l (CList.interval 0 (List.length l - 1)) in let lt, i = @@ -162,11 +162,11 @@ let pure_sos l = , List.fold_right (fun (c, p) rst -> Sum (Product (Rational_lt c, Square (term_of_poly p)), rst)) - polys (Rational_lt (Int 0)) ) + polys (Rational_lt Q.zero) ) in let proof = Sum (Axiom_lt i, pos) in - (* let s,proof' = scale_certificate proof in - let cert = snd (cert_of_pos proof') in *) + (* let s,proof' = scale_certificate proof in + let cert = snd (cert_of_pos proof') in *) S (Some proof) with (* | Sos.CsdpNotFound -> F "Sos.CsdpNotFound" *) | any -> @@ -184,8 +184,8 @@ let main () = try let (prover, poly) = (input_value stdin : provername * micromega_polys) in let cert = run_prover prover poly in - (* Printf.fprintf chan "%a -> %a" print_list_term poly output_csdp_certificate cert ; - close_out chan ; *) + (* Printf.fprintf chan "%a -> %a" print_list_term poly output_csdp_certificate cert ; + close_out chan ; *) output_value stdout (cert : csdp_certificate); flush stdout; Marshal.to_channel chan (cert : csdp_certificate) []; diff --git a/plugins/micromega/itv.ml b/plugins/micromega/itv.ml index 214edb46ba..74a9657038 100644 --- a/plugins/micromega/itv.ml +++ b/plugins/micromega/itv.ml @@ -8,12 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** Intervals (extracted from mfourier.ml) *) +open NumCompat +open Q.Notations -open Num +(** Intervals (extracted from mfourier.ml) *) (** The type of intervals is *) -type interval = num option * num option +type interval = Q.t option * Q.t option (** None models the absence of bound i.e. infinity As a result, - None , None -> \]-oo,+oo\[ @@ -26,11 +27,11 @@ type interval = num option * num option let pp o (n1, n2) = ( match n1 with | None -> output_string o "]-oo" - | Some n -> Printf.fprintf o "[%s" (string_of_num n) ); + | Some n -> Printf.fprintf o "[%s" (Q.to_string n) ); output_string o ","; match n2 with | None -> output_string o "+oo[" - | Some n -> Printf.fprintf o "%s]" (string_of_num n) + | Some n -> Printf.fprintf o "%s]" (Q.to_string n) (** if then interval [itv] is empty, [norm_itv itv] returns [None] otherwise, it returns [Some itv] *) @@ -51,11 +52,11 @@ let inter i1 i2 = | None, Some _ -> o2 | Some n1, Some n2 -> Some (f n1 n2) in - norm_itv (inter max_num l1 l2, inter min_num r1 r2) + norm_itv (inter Q.max l1 l2, inter Q.min r1 r2) let range = function | None, _ | _, None -> None - | Some i, Some j -> Some (floor_num j -/ ceiling_num i +/ Int 1) + | Some i, Some j -> Some (Q.floor j -/ Q.ceiling i +/ Q.one) let smaller_itv i1 i2 = match (range i1, range i2) with diff --git a/plugins/micromega/itv.mli b/plugins/micromega/itv.mli index c7164f2c98..0dec639353 100644 --- a/plugins/micromega/itv.mli +++ b/plugins/micromega/itv.mli @@ -7,13 +7,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Num +open NumCompat -type interval = num option * num option +type interval = Q.t option * Q.t option val pp : out_channel -> interval -> unit val inter : interval -> interval -> interval option -val range : interval -> num option +val range : interval -> Q.t option val smaller_itv : interval -> interval -> bool -val in_bound : interval -> num -> bool +val in_bound : interval -> Q.t -> bool val norm_itv : interval -> interval option diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index da75137185..838dab8ec8 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -8,8 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open NumCompat +open Q.Notations open Util -open Num open Polynomial open Vect @@ -61,11 +62,11 @@ let pp_cstr o (vect, bnd) = let l, r = bnd in ( match l with | None -> () - | Some n -> Printf.fprintf o "%s <= " (string_of_num n) ); + | Some n -> Printf.fprintf o "%s <= " (Q.to_string n) ); Vect.pp o vect; match r with | None -> output_string o "\n" - | Some n -> Printf.fprintf o "<=%s\n" (string_of_num n) + | Some n -> Printf.fprintf o "<=%s\n" (Q.to_string n) let pp_system o sys = System.iter (fun vect ibnd -> pp_cstr o (vect, !ibnd.bound)) sys @@ -121,12 +122,12 @@ let normalise_cstr vect cinfo = | None -> Contradiction | Some (l, r) -> ( match Vect.choose vect with - | None -> if Itv.in_bound (l, r) (Int 0) then Redundant else Contradiction + | None -> if Itv.in_bound (l, r) Q.zero then Redundant else Contradiction | Some (_, n, _) -> Cstr ( Vect.div n vect , let divn x = x // n in - if Int.equal (sign_num n) 1 then + if Int.equal (Q.sign n) 1 then {cinfo with bound = (Option.map divn l, Option.map divn r)} else { cinfo with @@ -139,7 +140,7 @@ let normalise_cstr vect cinfo = let count v = Vect.fold (fun (n, p) _ vl -> - let sg = sign_num vl in + let sg = Q.sign vl in assert (sg <> 0); if Int.equal sg 1 then (n, p + 1) else (n + 1, p)) (0, 0) v @@ -181,20 +182,20 @@ let system_list sys = System.fold (fun k bi l -> (k, !bi) :: l) s [] (** [add (v1,c1) (v2,c2) ] - precondition: (c1 <>/ Int 0 && c2 <>/ Int 0) + precondition: (c1 <>/ Q.zero && c2 <>/ Q.zero) @return a pair [(v,ln)] such that [v] is the sum of vector [v1] divided by [c1] and vector [v2] divided by [c2] Note that the resulting vector is not normalised. *) let add (v1, c1) (v2, c2) = - assert (c1 <>/ Int 0 && c2 <>/ Int 0); - let res = mul_add (Int 1 // c1) v1 (Int 1 // c2) v2 in + assert (c1 <>/ Q.zero && c2 <>/ Q.zero); + let res = mul_add (Q.one // c1) v1 (Q.one // c2) v2 in (res, count res) let add (v1, c1) (v2, c2) = let res = add (v1, c1) (v2, c2) in - (* Printf.printf "add(%a,%s,%a,%s) -> %a\n" pp_vect v1 (string_of_num c1) pp_vect v2 (string_of_num c2) pp_vect (fst res) ;*) + (* Printf.printf "add(%a,%s,%a,%s) -> %a\n" pp_vect v1 (Q.to_string c1) pp_vect v2 (Q.to_string c2) pp_vect (fst res) ;*) res (** To perform Fourier elimination, constraints are categorised depending on the sign of the variable to eliminate. *) @@ -207,11 +208,11 @@ let add (v1, c1) (v2, c2) = *) let split x (vect : vector) info (l, m, r) = - match get x vect with - | Int 0 -> + let vl = get x vect in + if Q.zero =/ vl then (* The constraint does not mention [x], store it in m *) (l, (vect, info) :: m, r) - | vl -> + else (* otherwise *) let cons_bound lst bd = match bd with @@ -219,7 +220,7 @@ let split x (vect : vector) info (l, m, r) = | Some bnd -> (vl, vect, {info with bound = (Some bnd, None)}) :: lst in let lb, rb = info.bound in - if Int.equal (sign_num vl) 1 then (cons_bound l lb, m, cons_bound r rb) + if Int.equal (Q.sign vl) 1 then (cons_bound l lb, m, cons_bound r rb) else (* sign_num vl = -1 *) (cons_bound l rb, m, cons_bound r lb) @@ -239,8 +240,8 @@ let project vr sys = let {neg = n1; pos = p1; bound = bound1; prf = prf1} = info1 and {neg = n2; pos = p2; bound = bound2; prf = prf2} = info2 in let bnd1 = Option.get (fst bound1) and bnd2 = Option.get (fst bound2) in - let bound = (bnd1 // v1) +/ (bnd2 // minus_num v2) in - let vres, (n, p) = add (vect1, v1) (vect2, minus_num v2) in + let bound = (bnd1 // v1) +/ (bnd2 // Q.neg v2) in + let vres, (n, p) = add (vect1, v1) (vect2, Q.neg v2) in ( vres , { neg = n ; pos = p @@ -270,11 +271,11 @@ let project vr sys = *) let project_using_eq vr c vect bound prf (vect', info') = - match get vr vect' with - | Int 0 -> (vect', info') - | c2 -> - let c1 = if c2 >=/ Int 0 then minus_num c else c in - let c2 = abs_num c2 in + let c2 = get vr vect' in + if Q.zero =/ c2 then (vect', info') + else + let c1 = if c2 >=/ Q.zero then Q.neg c else c in + let c2 = Q.abs c2 in let vres, (n, p) = add (vect, c1) (vect', c2) in let cst = bound // c1 in let bndres = @@ -315,14 +316,14 @@ let eval_vect map vect = let val_v = IMap.find v map in (sum +/ (val_v */ vl), rst) with Not_found -> (sum, Vect.set v vl rst)) - (Int 0, Vect.null) vect + (Q.zero, Vect.null) vect (** [restrict_bound n sum itv] returns the interval of [x] given that (fst itv) <= x * n + sum <= (snd itv) *) let restrict_bound n sum (itv : interval) = let f x = (x -/ sum) // n in let l, r = itv in - match sign_num n with + match Q.sign n with | 0 -> if in_bound itv sum then (None, None) (* redundant *) else failwith "SystemContradiction" @@ -339,7 +340,7 @@ let bound_of_variable map v sys = match inter bnd (restrict_bound vl sum !iref.bound) with | None -> Printf.fprintf stdout "bound_of_variable: eval_vecr %a = %s,%a\n" - Vect.pp vect (Num.string_of_num sum) Vect.pp rst; + Vect.pp vect (Q.to_string sum) Vect.pp rst; Printf.fprintf stdout "current interval: %a\n" Itv.pp !iref.bound; failwith "bound_of_variable: impossible" | Some itv -> itv) @@ -348,12 +349,12 @@ let bound_of_variable map v sys = (** [pick_small_value bnd] picks a value being closed to zero within the interval *) let pick_small_value bnd = match bnd with - | None, None -> Int 0 - | None, Some i -> if Int 0 <=/ floor_num i then Int 0 else floor_num i - | Some i, None -> if i <=/ Int 0 then Int 0 else ceiling_num i + | None, None -> Q.zero + | None, Some i -> if Q.zero <=/ Q.floor i then Q.zero else Q.floor i + | Some i, None -> if i <=/ Q.zero then Q.zero else Q.ceiling i | Some i, Some j -> - if i <=/ Int 0 && Int 0 <=/ j then Int 0 - else if ceiling_num i <=/ floor_num j then ceiling_num i (* why not *) + if i <=/ Q.zero && Q.zero <=/ j then Q.zero + else if Q.ceiling i <=/ Q.floor j then Q.ceiling i (* why not *) else i (** [solution s1 sys_l = Some(sn,\[(vn-1,sn-1);...; (v1,s1)\]\@sys_l)] @@ -373,8 +374,8 @@ let solve_sys black_v choose_eq choose_variable sys sys_l = fst (List.find (fun ((v, _, _, _), _) -> v <> black_v) eqs) in if debug then ( - Printf.printf "\nE %a = %s variable %i\n" Vect.pp vect - (string_of_num cst) v; + Printf.printf "\nE %a = %s variable %i\n" Vect.pp vect (Q.to_string cst) + v; flush stdout ); let sys' = elim_var_using_eq v vect cst ln sys in solve_sys sys' ((v, sys) :: sys_l) @@ -422,7 +423,7 @@ module EstimateElimVar = struct | Some bnd -> (info.neg + info.pos) :: lst in let lb, rb = info.bound in - if Int.equal (sign_num vl) 1 then + if Int.equal (Q.sign vl) 1 then xpart rl ((rl1, info) :: ltl) (cons_bound n lb) z (cons_bound p rb) else @@ -568,7 +569,7 @@ module Fourier = struct (* We add a dummy (fresh) variable for vector *) let fresh = List.fold_left (fun fr c -> max fr (Vect.fresh c.coeffs)) 0 l in let cstr = - {coeffs = Vect.set fresh (Int (-1)) vect; op = Eq; cst = Int 0} + {coeffs = Vect.set fresh Q.neg_one vect; op = Eq; cst = Q.zero} in match solve fresh choose_equality_var choose_variable (cstr :: l) with | Inr prf -> None (* This is an unsatisfiability proof *) @@ -619,28 +620,27 @@ module Proof = struct let pivot v (p1, c1) (p2, c2) = let {coeffs = v1; op = op1; cst = n1} = c1 and {coeffs = v2; op = op2; cst = n2} = c2 in - match (Vect.get v v1, Vect.get v v2) with - | Int 0, _ | _, Int 0 -> None - | a, b -> - if Int.equal (sign_num a * sign_num b) (-1) then - Some - ( add (p1, abs_num a) (p2, abs_num b) - , { coeffs = add (v1, abs_num a) (v2, abs_num b) - ; op = add_op op1 op2 - ; cst = (n1 // abs_num a) +/ (n2 // abs_num b) } ) - else if op1 == Eq then - Some - ( add (p1, minus_num (a // b)) (p2, Int 1) - , { coeffs = add (v1, minus_num (a // b)) (v2, Int 1) - ; op = add_op op1 op2 - ; cst = (n1 // minus_num (a // b)) +/ (n2 // Int 1) } ) - else if op2 == Eq then - Some - ( add (p2, minus_num (b // a)) (p1, Int 1) - , { coeffs = add (v2, minus_num (b // a)) (v1, Int 1) - ; op = add_op op1 op2 - ; cst = (n2 // minus_num (b // a)) +/ (n1 // Int 1) } ) - else None + let a, b = (Vect.get v v1, Vect.get v v2) in + if Q.zero =/ a || Q.zero =/ b then None + else if Int.equal (Q.sign a * Q.sign b) (-1) then + Some + ( add (p1, Q.abs a) (p2, Q.abs b) + , { coeffs = add (v1, Q.abs a) (v2, Q.abs b) + ; op = add_op op1 op2 + ; cst = (n1 // Q.abs a) +/ (n2 // Q.abs b) } ) + else if op1 == Eq then + Some + ( add (p1, Q.neg (a // b)) (p2, Q.one) + , { coeffs = add (v1, Q.neg (a // b)) (v2, Q.one) + ; op = add_op op1 op2 + ; cst = (n1 // Q.neg (a // b)) +/ (n2 // Q.one) } ) + else if op2 == Eq then + Some + ( add (p2, Q.neg (b // a)) (p1, Q.one) + , { coeffs = add (v2, Q.neg (b // a)) (v1, Q.one) + ; op = add_op op1 op2 + ; cst = (n2 // Q.neg (b // a)) +/ (n1 // Q.one) } ) + else None (* op2 could be Eq ... this might happen *) @@ -656,7 +656,7 @@ module Proof = struct | Cstr (v, info) -> Inl ((prf, cstr, v, info) :: acc) )) (Inl []) l - type oproof = (vector * cstr * num) option + type oproof = (vector * cstr * Q.t) option let merge_proof (oleft : oproof) (prf, cstr, v, info) (oright : oproof) = let l, r = info.bound in @@ -679,7 +679,7 @@ module Proof = struct (* There is a contradiction - it should show up by scaling up the vectors - any pivot should do*) match Vect.choose cstrr.coeffs with | None -> - Inr (add (prfl, Int 1) (prfr, Int 1), cstrr) (* this is wrong *) + Inr (add (prfl, Q.one) (prfr, Q.one), cstrr) (* this is wrong *) | Some (v, _, _) -> ( match pivot v (prfl, cstrl) (prfr, cstrr) with | None -> failwith "merge_proof : pivot is not possible" @@ -687,12 +687,12 @@ module Proof = struct let mk_proof hyps prf = (* I am keeping list - I might have a proof for the left bound and a proof for the right bound. - If I perform aggressive elimination of redundancies, I expect the list to be of length at most 2. - For each proof list, all the vectors should be of the form a.v for different constants a. - *) + If I perform aggressive elimination of redundancies, I expect the list to be of length at most 2. + For each proof list, all the vectors should be of the form a.v for different constants a. + *) let rec mk_proof prf = match prf with - | Assum i -> [(Vect.set i (Int 1) Vect.null, List.nth hyps i)] + | Assum i -> [(Vect.set i Q.one Vect.null, List.nth hyps i)] | Elim (v, prf1, prf2) -> let prfsl = mk_proof prf1 and prfsr = mk_proof prf2 in (* I take only the pairs for which the elimination is meaningful *) diff --git a/plugins/micromega/micromega_plugin.mlpack b/plugins/micromega/micromega_plugin.mlpack index e3aa0dab7d..2630e883c9 100644 --- a/plugins/micromega/micromega_plugin.mlpack +++ b/plugins/micromega/micromega_plugin.mlpack @@ -1,4 +1,5 @@ Micromega +NumCompat Mutils Itv Vect diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index 51f0328e4b..2e054a21c2 100644 --- a/plugins/micromega/mutils.ml +++ b/plugins/micromega/mutils.ml @@ -19,6 +19,9 @@ (* *) (************************************************************************) +open NumCompat +module Z_ = NumCompat.Z + module Int = struct type t = int @@ -159,24 +162,6 @@ let saturate_bin (type a) (module Set : Set.S with type elt = a) let s0 = List.fold_left (fun acc e -> Set.add e acc) Set.empty l in Set.elements (Set.diff (iterate Set.empty s0) s0) -open Num -open Big_int - -let ppcm x y = - let g = gcd_big_int x y in - let x' = div_big_int x g in - let y' = div_big_int y g in - mult_big_int g (mult_big_int x' y') - -let denominator = function - | Int _ | Big_int _ -> unit_big_int - | Ratio r -> Ratio.denominator_ratio r - -let numerator = function - | Ratio r -> Ratio.numerator_ratio r - | Int i -> Big_int.big_int_of_int i - | Big_int i -> i - let iterate_until_stable f x = let rec iter x = match f x with None -> x | Some x' -> iter x' in iter x @@ -207,24 +192,23 @@ module CoqToCaml = struct (* Swap left-right ? *) match i with XH -> 1 | XI i -> 1 + (2 * index i) | XO i -> 2 * index i - open Big_int - let rec positive_big_int p = match p with - | XH -> unit_big_int - | XI p -> add_int_big_int 1 (mult_int_big_int 2 (positive_big_int p)) - | XO p -> mult_int_big_int 2 (positive_big_int p) + | XH -> Z_.one + | XI p -> Z_.add Z_.one (Z_.mul Z_.two (positive_big_int p)) + | XO p -> Z_.mul Z_.two (positive_big_int p) let z_big_int x = match x with - | Z0 -> zero_big_int + | Z0 -> Z_.zero | Zpos p -> positive_big_int p - | Zneg p -> minus_big_int (positive_big_int p) + | Zneg p -> Z_.neg (positive_big_int p) let z x = match x with Z0 -> 0 | Zpos p -> index p | Zneg p -> -index p let q_to_num {qnum = x; qden = y} = - Big_int (z_big_int x) // Big_int (z_big_int (Zpos y)) + let open Q.Notations in + Q.of_bigint (z_big_int x) // Q.of_bigint (z_big_int (Zpos y)) end (** @@ -259,27 +243,24 @@ module CamlToCoq = struct (* this should be -1 *) Zneg (positive (-x)) - open Big_int - let positive_big_int n = - let two = big_int_of_int 2 in let rec _pos n = - if eq_big_int n unit_big_int then XH + if Z_.equal n Z_.one then XH else - let q, m = quomod_big_int n two in - if eq_big_int unit_big_int m then XI (_pos q) else XO (_pos q) + let q, m = Z_.quomod n Z_.two in + if Z_.equal Z_.one m then XI (_pos q) else XO (_pos q) in _pos n let bigint x = - match sign_big_int x with + match Z_.sign x with | 0 -> Z0 | 1 -> Zpos (positive_big_int x) - | _ -> Zneg (positive_big_int (minus_big_int x)) + | _ -> Zneg (positive_big_int (Z_.neg x)) let q n = - { Micromega.qnum = bigint (numerator n) - ; Micromega.qden = positive_big_int (denominator n) } + { Micromega.qnum = bigint (Q.num n) + ; Micromega.qden = positive_big_int (Q.den n) } end (** diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli index 9badddc255..a03b03ed8e 100644 --- a/plugins/micromega/mutils.mli +++ b/plugins/micromega/mutils.mli @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open NumCompat + module Int : sig type t = int @@ -28,9 +30,6 @@ module IMap : sig (** [from k m] returns the submap of [m] with keys greater or equal k *) end -val numerator : Num.num -> Big_int.big_int -val denominator : Num.num -> Big_int.big_int - module Cmp : sig val compare_list : ('a -> 'b -> int) -> 'a list -> 'b list -> int val compare_lexical : (unit -> int) list -> int @@ -53,19 +52,19 @@ val pp_list : module CamlToCoq : sig val positive : int -> Micromega.positive - val bigint : Big_int.big_int -> Micromega.z + val bigint : Z.t -> Micromega.z val n : int -> Micromega.n val nat : int -> Micromega.nat - val q : Num.num -> Micromega.q + val q : Q.t -> Micromega.q val index : int -> Micromega.positive val z : int -> Micromega.z - val positive_big_int : Big_int.big_int -> Micromega.positive + val positive_big_int : Z.t -> Micromega.positive end module CoqToCaml : sig - val z_big_int : Micromega.z -> Big_int.big_int + val z_big_int : Micromega.z -> Z.t val z : Micromega.z -> int - val q_to_num : Micromega.q -> Num.num + val q_to_num : Micromega.q -> Q.t val positive : Micromega.positive -> int val n : Micromega.n -> int val nat : Micromega.nat -> int @@ -96,7 +95,6 @@ module Hash : sig val hash_elt : ('a -> int) -> int -> 'a -> int end -val ppcm : Big_int.big_int -> Big_int.big_int -> Big_int.big_int val all_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list val try_any : (('a -> 'b option) * 'c) list -> 'a -> 'b option val is_sublist : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool diff --git a/plugins/micromega/numCompat.ml b/plugins/micromega/numCompat.ml new file mode 100644 index 0000000000..82993cd730 --- /dev/null +++ b/plugins/micromega/numCompat.ml @@ -0,0 +1,174 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +module type ZArith = sig + type t + + val zero : t + val one : t + val two : t + val add : t -> t -> t + val sub : t -> t -> t + val mul : t -> t -> t + val div : t -> t -> t + val neg : t -> t + val sign : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + val power_int : t -> int -> t + val quomod : t -> t -> t * t + val ppcm : t -> t -> t + val gcd : t -> t -> t + val lcm : t -> t -> t + val to_string : t -> string +end + +module Z = struct + type t = Big_int.big_int + + open Big_int + + let zero = zero_big_int + let one = unit_big_int + let two = big_int_of_int 2 + let add = Big_int.add_big_int + let sub = Big_int.sub_big_int + let mul = Big_int.mult_big_int + let div = Big_int.div_big_int + let neg = Big_int.minus_big_int + let sign = Big_int.sign_big_int + let equal = eq_big_int + let compare = compare_big_int + let power_int = power_big_int_positive_int + let quomod = quomod_big_int + + let ppcm x y = + let g = gcd_big_int x y in + let x' = div_big_int x g in + let y' = div_big_int y g in + mult_big_int g (mult_big_int x' y') + + let gcd = gcd_big_int + + let lcm x y = + if eq_big_int x zero && eq_big_int y zero then zero + else abs_big_int (div_big_int (mult_big_int x y) (gcd x y)) + + let to_string = string_of_big_int +end + +module type QArith = sig + module Z : ZArith + + type t + + val of_int : int -> t + val zero : t + val one : t + val two : t + val ten : t + val neg_one : t + + module Notations : sig + val ( // ) : t -> t -> t + val ( +/ ) : t -> t -> t + val ( -/ ) : t -> t -> t + val ( */ ) : t -> t -> t + val ( =/ ) : t -> t -> bool + val ( <>/ ) : t -> t -> bool + val ( >/ ) : t -> t -> bool + val ( >=/ ) : t -> t -> bool + val ( </ ) : t -> t -> bool + val ( <=/ ) : t -> t -> bool + end + + val compare : t -> t -> int + val make : Z.t -> Z.t -> t + val den : t -> Z.t + val num : t -> Z.t + val of_bigint : Z.t -> t + val to_bigint : t -> Z.t + val neg : t -> t + + (* val inv : t -> t *) + val max : t -> t -> t + val min : t -> t -> t + val sign : t -> int + val abs : t -> t + val mod_ : t -> t -> t + val floor : t -> t + + (* val floorZ : t -> Z.t *) + val ceiling : t -> t + val round : t -> t + val pow2 : int -> t + val pow10 : int -> t + val power : int -> t -> t + val to_string : t -> string + val of_string : string -> t + val to_float : t -> float +end + +module Q : QArith with module Z = Z = struct + module Z = Z + + type t = Num.num + + open Num + + let of_int x = Int x + let zero = Int 0 + let one = Int 1 + let two = Int 2 + let ten = Int 10 + let neg_one = Int (-1) + + module Notations = struct + let ( // ) = div_num + let ( +/ ) = add_num + let ( -/ ) = sub_num + let ( */ ) = mult_num + let ( =/ ) = eq_num + let ( <>/ ) = ( <>/ ) + let ( >/ ) = ( >/ ) + let ( >=/ ) = ( >=/ ) + let ( </ ) = ( </ ) + let ( <=/ ) = ( <=/ ) + end + + let compare = compare_num + let make x y = Big_int x // Big_int y + + let numdom r = + let r' = Ratio.normalize_ratio (ratio_of_num r) in + (Ratio.numerator_ratio r', Ratio.denominator_ratio r') + + let num x = numdom x |> fst + let den x = numdom x |> snd + let of_bigint x = Big_int x + let to_bigint = big_int_of_num + let neg = minus_num + + (* let inv = *) + let max = max_num + let min = min_num + let sign = sign_num + let abs = abs_num + let mod_ = mod_num + let floor = floor_num + let ceiling = ceiling_num + let round = round_num + let pow2 n = power_num two (Int n) + let pow10 n = power_num ten (Int n) + let power x = power_num (Int x) + let to_string = string_of_num + let of_string = num_of_string + let to_float = float_of_num +end diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli new file mode 100644 index 0000000000..183285e259 --- /dev/null +++ b/plugins/micromega/numCompat.mli @@ -0,0 +1,85 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +module type ZArith = sig + type t + + val zero : t + val one : t + val two : t + val add : t -> t -> t + val sub : t -> t -> t + val mul : t -> t -> t + val div : t -> t -> t + val neg : t -> t + val sign : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + val power_int : t -> int -> t + val quomod : t -> t -> t * t + val ppcm : t -> t -> t + val gcd : t -> t -> t + val lcm : t -> t -> t + val to_string : t -> string +end + +module type QArith = sig + module Z : ZArith + + type t + + val of_int : int -> t + val zero : t + val one : t + val two : t + val ten : t + val neg_one : t + + module Notations : sig + val ( // ) : t -> t -> t + val ( +/ ) : t -> t -> t + val ( -/ ) : t -> t -> t + val ( */ ) : t -> t -> t + val ( =/ ) : t -> t -> bool + val ( <>/ ) : t -> t -> bool + val ( >/ ) : t -> t -> bool + val ( >=/ ) : t -> t -> bool + val ( </ ) : t -> t -> bool + val ( <=/ ) : t -> t -> bool + end + + val compare : t -> t -> int + val make : Z.t -> Z.t -> t + val den : t -> Z.t + val num : t -> Z.t + val of_bigint : Z.t -> t + val to_bigint : t -> Z.t + val neg : t -> t + + (* val inv : t -> t *) + + val max : t -> t -> t + val min : t -> t -> t + val sign : t -> int + val abs : t -> t + val mod_ : t -> t -> t + val floor : t -> t + val ceiling : t -> t + val round : t -> t + val pow2 : int -> t + val pow10 : int -> t + val power : int -> t -> t + val to_string : t -> string + val of_string : string -> t + val to_float : t -> float +end + +module Z : ZArith +module Q : QArith with module Z = Z diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index d5b28cb03e..4777b5e231 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -82,9 +82,9 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct with Unix.Unix_error (_, _, _) -> () (* Here, this is really bad news -- - there is a pending lock which could cause a deadlock. - Should it be an anomaly or produce a warning ? - *); + there is a pending lock which could cause a deadlock. + Should it be an anomaly or produce a warning ? + *); ignore (lseek fd pos SEEK_SET) (* We make the assumption that an acquired lock can always be released *) diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index f83b36d847..68aa739a6f 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -14,7 +14,8 @@ (* *) (************************************************************************) -open Num +open NumCompat +open Q.Notations open Mutils module Mc = Micromega @@ -23,8 +24,8 @@ let max_nb_cstr = ref max_int type var = int let debug = false -let ( <+> ) = add_num -let ( <*> ) = mult_num +let ( <+> ) = ( +/ ) +let ( <*> ) = ( */ ) module Monomial : sig type t @@ -153,13 +154,11 @@ end let pp_mon o (m, i) = if Monomial.is_const m then - if eq_num (Int 0) i then () else Printf.fprintf o "%s" (string_of_num i) - else - match i with - | Int 1 -> Monomial.pp o m - | Int -1 -> Printf.fprintf o "-%a" Monomial.pp m - | Int 0 -> () - | _ -> Printf.fprintf o "%s*%a" (string_of_num i) Monomial.pp m + if Q.zero =/ i then () else Printf.fprintf o "%s" (Q.to_string i) + else if Q.one =/ i then Monomial.pp o m + else if Q.neg_one =/ i then Printf.fprintf o "-%a" Monomial.pp m + else if Q.zero =/ i then () + else Printf.fprintf o "%s*%a" (Q.to_string i) Monomial.pp m module Poly : (* A polynomial is a map of monomials *) (* @@ -171,51 +170,51 @@ sig type t val pp : out_channel -> t -> unit - val get : Monomial.t -> t -> num + val get : Monomial.t -> t -> Q.t val variable : var -> t - val add : Monomial.t -> num -> t -> t - val constant : num -> t + val add : Monomial.t -> Q.t -> t -> t + val constant : Q.t -> t val product : t -> t -> t val addition : t -> t -> t val uminus : t -> t - val fold : (Monomial.t -> num -> 'a -> 'a) -> t -> 'a -> 'a + val fold : (Monomial.t -> Q.t -> 'a -> 'a) -> t -> 'a -> 'a val factorise : var -> t -> t * t end = struct (*normalisation bug : 0*x ... *) module P = Map.Make (Monomial) open P - type t = num P.t + type t = Q.t P.t let pp o p = P.iter (fun mn i -> Printf.fprintf o "%a + " pp_mon (mn, i)) p (* Get the coefficient of monomial mn *) - let get : Monomial.t -> t -> num = - fun mn p -> try find mn p with Not_found -> Int 0 + let get : Monomial.t -> t -> Q.t = + fun mn p -> try find mn p with Not_found -> Q.zero (* The polynomial 1.x *) - let variable : var -> t = fun x -> add (Monomial.var x) (Int 1) empty + let variable : var -> t = fun x -> add (Monomial.var x) Q.one empty (*The constant polynomial *) - let constant : num -> t = fun c -> add Monomial.const c empty + let constant : Q.t -> t = fun c -> add Monomial.const c empty (* The addition of a monomial *) - let add : Monomial.t -> num -> t -> t = + let add : Monomial.t -> Q.t -> t -> t = fun mn v p -> - if sign_num v = 0 then p + if Q.sign v = 0 then p else let vl = get mn p <+> v in - if sign_num vl = 0 then remove mn p else add mn vl p + if Q.sign vl = 0 then remove mn p else add mn vl p (** Design choice: empty is not a polynomial I do not remember why .... **) (* The product by a monomial *) - let mult : Monomial.t -> num -> t -> t = + let mult : Monomial.t -> Q.t -> t -> t = fun mn v p -> - if sign_num v = 0 then constant (Int 0) + if Q.sign v = 0 then constant Q.zero else fold (fun mn' v' res -> P.add (Monomial.prod mn mn') (v <*> v') res) @@ -227,7 +226,7 @@ end = struct let product : t -> t -> t = fun p1 p2 -> fold (fun mn v res -> addition (mult mn v p2) res) p1 empty - let uminus : t -> t = fun p -> map (fun v -> minus_num v) p + let uminus : t -> t = fun p -> map (fun v -> Q.neg v) p let fold = P.fold let factorise x p = @@ -240,12 +239,12 @@ end = struct let mx = Monomial.prod m1 (Monomial.exp x (i - 1)) in (add mx v px, cx)) p - (constant (Int 0), constant (Int 0)) + (constant Q.zero, constant Q.zero) end type vector = Vect.t -type cstr = {coeffs : vector; op : op; cst : num} +type cstr = {coeffs : vector; op : op; cst : Q.t} and op = Eq | Ge | Gt @@ -256,8 +255,7 @@ let eval_op = function Eq -> ( =/ ) | Ge -> ( >=/ ) | Gt -> ( >/ ) let string_of_op = function Eq -> "=" | Ge -> ">=" | Gt -> ">" let output_cstr o {coeffs; op; cst} = - Printf.fprintf o "%a %s %s" Vect.pp coeffs (string_of_op op) - (string_of_num cst) + Printf.fprintf o "%a %s %s" Vect.pp coeffs (string_of_op op) (Q.to_string cst) let opMult o1 o2 = match (o1, o2) with Eq, _ | _, Eq -> Eq | Ge, _ | _, Ge -> Ge | Gt, Gt -> Gt @@ -308,11 +306,11 @@ module LinPoly = struct let _ = register Monomial.const end - let var v = Vect.set (MonT.register (Monomial.var v)) (Int 1) Vect.null + let var v = Vect.set (MonT.register (Monomial.var v)) Q.one Vect.null let of_monomial m = let v = MonT.register m in - Vect.set v (Int 1) Vect.null + Vect.set v Q.one Vect.null let linpol_of_pol p = Poly.fold @@ -324,7 +322,7 @@ module LinPoly = struct let pol_of_linpol v = Vect.fold (fun p vr n -> Poly.add (MonT.retrieve vr) n p) - (Poly.constant (Int 0)) v + (Poly.constant Q.zero) v let coq_poly_of_linpol cst p = let pol_of_mon m = @@ -332,13 +330,13 @@ module LinPoly = struct (fun x v p -> Mc.PEmul (Mc.PEpow (Mc.PEX (CamlToCoq.positive x), CamlToCoq.n v), p)) m - (Mc.PEc (cst (Int 1))) + (Mc.PEc (cst Q.one)) in Vect.fold (fun acc x v -> let mn = MonT.retrieve x in Mc.PEadd (Mc.PEmul (Mc.PEc (cst v), pol_of_mon mn), acc)) - (Mc.PEc (cst (Int 0))) + (Mc.PEc (cst Q.zero)) p let pp_var o vr = @@ -346,7 +344,7 @@ module LinPoly = struct with Not_found -> Printf.fprintf o "v%i" vr let pp o p = Vect.pp_gen pp_var o p - let constant c = if sign_num c = 0 then Vect.null else Vect.set 0 c Vect.null + let constant c = if Q.sign c = 0 then Vect.null else Vect.set 0 c Vect.null let is_linear p = Vect.for_all @@ -357,7 +355,7 @@ module LinPoly = struct let is_variable p = let (x, v), r = Vect.decomp_fst p in - if Vect.is_null r && v >/ Int 0 then Monomial.get_var (MonT.retrieve x) + if Vect.is_null r && v >/ Q.zero then Monomial.get_var (MonT.retrieve x) else None let factorise x p = @@ -431,17 +429,15 @@ module LinPoly = struct end module ProofFormat = struct - open Big_int - type prf_rule = | Annot of string * prf_rule | Hyp of int | Def of int - | Cst of Num.num + | Cst of Q.t | Zero | Square of Vect.t | MulC of Vect.t * prf_rule - | Gcd of Big_int.big_int * prf_rule + | Gcd of Z.t * prf_rule | MulPrf of prf_rule * prf_rule | AddPrf of prf_rule * prf_rule | CutPrf of prf_rule @@ -458,7 +454,7 @@ module ProofFormat = struct | Annot (s, p) -> Printf.fprintf o "(%a)@%s" output_prf_rule p s | Hyp i -> Printf.fprintf o "Hyp %i" i | Def i -> Printf.fprintf o "Def %i" i - | Cst c -> Printf.fprintf o "Cst %s" (string_of_num c) + | Cst c -> Printf.fprintf o "Cst %s" (Q.to_string c) | Zero -> Printf.fprintf o "Zero" | Square s -> Printf.fprintf o "(%a)^2" Poly.pp (LinPoly.pol_of_linpol s) | MulC (p, pr) -> @@ -469,8 +465,7 @@ module ProofFormat = struct | AddPrf (p1, p2) -> Printf.fprintf o "%a + %a" output_prf_rule p1 output_prf_rule p2 | CutPrf p -> Printf.fprintf o "[%a]" output_prf_rule p - | Gcd (c, p) -> - Printf.fprintf o "(%a)/%s" output_prf_rule p (string_of_big_int c) + | Gcd (c, p) -> Printf.fprintf o "(%a)/%s" output_prf_rule p (Z.to_string c) let rec output_proof o = function | Done -> Printf.fprintf o "." @@ -485,11 +480,11 @@ module ProofFormat = struct let rec pr_size = function | Annot (_, p) -> pr_size p - | Zero | Square _ -> Int 0 - | Hyp _ -> Int 1 - | Def _ -> Int 1 + | Zero | Square _ -> Q.zero + | Hyp _ -> Q.one + | Def _ -> Q.one | Cst n -> n - | Gcd (i, p) -> pr_size p // Big_int i + | Gcd (i, p) -> pr_size p // Q.of_bigint i | MulPrf (p1, p2) | AddPrf (p1, p2) -> pr_size p1 +/ pr_size p2 | CutPrf p -> pr_size p | MulC (v, p) -> pr_size p @@ -601,12 +596,12 @@ module ProofFormat = struct (id, ExProof (i, j, k, x, z, t, prf)) | Enum (i, p1, v, p2, pl) -> (* Why do I have top-level cuts ? *) - (* let p1 = implicit_cut p1 in - let p2 = implicit_cut p2 in - let (ids,prfs) = List.split (List.map (normalise_proof id) pl) in - (List.fold_left max 0 ids , - Enum(i,p1,v,p2,prfs)) - *) + (* let p1 = implicit_cut p1 in + let p2 = implicit_cut p2 in + let (ids,prfs) = List.split (List.map (normalise_proof id) pl) in + (List.fold_left max 0 ids , + Enum(i,p1,v,p2,prfs)) + *) let bds1, id, p1' = pr_rule_def_cut id (implicit_cut p1) in let bds2, id, p2' = pr_rule_def_cut id (implicit_cut p2) in let ids, prfs = List.split (List.map (normalise_proof id) pl) in @@ -649,13 +644,13 @@ module ProofFormat = struct if s1 = s2 then compare p1 p2 else String.compare s1 s2 | Hyp i, Hyp j -> Int.compare i j | Def i, Def j -> Int.compare i j - | Cst n, Cst m -> Num.compare_num n m + | Cst n, Cst m -> Q.compare n m | Zero, Zero -> 0 | Square v1, Square v2 -> Vect.compare v1 v2 | MulC (v1, p1), MulC (v2, p2) -> cmp_pair Vect.compare compare (v1, p1) (v2, p2) | Gcd (b1, p1), Gcd (b2, p2) -> - cmp_pair Big_int.compare_big_int compare (b1, p1) (b2, p2) + cmp_pair Z.compare compare (b1, p1) (b2, p2) | MulPrf (p1, q1), MulPrf (p2, q2) -> cmp_pair compare compare (p1, q1) (p2, q2) | AddPrf (p1, q1), MulPrf (p2, q2) -> @@ -672,11 +667,11 @@ module ProofFormat = struct | Annot (s, p) -> Annot (s, mul_cst_proof c p) | MulC (v, p') -> MulC (Vect.mul c v, p') | _ -> ( - match sign_num c with + match Q.sign c with | 0 -> Zero (* This is likely to be a bug *) | -1 -> MulC (LinPoly.constant c, p) (* [p] should represent an equality *) - | 1 -> if eq_num (Int 1) c then p else MulPrf (Cst c, p) + | 1 -> if Q.one =/ c then p else MulPrf (Cst c, p) | _ -> assert false ) let sMulC v p = @@ -698,7 +693,7 @@ module ProofFormat = struct match p with | Annot (s, p) -> dev_prf_rule p | Hyp _ | Def _ | Cst _ | Zero | Square _ -> - PrfRuleMap.singleton p (LinPoly.constant (Int 1)) + PrfRuleMap.singleton p (LinPoly.constant Q.one) | MulC (v, p) -> PrfRuleMap.map (fun v1 -> LinPoly.product v v1) (dev_prf_rule p) | AddPrf (p1, p2) -> @@ -716,9 +711,9 @@ module ProofFormat = struct let p2'' = prf_rule_of_map p2' in match p1'' with | Cst c -> PrfRuleMap.map (fun v1 -> Vect.mul c v1) p2' - | _ -> - PrfRuleMap.singleton (MulPrf (p1'', p2'')) (LinPoly.constant (Int 1)) ) - | _ -> PrfRuleMap.singleton p (LinPoly.constant (Int 1)) + | _ -> PrfRuleMap.singleton (MulPrf (p1'', p2'')) (LinPoly.constant Q.one) + ) + | _ -> PrfRuleMap.singleton p (LinPoly.constant Q.one) let simplify_prf_rule p = prf_rule_of_map (dev_prf_rule p) @@ -766,7 +761,7 @@ module ProofFormat = struct xid_of_hyp 0 l end - let cmpl_prf_rule norm (cst : num -> 'a) env prf = + let cmpl_prf_rule norm (cst : Q.t -> 'a) env prf = let rec cmpl = function | Annot (s, p) -> cmpl p | Hyp i | Def i -> Mc.PsatzIn (CamlToCoq.nat (Env.id_of_hyp i env)) @@ -783,7 +778,7 @@ module ProofFormat = struct cmpl prf let cmpl_prf_rule_z env r = - cmpl_prf_rule Mc.normZ (fun x -> CamlToCoq.bigint (numerator x)) env r + cmpl_prf_rule Mc.normZ (fun x -> CamlToCoq.bigint (Q.num x)) env r let rec cmpl_proof env = function | Done -> Mc.DoneProof @@ -810,7 +805,7 @@ module ProofFormat = struct | Hyp i | Def i -> env i | Cst n -> ( ( Vect.set 0 n Vect.null - , match Num.compare_num n (Int 0) with + , match Q.compare n Q.zero with | 0 -> Ge | 1 -> Gt | _ -> failwith "eval_prf_rule : negative constant" ) ) @@ -826,7 +821,7 @@ module ProofFormat = struct failwith "eval_prf_rule : not an equality" ) | Gcd (g, p) -> let v, op = eval_prf_rule env p in - (Vect.div (Big_int g) v, op) + (Vect.div (Q.of_bigint g) v, op) | MulPrf (p1, p2) -> let v1, o1 = eval_prf_rule env p1 in let v2, o2 = eval_prf_rule env p2 in @@ -839,7 +834,7 @@ module ProofFormat = struct let is_unsat (p, o) = let c, r = Vect.decomp_cst p in - if Vect.is_null r then not (eval_op o c (Int 0)) else false + if Vect.is_null r then not (eval_op o c Q.zero) else false let rec eval_proof env p = match p with @@ -882,7 +877,7 @@ module WithProof = struct let zero = ((Vect.null, Eq), ProofFormat.Zero) let const n = ((LinPoly.constant n, Ge), ProofFormat.Cst n) - let of_cstr (c, prf) = ((Vect.set 0 (Num.minus_num c.cst) c.coeffs, c.op), prf) + let of_cstr (c, prf) = ((Vect.set 0 (Q.neg c.cst) c.coeffs, c.op), prf) let product : t -> t -> t = fun ((p1, o1), prf1) ((p2, o2), prf2) -> @@ -897,7 +892,7 @@ module WithProof = struct | Eq -> ((LinPoly.product p p1, o1), ProofFormat.sMulC p prf1) | Gt | Ge -> let n, r = Vect.decomp_cst p in - if Vect.is_null r && n >/ Int 0 then + if Vect.is_null r && n >/ Q.zero then ((LinPoly.product p p1, o1), ProofFormat.mul_cst_proof n prf1) else ( if debug then @@ -908,34 +903,31 @@ module WithProof = struct let cutting_plane ((p, o), prf) = let c, p' = Vect.decomp_cst p in let g = Vect.gcd p' in - if - Big_int.eq_big_int Big_int.unit_big_int g - || c =/ Int 0 - || not (Big_int.eq_big_int (denominator c) Big_int.unit_big_int) - then None (* Nothing to do *) + if Z.equal Z.one g || c =/ Q.zero || not (Z.equal (Q.den c) Z.one) then None + (* Nothing to do *) else - let c1 = c // Big_int g in - let c1' = Num.floor_num c1 in + let c1 = c // Q.of_bigint g in + let c1' = Q.floor c1 in if c1 =/ c1' then None else match o with | Eq -> - Some ((Vect.set 0 (Int (-1)) Vect.null, Eq), ProofFormat.Gcd (g, prf)) + Some ((Vect.set 0 Q.neg_one Vect.null, Eq), ProofFormat.Gcd (g, prf)) | Gt -> failwith "cutting_plane ignore strict constraints" | Ge -> (* This is a non-trivial common divisor *) Some - ( (Vect.set 0 c1' (Vect.div (Big_int g) p), o) + ( (Vect.set 0 c1' (Vect.div (Q.of_bigint g) p), o) , ProofFormat.Gcd (g, prf) ) let construct_sign p = let c, p' = Vect.decomp_cst p in if Vect.is_null p' then Some - ( match sign_num c with + ( match Q.sign c with | 0 -> (true, Eq, ProofFormat.Zero) | 1 -> (true, Gt, ProofFormat.Cst c) - | _ (*-1*) -> (false, Gt, ProofFormat.Cst (minus_num c)) ) + | _ (*-1*) -> (false, Gt, ProofFormat.Cst (Q.neg c)) ) else None let get_sign l p = @@ -1007,7 +999,7 @@ module WithProof = struct | Some (c, p) -> Some (c, ProofFormat.simplify_prf_rule p) let is_substitution strict ((p, o), prf) = - let pred v = if strict then v =/ Int 1 || v =/ Int (-1) else true in + let pred v = if strict then v =/ Q.one || v =/ Q.neg_one else true in match o with Eq -> LinPoly.search_linear pred p | _ -> None let subst1 sys0 = @@ -1048,14 +1040,14 @@ module WithProof = struct , Some {cst = c2; var = v2; coeff = c2'} ) -> ( let good_coeff b o = match o with - | Eq -> Some (minus_num b) - | _ -> if b <=/ Int 0 then Some (minus_num b) else None + | Eq -> Some (Q.neg b) + | _ -> if b <=/ Q.zero then Some (Q.neg b) else None in match (good_coeff c1 o2, good_coeff c2 o1) with | None, _ | _, None -> None | Some c1, Some c2 -> let ext_mult c w = - if c =/ Int 0 then zero else mult (LinPoly.constant c) w + if c =/ Q.zero then zero else mult (LinPoly.constant c) w in Some (addition diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli index 797ff5827d..357a2b10e1 100644 --- a/plugins/micromega/polynomial.mli +++ b/plugins/micromega/polynomial.mli @@ -9,6 +9,7 @@ (************************************************************************) open Mutils +open NumCompat module Mc = Micromega val max_nb_cstr : int ref @@ -81,7 +82,7 @@ module Poly : sig type t - val constant : Num.num -> t + val constant : Q.t -> t (** [constant c] @return the constant polynomial c *) @@ -101,24 +102,24 @@ module Poly : sig (** [uminus p] @return the polynomial -p i.e product by -1 *) - val get : Monomial.t -> t -> Num.num + val get : Monomial.t -> t -> Q.t (** [get mi p] @return the coefficient ai of the monomial mi. *) - val fold : (Monomial.t -> Num.num -> 'a -> 'a) -> t -> 'a -> 'a + val fold : (Monomial.t -> Q.t -> 'a -> 'a) -> t -> 'a -> 'a (** [fold f p a] folds f over the monomials of p with non-zero coefficient *) - val add : Monomial.t -> Num.num -> t -> t + val add : Monomial.t -> Q.t -> t -> t (** [add m n p] @return the polynomial n*m + p *) end -type cstr = {coeffs : Vect.t; op : op; cst : Num.num} +type cstr = {coeffs : Vect.t; op : op; cst : Q.t} (* Representation of linear constraints *) and op = Eq | Ge | Gt -val eval_op : op -> Num.num -> Num.num -> bool +val eval_op : op -> Q.t -> Q.t -> bool (*val opMult : op -> op -> op*) @@ -172,7 +173,7 @@ module LinPoly : sig @return 1.y where y is the variable index of the monomial x^1. *) - val coq_poly_of_linpol : (Num.num -> 'a) -> t -> 'a Mc.pExpr + val coq_poly_of_linpol : (Q.t -> 'a) -> t -> 'a Mc.pExpr (** [coq_poly_of_linpol c p] @param p is a multi-variate polynomial. @param c maps a rational to a Coq polynomial coefficient. @@ -206,7 +207,7 @@ module LinPoly : sig @return true if the polynomial is linear in x i.e can be written c*x+r where c is a constant and r is independent from x *) - val constant : Num.num -> t + val constant : Q.t -> t (** [constant c] @return the constant polynomial c *) @@ -216,9 +217,9 @@ module LinPoly : sig p is linear in x i.e x does not occur in b and a is a constant such that [pred a] *) - val search_linear : (Num.num -> bool) -> t -> var option + val search_linear : (Q.t -> bool) -> t -> var option - val search_all_linear : (Num.num -> bool) -> t -> var list + val search_all_linear : (Q.t -> bool) -> t -> var list (** [search_all_linear pred p] @return all the variables x such p = a.x + b such that p is linear in x i.e x does not occur in b and @@ -270,11 +271,11 @@ module ProofFormat : sig | Annot of string * prf_rule | Hyp of int | Def of int - | Cst of Num.num + | Cst of Q.t | Zero | Square of Vect.t | MulC of Vect.t * prf_rule - | Gcd of Big_int.big_int * prf_rule + | Gcd of Z.t * prf_rule | MulPrf of prf_rule * prf_rule | AddPrf of prf_rule * prf_rule | CutPrf of prf_rule @@ -287,20 +288,20 @@ module ProofFormat : sig (* x = z - t, z >= 0, t >= 0 *) - val pr_size : prf_rule -> Num.num + val pr_size : prf_rule -> Q.t val pr_rule_max_id : prf_rule -> int val proof_max_id : proof -> int val normalise_proof : int -> proof -> int * proof val output_prf_rule : out_channel -> prf_rule -> unit val output_proof : out_channel -> proof -> unit val add_proof : prf_rule -> prf_rule -> prf_rule - val mul_cst_proof : Num.num -> prf_rule -> prf_rule + val mul_cst_proof : Q.t -> prf_rule -> prf_rule val mul_proof : prf_rule -> prf_rule -> prf_rule val compile_proof : int list -> proof -> Micromega.zArithProof val cmpl_prf_rule : ('a Micromega.pExpr -> 'a Micromega.pol) - -> (Num.num -> 'a) + -> (Q.t -> 'a) -> int list -> prf_rule -> 'a Micromega.psatz @@ -332,7 +333,7 @@ module WithProof : sig val zero : t (** [zero] represents the tautology (0=0) *) - val const : Num.num -> t + val const : Q.t -> t (** [const n] represents the tautology (n>=0) *) val product : t -> t -> t diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml index 54976221bc..15ab03964e 100644 --- a/plugins/micromega/simplex.ml +++ b/plugins/micromega/simplex.ml @@ -8,10 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open NumCompat +open Q.Notations open Polynomial -open Num - -(*open Util*) open Mutils type ('a, 'b) sum = Inl of 'a | Inr of 'b @@ -118,7 +117,7 @@ let output_vars o m = let unfeasible (rst : Restricted.t) tbl = Restricted.fold rst - (fun k v m -> if Vect.get_cst v >=/ Int 0 then m else IMap.add k () m) + (fun k v m -> if Vect.get_cst v >=/ Q.zero then m else IMap.add k () m) tbl IMap.empty let is_feasible rst tb = IMap.is_empty (unfeasible rst tb) @@ -138,7 +137,7 @@ let is_feasible rst tb = IMap.is_empty (unfeasible rst tb) let is_maximised_vect rst v = Vect.for_all (fun xi ai -> - if ai >/ Int 0 then false else Restricted.is_restricted xi rst) + if ai >/ Q.zero then false else Restricted.is_restricted xi rst) v (** [is_maximised rst v] @@ -161,11 +160,11 @@ let is_maximised rst v = *) type result = - | Max of num (** Maximum is reached *) + | Max of Q.t (** Maximum is reached *) | Ubnd of var (** Problem is unbounded *) | Feas (** Problem is feasible *) -type pivot = Done of result | Pivot of int * int * num +type pivot = Done of result | Pivot of int * int * Q.t type simplex = Opt of tableau * result (** For a row, x = ao.xo+...+ai.xi @@ -180,7 +179,7 @@ let rec find_pivot_column (rst : Restricted.t) (r : Vect.t) = match Vect.choose r with | None -> failwith "find_pivot_column" | Some (xi, ai, r') -> - if ai </ Int 0 then + if ai </ Q.zero then if Restricted.is_restricted xi rst then find_pivot_column rst r' (* ai.xi cannot be improved *) else (xi, -1) (* r is not restricted, sign of ai does not matter *) @@ -207,9 +206,9 @@ let find_pivot_row rst tbl j sgn = Restricted.fold rst (fun i' v res -> let aij = Vect.get j v in - if Int sgn */ aij </ Int 0 then + if Q.of_int sgn */ aij </ Q.zero then (* This would improve *) - let score' = Num.abs_num (Vect.get_cst v // aij) in + let score' = Q.abs (Vect.get_cst v // aij) in min_score res (i', score') else res) tbl None @@ -246,10 +245,10 @@ let find_pivot vr (rst : Restricted.t) tbl = let solve_column (c : var) (r : var) (e : Vect.t) : Vect.t = let a = Vect.get c e in - if a =/ Int 0 then failwith "Cannot solve column" + if a =/ Q.zero then failwith "Cannot solve column" else - let a' = Int (-1) // a in - Vect.mul a' (Vect.set r (Int (-1)) (Vect.set c (Int 0) e)) + let a' = Q.neg_one // a in + Vect.mul a' (Vect.set r Q.neg_one (Vect.set c Q.zero e)) (** [pivot_row r c e] @param c is such that c = e @@ -258,7 +257,7 @@ let solve_column (c : var) (r : var) (e : Vect.t) : Vect.t = let pivot_row (row : Vect.t) (c : var) (e : Vect.t) : Vect.t = let g = Vect.get c row in - if g =/ Int 0 then row else Vect.mul_add g e (Int 1) (Vect.set c (Int 0) row) + if g =/ Q.zero then row else Vect.mul_add g e Q.one (Vect.set c Q.zero row) let pivot_with (m : tableau) (v : var) (p : Vect.t) = IMap.map (fun (r : Vect.t) -> pivot_row r v p) m @@ -270,7 +269,7 @@ let pivot (m : tableau) (r : var) (c : var) = IMap.add c piv (pivot_with (IMap.remove r m) c piv) let adapt_unbounded vr x rst tbl = - if Vect.get_cst (IMap.find vr tbl) >=/ Int 0 then tbl else pivot tbl vr x + if Vect.get_cst (IMap.find vr tbl) >=/ Q.zero then tbl else pivot tbl vr x module BaseSet = Set.Make (struct type t = iset @@ -295,7 +294,7 @@ let simplex opt vr rst tbl = output_tableau stdout tbl; Printf.fprintf stdout "Error for variables %a\n" output_vars m end; - if (not opt) && Vect.get_cst (IMap.find vr tbl) >=/ Int 0 then + if (not opt) && Vect.get_cst (IMap.find vr tbl) >=/ Q.zero then Opt (tbl, Feas) else match find_pivot vr rst tbl with @@ -308,7 +307,7 @@ let simplex opt vr rst tbl = | Feas -> raise (Invalid_argument "find_pivot") ) | Pivot (i, j, s) -> if debug then begin - Printf.fprintf stdout "Find pivot for x%i(%s)\n" vr (string_of_num s); + Printf.fprintf stdout "Find pivot for x%i(%s)\n" vr (Q.to_string s); Printf.fprintf stdout "Leaving variable x%i\n" i; Printf.fprintf stdout "Entering variable x%i\n" j end; @@ -359,14 +358,13 @@ let push_real (opt : bool) (nw : var) (v : Vect.t) (rst : Restricted.t) | Feas -> Sat (t', None) | Max n -> if debug then begin - Printf.printf "The objective is maximised %s\n" (string_of_num n); + Printf.printf "The objective is maximised %s\n" (Q.to_string n); Printf.printf "%a = %a\n" LinPoly.pp_var nw pp_row (IMap.find nw t') end; - if n >=/ Int 0 then Sat (t', None) + if n >=/ Q.zero then Sat (t', None) else let v' = safe_find "push_real" nw t' in - Unsat - (Vect.set nw (Int 1) (Vect.set 0 (Int 0) (Vect.mul (Int (-1)) v'))) ) + Unsat (Vect.set nw Q.one (Vect.set 0 Q.zero (Vect.mul Q.neg_one v'))) ) open Mutils (** One complication is that equalities needs some pre-processing. @@ -381,7 +379,7 @@ let make_certificate vm l = (Vect.fold (fun acc x n -> let x', b = IMap.find x vm in - Vect.set x' (if b then n else Num.minus_num n) acc) + Vect.set x' (if b then n else Q.neg n) acc) Vect.null l) (** [eliminate_equalities vr0 l] @@ -397,11 +395,11 @@ let eliminate_equalities (vr0 : var) (l : Polynomial.cstr list) = | c :: l -> ( match c.op with | Ge -> - let v = Vect.set 0 (minus_num c.cst) c.coeffs in + let v = Vect.set 0 (Q.neg c.cst) c.coeffs in elim (idx + 1) (vr + 1) (IMap.add vr (idx, true) vm) l ((vr, v) :: acc) | Eq -> - let v1 = Vect.set 0 (minus_num c.cst) c.coeffs in - let v2 = Vect.mul (Int (-1)) v1 in + let v1 = Vect.set 0 (Q.neg c.cst) c.coeffs in + let v2 = Vect.mul Q.neg_one v1 in let vm = IMap.add vr (idx, true) (IMap.add (vr + 1) (idx, false) vm) in elim (idx + 1) (vr + 2) vm l ((vr, v1) :: (vr + 1, v2) :: acc) | Gt -> raise Strict ) @@ -419,7 +417,7 @@ let find_full_solution rst tbl = IMap.fold (fun vr v res -> Vect.set vr (Vect.get_cst v) res) tbl Vect.null let choose_conflict (sol : Vect.t) (l : (var * Vect.t) list) = - let esol = Vect.set 0 (Int 1) sol in + let esol = Vect.set 0 Q.one sol in let rec most_violating l e (x, v) rst = match l with | [] -> Some ((x, v), rst) @@ -476,7 +474,7 @@ let optimise obj l = let _, vm, l' = eliminate_equalities (vr0 + 1) l in let bound pos res = match res with - | Opt (_, Max n) -> Some (if pos then n else minus_num n) + | Opt (_, Max n) -> Some (if pos then n else Q.neg n) | Opt (_, Ubnd _) -> None | Opt (_, Feas) -> None in @@ -501,9 +499,7 @@ let make_farkas_certificate (env : WithProof.t IMap.t) vm v = begin try let x', b = IMap.find x vm in - mul_cst_proof - (if b then n else Num.minus_num n) - (snd (IMap.find x' env)) + mul_cst_proof (if b then n else Q.neg n) (snd (IMap.find x' env)) with Not_found -> (* This is an introduced hypothesis *) mul_cst_proof n (snd (IMap.find x env)) @@ -517,7 +513,7 @@ let make_farkas_proof (env : WithProof.t IMap.t) vm v = begin try let x', b = IMap.find x vm in - let n = if b then n else Num.minus_num n in + let n = if b then n else Q.neg n in let prf = IMap.find x' env in WithProof.mult (Vect.cst n) prf with Not_found -> @@ -526,7 +522,7 @@ let make_farkas_proof (env : WithProof.t IMap.t) vm v = end) WithProof.zero v -let frac_num n = n -/ Num.floor_num n +let frac_num n = n -/ Q.floor n type ('a, 'b) hitkind = | Forget @@ -538,38 +534,38 @@ type ('a, 'b) hitkind = let cut env rmin sol vm (rst : Restricted.t) tbl (x, v) = let n, r = Vect.decomp_cst v in let fn = frac_num n in - if fn =/ Int 0 then Forget (* The solution is integral *) + if fn =/ Q.zero then Forget (* The solution is integral *) else (* The cut construction is from: Letchford and Lodi. Strengthening Chvatal-Gomory cuts and Gomory fractional cuts. We implement the classic Proposition 2 from the "known results" - *) + *) (* Proposition 3 requires all the variables to be restricted and is therefore not always applicable. *) (* let ccoeff_prop1 v = frac_num v in - let ccoeff_prop3 v = - (* mixed integer cut *) - let fv = frac_num v in - Num.min_num fv (fn */ (Int 1 -/ fv) // (Int 1 -/ fn)) - in - let ccoeff_prop3 = - if Restricted.is_restricted x rst then ("Prop3", ccoeff_prop3) - else ("Prop1", ccoeff_prop1) - in *) - let n0_5 = Int 1 // Int 2 in + let ccoeff_prop3 v = + (* mixed integer cut *) + let fv = frac_num v in + Num.min_num fv (fn */ (Q.one -/ fv) // (Q.one -/ fn)) + in + let ccoeff_prop3 = + if Restricted.is_restricted x rst then ("Prop3", ccoeff_prop3) + else ("Prop1", ccoeff_prop1) + in *) + let n0_5 = Q.one // Q.two in (* If the fractional part [fn] is small, we construct the t-cut. If the fractional part [fn] is big, we construct the t-cut of the negated row. (This is only a cut if all the fractional variables are restricted.) - *) + *) let ccoeff_prop2 = let tmin = if fn </ n0_5 then (* t-cut *) - Num.ceiling_num (n0_5 // fn) + Q.ceiling (n0_5 // fn) else (* multiply by -1 & t-cut *) - minus_num (Num.ceiling_num (n0_5 // (Int 1 -/ fn))) + Q.neg (Q.ceiling (n0_5 // (Q.one -/ fn))) in ("Prop2", fun v -> frac_num (v */ tmin)) in @@ -651,7 +647,7 @@ let eliminate_variable (bounded, vr, env, tbl) x = let tv = var_of_vect t in (* x = z - t *) let xdef = Vect.add z (Vect.uminus t) in - let xp = ((Vect.set x (Int 1) (Vect.uminus xdef), Eq), Def vr) in + let xp = ((Vect.set x Q.one (Vect.uminus xdef), Eq), Def vr) in let zp = ((z, Ge), Def zv) in let tp = ((t, Ge), Def tv) in (* Pivot the current tableau using xdef *) @@ -662,11 +658,8 @@ let eliminate_variable (bounded, vr, env, tbl) x = (fun lp -> let (v, o), p = lp in let ai = Vect.get x v in - if ai =/ Int 0 then lp - else - WithProof.addition - (WithProof.mult (Vect.cst (Num.minus_num ai)) xp) - lp) + if ai =/ Q.zero then lp + else WithProof.addition (WithProof.mult (Vect.cst (Q.neg ai)) xp) lp) env in (* Add the variables to the environment *) diff --git a/plugins/micromega/simplex.mli b/plugins/micromega/simplex.mli index ff672edafd..8edea2d4b2 100644 --- a/plugins/micromega/simplex.mli +++ b/plugins/micromega/simplex.mli @@ -7,6 +7,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) + +open NumCompat open Polynomial (** Profiling *) @@ -23,7 +25,7 @@ val get_profile_info : unit -> profile_info (** Simplex interface *) -val optimise : Vect.t -> cstr list -> (Num.num option * Num.num option) option +val optimise : Vect.t -> cstr list -> (Q.t option * Q.t option) option val find_point : cstr list -> Vect.t option val find_unsat_certificate : cstr list -> Vect.t option diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml index 772ed7a8c5..2b04bb80e2 100644 --- a/plugins/micromega/sos.ml +++ b/plugins/micromega/sos.ml @@ -9,7 +9,9 @@ (* ========================================================================= *) (* Nonlinear universal reals procedure using SOS decomposition. *) (* ========================================================================= *) -open Num + +open NumCompat +open Q.Notations open Sos_types open Sos_lib @@ -27,19 +29,19 @@ exception Sanity let decimalize = let rec normalize y = - if abs_num y </ Int 1 // Int 10 then normalize (Int 10 */ y) - 1 - else if abs_num y >=/ Int 1 then normalize (y // Int 10) + 1 + if Q.abs y </ Q.one // Q.ten then normalize (Q.ten */ y) - 1 + else if Q.abs y >=/ Q.one then normalize (y // Q.ten) + 1 else 0 in fun d x -> - if x =/ Int 0 then "0.0" + if x =/ Q.zero then "0.0" else - let y = abs_num x in + let y = Q.abs x in let e = normalize y in - let z = (pow10 (-e) */ y) +/ Int 1 in - let k = round_num (pow10 d */ z) in - (if x </ Int 0 then "-0." else "0.") - ^ implode (List.tl (explode (string_of_num k))) + let z = (Q.pow10 (-e) */ y) +/ Q.one in + let k = Q.round (Q.pow10 d */ z) in + (if x </ Q.zero then "-0." else "0.") + ^ implode (List.tl (explode (Q.to_string k))) ^ if e = 0 then "" else "e" ^ string_of_int e (* ------------------------------------------------------------------------- *) @@ -55,22 +57,22 @@ let rec iter (m, n) f a = if n < m then a else iter (m + 1, n) f (f m a) (* The main types. *) (* ------------------------------------------------------------------------- *) -type vector = int * (int, num) func -type matrix = (int * int) * (int * int, num) func +type vector = int * (int, Q.t) func +type matrix = (int * int) * (int * int, Q.t) func type monomial = (vname, int) func -type poly = (monomial, num) func +type poly = (monomial, Q.t) func (* ------------------------------------------------------------------------- *) (* Assignment avoiding zeros. *) (* ------------------------------------------------------------------------- *) -let ( |--> ) x y a = if y =/ Int 0 then a else (x |-> y) a +let ( |--> ) x y a = if y =/ Q.zero then a else (x |-> y) a (* ------------------------------------------------------------------------- *) (* This can be generic. *) (* ------------------------------------------------------------------------- *) -let element (d, v) i = tryapplyd v i (Int 0) +let element (d, v) i = tryapplyd v i Q.zero let mapa f (d, v) = (d, foldl (fun a i c -> (i |--> f c) a) undefined v) let is_zero (d, v) = match v with Empty -> true | _ -> false @@ -82,12 +84,12 @@ let vector_0 n = ((n, undefined) : vector) let dim (v : vector) = fst v let vector_const c n = - if c =/ Int 0 then vector_0 n + if c =/ Q.zero then vector_0 n else ((n, List.fold_right (fun k -> k |-> c) (1 -- n) undefined) : vector) let vector_cmul c (v : vector) = let n = dim v in - if c =/ Int 0 then vector_0 n else (n, mapf (fun x -> c */ x) (snd v)) + if c =/ Q.zero then vector_0 n else (n, mapf (fun x -> c */ x) (snd v)) let vector_of_list l = let n = List.length l in @@ -102,15 +104,15 @@ let dimensions (m : matrix) = fst m let matrix_cmul c (m : matrix) = let i, j = dimensions m in - if c =/ Int 0 then matrix_0 (i, j) + if c =/ Q.zero then matrix_0 (i, j) else ((i, j), mapf (fun x -> c */ x) (snd m)) -let matrix_neg (m : matrix) = ((dimensions m, mapf minus_num (snd m)) : matrix) +let matrix_neg (m : matrix) = ((dimensions m, mapf Q.neg (snd m)) : matrix) let matrix_add (m1 : matrix) (m2 : matrix) = let d1 = dimensions m1 and d2 = dimensions m2 in if d1 <> d2 then failwith "matrix_add: incompatible dimensions" - else ((d1, combine ( +/ ) (fun x -> x =/ Int 0) (snd m1) (snd m2)) : matrix) + else ((d1, combine ( +/ ) (fun x -> x =/ Q.zero) (snd m1) (snd m2)) : matrix) let row k (m : matrix) = let i, j = dimensions m in @@ -150,21 +152,21 @@ let monomial_variables m = dom m (* ------------------------------------------------------------------------- *) let poly_0 = (undefined : poly) let poly_isconst (p : poly) = foldl (fun a m c -> m = monomial_1 && a) true p -let poly_var x = (monomial_var x |=> Int 1 : poly) -let poly_const c = if c =/ Int 0 then poly_0 else monomial_1 |=> c +let poly_var x = (monomial_var x |=> Q.one : poly) +let poly_const c = if c =/ Q.zero then poly_0 else monomial_1 |=> c let poly_cmul c (p : poly) = - if c =/ Int 0 then poly_0 else mapf (fun x -> c */ x) p + if c =/ Q.zero then poly_0 else mapf (fun x -> c */ x) p -let poly_neg (p : poly) = (mapf minus_num p : poly) +let poly_neg (p : poly) = (mapf Q.neg p : poly) let poly_add (p1 : poly) (p2 : poly) = - (combine ( +/ ) (fun x -> x =/ Int 0) p1 p2 : poly) + (combine ( +/ ) (fun x -> x =/ Q.zero) p1 p2 : poly) let poly_sub p1 p2 = poly_add p1 (poly_neg p2) let poly_cmmul (c, m) (p : poly) = - if c =/ Int 0 then poly_0 + if c =/ Q.zero then poly_0 else if m = monomial_1 then mapf (fun d -> c */ d) p else foldl (fun a m' d -> (monomial_mul m m' |-> c */ d) a) poly_0 p @@ -174,7 +176,7 @@ let poly_mul (p1 : poly) (p2 : poly) = let poly_square p = poly_mul p p let rec poly_pow p k = - if k = 0 then poly_const (Int 1) + if k = 0 then poly_const Q.one else if k = 1 then p else let q = poly_square (poly_pow p (k / 2)) in @@ -228,9 +230,9 @@ let string_of_monomial m = String.concat "*" vps let string_of_cmonomial (c, m) = - if m = monomial_1 then string_of_num c - else if c =/ Int 1 then string_of_monomial m - else string_of_num c ^ "*" ^ string_of_monomial m + if m = monomial_1 then Q.to_string c + else if c =/ Q.one then string_of_monomial m + else Q.to_string c ^ "*" ^ string_of_monomial m let string_of_poly (p : poly) = if p = poly_0 then "<<0>>" @@ -241,7 +243,7 @@ let string_of_poly (p : poly) = let s = List.fold_left (fun a (m, c) -> - if c </ Int 0 then a ^ " - " ^ string_of_cmonomial (minus_num c, m) + if c </ Q.zero then a ^ " - " ^ string_of_cmonomial (Q.neg c, m) else a ^ " + " ^ string_of_cmonomial (c, m)) "" cms in @@ -338,21 +340,19 @@ let token s = let decimal = let ( || ) = parser_or in let numeral = some isnum in - let decimalint = atleast 1 numeral >> o Num.num_of_string implode in + let decimalint = atleast 1 numeral >> o Q.of_string implode in let decimalfrac = atleast 1 numeral - >> fun s -> Num.num_of_string (implode s) // pow10 (List.length s) + >> fun s -> Q.of_string (implode s) // Q.pow10 (List.length s) in let decimalsig = decimalint ++ possibly (a "." ++ decimalfrac >> snd) >> function h, [x] -> h +/ x | h, _ -> h in - let signed prs = - a "-" ++ prs >> o minus_num snd || a "+" ++ prs >> snd || prs - in + let signed prs = a "-" ++ prs >> o Q.neg snd || a "+" ++ prs >> snd || prs in let exponent = (a "e" || a "E") ++ signed decimalint >> snd in signed decimalsig ++ possibly exponent - >> function h, [x] -> h */ power_num (Int 10) x | h, _ -> h + >> function h, [x] -> h */ Q.power 10 x | h, _ -> h let mkparser p s = let x, rst = p (explode s) in @@ -469,19 +469,19 @@ let run_csdp dbg obj mats = let scale_then = let common_denominator amat acc = - foldl (fun a m c -> lcm_num (denominator c) a) acc amat + foldl (fun a m c -> Z.lcm (Q.den c) a) acc amat and maximal_element amat acc = - foldl (fun maxa m c -> max_num maxa (abs_num c)) acc amat + foldl (fun maxa m c -> Q.max maxa (Q.abs c)) acc amat in fun solver obj mats -> - let cd1 = List.fold_right common_denominator mats (Int 1) - and cd2 = common_denominator (snd obj) (Int 1) in + let cd1 = Q.of_bigint @@ List.fold_right common_denominator mats Z.one + and cd2 = Q.of_bigint @@ common_denominator (snd obj) Z.one in let mats' = List.map (mapf (fun x -> cd1 */ x)) mats and obj' = vector_cmul cd2 obj in - let max1 = List.fold_right maximal_element mats' (Int 0) - and max2 = maximal_element (snd obj') (Int 0) in - let scal1 = pow2 (20 - int_of_float (log (float_of_num max1) /. log 2.0)) - and scal2 = pow2 (20 - int_of_float (log (float_of_num max2) /. log 2.0)) in + let max1 = List.fold_right maximal_element mats' Q.zero + and max2 = maximal_element (snd obj') Q.zero in + let scal1 = Q.pow2 (20 - int_of_float (log (Q.to_float max1) /. log 2.0)) + and scal2 = Q.pow2 (20 - int_of_float (log (Q.to_float max2) /. log 2.0)) in let mats'' = List.map (mapf (fun x -> x */ scal1)) mats' and obj'' = vector_cmul scal2 obj' in solver obj'' mats'' @@ -490,7 +490,7 @@ let scale_then = (* Round a vector to "nice" rationals. *) (* ------------------------------------------------------------------------- *) -let nice_rational n x = round_num (n */ x) // n +let nice_rational n x = Q.round (n */ x) // n let nice_vector n = mapa (nice_rational n) (* ------------------------------------------------------------------------- *) @@ -501,7 +501,7 @@ let nice_vector n = mapa (nice_rational n) let linear_program_basic a = let m, n = dimensions a in let mats = List.map (fun j -> diagonal (column j a)) (1 -- n) - and obj = vector_const (Int 1) m in + and obj = vector_const Q.one m in let rv, res = run_csdp false obj mats in if rv = 1 || rv = 2 then false else if rv = 0 then true @@ -521,8 +521,8 @@ let in_convex_hull pts pt = let mat = ( (m, n) , itern 1 pts2 - (fun pts j -> itern 1 pts (fun x i -> (i, j) |-> Int x)) - (iter (1, n) (fun i -> (v + i, i + 1) |-> Int 1) undefined) ) + (fun pts j -> itern 1 pts (fun x i -> (i, j) |-> Q.of_int x)) + (iter (1, n) (fun i -> (v + i, i + 1) |-> Q.one) undefined) ) in linear_program_basic mat @@ -544,12 +544,14 @@ let minimal_convex_hull = (* Stuff for "equations" (generic A->num functions). *) (* ------------------------------------------------------------------------- *) -let equation_cmul c eq = if c =/ Int 0 then Empty else mapf (fun d -> c */ d) eq -let equation_add eq1 eq2 = combine ( +/ ) (fun x -> x =/ Int 0) eq1 eq2 +let equation_cmul c eq = + if c =/ Q.zero then Empty else mapf (fun d -> c */ d) eq + +let equation_add eq1 eq2 = combine ( +/ ) (fun x -> x =/ Q.zero) eq1 eq2 let equation_eval assig eq = let value v = apply assig v in - foldl (fun a v c -> a +/ (value v */ c)) (Int 0) eq + foldl (fun a v c -> a +/ (value v */ c)) Q.zero eq (* ------------------------------------------------------------------------- *) (* Eliminate all variables, in an essentially arbitrary order. *) @@ -574,11 +576,11 @@ let eliminate_all_equations one = else let v = choose_variable eq in let a = apply eq v in - let eq' = equation_cmul (Int (-1) // a) (undefine v eq) in + let eq' = equation_cmul (Q.neg_one // a) (undefine v eq) in let elim e = - let b = tryapplyd e v (Int 0) in - if b =/ Int 0 then e - else equation_add e (equation_cmul (minus_num b // a) eq) + let b = tryapplyd e v Q.zero in + if b =/ Q.zero then e + else equation_add e (equation_cmul (Q.neg b // a) eq) in eliminate ((v |-> eq') (mapf elim dun)) (List.map elim oeqs) in @@ -631,8 +633,8 @@ let diag m = if is_zero m then [] else let a11 = element m (i, i) in - if a11 </ Int 0 then failwith "diagonalize: not PSD" - else if a11 =/ Int 0 then + if a11 </ Q.zero then failwith "diagonalize: not PSD" + else if a11 =/ Q.zero then if is_zero (row i m) then diagonalize (i + 1) m else failwith "diagonalize: not PSD" else @@ -659,21 +661,23 @@ let diag m = (* ------------------------------------------------------------------------- *) let deration d = - if d = [] then (Int 0, d) + if d = [] then (Q.zero, d) else let adj (c, l) = let a = - foldl (fun a i c -> lcm_num a (denominator c)) (Int 1) (snd l) - // foldl (fun a i c -> gcd_num a (numerator c)) (Int 0) (snd l) + Q.make + (foldl (fun a i c -> Z.lcm a (Q.den c)) Z.one (snd l)) + (foldl (fun a i c -> Z.gcd a (Q.num c)) Z.zero (snd l)) in (c // (a */ a), mapa (fun x -> a */ x) l) in let d' = List.map adj d in let a = - List.fold_right (o lcm_num (o denominator fst)) d' (Int 1) - // List.fold_right (o gcd_num (o numerator fst)) d' (Int 0) + Q.make + (List.fold_right (o Z.lcm (o Q.den fst)) d' Z.one) + (List.fold_right (o Z.gcd (o Q.num fst)) d' Z.zero) in - (Int 1 // a, List.map (fun (c, l) -> (a */ c, l)) d') + (Q.one // a, List.map (fun (c, l) -> (a */ c, l)) d') (* ------------------------------------------------------------------------- *) (* Enumeration of monomials with given multidegree bound. *) @@ -702,11 +706,11 @@ let rec enumerate_monomials d vars = (* ------------------------------------------------------------------------- *) let rec enumerate_products d pols = - if d = 0 then [(poly_const num_1, Rational_lt num_1)] + if d = 0 then [(poly_const Q.one, Rational_lt Q.one)] else if d < 0 then [] else match pols with - | [] -> [(poly_const num_1, Rational_lt num_1)] + | [] -> [(poly_const Q.one, Rational_lt Q.one)] | (p, b) :: ps -> let e = multidegree p in if e = 0 then enumerate_products d ps @@ -736,7 +740,7 @@ let epoly_pmul p q acc = (* ------------------------------------------------------------------------- *) let epoly_of_poly p = - foldl (fun a m c -> (m |-> ((0, 0, 0) |=> minus_num c)) a) undefined p + foldl (fun a m c -> (m |-> ((0, 0, 0) |=> Q.neg c)) a) undefined p (* ------------------------------------------------------------------------- *) (* String for block diagonal matrix numbered k. *) @@ -796,7 +800,7 @@ let csdp nblocks blocksizes obj mats = if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible" else if rv = 3 then () (*Format.print_string "csdp warning: Reduced accuracy"; - Format.print_newline() *) + Format.print_newline() *) else if rv <> 0 then failwith ("csdp: error " ^ string_of_int rv) else (); res @@ -805,12 +809,12 @@ let csdp nblocks blocksizes obj mats = (* 3D versions of matrix operations to consider blocks separately. *) (* ------------------------------------------------------------------------- *) -let bmatrix_add = combine ( +/ ) (fun x -> x =/ Int 0) +let bmatrix_add = combine ( +/ ) (fun x -> x =/ Q.zero) let bmatrix_cmul c bm = - if c =/ Int 0 then undefined else mapf (fun x -> c */ x) bm + if c =/ Q.zero then undefined else mapf (fun x -> c */ x) bm -let bmatrix_neg = bmatrix_cmul (Int (-1)) +let bmatrix_neg = bmatrix_cmul Q.neg_one (* ------------------------------------------------------------------------- *) (* Smash a block matrix into components. *) @@ -839,7 +843,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = in let monoid = if linf then - (poly_const num_1, Rational_lt num_1) + (poly_const Q.one, Rational_lt Q.one) :: List.filter (fun (p, c) -> multidegree p <= d) leqs else enumerate_products d leqs in @@ -850,7 +854,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = let nons = List.combine mons (1 -- List.length mons) in ( mons , List.fold_right - (fun (m, n) -> m |-> ((-k, -n, n) |=> Int 1)) + (fun (m, n) -> m |-> ((-k, -n, n) |=> Q.one)) nons undefined ) in let mk_sqmultiplier k (p, c) = @@ -865,7 +869,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = let m = monomial_mul m1 m2 in if n1 > n2 then a else - let c = if n1 = n2 then Int 1 else Int 2 in + let c = if n1 = n2 then Q.one else Q.two in let e = tryapplyd a m undefined in (m |-> equation_add ((k, n1, n2) |=> c) e) a) nons) @@ -889,14 +893,14 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = let eqns = foldl (fun a m e -> e :: a) [] bigsum in let pvs, assig = eliminate_all_equations (0, 0, 0) eqns in let qvars = (0, 0, 0) :: pvs in - let allassig = List.fold_right (fun v -> v |-> (v |=> Int 1)) pvs assig in + let allassig = List.fold_right (fun v -> v |-> (v |=> Q.one)) pvs assig in let mk_matrix v = foldl (fun m (b, i, j) ass -> if b < 0 then m else - let c = tryapplyd ass v (Int 0) in - if c =/ Int 0 then m else ((b, j, i) |-> c) (((b, i, j) |-> c) m)) + let c = tryapplyd ass v Q.zero in + if c =/ Q.zero then m else ((b, j, i) |-> c) (((b, i, j) |-> c) m)) undefined allassig in let diagents = @@ -907,7 +911,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = let mats = List.map mk_matrix qvars and obj = ( List.length pvs - , itern 1 pvs (fun v i -> i |--> tryapplyd diagents v (Int 0)) undefined ) + , itern 1 pvs (fun v i -> i |--> tryapplyd diagents v Q.zero) undefined ) in let raw_vec = if pvs = [] then vector_0 0 @@ -915,7 +919,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = in let find_rounding d = if !debugging then ( - Format.print_string ("Trying rounding with limit " ^ string_of_num d); + Format.print_string ("Trying rounding with limit " ^ Q.to_string d); Format.print_newline () ) else (); let vec = nice_vector d raw_vec in @@ -930,16 +934,16 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = (vec, List.map diag allmats) in let vec, ratdias = - if pvs = [] then find_rounding num_1 + if pvs = [] then find_rounding Q.one else tryfind find_rounding - (List.map Num.num_of_int (1 -- 31) @ List.map pow2 (5 -- 66)) + (List.map Q.of_int (1 -- 31) @ List.map Q.pow2 (5 -- 66)) in let newassigs = List.fold_right (fun k -> List.nth pvs (k - 1) |-> element vec k) (1 -- dim vec) - ((0, 0, 0) |=> Int (-1)) + ((0, 0, 0) |=> Q.neg_one) in let finalassigs = foldl (fun a v e -> (v |-> equation_eval newassigs e) a) newassigs allassig @@ -1017,7 +1021,7 @@ let monomial_order = let term_of_varpow x k = if k = 1 then Var x else Pow (Var x, k) let term_of_monomial m = - if m = monomial_1 then Const num_1 + if m = monomial_1 then Const Q.one else let m' = dest_monomial m in let vps = List.fold_right (fun (x, k) a -> term_of_varpow x k :: a) m' [] in @@ -1025,7 +1029,7 @@ let term_of_monomial m = let term_of_cmonomial (m, c) = if m = monomial_1 then Const c - else if c =/ num_1 then term_of_monomial m + else if c =/ Q.one then term_of_monomial m else Mul (Const c, term_of_monomial m) let term_of_poly p = @@ -1114,8 +1118,8 @@ let csdp obj mats = let rv, res = run_csdp !debugging obj mats in if rv = 1 || rv = 2 then failwith "csdp: Problem is infeasible" else if rv = 3 then () - (* (Format.print_string "csdp warning: Reduced accuracy"; - Format.print_newline()) *) + (* (Format.print_string "csdp warning: Reduced accuracy"; + Format.print_newline()) *) else if rv <> 0 then failwith ("csdp: error " ^ string_of_int rv) else (); res @@ -1162,7 +1166,7 @@ let sumofsquares_general_symmetry tool pol = match cls with | [] -> raise Sanity | [h] -> acc - | h :: t -> List.map (fun k -> (k |-> Int (-1)) (h |=> Int 1)) t @ acc + | h :: t -> List.map (fun k -> (k |-> Q.neg_one) (h |=> Q.one)) t @ acc in List.fold_right mk_eq eqvcls [] in @@ -1176,13 +1180,13 @@ let sumofsquares_general_symmetry tool pol = let m = monomial_mul m1 m2 in if n1 > n2 then f else - let c = if n1 = n2 then Int 1 else Int 2 in + let c = if n1 = n2 then Q.one else Q.two in (m |-> ((n1, n2) |-> c) (tryapplyd f m undefined)) f)) (foldl (fun a m c -> (m |-> ((0, 0) |=> c)) a) undefined pol)) @ sym_eqs in let pvs, assig = eliminate_all_equations (0, 0) eqs in - let allassig = List.fold_right (fun v -> v |-> (v |=> Int 1)) pvs assig in + let allassig = List.fold_right (fun v -> v |-> (v |=> Q.one)) pvs assig in let qvars = (0, 0) :: pvs in let diagents = end_itlist equation_add (List.map (fun i -> apply allassig (i, i)) (1 -- n)) @@ -1191,20 +1195,20 @@ let sumofsquares_general_symmetry tool pol = ( ( (n, n) , foldl (fun m (i, j) ass -> - let c = tryapplyd ass v (Int 0) in - if c =/ Int 0 then m else ((j, i) |-> c) (((i, j) |-> c) m)) + let c = tryapplyd ass v Q.zero in + if c =/ Q.zero then m else ((j, i) |-> c) (((i, j) |-> c) m)) undefined allassig ) : matrix ) in let mats = List.map mk_matrix qvars and obj = ( List.length pvs - , itern 1 pvs (fun v i -> i |--> tryapplyd diagents v (Int 0)) undefined ) + , itern 1 pvs (fun v i -> i |--> tryapplyd diagents v Q.zero) undefined ) in let raw_vec = if pvs = [] then vector_0 0 else tool obj mats in let find_rounding d = if !debugging then ( - Format.print_string ("Trying rounding with limit " ^ string_of_num d); + Format.print_string ("Trying rounding with limit " ^ Q.to_string d); Format.print_newline () ) else (); let vec = nice_vector d raw_vec in @@ -1223,7 +1227,7 @@ let sumofsquares_general_symmetry tool pol = deration (diag mat) else tryfind find_rounding - (List.map Num.num_of_int (1 -- 31) @ List.map pow2 (5 -- 66)) + (List.map Q.of_int (1 -- 31) @ List.map Q.pow2 (5 -- 66)) in let poly_of_lin (d, v) = (d, foldl (fun a i c -> (List.nth lpps (i - 1) |-> c) a) undefined (snd v)) diff --git a/plugins/micromega/sos.mli b/plugins/micromega/sos.mli index ac75bd37f0..8a461b4c20 100644 --- a/plugins/micromega/sos.mli +++ b/plugins/micromega/sos.mli @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open NumCompat open Sos_types type poly @@ -16,13 +17,10 @@ val poly_isconst : poly -> bool val poly_neg : poly -> poly val poly_mul : poly -> poly -> poly val poly_pow : poly -> int -> poly -val poly_const : Num.num -> poly +val poly_const : Q.t -> poly val poly_of_term : term -> poly val term_of_poly : poly -> term - -val term_of_sos : - positivstellensatz * (Num.num * poly) list -> positivstellensatz - +val term_of_sos : positivstellensatz * (Q.t * poly) list -> positivstellensatz val string_of_poly : poly -> string val real_positivnullstellensatz_general : @@ -31,6 +29,6 @@ val real_positivnullstellensatz_general : -> poly list -> (poly * positivstellensatz) list -> poly - -> poly list * (positivstellensatz * (Num.num * poly) list) list + -> poly list * (positivstellensatz * (Q.t * poly) list) list -val sumofsquares : poly -> Num.num * (Num.num * poly) list +val sumofsquares : poly -> Q.t * (Q.t * poly) list diff --git a/plugins/micromega/sos_lib.ml b/plugins/micromega/sos_lib.ml index 51221aa6b9..99c552e379 100644 --- a/plugins/micromega/sos_lib.ml +++ b/plugins/micromega/sos_lib.ml @@ -7,8 +7,6 @@ (* - Frédéric Besson (fbesson@irisa.fr) is using it to feed micromega *) (* ========================================================================= *) -open Num - (* ------------------------------------------------------------------------- *) (* Comparisons that are reflexive on NaN and also short-circuiting. *) (* ------------------------------------------------------------------------- *) @@ -28,32 +26,6 @@ let ( >? ) x y = cmp x y > 0 let o f g x = f (g x) (* ------------------------------------------------------------------------- *) -(* Some useful functions on "num" type. *) -(* ------------------------------------------------------------------------- *) - -let num_0 = Int 0 -and num_1 = Int 1 -and num_2 = Int 2 -and num_10 = Int 10 - -let pow2 n = power_num num_2 (Int n) -let pow10 n = power_num num_10 (Int n) - -let numdom r = - let r' = Ratio.normalize_ratio (ratio_of_num r) in - ( num_of_big_int (Ratio.numerator_ratio r') - , num_of_big_int (Ratio.denominator_ratio r') ) - -let numerator = o fst numdom -and denominator = o snd numdom - -let gcd_num n1 n2 = - num_of_big_int (Big_int.gcd_big_int (big_int_of_num n1) (big_int_of_num n2)) - -let lcm_num x y = - if x =/ num_0 && y =/ num_0 then num_0 else abs_num (x */ y // gcd_num x y) - -(* ------------------------------------------------------------------------- *) (* Various versions of list iteration. *) (* ------------------------------------------------------------------------- *) @@ -518,8 +490,8 @@ let deepen_until limit f n = let rec d_until f n = try (* if !debugging - then (print_string "Searching with depth limit "; - print_int n; print_newline()) ;*) + then (print_string "Searching with depth limit "; + print_int n; print_newline()) ;*) f n with Failure x -> (*if !debugging then (Printf.printf "solver error : %s\n" x) ; *) diff --git a/plugins/micromega/sos_lib.mli b/plugins/micromega/sos_lib.mli index 2bbcbf336b..7795808e12 100644 --- a/plugins/micromega/sos_lib.mli +++ b/plugins/micromega/sos_lib.mli @@ -9,9 +9,6 @@ (************************************************************************) val o : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b -val num_1 : Num.num -val pow10 : int -> Num.num -val pow2 : int -> Num.num val implode : string list -> string val explode : string -> string list val funpow : int -> ('a -> 'a) -> 'a -> 'a @@ -50,10 +47,6 @@ val sort : ('a -> 'a -> bool) -> 'a list -> 'a list val setify : 'a list -> 'a list val increasing : ('a -> 'b) -> 'a -> 'a -> bool val allpairs : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list -val gcd_num : Num.num -> Num.num -> Num.num -val lcm_num : Num.num -> Num.num -> Num.num -val numerator : Num.num -> Num.num -val denominator : Num.num -> Num.num val end_itlist : ('a -> 'a -> 'a) -> 'a list -> 'a val ( >> ) : ('a -> 'b * 'c) -> ('b -> 'd) -> 'a -> 'd * 'c val ( ++ ) : ('a -> 'b * 'c) -> ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e diff --git a/plugins/micromega/sos_types.ml b/plugins/micromega/sos_types.ml index 988024968b..62699d8362 100644 --- a/plugins/micromega/sos_types.ml +++ b/plugins/micromega/sos_types.ml @@ -9,13 +9,13 @@ (************************************************************************) (* The type of positivstellensatz -- used to communicate with sos *) -open Num - type vname = string +open NumCompat + type term = | Zero - | Const of Num.num + | Const of Q.t | Var of vname | Opp of term | Add of (term * term) @@ -26,7 +26,7 @@ type term = let rec output_term o t = match t with | Zero -> output_string o "0" - | Const n -> output_string o (string_of_num n) + | Const n -> output_string o (Q.to_string n) | Var n -> Printf.fprintf o "v%s" n | Opp t -> Printf.fprintf o "- (%a)" output_term t | Add (t1, t2) -> Printf.fprintf o "(%a)+(%a)" output_term t1 output_term t2 @@ -42,9 +42,9 @@ type positivstellensatz = | Axiom_eq of int | Axiom_le of int | Axiom_lt of int - | Rational_eq of num - | Rational_le of num - | Rational_lt of num + | Rational_eq of Q.t + | Rational_le of Q.t + | Rational_lt of Q.t | Square of term | Monoid of int list | Eqmul of term * positivstellensatz @@ -55,9 +55,9 @@ let rec output_psatz o = function | Axiom_eq i -> Printf.fprintf o "Aeq(%i)" i | Axiom_le i -> Printf.fprintf o "Ale(%i)" i | Axiom_lt i -> Printf.fprintf o "Alt(%i)" i - | Rational_eq n -> Printf.fprintf o "eq(%s)" (string_of_num n) - | Rational_le n -> Printf.fprintf o "le(%s)" (string_of_num n) - | Rational_lt n -> Printf.fprintf o "lt(%s)" (string_of_num n) + | Rational_eq n -> Printf.fprintf o "eq(%s)" (Q.to_string n) + | Rational_le n -> Printf.fprintf o "le(%s)" (Q.to_string n) + | Rational_lt n -> Printf.fprintf o "lt(%s)" (Q.to_string n) | Square t -> Printf.fprintf o "(%a)^2" output_term t | Monoid l -> Printf.fprintf o "monoid" | Eqmul (t, ps) -> Printf.fprintf o "%a * %a" output_term t output_psatz ps diff --git a/plugins/micromega/sos_types.mli b/plugins/micromega/sos_types.mli index ca9a43b1d0..a0b9157880 100644 --- a/plugins/micromega/sos_types.mli +++ b/plugins/micromega/sos_types.mli @@ -8,13 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open NumCompat + (* The type of positivstellensatz -- used to communicate with sos *) type vname = string type term = | Zero - | Const of Num.num + | Const of Q.t | Var of vname | Opp of term | Add of (term * term) @@ -28,9 +30,9 @@ type positivstellensatz = | Axiom_eq of int | Axiom_le of int | Axiom_lt of int - | Rational_eq of Num.num - | Rational_le of Num.num - | Rational_lt of Num.num + | Rational_eq of Q.t + | Rational_le of Q.t + | Rational_lt of Q.t | Square of term | Monoid of int list | Eqmul of term * positivstellensatz diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml index f53a7b42c9..198430295b 100644 --- a/plugins/micromega/vect.ml +++ b/plugins/micromega/vect.ml @@ -8,7 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Num +open NumCompat +open Q.Notations open Mutils type var = int @@ -18,7 +19,7 @@ type var = int - values are all non-zero *) -type t = (var * num) list +type t = (var * Q.t) list type vector = t (** [equal v1 v2 = true] if the vectors are syntactically equal. *) @@ -33,32 +34,30 @@ let rec equal v1 v2 = let hash v = let rec hash i = function | [] -> i - | (vr, vl) :: l -> hash (i + Hashtbl.hash (vr, float_of_num vl)) l + | (vr, vl) :: l -> hash (i + Hashtbl.hash (vr, Q.to_float vl)) l in Hashtbl.hash (hash 0 v) let null = [] -let is_null v = match v with [] | [(0, Int 0)] -> true | _ -> false + +let is_null v = + match v with [] -> true | [(0, x)] when Q.zero =/ x -> true | _ -> false let pp_var_num pp_var o (v, n) = if Int.equal v 0 then - if eq_num (Int 0) n then () else Printf.fprintf o "%s" (string_of_num n) - else - match n with - | Int 1 -> pp_var o v - | Int -1 -> Printf.fprintf o "-%a" pp_var v - | Int 0 -> () - | _ -> Printf.fprintf o "%s*%a" (string_of_num n) pp_var v + if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n) + else if Q.one =/ n then pp_var o v + else if Q.neg_one =/ n then Printf.fprintf o "-%a" pp_var v + else if Q.zero =/ n then () + else Printf.fprintf o "%s*%a" (Q.to_string n) pp_var v let pp_var_num_smt pp_var o (v, n) = if Int.equal v 0 then - if eq_num (Int 0) n then () else Printf.fprintf o "%s" (string_of_num n) - else - match n with - | Int 1 -> pp_var o v - | Int -1 -> Printf.fprintf o "(- %a)" pp_var v - | Int 0 -> () - | _ -> Printf.fprintf o "(* %s %a)" (string_of_num n) pp_var v + if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n) + else if Q.one =/ n then pp_var o v + else if Q.neg_one =/ n then Printf.fprintf o "(- %a)" pp_var v + else if Q.zero =/ n then () + else Printf.fprintf o "(* %s %a)" (Q.to_string n) pp_var v let rec pp_gen pp_var o v = match v with @@ -75,36 +74,34 @@ let pp_smt o v = in Printf.fprintf o "(+ %a)" list v -let from_list (l : num list) = +let from_list (l : Q.t list) = let rec xfrom_list i l = match l with | [] -> [] | e :: l -> - if e <>/ Int 0 then (i, e) :: xfrom_list (i + 1) l + if e <>/ Q.zero then (i, e) :: xfrom_list (i + 1) l else xfrom_list (i + 1) l in xfrom_list 0 l -let zero_num = Int 0 - let to_list m = let rec xto_list i l = match l with | [] -> [] | (x, v) :: l' -> - if i = x then v :: xto_list (i + 1) l' else zero_num :: xto_list (i + 1) l + if i = x then v :: xto_list (i + 1) l' else Q.zero :: xto_list (i + 1) l in xto_list 0 m -let cons i v rst = if v =/ Int 0 then rst else (i, v) :: rst +let cons i v rst = if v =/ Q.zero then rst else (i, v) :: rst let rec update i f t = match t with - | [] -> cons i (f zero_num) [] + | [] -> cons i (f Q.zero) [] | (k, v) :: l -> ( match Int.compare i k with | 0 -> cons k (f v) l - | -1 -> cons i (f zero_num) t + | -1 -> cons i (f Q.zero) t | 1 -> (k, v) :: update i f l | _ -> failwith "compare_num" ) @@ -118,18 +115,17 @@ let rec set i n t = | 1 -> (k, v) :: set i n l | _ -> failwith "compare_num" ) -let cst n = if n =/ Int 0 then [] else [(0, n)] +let cst n = if n =/ Q.zero then [] else [(0, n)] let mul z t = - match z with - | Int 0 -> [] - | Int 1 -> t - | _ -> List.map (fun (i, n) -> (i, mult_num z n)) t + if z =/ Q.zero then [] + else if z =/ Q.one then t + else List.map (fun (i, n) -> (i, z */ n)) t let div z t = - if z <>/ Int 1 then List.map (fun (x, nx) -> (x, nx // z)) t else t + if z <>/ Q.one then List.map (fun (x, nx) -> (x, nx // z)) t else t -let uminus t = List.map (fun (i, n) -> (i, minus_num n)) t +let uminus t = List.map (fun (i, n) -> (i, Q.neg n)) t let rec add (ve1 : t) (ve2 : t) = match (ve1, ve2) with @@ -137,12 +133,12 @@ let rec add (ve1 : t) (ve2 : t) = | (v1, c1) :: l1, (v2, c2) :: l2 -> let cmp = Int.compare v1 v2 in if cmp == 0 then - let s = add_num c1 c2 in - if eq_num (Int 0) s then add l1 l2 else (v1, s) :: add l1 l2 + let s = c1 +/ c2 in + if Q.zero =/ s then add l1 l2 else (v1, s) :: add l1 l2 else if cmp < 0 then (v1, c1) :: add l1 ve2 else (v2, c2) :: add l2 ve1 -let rec xmul_add (n1 : num) (ve1 : t) (n2 : num) (ve2 : t) = +let rec xmul_add (n1 : Q.t) (ve1 : t) (n2 : Q.t) (ve2 : t) = match (ve1, ve2) with | [], _ -> mul n2 ve2 | _, [] -> mul n1 ve1 @@ -150,19 +146,19 @@ let rec xmul_add (n1 : num) (ve1 : t) (n2 : num) (ve2 : t) = let cmp = Int.compare v1 v2 in if cmp == 0 then let s = (n1 */ c1) +/ (n2 */ c2) in - if eq_num (Int 0) s then xmul_add n1 l1 n2 l2 + if Q.zero =/ s then xmul_add n1 l1 n2 l2 else (v1, s) :: xmul_add n1 l1 n2 l2 else if cmp < 0 then (v1, n1 */ c1) :: xmul_add n1 l1 n2 ve2 else (v2, n2 */ c2) :: xmul_add n1 ve1 n2 l2 let mul_add n1 ve1 n2 ve2 = - if n1 =/ Int 1 && n2 =/ Int 1 then add ve1 ve2 else xmul_add n1 ve1 n2 ve2 + if n1 =/ Q.one && n2 =/ Q.one then add ve1 ve2 else xmul_add n1 ve1 n2 ve2 let compare : t -> t -> int = Mutils.Cmp.compare_list (fun x y -> Mutils.Cmp.compare_lexical [ (fun () -> Int.compare (fst x) (fst y)) - ; (fun () -> compare_num (snd x) (snd y)) ]) + ; (fun () -> Q.compare (snd x) (snd y)) ]) (** [tail v vect] returns - [None] if [v] is not a variable of the vector [vect] @@ -181,28 +177,28 @@ let rec tail (v : var) (vect : t) = (* Hopeless *) -let get v vect = match tail v vect with None -> Int 0 | Some (vl, _) -> vl +let get v vect = match tail v vect with None -> Q.zero | Some (vl, _) -> vl let is_constant v = match v with [] | [(0, _)] -> true | _ -> false -let get_cst vect = match vect with (0, v) :: _ -> v | _ -> Int 0 +let get_cst vect = match vect with (0, v) :: _ -> v | _ -> Q.zero let choose v = match v with [] -> None | (vr, vl) :: rst -> Some (vr, vl, rst) let rec fresh v = match v with [] -> 1 | [(v, _)] -> v + 1 | _ :: v -> fresh v let variables v = List.fold_left (fun acc (x, _) -> ISet.add x acc) ISet.empty v -let decomp_cst v = match v with (0, vl) :: v -> (vl, v) | _ -> (Int 0, v) +let decomp_cst v = match v with (0, vl) :: v -> (vl, v) | _ -> (Q.zero, v) let rec decomp_at i v = match v with - | [] -> (Int 0, null) + | [] -> (Q.zero, null) | (vr, vl) :: r -> - if i = vr then (vl, r) else if i < vr then (Int 0, v) else decomp_at i r + if i = vr then (vl, r) else if i < vr then (Q.zero, v) else decomp_at i r -let decomp_fst v = match v with [] -> ((0, Int 0), []) | x :: v -> (x, v) +let decomp_fst v = match v with [] -> ((0, Q.zero), []) | x :: v -> (x, v) let rec subst (vr : int) (e : t) (v : t) = match v with | [] -> [] | (x, n) :: v' -> ( match Int.compare vr x with - | 0 -> mul_add n e (Int 1) v' + | 0 -> mul_add n e Q.one v' | -1 -> v | 1 -> add [(x, n)] (subst vr e v') | _ -> assert false ) @@ -227,25 +223,23 @@ let for_all p l = List.for_all (fun (v, n) -> p v n) l let decr_var i v = List.map (fun (v, n) -> (v - i, n)) v let incr_var i v = List.map (fun (v, n) -> (v + i, n)) v -open Big_int - let gcd v = let res = fold (fun c _ n -> - assert (Int.equal (compare_big_int (denominator n) unit_big_int) 0); - gcd_big_int c (numerator n)) - zero_big_int v + assert (Int.equal (Z.compare (Q.den n) Z.one) 0); + Z.gcd c (Q.num n)) + Z.zero v in - if Int.equal (compare_big_int res zero_big_int) 0 then unit_big_int else res + if Int.equal (Z.compare res Z.zero) 0 then Z.one else res let normalise v = - let ppcm = fold (fun c _ n -> ppcm c (denominator n)) unit_big_int v in + let ppcm = fold (fun c _ n -> Z.ppcm c (Q.den n)) Z.one v in let gcd = - let gcd = fold (fun c _ n -> gcd_big_int c (numerator n)) zero_big_int v in - if Int.equal (compare_big_int gcd zero_big_int) 0 then unit_big_int else gcd + let gcd = fold (fun c _ n -> Z.gcd c (Q.num n)) Z.zero v in + if Int.equal (Z.compare gcd Z.zero) 0 then Z.one else gcd in - List.map (fun (x, v) -> (x, v */ Big_int ppcm // Big_int gcd)) v + List.map (fun (x, v) -> (x, v */ Q.of_bigint ppcm // Q.of_bigint gcd)) v let rec exists2 p vect1 vect2 = match (vect1, vect2) with @@ -265,7 +259,7 @@ let dotproduct v1 v2 = else if x1 < x2 then dot acc v1' v2 else dot acc v1 v2' in - dot (Int 0) v1 v2 + dot Q.zero v1 v2 let map f v = List.map (fun (x, v) -> f x v) v @@ -276,18 +270,18 @@ let abs_min_elt v = Some (List.fold_left (fun (v1, vl1) (v2, vl2) -> - if abs_num vl1 </ abs_num vl2 then (v1, vl1) else (v2, vl2)) + if Q.abs vl1 </ Q.abs vl2 then (v1, vl1) else (v2, vl2)) (v, vl) r) let partition p = List.partition (fun (vr, vl) -> p vr vl) -let mkvar x = set x (Int 1) null +let mkvar x = set x Q.one null module Bound = struct - type t = {cst : num; var : var; coeff : num} + type t = {cst : Q.t; var : var; coeff : Q.t} let of_vect (v : vector) = match v with - | [(x, v)] -> if x = 0 then None else Some {cst = Int 0; var = x; coeff = v} + | [(x, v)] -> if x = 0 then None else Some {cst = Q.zero; var = x; coeff = v} | [(0, v); (x, v')] -> Some {cst = v; var = x; coeff = v'} | _ -> None end diff --git a/plugins/micromega/vect.mli b/plugins/micromega/vect.mli index 4b814cbb82..56c8ce87dd 100644 --- a/plugins/micromega/vect.mli +++ b/plugins/micromega/vect.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Num +open NumCompat open Mutils type var = int @@ -50,18 +50,18 @@ val pp_smt : out_channel -> t -> unit val variables : t -> ISet.t (** [variables v] returns the set of variables with non-zero coefficients *) -val get_cst : t -> num +val get_cst : t -> Q.t (** [get_cst v] returns c i.e. the coefficient of the variable zero *) -val decomp_cst : t -> num * t +val decomp_cst : t -> Q.t * t (** [decomp_cst v] returns the pair (c,a1.x1+...+an.xn) *) -val decomp_at : int -> t -> num * t +val decomp_at : int -> t -> Q.t * t (** [decomp_cst v] returns the pair (ai, ai+1.xi+...+an.xn) *) -val decomp_fst : t -> (var * num) * t +val decomp_fst : t -> (var * Q.t) * t -val cst : num -> t +val cst : Q.t -> t (** [cst c] returns the vector v=c+0.x1+...+0.xn *) val is_constant : t -> bool @@ -74,33 +74,33 @@ val null : t val is_null : t -> bool (** [is_null v] returns whether [v] is the [null] vector i.e [equal v null] *) -val get : var -> t -> num +val get : var -> t -> Q.t (** [get xi v] returns the coefficient ai of the variable [xi]. [get] is also defined for the variable 0 *) -val set : var -> num -> t -> t +val set : var -> Q.t -> t -> t (** [set xi ai' v] returns the vector c+a1.x1+...ai'.xi+...+an.xn i.e. the coefficient of the variable xi is set to ai' *) val mkvar : var -> t (** [mkvar xi] returns 1.xi *) -val update : var -> (num -> num) -> t -> t +val update : var -> (Q.t -> Q.t) -> t -> t (** [update xi f v] returns c+a1.x1+...+f(ai).xi+...+an.xn *) val fresh : t -> int (** [fresh v] return the fresh variable with index 1+ max (variables v) *) -val choose : t -> (var * num * t) option +val choose : t -> (var * Q.t * t) option (** [choose v] decomposes a vector [v] depending on whether it is [null] or not. @return None if v is [null] @return Some(x,n,r) where v = r + n.x x is the smallest variable with non-zero coefficient n <> 0. *) -val from_list : num list -> t +val from_list : Q.t list -> t (** [from_list l] returns the vector c+a1.x1...an.xn from the list of coefficient [l=c;a1;...;an] *) -val to_list : t -> num list +val to_list : t -> Q.t list (** [to_list v] returns the list of all coefficient of the vector v i.e. [c;a1;...;an] The list representation is (obviously) not sparsed and therefore certain ai may be 0 *) @@ -114,7 +114,7 @@ val incr_var : int -> t -> t (** [incr_var i v] increments the variables of the vector [v] by the amount [i]. *) -val gcd : t -> Big_int.big_int +val gcd : t -> Z.t (** [gcd v] returns gcd(num(c),num(a1),...,num(an)) where num extracts the numerator of a rational value. *) @@ -130,17 +130,17 @@ val add : t -> t -> t @return c1+c1'+ (a1+a1').x1 + ... + (an+an').xn *) -val mul : num -> t -> t +val mul : Q.t -> t -> t (** [mul a v] is vector multiplication of vector [v] by a scalar [a]. @return a.v = a.c+a.a1.x1+...+a.an.xn *) -val mul_add : num -> t -> num -> t -> t +val mul_add : Q.t -> t -> Q.t -> t -> t (** [mul_add c1 v1 c2 v2] returns the linear combination c1.v1+c2.v2 *) val subst : int -> t -> t -> t (** [subst x v v'] replaces x by v in vector v' *) -val div : num -> t -> t +val div : Q.t -> t -> t (** [div c1 v1] returns the mutiplication by the inverse of c1 i.e (1/c1).v1 *) val uminus : t -> t @@ -148,36 +148,36 @@ val uminus : t -> t (** {1 Iterators} *) -val fold : ('acc -> var -> num -> 'acc) -> 'acc -> t -> 'acc +val fold : ('acc -> var -> Q.t -> 'acc) -> 'acc -> t -> 'acc (** [fold f acc v] returns f (f (f acc 0 c ) x1 a1 ) ... xn an *) -val fold_error : ('acc -> var -> num -> 'acc option) -> 'acc -> t -> 'acc option +val fold_error : ('acc -> var -> Q.t -> 'acc option) -> 'acc -> t -> 'acc option (** [fold_error f acc v] is the same as [fold (fun acc x i -> match acc with None -> None | Some acc' -> f acc' x i) (Some acc) v] but with early exit... *) -val find : (var -> num -> 'c option) -> t -> 'c option +val find : (var -> Q.t -> 'c option) -> t -> 'c option (** [find f v] returns the first [f xi ai] such that [f xi ai <> None]. If no such xi ai exists, it returns None *) -val for_all : (var -> num -> bool) -> t -> bool +val for_all : (var -> Q.t -> bool) -> t -> bool (** [for_all p v] returns /\_{i>=0} (f xi ai) *) -val exists2 : (num -> num -> bool) -> t -> t -> (var * num * num) option +val exists2 : (Q.t -> Q.t -> bool) -> t -> t -> (var * Q.t * Q.t) option (** [exists2 p v v'] returns Some(xi,ai,ai') if p(xi,ai,ai') holds and ai,ai' <> 0. It returns None if no such pair of coefficient exists. *) -val dotproduct : t -> t -> num +val dotproduct : t -> t -> Q.t (** [dotproduct v1 v2] is the dot product of v1 and v2. *) -val map : (var -> num -> 'a) -> t -> 'a list -val abs_min_elt : t -> (var * num) option -val partition : (var -> num -> bool) -> t -> t * t +val map : (var -> Q.t -> 'a) -> t -> 'a list +val abs_min_elt : t -> (var * Q.t) option +val partition : (var -> Q.t -> bool) -> t -> t * t module Bound : sig - type t = {cst : num; var : var; coeff : num} + type t = {cst : Q.t; var : var; coeff : Q.t} (** represents a0 + ai.xi *) val of_vect : vector -> t option diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index b3b627be14..dd8ea2c5ba 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -147,7 +147,7 @@ type classify_op = | OpConv (* e.g. Pos.ge == \x.y. Z.ge (Z.pos x) (Z.pos y) \x.y. Z.pos (Pos.add x y) == \x.y. Z.add (Z.pos x) (Z.pos y) Z.succ == (\x.x + 1) - *) + *) | OpOther (*let pp_classify_op = function @@ -1043,8 +1043,8 @@ let rec trans_expr env evd e = app_binop evd e binop a.(n - 2) prf1 a.(n - 1) prf2 | d -> mkvar evd inj e with Not_found -> - (* Feedback.msg_debug - Pp.(str "Not found " ++ Termops.Internal.debug_print_constr e); *) + (* Feedback.msg_debug + Pp.(str "Not found " ++ Termops.Internal.debug_print_constr e); *) mkvar evd inj e let trans_expr env evd e = diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index f6fbdaa958..fa824a88ee 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -134,7 +134,7 @@ let r_of_rawnum ?loc (sign,n) = | '+' -> Bigint.of_string (String.sub e 2 (String.length e - 2)) | '-' -> Bigint.(neg (of_string (String.sub e 2 (String.length e - 2)))) | _ -> Bigint.of_string (String.sub e 1 (String.length e - 1)) in - Bigint.(sub e (of_int (String.length f))) in + Bigint.(sub e (of_int (String.length (String.concat "" (String.split_on_char '_' f))))) in if Bigint.is_strictly_pos e then rmult n (izr (pow10 e)) else if Bigint.is_strictly_neg e then rdiv n (izr (pow10 (neg e))) else n (* e = 0 *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index aafd662f7d..c9ccd668ca 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -78,9 +78,9 @@ let get_polymorphic_positions env sigma f = match EConstr.kind sigma f with | Ind (ind, u) | Construct ((ind, _), u) -> let mib,oib = Inductive.lookup_mind_specif env ind in - (match oib.mind_arity with - | RegularArity _ -> assert false - | TemplateArity templ -> templ.template_param_levels) + (match mib.mind_template with + | None -> assert false + | Some templ -> templ.template_param_levels) | _ -> assert false let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index a4406aeba1..01994a35c7 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -681,13 +681,17 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = match mip.mind_arity with | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity) | TemplateArity ar -> + let templ = match mib.mind_template with + | None -> assert false + | Some t -> t + in let _,scl = splay_arity env sigma conclty in let scl = EConstr.ESorts.kind sigma scl in let ctx = List.rev mip.mind_arity_ctxt in let evdref = ref sigma in let ctx = instantiate_universes - env evdref scl ar.template_level (ctx,ar.template_param_levels) in + env evdref scl ar.template_level (ctx,templ.template_param_levels) in !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl)) let type_of_projection_constant env (p,u) = diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 4afed07eda..fdf0db9909 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1009,11 +1009,11 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c = let app = (mkApp (hdf, Array.sub al 0 (Array.length al - 1))) in let app' = f acc app in let a' = f acc a in - (match EConstr.kind sigma app' with - | App (hdf', al') when hdf' == hdf -> - (* Still the same projection, we ignore the change in parameters *) - mkProj (p, a') - | _ -> mkApp (app', [| a' |])) + let hdf', _ = decompose_app_vect sigma app' in + if hdf' == hdf then + (* Still the same projection, we ignore the change in parameters *) + mkProj (p, a') + else mkApp (app', [| a' |]) | _ -> map_constr_with_binders_left_to_right sigma g f acc c let e_contextually byhead (occs,c) f = begin fun env sigma t -> diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 7cdfd0637a..a7ba12bb1f 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -120,18 +120,14 @@ let build_constant_by_tactic ~name ?(opaque=Proof_global.Transparent) ctx sign ~ let evd = Evd.from_ctx ctx in let goals = [ (Global.env_of_context sign , typ) ] in let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in - try - let pf, status = by tac pf in - let open Proof_global in - let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in - match entries with - | [entry] -> - entry, status, universes - | _ -> - CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") - with reraise -> - let reraise = Exninfo.capture reraise in - Exninfo.iraise reraise + let pf, status = by tac pf in + let open Proof_global in + let { entries; universes } = close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pf in + match entries with + | [entry] -> + entry, status, universes + | _ -> + CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term") let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac = let name = Id.of_string ("temporary_proof"^string_of_int (next())) in diff --git a/test-suite/bugs/closed/bug_11730.v b/test-suite/bugs/closed/bug_11730.v new file mode 100644 index 0000000000..f788636f9c --- /dev/null +++ b/test-suite/bugs/closed/bug_11730.v @@ -0,0 +1,6 @@ +Set Mangle Names. + +Infix "&&&" := andb (at level 40, left associativity). +(* Error: Variable _0 occurs more than once. *) + +Check (_ &&& _). diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v index 25285622a9..bad9d64f65 100644 --- a/test-suite/bugs/closed/bug_9512.v +++ b/test-suite/bugs/closed/bug_9512.v @@ -4,9 +4,10 @@ Set Primitive Projections. Record params := { width : Z }. Definition p : params := Build_params 64. +Definition width' := width. Set Printing All. -Goal width p = 0%Z -> width p = 0%Z. +Lemma foo : width p = 0%Z -> width p = 0%Z. intros. assert_succeeds (enough True; [omega|]). @@ -16,7 +17,9 @@ Goal width p = 0%Z -> width p = 0%Z. (* ============================ *) (* @eq Z (width p) Z0 *) - change tt with tt in H. + change (width' p = 0%Z) in H;cbv [width'] in H. + (* check that we correctly got the compat constant in H *) + Fail match goal with H : ?l = _ |- ?l' = _ => constr_eq l l' end. (* H : @eq Z (width p) Z0 *) (* ============================ *) diff --git a/test-suite/bugs/closed/bug_9930.v b/test-suite/bugs/closed/bug_9930.v new file mode 100644 index 0000000000..042cd69fbe --- /dev/null +++ b/test-suite/bugs/closed/bug_9930.v @@ -0,0 +1,14 @@ +Set Primitive Projections. +Record params := { width : nat }. +Definition p : params := Build_params 64. + +Lemma foo : width p = 0 -> width p = 0. + intros. + let e := lazymatch type of H with ?e = 0 => e end in + change tt with tt in H; + let E := lazymatch type of H with ?E = 0 => E end in + idtac "before:" e; idtac "after :" E; + (* before: (width p) *) + (* after : (width p) *) + tryif constr_eq e E then exact H else idtac. +Qed. diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index 2d877bd813..2b14ca7069 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -2,6 +2,8 @@ : R (-31)%R : R +15e-1%R + : R eq_refl : 102e-2 = 102e-2 : 102e-2 = 102e-2 eq_refl : 102e-1 = 102e-1 diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v index cb3bce70d4..7be8b18ac8 100644 --- a/test-suite/output/RealSyntax.v +++ b/test-suite/output/RealSyntax.v @@ -2,6 +2,8 @@ Require Import Reals.Rdefinitions. Check 32%R. Check (-31)%R. +Check 1.5_%R. + Open Scope R_scope. Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)). diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 918b0efc5a..8904f3f936 100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -41,11 +41,15 @@ Proof. apply Nat.lt_succ_r. Qed. +Register lt_n_Sm_le as num.nat.lt_n_Sm_le. + Theorem le_lt_n_Sm n m : n <= m -> n < S m. Proof. apply Nat.lt_succ_r. Qed. +Register le_lt_n_Sm as num.nat.le_lt_n_Sm. + Hint Immediate lt_le_S: arith. Hint Immediate lt_n_Sm_le: arith. Hint Immediate le_lt_n_Sm: arith. @@ -99,6 +103,8 @@ Proof. apply Nat.succ_lt_mono. Qed. +Register lt_S_n as num.nat.lt_S_n. + Hint Resolve lt_n_Sn lt_S lt_n_S : arith. Hint Immediate lt_S_n : arith. @@ -133,6 +139,8 @@ Notation lt_trans := Nat.lt_trans (only parsing). Notation lt_le_trans := Nat.lt_le_trans (only parsing). Notation le_lt_trans := Nat.le_lt_trans (only parsing). +Register le_lt_trans as num.nat.le_lt_trans. + Hint Resolve lt_trans lt_le_trans le_lt_trans: arith. (** * Large = strict or equal *) diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index f12785029a..4657b7f46d 100644 --- a/theories/Arith/PeanoNat.v +++ b/theories/Arith/PeanoNat.v @@ -764,6 +764,9 @@ Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope. Hint Unfold Nat.le : core. Hint Unfold Nat.lt : core. +Register Nat.le_trans as num.nat.le_trans. +Register Nat.nlt_0_r as num.nat.nlt_0_r. + (** [Nat] contains an [order] tactic for natural numbers *) (** Note that [Nat.order] is domain-agnostic: it will not prove diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 1c183930f9..c5a6651c05 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -34,6 +34,8 @@ Proof. intros a. apply (H (S (f a))). auto with arith. Defined. +Register well_founded_ltof as num.nat.well_founded_ltof. + Theorem well_founded_gtof : well_founded gtof. Proof. exact well_founded_ltof. diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 149a7a0cc5..beb06ea912 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -159,6 +159,8 @@ Inductive le (n:nat) : nat -> Prop := where "n <= m" := (le n m) : nat_scope. +Register le_n as num.nat.le_n. + Hint Constructors le: core. (*i equivalent to : "Hints Resolve le_n le_S : core." i*) diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 998bbc7047..bd5185fdb0 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -32,11 +32,14 @@ Section Well_founded. Inductive Acc (x: A) : Prop := Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x. + Register Acc as core.wf.acc. + Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y. destruct 1; trivial. Defined. Global Arguments Acc_inv [x] _ [y] _, [x] _ y _. + Register Acc_inv as core.wf.acc_inv. (** A relation is well-founded if every element is accessible *) diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index edb03a5c89..718e62b9b7 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -329,10 +329,7 @@ let template_polymorphism_candidate ~ctor_levels uctx params concl = if not concltemplate then false else let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in - let params, conclunivs = - IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu - in - not (Univ.LSet.is_empty conclunivs) + Option.has_some @@ IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu | Entries.Polymorphic_entry _ -> false let check_param = function @@ -370,6 +367,14 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames (* Build the inductive entries *) let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) -> + { mind_entry_typename = indname; + mind_entry_arity = arity; + mind_entry_consnames = cnames; + mind_entry_lc = ctypes + }) + indnames arities arityconcl constructors + in + let template = List.map4 (fun indname (templatearity, _) concl (_, ctypes) -> let template_candidate () = templatearity || let ctor_levels = @@ -385,22 +390,17 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames in template_polymorphism_candidate ~ctor_levels uctx ctx_params concl in - let template = match template with + match template with | Some template -> if poly && template then user_err Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible."); template | None -> should_auto_template indname (template_candidate ()) - in - { mind_entry_typename = indname; - mind_entry_arity = arity; - mind_entry_template = template; - mind_entry_consnames = cnames; - mind_entry_lc = ctypes - }) + ) indnames arities arityconcl constructors in + let is_template = List.for_all (fun t -> t) template in (* Build the mutual inductive entry *) let mind_ent = { mind_entry_params = ctx_params; @@ -409,6 +409,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames mind_entry_inds = entries; mind_entry_private = if private_ind then Some false else None; mind_entry_universes = uctx; + mind_entry_template = is_template; mind_entry_cumulative = poly && cumulative; } in diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 33fd14a731..10946d78f0 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1708,7 +1708,7 @@ let add_infix ~local deprecation env ({CAst.loc;v=inf},modifiers) pr sc = (* check the precedence *) let vars = names_of_constr_expr pr in let x = Namegen.next_ident_away (Id.of_string "x") vars in - let y = Namegen.next_ident_away (Id.of_string "y") vars in + let y = Namegen.next_ident_away (Id.of_string "y") (Id.Set.add x vars) in let metas = [inject_var x; inject_var y] in let c = mkAppC (pr,metas) in let df = CAst.make ?loc @@ Id.to_string x ^" "^(quote_notation_token inf)^" "^Id.to_string y in diff --git a/vernac/record.ml b/vernac/record.ml index 3e44cd85cc..065641989d 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -423,7 +423,13 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa let args = Context.Rel.to_extended_list mkRel nfields params in let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in - let template = + { mind_entry_typename = id; + mind_entry_arity = arity; + mind_entry_consnames = [idbuild]; + mind_entry_lc = [type_constructor] } + in + let blocks = List.mapi mk_block record_data in + let check_template (id, _, min_univ, _, _, fields, _, _) = let template_candidate () = (* we use some dummy values for the arities in the rel_context as univs_of_constr doesn't care about localassums and @@ -454,14 +460,8 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa | None, template -> (* auto detect template *) ComInductive.should_auto_template id (template && template_candidate ()) - in - { mind_entry_typename = id; - mind_entry_arity = arity; - mind_entry_template = template; - mind_entry_consnames = [idbuild]; - mind_entry_lc = [type_constructor] } in - let blocks = List.mapi mk_block record_data in + let template = List.for_all check_template record_data in let primitive = !primitive_flag && List.for_all (fun (_,_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data @@ -473,6 +473,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa mind_entry_inds = blocks; mind_entry_private = None; mind_entry_universes = univs; + mind_entry_template = template; mind_entry_cumulative = poly && cumulative; } in diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index e0afb7f483..5d38ea32be 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -92,28 +92,18 @@ let warn_deprecated_command = (* Interpretation of a vernac command *) let type_vernac opn converted_args ~atts = - let phase = ref "Looking up command" in - try - let depr, callback = vinterp_map opn in - let () = if depr then + let depr, callback = vinterp_map opn in + let () = if depr then let rules = Egramml.get_extend_vernac_rule opn in let pr_gram = function - | Egramml.GramTerminal s -> str s - | Egramml.GramNonTerminal _ -> str "_" + | Egramml.GramTerminal s -> str s + | Egramml.GramNonTerminal _ -> str "_" in let pr = pr_sequence pr_gram rules in warn_deprecated_command pr; - in - phase := "Checking arguments"; - let hunk = callback converted_args in - phase := "Executing command"; - hunk ~atts - with - | reraise -> - let reraise = Exninfo.capture reraise in - if !Flags.debug then - Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); - Exninfo.iraise reraise + in + let hunk = callback converted_args in + hunk ~atts (** VERNAC EXTEND registering *) diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 59557a60a6..280343f315 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -18,12 +18,9 @@ module Parser = struct let parse ps entry pa = Pcoq.unfreeze ps; - Flags.with_option Flags.we_are_parsing (fun () -> - try Pcoq.Entry.parse entry pa - with e when CErrors.noncritical e -> - let (e, info) = Exninfo.capture e in - Exninfo.iraise (e, info)) - () + Flags.with_option Flags.we_are_parsing + (fun () -> Pcoq.Entry.parse entry pa) + () end |