diff options
48 files changed, 360 insertions, 891 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 51d39936d0..cc8a4d34c9 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -19,7 +19,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2020-08-18-V29" + CACHEKEY: "bionic_coq-V2020-08-28-V92" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -600,7 +600,7 @@ test-suite:edge:dune:dev: - opam repo add ocaml-beta https://github.com/ocaml/ocaml-beta-repository.git - opam update - opam install ocaml-variants=$OCAMLVER - - opam install dune num + - opam install dune num zarith - eval $(opam env) - export COQ_UNIT_TEST=noop - make -f Makefile.dune test-suite diff --git a/INSTALL.md b/INSTALL.md index c44c3dde7d..2b5986ded4 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -12,6 +12,8 @@ To compile Coq yourself, you need: - The [num](https://github.com/ocaml/num) library; note that it is included in the OCaml distribution for OCaml versions < 4.06.0 +- The [ZArith library](https://github.com/ocaml/Zarith) >= 1.8 + - The [findlib](http://projects.camlcity.org/projects/findlib.html) library (version >= 1.8.0) - GNU Make (version >= 3.81) diff --git a/META.coq.in b/META.coq.in index 883a7286e4..5aaa8cc8a6 100644 --- a/META.coq.in +++ b/META.coq.in @@ -120,7 +120,7 @@ package "interp" ( description = "Coq Term Interpretation" version = "8.13" - requires = "coq.pretyping" + requires = "zarith, coq.pretyping" directory = "interp" archive(byte) = "interp.cma" @@ -327,7 +327,7 @@ package "plugins" ( description = "Coq micromega plugin" version = "8.13" - requires = "num,coq.plugins.ltac" + requires = "num, coq.plugins.ltac" directory = "micromega" archive(byte) = "micromega_plugin.cmo" @@ -462,7 +462,7 @@ package "plugins" ( description = "Coq nsatz plugin" version = "8.13" - requires = "num,coq.plugins.ltac" + requires = "zarith, coq.plugins.ltac" directory = "nsatz" archive(byte) = "nsatz_plugin.cmo" diff --git a/Makefile.build b/Makefile.build index 4fb4b12be2..061489f47f 100644 --- a/Makefile.build +++ b/Makefile.build @@ -245,7 +245,7 @@ COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS) BOOTCOQC=$(TIMER) $(COQC) -coqlib . -q $(COQOPTS) LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS)) -MLINCLUDES=$(LOCALINCLUDES) +MLINCLUDES=$(LOCALINCLUDES) -package zarith USERCONTRIBINCLUDES=$(addprefix -I user-contrib/,$(USERCONTRIBDIRS)) @@ -302,7 +302,7 @@ $(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ -linkpkg $(1) $^ endef # Main packages linked by Coq. -SYSMOD:=-package num,str,unix,dynlink,threads +SYSMOD:=-package str,unix,dynlink,threads,num,zarith ########################################################################### # Infrastructure for the rest of the Makefile @@ -709,10 +709,6 @@ plugins/micromega/%.cmi: plugins/micromega/%.mli $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< -plugins/nsatz/%.cmi: plugins/nsatz/%.mli - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< - %.cmi: %.mli $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< @@ -721,10 +717,6 @@ plugins/micromega/%.cmo: plugins/micromega/%.ml $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< -plugins/nsatz/%.cmo: plugins/nsatz/%.ml - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -package unix,num -c $< - %.cmo: %.ml $(SHOW)'OCAMLC $<' $(HIDE)$(OCAMLC) $(COND_BYTEFLAGS) -c $< @@ -762,10 +754,6 @@ plugins/micromega/%.cmx: plugins/micromega/%.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $< -plugins/nsatz/%.cmx: plugins/nsatz/%.ml - $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -package unix,num -c $< - plugins/%.cmx: plugins/%.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) $($(@:.cmx=_FORPACK)) -c $< diff --git a/azure-pipelines.yml b/azure-pipelines.yml index b27d1df39d..5830095861 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -22,7 +22,7 @@ jobs: powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')" SET CYGROOT=C:\cygwin64 SET CYGCACHE=%CYGROOT%\var\cache\setup - setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib -P python3 + setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib,mingw64-x86_64-gmp -P python3 SET TARGET_ARCH=x86_64-w64-mingw32 SET CD_MFMT=%cd:\=/% @@ -64,7 +64,7 @@ jobs: set -e brew update (cd $(brew --repository)/Library/Taps/homebrew/homebrew-core/ && git fetch --shallow-since=${HBCORE_DATE} && git checkout ${HBCORE_REF}) - brew install gnu-time opam pkg-config gtksourceview3 adwaita-icon-theme || true + brew install gnu-time opam pkg-config gtksourceview3 adwaita-icon-theme gmp || true # || true: workaround #12657, see also #12672 and commit message for this line pip3 install macpack displayName: 'Install system dependencies' @@ -80,7 +80,7 @@ jobs: opam switch set ocaml-base-compiler.$COMPILER eval $(opam env) opam update - opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 + opam install -j "$NJOBS" num ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.9.1 opam list displayName: 'Install OCaml dependencies' env: diff --git a/clib/bigint.ml b/clib/bigint.ml deleted file mode 100644 index 735ff3261e..0000000000 --- a/clib/bigint.ml +++ /dev/null @@ -1,526 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(***************************************************) -(* Basic operations on (unbounded) integer numbers *) -(***************************************************) - -(* An integer is canonically represented as an array of k-digits blocs, - i.e. in base 10^k. - - 0 is represented by the empty array and -1 by the singleton [|-1|]. - The first bloc is in the range ]0;base[ for positive numbers. - The first bloc is in the range [-base;-1[ for numbers < -1. - All other blocs are numbers in the range [0;base[. - - Negative numbers are represented using 2's complementation : - one unit is "borrowed" from the top block for complementing - the other blocs. For instance, with 4-digits blocs, - [|-5;6789|] denotes -43211 - since -5.10^4+6789=-((4.10^4)+(10000-6789)) = -43211 - - The base is a power of 10 in order to facilitate the parsing and printing - of numbers in digital notation. - - All functions, to the exception of to_string and of_string should work - with an arbitrary base, even if not a power of 10. - - In practice, we set k=4 on 32-bits machines, so that no overflow in ocaml - machine words (i.e. the interval [-2^30;2^30-1]) occur when multiplying two - numbers less than (10^k). On 64-bits machines, k=9. -*) - -(* The main parameters *) - -let size = - let rec log10 n = if n < 10 then 0 else 1 + log10 (n / 10) in - (log10 max_int) / 2 - -let format_size = - (* How to parametrize a printf format *) - if Int.equal size 4 then Printf.sprintf "%04d" - else if Int.equal size 9 then Printf.sprintf "%09d" - else fun n -> - let rec aux j l n = - if Int.equal j size then l else aux (j+1) (string_of_int (n mod 10) :: l) (n/10) - in String.concat "" (aux 0 [] n) - -(* The base is 10^size *) -let base = - let rec exp10 = function 0 -> 1 | n -> 10 * exp10 (n-1) in exp10 size - -(******************************************************************) -(* First, we represent all numbers by int arrays. - Later, we will optimize the particular case of small integers *) -(******************************************************************) - -module ArrayInt = struct - -(* Basic numbers *) -let zero = [||] - -let is_zero = function -| [||] -> true -| _ -> false - -(* An array is canonical when - - it is empty - - it is [|-1|] - - its first bloc is in [-base;-1[U]0;base[ - and the other blocs are in [0;base[. *) -(* -let canonical n = - let ok x = (0 <= x && x < base) in - let rec ok_tail k = (Int.equal k 0) || (ok n.(k) && ok_tail (k-1)) in - let ok_init x = (-base <= x && x < base && not (Int.equal x (-1)) && not (Int.equal x 0)) - in - (is_zero n) || (match n with [|-1|] -> true | _ -> false) || - (ok_init n.(0) && ok_tail (Array.length n - 1)) -*) - -(* [normalize_pos] : removing initial blocks of 0 *) - -let normalize_pos n = - let k = ref 0 in - while !k < Array.length n && Int.equal n.(!k) 0 do incr k done; - Array.sub n !k (Array.length n - !k) - -(* [normalize_neg] : avoid (-1) as first bloc. - input: an array with -1 as first bloc and other blocs in [0;base[ - output: a canonical array *) - -let normalize_neg n = - let k = ref 1 in - while !k < Array.length n && Int.equal n.(!k) (base - 1) do incr k done; - let n' = Array.sub n !k (Array.length n - !k) in - if Int.equal (Array.length n') 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n') - -(* [normalize] : avoid 0 and (-1) as first bloc. - input: an array with first bloc in [-base;base[ and others in [0;base[ - output: a canonical array *) - -let normalize n = - if Int.equal (Array.length n) 0 then n - else if Int.equal n.(0) (-1) then normalize_neg n - else if Int.equal n.(0) 0 then normalize_pos n - else n - -(* Opposite (expects and returns canonical arrays) *) - -let neg m = - if is_zero m then zero else - let n = Array.copy m in - let i = ref (Array.length m - 1) in - while !i > 0 && Int.equal n.(!i) 0 do decr i done; - if Int.equal !i 0 then begin - n.(0) <- - n.(0); - (* n.(0) cannot be 0 since m is canonical *) - if Int.equal n.(0) (-1) then normalize_neg n - else if Int.equal n.(0) base then (n.(0) <- 0; Array.append [| 1 |] n) - else n - end else begin - (* here n.(!i) <> 0, hence 0 < base - n.(!i) < base for n canonical *) - n.(!i) <- base - n.(!i); decr i; - while !i > 0 do n.(!i) <- base - 1 - n.(!i); decr i done; - (* since -base <= n.(0) <= base-1, hence -base <= -n.(0)-1 <= base-1 *) - n.(0) <- - n.(0) - 1; - (* since m is canonical, m.(0)<>0 hence n.(0)<>-1, - and m=-1 is already handled above, so here m.(0)<>-1 hence n.(0)<>0 *) - n - end - -let push_carry r j = - let j = ref j in - while !j > 0 && r.(!j) < 0 do - r.(!j) <- r.(!j) + base; decr j; r.(!j) <- r.(!j) - 1 - done; - while !j > 0 && r.(!j) >= base do - r.(!j) <- r.(!j) - base; decr j; r.(!j) <- r.(!j) + 1 - done; - (* here r.(0) could be in [-2*base;2*base-1] *) - if r.(0) >= base then (r.(0) <- r.(0) - base; Array.append [| 1 |] r) - else if r.(0) < -base then (r.(0) <- r.(0) + 2*base; Array.append [| -2 |] r) - else normalize r (* in case r.(0) is 0 or -1 *) - -let add_to r a j = - if is_zero a then r else begin - for i = Array.length r - 1 downto j+1 do - r.(i) <- r.(i) + a.(i-j); - if r.(i) >= base then (r.(i) <- r.(i) - base; r.(i-1) <- r.(i-1) + 1) - done; - r.(j) <- r.(j) + a.(0); - push_carry r j - end - -let add n m = - let d = Array.length n - Array.length m in - if d > 0 then add_to (Array.copy n) m d else add_to (Array.copy m) n (-d) - -let sub_to r a j = - if is_zero a then r else begin - for i = Array.length r - 1 downto j+1 do - r.(i) <- r.(i) - a.(i-j); - if r.(i) < 0 then (r.(i) <- r.(i) + base; r.(i-1) <- r.(i-1) - 1) - done; - r.(j) <- r.(j) - a.(0); - push_carry r j - end - -let sub n m = - let d = Array.length n - Array.length m in - if d >= 0 then sub_to (Array.copy n) m d - else let r = neg m in add_to r n (Array.length r - Array.length n) - -let mult m n = - if is_zero m || is_zero n then zero else - let l = Array.length m + Array.length n in - let r = Array.make l 0 in - for i = Array.length m - 1 downto 0 do - for j = Array.length n - 1 downto 0 do - let p = m.(i) * n.(j) + r.(i+j+1) in - let (q,s) = - if p < 0 - then (p + 1) / base - 1, (p + 1) mod base + base - 1 - else p / base, p mod base in - r.(i+j+1) <- s; - if not (Int.equal q 0) then r.(i+j) <- r.(i+j) + q; - done - done; - normalize r - -(* Comparisons *) - -let is_strictly_neg n = not (is_zero n) && n.(0) < 0 -let is_strictly_pos n = not (is_zero n) && n.(0) > 0 -let is_neg_or_zero n = is_zero n || n.(0) < 0 -let is_pos_or_zero n = is_zero n || n.(0) > 0 - -(* Is m without its i first blocs less then n without its j first blocs ? - Invariant : |m|-i = |n|-j *) - -let rec less_than_same_size m n i j = - i < Array.length m && - (m.(i) < n.(j) || (Int.equal m.(i) n.(j) && less_than_same_size m n (i+1) (j+1))) - -let less_than m n = - if is_strictly_neg m then - is_pos_or_zero n || Array.length m > Array.length n - || (Int.equal (Array.length m) (Array.length n) && less_than_same_size m n 0 0) - else - is_strictly_pos n && (Array.length m < Array.length n || - (Int.equal (Array.length m) (Array.length n) && less_than_same_size m n 0 0)) - -(* For this equality test it is critical that n and m are canonical *) - -let rec array_eq len v1 v2 i = - if Int.equal len i then true - else - Int.equal v1.(i) v2.(i) && array_eq len v1 v2 (succ i) - -let equal m n = - let lenm = Array.length m in - let lenn = Array.length n in - (Int.equal lenm lenn) && (array_eq lenm m n 0) - -(* Is m without its k top blocs less than n ? *) - -let less_than_shift_pos k m n = - (Array.length m - k < Array.length n) - || (Int.equal (Array.length m - k) (Array.length n) && less_than_same_size m n k 0) - -let rec can_divide k m d i = - (Int.equal i (Array.length d)) || - (m.(k+i) > d.(i)) || - (Int.equal m.(k+i) d.(i) && can_divide k m d (i+1)) - -(* For two big nums m and d and a small number q, - computes m - d * q * base^(|m|-|d|-k) in-place (in m). - Both m d and q are positive. *) - -let sub_mult m d q k = - if not (Int.equal q 0) then - for i = Array.length d - 1 downto 0 do - let v = d.(i) * q in - m.(k+i) <- m.(k+i) - v mod base; - if m.(k+i) < 0 then (m.(k+i) <- m.(k+i) + base; m.(k+i-1) <- m.(k+i-1) -1); - if v >= base then begin - m.(k+i-1) <- m.(k+i-1) - v / base; - let j = ref (i-1) in - while m.(k + !j) < 0 do (* result is positive, hence !j remains >= 0 *) - m.(k + !j) <- m.(k + !j) + base; decr j; m.(k + !j) <- m.(k + !j) -1 - done - end - done - -(** Euclid division m/d = (q,r), with m = q*d+r and |r|<|q|. - This is the "Trunc" variant (a.k.a "Truncated-Toward-Zero"), - as with ocaml's / (but not as ocaml's Big_int.quomod_big_int). - We have sign r = sign m *) - -let euclid m d = - let isnegm, m = - if is_strictly_neg m then (-1),neg m else 1,Array.copy m in - let isnegd, d = if is_strictly_neg d then (-1),neg d else 1,d in - if is_zero d then raise Division_by_zero; - let q,r = - if less_than m d then (zero,m) else - let ql = Array.length m - Array.length d in - let q = Array.make (ql+1) 0 in - let i = ref 0 in - while not (less_than_shift_pos !i m d) do - if Int.equal m.(!i) 0 then incr i else - if can_divide !i m d 0 then begin - let v = - if Array.length d > 1 && not (Int.equal d.(0) m.(!i)) then - (m.(!i) * base + m.(!i+1)) / (d.(0) * base + d.(1) + 1) - else - m.(!i) / d.(0) in - q.(!i) <- q.(!i) + v; - sub_mult m d v !i - end else begin - let v = (m.(!i) * base + m.(!i+1)) / (d.(0) + 1) in - q.(!i) <- q.(!i) + v / base; - sub_mult m d (v / base) !i; - q.(!i+1) <- q.(!i+1) + v mod base; - if q.(!i+1) >= base then - (q.(!i+1) <- q.(!i+1)-base; q.(!i) <- q.(!i)+1); - sub_mult m d (v mod base) (!i+1) - end - done; - (normalize q, normalize m) in - (if Int.equal (isnegd * isnegm) (-1) then neg q else q), - (if Int.equal isnegm (-1) then neg r else r) - -(* Parsing/printing ordinary 10-based numbers *) - -let of_string s = - let len = String.length s in - let isneg = len > 1 && s.[0] == '-' in - let d = ref (if isneg then 1 else 0) in - while !d < len && s.[!d] == '0' do incr d done; - if Int.equal !d len then zero else - let r = (len - !d) mod size in - let h = String.sub s (!d) r in - let e = match h with "" -> 0 | _ -> 1 in - let l = (len - !d) / size in - let a = Array.make (l + e) 0 in - if Int.equal e 1 then a.(0) <- int_of_string h; - for i = 1 to l do - a.(i+e-1) <- int_of_string (String.sub s ((i-1)*size + !d + r) size) - done; - if isneg then neg a else a - -let to_string_pos sgn n = - if Int.equal (Array.length n) 0 then "0" else - sgn ^ - String.concat "" - (string_of_int n.(0) :: List.map format_size (List.tl (Array.to_list n))) - -let to_string n = - if is_strictly_neg n then to_string_pos "-" (neg n) - else to_string_pos "" n - -end - -(******************************************************************) -(* Optimized operations on (unbounded) integer numbers *) -(* integers smaller than base are represented as machine integers *) -(******************************************************************) - -open ArrayInt - -type bigint = Obj.t - -(* Since base is the largest power of 10 such that base*base <= max_int, - we have max_int < 100*base*base : any int can be represented - by at most three blocs *) - -let small n = (-base <= n) && (n < base) - -let mkarray n = - (* n isn't small, this case is handled separately below *) - let lo = n mod base - and hi = n / base in - let t = if small hi then [|hi;lo|] else [|hi/base;hi mod base;lo|] - in - for i = Array.length t -1 downto 1 do - if t.(i) < 0 then (t.(i) <- t.(i) + base; t.(i-1) <- t.(i-1) -1) - done; - t - -let ints_of_int n = - if Int.equal n 0 then [| |] - else if small n then [| n |] - else mkarray n - -let of_int n = - if small n then Obj.repr n else Obj.repr (mkarray n) - -let of_ints n = - let n = normalize n in (* TODO: using normalize here seems redundant now *) - if is_zero n then Obj.repr 0 else - if Int.equal (Array.length n) 1 then Obj.repr n.(0) else - Obj.repr n - -let coerce_to_int = (Obj.magic : Obj.t -> int) -let coerce_to_ints = (Obj.magic : Obj.t -> int array) - -let to_ints n = - if Obj.is_int n then ints_of_int (coerce_to_int n) - else coerce_to_ints n - -let int_of_ints = - let maxi = mkarray max_int and mini = mkarray min_int in - fun t -> - let l = Array.length t in - if (l > 3) || (Int.equal l 3 && (less_than maxi t || less_than t mini)) - then failwith "Bigint.to_int: too large"; - let sum = ref 0 in - let pow = ref 1 in - for i = l-1 downto 0 do - sum := !sum + t.(i) * !pow; - pow := !pow*base; - done; - !sum - -let to_int n = - if Obj.is_int n then coerce_to_int n - else int_of_ints (coerce_to_ints n) - -let app_pair f (m, n) = - (f m, f n) - -let add m n = - if Obj.is_int m && Obj.is_int n - then of_int (coerce_to_int m + coerce_to_int n) - else of_ints (add (to_ints m) (to_ints n)) - -let sub m n = - if Obj.is_int m && Obj.is_int n - then of_int (coerce_to_int m - coerce_to_int n) - else of_ints (sub (to_ints m) (to_ints n)) - -let mult m n = - if Obj.is_int m && Obj.is_int n - then of_int (coerce_to_int m * coerce_to_int n) - else of_ints (mult (to_ints m) (to_ints n)) - -let euclid m n = - if Obj.is_int m && Obj.is_int n - then app_pair of_int - (coerce_to_int m / coerce_to_int n, coerce_to_int m mod coerce_to_int n) - else app_pair of_ints (euclid (to_ints m) (to_ints n)) - -let less_than m n = - if Obj.is_int m && Obj.is_int n - then coerce_to_int m < coerce_to_int n - else less_than (to_ints m) (to_ints n) - -let neg n = - if Obj.is_int n then of_int (- (coerce_to_int n)) - else of_ints (neg (to_ints n)) - -let of_string m = of_ints (of_string m) -let to_string m = to_string (to_ints m) - -let zero = of_int 0 -let one = of_int 1 -let two = of_int 2 -let sub_1 n = sub n one -let add_1 n = add n one -let mult_2 n = add n n - -let div2_with_rest n = - let (q,b) = euclid n two in - (q, b == one) - -let is_strictly_neg n = is_strictly_neg (to_ints n) -let is_strictly_pos n = is_strictly_pos (to_ints n) -let is_neg_or_zero n = is_neg_or_zero (to_ints n) -let is_pos_or_zero n = is_pos_or_zero (to_ints n) - -let equal m n = - if Obj.is_block m && Obj.is_block n then - ArrayInt.equal (Obj.obj m) (Obj.obj n) - else m == n - -(* spiwack: computes n^m *) -(* The basic idea of the algorithm is that n^(2m) = (n^2)^m *) -(* In practice the algorithm performs : - k*n^0 = k - k*n^(2m) = k*(n*n)^m - k*n^(2m+1) = (n*k)*(n*n)^m *) -let pow = - let rec pow_aux odd_rest n m = (* odd_rest is the k from above *) - if m<=0 then - odd_rest - else - let quo = m lsr 1 (* i.e. m/2 *) - and odd = not (Int.equal (m land 1) 0) in - pow_aux - (if odd then mult n odd_rest else odd_rest) - (mult n n) - quo - in - pow_aux one - -(** Testing suite w.r.t. OCaml's Big_int *) - -(* -module B = struct - open Big_int - let zero = zero_big_int - let to_string = string_of_big_int - let of_string = big_int_of_string - let add = add_big_int - let opp = minus_big_int - let sub = sub_big_int - let mul = mult_big_int - let abs = abs_big_int - let sign = sign_big_int - let euclid n m = - let n' = abs n and m' = abs m in - let q',r' = quomod_big_int n' m' in - (if sign (mul n m) < 0 && sign q' <> 0 then opp q' else q'), - (if sign n < 0 then opp r' else r') -end - -let check () = - let roots = [ 1; 100; base; 100*base; base*base ] in - let rands = [ 1234; 5678; 12345678; 987654321 ] in - let nums = (List.flatten (List.map (fun x -> [x-1;x;x+1]) roots)) @ rands in - let numbers = - List.map string_of_int nums @ - List.map (fun n -> string_of_int (-n)) nums - in - let i = ref 0 in - let compare op x y n n' = - incr i; - let s = Printf.sprintf "%30s" (to_string n) in - let s' = Printf.sprintf "%30s" (B.to_string n') in - if s <> s' then Printf.printf "%s%s%s: %s <> %s\n" x op y s s' in - let test x y = - let n = of_string x and m = of_string y in - let n' = B.of_string x and m' = B.of_string y in - let a = add n m and a' = B.add n' m' in - let s = sub n m and s' = B.sub n' m' in - let p = mult n m and p' = B.mul n' m' in - let q,r = try euclid n m with Division_by_zero -> zero,zero - and q',r' = try B.euclid n' m' with Division_by_zero -> B.zero, B.zero - in - compare "+" x y a a'; - compare "-" x y s s'; - compare "*" x y p p'; - compare "/" x y q q'; - compare "%" x y r r' - in - List.iter (fun a -> List.iter (test a) numbers) numbers; - Printf.printf "%i tests done\n" !i -*) diff --git a/clib/bigint.mli b/clib/bigint.mli deleted file mode 100644 index 9677c93873..0000000000 --- a/clib/bigint.mli +++ /dev/null @@ -1,53 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(** Arbitrary large integer numbers *) - -type bigint - -val of_string : string -> bigint -(** May raise a Failure just as [int_of_string] on non-numerical strings *) - -val to_string : bigint -> string - -val of_int : int -> bigint -val to_int : bigint -> int (** May raise a Failure on oversized numbers *) - -val zero : bigint -val one : bigint -val two : bigint - -val div2_with_rest : bigint -> bigint * bool (** true=odd; false=even *) - -val add_1 : bigint -> bigint -val sub_1 : bigint -> bigint -val mult_2 : bigint -> bigint - -val add : bigint -> bigint -> bigint -val sub : bigint -> bigint -> bigint -val mult : bigint -> bigint -> bigint - -(** Euclid division m/d = (q,r), with m = q*d+r and |r|<|q|. - This is the "Trunc" variant (a.k.a "Truncated-Toward-Zero"), - as with ocaml's / (but not as ocaml's Big_int.quomod_big_int). - We have sign r = sign m *) - -val euclid : bigint -> bigint -> bigint * bigint - -val less_than : bigint -> bigint -> bool -val equal : bigint -> bigint -> bool - -val is_strictly_pos : bigint -> bool -val is_strictly_neg : bigint -> bool -val is_pos_or_zero : bigint -> bool -val is_neg_or_zero : bigint -> bool -val neg : bigint -> bigint - -val pow : bigint -> int -> bigint diff --git a/configure.ml b/configure.ml index 6863d412cc..2dbc01651e 100644 --- a/configure.ml +++ b/configure.ml @@ -688,19 +688,20 @@ let operating_system = else (try Sys.getenv "OS" with Not_found -> "") -(** Num library *) - -(* since 4.06, the Num library is no longer distributed with OCaml (replaced - by Zarith) -*) +(** Zarith and num libraries *) let check_for_numlib () = - if caml_version_nums >= [4;6;0] then + (if caml_version_nums >= [4;6;0] then let numlib,_ = tryrun camlexec.find ["query";"num"] in match numlib with | "" -> - die "Num library not installed, required for OCaml 4.06 or later" - | _ -> cprintf "You have the Num library installed. Good!" + die "Num library not installed, required for OCaml 4.06 or later" + | _ -> cprintf "You have the Num library installed. Good!"); + let zarith,_ = tryrun camlexec.find ["query";"zarith"] in + match zarith with + | "" -> + die "Zarith library not installed, required" + | _ -> cprintf "You have the Zarith library installed. Good!" let numlib = check_for_numlib () @@ -25,6 +25,7 @@ depends: [ "dune" { >= "2.5.0" } "ocamlfind" { build } "num" + "zarith" { >= "1.9.1" } ] build: [ diff --git a/coq.opam.docker b/coq.opam.docker index 229a47a87b..ac1869f344 100644 --- a/coq.opam.docker +++ b/coq.opam.docker @@ -24,6 +24,7 @@ depends: [ "ocaml" { >= "4.05.0" } "ocamlfind" { build } "num" + "zarith" { >= "1.9.1" } "conf-findutils" {build} ] diff --git a/default.nix b/default.nix index df1c43101b..ef969acd31 100644 --- a/default.nix +++ b/default.nix @@ -43,7 +43,7 @@ stdenv.mkDerivation rec { hostname python3 time # coq-makefile timing tools ] - ++ (with ocamlPackages; [ ocaml findlib ]) + ++ (with ocamlPackages; [ ocaml findlib num zarith ]) ++ optionals buildIde [ ocamlPackages.lablgtk3-sourceview3 glib gnome3.defaultIconTheme wrapGAppsHook diff --git a/dev/base_include b/dev/base_include index 1f14fc2941..daee2d97c5 100644 --- a/dev/base_include +++ b/dev/base_include @@ -29,7 +29,6 @@ #install_printer ppatom;; #install_printer ppwhd;; #install_printer ppvblock;; -#install_printer (* bigint *) ppbigint;; #install_printer (* loc *) pploc;; #install_printer (* substitution *) ppsubst;; diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index fd6ea9bb09..8eff2cf577 100755 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -389,6 +389,7 @@ IF "%RUNSETUP%"=="Y" ( -P libfontconfig1 ^
-P gtk-update-icon-cache ^
-P libtool,automake ^
+ -P libgmp-devel ^
-P intltool ^
-P bison,flex ^
%EXTRAPACKAGES% ^
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index cc9fd13fdc..cde1d798a0 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1006,6 +1006,7 @@ function make_ocaml_tools { function make_ocaml_libs { make_num + make_zarith make_findlib make_lablgtk } @@ -1023,6 +1024,16 @@ function make_num { fi } +function make_zarith { + make_ocaml + if build_prep https://github.com/ocaml/Zarith/archive release-1.9.1 tar.gz 1 zarith-1.9.1; then + logn configure ./configure + log1 make + log2 make install + build_post + fi +} + ##### OCAMLBUILD ##### function make_ocamlbuild { diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh index 64936cd236..17d71ac52a 100755 --- a/dev/ci/azure-opam.sh +++ b/dev/ci/azure-opam.sh @@ -10,4 +10,4 @@ bash opam64/install.sh opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $OPAM_VARIANT --disable-sandboxing eval "$(opam env)" -opam install -y num ocamlfind dune ounit +opam install -y num ocamlfind dune ounit zarith diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 67a8415891..78c8673299 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-08-18-V29" +# CACHEKEY: "bionic_coq-V2020-08-28-V92" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -6,9 +6,14 @@ LABEL maintainer="e@x80.org" ENV DEBIAN_FRONTEND="noninteractive" +# We need libgmp-dev:i386 for zarith; maybe we could also install GTK +RUN dpkg --add-architecture i386 + RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ # Dependencies of the image, the test-suite and external projects m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip jq \ + # Dependencies of ZArith + perl libgmp-dev libgmp-dev:i386 \ # Dependencies of lablgtk (for CoqIDE) libgtksourceview-3.0-dev \ # Dependencies of stdlib and sphinx doc @@ -35,10 +40,10 @@ ENV NJOBS="2" \ # Base opam is the set of base packages required by Coq ENV COMPILER="4.05.0" -# Common OPAM packages. -# `num` does not have a version number as the right version to install varies -# with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.0" \ +# Common OPAM packages, num to be removed once the migration to +# micromega is complete, `num` also does not have a version number as +# the right version to install varies with the compiler version. +ENV BASE_OPAM="num zarith.1.9.1 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.0" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ BASE_ONLY_OPAM="elpi.1.11.0" @@ -52,9 +57,10 @@ ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0" RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \ opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM $BASE_ONLY_OPAM -# base+32bit switch +# base+32bit switch, note the zarith hack RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ - opam install $BASE_OPAM + i386 env CC='gcc -m32' opam install zarith.1.9.1 && \ + opam install $BASE_OPAM # EDGE switch ENV COMPILER_EDGE="4.10.0" \ diff --git a/dev/ci/user-overlays/08743-ejgallego-zarith.sh b/dev/ci/user-overlays/08743-ejgallego-zarith.sh new file mode 100644 index 0000000000..da1d30c1e9 --- /dev/null +++ b/dev/ci/user-overlays/08743-ejgallego-zarith.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "11742" ] || [ "$CI_BRANCH" = "zarith+core" ]; then + + bignums_CI_REF=zarith + bignums_CI_GITURL=https://github.com/ejgallego/bignums + +fi diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index 63071bba72..60618f6491 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -23,7 +23,6 @@ install_printer Top_printers.ppconstr_expr install_printer Top_printers.ppglob_constr install_printer Top_printers.pppattern install_printer Top_printers.ppfconstr -install_printer Top_printers.ppbigint install_printer Top_printers.ppnumtokunsigned install_printer Top_printers.ppnumtokunsignednat install_printer Top_printers.ppintset diff --git a/dev/top_printers.ml b/dev/top_printers.ml index ea90e83a83..773170207e 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -80,7 +80,6 @@ let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x)) let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e))) let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) -let ppbigint n = pp (str (Bigint.to_string n));; let ppnumtokunsigned n = pp (NumTok.Unsigned.print n) let ppnumtokunsignednat n = pp (NumTok.UnsignedNat.print n) diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 65eab8daa3..b1bb5e4702 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -53,7 +53,6 @@ val ppglob_constr : 'a Glob_term.glob_constr_g -> unit val pppattern : Pattern.constr_pattern -> unit val ppfconstr : CClosure.fconstr -> unit -val ppbigint : Bigint.bigint -> unit val ppnumtokunsigned : NumTok.Unsigned.t -> unit val ppnumtokunsignednat : NumTok.UnsignedNat.t -> unit diff --git a/doc/changelog/11-infrastructure-and-dependencies/11742-zarith+core.rst b/doc/changelog/11-infrastructure-and-dependencies/11742-zarith+core.rst new file mode 100644 index 0000000000..3b34e11ff8 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/11742-zarith+core.rst @@ -0,0 +1,8 @@ +- **Changed:** + Coq's core system now uses the `zarith <https://github.com/ocaml/Zarith>`_ + library, based on GNU's gmp instead of ``num`` which is + deprecated upstream. The custom ``bigint`` module is + not longer provided; note that the ``micromega`` still uses + ``num`` + (`#11742 <https://github.com/coq/coq/pull/11742>`_, + by Emilio Jesus Gallego Arias and Vicent Laporte). diff --git a/interp/dune b/interp/dune index e9ef7ba99a..6d73d5724c 100644 --- a/interp/dune +++ b/interp/dune @@ -3,4 +3,4 @@ (synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]") (public_name coq.interp) (wrapped false) - (libraries pretyping)) + (libraries zarith pretyping)) diff --git a/interp/notation.ml b/interp/notation.ml index 0bd5da5729..17ae045187 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -388,7 +388,7 @@ module InnerPrimToken = struct type interpreter = | RawNumInterp of (?loc:Loc.t -> rawnum -> glob_constr) - | BigNumInterp of (?loc:Loc.t -> Bigint.bigint -> glob_constr) + | BigNumInterp of (?loc:Loc.t -> Z.t -> glob_constr) | StringInterp of (?loc:Loc.t -> string -> glob_constr) let interp_eq f f' = match f,f' with @@ -410,7 +410,7 @@ module InnerPrimToken = struct type uninterpreter = | RawNumUninterp of (any_glob_constr -> rawnum option) - | BigNumUninterp of (any_glob_constr -> Bigint.bigint option) + | BigNumUninterp of (any_glob_constr -> Z.t option) | StringUninterp of (any_glob_constr -> string option) let uninterp_eq f f' = match f,f' with @@ -612,13 +612,14 @@ let uninterp to_raw o (Glob_term.AnyGlobConstr n) = end +let z_two = Z.of_int 2 + (** Conversion from bigint to int63 *) let rec int63_of_pos_bigint i = - let open Bigint in - if equal i zero then Uint63.of_int 0 + if Z.(equal i zero) then Uint63.of_int 0 else - let (quo,rem) = div2_with_rest i in - if rem then Uint63.add (Uint63.of_int 1) + let quo, remi = Z.div_rem i z_two in + if Z.(equal remi one) then Uint63.add (Uint63.of_int 1) (Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo)) else Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo) @@ -800,24 +801,24 @@ let rawnum_of_coqint c = (** First, [positive] from/to bigint *) let rec pos_of_bigint posty n = - match Bigint.div2_with_rest n with - | (q, false) -> + match Z.div_rem n z_two with + | (q, rem) when rem = Z.zero -> let c = mkConstruct (posty, 2) in (* xO *) mkApp (c, [| pos_of_bigint posty q |]) - | (q, true) when not (Bigint.equal q Bigint.zero) -> + | (q, _) when not (Z.equal q Z.zero) -> let c = mkConstruct (posty, 1) in (* xI *) mkApp (c, [| pos_of_bigint posty q |]) - | (q, true) -> + | (q, _) -> mkConstruct (posty, 3) (* xH *) let rec bigint_of_pos c = match Constr.kind c with - | Construct ((_, 3), _) -> (* xH *) Bigint.one + | Construct ((_, 3), _) -> (* xH *) Z.one | App (c, [| d |]) -> begin match Constr.kind c with | Construct ((_, n), _) -> begin match n with - | 1 -> (* xI *) Bigint.add_1 (Bigint.mult_2 (bigint_of_pos d)) - | 2 -> (* xO *) Bigint.mult_2 (bigint_of_pos d) + | 1 -> (* xI *) Z.add Z.one (Z.mul z_two (bigint_of_pos d)) + | 2 -> (* xO *) Z.mul z_two (bigint_of_pos d) | n -> assert false (* no other constructor of type positive *) end | x -> raise NotAValidPrimToken @@ -827,24 +828,24 @@ let rec bigint_of_pos c = match Constr.kind c with (** Now, [Z] from/to bigint *) let z_of_bigint { z_ty; pos_ty } n = - if Bigint.equal n Bigint.zero then + if Z.(equal n zero) then mkConstruct (z_ty, 1) (* Z0 *) else let (s, n) = - if Bigint.is_pos_or_zero n then (2, n) (* Zpos *) - else (3, Bigint.neg n) (* Zneg *) + if Z.(leq zero n) then (2, n) (* Zpos *) + else (3, Z.neg n) (* Zneg *) in let c = mkConstruct (z_ty, s) in mkApp (c, [| pos_of_bigint pos_ty n |]) let bigint_of_z z = match Constr.kind z with - | Construct ((_, 1), _) -> (* Z0 *) Bigint.zero + | Construct ((_, 1), _) -> (* Z0 *) Z.zero | App (c, [| d |]) -> begin match Constr.kind c with | Construct ((_, n), _) -> begin match n with | 2 -> (* Zpos *) bigint_of_pos d - | 3 -> (* Zneg *) Bigint.neg (bigint_of_pos d) + | 3 -> (* Zneg *) Z.neg (bigint_of_pos d) | n -> assert false (* no other constructor of type Z *) end | _ -> raise NotAValidPrimToken @@ -861,20 +862,19 @@ let error_negative ?loc = CErrors.user_err ?loc ~hdr:"interp_int63" (Pp.str "int63 are only non-negative numbers.") let error_overflow ?loc n = - CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Bigint.to_string n)) + CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Z.to_string n)) let interp_int63 ?loc n = - let open Bigint in - if is_pos_or_zero n + if Z.(leq zero n) then - if less_than n (pow two 63) + if Z.(lt n (pow z_two 63)) then int63_of_pos_bigint ?loc n else error_overflow ?loc n else error_negative ?loc let bigint_of_int63 c = match Constr.kind c with - | Int i -> Bigint.of_string (Uint63.to_string i) + | Int i -> Z.of_string (Uint63.to_string i) | _ -> raise NotAValidPrimToken let interp o ?loc n = diff --git a/interp/notation.mli b/interp/notation.mli index 05ddd25a62..948831b317 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -101,7 +101,7 @@ val register_rawnumeral_interpretation : ?allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit val register_bignumeral_interpretation : - ?allow_overwrite:bool -> prim_token_uid -> Bigint.bigint prim_token_interpretation -> unit + ?allow_overwrite:bool -> prim_token_uid -> Z.t prim_token_interpretation -> unit val register_string_interpretation : ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit @@ -196,8 +196,8 @@ val enable_prim_token_interpretation : prim_token_infos -> unit *) val declare_numeral_interpreter : ?local:bool -> scope_name -> required_module -> - Bigint.bigint prim_token_interpreter -> - glob_constr list * Bigint.bigint prim_token_uninterpreter * bool -> unit + Z.t prim_token_interpreter -> + glob_constr list * Z.t prim_token_uninterpreter * bool -> unit val declare_string_interpreter : ?local:bool -> scope_name -> required_module -> string prim_token_interpreter -> glob_constr list * string prim_token_uninterpreter * bool -> unit @@ -349,4 +349,4 @@ val level_of_notation : notation -> level val with_notation_protection : ('a -> 'b) -> 'a -> 'b (** Conversion from bigint to int63 *) -val int63_of_pos_bigint : Bigint.bigint -> Uint63.t +val int63_of_pos_bigint : Z.t -> Uint63.t diff --git a/interp/numTok.ml b/interp/numTok.ml index bb14649b91..124a6cd249 100644 --- a/interp/numTok.ml +++ b/interp/numTok.ml @@ -80,63 +80,14 @@ struct let to_string (sign,n) = (match sign with SPlus -> "" | SMinus -> "-") ^ UnsignedNat.to_string n let classify (_,n) = UnsignedNat.classify n - let bigint_of_string (sign,n) = - (* nasty code to remove when switching to zarith - since zarith's of_string handles hexadecimal *) - match UnsignedNat.classify n with - | CDec -> Bigint.of_string (to_string (sign,n)) - | CHex -> - let int_of_char c = match c with - | 'a'..'f' -> 10 + int_of_char c - int_of_char 'a' - | _ -> int_of_char c - int_of_char '0' in - let c16 = Bigint.of_int 16 in - let s = UnsignedNat.to_string n in - let n = ref Bigint.zero in - let len = String.length s in - for d = 2 to len - 1 do - n := Bigint.(add (mult !n c16) (of_int (int_of_char s.[d]))) - done; - match sign with SPlus -> !n | SMinus -> Bigint.neg !n + let bigint_of_string (sign,n) = Z.of_string (to_string (sign,n)) let to_bigint n = bigint_of_string n let string_of_nonneg_bigint c n = - (* nasty code to remove when switching to zarith - since zarith's format handles hexadecimal *) match c with - | CDec -> Bigint.to_string n - | CHex -> - let div16 n = - let n, r0 = Bigint.div2_with_rest n in - let n, r1 = Bigint.div2_with_rest n in - let n, r2 = Bigint.div2_with_rest n in - let n, r3 = Bigint.div2_with_rest n in - let r = match r3, r2, r1, r0 with - | false, false, false, false -> "0" - | false, false, false, true -> "1" - | false, false, true, false -> "2" - | false, false, true, true -> "3" - | false, true, false, false -> "4" - | false, true, false, true -> "5" - | false, true, true, false -> "6" - | false, true, true, true -> "7" - | true, false, false, false -> "8" - | true, false, false, true -> "9" - | true, false, true, false -> "a" - | true, false, true, true -> "b" - | true, true, false, false -> "c" - | true, true, false, true -> "d" - | true, true, true, false -> "e" - | true, true, true, true -> "f" in - n, r in - let n = ref n in - let l = ref [] in - while Bigint.is_strictly_pos !n do - let n', r = div16 !n in - n := n'; - l := r :: !l - done; - "0x" ^ String.concat "" (List.rev !l) + | CDec -> Z.format "%d" n + | CHex -> Z.format "0x%x" n let of_bigint c n = - let sign, n = if Bigint.is_strictly_neg n then (SMinus, Bigint.neg n) else (SPlus, n) in + let sign, n = if Int.equal (-1) (Z.sign n) then (SMinus, Z.neg n) else (SPlus, n) in (sign, string_of_nonneg_bigint c n) end @@ -339,13 +290,13 @@ struct let frac = UnsignedNat.to_string frac in let i = SignedNat.to_bigint (s, int ^ frac) in let e = - let e = if exp = "" then Bigint.zero else match exp.[1] with - | '+' -> Bigint.of_string (UnsignedNat.to_string (string_del_head 2 exp)) - | '-' -> Bigint.(neg (of_string (UnsignedNat.to_string (string_del_head 2 exp)))) - | _ -> Bigint.of_string (UnsignedNat.to_string (string_del_head 1 exp)) in + let e = if exp = "" then Z.zero else match exp.[1] with + | '+' -> Z.of_string (UnsignedNat.to_string (string_del_head 2 exp)) + | '-' -> Z.(neg (of_string (UnsignedNat.to_string (string_del_head 2 exp)))) + | _ -> Z.of_string (UnsignedNat.to_string (string_del_head 1 exp)) in let l = String.length frac in let l = match c with CDec -> l | CHex -> 4 * l in - Bigint.(sub e (of_int l)) in + Z.(sub e (of_int l)) in (i, match c with CDec -> EDec e | CHex -> EBin e) let of_bigint_and_exponent i e = diff --git a/interp/numTok.mli b/interp/numTok.mli index 11d5a0f980..bcfe663dd2 100644 --- a/interp/numTok.mli +++ b/interp/numTok.mli @@ -65,8 +65,8 @@ sig val classify : t -> num_class - val of_bigint : num_class -> Bigint.bigint -> t - val to_bigint : t -> Bigint.bigint + val of_bigint : num_class -> Z.t -> t + val to_bigint : t -> Z.t end (** {6 Unsigned decimal numerals } *) @@ -131,8 +131,8 @@ sig val to_string : t -> string (** Returns a string in the syntax of OCaml's float_of_string *) - val of_bigint : num_class -> Bigint.bigint -> t - val to_bigint : t -> Bigint.bigint option + val of_bigint : num_class -> Z.t -> t + val to_bigint : t -> Z.t option (** Convert from and to bigint when the denotation of a bigint *) val of_int_frac_and_exponent : SignedNat.t -> UnsignedNat.t option -> SignedNat.t option -> t @@ -140,8 +140,8 @@ sig (** n, p and q such that the number is n.p*10^q or n.p*2^q pre/postcondition: classify n = classify p, classify q = CDec *) - val of_bigint_and_exponent : Bigint.bigint -> Bigint.bigint exp -> t - val to_bigint_and_exponent : t -> Bigint.bigint * Bigint.bigint exp + val of_bigint_and_exponent : Z.t -> Z.t exp -> t + val to_bigint_and_exponent : t -> Z.t * Z.t exp (** n and p such that the number is n*10^p or n*2^p *) val classify : t -> num_class diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml index 19055fd425..7228f709f1 100644 --- a/plugins/extraction/big.ml +++ b/plugins/extraction/big.ml @@ -8,63 +8,61 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** [Big] : a wrapper around ocaml [Big_int] with nicer names, +(** [Big] : a wrapper around ocaml [ZArith] with nicer names, and a few extraction-specific constructions *) -(** To be linked with [nums.(cma|cmxa)] *) +(** To be linked with [zarith] *) -open Big_int - -type big_int = Big_int.big_int +type big_int = Z.t (** The type of big integers. *) -let zero = zero_big_int +let zero = Z.zero (** The big integer [0]. *) -let one = unit_big_int +let one = Z.one (** The big integer [1]. *) -let two = big_int_of_int 2 +let two = Z.of_int 2 (** The big integer [2]. *) (** {6 Arithmetic operations} *) -let opp = minus_big_int +let opp = Z.neg (** Unary negation. *) -let abs = abs_big_int +let abs = Z.abs (** Absolute value. *) -let add = add_big_int +let add = Z.add (** Addition. *) -let succ = succ_big_int - (** Successor (add 1). *) +let succ = Z.succ +(** Successor (add 1). *) -let add_int = add_int_big_int +let add_int = Z.add (** Addition of a small integer to a big integer. *) -let sub = sub_big_int +let sub = Z.sub (** Subtraction. *) -let pred = pred_big_int +let pred = Z.pred (** Predecessor (subtract 1). *) -let mult = mult_big_int +let mult = Z.mul (** Multiplication of two big integers. *) -let mult_int = mult_int_big_int +let mult_int x y = Z.mul (Z.of_int x) y (** Multiplication of a big integer by a small integer *) -let square = square_big_int +let square x = Z.mul x x (** Return the square of the given big integer *) -let sqrt = sqrt_big_int +let sqrt = Z.sqrt (** [sqrt_big_int a] returns the integer square root of [a], that is, the largest big integer [r] such that [r * r <= a]. Raise [Invalid_argument] if [a] is negative. *) -let quomod = quomod_big_int +let quomod = Z.div_rem (** Euclidean division of two big integers. The first part of the result is the quotient, the second part is the remainder. @@ -72,18 +70,18 @@ let quomod = quomod_big_int [a = q * b + r] and [0 <= r < |b|]. Raise [Division_by_zero] if the divisor is zero. *) -let div = div_big_int +let div = Z.div (** Euclidean quotient of two big integers. This is the first result [q] of [quomod_big_int] (see above). *) -let modulo = mod_big_int +let modulo = Z.(mod) (** Euclidean modulus of two big integers. This is the second result [r] of [quomod_big_int] (see above). *) -let gcd = gcd_big_int +let gcd = Z.gcd (** Greatest common divisor of two big integers. *) -let power = power_big_int_positive_big_int +let power = Z.pow (** Exponentiation functions. Return the big integer representing the first argument [a] raised to the power [b] (the second argument). Depending @@ -92,45 +90,45 @@ let power = power_big_int_positive_big_int (** {6 Comparisons and tests} *) -let sign = sign_big_int +let sign = Z.sign (** Return [0] if the given big integer is zero, [1] if it is positive, and [-1] if it is negative. *) -let compare = compare_big_int +let compare = Z.compare (** [compare_big_int a b] returns [0] if [a] and [b] are equal, [1] if [a] is greater than [b], and [-1] if [a] is smaller than [b]. *) -let eq = eq_big_int -let le = le_big_int -let ge = ge_big_int -let lt = lt_big_int -let gt = gt_big_int +let eq = Z.equal +let le = Z.leq +let ge = Z.geq +let lt = Z.lt +let gt = Z.gt (** Usual boolean comparisons between two big integers. *) -let max = max_big_int +let max = Z.max (** Return the greater of its two arguments. *) -let min = min_big_int +let min = Z.min (** Return the smaller of its two arguments. *) (** {6 Conversions to and from strings} *) -let to_string = string_of_big_int +let to_string = Z.to_string (** Return the string representation of the given big integer, in decimal (base 10). *) -let of_string = big_int_of_string +let of_string = Z.of_string (** Convert a string to a big integer, in decimal. The string consists of an optional [-] or [+] sign, followed by one or several decimal digits. *) (** {6 Conversions to and from other numerical types} *) -let of_int = big_int_of_int +let of_int = Z.of_int (** Convert a small integer to a big integer. *) -let is_int = is_int_big_int +let is_int = Z.fits_int (** Test whether the given big integer is small enough to be representable as a small integer (type [int]) without loss of precision. On a 32-bit platform, @@ -139,7 +137,7 @@ let is_int = is_int_big_int [is_int_big_int a] returns [true] if and only if [a] is between -2{^62} and 2{^62}-1. *) -let to_int = int_of_big_int +let to_int = Z.to_int (** Convert a big integer to a small integer (type [int]). Raises [Failure "int_of_big_int"] if the big integer is not representable as a small integer. *) diff --git a/plugins/extraction/dune b/plugins/extraction/dune index 0c01dcd488..d9d675fe6a 100644 --- a/plugins/extraction/dune +++ b/plugins/extraction/dune @@ -2,6 +2,6 @@ (name extraction_plugin) (public_name coq.plugins.extraction) (synopsis "Coq's extraction plugin") - (libraries num coq.plugins.ltac)) + (libraries coq.plugins.ltac)) (coq.pp (modules g_extraction)) diff --git a/plugins/nsatz/dune b/plugins/nsatz/dune index b921c9c408..3b67ab3429 100644 --- a/plugins/nsatz/dune +++ b/plugins/nsatz/dune @@ -2,6 +2,6 @@ (name nsatz_plugin) (public_name coq.plugins.nsatz) (synopsis "Coq's nsatz solver plugin") - (libraries num coq.plugins.ltac)) + (libraries coq.plugins.ltac)) (coq.pp (modules g_nsatz)) diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index 387145a5d0..cbc1773ede 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -153,8 +153,8 @@ end module Make (P:Polynom.S) = struct type coef = P.t - let coef0 = P.of_num (Num.Int 0) - let coef1 = P.of_num (Num.Int 1) + let coef0 = P.of_num Q.zero + let coef1 = P.of_num Q.one let string_of_coef c = "["^(P.to_string c)^"]" (*********************************************************************** @@ -305,7 +305,7 @@ let mult_t_pol a m p = let map (b, m') = (P.multP a b, mult_mon m m') in CList.map map p -let coef_of_int x = P.of_num (Num.Int x) +let coef_of_int x = P.of_num (Q.of_int x) (* variable i *) let gen d i = diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml index 29d08fb4ea..f3021f4ee6 100644 --- a/plugins/nsatz/nsatz.ml +++ b/plugins/nsatz/nsatz.ml @@ -13,30 +13,20 @@ open Util open Constr open Tactics -open Num open Utile (*********************************************************************** Operations on coefficients *) -let num_0 = Int 0 -and num_1 = Int 1 -and num_2 = Int 2 - -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') - module BigInt = struct - open Big_int + open Big_int_Z type t = big_int let of_int = big_int_of_int let coef0 = of_int 0 - let of_num = Num.big_int_of_num - let to_num = Num.num_of_big_int + let of_num = Q.to_bigint + let to_num = Q.of_bigint let equal = eq_big_int let lt = lt_big_int let le = le_big_int @@ -113,7 +103,7 @@ type vname = string type term = | Zero - | Const of Num.num + | Const of Q.t | Var of vname | Opp of term | Add of term * term @@ -122,7 +112,7 @@ type term = | Pow of term * int let const n = - if eq_num n num_0 then Zero else Const n + if Q.(equal zero) n then Zero else Const n let pow(p,i) = if Int.equal i 1 then p else Pow(p,i) let add = function (Zero,q) -> q @@ -131,8 +121,8 @@ let add = function let mul = function (Zero,_) -> Zero | (_,Zero) -> Zero - | (p,Const n) when eq_num n num_1 -> p - | (Const n,q) when eq_num n num_1 -> q + | (p,Const n) when Q.(equal one) n -> p + | (Const n,q) when Q.(equal one) n -> q | (p,q) -> Mul(p,q) let gen_constant n = lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref n)) @@ -167,62 +157,64 @@ let mkt_app name l = mkApp (Lazy.force name, Array.of_list l) let tlp () = mkt_app tlist [mkt_app tpexpr [Lazy.force tz]] let tllp () = mkt_app tlist [tlp()] -let rec mkt_pos n = - if n =/ num_1 then Lazy.force pxH - else if mod_num n num_2 =/ num_0 then - mkt_app pxO [mkt_pos (quo_num n num_2)] +let mkt_pos n = + let rec mkt_pos n = + if Z.(equal one) n then Lazy.force pxH + else if Z.is_even n then + mkt_app pxO [mkt_pos Z.(n asr 1)] else - mkt_app pxI [mkt_pos (quo_num n num_2)] + mkt_app pxI [mkt_pos Z.(n asr 1)] + in mkt_pos (Q.to_bigint n) let mkt_n n = - if Num.eq_num n num_0 + if Q.(equal zero) n then Lazy.force nN0 else mkt_app nNpos [mkt_pos n] let mkt_z z = - if z =/ num_0 then Lazy.force z0 - else if z >/ num_0 then + if Q.(equal zero) z then Lazy.force z0 + else if Q.(lt zero) z then mkt_app zpos [mkt_pos z] else - mkt_app zneg [mkt_pos ((Int 0) -/ z)] + mkt_app zneg [mkt_pos (Q.neg z)] let rec mkt_term t = match t with -| Zero -> mkt_term (Const num_0) -| Const r -> let (n,d) = numdom r in - mkt_app ttconst [Lazy.force tz; mkt_z n] -| Var v -> mkt_app ttvar [Lazy.force tz; mkt_pos (num_of_string v)] +| Zero -> mkt_term (Const Q.zero) +| Const r -> let n = r |> Q.num |> Q.of_bigint in + mkt_app ttconst [Lazy.force tz; mkt_z n] +| Var v -> mkt_app ttvar [Lazy.force tz; mkt_pos (Q.of_string v)] | Opp t1 -> mkt_app ttopp [Lazy.force tz; mkt_term t1] | Add (t1,t2) -> mkt_app ttadd [Lazy.force tz; mkt_term t1; mkt_term t2] | Sub (t1,t2) -> mkt_app ttsub [Lazy.force tz; mkt_term t1; mkt_term t2] | Mul (t1,t2) -> mkt_app ttmul [Lazy.force tz; mkt_term t1; mkt_term t2] | Pow (t1,n) -> if Int.equal n 0 then - mkt_app ttconst [Lazy.force tz; mkt_z num_1] + mkt_app ttconst [Lazy.force tz; mkt_z Q.one] else - mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (num_of_int n)] + mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (Q.of_int n)] let rec parse_pos p = match Constr.kind p with | App (a,[|p2|]) -> - if Constr.equal a (Lazy.force pxO) then num_2 */ (parse_pos p2) - else num_1 +/ (num_2 */ (parse_pos p2)) -| _ -> num_1 + if Constr.equal a (Lazy.force pxO) then Q.(mul (of_int 2)) (parse_pos p2) + else Q.(add one) Q.(mul (of_int 2) (parse_pos p2)) +| _ -> Q.one let parse_z z = match Constr.kind z with | App (a,[|p2|]) -> - if Constr.equal a (Lazy.force zpos) then parse_pos p2 else (num_0 -/ (parse_pos p2)) -| _ -> num_0 + if Constr.equal a (Lazy.force zpos) then parse_pos p2 else Q.neg (parse_pos p2) +| _ -> Q.zero let parse_n z = match Constr.kind z with | App (a,[|p2|]) -> parse_pos p2 -| _ -> num_0 +| _ -> Q.zero let rec parse_term p = match Constr.kind p with | App (a,[|_;p2|]) -> - if Constr.equal a (Lazy.force ttvar) then Var (string_of_num (parse_pos p2)) + if Constr.equal a (Lazy.force ttvar) then Var (Q.to_string (parse_pos p2)) else if Constr.equal a (Lazy.force ttconst) then Const (parse_z p2) else if Constr.equal a (Lazy.force ttopp) then Opp (parse_term p2) else Zero @@ -231,7 +223,7 @@ let rec parse_term p = else if Constr.equal a (Lazy.force ttsub) then Sub (parse_term p2, parse_term p3) else if Constr.equal a (Lazy.force ttmul) then Mul (parse_term p2, parse_term p3) else if Constr.equal a (Lazy.force ttpow) then - Pow (parse_term p2, int_of_num (parse_n p3)) + Pow (parse_term p2, Q.to_int (parse_n p3)) else Zero | _ -> Zero @@ -278,7 +270,7 @@ let term_pol_sparse nvars np t= match t with | Zero -> zeroP | Const r -> - if Num.eq_num r num_0 + if Q.(equal zero) r then zeroP else polconst d (Poly.Pint (Coef.of_num r)) | Var v -> @@ -316,7 +308,7 @@ let pol_sparse_to_term n2 p = let p = PIdeal.repr p in let rec aux p = match p with - [] -> const (num_of_string "0") + [] -> const Q.zero | (a,m)::p1 -> let m = Ideal.Monomial.repr m in let n = (Array.length m)-1 in @@ -443,8 +435,9 @@ let expand_pol lb lp = let theoremedeszeros_termes lp = let nvars = List.fold_left set_nvars_term 0 lp in match lp with - | Const (Int sugarparam)::Const (Int nparam)::lp -> - ((match sugarparam with + | Const sugarparam :: Const nparam :: lp -> + let nparam = Q.to_int nparam in + ((match Q.to_int sugarparam with |0 -> sinfo "computation without sugar"; lexico:=false; |1 -> sinfo "computation with sugar"; diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml index 726ad54cad..2565d88b13 100644 --- a/plugins/nsatz/polynom.ml +++ b/plugins/nsatz/polynom.ml @@ -30,7 +30,7 @@ module type Coef = sig val pgcd : t -> t -> t val hash : t -> int - val of_num : Num.num -> t + val of_num : Q.t -> t val to_string : t -> string end @@ -39,7 +39,7 @@ module type S = sig type variable = int type t = Pint of coef | Prec of variable * t array - val of_num : Num.num -> t + val of_num : Q.t -> t val x : variable -> t val monome : variable -> int -> t val is_constantP : t -> bool @@ -106,7 +106,7 @@ end module Make (C:Coef) = struct type coef = C.t -let coef_of_int i = C.of_num (Num.Int i) +let coef_of_int i = C.of_num (Q.of_int i) let coef0 = coef_of_int 0 let coef1 = coef_of_int 1 @@ -125,8 +125,8 @@ type t = (* constant polynomials *) let of_num x = Pint (C.of_num x) -let cf0 = of_num (Num.Int 0) -let cf1 = of_num (Num.Int 1) +let cf0 = of_num Q.zero +let cf1 = of_num Q.one (* nth variable *) let x n = Prec (n,[|cf0;cf1|]) diff --git a/plugins/nsatz/polynom.mli b/plugins/nsatz/polynom.mli index 3807a8582b..91f1bcda90 100644 --- a/plugins/nsatz/polynom.mli +++ b/plugins/nsatz/polynom.mli @@ -26,7 +26,7 @@ module type Coef = sig val pgcd : t -> t -> t val hash : t -> int - val of_num : Num.num -> t + val of_num : Q.t -> t val to_string : t -> string end @@ -35,7 +35,7 @@ module type S = sig type variable = int type t = Pint of coef | Prec of variable * t array - val of_num : Num.num -> t + val of_num : Q.t -> t val x : variable -> t val monome : variable -> int -> t val is_constantP : t -> bool diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index cd5b747d75..4f7b3fbe74 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -32,7 +32,22 @@ open Tactypes open Context.Named.Declaration module NamedDecl = Context.Named.Declaration -module OmegaSolver = Omega.MakeOmegaSolver (Bigint) + +module ZOmega = struct + type bigint = Z.t + let equal = Z.equal + let less_than = Z.lt + let add = Z.add + let sub = Z.sub + let mult = Z.mul + let euclid = Z.div_rem + let neg = Z.neg + let zero = Z.zero + let one = Z.one + let to_string = Z.to_string +end + +module OmegaSolver = Omega.MakeOmegaSolver (ZOmega) open OmegaSolver (* Added by JCF, 09/03/98 *) @@ -719,7 +734,7 @@ let rec shuffle p (t1,t2) = Oplus(l2,t') else [],Oplus(t1,t2) | Oz t1,Oz t2 -> - [focused_simpl p], Oz(Bigint.add t1 t2) + [focused_simpl p], Oz(Z.add t1 t2) | t1,t2 -> if weight t1 < weight t2 then [clever_rewrite p [[P_APP 1];[P_APP 2]] @@ -741,7 +756,7 @@ let shuffle_mult p_init k1 e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA10) in - if Bigint.add (Bigint.mult k1 c1) (Bigint.mult k2 c2) =? zero then + if Z.add (Z.mul k1 c1) (Z.mul k2 c2) =? zero then let tac' = clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zred_factor5) in @@ -798,7 +813,7 @@ let shuffle_mult_right p_init e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA15) in - if Bigint.add c1 (Bigint.mult k2 c2) =? zero then + if Z.add c1 (Z.mul k2 c2) =? zero then let tac' = clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zred_factor5) @@ -1004,7 +1019,7 @@ let reduce_factor p = function | Otimes(Oatom v,c) -> let rec compute = function | Oz n -> n - | Oplus(t1,t2) -> Bigint.add (compute t1) (compute t2) + | Oplus(t1,t2) -> Z.add (compute t1) (compute t2) | _ -> CErrors.user_err Pp.(str "condense.1") in [focused_simpl (P_APP 2 :: p)], Otimes(Oatom v,Oz(compute c)) @@ -1160,7 +1175,7 @@ let replay_history tactic_normalisation = | NOT_EXACT_DIVIDE (e1,k) :: l -> let c = floor_div e1.constant k in - let d = Bigint.sub e1.constant (Bigint.mult c k) in + let d = Z.sub e1.constant (Z.mul c k) in let e2 = {id=e1.id; kind=EQUA;constant = c; body = map_eq_linear (fun c -> c / k) e1.body } in let eq2 = val_of(decompile e2) in diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 95faede7d0..6ed6b8da91 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -146,17 +146,21 @@ let ic_unsafe c = (*FIXME remove *) let sigma = Evd.from_env env in fst (Constrintern.interp_constr env sigma c) -let decl_constant na univs c = +let decl_constant name univs c = let open Constr in let vars = CVars.universes_of_constr c in let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in let () = DeclareUctx.declare_universe_context ~poly:false univs in let types = (Typeops.infer (Global.env ()) c).uj_type in let univs = Monomorphic_entry Univ.ContextSet.empty in - mkConst(declare_constant ~name:(Id.of_string na) + mkConst(declare_constant ~name ~kind:Decls.(IsProof Lemma) (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c))) +let decl_constant na suff univs c = + let na = Namegen.next_global_ident_away (Nameops.add_suffix na suff) Id.Set.empty in + decl_constant na univs c + (* Calling a global tactic *) let ltac_call tac (args:glob_tactic_arg list) = TacArg(CAst.make @@ TacCall (CAst.make (ArgArg(Loc.tag @@ Lazy.force tac),args))) @@ -581,9 +585,9 @@ let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div let lemma2 = params.(4) in let lemma1 = - decl_constant (Id.to_string name^"_ring_lemma1") ctx lemma1 in + decl_constant name "_ring_lemma1" ctx lemma1 in let lemma2 = - decl_constant (Id.to_string name^"_ring_lemma2") ctx lemma2 in + decl_constant name "_ring_lemma2" ctx lemma2 in let cst_tac = interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in let pretac = @@ -898,15 +902,15 @@ let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign od match inj with | Some thm -> mkApp(params.(8),[|EConstr.to_constr sigma thm|]) | None -> params.(7) in - let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") + let lemma1 = decl_constant name "_field_lemma1" ctx lemma1 in - let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") + let lemma2 = decl_constant name "_field_lemma2" ctx lemma2 in - let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") + let lemma3 = decl_constant name "_field_lemma3" ctx lemma3 in - let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") + let lemma4 = decl_constant name "_field_lemma4" ctx lemma4 in - let cond_lemma = decl_constant (Id.to_string name^"_lemma5") + let cond_lemma = decl_constant name "_lemma5" ctx cond_lemma in let cst_tac = interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml index 8e87fc13ca..5d8dcd04fe 100644 --- a/plugins/syntax/float_syntax.ml +++ b/plugins/syntax/float_syntax.ml @@ -48,21 +48,21 @@ let interp_float ?loc n = | None -> "" | Some f -> NumTok.UnsignedNat.to_string f in let e = match e with | None -> "0" | Some e -> NumTok.SignedNat.to_string e in - Bigint.of_string (i ^ f), + Z.of_string (i ^ f), (try int_of_string e with Failure _ -> 0) - String.length f in let m', e' = let m', e' = Float64.frshiftexp f in let m' = Float64.normfr_mantissa m' in let e' = Uint63.to_int_min e' 4096 - Float64.eshift - 53 in - Bigint.of_string (Uint63.to_string m'), + Z.of_string (Uint63.to_string m'), e' in - let c2, c5 = Bigint.(of_int 2, of_int 5) in + let c2, c5 = Z.(of_int 2, of_int 5) in (* check m*5^e <> m'*2^e' *) let check m e m' e' = - not (Bigint.(equal (mult m (pow c5 e)) (mult m' (pow c2 e')))) in + not (Z.(equal (mul m (pow c5 e)) (mul m' (pow c2 e')))) in (* check m*5^e*2^e' <> m' *) let check' m e e' m' = - not (Bigint.(equal (mult (mult m (pow c5 e)) (pow c2 e')) m')) in + not (Z.(equal (mul (mul m (pow c5 e)) (pow c2 e')) m')) in (* we now have to check m*10^e <> m'*2^e' *) if e >= 0 then if e <= e' then check m e m' (e' - e) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 23a7cc07c5..d66b9537b4 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -11,7 +11,6 @@ open Util open Names open Glob_term -open Bigint (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "r_syntax_plugin" @@ -47,10 +46,10 @@ let pos_of_bignat ?loc x = let ref_xH = DAst.make @@ GRef (glob_xH, None) in let ref_xO = DAst.make @@ GRef (glob_xO, None) in let rec pos_of x = - match div2_with_rest x with - | (q,false) -> DAst.make @@ GApp (ref_xO,[pos_of q]) - | (q,true) when not (Bigint.equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q]) - | (q,true) -> ref_xH + match Z.(div_rem x (of_int 2)) with + | (q,rem) when rem = Z.zero -> DAst.make @@ GApp (ref_xO,[pos_of q]) + | (q,_) when not Z.(equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q]) + | (q,_) -> ref_xH in pos_of x @@ -59,9 +58,9 @@ let pos_of_bignat ?loc x = (**********************************************************************) let rec bignat_of_pos c = match DAst.get c with - | GApp (r, [a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a) - | GApp (r, [a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a)) - | GRef (a, _) when GlobRef.equal a glob_xH -> Bigint.one + | GApp (r, [a]) when is_gr r glob_xO -> Z.mul Z.(of_int 2) (bignat_of_pos a) + | GApp (r, [a]) when is_gr r glob_xI -> Z.add Z.one Z.(mul (of_int 2) (bignat_of_pos a)) + | GRef (a, _) when GlobRef.equal a glob_xH -> Z.one | _ -> raise Non_closed_number (**********************************************************************) @@ -77,9 +76,9 @@ let glob_POS = GlobRef.ConstructRef path_of_POS let glob_NEG = GlobRef.ConstructRef path_of_NEG let z_of_int ?loc n = - if not (Bigint.equal n zero) then + if not Z.(equal n zero) then let sgn, n = - if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in + if Z.(leq zero n) then glob_POS, n else glob_NEG, Z.neg n in DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n]) else DAst.make @@ GRef (glob_ZERO, None) @@ -90,8 +89,8 @@ let z_of_int ?loc n = let bigint_of_z c = match DAst.get c with | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a - | GApp (r,[a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a) - | GRef (a, _) when GlobRef.equal a glob_ZERO -> Bigint.zero + | GApp (r,[a]) when is_gr r glob_NEG -> Z.neg (bignat_of_pos a) + | GRef (a, _) when GlobRef.equal a glob_ZERO -> Z.zero | _ -> raise Non_closed_number (**********************************************************************) @@ -122,13 +121,13 @@ let r_of_rawnum ?loc n = let rdiv r r' = DAst.make @@ GApp (DAst.make @@ GRef(glob_Rdiv,None), [r; r']) in let pow p e = - let p = z_of_int ?loc (Bigint.of_int p) in + let p = z_of_int ?loc (Z.of_int p) in let e = pos_of_bignat e in DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [p; e]) in let n = izr (z_of_int ?loc n) in - if Bigint.is_strictly_pos e then rmult n (izr (pow p e)) - else if Bigint.is_strictly_neg e then rdiv n (izr (pow p (neg e))) + if Int.equal (Z.sign e) 1 then rmult n (izr (pow p e)) + else if Int.equal (Z.sign e) (-1) then rdiv n (izr (pow p (Z.neg e))) else n (* e = 0 *) (**********************************************************************) @@ -141,24 +140,24 @@ let rawnum_of_r c = (* choose between 123e-2 and 1.23, this is purely heuristic and doesn't play any soundness role *) let choose_exponent = - if Bigint.is_strictly_pos e then + if Int.equal (Z.sign e) 1 then true (* don't print 12 * 10^2 as 1200 to distinguish them *) else - let i = Bigint.to_string i in + let i = Z.to_string i in let li = if i.[0] = '-' then String.length i - 1 else String.length i in - let e = Bigint.neg e in - let le = String.length (Bigint.to_string e) in - Bigint.(less_than (add (of_int li) (of_int le)) e) in + let e = Z.neg e in + let le = String.length (Z.to_string e) in + Z.(lt (add (of_int li) (of_int le)) e) in (* print 123 * 10^-2 as 123e-2 *) let numTok_exponent () = NumTok.Signed.of_bigint_and_exponent i (NumTok.EDec e) in (* print 123 * 10^-2 as 1.23, precondition e < 0 *) let numTok_dot () = let s, i = - if Bigint.is_pos_or_zero i then NumTok.SPlus, Bigint.to_string i - else NumTok.SMinus, Bigint.(to_string (neg i)) in + if Z.sign i >= 0 then NumTok.SPlus, Z.to_string i + else NumTok.SMinus, Z.(to_string (neg i)) in let ni = String.length i in - let e = - (Bigint.to_int e) in + let e = - (Z.to_int e) in assert (e > 0); let i, f = if e < ni then String.sub i 0 (ni - e), String.sub i (ni - e) e @@ -178,12 +177,12 @@ let rawnum_of_r c = begin match DAst.get r with | GApp (p, [t; e]) when is_gr p glob_pow_pos -> let t = bigint_of_z t in - if not (Bigint.(equal t (of_int 10))) then + if not (Z.(equal t (of_int 10))) then raise Non_closed_number else let i = bigint_of_z l in let e = bignat_of_pos e in - let e = if is_gr md glob_Rdiv then neg e else e in + let e = if is_gr md glob_Rdiv then Z.neg e else e in numTok_of_int_exp i e | _ -> raise Non_closed_number end diff --git a/stm/stm.ml b/stm/stm.ml index c94a6d3a5d..9999e66c45 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1922,7 +1922,8 @@ end = struct (* {{{ *) str" solves the goal and leaves no unresolved existential variables. The following" ++ str" existentials remain unsolved: " ++ prlist (Termops.pr_existential_key sigma) (Evar.Set.elements evars)) end) () - with e when CErrors.noncritical e -> RespError (CErrors.print e) + with e when CErrors.noncritical e -> + RespError (CErrors.print e ++ spc() ++ str "(for subgoal "++int (fst r_ast) ++ str ")") let name_of_task { t_name } = t_name let name_of_request { r_name } = r_name diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 6b575d0807..83ae3ea09a 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -60,33 +60,39 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let name = name_op_to_name ~name_op ~name suffix in Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let current_sign = Global.named_context_val () - and global_sign = Proofview.Goal.hyps gl in - let sign,secsign = - List.fold_right - (fun d (s1,s2) -> - let id = NamedDecl.get_id d in - if mem_named_context_val id current_sign && - interpretable_as_section_decl env sigma (lookup_named_val id current_sign) d - then (s1,push_named_context_val d s2) - else (Context.Named.add d s1,s2)) - global_sign (Context.Named.empty, Environ.empty_named_context_val) in - let name = Namegen.next_global_ident_away name (pf_ids_set_of_hyps gl) in - let concl = match goal_type with - | None -> Proofview.Goal.concl gl - | Some ty -> ty in - let concl = it_mkNamedProd_or_LetIn concl sign in - let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in - let effs, sigma, lem, args, safe = - !declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl in - let solve = - Proofview.tclEFFECTS effs <*> - tacK lem args - in - let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let section_sign = Global.named_context_val () in + let goal_sign = Proofview.Goal.hyps gl in + let sign,secsign = + List.fold_right + (fun d (s1,s2) -> + let id = NamedDecl.get_id d in + if mem_named_context_val id section_sign && + interpretable_as_section_decl env sigma (lookup_named_val id section_sign) d + then (s1,push_named_context_val d s2) + else (Context.Named.add d s1,s2)) + goal_sign (Context.Named.empty, Environ.empty_named_context_val) + in + let name = Namegen.next_global_ident_away name (pf_ids_set_of_hyps gl) in + let concl = match goal_type with + | None -> Proofview.Goal.concl gl + | Some ty -> ty + in + let concl = it_mkNamedProd_or_LetIn concl sign in + let solve_tac = tclCOMPLETE + (Tactics.intros_mustbe_force (List.rev_map NamedDecl.get_id sign) <*> + tac) + in + let effs, sigma, lem, args, safe = + !declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl + in + let solve = + Proofview.tclEFFECTS effs <*> + tacK lem args + in + let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac end let abstract_subproof ~opaque tac = diff --git a/test-suite/bugs/closed/bug_12889.v b/test-suite/bugs/closed/bug_12889.v new file mode 100644 index 0000000000..f53cb8272d --- /dev/null +++ b/test-suite/bugs/closed/bug_12889.v @@ -0,0 +1,28 @@ +Require Import Relations. +Require Import Setoid. +Require Import Ring_theory. +Require Import Ring_base. + +Section S1. +Variable R : Type. +Variable Rone Rzero : R. +Variable Rplus Rmult Rminus : R -> R -> R. +Variable Rneg : R -> R. + +Lemma my_ring_theory1 : @ring_theory R Rzero Rone Rplus Rmult Rminus Rneg (@eq +R). +Admitted. +Add Ring my_ring : my_ring_theory1. +End S1. + +Section S2. +Variable R : Type. +Variable Rone Rzero : R. +Variable Rplus Rmult Rminus : R -> R -> R. +Variable Rneg : R -> R. + +Lemma my_ring_theory2 : @ring_theory R Rzero Rone Rplus Rmult Rminus Rneg (@eq +R). +Admitted. +Add Ring my_ring : my_ring_theory2. +End S2. diff --git a/test-suite/bugs/closed/bug_12928.v b/test-suite/bugs/closed/bug_12928.v new file mode 100644 index 0000000000..2f4d1dd16d --- /dev/null +++ b/test-suite/bugs/closed/bug_12928.v @@ -0,0 +1,7 @@ + +Lemma test: forall (x:bool) (x: nat), nat. +Proof. intros y x; abstract (exact x). Qed. + +Set Mangle Names. +Lemma test': forall x : nat, nat. +Proof. intros x. abstract exact x. Qed. diff --git a/test-suite/bugs/closed/bug_3146.v b/test-suite/bugs/closed/bug_3146.v new file mode 100644 index 0000000000..c42e28818a --- /dev/null +++ b/test-suite/bugs/closed/bug_3146.v @@ -0,0 +1,5 @@ +Axiom x : True. +Goal nat -> nat. + intro x. + abstract (exact x). +Qed. diff --git a/test-suite/bugs/closed/bug_5703.v b/test-suite/bugs/closed/bug_5703.v new file mode 100644 index 0000000000..c6e9eab9a7 --- /dev/null +++ b/test-suite/bugs/closed/bug_5703.v @@ -0,0 +1,9 @@ +Class A := {}. +Instance a:A := {}. +Hint Extern 0 A => abstract (exact a) : typeclass_instances. +Lemma lem : A. +Proof. + let a := constr:(_:A) in + let b := type of a in + exact a. +Defined. diff --git a/test-suite/output/Partac.out b/test-suite/output/Partac.out new file mode 100644 index 0000000000..889e698fa2 --- /dev/null +++ b/test-suite/output/Partac.out @@ -0,0 +1,6 @@ +The command has indeed failed with message: +The term "false" has type "bool" while it is expected to have type "nat". +(for subgoal 1) +The command has indeed failed with message: +The term "0" has type "nat" while it is expected to have type "bool". +(for subgoal 2) diff --git a/test-suite/output/Partac.v b/test-suite/output/Partac.v new file mode 100644 index 0000000000..f579ee683b --- /dev/null +++ b/test-suite/output/Partac.v @@ -0,0 +1,6 @@ +Goal nat * bool. +Proof. + split. + Fail par: exact false. + Fail par: exact 0. +Abort. diff --git a/test-suite/success/name_mangling.v b/test-suite/success/name_mangling.v index e982414206..d99e407b0d 100644 --- a/test-suite/success/name_mangling.v +++ b/test-suite/success/name_mangling.v @@ -1,7 +1,6 @@ -(* -*- coq-prog-args: ("-mangle-names" "_") -*- *) +Set Mangle Names. (* Check that refine policy of redefining previous names make these names private *) -(* abstract can change names in the environment! See bug #3146 *) Goal True -> True. intro. @@ -58,7 +57,7 @@ Abort. Goal False -> False. intro H. -Fail abstract exact H. +abstract exact H. Abort. (* Variant *) @@ -70,12 +69,11 @@ Abort. (* Example from Jason *) -Goal False -> False. +Lemma lem1 : False -> False. intro H. (* Name H' is from Ltac here, so it preserves the privacy *) (* But abstract messes everything up *) -Fail let H' := H in abstract exact H'. -let H' := H in exact H'. +let H' := H in abstract exact H'. Qed. (* Variant *) @@ -111,7 +109,7 @@ Goal forall b : False, b = b. Fail destruct b0. Abort. -Goal forall b : False, b = b. +Lemma lem2 : forall b : False, b = b. now destruct b. Qed. End foo. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 0086516785..02ababd928 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -104,7 +104,7 @@ BEFORE ?= AFTER ?= # FIXME this should be generated by Coq (modules already linked by Coq) -CAMLDONTLINK=num,str,unix,dynlink,threads +CAMLDONTLINK=str,unix,dynlink,threads,num,zarith # OCaml binaries CAMLC ?= "$(OCAMLFIND)" ocamlc -c diff --git a/toplevel/dune b/toplevel/dune index 2d64ae303c..5f10346ac4 100644 --- a/toplevel/dune +++ b/toplevel/dune @@ -3,8 +3,9 @@ (public_name coq.toplevel) (synopsis "Coq's Interactive Shell [terminal-based]") (wrapped false) + ; num still here due to some plugins using it (libraries num coq.stm)) -; Coqlevel provides the `Num` library to plugins, we could also use +; Interp provides the `zarith` library to plugins, we could also use ; -linkall in the plugins file, to be discussed. (coq.pp (modules g_toplevel)) |