diff options
137 files changed, 1213 insertions, 1568 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 51d39936d0..ca5584bcb5 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 @@ -803,7 +803,7 @@ library:ci-geocoq: library:ci-hott: extends: .ci-template -library:ci-lambda_rust: +library:ci-iris: extends: .ci-template-flambda library:ci-math_classes: 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/Makefile.ci b/Makefile.ci index 85e4b965f9..af78f252df 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -37,7 +37,7 @@ CI_TARGETS= \ ci-geocoq \ ci-coqhammer \ ci-hott \ - ci-lambda_rust \ + ci-iris \ ci-math_classes \ ci-mathcomp \ ci-metacoq \ 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/bench/gitlab-bench.yml b/dev/bench/gitlab-bench.yml index a2207081f4..4275e3d121 100644 --- a/dev/bench/gitlab-bench.yml +++ b/dev/bench/gitlab-bench.yml @@ -28,5 +28,10 @@ bench: paths: - _bench/html/**/*.v.html - _bench/logs + - _bench/files.listing + - _bench/opam.NEW/**/*.log + - _bench/opam.NEW/**/*.timing + - _bench/opam.OLD/**/*.log + - _bench/opam.OLD/**/*.timing when: always expire_in: 1 year diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh index 38b4e25bde..7625e4e7f7 100755 --- a/dev/bench/gitlab.sh +++ b/dev/bench/gitlab.sh @@ -12,6 +12,9 @@ r='\033[0m' # reset (all attributes off) b='\033[1m' # bold u='\033[4m' # underline nl=$'\n' +bt='`' # backtick +start_code_block='```' +end_code_block='```' number_of_processors=$(cat /proc/cpuinfo | grep '^processor *' | wc -l) @@ -36,6 +39,7 @@ echo $PWD #check_variable "BUILD_URL" #check_variable "JOB_NAME" #check_variable "JENKINS_URL" +check_variable "CI_JOB_URL" check_variable "coq_pr_number" check_variable "coq_pr_comment_id" check_variable "new_ocaml_switch" @@ -61,8 +65,9 @@ else exit 1 fi -mkdir -p "_bench" -working_dir="$PWD/_bench" +bench_dirname="_bench" +mkdir -p "${bench_dirname}" +working_dir="$PWD/${bench_dirname}" log_dir=$working_dir/logs mkdir "$log_dir" @@ -109,6 +114,15 @@ else exit 1 fi +if which du > /dev/null; then + : +else + echo > /dev/stderr + echo "ERROR: \"du\" program is not available." > /dev/stderr + echo > /dev/stderr + exit 1 +fi + if [ ! -e "$working_dir" ]; then echo > /dev/stderr echo "ERROR: \"$working_dir\" does not exist." > /dev/stderr @@ -146,22 +160,31 @@ function coqbot_update_comment() { if [ ! -z "${coq_pr_number}" ]; then comment_text="" + artifact_text="" if [ -z "${is_done}" ]; then comment_text="in progress, " + artifact_text="eventually " else comment_text="" + artifact_text="" fi - comment_text="Benchmarking ${comment_text}log available [here](${BUILD_URL}/console), workspace available [here](${JENKINS_URL}/view/benchmarking/job/${JOB_NAME}/ws/${BUILD_ID})" + comment_text="Benchmarking ${comment_text}log available [here](${CI_JOB_URL}) ([raw log here](${CI_JOB_URL}/raw)), artifacts ${artifact_text}available for [download](${CI_JOB_URL}/artifacts/download) and [browsing](${CI_JOB_URL}/artifacts/browse)" if [ ! -z "${comment_body}" ]; then - comment_text="${comment_text}${nl}"'```'"${nl}${comment_body}${nl}"'```' + comment_text="${comment_text}${nl}${start_code_block}${nl}${comment_body}${nl}${end_code_block}" fi if [ ! -z "${uninstallable_packages}" ]; then comment_text="${comment_text}${nl}The following packages failed to install: ${uninstallable_packages}" fi + comment_text="${comment_text}${nl}${nl}<details><summary>Old Coq version ${old_coq_commit}</summary>" + comment_text="${comment_text}${nl}${nl}${start_code_block}${nl}$(git log -n 1 "${old_coq_commit}")${nl}${end_code_block}${nl}</details>" + comment_text="${comment_text}${nl}${nl}<details><summary>New Coq version ${new_coq_commit}</summary>" + comment_text="${comment_text}${nl}${nl}${start_code_block}${nl}$(git log -n 1 "${new_coq_commit}")${nl}${end_code_block}${nl}</details>" + comment_text="${comment_text}${nl}${nl}[Diff: ${bt}${old_coq_commit}..${new_coq_commit}${bt}](https://github.com/coq/coq/compare/${old_coq_commit}..${new_coq_commit})" + # if there's a comment id, we update the comment while we're # in progress; otherwise, we wait until the end to post a new # comment @@ -416,6 +439,11 @@ for coq_opam_package in $sorted_coq_opam_packages; do done done +# Since we do not upload all files, store a list of the files +# available so that if we at some point want to tweak which files we +# upload, we'll know which ones are available for upload +du -ha "$working_dir" > "$working_dir/files.listing" + # The following directories in $working_dir are no longer used: # # - coq, opam.OLD, opam.NEW @@ -430,7 +458,7 @@ done # # The next script processes all these files and prints results in a table. -echo "INFO: workspace = https://ci.inria.fr/coq/view/benchmarking/job/$JOB_NAME/ws/$BUILD_ID" +echo "INFO: workspace = ${CI_JOB_URL}/artifacts/browse/${bench_dirname}" # Print the final results. if [ -z "$installable_coq_opam_packages" ]; then @@ -444,7 +472,7 @@ else rendered_results="$($program_path/render_results "$log_dir" $num_of_iterations $new_coq_commit_long $old_coq_commit_long 0 user_time_pdiff $installable_coq_opam_packages)" echo "${rendered_results}" - echo "INFO: per line timing: https://ci.inria.fr/coq/job/$JOB_NAME/ws/$BUILD_ID/html/" + echo "INFO: per line timing: ${CI_JOB_URL}/artifacts/browse/${bench_dirname}/html/" cd "$coq_dir" echo INFO: Old Coq version 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/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 2725e6b56c..75d9efaadc 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -62,9 +62,17 @@ : "${iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}" : "${iris_CI_ARCHIVEURL:=${iris_CI_GITURL}/-/archive}" -: "${lambda_rust_CI_REF:=master}" -: "${lambda_rust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}" -: "${lambda_rust_CI_ARCHIVEURL:=${lambda_rust_CI_GITURL}/-/archive}" +: "${autosubst_CI_REF:=coq86-devel}" +: "${autosubst_CI_GITURL:=https://github.com/RalfJung/autosubst}" +: "${autosubst_CI_ARCHIVEURL:=${autosubst_CI_GITURL}/archive}" + +: "${iris_string_ident_CI_REF:=master}" +: "${iris_string_ident_CI_GITURL:=https://gitlab.mpi-sws.org/iris/string-ident}" +: "${iris_string_ident_CI_ARCHIVEURL:=${iris_string_ident_CI_GITURL}/-/archive}" + +: "${iris_examples_CI_REF:=master}" +: "${iris_examples_CI_GITURL:=https://gitlab.mpi-sws.org/iris/examples}" +: "${iris_examples_CI_ARCHIVEURL:=${iris_examples_CI_GITURL}/-/archive}" ######################################################################## # HoTT diff --git a/dev/ci/ci-iris.sh b/dev/ci/ci-iris.sh new file mode 100755 index 0000000000..0256906112 --- /dev/null +++ b/dev/ci/ci-iris.sh @@ -0,0 +1,36 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +# Setup iris_examples and separate dependencies first +git_download autosubst +git_download iris_string_ident +git_download iris_examples + +# Extract required version of Iris (avoiding "+" which does not work on MacOS :( *) +iris_CI_REF=$(grep -F '"coq-iris"' < "${CI_BUILD_DIR}/iris_examples/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') + +# Setup Iris +git_download iris + +# Extract required version of std++ +stdpp_CI_REF=$(grep -F '"coq-stdpp"' < "${CI_BUILD_DIR}/iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') + +# Setup std++ +git_download stdpp + +# Build std++ +( cd "${CI_BUILD_DIR}/stdpp" && make && make install ) + +# Build and validate Iris +( cd "${CI_BUILD_DIR}/iris" && make && make validate && make install ) + +# Build autosubst +( cd "${CI_BUILD_DIR}/autosubst" && make && make install ) + +# Build iris-string-ident +( cd "${CI_BUILD_DIR}/iris_string_ident" && make && make install ) + +# Build Iris examples +( cd "${CI_BUILD_DIR}/iris_examples" && make && make install ) diff --git a/dev/ci/ci-lambda_rust.sh b/dev/ci/ci-lambda_rust.sh deleted file mode 100755 index 1ef0c2cb8f..0000000000 --- a/dev/ci/ci-lambda_rust.sh +++ /dev/null @@ -1,30 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -install_ssreflect - -# Setup lambda_rust first -git_download lambda_rust - -# Extract required version of Iris (avoiding "+" which does not work on MacOS :( *) -iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambda_rust/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') - -# Setup Iris -git_download iris - -# Extract required version of std++ -stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') - -# Setup std++ -git_download stdpp - -# Build std++ -( cd "${CI_BUILD_DIR}/stdpp" && make && make install ) - -# Build and validate Iris -( cd "${CI_BUILD_DIR}/iris" && make && make validate && make install ) - -# Build lambda_rust -( cd "${CI_BUILD_DIR}/lambda_rust" && make && make install ) 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/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh b/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh new file mode 100644 index 0000000000..bb08c13ef3 --- /dev/null +++ b/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12875" ] || [ "$CI_BRANCH" = "master+about-print-all-arguments-names" ]; then + + elpi_CI_REF=coq-master+adapt-coq12875-arguments-pass-name-impargs + elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + +fi diff --git a/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh b/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh new file mode 100644 index 0000000000..f0878202d3 --- /dev/null +++ b/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "12892" ] || [ "$CI_BRANCH" = "update-s-univs" ]; then + + elpi_CI_REF=update-s-univs + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + + equations_CI_REF=update-s-univs + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh b/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh new file mode 100644 index 0000000000..ee75944a52 --- /dev/null +++ b/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12968" ] || [ "$CI_BRANCH" = "delay-frozen-evarconv" ]; then + + equations_CI_REF=delay-frozen-evarconv + equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations + +fi diff --git a/dev/core.dbg b/dev/core.dbg index ec946e2df0..6d52bae773 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -1,5 +1,6 @@ load_printer threads.cma load_printer str.cma +load_printer zarith.cma load_printer config.cma load_printer clib.cma load_printer dynlink.cma diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg index 4e1035f7b6..3f73cf126a 100644 --- a/dev/core_dune.dbg +++ b/dev/core_dune.dbg @@ -1,5 +1,6 @@ load_printer threads.cma load_printer str.cma +load_printer zarith.cma load_printer config.cma load_printer clib.cma load_printer dynlink.cma diff --git a/dev/dune_db_408 b/dev/dune_db_408 index 3bf13da62d..5f826fe383 100644 --- a/dev/dune_db_408 +++ b/dev/dune_db_408 @@ -1,5 +1,6 @@ load_printer threads.cma load_printer str.cma +load_printer zarith.cma load_printer config.cma load_printer clib.cma load_printer dynlink.cma diff --git a/dev/dune_db_409 b/dev/dune_db_409 index 1267fd5393..2e58272c75 100644 --- a/dev/dune_db_409 +++ b/dev/dune_db_409 @@ -1,5 +1,6 @@ load_printer threads.cma load_printer str.cma +load_printer zarith.cma load_printer config.cma load_printer clib.cma load_printer lib.cma diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index a11269e059..91cb6168e1 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -34,4 +34,5 @@ exec $OCAMLDEBUG \ -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ -I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \ -I $COQTOP/ide \ + $(ocamlfind query -recursive -i-format zarith) \ "$@" 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/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index c01e6a5aa6..070e899c9d 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -159,7 +159,7 @@ High level view of `lia` Over :math:`\mathbb{R}`, *positivstellensatz* refutations are a complete proof principle [#mayfail]_. However, this is not the case over :math:`\mathbb{Z}`. Actually, *positivstellensatz* refutations are not even sufficient to decide -linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 -> \mathtt{False}` +linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 \to \mathtt{False}` which is a theorem of :math:`\mathbb{Z}` but not a theorem of :math:`{\mathbb{R}}`. To remedy this weakness, the :tacn:`lia` tactic is using recursively a combination of: @@ -180,7 +180,7 @@ are a way to take into account the discreteness of :math:`\mathbb{Z}` by roundin Let :math:`p` be an integer and :math:`c` a rational constant. Then :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. -For instance, from 2 x = 1 we can deduce +For instance, from :math:`2 x = 1` we can deduce + :math:`x \ge 1/2` whose cut plane is :math:`x \ge \lceil{1/2}\rceil = 1`; + :math:`x \le 1/2` whose cut plane is :math:`x \le \lfloor{1/2}\rfloor = 0`. diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index 34752a4c4d..182f599a29 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -880,10 +880,10 @@ Here is a summary of the error messages corresponding to each situation: .. exn:: The constructor @ident expects @num arguments. + The variable ident is bound several times in pattern term + Found a constructor of inductive type term while a constructor of term is expected - The variable ident is bound several times in pattern termFound a constructor - of inductive type term while a constructor of term is expectedPatterns are - incorrect (because constructors are not applied to the correct number of the + Patterns are incorrect (because constructors are not applied to the correct number of arguments, because they are not linear or they are wrongly typed). .. exn:: Non exhaustive pattern matching. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index e7ba82fb31..d8b2af092f 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -375,8 +375,14 @@ behavior.) | ! | par - Applies :token:`ltac_expr` to the selected goals. It can only be used at the top - level of a tactic expression; it cannot be used within a tactic expression. + Reorders the goals and applies :token:`ltac_expr` to the selected goals. It can + only be used at the top level of a tactic expression; it cannot be used within a + tactic expression. The selected goals are reordered so they appear after the + lowest-numbered selected goal, ordered by goal number. :ref:`Example + <reordering_goals_ex>`. If the selector applies + to a single goal or to all goals, the reordering will not be apparent. The order of + the goals in the :token:`selector` is irrelevant. (This may not be what you expect; + see `#8481 <https://github.com/coq/coq/issues/8481>`_.) .. todo why shouldn't "all" and "!" be accepted anywhere a @selector is accepted? It would be simpler to explain. @@ -430,6 +436,19 @@ Selectors can also be used nested within a tactic expression with the :name: No such goal. (Goal selector) :undocumented: +.. _reordering_goals_ex: + +.. example:: Selector reordering goals + + .. coqtop:: reset in + + Goal 1=0 /\ 2=0 /\ 3=0. + + .. coqtop:: all + + repeat split. + 1,3: idtac. + .. TODO change error message index entry diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index f3dc9a6cb1..72c6ec4ac5 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -54,7 +54,7 @@ Invocation of tactics ~~~~~~~~~~~~~~~~~~~~~ A tactic is applied as an ordinary command. It may be preceded by a -goal selector (see Section :ref:`ltac-semantics`). If no selector is +goal selector (see Section :ref:`goal-selectors`). If no selector is specified, the default selector is used. .. _tactic_invocation_grammar: @@ -4751,9 +4751,13 @@ Non-logical tactics .. tacn:: cycle @num :name: cycle - This tactic puts the :n:`@num` first goals at the end of the list of goals. - If :n:`@num` is negative, it will put the last :math:`|num|` goals at the + Reorders the selected goals so that the first :n:`@num` goals appear after the + other selected goals. + If :n:`@num` is negative, it puts the last :n:`@num` goals at the beginning of the list. + The tactic is only useful with a goal selector, most commonly `all:`. + Note that other selectors reorder goals; `1,3: cycle 1` is not equivalent + to `all: cycle 1`. See :tacn:`… : … (goal selector)`. .. example:: @@ -4771,10 +4775,12 @@ Non-logical tactics .. tacn:: swap @num @num :name: swap - This tactic switches the position of the goals of indices :n:`@num` and - :n:`@num`. Negative values for:n:`@num` indicate counting goals - backward from the end of the focused goal list. Goals are indexed from 1, - there is no goal with position 0. + Exchanges the position of the specified goals. + Negative values for :n:`@num` indicate counting goals + backward from the end of the list of selected goals. Goals are indexed from 1. + The tactic is only useful with a goal selector, most commonly `all:`. + Note that other selectors reorder goals; `1,3: swap 1 3` is not equivalent + to `all: swap 1 3`. See :tacn:`… : … (goal selector)`. .. example:: @@ -4788,7 +4794,9 @@ Non-logical tactics .. tacn:: revgoals :name: revgoals - This tactics reverses the list of the focused goals. + Reverses the order of the selected goals. The tactic is only useful with a goal + selector, most commonly `all :`. Note that other selectors reorder goals; + `1,3: revgoals` is not equivalent to `all: revgoals`. See :tacn:`… : … (goal selector)`. .. example:: diff --git a/engine/evd.ml b/engine/evd.ml index 62a818ee6f..65df2643f2 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -468,7 +468,6 @@ module FutureGoals : sig type t = private { comb : Evar.t list; - shelf : Evar.t list; principal : Evar.t option; (** if [Some e], [e] must be contained in [comb]. The evar @@ -492,18 +491,17 @@ module FutureGoals : sig val push : stack -> stack val pop : stack -> t * stack - val add : shelve:bool -> principal:bool -> Evar.t -> stack -> stack + val add : principal:bool -> Evar.t -> stack -> stack val remove : Evar.t -> stack -> stack val fold : ('a -> Evar.t -> 'a) -> 'a -> stack -> 'a - val put_shelf : Evar.t list -> stack -> stack + val pr_stack : stack -> Pp.t end = struct type t = { comb : Evar.t list; - shelf : Evar.t list; principal : Evar.t option; (** if [Some e], [e] must be contained in [comb]. The evar @@ -521,12 +519,9 @@ end = struct | hd :: tl -> f hd :: tl - let add ~shelve ~principal evk stack = + let add ~principal evk stack = let add fgl = - let (comb,shelf) = - if shelve then (fgl.comb,evk::fgl.shelf) - else (evk::fgl.comb,fgl.shelf) - in + let comb = evk :: fgl.comb in let principal = if principal then match fgl.principal with @@ -534,7 +529,7 @@ end = struct | None -> Some evk else fgl.principal in - { comb; shelf; principal } + { comb; principal } in set add stack @@ -543,15 +538,13 @@ end = struct let filter e' = not (Evar.equal e e') in let principal = Option.filter filter fgl.principal in let comb = List.filter filter fgl.comb in - let shelf = List.filter filter fgl.shelf in - { principal; comb; shelf } + { principal; comb } in List.map remove stack let empty = { principal = None; comb = []; - shelf = []; } let empty_stack = [empty] @@ -566,31 +559,29 @@ end = struct let fold f acc stack = let future_goals = List.hd stack in - let future_goals = future_goals.comb @ future_goals.shelf in - List.fold_left f acc future_goals + List.fold_left f acc future_goals.comb let filter f fgl = let comb = List.filter f fgl.comb in - let shelf = List.filter f fgl.shelf in let principal = Option.filter f fgl.principal in - { comb; shelf; principal } + { comb; principal } let map_filter f fgl = let comb = List.map_filter f fgl.comb in - let shelf = List.map_filter f fgl.shelf in let principal = Option.bind fgl.principal f in - { comb; shelf; principal } + { comb; principal } - let put_shelf shelved stack = - match stack with - | [] -> anomaly Pp.(str"future_goals stack should not be empty") - | hd :: tl -> - let shelf = shelved @ hd.shelf in - { hd with shelf } :: tl + let pr_stack stack = + let open Pp in + let pr_future_goals fgl = + prlist_with_sep spc Evar.print fgl.comb ++ + pr_opt (fun ev -> str"(principal: " ++ Evar.print ev ++ str")") fgl.principal + in + if List.is_empty stack then str"(empty stack)" + else prlist_with_sep (fun () -> str"||") pr_future_goals stack end - type evar_map = { (* Existential variables *) defn_evars : evar_info EvMap.t; @@ -609,6 +600,7 @@ type evar_map = { future_goals : FutureGoals.stack; (** list of newly created evars, to be eventually turned into goals if not solved.*) given_up : Evar.Set.t; + shelf : Evar.t list list; extras : Store.t; } @@ -837,6 +829,7 @@ let empty = { evar_names = EvNames.empty; (* id<->key for undefined evars *) future_goals = FutureGoals.empty_stack; given_up = Evar.Set.empty; + shelf = [[]]; extras = Store.empty; } @@ -848,6 +841,8 @@ let has_undefined evd = not (EvMap.is_empty evd.undf_evars) let has_given_up evd = not (Evar.Set.is_empty evd.given_up) +let has_shelved evd = not (List.for_all List.is_empty evd.shelf) + let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d = let conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs in let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in @@ -1149,8 +1144,8 @@ let universe_binders evd = UState.universe_binders evd.universes let universes evd = UState.ugraph evd.universes -let update_sigma_env evd env = - { evd with universes = UState.update_sigma_env evd.universes env } +let update_sigma_univs ugraph evd = + { evd with universes = UState.update_sigma_univs evd.universes ugraph } exception UniversesDiffer = UState.UniversesDiffer @@ -1172,12 +1167,12 @@ let drop_side_effects evd = let eval_side_effects evd = evd.effects (* Future goals *) -let declare_future_goal ?(shelve=false) evk evd = - let future_goals = FutureGoals.add ~shelve ~principal:false evk evd.future_goals in +let declare_future_goal evk evd = + let future_goals = FutureGoals.add ~principal:false evk evd.future_goals in { evd with future_goals } -let declare_principal_goal ?(shelve=false) evk evd = - let future_goals = FutureGoals.add ~shelve ~principal:true evk evd.future_goals in +let declare_principal_goal evk evd = + let future_goals = FutureGoals.add ~principal:true evk evd.future_goals in { evd with future_goals } let push_future_goals evd = @@ -1190,18 +1185,45 @@ let pop_future_goals evd = let fold_future_goals f sigma = FutureGoals.fold f sigma sigma.future_goals -let shelve_on_future_goals shelved evd = - let future_goals = FutureGoals.put_shelf shelved evd.future_goals in - { evd with future_goals } - let remove_future_goal evd evk = { evd with future_goals = FutureGoals.remove evk evd.future_goals } +let pr_future_goals_stack evd = + FutureGoals.pr_stack evd.future_goals + let give_up ev evd = { evd with given_up = Evar.Set.add ev evd.given_up } +let push_shelf evd = + { evd with shelf = [] :: evd.shelf } + +let pop_shelf evd = + match evd.shelf with + | [] -> anomaly Pp.(str"shelf stack should not be empty") + | hd :: tl -> + hd, { evd with shelf = tl } + +let filter_shelf f evd = + { evd with shelf = List.map (List.filter f) evd.shelf } + +let shelve evd l = + match evd.shelf with + | [] -> anomaly Pp.(str"shelf stack should not be empty") + | hd :: tl -> + { evd with shelf = (hd@l) :: tl } + +let unshelve evd l = + { evd with shelf = List.map (List.filter (fun ev -> not (CList.mem_f Evar.equal ev l))) evd.shelf } + let given_up evd = evd.given_up +let shelf evd = List.flatten evd.shelf + +let pr_shelf evd = + let open Pp in + if List.is_empty evd.shelf then str"(empty stack)" + else prlist_with_sep (fun () -> str"||") (prlist_with_sep spc Evar.print) evd.shelf + (**********************************************************) (* Accessing metas *) @@ -1219,6 +1241,7 @@ let set_metas evd metas = { evar_names = evd.evar_names; future_goals = evd.future_goals; given_up = evd.given_up; + shelf = evd.shelf; extras = evd.extras; } diff --git a/engine/evd.mli b/engine/evd.mli index db5265ca0a..9394f9a9dd 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -171,6 +171,10 @@ val has_given_up : evar_map -> bool (** [has_given_up sigma] is [true] if and only if there are given up evars in [sigma]. *) +val has_shelved : evar_map -> bool +(** [has_shelved sigma] is [true] if and only if + there are shelved evars in [sigma]. *) + val new_evar : evar_map -> ?name:Id.t -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t (** Creates a fresh evar mapping to the given information. *) @@ -347,11 +351,11 @@ val drop_side_effects : evar_map -> evar_map (** {5 Future goals} *) -val declare_future_goal : ?shelve:bool -> Evar.t -> evar_map -> evar_map +val declare_future_goal : Evar.t -> evar_map -> evar_map (** Adds an existential variable to the list of future goals. For internal uses only. *) -val declare_principal_goal : ?shelve:bool -> Evar.t -> evar_map -> evar_map +val declare_principal_goal : Evar.t -> evar_map -> evar_map (** Adds an existential variable to the list of future goals and make it principal. Only one existential variable can be made principal, an error is raised otherwise. For internal uses only. *) @@ -360,7 +364,6 @@ module FutureGoals : sig type t = private { comb : Evar.t list; - shelf : Evar.t list; principal : Evar.t option; (** if [Some e], [e] must be contained in [future_comb]. The evar @@ -385,17 +388,29 @@ val pop_future_goals : evar_map -> FutureGoals.t * evar_map val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map -(** Fold future goals *) - -val shelve_on_future_goals : Evar.t list -> evar_map -> evar_map -(** Push goals on the shelve of future goals *) val remove_future_goal : evar_map -> Evar.t -> evar_map +val pr_future_goals_stack : evar_map -> Pp.t + +val push_shelf : evar_map -> evar_map + +val pop_shelf : evar_map -> Evar.t list * evar_map + +val filter_shelf : (Evar.t -> bool) -> evar_map -> evar_map + val give_up : Evar.t -> evar_map -> evar_map +val shelve : evar_map -> Evar.t list -> evar_map + +val unshelve : evar_map -> Evar.t list -> evar_map + val given_up : evar_map -> Evar.Set.t +val shelf : evar_map -> Evar.t list + +val pr_shelf : evar_map -> Pp.t + (** {5 Sort variables} Evar maps also keep track of the universe constraints defined at a given @@ -658,7 +673,8 @@ val fix_undefined_variables : evar_map -> evar_map (** Universe minimization *) val minimize_universes : evar_map -> evar_map -val update_sigma_env : evar_map -> env -> evar_map +(** Lift [UState.update_sigma_univs] *) +val update_sigma_univs : UGraph.t -> evar_map -> evar_map (** Polymorphic universes *) diff --git a/engine/namegen.ml b/engine/namegen.ml index fb9f6db0ea..f398f29f41 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -273,8 +273,8 @@ let visible_ids sigma (nenv, c) = accu := (gseen, vseen, ids) | Rel p -> let (gseen, vseen, ids) = !accu in - if p > n && not (Int.Set.mem p vseen) then - let vseen = Int.Set.add p vseen in + if p > n && not (Int.Set.mem (p - n) vseen) then + let vseen = Int.Set.add (p - n) vseen in let name = try Some (List.nth nenv (p - n - 1)) with Invalid_argument _ | Failure _ -> @@ -290,7 +290,7 @@ let visible_ids sigma (nenv, c) = accu := (gseen, vseen, ids) | _ -> EConstr.iter_with_binders sigma succ visible_ids n c in - let () = visible_ids 1 c in + let () = visible_ids 1 c in (* n = 1 to count the binder to rename *) let (_, _, ids) = !accu in ids @@ -416,6 +416,8 @@ let next_name_away_for_default_printing sigma env_t na avoid = *) type renaming_flags = + (* The term is the body of a binder and the environment excludes this binder *) + (* so, there is a missing binder in the environment *) | RenamingForCasesPattern of (Name.t list * constr) | RenamingForGoal | RenamingElsewhereFor of (Name.t list * constr) diff --git a/engine/proofview.ml b/engine/proofview.ml index 2fc5ade0d2..978088872c 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -69,13 +69,13 @@ let dependent_init = let src = Loc.tag @@ Evar_kinds.GoalEvar in (* Main routine *) let rec aux = function - | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } + | TNil sigma -> [], { solution = sigma; comb = [] } | TCons (env, sigma, typ, t) -> let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~typeclass_candidate:false typ in let (gl, _) = EConstr.destEvar sigma econstr in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let entry = (econstr, typ) :: ret in - entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] } + entry, { solution = sol; comb = with_empty_state gl :: comb } in fun t -> let t = map_telescope_evd Evd.push_future_goals t in @@ -235,8 +235,6 @@ let apply ~name ~poly env t sp = match ans with | Nil (e, info) -> Exninfo.iraise (TacticFailure e, info) | Cons ((r, (state, _), status, info), _) -> - let status = (status, state.shelf) in - let state = { state with shelf = [] } in r, state, status, Trace.to_tree info @@ -621,7 +619,8 @@ let shelve = Comb.get >>= fun initial -> Comb.set [] >> InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve")) >> - Shelf.modify (fun gls -> gls @ CList.map drop_state initial) + let initial = CList.map drop_state initial in + Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution initial }) let shelve_goals l = let open Proof in @@ -629,7 +628,7 @@ let shelve_goals l = let comb = CList.filter (fun g -> not (CList.mem (drop_state g) l)) initial in Comb.set comb >> InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve_goals")) >> - Shelf.modify (fun gls -> gls @ l) + Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution l }) (** [depends_on sigma src tgt] checks whether the goal [src] appears as an existential variable in the definition of the goal [tgt] in @@ -696,7 +695,7 @@ let shelve_unifiable_informative = Comb.set n >> InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve_unifiable")) >> let u = CList.map drop_state u in - Shelf.modify (fun gls -> gls @ u) >> + Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution u }) >> tclUNIT u let shelve_unifiable = @@ -716,13 +715,17 @@ let guard_no_unifiable = let l = CList.map (fun id -> Names.Name id) l in tclUNIT (Some l) -(** [unshelve l p] adds all the goals in [l] at the end of the focused - goals of p *) +(** [unshelve l p] moves all the goals in [l] from the shelf and put them at + the end of the focused goals of p, if they are still undefined after [advance] *) let unshelve l p = + let solution = Evd.unshelve p.solution l in let l = List.map with_empty_state l in (* advance the goals in case of clear *) let l = undefined p.solution l in - { p with comb = p.comb@l } + { comb = p.comb@l; solution } + +let filter_shelf f pv = + { pv with solution = Evd.filter_shelf f pv.solution } let mark_in_evm ~goal evd evars = let evd = @@ -750,19 +753,20 @@ let mark_in_evm ~goal evd evars = let with_shelf tac = let open Proof in Pv.get >>= fun pv -> - let { shelf; solution } = pv in - Pv.set { pv with shelf = []; solution = Evd.push_future_goals solution } >> + let { solution } = pv in + Pv.set { pv with solution = Evd.push_shelf @@ Evd.push_future_goals solution } >> tac >>= fun ans -> Pv.get >>= fun npv -> - let { shelf = gls; solution = sigma } = npv in + let { solution = sigma } = npv in + let gls, sigma = Evd.pop_shelf sigma in (* The pending future goals are necessarily coming from V82.tactic *) (* and thus considered as to shelve, as in Proof.run_tactic *) let fgl, sigma = Evd.pop_future_goals sigma in (* Ensure we mark and return only unsolved goals *) - let gls' = CList.rev_append fgl.Evd.FutureGoals.shelf (CList.rev_append fgl.Evd.FutureGoals.comb gls) in + let gls' = CList.rev_append fgl.Evd.FutureGoals.comb gls in let gls' = undefined_evars sigma gls' in let sigma = mark_in_evm ~goal:false sigma gls' in - let npv = { npv with shelf; solution = sigma } in + let npv = { npv with solution = sigma } in Pv.set npv >> tclUNIT (gls', ans) (** [goodmod p m] computes the representative of [p] modulo [m] in the @@ -993,6 +997,8 @@ let tclProofInfo = module Unsafe = struct + let (>>=) = tclBIND + let tclEVARS evd = Pv.modify (fun ps -> { ps with solution = evd }) @@ -1002,21 +1008,22 @@ module Unsafe = struct { step with comb = step.comb @ gls } end + let tclNEWSHELVED gls = + Pv.modify begin fun step -> + let gls = undefined_evars step.solution gls in + { step with solution = Evd.shelve step.solution gls } + end + + let tclGETSHELF = tclEVARMAP >>= fun sigma -> tclUNIT @@ Evd.shelf sigma + let tclSETENV = Env.set let tclGETGOALS = Comb.get let tclSETGOALS = Comb.set - let tclGETSHELF = Shelf.get - - let tclSETSHELF = Shelf.set - - let tclPUTSHELF to_shelve = - tclBIND tclGETSHELF (fun shelf -> tclSETSHELF (to_shelve@shelf)) - let tclEVARSADVANCE evd = - Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb }) + Pv.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb }) let tclEVARUNIVCONTEXT ctx = Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) @@ -1037,8 +1044,8 @@ module Unsafe = struct let mark_as_unresolvables p evs = { p with solution = mark_in_evm ~goal:false p.solution evs } - let update_sigma_env pv env = - { pv with solution = Evd.update_sigma_env pv.solution env } + let update_sigma_univs ugraph pv = + { pv with solution = Evd.update_sigma_univs ugraph pv.solution } end @@ -1226,7 +1233,7 @@ module V82 = struct let sgs = CList.flatten goalss in let sgs = undefined evd sgs in InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"<unknown>")) >> - Pv.set { ps with solution = evd; comb = sgs; } + Pv.set { solution = evd; comb = sgs; } with e when catchable_exception e -> let (e, info) = Exninfo.capture e in tclZERO ~info e @@ -1266,7 +1273,7 @@ module V82 = struct let of_tactic t gls = try let env = Global.env () in - let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in + let init = { solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in let name, poly = Names.Id.of_string "legacy_pe", false in let (_,final,_,_) = apply ~name ~poly (goal_env env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = CList.map drop_state final.comb } diff --git a/engine/proofview.mli b/engine/proofview.mli index 8853013a84..816b45984b 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -162,7 +162,7 @@ val apply -> 'a tactic -> proofview -> 'a * proofview - * (bool*Evar.t list) + * bool * Proofview_monad.Info.tree (** {7 Monadic primitives} *) @@ -331,17 +331,16 @@ val unifiable : Evd.evar_map -> Evar.t -> Evar.t list -> bool considered). *) val shelve_unifiable : unit tactic -(** Idem but also returns the list of shelved variables *) -val shelve_unifiable_informative : Evar.t list tactic - (** [guard_no_unifiable] returns the list of unifiable goals if some goals are unifiable (see {!shelve_unifiable}) in the current focus. *) val guard_no_unifiable : Names.Name.t list option tactic -(** [unshelve l p] adds all the goals in [l] at the end of the focused - goals of p *) +(** [unshelve l p] moves all the goals in [l] from the shelf and put them at + the end of the focused goals of p, if they are still undefined after [advance] *) val unshelve : Evar.t list -> proofview -> proofview +val filter_shelf : (Evar.t -> bool) -> proofview -> proofview + (** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *) val depends_on : Evd.evar_map -> Evar.t -> Evar.t -> bool @@ -454,6 +453,10 @@ module Unsafe : sig goal is already solved, it is not added. *) val tclNEWGOALS : Proofview_monad.goal_with_state list -> unit tactic + (** [tclNEWSHELVED gls] adds the goals [gls] to the shelf. If a + goal is already solved, it is not added. *) + val tclNEWSHELVED : Evar.t list -> unit tactic + (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a goal is already solved, it is not set. *) val tclSETGOALS : Proofview_monad.goal_with_state list -> unit tactic @@ -461,15 +464,9 @@ module Unsafe : sig (** [tclGETGOALS] returns the list of goals under focus. *) val tclGETGOALS : Proofview_monad.goal_with_state list tactic - (** [tclSETSHELF gls] sets goals [gls] as the current shelf. *) - val tclSETSHELF : Evar.t list -> unit tactic - (** [tclGETSHELF] returns the list of goals on the shelf. *) val tclGETSHELF : Evar.t list tactic - (** [tclPUTSHELF] appends goals to the shelf. *) - val tclPUTSHELF : Evar.t list -> unit tactic - (** Sets the evar universe context. *) val tclEVARUNIVCONTEXT : UState.t -> unit tactic @@ -500,8 +497,8 @@ module Unsafe : sig val undefined : Evd.evar_map -> Proofview_monad.goal_with_state list -> Proofview_monad.goal_with_state list - (** [update_sigma_env] lifts [Evd.update_sigma_env] to the proofview *) - val update_sigma_env : proofview -> Environ.env -> proofview + (** [update_sigma_univs] lifts [UState.update_sigma_univs] to the proofview *) + val update_sigma_univs : UGraph.t -> proofview -> proofview end diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index 4b3dd8f633..df9fc5dab3 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -166,7 +166,6 @@ let map_goal_with_state f (g, s) = (f g, s) type proofview = { solution : Evd.evar_map; comb : goal_with_state list; - shelf : goal list; } (** {6 Instantiation of the logic monad} *) @@ -238,14 +237,6 @@ module Status : Writer with type t := bool = struct let put s = Logical.put s end -module Shelf : State with type t = goal list = struct - (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *) - type t = goal list - let get = Logical.map (fun {shelf} -> shelf) Pv.get - let set c = Pv.modify (fun pv -> { pv with shelf = c }) - let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf }) -end - (** Lens and utilities pertaining to the info trace *) module InfoL = struct let recording = Logical.(map (fun {P.trace} -> trace) current) diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index af866528c8..6cca3f5a5e 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -83,7 +83,6 @@ val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state type proofview = { solution : Evd.evar_map; comb : goal_with_state list; - shelf : goal list; } (** {6 Instantiation of the logic monad} *) @@ -137,10 +136,6 @@ module Env : State with type t := Environ.env (** Lens to the tactic status ([true] if safe, [false] if unsafe) *) module Status : Writer with type t := bool -(** Lens to the list of goals which have been shelved during the - execution of the tactic. *) -module Shelf : State with type t = goal list - (** Lens and utilities pertaining to the info trace *) module InfoL : sig (** [record_trace t] behaves like [t] and compute its [info] trace. *) diff --git a/engine/termops.ml b/engine/termops.ml index e5231ef9cd..ac6870a39e 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -301,8 +301,12 @@ let pr_evar_map_gen with_univs pr_evars env sigma = if List.is_empty (Evd.meta_list sigma) then mt () else str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma + and shelf = + str "SHELF:" ++ brk (0, 1) ++ Evd.pr_shelf sigma ++ fnl () + and future_goals = + str "FUTURE GOALS STACK:" ++ brk (0, 1) ++ Evd.pr_future_goals_stack sigma ++ fnl () in - evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas + evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas ++ shelf ++ future_goals let pr_evar_list env sigma l = let open Evd in diff --git a/engine/uState.ml b/engine/uState.ml index ca0a21acf7..8d1584cd95 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -568,8 +568,8 @@ let emit_side_effects eff u = let u = demote_seff_univs (fst uctx) u in merge_seff u uctx -let update_sigma_env uctx env = - let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul()) (Environ.universes env) in +let update_sigma_univs uctx ugraph = + let univs = UGraph.set_cumulative_sprop (elaboration_sprop_cumul()) ugraph in let eunivs = { uctx with initial_universes = univs; diff --git a/engine/uState.mli b/engine/uState.mli index 607c6c9452..7fec03e3b2 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -185,7 +185,7 @@ val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t (** {5 TODO: Document me} *) -val update_sigma_env : t -> Environ.env -> t +val update_sigma_univs : t -> UGraph.t -> t (** {5 Pretty-printing} *) diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 751bddc7c4..ad21f663e4 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -220,11 +220,11 @@ let process_goal_diffs diff_goal_map oldp nsigma ng = let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng } -let export_pre_goals Proof.{ sigma; goals; stack; shelf } process = +let export_pre_goals Proof.{ sigma; goals; stack } process = let process = List.map (process sigma) in { Interface.fg_goals = process goals ; Interface.bg_goals = List.(map (fun (lg,rg) -> process lg, process rg)) stack - ; Interface.shelved_goals = process shelf + ; Interface.shelved_goals = process @@ Evd.shelf sigma ; Interface.given_up_goals = process (Evar.Set.elements @@ Evd.given_up sigma) } 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/impargs.ml b/interp/impargs.ml index 48961c6c8a..7742f985de 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -667,10 +667,12 @@ let explicit_kind i = function let compute_implicit_statuses autoimps l = let rec aux i = function - | _ :: autoimps, Explicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps) - | na :: autoimps, MaxImplicit :: manualimps -> + | _ :: autoimps, (_, Explicit) :: manualimps -> None :: aux (i+1) (autoimps, manualimps) + | na :: autoimps, (Anonymous, MaxImplicit) :: manualimps + | _ :: autoimps, (na, MaxImplicit) :: manualimps -> Some (explicit_kind i na, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps) - | na :: autoimps, NonMaxImplicit :: manualimps -> + | na :: autoimps, (Anonymous, NonMaxImplicit) :: manualimps + | _ :: autoimps, (na, NonMaxImplicit) :: manualimps -> let imps' = aux (i+1) (autoimps, manualimps) in let max = set_maximality Error na i imps' false in Some (explicit_kind i na, Manual, (max, true)) :: imps' @@ -693,7 +695,7 @@ let set_implicits local ref l = check_rigidity (is_rigid env sigma t); (* Sort by number of implicits, decreasing *) let is_implicit = function - | Explicit -> false + | _, Explicit -> false | _ -> true in let l = List.map (fun imps -> (imps,List.count is_implicit imps)) l in let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in diff --git a/interp/impargs.mli b/interp/impargs.mli index 97841b37f2..c8bcef19c8 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -117,7 +117,7 @@ val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool -> (** [set_implicits local ref l] Manual declaration of implicit arguments. `l` is a list of possible sequences of implicit statuses. *) -val set_implicits : bool -> GlobRef.t -> Glob_term.binding_kind list list -> unit +val set_implicits : bool -> GlobRef.t -> (Name.t * Glob_term.binding_kind) list list -> unit val implicits_of_global : GlobRef.t -> implicits_list list 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/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8b85072d6d..da77a2882e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -936,12 +936,14 @@ let add_private_constant l decl senv : (Constant.t * private_constants) * safe_e | DefinitionEff ce -> Term_typing.translate_constant senv.env kn (Entries.DefinitionEntry ce) in - let senv, dcb = match cb.const_body with - | Def _ as const_body -> senv, { cb with const_body } - | OpaqueDef c -> - let local = empty_private cb.const_universes in - let senv, o = push_opaque_proof (Future.from_val (c, local)) senv in - senv, { cb with const_body = OpaqueDef o } + let dcb = match cb.const_body with + | Def _ as const_body -> { cb with const_body } + | OpaqueDef _ -> + (* We drop the body, to save the definition of an opaque and thus its + hashconsing. It does not matter since this only happens inside a proof, + and depending of the opaque status of the latter, this proof term will be + either inlined or reexported. *) + { cb with const_body = Undef None } | Undef _ | Primitive _ -> assert false in let senv = add_constant_aux senv (kn, dcb) in diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 927db9e9e6..52e93a9e22 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -142,6 +142,12 @@ let enforce_leq_alg u v g = | Inl x -> x | Inr e -> raise e +let enforce_leq_alg u v g = + match Universe.is_sprop u, Universe.is_sprop v with + | true, true -> Constraint.empty, g + | true, false | false, true -> raise (UniverseInconsistency (Le, u, v, None)) + | false, false -> enforce_leq_alg u v g + (* sanity check wrapper *) let enforce_leq_alg u v g = let _,g as cg = enforce_leq_alg u v g in 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/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 6233807016..f69fe064a7 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -831,7 +831,7 @@ let pr_goal_selector ~toplevel s = ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h ) | TacChange (check,op,c,h) -> - let name = if check then "change_no_check" else "change" in + let name = if check then "change" else "change_no_check" in hov 1 ( primitive name ++ brk (1,1) ++ ( diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index fb149071c9..a1dbf9a439 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -546,7 +546,7 @@ let rewrite_core_unif_flags = { Unification.check_applied_meta_types = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; - Unification.allowed_evars = Unification.AllowAll; + Unification.allowed_evars = Evarsolve.AllowedEvars.all; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; 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/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 24772a8514..4a907b2795 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -159,7 +159,7 @@ let declare_one_prenex_implicit locality f = | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f) | impls -> - Impargs.set_implicits locality fref [impls] + Impargs.set_implicits locality fref [List.map (fun imp -> (Anonymous,imp)) impls] } 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/pretyping/evarconv.ml b/pretyping/evarconv.ml index 489e8de602..61453ff214 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -40,7 +40,7 @@ let default_transparent_state env = TransparentState.full let default_flags_of ?(subterm_ts=TransparentState.empty) ts = { modulo_betaiota = true; open_ts = ts; closed_ts = ts; subterm_ts; - frozen_evars = Evar.Set.empty; with_cs = true; + allowed_evars = AllowedEvars.all; with_cs = true; allow_K_at_toplevel = true } let default_flags env = @@ -118,8 +118,6 @@ type flex_kind_of_term = | MaybeFlexible of EConstr.t (* reducible but not necessarily reduced *) | Flexible of EConstr.existential -let is_frozen flags (evk, _) = Evar.Set.mem evk flags.frozen_evars - let flex_kind_of_term flags env evd c sk = match EConstr.kind evd c with | LetIn _ | Rel _ | Const _ | Var _ | Proj _ -> @@ -128,8 +126,7 @@ let flex_kind_of_term flags env evd c sk = if flags.modulo_betaiota then MaybeFlexible c else Rigid | Evar ev -> - if is_frozen flags ev then Rigid - else Flexible ev + if is_evar_allowed flags (fst ev) then Flexible ev else Rigid | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Rigid | Meta _ -> Rigid | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) @@ -192,11 +189,11 @@ let occur_rigidly flags env evd (evk,_) t = | Rigid _ as res -> res | Normal b -> Reducible | Reducible -> Reducible) - | Evar (evk',l as ev) -> + | Evar (evk',l) -> if Evar.equal evk evk' then Rigid true - else if is_frozen flags ev then - Rigid (List.exists (fun x -> rigid_normal_occ (aux x)) l) - else Reducible + else if is_evar_allowed flags evk' then + Reducible + else Rigid (List.exists (fun x -> rigid_normal_occ (aux x)) l) | Cast (p, _, _) -> aux p | Lambda (na, t, b) -> aux b | LetIn (na, _, _, b) -> aux b @@ -458,7 +455,7 @@ let conv_fun f flags on_types = let typefn env evd pbty term1 term2 = let flags = { (default_flags env) with with_cs = flags.with_cs; - frozen_evars = flags.frozen_evars } + allowed_evars = flags.allowed_evars } in f flags env evd pbty term1 term2 in let termfn env evd pbty term1 term2 = @@ -500,7 +497,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 = (whd_nored_state env evd (term2,Stack.empty)) in begin match EConstr.kind evd term1, EConstr.kind evd term2 with - | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) -> + | Evar ev, _ when Evd.is_undefined evd (fst ev) && is_evar_allowed flags (fst ev) -> (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd (position_problem true pbty,ev,term2) with | UnifFailure (_,(OccurCheck _ | NotClean _)) -> @@ -511,7 +508,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 = Miller patterns *) default () | x -> x) - | _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) -> + | _, Evar ev when Evd.is_undefined evd (fst ev) && is_evar_allowed flags (fst ev) -> (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd (position_problem false pbty,ev,term1) with | UnifFailure (_, (OccurCheck _ | NotClean _)) -> @@ -1206,14 +1203,14 @@ type occurrences_selection = let default_occurrence_selection = Unspecified Abstraction.Imitate -let default_occurrence_test ~frozen_evars ts _ origsigma _ env sigma _ c pat = - let flags = { (default_flags_of ~subterm_ts:ts ts) with frozen_evars } in +let default_occurrence_test ~allowed_evars ts _ origsigma _ env sigma _ c pat = + let flags = { (default_flags_of ~subterm_ts:ts ts) with allowed_evars } in match evar_conv_x flags env sigma CONV c pat with | Success sigma -> true, sigma | UnifFailure _ -> false, sigma -let default_occurrences_selection ?(frozen_evars=Evar.Set.empty) ts n = - (default_occurrence_test ~frozen_evars ts, +let default_occurrences_selection ?(allowed_evars=AllowedEvars.all) ts n = + (default_occurrence_test ~allowed_evars ts, List.init n (fun _ -> default_occurrence_selection)) let apply_on_subterm env evd fixedref f test c t = @@ -1554,7 +1551,7 @@ let second_order_matching_with_args flags env evd with_ho pbty ev l t = if with_ho then let evd,ev = evar_absorb_arguments env evd ev (Array.to_list l) in let argoccs = default_evar_selection flags evd ev in - let test = default_occurrence_test ~frozen_evars:flags.frozen_evars flags.subterm_ts in + let test = default_occurrence_test ~allowed_evars:flags.allowed_evars flags.subterm_ts in let evd, b = try second_order_matching flags env evd ev (test,argoccs) t with PretypeError (_, _, NoOccurrenceFound _) -> evd, false @@ -1582,8 +1579,8 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = Termops.Internal.print_constr_env env evd t2 ++ cut ())) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in match EConstr.kind evd term1, EConstr.kind evd term2 with - | Evar (evk1,args1 as ev1), (Rel _|Var _) when app_empty - && not (is_frozen flags ev1) + | Evar (evk1,args1), (Rel _|Var _) when app_empty + && is_evar_allowed flags evk1 && List.for_all (fun a -> EConstr.eq_constr evd a term2 || isEvar evd a) (remove_instance_local_defs evd evk1 args1) -> (* The typical kind of constraint coming from pattern-matching return @@ -1593,8 +1590,8 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = | None -> let reason = ProblemBeyondCapabilities in UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) - | (Rel _|Var _), Evar (evk2,args2 as ev2) when app_empty - && not (is_frozen flags ev2) + | (Rel _|Var _), Evar (evk2,args2) when app_empty + && is_evar_allowed flags evk2 && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a) (remove_instance_local_defs evd evk2 args2) -> (* The typical kind of constraint coming from pattern-matching return @@ -1620,24 +1617,24 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = (evar_define evar_unify flags ~choose:true) evar_unify flags env evd (position_problem true pbty) ev1 ev2) - | Evar ev1,_ when not (is_frozen flags ev1) && Array.length l1 <= Array.length l2 -> + | Evar ev1,_ when is_evar_allowed flags (fst ev1) && Array.length l1 <= Array.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) (* and otherwise second-order matching *) ise_try evd [(fun evd -> first_order_unification flags env evd (ev1,l1) appr2); (fun evd -> second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2)] - | _,Evar ev2 when not (is_frozen flags ev2) && Array.length l2 <= Array.length l1 -> + | _,Evar ev2 when is_evar_allowed flags (fst ev2) && Array.length l2 <= Array.length l1 -> (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *) (* and otherwise second-order matching *) ise_try evd [(fun evd -> first_order_unification flags env evd (ev2,l2) appr1); (fun evd -> second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1)] - | Evar ev1,_ when not (is_frozen flags ev1) -> + | Evar ev1,_ when is_evar_allowed flags (fst ev1) -> (* Try second-order pattern-matching *) second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2 - | _,Evar ev2 when not (is_frozen flags ev2) -> + | _,Evar ev2 when is_evar_allowed flags (fst ev2) -> (* Try second-order pattern-matching *) second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1 | _ -> diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 767a173131..a5a8d1f916 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -105,11 +105,11 @@ val default_occurrence_selection : occurrence_selection type occurrences_selection = occurrence_match_test * occurrence_selection list -val default_occurrence_test : frozen_evars:Evar.Set.t -> TransparentState.t -> occurrence_match_test +val default_occurrence_test : allowed_evars:Evarsolve.AllowedEvars.t -> TransparentState.t -> occurrence_match_test (** [default_occurrence_selection n] Gives the default test and occurrences for [n] arguments *) -val default_occurrences_selection : ?frozen_evars:Evar.Set.t (* By default, none *) -> +val default_occurrences_selection : ?allowed_evars:Evarsolve.AllowedEvars.t (* By default, all *) -> TransparentState.t -> int -> occurrences_selection val second_order_matching : unify_flags -> env -> evar_map -> diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 989fb05c3d..4d5715a391 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -25,14 +25,43 @@ open Reductionops open Evarutil open Pretype_errors +module AllowedEvars = struct + + type t = + | AllowAll + | AllowFun of (Evar.t -> bool) * Evar.Set.t + + let mem allowed evk = + match allowed with + | AllowAll -> true + | AllowFun (f,except) -> f evk && not (Evar.Set.mem evk except) + + let remove evk = function + | AllowAll -> AllowFun ((fun _ -> true), Evar.Set.singleton evk) + | AllowFun (f,except) -> AllowFun (f, Evar.Set.add evk except) + + let all = AllowAll + + let except evars = + AllowFun ((fun _ -> true), evars) + + let from_pred f = + AllowFun (f, Evar.Set.empty) + +end + type unify_flags = { modulo_betaiota: bool; open_ts : TransparentState.t; closed_ts : TransparentState.t; subterm_ts : TransparentState.t; - frozen_evars : Evar.Set.t; + allowed_evars : AllowedEvars.t; allow_K_at_toplevel : bool; - with_cs : bool } + with_cs : bool +} + +let is_evar_allowed flags evk = + AllowedEvars.mem flags.allowed_evars evk type unification_kind = | TypeUnification @@ -1307,24 +1336,24 @@ let preferred_orientation evd evk1 evk2 = let solve_evar_evar_aux force f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let aliases = make_alias_map env evd in - let frozen_ev1 = Evar.Set.mem evk1 flags.frozen_evars in - let frozen_ev2 = Evar.Set.mem evk2 flags.frozen_evars in + let allowed_ev1 = is_evar_allowed flags evk1 in + let allowed_ev2 = is_evar_allowed flags evk2 in if preferred_orientation evd evk1 evk2 then - try if not frozen_ev1 then + try if allowed_ev1 then solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1 else raise (CannotProject (evd,ev2)) with CannotProject (evd,ev2) -> - try if not frozen_ev2 then + try if allowed_ev2 then solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2 else raise (CannotProject (evd,ev1)) with CannotProject (evd,ev1) -> add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd else - try if not frozen_ev2 then + try if allowed_ev2 then solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2 else raise (CannotProject (evd,ev1)) with CannotProject (evd,ev1) -> - try if not frozen_ev1 then + try if allowed_ev1 then solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1 else raise (CannotProject (evd,ev2)) with CannotProject (evd,ev2) -> @@ -1390,15 +1419,15 @@ let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 = let candidates = filter_candidates evd evk untypedfilter NoUpdate in let filter = closure_of_filter evd evk untypedfilter in let evd',ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in - let frozen = Evar.Set.mem evk flags.frozen_evars in - if Evar.equal (fst ev1) evk && (frozen || can_drop) then + let allowed = is_evar_allowed flags evk in + if Evar.equal (fst ev1) evk && (not allowed || can_drop) then (* No refinement needed *) evd' else (* either progress, or not allowed to drop, e.g. to preserve possibly *) (* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *) (* if e can depend on x until ?y is not resolved, or, conversely, we *) (* don't know if ?y has to be unified with ?y, until e is resolved *) - if frozen then + if not allowed then (* We cannot prune a frozen evar *) add_conv_oriented_pb (pbty,env,mkEvar (evk, argsv1),mkEvar (evk,argsv2)) evd else @@ -1455,7 +1484,8 @@ let occur_evar_upto_types sigma n c = let instantiate_evar unify flags env evd evk body = (* Check instance freezing the evar to be defined, as checking could involve the same evar definition problem again otherwise *) - let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in + let allowed_evars = AllowedEvars.remove evk flags.allowed_evars in + let flags = { flags with allowed_evars } in let evd' = check_evar_instance unify flags env evd evk body in Evd.define evk body evd' diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 3fb80432ad..8ff2d7fc63 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -16,6 +16,28 @@ type alias val of_alias : alias -> EConstr.t +module AllowedEvars : sig + + type t + (** Represents the set of evars that can be defined by the pretyper *) + + val all : t + (** All evars can be defined *) + + val mem : t -> Evar.t -> bool + (** [mem allowed evk] is true iff evk can be defined *) + + val from_pred : (Evar.t -> bool) -> t + (** [from_pred p] means evars satisfying p can be defined *) + + val except : Evar.Set.t -> t + (** [except evars] means all evars can be defined except the ones in [evars] *) + + val remove : Evar.t -> t -> t + (** [remove evk allowed] removes [evk] from the set of evars allowed by [allowed] *) + +end + type unify_flags = { modulo_betaiota : bool; (* Enable beta-iota reductions during unification *) @@ -26,8 +48,8 @@ type unify_flags = { subterm_ts : TransparentState.t; (* Enable delta reduction according to subterm_ts for selection of subterms during higher-order unifications. *) - frozen_evars : Evar.Set.t; - (* Frozen evars are treated like rigid variables during unification: they can not be instantiated. *) + allowed_evars : AllowedEvars.t; + (* Disallowed evars are treated like rigid variables during unification: they can not be instantiated. *) allow_K_at_toplevel : bool; (* During higher-order unifications, allow to produce K-redexes: i.e. to produce an abstraction for an unused argument *) @@ -41,6 +63,8 @@ type unification_result = val is_success : unification_result -> bool +val is_evar_allowed : unify_flags -> Evar.t -> bool + (** Replace the vars and rels that are aliases to other vars and rels by their representative that is most ancient in the context *) val expand_vars_in_term : env -> evar_map -> constr -> constr diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d1b65775bd..adb9c5299f 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -68,6 +68,7 @@ type typeclass = { } type typeclasses = typeclass GlobRef.Map.t +(* Invariant: for any pair (gr, tc) in the map, gr and tc.cl_impl are equal *) type instance = { is_class: GlobRef.t; @@ -268,7 +269,7 @@ let instances env sigma r = let cl = class_info env sigma r in instances_of cl let is_class gr = - GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes + GlobRef.Map.mem gr !classes open Evar_kinds type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool diff --git a/pretyping/unification.ml b/pretyping/unification.ml index a26c981cb9..207a03d80f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -252,10 +252,6 @@ let unify_r2l x = x let sort_eqns = unify_r2l *) -type allowed_evars = -| AllowAll -| AllowFun of (Evar.t -> bool) - type core_unify_flags = { modulo_conv_on_closed_terms : TransparentState.t option; (* What this flag controls was activated with all constants transparent, *) @@ -289,7 +285,7 @@ type core_unify_flags = { (* This allowed for instance to unify "forall x:?A, ?B x" with "A' -> B'" *) (* when ?B is a Meta. *) - allowed_evars : allowed_evars; + allowed_evars : AllowedEvars.t; (* Evars that are allowed to be instantiated *) (* Useful e.g. for autorewrite *) @@ -341,7 +337,7 @@ let default_core_unify_flags () = check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; modulo_eta = true; @@ -421,7 +417,7 @@ let default_no_delta_unify_flags ts = let allow_new_evars sigma = let undefined = Evd.undefined_map sigma in - AllowFun (fun evk -> not (Evar.Map.mem evk undefined)) + AllowedEvars.from_pred (fun evk -> not (Evar.Map.mem evk undefined)) (* Default flags for looking for subterms in elimination tactics *) (* Not used in practice at the current date, to the exception of *) @@ -604,9 +600,8 @@ let do_reduce ts (env, nb) sigma c = Stack.zip sigma (whd_betaiota_deltazeta_for_iota_state ts env sigma (c, Stack.empty)) -let is_evar_allowed flags evk = match flags.allowed_evars with -| AllowAll -> true -| AllowFun f -> f evk +let is_evar_allowed flags evk = + AllowedEvars.mem flags.allowed_evars evk let isAllowedEvar sigma flags c = match EConstr.kind sigma c with | Evar (evk,_) -> is_evar_allowed flags evk diff --git a/pretyping/unification.mli b/pretyping/unification.mli index f9a969a253..5462e09359 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -13,10 +13,6 @@ open EConstr open Environ open Evd -type allowed_evars = -| AllowAll -| AllowFun of (Evar.t -> bool) - type core_unify_flags = { modulo_conv_on_closed_terms : TransparentState.t option; use_metas_eagerly_in_conv_on_closed_terms : bool; @@ -26,7 +22,7 @@ type core_unify_flags = { check_applied_meta_types : bool; use_pattern_unification : bool; use_meta_bound_pattern_unification : bool; - allowed_evars : allowed_evars; + allowed_evars : Evarsolve.AllowedEvars.t; restrict_conv_on_strict_subterms : bool; modulo_betaiota : bool; modulo_eta : bool; diff --git a/printing/printer.ml b/printing/printer.ml index 0f635623e7..a1a2d9ae51 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -780,7 +780,8 @@ let pr_open_subgoals_diff ?(quiet=false) ?(diffs=false) ?oproof proof = straightforward, but seriously, [Proof.proof] should return [evar_info]-s instead. *) let p = proof in - let Proof.{goals; stack; shelf; sigma} = Proof.data p in + let Proof.{goals; stack; sigma} = Proof.data p in + let shelf = Evd.shelf sigma in let given_up = Evd.given_up sigma in let stack = List.map (fun (l,r) -> List.length l + List.length r) stack in let seeds = Proof.V82.top_evars p in diff --git a/proofs/clenv.ml b/proofs/clenv.ml index db76d08736..31bc698830 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -618,9 +618,6 @@ let clenv_cast_meta clenv = in crec -let clenv_value_cast_meta clenv = - clenv_cast_meta clenv (clenv_value clenv) - let clenv_pose_dependent_evars ?(with_evars=false) clenv = let dep_mvs = clenv_dependent clenv in let env, sigma = clenv.env, clenv.evd in @@ -673,7 +670,7 @@ let fail_quick_core_unif_flags = { check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; (* ? *) - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = false; modulo_eta = true; @@ -716,12 +713,6 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function | NoBindings -> mk_clenv_from_env env sigma n (c,t) -let make_clenv_binding_env_apply env sigma n = - make_clenv_binding_gen true n env sigma - -let make_clenv_binding_env env sigma = - make_clenv_binding_gen false None env sigma - let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 43e808dac7..a72c8c5e1f 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -75,17 +75,10 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv (** the arity of the lemma is fixed the optional int tells how many prods of the lemma have to be used use all of them if None *) -val make_clenv_binding_env_apply : - env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings -> - clausenv - val make_clenv_binding_apply : env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv -val make_clenv_binding_env : - env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv - val make_clenv_binding : env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv @@ -99,7 +92,6 @@ val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv -val clenv_value_cast_meta : clausenv -> constr (** {6 Pretty-print (debug only) } *) val pr_clenv : clausenv -> Pp.t diff --git a/proofs/proof.ml b/proofs/proof.ml index d7904c56a8..d864aed25a 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -24,8 +24,6 @@ the focus kind is actually stored inside the condition). To unfocus, one needs to know the focus kind, and the condition (for instance "no condition" or the proof under focused must be complete) must be met. - - Shelf: A list of goals which have been put aside during the proof. They can be - retrieved with the [Unshelve] command, or solved by side effects - Given up goals: as long as there is a given up goal, the proof is not completed. Given up goals cannot be retrieved, the user must go back where the tactic [give_up] was run and solve the goal there. @@ -113,8 +111,6 @@ type t = (** History of the focusings, provides information on how to unfocus the proof and the extra information stored while focusing. The list is empty when the proof is fully unfocused. *) - ; shelf : Goal.goal list - (** List of goals that have been shelved. *) ; name : Names.Id.t (** the name of the theorem whose proof is being constructed *) ; poly : bool @@ -135,8 +131,7 @@ let proof p = let stack = map_minus_one (fun (_,_,c) -> Proofview.focus_context c) p.focus_stack in - let shelf = p.shelf in - (goals,stack,shelf,sigma) + (goals,stack,sigma) let rec unroll_focus pv = function | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk @@ -152,7 +147,9 @@ let is_done p = (* spiwack: for compatibility with <= 8.2 proof engine *) let has_unresolved_evar p = Proofview.V82.has_unresolved_evar p.proofview -let has_shelved_goals p = not (CList.is_empty (p.shelf)) +let has_shelved_goals p = + let (_goals,sigma) = Proofview.proofview p.proofview in + Evd.has_shelved sigma let has_given_up_goals p = let (_goals,sigma) = Proofview.proofview p.proofview in Evd.has_given_up sigma @@ -216,13 +213,10 @@ let focus_id cond inf id pr = (* goal is already under focus *) _focus cond (Obj.repr inf) i i pr | None -> - if CList.mem_f Evar.equal ev pr.shelf then + if CList.mem_f Evar.equal ev (Evd.shelf evar_map) then (* goal is on the shelf, put it in focus *) let proofview = Proofview.unshelve [ev] pr.proofview in - let shelf = - CList.filter (fun ev' -> Evar.equal ev ev' |> not) pr.shelf - in - let pr = { pr with proofview; shelf } in + let pr = { pr with proofview } in let (focused_goals, _) = Proofview.proofview pr.proofview in let i = (* Now we know that this will succeed *) @@ -290,7 +284,6 @@ let start ~name ~poly sigma goals = { proofview ; entry ; focus_stack = [] - ; shelf = [] ; name ; poly } in @@ -302,7 +295,6 @@ let dependent_start ~name ~poly goals = { proofview ; entry ; focus_stack = [] - ; shelf = [] ; name ; poly } in @@ -353,8 +345,8 @@ let compact p = let entry, proofview = Proofview.compact p.entry p.proofview in { p with proofview; entry } -let update_sigma_env p env = - let proofview = Proofview.Unsafe.update_sigma_env p.proofview env in +let update_sigma_univs ugraph p = + let proofview = Proofview.Unsafe.update_sigma_univs ugraph p.proofview in { p with proofview } (*** Function manipulation proof extra informations ***) @@ -365,34 +357,41 @@ let run_tactic env tac pr = let open Proofview.Notations in let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in let tac = + Proofview.tclEVARMAP >>= fun sigma -> + Proofview.Unsafe.tclEVARS (Evd.push_shelf sigma) >>= fun () -> tac >>= fun result -> Proofview.tclEVARMAP >>= fun sigma -> (* Already solved goals are not to be counted as shelved. Nor are they to be marked as unresolvable. *) let retrieved, sigma = Evd.pop_future_goals sigma in let retrieved = Evd.FutureGoals.filter (Evd.is_undefined sigma) retrieved in - let retrieved = List.rev_append retrieved.Evd.FutureGoals.shelf (List.rev retrieved.Evd.FutureGoals.comb) in + let retrieved = List.rev retrieved.Evd.FutureGoals.comb in let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in + let to_shelve, sigma = Evd.pop_shelf sigma in Proofview.Unsafe.tclEVARS sigma >>= fun () -> - Proofview.tclUNIT (result,retrieved) + Proofview.Unsafe.tclNEWSHELVED (retrieved@to_shelve) <*> + Proofview.tclUNIT (result,retrieved,to_shelve) in let { name; poly; proofview } = pr in let proofview = Proofview.Unsafe.push_future_goals proofview in - let ((result,retrieved),proofview,(status,to_shelve),info_trace) = + let ((result,retrieved,to_shelve),proofview,status,info_trace) = Proofview.apply ~name ~poly env tac proofview in let sigma = Proofview.return proofview in let to_shelve = undef sigma to_shelve in - let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in let proofview = Proofview.Unsafe.mark_as_unresolvables proofview to_shelve in - { pr with proofview ; shelf },(status,info_trace),result + let proofview = Proofview.filter_shelf (Evd.is_undefined sigma) proofview in + { pr with proofview },(status,info_trace),result (*** Commands ***) (* Remove all the goals from the shelf and adds them at the end of the focused goals. *) let unshelve p = - { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] } + let sigma = Proofview.return p.proofview in + let shelf = Evd.shelf sigma in + let proofview = Proofview.unshelve shelf p.proofview in + { p with proofview } (*** Compatibility layer with <=v8.2 ***) module V82 = struct @@ -438,22 +437,22 @@ module V82 = struct end in let { name; poly } = pr in let ((), proofview, _, _) = Proofview.apply ~name ~poly env tac pr.proofview in - let shelf = - List.filter begin fun g -> + let proofview = Proofview.filter_shelf + begin fun g -> Evd.is_undefined (Proofview.return proofview) g - end pr.shelf + end proofview in - { pr with proofview ; shelf } + { pr with proofview } end let all_goals p = let add gs set = List.fold_left (fun s g -> Goal.Set.add g s) set gs in - let (goals,stack,shelf,sigma) = proof p in + let (goals,stack,sigma) = proof p in let set = add goals Goal.Set.empty in let set = List.fold_left (fun s gs -> let (g1, g2) = gs in add g1 (add g2 set)) set stack in - let set = add shelf set in + let set = add (Evd.shelf sigma) set in let set = Goal.Set.union (Evd.given_up sigma) set in let { Evd.it = bgoals ; sigma = bsigma } = V82.background_subgoals p in add bgoals set @@ -467,15 +466,13 @@ type data = (** Entry for the proofview *) ; stack : (Evar.t list * Evar.t list) list (** A representation of the focus stack *) - ; shelf : Evar.t list - (** A representation of the shelf *) ; name : Names.Id.t (** The name of the theorem whose proof is being constructed *) ; poly : bool (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *) } -let data { proofview; focus_stack; entry; shelf; name; poly } = +let data { proofview; focus_stack; entry; name; poly } = let goals, sigma = Proofview.proofview proofview in (* spiwack: beware, the bottom of the stack is used by [Proof] internally, and should not be exposed. *) @@ -486,10 +483,10 @@ let data { proofview; focus_stack; entry; shelf; name; poly } = in let stack = map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in - { sigma; goals; entry; stack; shelf; name; poly } + { sigma; goals; entry; stack; name; poly } let pr_proof p = - let { goals=fg_goals; stack=bg_goals; shelf; sigma } = data p in + let { goals=fg_goals; stack=bg_goals; sigma } = data p in Pp.( let pr_goal_list = prlist_with_sep spc Goal.pr_goal in let rec aux acc = function @@ -499,7 +496,7 @@ let pr_proof p = pr_goal_list after) stack in str "[" ++ str "focus structure: " ++ aux (pr_goal_list fg_goals) bg_goals ++ str ";" ++ spc () ++ - str "shelved: " ++ pr_goal_list shelf ++ str ";" ++ spc () ++ + str "shelved: " ++ pr_goal_list (Evd.shelf sigma) ++ str ";" ++ spc () ++ str "given up: " ++ pr_goal_list (Evar.Set.elements @@ Evd.given_up sigma) ++ str "]" ) @@ -580,7 +577,7 @@ let refine_by_tactic ~name ~poly env sigma ty tac = Exninfo.iraise (e, info) in (* Plug back the retrieved sigma *) - let { goals; stack; shelf; sigma; entry } = data prf in + let { goals; stack; sigma; entry } = data prf in assert (stack = []); let ans = match Proofview.initial_goals entry with | [c, _] -> c @@ -597,9 +594,6 @@ let refine_by_tactic ~name ~poly env sigma ty tac = (* Push remaining goals as future_goals which is the only way we have to inform the caller that there are goals to collect while not being encapsulated in the monad *) - (* Goals produced by tactic "shelve" *) - let sigma = List.fold_right (Evd.declare_future_goal ~shelve:true) shelf sigma in - (* Other goals *) let sigma = List.fold_right Evd.declare_future_goal goals sigma in (* Get rid of the fresh side-effects by internalizing them in the term itself. Note that this is unsound, because the tactic may have solved diff --git a/proofs/proof.mli b/proofs/proof.mli index a0d4759bfc..f487595dac 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -43,8 +43,6 @@ type data = (** Entry for the proofview *) ; stack : (Evar.t list * Evar.t list) list (** A representation of the focus stack *) - ; shelf : Evar.t list - (** A representation of the shelf *) ; name : Names.Id.t (** The name of the theorem whose proof is being constructed *) ; poly : bool; @@ -76,8 +74,8 @@ val partial_proof : t -> EConstr.constr list val compact : t -> t -(** [update_sigma_env] lifts [Evd.update_sigma_env] to the proof *) -val update_sigma_env : t -> Environ.env -> t +(** [update_sigma_univs] lifts [UState.update_sigma_univs] to the proof *) +val update_sigma_univs : UGraph.t -> t -> t (* Returns the proofs (with their type) of the initial goals. Raises [UnfinishedProof] is some goals remain to be considered. diff --git a/proofs/refine.ml b/proofs/refine.ml index 51d6c923b6..dcff5e2b6c 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -92,7 +92,6 @@ let generic_refine ~typecheck f gl = in (* Mark goals *) let sigma = Proofview.Unsafe.mark_as_goals sigma future_goals.Evd.FutureGoals.comb in - let sigma = Proofview.Unsafe.mark_unresolvables sigma future_goals.Evd.FutureGoals.shelf in let comb = CList.rev_map (fun x -> Proofview.goal_with_state x state) future_goals.Evd.FutureGoals.comb in let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++ Termops.Internal.print_constr_env env sigma c)) in @@ -100,7 +99,6 @@ let generic_refine ~typecheck f gl = Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*> Proofview.Unsafe.tclEVARS sigma <*> Proofview.Unsafe.tclSETGOALS comb <*> - Proofview.Unsafe.tclPUTSHELF @@ List.rev future_goals.Evd.FutureGoals.shelf <*> Proofview.tclUNIT v end diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index e41f62361d..f367167d48 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -51,8 +51,8 @@ let is_focused_goal_simple ~doc id = | `Valid (Some { Vernacstate.lemmas }) -> Option.cata (Vernacstate.LemmaStack.with_top ~f:(fun proof -> let proof = Declare.Proof.get proof in - let Proof.{ goals=focused; stack=r1; shelf=r2; sigma } = Proof.data proof in - let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ (Evar.Set.elements @@ Evd.given_up sigma) in + let Proof.{ goals=focused; stack=r1; sigma } = Proof.data proof in + let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ (Evd.shelf sigma) @ (Evar.Set.elements @@ Evd.given_up sigma) in if List.for_all (fun x -> simple_goal sigma x rest) focused then `Simple focused else `Not)) `Not lemmas diff --git a/stm/stm.ml b/stm/stm.ml index c94a6d3a5d..4ca0c365bf 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -142,10 +142,6 @@ let may_pierce_opaque = function | VernacExtend (("ExtractionInductive",_), _) -> true | _ -> false -let update_global_env () = - if PG_compat.there_are_pending_proofs () then - PG_compat.update_global_env () - module Vcs_ = Vcs.Make(Stateid.Self) type future_proof = Declare.Proof.closed_proof_output Future.computation @@ -1922,7 +1918,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 @@ -2335,7 +2332,9 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = (* ugly functions to process nested lemmas, i.e. hard to reproduce * side effects *) let inject_non_pstate (s,l) = - Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env () + Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; + if PG_compat.there_are_pending_proofs () then + PG_compat.update_sigma_univs (Global.universes ()) in let rec pure_cherry_pick_non_pstate safe_id id = 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/tactics/auto.ml b/tactics/auto.ml index 784322679f..369508c2a3 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -47,7 +47,7 @@ let auto_core_unif_flags_of st1 st2 = { check_applied_meta_types = false; use_pattern_unification = false; use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; (* Compat *) modulo_betaiota = false; modulo_eta = true; diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ccb69cf845..96cbbf0ba8 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -134,7 +134,7 @@ let auto_core_unif_flags st allowed_evars = { modulo_eta = false; } -let auto_unif_flags ?(allowed_evars = AllowAll) st = +let auto_unif_flags ?(allowed_evars = Evarsolve.AllowedEvars.all) st = let fl = auto_core_unif_flags st allowed_evars in { core_unify_flags = fl; merge_unify_flags = fl; @@ -307,10 +307,10 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm if cl.cl_strict then let undefined = lazy (Evarutil.undefined_evars_of_term sigma concl) in let allowed evk = not (Evar.Set.mem evk (Lazy.force undefined)) in - AllowFun allowed - else AllowAll - | _ -> AllowAll - with e when CErrors.noncritical e -> AllowAll + Evarsolve.AllowedEvars.from_pred allowed + else Evarsolve.AllowedEvars.all + | _ -> Evarsolve.AllowedEvars.all + with e when CErrors.noncritical e -> Evarsolve.AllowedEvars.all in let tac_of_hint = fun (flags, h) -> @@ -931,12 +931,14 @@ module Search = struct top_sort evm goals else Evar.Set.elements goals in - let tac = tac <*> Proofview.Unsafe.tclGETGOALS >>= + let goalsl = List.map Proofview_monad.with_empty_state goalsl in + let tac = + Proofview.Unsafe.tclNEWGOALS goalsl <*> + tac <*> Proofview.Unsafe.tclGETGOALS >>= fun stuck -> Proofview.shelve_goals (List.map Proofview_monad.drop_state stuck) in let evm = Evd.set_typeclass_evars evm Evar.Set.empty in let evm = Evd.push_future_goals evm in let _, pv = Proofview.init evm [] in - let pv = Proofview.unshelve goalsl pv in try (* Instance may try to call this before a proof is set up! Thus, give_me_the_proof will fail. Beware! *) @@ -947,17 +949,17 @@ module Search = struct * with | Proof_global.NoCurrentProof -> *) Id.of_string "instance", false in - let finish pv' shelved = + let finish pv' = let evm' = Proofview.return pv' in + let shelf = Evd.shelf evm' in assert(Evd.fold_undefined (fun ev _ acc -> - let okev = Evd.mem evm ev || List.mem ev shelved in + let okev = Evd.mem evm ev || List.mem ev shelf in if not okev then Feedback.msg_debug (str "leaking evar " ++ int (Evar.repr ev) ++ spc () ++ pr_ev evm' ev); acc && okev) evm' true); let _, evm' = Evd.pop_future_goals evm' in - let evm' = Evd.shelve_on_future_goals shelved evm' in let nongoals' = Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with | Some ev' -> Evar.Set.add ev acc @@ -968,8 +970,8 @@ module Search = struct let evm' = Evd.set_typeclass_evars evm' nongoals' in Some evm' in - let (), pv', (unsafe, shelved), _ = Proofview.apply ~name ~poly env tac pv in - if Proofview.finished pv' then finish pv' shelved + let (), pv', unsafe, _ = Proofview.apply ~name ~poly env tac pv in + if Proofview.finished pv' then finish pv' else raise Not_found with Logic_monad.TacticFailure _ -> raise Not_found diff --git a/tactics/elim.ml b/tactics/elim.ml index 274ebc9f60..49437a2aef 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -10,33 +10,137 @@ open Util open Names +open Constr open Termops open EConstr open Inductiveops open Hipattern open Tacmach.New open Tacticals.New +open Clenv open Tactics open Proofview.Notations +type branch_args = { + branchnum : int; (* the branch number *) + nassums : int; (* number of assumptions/letin to be introduced *) + branchsign : bool list; (* the signature of the branch. + true=assumption, false=let-in *) + branchnames : Tactypes.intro_patterns} + module NamedDecl = Context.Named.Declaration +type elim_kind = Case of bool | Elim + +(* Find the right elimination suffix corresponding to the sort of the goal *) +(* c should be of type A1->.. An->B with B an inductive definition *) +let general_elim_then_using mk_elim + rec_flag allnames tac predicate (ind, u, args) id = + let open Pp in + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sort = Retyping.get_sort_family_of env sigma (Proofview.Goal.concl gl) in + let sigma, elim = match mk_elim with + | Case dep -> + let u = EInstance.kind sigma u in + let (sigma, r) = Indrec.build_case_analysis_scheme env sigma (ind, u) dep sort in + (sigma, EConstr.of_constr r) + | Elim -> + let gr = Indrec.lookup_eliminator env ind sort in + Evd.fresh_global env sigma gr + in + let indclause = mk_clenv_from_env env sigma None (mkVar id, mkApp (mkIndU (ind, u), args)) in + (* applying elimination_scheme just a little modified *) + let elimclause = mk_clenv_from_env env sigma None (elim, Retyping.get_type_of env sigma elim) in + let indmv = + match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with + | Meta mv -> mv + | _ -> CErrors.anomaly (str"elimination.") + in + let pmv = + let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in + match EConstr.kind elimclause.evd p with + | Meta p -> p + | _ -> + let name_elim = + match EConstr.kind sigma elim with + | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env env sigma elim + | _ -> mt () + in + CErrors.user_err ~hdr:"Tacticals.general_elim_then_using" + (str "The elimination combinator " ++ name_elim ++ str " is unknown.") + in + let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in + let branchsigns = Tacticals.compute_constructor_signatures ~rec_flag (ind, u) in + let brnames = Tacticals.compute_induction_names false branchsigns allnames in + let flags = Unification.elim_flags () in + let elimclause' = + match predicate with + | None -> elimclause' + | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause' + in + let after_tac i = + let ba = { branchsign = branchsigns.(i); + branchnames = brnames.(i); + nassums = List.length branchsigns.(i); + branchnum = i+1; } + in + tac ba + in + let branchtacs = List.init (Array.length branchsigns) after_tac in + Proofview.tclTHEN + (Clenv.res_pf ~flags elimclause') + (Proofview.tclEXTEND [] tclIDTAC branchtacs) + end + +(* computing the case/elim combinators *) + +let make_elim_branch_assumptions ba hyps = + let assums = + try List.rev (List.firstn ba.nassums hyps) + with Failure _ -> CErrors.anomaly (Pp.str "make_elim_branch_assumptions.") in + assums + +let elim_on_ba tac ba = + Proofview.Goal.enter begin fun gl -> + let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in + tac branches + end + +let elimination_then tac id = + let open Declarations in + Proofview.Goal.enter begin fun gl -> + let ((ind, u), t) = pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl (mkVar id)) in + let _, args = decompose_app_vect (Proofview.Goal.sigma gl) t in + let isrec,mkelim = + match (Global.lookup_mind (fst ind)).mind_record with + | NotRecord -> true, Elim + | FakeRecord | PrimRecord _ -> false, Case true + in + general_elim_then_using mkelim isrec None tac None (ind, u, args) id + end + (* Supposed to be called without as clause *) let introElimAssumsThen tac ba = - assert (ba.Tacticals.branchnames == []); - let introElimAssums = tclDO ba.Tacticals.nassums intro in + assert (ba.branchnames == []); + let introElimAssums = tclDO ba.nassums intro in (tclTHEN introElimAssums (elim_on_ba tac ba)) (* Supposed to be called with a non-recursive scheme *) let introCaseAssumsThen with_evars tac ba = - let n1 = List.length ba.Tacticals.branchsign in - let n2 = List.length ba.Tacticals.branchnames in + let n1 = List.length ba.branchsign in + let n2 = List.length ba.branchnames in let (l1,l2),l3 = - if n1 < n2 then List.chop n1 ba.Tacticals.branchnames, [] - else (ba.Tacticals.branchnames, []), List.make (n1-n2) false in + if n1 < n2 then List.chop n1 ba.branchnames, [] + else (ba.branchnames, []), List.make (n1-n2) false in let introCaseAssums = tclTHEN (intro_patterns with_evars l1) (intros_clearing l3) in - (tclTHEN introCaseAssums (case_on_ba (tac l2) ba)) + (tclTHEN introCaseAssums (elim_on_ba (tac l2) ba)) + +let case_tac dep names tac elim ind c = + let tac = introCaseAssumsThen false (* ApplyOn not supported by inversion *) tac in + general_elim_then_using (Case dep) false names tac (Some elim) ind c (* The following tactic Decompose repeatedly applies the elimination(s) rule(s) of the types satisfying the predicate @@ -56,19 +160,16 @@ Another example : Qed. *) -let elimHypThen tac id = - elimination_then tac (mkVar id) - let rec general_decompose_on_hyp recognizer = ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT()) and general_decompose_aux recognizer id = - elimHypThen + elimination_then (introElimAssumsThen (fun bas -> tclTHEN (clear [id]) (tclMAP (general_decompose_on_hyp recognizer) - (ids_of_named_context bas.Tacticals.assums)))) + (ids_of_named_context bas)))) id (* We should add a COMPLETE to be sure that the created hypothesis @@ -76,7 +177,6 @@ and general_decompose_aux recognizer id = (* Best strategies but loss of compatibility *) let tmphyp_name = Id.of_string "_TmpHyp" -let up_to_delta = ref false (* true *) let general_decompose recognizer c = Proofview.Goal.enter begin fun gl -> @@ -90,14 +190,10 @@ let general_decompose recognizer c = end let head_in indl t gl = - let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in try - let ity,_ = - if !up_to_delta - then find_mrectype env sigma t - else extract_mrectype sigma t - in List.exists (fun i -> eq_ind (fst i) (fst ity)) indl + let ity,_ = extract_mrectype sigma t in + List.exists (fun i -> eq_ind (fst i) (fst ity)) indl with Not_found -> false let decompose_these c l = @@ -124,9 +220,6 @@ let h_decompose_and = decompose_and (* The tactic Double performs a double induction *) -let simple_elimination c = - elimination_then (fun _ -> tclIDTAC) c - let induction_trailer abs_i abs_j bargs = tclTHEN (tclDO (abs_j - abs_i) intro) @@ -136,7 +229,7 @@ let induction_trailer abs_i abs_j bargs = let idty = pf_get_type_of gl (mkVar id) in let fvty = global_vars (pf_env gl) (project gl) idty in let possible_bring_hyps = - (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums + (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs in let (hyps,_) = List.fold_left @@ -149,7 +242,7 @@ let induction_trailer abs_i abs_j bargs = in let ids = List.rev (ids_of_named_context hyps) in (tclTHENLIST - [revert ids; simple_elimination (mkVar id)]) + [revert ids; elimination_then (fun _ -> tclIDTAC) id]) end )) @@ -167,7 +260,7 @@ let double_ind h1 h2 = (onLastHypId (fun id -> elimination_then - (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) + (introElimAssumsThen (induction_trailer abs_i abs_j)) id))) end let h_double_induction = double_ind diff --git a/tactics/elim.mli b/tactics/elim.mli index e89855a050..01053502e4 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -10,14 +10,13 @@ open Names open EConstr -open Tacticals open Tactypes (** Eliminations tactics. *) -val introCaseAssumsThen : Tactics.evars_flag -> - (intro_patterns -> branch_assumptions -> unit Proofview.tactic) -> - branch_args -> unit Proofview.tactic +val case_tac : bool -> or_and_intro_pattern option -> + (intro_patterns -> named_context -> unit Proofview.tactic) -> + constr -> inductive * EInstance.t * EConstr.t array -> Id.t -> unit Proofview.tactic val h_decompose : inductive list -> constr -> unit Proofview.tactic val h_decompose_or : constr -> unit Proofview.tactic diff --git a/tactics/equality.ml b/tactics/equality.ml index b4def7bb51..26ae35a79d 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -105,7 +105,7 @@ let rewrite_core_unif_flags = { check_applied_meta_types = true; use_pattern_unification = true; use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; modulo_eta = true; @@ -130,7 +130,7 @@ let freeze_initial_evars sigma flags clause = if Evar.Map.mem evk initial then false else Evar.Set.mem evk (Lazy.force newevars) in - let allowed_evars = AllowFun allowed in + let allowed_evars = Evarsolve.AllowedEvars.from_pred allowed in {flags with core_unify_flags = {flags.core_unify_flags with allowed_evars}; merge_unify_flags = {flags.merge_unify_flags with allowed_evars}; @@ -187,7 +187,7 @@ let rewrite_conv_closed_core_unif_flags = { use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = false; @@ -221,7 +221,7 @@ let rewrite_keyed_core_unif_flags = { use_meta_bound_pattern_unification = true; - allowed_evars = AllowAll; + allowed_evars = Evarsolve.AllowedEvars.all; restrict_conv_on_strict_subterms = false; modulo_betaiota = true; @@ -1013,19 +1013,16 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind = Proofview.tclUNIT (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2])) +type equality = { + eq_data : (coq_eq_data * (EConstr.t * EConstr.t * EConstr.t)); + (* equality data + A : Type, t1 : A, t2 : A *) + eq_clenv : clausenv; + (* clause [M : R A t1 t2] where [R] is the equality from above *) +} let eq_baseid = Id.of_string "e" -let apply_on_clause (f,t) clause = - let sigma = clause.evd in - let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in - let argmv = - (match EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with - | Meta mv -> mv - | _ -> user_err (str "Ill-formed clause applicator.")) in - clenv_fchain ~with_univs:false argmv f_clause clause - -let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = +let discr_positions env sigma { eq_data = (lbeq,(t,t1,t2)); eq_clenv = eq_clause } cpath dirn = build_coq_True () >>= fun true_0 -> build_coq_False () >>= fun false_0 -> let false_ty = Retyping.get_type_of env sigma false_0 in @@ -1043,13 +1040,13 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = in discriminator >>= fun discriminator -> discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf -> - let pf_ty = mkArrow eqn Sorts.Relevant false_0 in - let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in - let pf = Clenv.clenv_value_cast_meta absurd_clause in + (* pf : eq t t1 t2 -> False *) + let pf = EConstr.mkApp (pf, [|clenv_value eq_clause|]) in tclTHENS (assert_after Anonymous false_0) [onLastHypId gen_absurdity; (Logic.refiner ~check:true EConstr.Unsafe.(to_constr pf))] -let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = +let discrEq eq = + let { eq_data = (_, (_, t1, t2)); eq_clenv = eq_clause } = eq in let sigma = eq_clause.evd in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -1058,7 +1055,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = let info = Exninfo.reify () in tclZEROMSG ~info (str"Not a discriminable equality.") | Inl (cpath, (_,dirn), _) -> - discr_positions env sigma u eq_clause cpath dirn + discr_positions env sigma eq cpath dirn end let onEquality with_evars tac (c,lbindc) = @@ -1071,9 +1068,10 @@ let onEquality with_evars tac (c,lbindc) = let eqn = clenv_type eq_clause' in (* FIXME evar leak *) let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in + let eq = { eq_data = (eq, eq_args); eq_clenv = eq_clause' } in tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) - (tac (eq,eqn,eq_args) eq_clause') + (tac eq) end let onNegatedEquality with_evars tac = @@ -1385,7 +1383,8 @@ let simplify_args env sigma t = | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2]) | _ -> t -let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = +let inject_at_positions env sigma l2r eq posns tac = + let { eq_data = (eq, (t,t1,t2)); eq_clenv = eq_clause } = eq in let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (LocalAssum (make_annot e Sorts.Relevant,t)) env in let evdref = ref sigma in @@ -1395,11 +1394,12 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in let injfun = mkNamedLambda (make_annot e Sorts.Relevant) t injbody in let sigma,congr = Evd.fresh_global env sigma eq.congr in - let pf = applist(congr,[t;resty;injfun;t1;t2]) in + (* pf : eq t t1 t2 -> eq resty (injfun t1) (injfun t2) *) + let pf = mkApp (congr,[|t; resty; injfun; t1; t2|]) in let sigma, pf_typ = Typing.type_of env sigma pf in - let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in - let pf = Clenv.clenv_value_cast_meta inj_clause in - let ty = simplify_args env sigma (clenv_type inj_clause) in + let pf_typ = Vars.subst1 mkProp (pi3 @@ destProd sigma pf_typ) in + let pf = mkApp (pf, [| Clenv.clenv_value eq_clause |]) in + let ty = simplify_args env sigma pf_typ in evdref := sigma; Some (pf, ty) with Failure _ -> None @@ -1422,7 +1422,8 @@ let () = CErrors.register_handler (function | NothingToInject -> Some (Pp.str "Nothing to inject.") | _ -> None) -let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = +let injEqThen keep_proofs tac l2r eql = + let { eq_data = (eq, (t,t1,t2)); eq_clenv = eq_clause } = eql in let sigma = eq_clause.evd in let env = eq_clause.env in match find_positions env sigma ~keep_proofs ~no_discr:true t1 t2 with @@ -1437,7 +1438,7 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause = | Inr [([],_,_)] -> Proofview.tclZERO NothingToInject | Inr posns -> - inject_at_positions env sigma l2r u eq_clause posns + inject_at_positions env sigma l2r eql posns (tac (clenv_value eq_clause)) let get_previous_hyp_position id gl = @@ -1491,17 +1492,18 @@ let simpleInjClause flags with_evars = function let injConcl flags = injClause flags None false None let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent CAst.(make id))) -let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause = +let decompEqThen keep_proofs ntac eq = + let { eq_data = (_, (_,t1,t2) as u); eq_clenv = clause } = eq in Proofview.Goal.enter begin fun gl -> let sigma = clause.evd in let env = Proofview.Goal.env gl in match find_positions env sigma ~keep_proofs ~no_discr:false t1 t2 with | Inl (cpath, (_,dirn), _) -> - discr_positions env sigma u clause cpath dirn + discr_positions env sigma eq cpath dirn | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) ntac (clenv_value clause) 0 | Inr posns -> - inject_at_positions env sigma true u clause posns + inject_at_positions env sigma true eq posns (ntac (clenv_value clause)) end @@ -1513,10 +1515,11 @@ let dEq ~keep_proofs with_evars = dEqThen ~keep_proofs with_evars (fun clear_flag c x -> (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)) -let intro_decomp_eq tac data (c, t) = +let intro_decomp_eq tac (eq, _, data) (c, t) = Proofview.Goal.enter begin fun gl -> let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in - decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl + let eq = { eq_data = (eq, data); eq_clenv = cl } in + decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) eq end let () = declare_intro_decomp_eq intro_decomp_eq diff --git a/tactics/hints.ml b/tactics/hints.ml index db4b23705f..355cea8fa8 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -837,7 +837,7 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) = db = None; secvars; code = with_uid (Give_exact (c, cty, ctx, poly)); }) -let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (c, cty, ctx) = +let make_apply_entry env sigma hnf info ~poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in match EConstr.kind sigma cty with | Prod _ -> @@ -862,25 +862,11 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) ( db = None; secvars; code = with_uid (Res_pf(c,cty,ctx,poly)); }) - else begin - if not eapply then failwith "make_apply_entry"; - if verbose then begin - let variables = str (CString.plural nmiss "variable") in - Feedback.msg_info ( - strbrk "The hint " ++ - pr_leconstr_env env sigma' c ++ - strbrk " will only be used by eauto, because applying " ++ - pr_leconstr_env env sigma' c ++ - strbrk " would leave " ++ variables ++ Pp.spc () ++ - Pp.prlist_with_sep Pp.pr_comma Name.print (List.map (Evd.meta_name ce.evd) miss) ++ - strbrk " as unresolved existential " ++ variables ++ str "." - ) - end; + else (Some hd, { pri; pat = Some pat; name; db = None; secvars; code = with_uid (ERes_pf(c,cty,ctx,poly)); }) - end | _ -> failwith "make_apply_entry" (* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose @@ -916,19 +902,25 @@ let fresh_global_or_constr env sigma poly cr = (c, Univ.ContextSet.empty) end -let make_resolves env sigma flags info ~check ~poly ?name cr = +let make_resolves env sigma (eapply, hnf) info ~check ~poly ?name cr = let c, ctx = fresh_global_or_constr env sigma poly cr in let cty = Retyping.get_type_of env sigma c in let try_apply f = - try Some (f (c, cty, ctx)) with Failure _ -> None in + try + let (_, hint) as ans = f (c, cty, ctx) in + match hint.code.obj with + | ERes_pf _ -> if not eapply then None else Some ans + | _ -> Some ans + with Failure _ -> None + in let ents = List.map_filter try_apply [make_exact_entry env sigma info ~poly ?name; - make_apply_entry env sigma flags info ~poly ?name] + make_apply_entry env sigma hnf info ~poly ?name] in if check && List.is_empty ents then user_err ~hdr:"Hint" (pr_leconstr_env env sigma c ++ spc() ++ - (if pi1 flags then str"cannot be used as a hint." + (if eapply then str"cannot be used as a hint." else str "can be used as a hint only for eauto.")); ents @@ -937,7 +929,7 @@ let make_resolve_hyp env sigma decl = let hname = NamedDecl.get_id decl in let c = mkVar hname in try - [make_apply_entry env sigma (true, true, false) empty_hint_info ~poly:false + [make_apply_entry env sigma true empty_hint_info ~poly:false ~name:(PathHints [GlobRef.VarRef hname]) (c, NamedDecl.get_type decl, Univ.ContextSet.empty)] with @@ -1223,9 +1215,28 @@ let add_resolves env sigma clist ~local ~superglobal dbnames = (fun dbname -> let r = List.flatten (List.map (fun (pri, poly, hnf, path, gr) -> - make_resolves env sigma (true,hnf,not !Flags.quiet) + make_resolves env sigma (true, hnf) pri ~check:true ~poly ~name:path gr) clist) in + let check (_, hint) = match hint.code.obj with + | ERes_pf (c, cty, ctx, _) -> + let sigma' = Evd.merge_context_set univ_flexible sigma ctx in + let ce = mk_clenv_from_env env sigma' None (c,cty) in + let miss = clenv_missing ce in + let nmiss = List.length miss in + let variables = str (CString.plural nmiss "variable") in + Feedback.msg_info ( + strbrk "The hint " ++ + pr_leconstr_env env sigma' c ++ + strbrk " will only be used by eauto, because applying " ++ + pr_leconstr_env env sigma' c ++ + strbrk " would leave " ++ variables ++ Pp.spc () ++ + Pp.prlist_with_sep Pp.pr_comma Name.print (List.map (Evd.meta_name ce.evd) miss) ++ + strbrk " as unresolved existential " ++ variables ++ str "." + ) + | _ -> () + in + let () = if not !Flags.quiet then List.iter check r in let hint = make_hint ~local dbname (AddHints { superglobal; hints = r }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames @@ -1375,10 +1386,10 @@ let expand_constructor_hints env sigma lems = let constructor_hints env sigma eapply lems = let lems = expand_constructor_hints env sigma lems in List.map_append (fun (poly, lem) -> - make_resolves env sigma (eapply,true,false) empty_hint_info ~check:true ~poly lem) lems + make_resolves env sigma (eapply, true) empty_hint_info ~check:true ~poly lem) lems let make_resolves env sigma info ~check ~poly ?name hint = - make_resolves env sigma (true, false, false) info ~check ~poly ?name hint + make_resolves env sigma (true, false) info ~check ~poly ?name hint let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in diff --git a/tactics/inv.ml b/tactics/inv.ml index 4b94dd0e72..41899132a6 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -409,7 +409,7 @@ let nLastDecls i tac = let rewrite_equations as_mode othin neqns names ba = Proofview.Goal.enter begin fun gl -> - let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in + let (depids,nodepids) = split_dep_and_nodep ba gl in let first_eq = ref Logic.MoveLast in let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in match othin with @@ -463,7 +463,7 @@ let raw_inversion inv_kind id status names = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let c = mkVar id in - let (ind, t) = + let ((ind, u), t) = try pf_apply Tacred.reduce_to_atomic_ind gl (pf_get_type_of gl c) with UserError _ -> let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in @@ -474,13 +474,12 @@ let raw_inversion inv_kind id status names = let (elim_predicate, args) = make_inv_predicate env evdref indf realargs id status concl in let sigma = !evdref in - let (cut_concl,case_tac) = - if status != NoDep && (local_occur_var sigma id concl) then - Reductionops.beta_applist sigma (elim_predicate, realargs@[c]), - case_then_using + let dep = status != NoDep && (local_occur_var sigma id concl) in + let cut_concl = + if dep then + Reductionops.beta_applist sigma (elim_predicate, realargs@[c]) else - Reductionops.beta_applist sigma (elim_predicate, realargs), - case_nodep_then_using + Reductionops.beta_applist sigma (elim_predicate, realargs) in let refined id = let prf = mkApp (mkVar id, args) in @@ -488,13 +487,11 @@ let raw_inversion inv_kind id status names = in let neqns = List.length realargs in let as_mode = names != None in + let (_, args) = decompose_app_vect sigma t in tclTHEN (Proofview.Unsafe.tclEVARS sigma) (tclTHENS (assert_before Anonymous cut_concl) - [case_tac names - (introCaseAssumsThen false (* ApplyOn not supported by inversion *) - (rewrite_equations_tac as_mode inv_kind id neqns)) - (Some elim_predicate) ind (c,t); + [case_tac dep names (rewrite_equations_tac as_mode inv_kind id neqns) elim_predicate (ind, u, args) id; onLastHypId (fun id -> tclTHEN (refined id) reflexivity)]) end diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index ec770e2473..fc099f643d 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -14,10 +14,8 @@ open Util open Names open Constr open EConstr -open Termops open Declarations open Tacmach -open Clenv open Tactypes module RelDecl = Context.Rel.Declaration @@ -335,18 +333,6 @@ let ifOnHyp pred tac1 tac2 id gl = used to keep track of some information about the ``branches'' of the elimination. *) -type branch_args = { - ity : pinductive; (* the type we were eliminating on *) - branchnum : int; (* the branch number *) - nassums : int; (* number of assumptions/letin to be introduced *) - branchsign : bool list; (* the signature of the branch. - true=assumption, false=let-in *) - branchnames : intro_patterns} - -type branch_assumptions = { - ba : branch_args; (* the branch args *) - assums : named_context} (* the list of assumptions introduced *) - let fix_empty_or_and_pattern nv l = (* 1- The syntax does not distinguish between "[ ]" for one clause with no names and "[ ]" for no clause at all *) @@ -401,15 +387,13 @@ let get_and_check_or_and_pattern_gen ?loc check_and names branchsigns = let get_and_check_or_and_pattern ?loc = get_and_check_or_and_pattern_gen ?loc true -let compute_induction_names_gen check_and branchletsigns = function +let compute_induction_names check_and branchletsigns = function | None -> Array.make (Array.length branchletsigns) [] | Some {CAst.loc;v=names} -> let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in get_and_check_or_and_pattern_gen check_and ?loc names branchletsigns -let compute_induction_names = compute_induction_names_gen true - (* Compute the let-in signature of case analysis or standard induction scheme *) let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = let rec analrec c recargs = @@ -844,60 +828,6 @@ module New = struct tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl) end - (* Find the right elimination suffix corresponding to the sort of the goal *) - (* c should be of type A1->.. An->B with B an inductive definition *) - let general_elim_then_using mk_elim - rec_flag allnames tac predicate ind (c, t) = - Proofview.Goal.enter begin fun gl -> - let sigma, elim = mk_elim ind gl in - let ind = on_snd (fun u -> EInstance.kind sigma u) ind in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Proofview.Goal.enter begin fun gl -> - let indclause = mk_clenv_from gl (c, t) in - (* applying elimination_scheme just a little modified *) - let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim) in - let indmv = - match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with - | Meta mv -> mv - | _ -> anomaly (str"elimination.") - in - let pmv = - let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in - match EConstr.kind elimclause.evd p with - | Meta p -> p - | _ -> - let name_elim = - match EConstr.kind sigma elim with - | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim - | _ -> mt () - in - user_err ~hdr:"Tacticals.general_elim_then_using" - (str "The elimination combinator " ++ name_elim ++ str " is unknown.") - in - let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in - let branchsigns = compute_constructor_signatures ~rec_flag ind in - let brnames = compute_induction_names_gen false branchsigns allnames in - let flags = Unification.elim_flags () in - let elimclause' = - match predicate with - | None -> elimclause' - | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause' - in - let after_tac i = - let ba = { branchsign = branchsigns.(i); - branchnames = brnames.(i); - nassums = List.length branchsigns.(i); - branchnum = i+1; - ity = ind; } - in - tac ba - in - let branchtacs = List.init (Array.length branchsigns) after_tac in - Proofview.tclTHEN - (Clenv.res_pf ~flags elimclause') - (Proofview.tclEXTEND [] tclIDTAC branchtacs) - end) end - let elimination_sort_of_goal gl = (* Retyping will expand evars anyway. *) let c = Proofview.Goal.concl gl in @@ -912,68 +842,6 @@ module New = struct | None -> elimination_sort_of_goal gl | Some id -> elimination_sort_of_hyp id gl - (* computing the case/elim combinators *) - - let gl_make_elim ind = begin fun gl -> - let env = Proofview.Goal.env gl in - let gr = Indrec.lookup_eliminator env (fst ind) (elimination_sort_of_goal gl) in - let (sigma, c) = pf_apply Evd.fresh_global gl gr in - (sigma, c) - end - - let gl_make_case_dep (ind, u) = begin fun gl -> - let sigma = project gl in - let u = EInstance.kind (project gl) u in - let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true - (elimination_sort_of_goal gl) - in - (sigma, EConstr.of_constr r) - end - - let gl_make_case_nodep (ind, u) = begin fun gl -> - let sigma = project gl in - let u = EInstance.kind sigma u in - let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false - (elimination_sort_of_goal gl) - in - (sigma, EConstr.of_constr r) - end - - let make_elim_branch_assumptions ba hyps = - let assums = - try List.rev (List.firstn ba.nassums hyps) - with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions.") in - { ba = ba; assums = assums } - - let elim_on_ba tac ba = - Proofview.Goal.enter begin fun gl -> - let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in - tac branches - end - - let case_on_ba tac ba = - Proofview.Goal.enter begin fun gl -> - let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in - tac branches - end - - let elimination_then tac c = - Proofview.Goal.enter begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl c) in - let isrec,mkelim = - match (Global.lookup_mind (fst (fst ind))).mind_record with - | NotRecord -> true,gl_make_elim - | FakeRecord | PrimRecord _ -> false,gl_make_case_dep - in - general_elim_then_using mkelim isrec None tac None ind (c, t) - end - - let case_then_using = - general_elim_then_using gl_make_case_dep false - - let case_nodep_then_using = - general_elim_then_using gl_make_case_nodep false - let pf_constr_of_global ref = Proofview.tclEVARMAP >>= fun sigma -> Proofview.tclENV >>= fun env -> diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 48a06e6e1d..bfead34b3b 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Constr open EConstr open Evd open Locus @@ -94,18 +93,6 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic (** {6 Elimination tacticals. } *) -type branch_args = private { - ity : pinductive; (** the type we were eliminating on *) - branchnum : int; (** the branch number *) - nassums : int; (** number of assumptions/letin to be introduced *) - branchsign : bool list; (** the signature of the branch. - true=assumption, false=let-in *) - branchnames : intro_patterns} - -type branch_assumptions = private { - ba : branch_args; (** the branch args *) - assums : named_context} (** the list of assumptions introduced *) - (** [get_and_check_or_and_pattern loc pats branchsign] returns an appropriate error message if |pats| <> |branchsign|; extends them if no pattern is given for let-ins in the case of a conjunctive pattern *) @@ -122,7 +109,7 @@ val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool lis (** Useful for [as intro_pattern] modifier *) val compute_induction_names : - bool list array -> or_and_intro_pattern option -> intro_patterns array + bool -> bool list array -> or_and_intro_pattern option -> intro_patterns array val elimination_sort_of_goal : Goal.goal sigma -> Sorts.family val elimination_sort_of_hyp : Id.t -> Goal.goal sigma -> Sorts.family @@ -249,20 +236,5 @@ module New : sig val elimination_sort_of_hyp : Id.t -> Proofview.Goal.t -> Sorts.family val elimination_sort_of_clause : Id.t option -> Proofview.Goal.t -> Sorts.family - val elimination_then : - (branch_args -> unit Proofview.tactic) -> - constr -> unit Proofview.tactic - - val case_then_using : - or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic - - val case_nodep_then_using : - or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic - - val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic - val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic - val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index eb7b7e363f..d33f3a5062 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2330,7 +2330,7 @@ let intro_decomp_eq ?loc l thin tac id = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma, t = Typing.type_of env sigma c in - let _,t = reduce_to_quantified_ind env sigma t in + let _,t = reduce_to_atomic_ind env sigma t in match my_find_eq_data_decompose env sigma t with | Some (eq,u,eq_args) -> !intro_decomp_eq_function @@ -3248,13 +3248,10 @@ let rec consume_pattern avoid na isdep gl = let open CAst in function | {loc;v=IntroForthcoming true}::names when not isdep -> consume_pattern avoid na isdep gl names | {loc;v=IntroForthcoming _}::names as fullpat -> - let avoid = Id.Set.union avoid (explicit_intro_names names) in (CAst.make ?loc @@ intropattern_of_name gl avoid na, fullpat) | {loc;v=IntroNaming IntroAnonymous}::names -> - let avoid = Id.Set.union avoid (explicit_intro_names names) in (CAst.make ?loc @@ intropattern_of_name gl avoid na, names) | {loc;v=IntroNaming (IntroFresh id')}::names -> - let avoid = Id.Set.union avoid (explicit_intro_names names) in (CAst.make ?loc @@ IntroNaming (IntroIdentifier (new_fresh_id avoid id' gl)), names) | pat::names -> (pat,names) @@ -3312,7 +3309,7 @@ let get_recarg_dest (recargdests,tophyp) = *) let induct_discharge with_evars dests avoid' tac (avoid,ra) names = - let avoid = Id.Set.union avoid avoid' in + let avoid = Id.Set.union avoid' (Id.Set.union avoid (explicit_intro_names names)) in let rec peel_tac ra dests names thin = match ra with | (RecArg,_,deprec,recvarname) :: @@ -3320,7 +3317,7 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = Proofview.Goal.enter begin fun gl -> let (recpat,names) = match names with | [{CAst.loc;v=IntroNaming (IntroIdentifier id)} as pat] -> - let id' = next_ident_away (add_prefix "IH" id) avoid in + let id' = new_fresh_id avoid (add_prefix "IH" id) gl in (pat, [CAst.make @@ IntroNaming (IntroIdentifier id')]) | _ -> consume_pattern avoid (Name recvarname) deprec gl names in let dest = get_recarg_dest dests in @@ -4397,7 +4394,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let branchletsigns = let f (_,is_not_let,_,_) = is_not_let in Array.map (fun (_,l) -> List.map f l) indsign in - let names = compute_induction_names branchletsigns names in + let names = compute_induction_names true branchletsigns names in Array.iter (check_name_unicity env toclear []) names; let tac = (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) 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_12909.v b/test-suite/bugs/closed/bug_12909.v new file mode 100644 index 0000000000..fafb6a418f --- /dev/null +++ b/test-suite/bugs/closed/bug_12909.v @@ -0,0 +1,8 @@ +Module Type T. +Axiom A : Type. +End T. + +Module M. + Axiom A : SProp. +End M. +Fail Module N <: T := M. 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_12944.v b/test-suite/bugs/closed/bug_12944.v new file mode 100644 index 0000000000..d6720d9906 --- /dev/null +++ b/test-suite/bugs/closed/bug_12944.v @@ -0,0 +1,12 @@ + +Inductive vector A : nat -> Type := + |nil : vector A 0 + |cons : forall (h:A) (n:nat), vector A n -> vector A (S n). + +Global Set Mangle Names. + +Lemma vlookup_middle {A n} (v : vector A n) : True. +Proof. + induction v as [|?? IHv]. + all:exact I. +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/Arguments.out b/test-suite/output/Arguments.out index 8cf0797b17..5d1da05809 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -43,7 +43,7 @@ forall {D1 C1 : Type}, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 pf is not universe polymorphic -Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] : simpl never +Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] _ _ : simpl never The reduction tactics never unfold pf pf is transparent Expands to: Constant Arguments.pf diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index c28bb14eb3..e46774f68a 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -13,21 +13,25 @@ where ?y : [ |- nat] Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -Arguments eq {A}%type_scope -Arguments eq_refl {B}%type_scope {y}, [B] _ -eq_refl : forall {A : Type} {x : A}, x = x +Arguments eq {A}%type_scope _ _ +Arguments eq_refl {B}%type_scope {y}, [_] _ + (where some original arguments have been renamed) +eq_refl : forall {B : Type} {y : B}, y = y eq_refl is not universe polymorphic -Arguments eq_refl {B}%type_scope {y}, [B] _ +Arguments eq_refl {B}%type_scope {y}, [_] _ + (where some original arguments have been renamed) Expands to: Constructor Coq.Init.Logic.eq_refl Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x -Arguments myEq _%type_scope -Arguments myrefl {C}%type_scope x : rename -myrefl : forall {B : Type} (x : A), B -> myEq B x x +Arguments myEq _%type_scope _ _ +Arguments myrefl {C}%type_scope x _ + (where some original arguments have been renamed) +myrefl : forall {C : Type} (x : A), C -> myEq C x x myrefl is not universe polymorphic -Arguments myrefl {C}%type_scope x : rename +Arguments myrefl {C}%type_scope x _ + (where some original arguments have been renamed) Expands to: Constructor Arguments_renaming.Test1.myrefl myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := @@ -37,11 +41,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename -myplus : forall {T : Type}, T -> nat -> nat -> nat +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope + (where some original arguments have been renamed) +myplus : forall {Z : Type}, Z -> nat -> nat -> nat myplus is not universe polymorphic -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope + (where some original arguments have been renamed) The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent @@ -51,12 +57,14 @@ Expands to: Constant Arguments_renaming.Test1.myplus Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x -Arguments myEq (_ _)%type_scope -Arguments myrefl A%type_scope {C}%type_scope x : rename -myrefl : forall (A : Type) {B : Type} (x : A), B -> myEq A B x x +Arguments myEq (_ _)%type_scope _ _ +Arguments myrefl A%type_scope {C}%type_scope x _ + (where some original arguments have been renamed) +myrefl : forall (A : Type) {C : Type} (x : A), C -> myEq A C x x myrefl is not universe polymorphic -Arguments myrefl A%type_scope {C}%type_scope x : rename +Arguments myrefl A%type_scope {C}%type_scope x _ + (where some original arguments have been renamed) Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x @@ -68,11 +76,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename -myplus : forall {T : Type}, T -> nat -> nat -> nat +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope + (where some original arguments have been renamed) +myplus : forall {Z : Type}, Z -> nat -> nat -> nat myplus is not universe polymorphic -Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope + (where some original arguments have been renamed) The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent @@ -87,6 +97,9 @@ The command has indeed failed with message: Argument number 3 is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ]. The command has indeed failed with message: +Argument z is a trailing implicit, so it can't be declared non maximal. +Please use { } instead of [ ]. +The command has indeed failed with message: Extra arguments: y. The command has indeed failed with message: Flag "rename" expected to rename A into R. diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 6001850046..13bda0c070 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -48,6 +48,7 @@ Check @myplus. Fail Arguments eq_refl {F g}, [H] k. Fail Arguments eq_refl {F}, [F] : rename. +Fail Arguments eq {A} x [_] : rename. Fail Arguments eq {A} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 6976610b22..da2fc90fc3 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -7,7 +7,7 @@ fix F (t : t) : P t := : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t -Arguments t_rect (_ _)%function_scope +Arguments t_rect (_ _)%function_scope _ = fun d : TT => match d with | {| f3 := b |} => b end @@ -26,7 +26,7 @@ match Nat.eq_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y -Arguments proj (_ _)%nat_scope _%function_scope +Arguments proj (_ _)%nat_scope _%function_scope _ _ foo = fix foo (A : Type) (l : list A) {struct l} : option A := match l with @@ -43,7 +43,7 @@ fun (A : Type) (x : I A) => match x with end : forall A : Type, I A -> A -Arguments uncast _%type_scope +Arguments uncast _%type_scope _ foo' = if A 0 then true else false : bool f = diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index d8b88b8c1c..781e8e13a3 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -Arguments d2 [x x]%nat_scope +Arguments d2 [x x]%nat_scope _ map id (1 :: nil) : list nat map id' (1 :: nil) diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index e6c2806433..8e10107673 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -7,7 +7,7 @@ l : list' A Unable to unify "list' (A * A)%type" with "list' A". Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x -Arguments foo _%type_scope -Arguments Foo _%type_scope +Arguments foo _%type_scope _ +Arguments Foo _%type_scope _ myprod unit bool : Set diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index da255e86cd..02e58775b5 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -2,7 +2,7 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} Arguments sig2 [A]%type_scope (_ _)%type_scope -Arguments exist2 [A]%type_scope (_ _)%function_scope +Arguments exist2 [A]%type_scope (_ _)%function_scope _ _ _ exists x : nat, x = x : Prop fun b : bool => if b then b else b 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/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index bdfa8afb6a..b8daa69ad2 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -15,7 +15,7 @@ swap = fun (A B : Type) '(x, y) => (y, x) : forall A B : Type, A * B -> B * A -Arguments swap {A B}%type_scope +Arguments swap {A B}%type_scope _ fun (A B : Type) '(x, y) => swap (x, y) = (y, x) : forall A B : Type, A * B -> Prop forall (A B : Type) '(x, y), swap (x, y) = (y, x) diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 8fb267e343..fe16dba496 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,24 +1,24 @@ existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x} existT is template universe polymorphic on sigT.u0 sigT.u1 -Arguments existT [A]%type_scope _%function_scope +Arguments existT [A]%type_scope _%function_scope _ _ Expands to: Constructor Coq.Init.Specif.existT Inductive sigT (A : Type) (P : A -> Type) : Type := existT : forall x : A, P x -> {x : A & P x} Arguments sigT [A]%type_scope _%type_scope -Arguments existT [A]%type_scope _%function_scope +Arguments existT [A]%type_scope _%function_scope _ _ existT : forall [A : Type] (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -Arguments eq {A}%type_scope -Arguments eq_refl {A}%type_scope {x}, [A] _ +Arguments eq {A}%type_scope _ _ +Arguments eq_refl {A}%type_scope {x}, [_] _ eq_refl : forall {A : Type} {x : A}, x = x eq_refl is not universe polymorphic -Arguments eq_refl {A}%type_scope {x}, [A] _ +Arguments eq_refl {A}%type_scope {x}, [_] _ Expands to: Constructor Coq.Init.Logic.eq_refl eq_refl : forall {A : Type} {x : A}, x = x @@ -54,7 +54,7 @@ Inductive le (n : nat) : nat -> Prop := Arguments le (_ _)%nat_scope Arguments le_n _%nat_scope -Arguments le_S {n}%nat_scope [m]%nat_scope +Arguments le_S {n}%nat_scope [m]%nat_scope _ comparison : Set comparison is not universe polymorphic @@ -80,8 +80,8 @@ Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -Arguments eq {A}%type_scope -Arguments eq_refl {A}%type_scope {x}, {A} _ +Arguments eq {A}%type_scope _ _ +Arguments eq_refl {A}%type_scope {x}, {_} _ n:nat Hypothesis of the goal context. diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out index 1dd89c9bcd..1cdb39b020 100644 --- a/test-suite/output/Projections.out +++ b/test-suite/output/Projections.out @@ -7,11 +7,11 @@ let B := A in fun (C : Type) (u : U A C) => (A, B, C, c _ _ u) let B := A in forall C : Type, U A C -> Type * Type * Type * (B * A * C) -Arguments a (_ _)%type_scope +Arguments a (_ _)%type_scope _ b = fun A : Type => let B := A in fun (C : Type) (u : U A C) => b _ _ u : forall A : Type, let B := A in forall (C : Type) (u : U A C), (A, B, C, c _ _ u) = (A, B, C, c _ _ u) -Arguments b (_ _)%type_scope +Arguments b (_ _)%type_scope _ diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index edd2c9674f..163ed15606 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -5,24 +5,24 @@ Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } PWrap has primitive projections with eta conversion. Arguments PWrap _%type_scope -Arguments pwrap _%type_scope +Arguments pwrap _%type_scope _ punwrap@{u} = fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p : forall A : Type@{u}, PWrap@{u} A -> A (* u |= *) -Arguments punwrap _%type_scope +Arguments punwrap _%type_scope _ Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } (* u |= *) Arguments RWrap _%type_scope -Arguments rwrap _%type_scope +Arguments rwrap _%type_scope _ runwrap@{u} = fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap : forall A : Type@{u}, RWrap@{u} A -> A (* u |= *) -Arguments runwrap _%type_scope +Arguments runwrap _%type_scope _ Wrap@{u} = fun A : Type@{u} => A : Type@{u} -> Type@{u} (* u |= *) @@ -87,12 +87,12 @@ Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } PWrap has primitive projections with eta conversion. Arguments PWrap _%type_scope -Arguments pwrap _%type_scope +Arguments pwrap _%type_scope _ punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A (* K |= *) punwrap is universe polymorphic -Arguments punwrap _%type_scope +Arguments punwrap _%type_scope _ punwrap is transparent Expands to: Constant UnivBinders.punwrap The command has indeed failed with message: diff --git a/test-suite/output/bug_12887.out b/test-suite/output/bug_12887.out new file mode 100644 index 0000000000..5ea7722bc6 --- /dev/null +++ b/test-suite/output/bug_12887.out @@ -0,0 +1,10 @@ +The command has indeed failed with message: +Cannot infer this placeholder of type "Type" in +environment: +Functor : (Type -> Type) -> Type +F : Type -> Type +fmap : forall A B : Type, (A -> B) -> F A -> F B +The command has indeed failed with message: +Cannot infer an existential variable of type "nat" in +environment: +R : nat -> Type diff --git a/test-suite/output/bug_12887.v b/test-suite/output/bug_12887.v new file mode 100644 index 0000000000..4208c3e8e9 --- /dev/null +++ b/test-suite/output/bug_12887.v @@ -0,0 +1,10 @@ +Arguments id {_} _. + +Fail Record Functor (F : Type -> Type) := { + fmap : forall A B, (A -> B) -> F A -> F B; + fmap_identity : fmap _ _ id = id; +}. + +Fail Inductive R (x:nat) := { y : R ltac:(clear x) }. + +Inductive R (x:nat) := { y : bool; z : R _ }. diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 73fe53c757..a39b17e1f1 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -196,3 +196,13 @@ Goal forall m n:nat, n=m. double induction m n. Abort. +(* Mentioned as part of bug #12944 *) + +Inductive test : Set := cons : forall (IHv : nat) (v : test), test. + +Goal test -> test. +induction 1 as [? IHv]. +Undo. +destruct 1 as [? IHv]. +exact IHv. (* Check that the name is granted *) +Qed. 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/coqloop.ml b/toplevel/coqloop.ml index 9917ae0f01..88924160ff 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -324,11 +324,11 @@ let loop_flush_all () = let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2 let evleq e1 e2 = CList.equal Evar.equal e1 e2 let cproof p1 p2 = - let Proof.{goals=a1;stack=a2;shelf=a3;sigma=sigma1} = Proof.data p1 in - let Proof.{goals=b1;stack=b2;shelf=b3;sigma=sigma2} = Proof.data p2 in + let Proof.{goals=a1;stack=a2;sigma=sigma1} = Proof.data p1 in + let Proof.{goals=b1;stack=b2;sigma=sigma2} = Proof.data p2 in evleq a1 b1 && CList.equal (pequal evleq evleq) a2 b2 && - CList.equal Evar.equal a3 b3 && + CList.equal Evar.equal (Evd.shelf sigma1) (Evd.shelf sigma2) && Evar.Set.equal (Evd.given_up sigma1) (Evd.given_up sigma2) let drop_last_doc = ref None 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)) diff --git a/vernac/classes.ml b/vernac/classes.ml index 82a1e32a14..02cb60f1cf 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -359,7 +359,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id consequence, we use the low-level primitives to code the refinement manually.*) let future_goals, sigma = Evd.pop_future_goals sigma in - let gls = List.rev_append future_goals.Evd.FutureGoals.shelf (List.rev future_goals.Evd.FutureGoals.comb) in + let gls = List.rev future_goals.Evd.FutureGoals.comb in let sigma = Evd.push_future_goals sigma in let kind = Decls.(IsDefinition Instance) in let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index be9cc059a7..adf1f42beb 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -218,9 +218,8 @@ let vernac_arguments ~section_local reference args more_implicits flags = in let implicits = implicits :: more_implicits in - let implicits = List.map (List.map snd) implicits in let implicits_specified = match implicits with - | [l] -> List.exists (function Glob_term.Explicit -> false | _ -> true) l + | [l] -> List.exists (function _, Glob_term.Explicit -> false | _ -> true) l | _ -> true in if implicits_specified && clear_implicits_flag then diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 673124296d..452de69b1d 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -451,7 +451,7 @@ let interp_params env udecl uparamsl paramsl = do the unification. [env_ar_par] is [uparams; inds; params] *) -let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams c = +let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams ~binders:k c = let is_ind sigma k c = match EConstr.kind sigma c with | Constr.Rel n -> (* env is [uparams; inds; params; k other things] *) @@ -462,14 +462,18 @@ let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams c = | Constr.App (h,args) when is_ind sigma k h -> Array.fold_left_i (fun i sigma arg -> if i >= nparams || not (EConstr.isEvar sigma arg) then sigma - else Evarconv.unify_delay env sigma arg (EConstr.mkRel (k+nparams-i))) + else begin try Evarconv.unify_delay env sigma arg (EConstr.mkRel (k+nparams-i)) + with Evarconv.UnableToUnify _ -> + (* ignore errors, we will get a "Cannot infer ..." error instead *) + sigma + end) sigma args | _ -> Termops.fold_constr_with_full_binders sigma (fun d (env,k) -> EConstr.push_rel d env, k+1) aux envk sigma c in - aux (env_ar_par,0) sigma c + aux (env_ar_par,k) sigma c let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite = check_all_names_different indl; @@ -527,7 +531,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let sigma = List.fold_left (fun sigma (_,ctyps,_) -> List.fold_left (fun sigma ctyp -> - maybe_unify_params_in env_ar_params sigma ~ninds ~nparams ctyp) + maybe_unify_params_in env_ar_params sigma ~ninds ~nparams ~binders:0 ctyp) sigma ctyps) sigma constructors in diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 9c876787a3..91e8f609d5 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -81,8 +81,8 @@ val template_polymorphism_candidate monomorphic universe context that can be made parametric in its conclusion sort, if one is given. *) -val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int +val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int -> binders:int -> EConstr.t -> Evd.evar_map (** [nparams] is the number of parameters which aren't treated as uniform, ie the length of params (including letins) where the env - is [uniform params, inductives, params]. *) + is [uniform params, inductives, params, binders]. *) diff --git a/vernac/declare.ml b/vernac/declare.ml index 28e6f21d41..099a63cf8f 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1553,11 +1553,11 @@ let set_used_variables ps l = ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) } let get_open_goals ps = - let Proof.{ goals; stack; shelf } = Proof.data ps.proof in + let Proof.{ goals; stack; sigma } = Proof.data ps.proof in List.length goals + List.fold_left (+) 0 (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) + - List.length shelf + List.length (Evd.shelf sigma) type proof_object = { name : Names.Id.t @@ -1734,8 +1734,8 @@ let return_proof ps = let p, uctx = prepare_proof ~unsafe_typ:false ps in List.map (fun (((_ub, body),eff),_) -> (body,eff)) p, uctx -let update_global_env = - map ~f:(fun p -> Proof.update_sigma_env p (Global.env ())) +let update_sigma_univs ugraph p = + map ~f:(Proof.update_sigma_univs ugraph) p let next = let n = ref 0 in fun () -> incr n; !n @@ -2014,7 +2014,7 @@ let finish_derived ~f ~name ~entries = let lemma_def = Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in let lemma_def = DefinitionEntry lemma_def in let ct = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in - [GlobRef.ConstRef ct] + [GlobRef.ConstRef f_kn; GlobRef.ConstRef ct] let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 = @@ -2251,7 +2251,7 @@ let rec solve_obligation prg num tac = let scope = Locality.Global Locality.ImportNeedQualified in let kind = kind_of_obligation (snd obl.obl_status) in let evd = Evd.from_ctx (Internal.get_uctx prg) in - let evd = Evd.update_sigma_env evd (Global.env ()) in + let evd = Evd.update_sigma_univs (Global.universes ()) evd in let auto ~pm n oblset tac = auto_solve_obligations ~pm n ~oblset tac in let proof_ending = let name = Internal.get_name prg in @@ -2292,7 +2292,7 @@ and solve_obligation_by_tac prg obls i tac = | None -> !default_tactic in let uctx = Internal.get_uctx prg in - let uctx = UState.update_sigma_env uctx (Global.env ()) in + let uctx = UState.update_sigma_univs uctx (Global.universes ()) in let poly = Internal.get_poly prg in match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac ~poly ~uctx with | None -> None diff --git a/vernac/declare.mli b/vernac/declare.mli index 3001d0d206..1ad79928d5 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -246,10 +246,10 @@ module Proof : sig val compact : t -> t - (** Update the proofs global environment after a side-effecting command - (e.g. a sublemma definition) has been run inside it. Assumes - there_are_pending_proofs. *) - val update_global_env : t -> t + (** Update the proof's universe information typically after a + side-effecting command (e.g. a sublemma definition) has been run + inside it. *) + val update_sigma_univs : UGraph.t -> t -> t val get_open_goals : t -> int diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 2b46542287..8b00484b4a 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -75,12 +75,12 @@ let print_ref reduce ref udecl = let inst = Univ.make_abstract_instance univs in let bl = Printer.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in - let typ = EConstr.of_constr typ in let typ = if reduce then - let ctx,ccl = Reductionops.splay_prod_assum env sigma typ - in EConstr.it_mkProd_or_LetIn ccl ctx + let ctx,ccl = Reductionops.splay_prod_assum env sigma (EConstr.of_constr typ) + in EConstr.to_constr sigma (EConstr.it_mkProd_or_LetIn ccl ctx) else typ in + let typ = Arguments_renaming.rename_type typ ref in let impargs = select_stronger_impargs (implicits_of_global ref) in let impargs = List.map binding_kind_of_status impargs in let variance = let open GlobRef in match ref with @@ -95,7 +95,7 @@ let print_ref reduce ref udecl = else mt () in let priv = None in (* We deliberately don't print private univs in About. *) - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma ~impargs typ ++ + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_ltype_env env sigma ~impargs typ ++ Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv) (********************************) @@ -261,6 +261,10 @@ let implicit_kind_of_status = function | None -> Anonymous, Glob_term.Explicit | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit +let extra_implicit_kind_of_status imp = + let _,imp = implicit_kind_of_status imp in + (Anonymous, imp) + let dummy = { Vernacexpr.implicit_status = Glob_term.Explicit; name = Anonymous; @@ -268,8 +272,10 @@ let dummy = { notation_scope = None; } -let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} = - name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit +let is_dummy = function + | Vernacexpr.(RealArg {implicit_status; name; recarg_like; notation_scope}) -> + name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit + | _ -> false let rec main_implicits i renames recargs scopes impls = if renames = [] && recargs = [] && scopes = [] && impls = [] then [] @@ -292,9 +298,7 @@ let rec main_implicits i renames recargs scopes impls = let tl = function [] -> [] | _::tl -> tl in (* recargs is special -> tl handled above *) let rest = main_implicits (i+1) (tl renames) recargs (tl scopes) (tl impls) in - if is_dummy status && rest = [] - then [] (* we may have a trail of dummies due to eg "clear scopes" *) - else status :: rest + status :: rest let rec insert_fake_args volatile bidi impls = let open Vernacexpr in @@ -320,11 +324,7 @@ let print_arguments ref = | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs in - let flags, renames = match Arguments_renaming.arguments_names ref with - | exception Not_found -> flags, [] - | [] -> flags, [] - | renames -> `Rename::flags, renames - in + let renames = try Arguments_renaming.arguments_names ref with Not_found -> [] in let scopes = Notation.find_arguments_scope ref in let flags = if needs_extra_scopes ref scopes then `ExtraScopes::flags else flags in let impls = Impargs.extract_impargs_data (Impargs.implicits_of_global ref) in @@ -333,15 +333,17 @@ let print_arguments ref = | [] -> assert false in let impls = main_implicits 0 renames recargs scopes impls in - let moreimpls = List.map (fun (_,i) -> List.map implicit_kind_of_status i) moreimpls in + let moreimpls = List.map (fun (_,i) -> List.map extra_implicit_kind_of_status i) moreimpls in let bidi = Pretyping.get_bidirectionality_hint ref in let impls = insert_fake_args nargs_for_red bidi impls in - if impls = [] && moreimpls = [] && flags = [] then [] + if List.for_all is_dummy impls && moreimpls = [] && flags = [] then [] else let open Constrexpr in let open Vernacexpr in [Ppvernac.pr_vernac_expr - (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags))] + (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags)) ++ + (if renames = [] then mt () else + fnl () ++ str " (where some original arguments have been renamed)")] let print_name_infos ref = let type_info_for_implicit = diff --git a/vernac/record.ml b/vernac/record.ml index d0036e40f9..bd5b71cd6b 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -81,12 +81,12 @@ let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l = (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls)) (env, sigma, [], [], impls_env) nots l in - let _, sigma = Context.Rel.fold_outside ~init:(env,sigma) (fun f (env,sigma) -> + let _, _, sigma = Context.Rel.fold_outside ~init:(env,0,sigma) (fun f (env,k,sigma) -> let sigma = RelDecl.fold_constr (fun c sigma -> - ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams c) + ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams ~binders:k c) f sigma in - EConstr.push_rel f env, sigma) + EConstr.push_rel f env, k+1, sigma) newfs in sigma, (impls, newfs) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 540e85621a..6a4c2a626d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -112,7 +112,8 @@ let show_proof ~pstate = let show_top_evars ~proof = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) - let Proof.{goals;shelf;sigma} = Proof.data proof in + let Proof.{goals; sigma} = Proof.data proof in + let shelf = Evd.shelf sigma in let given_up = Evar.Set.elements @@ Evd.given_up sigma in pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma) diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 6be2fb0d43..edf48fef1a 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -211,8 +211,11 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) = (fun ~st -> let before_univs = Global.universes () in let pstack, pm = interp_expr ~atts:cmd.attrs ~st cmd.expr in - if before_univs == Global.universes () then pstack, pm - else Option.map (Vernacstate.LemmaStack.map_top ~f:Declare.Proof.update_global_env) pstack, pm) + let after_univs = Global.universes () in + if before_univs == after_univs then pstack, pm + else + let f = Declare.Proof.update_sigma_univs after_univs in + Option.map (Vernacstate.LemmaStack.map ~f) pstack, pm) ~st (* XXX: This won't properly set the proof mode, as of today, it is diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 6d12d72408..204008997d 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -80,7 +80,7 @@ module LemmaStack = struct type t = Declare.Proof.t * Declare.Proof.t list - let map f (pf, pfl) = (f pf, List.map f pfl) + let map ~f (pf, pfl) = (f pf, List.map f pfl) let map_top ~f (pf, pfl) = (f pf, pfl) let pop (ps, p) = match p with @@ -96,7 +96,7 @@ module LemmaStack = struct let get_all_proof_names (pf : t) = let prj x = Declare.Proof.get x in - let (pn, pns) = map Proof.(function pf -> (data (prj pf)).name) pf in + let (pn, pns) = map ~f:Proof.(function pf -> (data (prj pf)).name) pf in pn :: pns let copy_info src tgt = @@ -218,7 +218,7 @@ module Declare_ = struct Declare.Proof.info pt) let discard_all () = s_lemmas := None - let update_global_env () = dd (Declare.Proof.update_global_env) + let update_sigma_univs ugraph = dd (Declare.Proof.update_sigma_univs ugraph) let get_current_context () = cc Declare.Proof.get_current_context diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 5efdb3cc68..e1b13dcb73 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -40,6 +40,7 @@ module LemmaStack : sig val pop : t -> Declare.Proof.t * t option val push : t option -> Declare.Proof.t -> t + val map : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t val map_top : f:(Declare.Proof.t -> Declare.Proof.t) -> t -> t val with_top : t -> f:(Declare.Proof.t -> 'a ) -> 'a @@ -112,7 +113,7 @@ module Declare : sig val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof val discard_all : unit -> unit - val update_global_env : unit -> unit + val update_sigma_univs : UGraph.t -> unit val get_current_context : unit -> Evd.evar_map * Environ.env |