diff options
93 files changed, 1748 insertions, 1157 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 5dd376079..04b75bfdf 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -26,7 +26,7 @@ variables: COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev" #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386" COQIDE_OPAM: "lablgtk-extras" - COQIDE_OPAM_BE: "num lablgtk.2.18.6 lablgtk-extras.1.6" + COQIDE_OPAM_BE: "lablgtk.2.18.6 lablgtk-extras.1.6" COQDOC_PACKAGES: "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript transfig imagemagick tipa" COQDOC_OPAM: "hevea" @@ -49,7 +49,7 @@ before_script: - opam switch ${COMPILER} - eval $(opam config env) - opam config list - - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM} + - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind num ${EXTRA_OPAM} - rm -rf ~/.opam/log/ - opam list diff --git a/.travis.yml b/.travis.yml index 481a63558..1699568ca 100644 --- a/.travis.yml +++ b/.travis.yml @@ -190,7 +190,7 @@ matrix: # Ocaml warnings with two compilers - env: - MAIN_TARGET="coqocaml" - - EXTRA_CONF="-byte-only -coqide byte -warn-error" + - EXTRA_CONF="-byte-only -coqide byte -warn-error yes" - EXTRA_OPAM="hevea ${LABLGTK}" # dummy target - BUILD_TARGET="clean" @@ -209,7 +209,7 @@ matrix: - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - - EXTRA_CONF="-byte-only -coqide byte -warn-error" + - EXTRA_CONF="-byte-only -coqide byte -warn-error yes" - EXTRA_OPAM="num hevea ${LABLGTK_BE}" # dummy target - BUILD_TARGET="clean" @@ -239,7 +239,7 @@ matrix: - CAMLP5_VER=".6.17" - NATIVE_COMP="no" - COQ_DEST="-prefix ${PWD}/_install" - - EXTRA_CONF="-coqide opt -warn-error" + - EXTRA_CONF="-coqide opt -warn-error yes" - EXTRA_OPAM="${LABLGTK}" before_install: - brew update @@ -63,6 +63,7 @@ Focusing - Focusing bracket `{` now supports single-numbered goal selector, e.g. `2: {` will focus on the second sub-goal. As usual, unfocus with `}` once the sub-goal is fully solved. + The `Focus` and `Unfocus` commands are now deprecated. Vernacular Commands @@ -73,6 +74,9 @@ Vernacular Commands was removed. Use Local as a prefix instead. - For the Extraction Language command, "OCaml" is spelled correctly. The older "Ocaml" is still accepted, but deprecated. +- Using “Require” inside a section is deprecated. +- An experimental command "Show Extraction" allows to extract the content + of the current ongoing proof (grant wish #4129). Universes @@ -89,6 +93,13 @@ Universes - `with Definition` now understands universe declarations (like `@{u| Set < u}`). +Tools + +- Coq can now be run with the option -mangle-names to change the auto-generated + name scheme. This is intended to function as a linter for developments that + want to be robust to changes in auto-generated names. This feature is experimental, + and may change or dissapear without warning. + Checker - The checker now accepts filenames in addition to logical paths. @@ -98,6 +109,12 @@ CoqIDE - Find and Replace All report the number of occurrences found; Find indicates when it wraps. +coqdep + +- Learned to read -I, -Q, -R and filenames from _CoqProject files. + This is used by coq_makefile when generating dependencies for .v + files (but not other files). + Documentation - The Coq FAQ, formerly located at https://coq.inria.fr/faq, has been @@ -272,6 +289,7 @@ Standard Library lemmas such as INR_IZR_INZ should be used instead. - Real constants are now represented using IZR rather than R0 and R1; this might cause rewriting rules to fail to apply to constants. +- Added new notation {x & P} for sigT (without a type for x) Plugins diff --git a/appveyor.yml b/appveyor.yml index 64c1bedb5..44a93d15d 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -10,12 +10,12 @@ image: environment: CYGMIRROR: http://ftp.inf.tu-dresden.de/software/windows/cygwin32 matrix: - - USEOPAM: true - ARCH: 64 - USEOPAM: false ARCH: 32 - USEOPAM: false ARCH: 64 + - USEOPAM: true + ARCH: 64 build_script: - cmd: 'call %APPVEYOR_BUILD_FOLDER%\dev\ci\appveyor.bat' diff --git a/configure.ml b/configure.ml index 69db9407a..1eae3bd93 100644 --- a/configure.ml +++ b/configure.ml @@ -22,8 +22,10 @@ let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqworkmgr"; let verbose = ref false (* for debugging this script *) (** * Utility functions *) - -let die msg = eprintf "%s\nConfiguration script failed!\n" msg; exit 1 +let cfprintf oc = kfprintf (fun oc -> fprintf oc "\n%!") oc +let cprintf s = cfprintf stdout s +let ceprintf s = cfprintf stderr s +let die msg = ceprintf "%s\nConfiguration script failed!" msg; exit 1 let s2i = int_of_string let i2s = string_of_int @@ -107,7 +109,7 @@ let run ?(fatal=true) ?(err=StdErr) prog args = let cmd = String.concat " " (prog::args) in let exn = match e with Failure s -> s | _ -> Printexc.to_string e in let msg = sprintf "Error while running '%s' (%s)" cmd exn in - if fatal then die msg else (printf "W: %s\n" msg; "", []) + if fatal then die msg else (cprintf "W: %s" msg; "", []) let tryrun prog args = run ~fatal:false ~err:DevNull prog args @@ -203,7 +205,7 @@ let win_aware_quote_executable str = sprintf "%S" str else let _ = if contains_suspicious_characters str then - printf "*Warning* The string %S contains suspicious characters; ocamlfind might fail\n" str in + cprintf "*Warning* The string %S contains suspicious characters; ocamlfind might fail" str in Str.global_replace (Str.regexp "\\\\") "/" str (** * Date *) @@ -235,6 +237,101 @@ let _ = if not (dir_exists "bin") then Unix.mkdir "bin" 0o755 type ide = Opt | Byte | No +type preferences = { + prefix : string option; + local : bool; + vmbyteflags : string option; + custom : bool option; + bindir : string option; + libdir : string option; + configdir : string option; + datadir : string option; + mandir : string option; + docdir : string option; + emacslib : string option; + coqdocdir : string option; + ocamlfindcmd : string option; + lablgtkdir : string option; + camlp5dir : string option; + arch : string option; + natdynlink : bool; + coqide : ide option; + macintegration : bool; + browser : string option; + withdoc : bool; + byteonly : bool; + flambda_flags : string list; + debug : bool; + profile : bool; + bin_annot : bool; + annot : bool; + bytecodecompiler : bool; + nativecompiler : bool; + coqwebsite : string; + force_caml_version : bool; + force_findlib_version : bool; + warn_error : bool; +} + +module Profiles = struct + +let default = { + prefix = None; + local = false; + vmbyteflags = None; + custom = None; + bindir = None; + libdir = None; + configdir = None; + datadir = None; + mandir = None; + docdir = None; + emacslib = None; + coqdocdir = None; + ocamlfindcmd = None; + lablgtkdir = None; + camlp5dir = None; + arch = None; + natdynlink = true; + coqide = None; + macintegration = true; + browser = None; + withdoc = false; + byteonly = false; + flambda_flags = []; + debug = true; + profile = false; + bin_annot = false; + annot = false; + bytecodecompiler = true; + nativecompiler = not (os_type_win32 || os_type_cygwin); + coqwebsite = "http://coq.inria.fr/"; + force_caml_version = false; + force_findlib_version = false; + warn_error = false; +} + +let devel state = { state with + local = true; + bin_annot = true; + annot = true; + warn_error = true; +} +let devel_doc = "-local -annot -bin-annot -warn-error yes" + +let get = function + | "devel" -> devel + | s -> raise (Arg.Bad ("profile name expected instead of "^s)) + +let doc = + "<profile> Sets a bunch of flags. Supported profiles: + devel = " ^ devel_doc + +end + +let prefs = ref Profiles.default + + let get_bool = function | "true" | "yes" | "y" | "all" -> true | "false" | "no" | "n" -> false @@ -246,123 +343,99 @@ let get_ide = function | "no" -> No | s -> raise (Arg.Bad ("(opt|byte|no) argument expected instead of "^s)) -let arg_bool r = Arg.String (fun s -> r := get_bool s) - -let arg_string_option r = Arg.String (fun s -> r := Some s) - -module Prefs = struct - let prefix = ref (None : string option) - let local = ref false - let vmbyteflags = ref (None : string option) - let custom = ref (None : bool option) - let bindir = ref (None : string option) - let libdir = ref (None : string option) - let configdir = ref (None : string option) - let datadir = ref (None : string option) - let mandir = ref (None : string option) - let docdir = ref (None : string option) - let emacslib = ref (None : string option) - let coqdocdir = ref (None : string option) - let ocamlfindcmd = ref (None : string option) - let lablgtkdir = ref (None : string option) - let camlp5dir = ref (None : string option) - let arch = ref (None : string option) - let natdynlink = ref true - let coqide = ref (None : ide option) - let macintegration = ref true - let browser = ref (None : string option) - let withdoc = ref false - let byteonly = ref false - let flambda_flags = ref [] - let debug = ref true - let profile = ref false - let bin_annot = ref false - let annot = ref false - let bytecodecompiler = ref true - let nativecompiler = ref (not (os_type_win32 || os_type_cygwin)) - let coqwebsite = ref "http://coq.inria.fr/" - let force_caml_version = ref false - let force_findlib_version = ref false - let warn_error = ref false -end +let arg_bool f = Arg.String (fun s -> prefs := f !prefs (get_bool s)) + +let arg_string f = Arg.String (fun s -> prefs := f !prefs s) +let arg_string_option f = Arg.String (fun s -> prefs := f !prefs (Some s)) +let arg_string_list c f = Arg.String (fun s -> prefs := f !prefs (string_split c s)) + +let arg_set f = Arg.Unit (fun () -> prefs := f !prefs true) +let arg_clear f = Arg.Unit (fun () -> prefs := f !prefs false) + +let arg_set_option f = Arg.Unit (fun () -> prefs := f !prefs (Some true)) +let arg_clear_option f = Arg.Unit (fun () -> prefs := f !prefs (Some false)) + +let arg_ide f = Arg.String (fun s -> prefs := f !prefs (Some (get_ide s))) + +let arg_profile = Arg.String (fun s -> prefs := Profiles.get s !prefs) (* TODO : earlier any option -foo was also available as --foo *) let args_options = Arg.align [ - "-prefix", arg_string_option Prefs.prefix, + "-prefix", arg_string_option (fun p prefix -> { p with prefix }), "<dir> Set installation directory to <dir>"; - "-local", Arg.Set Prefs.local, + "-local", arg_set (fun p local -> { p with local }), " Set installation directory to the current source tree"; - "-vmbyteflags", arg_string_option Prefs.vmbyteflags, + "-vmbyteflags", arg_string_option (fun p vmbyteflags -> { p with vmbyteflags }), "<flags> Comma-separated link flags for the VM of coqtop.byte"; - "-custom", Arg.Unit (fun () -> Prefs.custom := Some true), + "-custom", arg_set_option (fun p custom -> { p with custom }), " Build bytecode executables with -custom (not recommended)"; - "-no-custom", Arg.Unit (fun () -> Prefs.custom := Some false), + "-no-custom", arg_clear_option (fun p custom -> { p with custom }), " Do not build with -custom on Windows and MacOS"; - "-bindir", arg_string_option Prefs.bindir, + "-bindir", arg_string_option (fun p bindir -> { p with bindir }), "<dir> Where to install bin files"; - "-libdir", arg_string_option Prefs.libdir, + "-libdir", arg_string_option (fun p libdir -> { p with libdir }), "<dir> Where to install lib files"; - "-configdir", arg_string_option Prefs.configdir, + "-configdir", arg_string_option (fun p configdir -> { p with configdir }), "<dir> Where to install config files"; - "-datadir", arg_string_option Prefs.datadir, + "-datadir", arg_string_option (fun p datadir -> { p with datadir }), "<dir> Where to install data files"; - "-mandir", arg_string_option Prefs.mandir, + "-mandir", arg_string_option (fun p mandir -> { p with mandir }), "<dir> Where to install man files"; - "-docdir", arg_string_option Prefs.docdir, + "-docdir", arg_string_option (fun p docdir -> { p with docdir }), "<dir> Where to install doc files"; - "-emacslib", arg_string_option Prefs.emacslib, + "-emacslib", arg_string_option (fun p emacslib -> { p with emacslib }), "<dir> Where to install emacs files"; - "-coqdocdir", arg_string_option Prefs.coqdocdir, + "-coqdocdir", arg_string_option (fun p coqdocdir -> { p with coqdocdir }), "<dir> Where to install Coqdoc style files"; - "-ocamlfind", arg_string_option Prefs.ocamlfindcmd, + "-ocamlfind", arg_string_option (fun p ocamlfindcmd -> { p with ocamlfindcmd }), "<dir> Specifies the ocamlfind command to use"; - "-lablgtkdir", arg_string_option Prefs.lablgtkdir, + "-lablgtkdir", arg_string_option (fun p lablgtkdir -> { p with lablgtkdir }), "<dir> Specifies the path to the Lablgtk library"; - "-camlp5dir", - Arg.String (fun s -> Prefs.camlp5dir:=Some s), + "-camlp5dir", arg_string_option (fun p camlp5dir -> { p with camlp5dir }), "<dir> Specifies where is the Camlp5 library and tells to use it"; - "-flambda-opts", - Arg.String (fun s -> Prefs.flambda_flags := string_split ' ' s), + "-flambda-opts", arg_string_list ' ' (fun p flambda_flags -> { p with flambda_flags }), "<flags> Specifies additional flags to be passed to the flambda optimizing compiler"; - "-arch", arg_string_option Prefs.arch, + "-arch", arg_string_option (fun p arch -> { p with arch }), "<arch> Specifies the architecture"; - "-natdynlink", arg_bool Prefs.natdynlink, + "-natdynlink", arg_bool (fun p natdynlink -> { p with natdynlink }), "(yes|no) Use dynamic loading of native code or not"; - "-coqide", Arg.String (fun s -> Prefs.coqide := Some (get_ide s)), + "-coqide", arg_ide (fun p coqide -> { p with coqide }), "(opt|byte|no) Specifies whether or not to compile CoqIDE"; - "-nomacintegration", Arg.Clear Prefs.macintegration, + "-nomacintegration", arg_clear (fun p macintegration -> { p with macintegration }), " Do not try to build CoqIDE MacOS integration"; - "-browser", arg_string_option Prefs.browser, + "-browser", arg_string_option (fun p browser -> { p with browser }), "<command> Use <command> to open URL %s"; - "-with-doc", arg_bool Prefs.withdoc, + "-with-doc", arg_bool (fun p withdoc -> { p with withdoc }), "(yes|no) Compile the documentation or not"; - "-byte-only", Arg.Set Prefs.byteonly, + "-byte-only", arg_set (fun p byteonly -> { p with byteonly }), " Compiles only bytecode version of Coq"; - "-nodebug", Arg.Clear Prefs.debug, + "-nodebug", arg_clear (fun p debug -> { p with debug }), " Do not add debugging information in the Coq executables"; - "-profile", Arg.Set Prefs.profile, + "-profiling", arg_set (fun p profile -> { p with profile }), " Add profiling information in the Coq executables"; - "-annotate", Arg.Unit (fun () -> printf "*Warning* -annotate is deprecated. Please use -annot or -bin-annot instead.\n"), + "-annotate", Arg.Unit (fun () -> cprintf "*Warning* -annotate is deprecated. Please use -annot or -bin-annot instead."), " Deprecated. Please use -annot or -bin-annot instead"; - "-annot", Arg.Set Prefs.annot, + "-annot", arg_set (fun p annot -> { p with annot }), " Dumps ml text annotation files while compiling Coq (e.g. for Tuareg)"; - "-bin-annot", Arg.Set Prefs.bin_annot, + "-bin-annot", arg_set (fun p bin_annot -> { p with bin_annot }), " Dumps ml binary annotation files while compiling Coq (e.g. for Merlin)"; - "-bytecode-compiler", arg_bool Prefs.bytecodecompiler, + "-bytecode-compiler", arg_bool (fun p bytecodecompiler -> { p with bytecodecompiler }), "(yes|no) Enable Coq's bytecode reduction machine (VM)"; - "-native-compiler", arg_bool Prefs.nativecompiler, + "-native-compiler", arg_bool (fun p nativecompiler -> { p with nativecompiler }), "(yes|no) Compilation to native code for conversion and normalization"; - "-coqwebsite", Arg.Set_string Prefs.coqwebsite, + "-coqwebsite", arg_string (fun p coqwebsite -> { p with coqwebsite }), " URL of the coq website"; - "-force-caml-version", Arg.Set Prefs.force_caml_version, + "-force-caml-version", arg_set (fun p force_caml_version -> { p with force_caml_version }), " Force OCaml version"; - "-force-findlib-version", Arg.Set Prefs.force_findlib_version, + "-force-findlib-version", arg_set (fun p force_findlib_version -> { p with force_findlib_version }), " Force findlib version"; - "-warn-error", Arg.Set Prefs.warn_error, - " Make OCaml warnings into errors"; + "-warn-error", arg_bool (fun p warn_error -> { p with warn_error }), + "(yes|no) Make OCaml warnings into errors (default no)"; "-camldir", Arg.String (fun _ -> ()), "<dir> Specifies path to 'ocaml' for running configure script"; + "-profile", arg_profile, + Profiles.doc ] let parse_args () = @@ -370,7 +443,7 @@ let parse_args () = args_options (fun s -> raise (Arg.Bad ("Unknown option: "^s))) "Available options for configure are:"; - if !Prefs.local && !Prefs.prefix <> None then + if !prefs.local && !prefs.prefix <> None then die "Options -prefix and -local are incompatible." let _ = parse_args () @@ -391,10 +464,10 @@ let reset_caml_lex c o = c.lex <- o let reset_caml_top c o = c.top <- o let reset_caml_find c o = c.find <- o -let coq_debug_flag = if !Prefs.debug then "-g" else "" -let coq_profile_flag = if !Prefs.profile then "-p" else "" -let coq_annot_flag = if !Prefs.annot then "-annot" else "" -let coq_bin_annot_flag = if !Prefs.bin_annot then "-bin-annot" else "" +let coq_debug_flag = if !prefs.debug then "-g" else "" +let coq_profile_flag = if !prefs.profile then "-p" else "" +let coq_annot_flag = if !prefs.annot then "-annot" else "" +let coq_bin_annot_flag = if !prefs.bin_annot then "-bin-annot" else "" (* This variable can be overriden only for debug purposes, use with care. *) @@ -412,8 +485,8 @@ let arch_progs = ("/usr/ucb/arch", []) ] let query_arch () = - printf "I can not automatically find the name of your architecture.\n"; - printf "Give me a name, please [win32 for Win95, Win98 or WinNT]: %!"; + cprintf "I can not automatically find the name of your architecture."; + cprintf "Give me a name, please [win32 for Win95, Win98 or WinNT]: %!"; read_line () let rec try_archs = function @@ -423,7 +496,7 @@ let rec try_archs = function | _ :: rest -> try_archs rest | [] -> query_arch () -let arch = match !Prefs.arch with +let arch = match !prefs.arch with | Some a -> a | None -> let arch,_ = tryrun "uname" ["-s"] in @@ -455,7 +528,7 @@ let vcs = let _ = let f = ".git/hooks/pre-commit" in if vcs = "git" && dir_exists ".git/hooks" && not (Sys.file_exists f) then begin - printf "Creating pre-commit hook in %s\n" f; + cprintf "Creating pre-commit hook in %s" f; let o = open_out f in let pr s = fprintf o s in pr "#!/bin/sh\n"; @@ -470,7 +543,7 @@ let _ = (** * Browser command *) let browser = - match !Prefs.browser with + match !prefs.browser with | Some b -> b | None when arch_is_win32 -> "start %s" | None when arch = "Darwin" -> "open %s" @@ -479,7 +552,7 @@ let browser = (** * OCaml programs *) let camlbin, caml_version, camllib, findlib_version = - let () = match !Prefs.ocamlfindcmd with + let () = match !prefs.ocamlfindcmd with | Some cmd -> reset_caml_find camlexec cmd | None -> try reset_caml_find camlexec (which camlexec.find) @@ -521,11 +594,11 @@ let caml_version_nums = let check_caml_version () = if caml_version_nums >= [4;2;1] then - printf "You have OCaml %s. Good!\n" caml_version + cprintf "You have OCaml %s. Good!" caml_version else - let () = printf "Your version of OCaml is %s.\n" caml_version in - if !Prefs.force_caml_version then - printf "*Warning* Your version of OCaml is outdated.\n" + let () = cprintf "Your version of OCaml is %s." caml_version in + if !prefs.force_caml_version then + cprintf "*Warning* Your version of OCaml is outdated." else die "You need OCaml 4.02.1 or later." @@ -543,11 +616,11 @@ let findlib_version_nums = let check_findlib_version () = if findlib_version_nums >= [1;4;1] then - printf "You have OCamlfind %s. Good!\n" findlib_version + cprintf "You have OCamlfind %s. Good!" findlib_version else - let () = printf "Your version of OCamlfind is %s.\n" findlib_version in - if !Prefs.force_findlib_version then - printf "*Warning* Your version of OCamlfind is outdated.\n" + let () = cprintf "Your version of OCamlfind is %s." findlib_version in + if !prefs.force_findlib_version then + cprintf "*Warning* Your version of OCamlfind is outdated." else die "You need OCamlfind 1.4.1 or later." @@ -571,7 +644,7 @@ let camltag = match caml_version_list with *) let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50" let coq_warn_error = - if !Prefs.warn_error + if !prefs.warn_error then "-warn-error +a" ^ (if caml_version_nums > [4;2;3] then "-56" @@ -611,7 +684,7 @@ let which_camlp5 base = (* TODO: camlp5dir should rather be the *binary* location, just as camldir *) (* TODO: remove the late attempts at finding gramlib.cma *) -let check_camlp5 testcma = match !Prefs.camlp5dir with +let check_camlp5 testcma = match !prefs.camlp5dir with | Some dir -> if Sys.file_exists (dir/testcma) then let camlp5o = @@ -636,7 +709,7 @@ let check_camlp5_version camlp5o = let version = List.nth (string_split ' ' version_line) 2 in match numeric_prefix_list version with | major::minor::_ when s2i major > 6 || (s2i major, s2i minor) >= (6,6) -> - printf "You have Camlp5 %s. Good!\n" version; version + cprintf "You have Camlp5 %s. Good!" version; version | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n" let config_camlp5 () = @@ -659,22 +732,22 @@ let camlp5libdir = shorten_camllib fullcamlp5libdir (** * Native compiler *) let msg_byteonly () = - printf "Only the bytecode version of Coq will be available.\n" + cprintf "Only the bytecode version of Coq will be available." let msg_no_ocamlopt () = - printf "Cannot find the OCaml native-code compiler.\n"; msg_byteonly () + cprintf "Cannot find the OCaml native-code compiler."; msg_byteonly () let msg_no_camlp5_cmxa () = - printf "Cannot find the native-code library of camlp5.\n"; msg_byteonly () + cprintf "Cannot find the native-code library of camlp5."; msg_byteonly () let msg_no_dynlink_cmxa () = - printf "Cannot find native-code dynlink library.\n"; msg_byteonly (); - printf "For building a native-code Coq, you may try to first\n"; - printf "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)\n"; - printf "and then run ./configure -natdynlink no\n" + cprintf "Cannot find native-code dynlink library."; msg_byteonly (); + cprintf "For building a native-code Coq, you may try to first"; + cprintf "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)"; + cprintf "and then run ./configure -natdynlink no" let check_native () = - let () = if !Prefs.byteonly then raise Not_found in + let () = if !prefs.byteonly then raise Not_found in let version, _ = tryrun camlexec.find ["opt";"-version"] in if version = "" then let () = msg_no_ocamlopt () in raise Not_found else if not (Sys.file_exists (fullcamlp5libdir/camlp5mod^".cmxa")) @@ -684,16 +757,16 @@ let check_native () = else let () = if version <> caml_version then - printf - "Warning: Native and bytecode compilers do not have the same version!\n" - in printf "You have native-code compilation. Good!\n" + cprintf + "Warning: Native and bytecode compilers do not have the same version!" + in cprintf "You have native-code compilation. Good!" let best_compiler = try check_native (); "opt" with Not_found -> "byte" (** * Native dynlink *) -let hasnatdynlink = !Prefs.natdynlink && best_compiler = "opt" +let hasnatdynlink = !prefs.natdynlink && best_compiler = "opt" let natdynlinkflag = if hasnatdynlink then "true" else "false" @@ -723,7 +796,7 @@ let check_for_numlib () = match numlib with | "" -> die "Num library not installed, required for OCaml 4.06 or later" - | _ -> printf "You have the Num library installed. Good!\n" + | _ -> cprintf "You have the Num library installed. Good!" let numlib = check_for_numlib () @@ -740,7 +813,7 @@ let get_source = function (** Is some location a suitable LablGtk2 installation ? *) let check_lablgtkdir ?(fatal=false) src dir = - let yell msg = if fatal then die msg else (printf "%s\n" msg; false) in + let yell msg = if fatal then die msg else (cprintf "%s" msg; false) in let msg = get_source src in if not (dir_exists dir) then yell (sprintf "No such directory '%s' (%s)." dir msg) @@ -753,7 +826,7 @@ let check_lablgtkdir ?(fatal=false) src dir = (** Detect and/or verify the Lablgtk2 location *) let get_lablgtkdir () = - match !Prefs.lablgtkdir with + match !prefs.lablgtkdir with | Some dir -> let msg = Manual in if check_lablgtkdir ~fatal:true msg dir then dir, msg @@ -776,7 +849,7 @@ let get_lablgtkdir () = let check_lablgtk_version src dir = match src with | Manual | Stdlib -> - printf "Warning: could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3.\n"; + cprintf "Warning: could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3."; (true, "an unknown version") | OCamlFind -> let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in @@ -787,7 +860,7 @@ let check_lablgtk_version src dir = match src with else if vi < [2; 18; 3] then begin (* Version 2.18.3 is known to report incorrectly as 2.18.0, and Launchpad packages report as version 2.16.0 due to a misconfigured META file; see https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 *) - printf "Warning: Your installed lablgtk reports as %s.\n It is possible that the installed version is actually more recent\n but reports an incorrect version. If the installed version is\n actually more recent than 2.18.3, that's fine; if it is not,\n CoqIDE will compile but may be very unstable.\n" v; + cprintf "Warning: Your installed lablgtk reports as %s.\n It is possible that the installed version is actually more recent\n but reports an incorrect version. If the installed version is\n actually more recent than 2.18.3, that's fine; if it is not,\n CoqIDE will compile but may be very unstable." v; (true, "an unknown version") end else @@ -800,11 +873,11 @@ exception Ide of ide (** If the user asks an impossible coqide, we abort the configuration *) -let set_ide ide msg = match ide, !Prefs.coqide with +let set_ide ide msg = match ide, !prefs.coqide with | No, Some (Byte|Opt) | Byte, Some Opt -> die (msg^":\n=> cannot build requested CoqIde") | _ -> - printf "%s:\n=> %s CoqIde will be built.\n" msg (pr_ide ide); + cprintf "%s:\n=> %s CoqIde will be built." msg (pr_ide ide); raise (Ide ide) let lablgtkdir = ref "" @@ -813,7 +886,7 @@ let lablgtkdir = ref "" This function also sets the lablgtkdir reference in case of success. *) let check_coqide () = - if !Prefs.coqide = Some No then set_ide No "CoqIde manually disabled"; + if !prefs.coqide = Some No then set_ide No "CoqIde manually disabled"; let dir, via = get_lablgtkdir () in if dir = "" then set_ide No "LablGtk2 not found"; let (ok, version) = check_lablgtk_version via dir in @@ -821,7 +894,7 @@ let check_coqide () = if not ok then set_ide No (found^", but too old (required >= 2.18.3, found " ^ version ^ ")"); (* We're now sure to produce at least one kind of coqide *) lablgtkdir := shorten_camllib dir; - if !Prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested"); + if !prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested"); if best_compiler<>"opt" then set_ide Byte (found^", but no native compiler"); if not (Sys.file_exists (dir/"gtkThread.cmx")) then set_ide Byte (found^", but no native LablGtk2"); @@ -844,7 +917,7 @@ let idearchdef = ref "X11" let coqide_flags () = if !lablgtkdir <> "" then lablgtkincludes := sprintf "-I %S" !lablgtkdir; match coqide, arch with - | "opt", "Darwin" when !Prefs.macintegration -> + | "opt", "Darwin" when !prefs.macintegration -> let osxdir,_ = tryrun camlexec.find ["query";"lablgtkosx"] in if osxdir <> "" then begin lablgtkincludes := sprintf "%s -I %S" !lablgtkincludes osxdir; @@ -870,7 +943,7 @@ let strip = if arch = "Darwin" then if hasnatdynlink then "true" else "strip" else - if !Prefs.profile || !Prefs.debug then "true" else begin + if !prefs.profile || !prefs.debug then "true" else begin let _, all = run camlexec.find ["ocamlc";"-config"] in let strip = String.concat "" (List.map (fun l -> match string_split ' ' l with @@ -886,11 +959,11 @@ let strip = let check_doc () = let err s = - printf "%s was not found; documentation will not be available\n" s; + ceprintf "%s was not found; documentation will not be available" s; raise Not_found in try - if not !Prefs.withdoc then raise Not_found; + if not !prefs.withdoc then raise Not_found; if not (program_in_path "latex") then err "latex"; if not (program_in_path "hevea") then err "hevea"; if not (program_in_path "hacha") then err "hacha"; @@ -908,28 +981,28 @@ let coqtop = Sys.getcwd () let unix = os_type_cygwin || not arch_is_win32 -(** Variable name, description, ref in Prefs, default dir, prefix-relative *) +(** Variable name, description, ref in prefs, default dir, prefix-relative *) type path_style = | Absolute of string (* Should start with a "/" *) | Relative of string (* Should not start with a "/" *) let install = [ - "BINDIR", "the Coq binaries", Prefs.bindir, + "BINDIR", "the Coq binaries", !prefs.bindir, Relative "bin", Relative "bin", Relative "bin"; - "COQLIBINSTALL", "the Coq library", Prefs.libdir, + "COQLIBINSTALL", "the Coq library", !prefs.libdir, Relative "lib", Relative "lib/coq", Relative ""; - "CONFIGDIR", "the Coqide configuration files", Prefs.configdir, + "CONFIGDIR", "the Coqide configuration files", !prefs.configdir, Relative "config", Absolute "/etc/xdg/coq", Relative "ide"; - "DATADIR", "the Coqide data files", Prefs.datadir, + "DATADIR", "the Coqide data files", !prefs.datadir, Relative "share", Relative "share/coq", Relative "ide"; - "MANDIR", "the Coq man pages", Prefs.mandir, + "MANDIR", "the Coq man pages", !prefs.mandir, Relative "man", Relative "share/man", Relative "man"; - "DOCDIR", "the Coq documentation", Prefs.docdir, + "DOCDIR", "the Coq documentation", !prefs.docdir, Relative "doc", Relative "share/doc/coq", Relative "doc"; - "EMACSLIB", "the Coq Emacs mode", Prefs.emacslib, + "EMACSLIB", "the Coq Emacs mode", !prefs.emacslib, Relative "emacs", Relative "share/emacs/site-lisp", Relative "tools"; - "COQDOCDIR", "the Coqdoc LaTeX files", Prefs.coqdocdir, + "COQDOCDIR", "the Coqdoc LaTeX files", !prefs.coqdocdir, Relative "latex", Relative "share/texmf/tex/latex/misc", Relative "tools/coqdoc"; ] @@ -959,8 +1032,8 @@ let find_suffix prefix path = match prefix with let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,locallayout) = let dir,suffix = - if !Prefs.local then (use_suffix coqtop locallayout,locallayout) - else match !uservalue, !Prefs.prefix with + if !prefs.local then (use_suffix coqtop locallayout,locallayout) + else match uservalue, !prefs.prefix with | Some d, p -> d,find_suffix p d | _, Some p -> let suffix = if arch_is_win32 then selfcontainedlayout else relativize unixlayout in @@ -992,7 +1065,7 @@ let datadir,datadirsuffix = let (_,_,d,s) = select "DATADIR" in d,s let custom_os = arch_is_win32 || arch = "Darwin" -let use_custom = match !Prefs.custom with +let use_custom = match !prefs.custom with | Some b -> b | None -> custom_os @@ -1002,10 +1075,10 @@ let build_loadpath = ref "# you might want to set CAML_LD_LIBRARY_PATH by hand!" let config_runtime () = - match !Prefs.vmbyteflags with + match !prefs.vmbyteflags with | Some flags -> string_split ',' flags | _ when use_custom -> [custom_flag] - | _ when !Prefs.local -> + | _ when !prefs.local -> ["-dllib";"-lcoqrun";"-dllpath";coqtop/"kernel/byterun"] | _ -> let ld="CAML_LD_LIBRARY_PATH" in @@ -1029,7 +1102,7 @@ let print_summary () = pr " OCaml version : %s\n" caml_version; pr " OCaml binaries in : %s\n" (esc camlbin); pr " OCaml library in : %s\n" (esc camllib); - pr " OCaml flambda flags : %s\n" (String.concat " " !Prefs.flambda_flags); + pr " OCaml flambda flags : %s\n" (String.concat " " !prefs.flambda_flags); pr " Camlp5 version : %s\n" camlp5_version; pr " Camlp5 binaries in : %s\n" (esc camlp5bindir); pr " Camlp5 library in : %s\n" (esc camlp5libdir); @@ -1043,10 +1116,10 @@ let print_summary () = pr " Documentation : %s\n" (if withdoc then "All" else "None"); pr " Web browser : %s\n" browser; - pr " Coq web site : %s\n" !Prefs.coqwebsite; - pr " Bytecode VM enabled : %B\n" !Prefs.bytecodecompiler; - pr " Native Compiler enabled : %B\n\n" !Prefs.nativecompiler; - if !Prefs.local then + pr " Coq web site : %s\n" !prefs.coqwebsite; + pr " Bytecode VM enabled : %B\n" !prefs.bytecodecompiler; + pr " Native Compiler enabled : %B\n\n" !prefs.nativecompiler; + if !prefs.local then pr " Local build, no installation...\n" else (pr " Paths for true installation:\n"; @@ -1095,7 +1168,7 @@ let write_configml f = pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n"; pr "(* Exact command that generated this file: *)\n"; pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv)); - pr_b "local" !Prefs.local; + pr_b "local" !prefs.local; pr "let vmbyteflags = ["; List.iter (pr "%S;") vmbyteflags; pr "]\n"; pr_s "coqlib" coqlib; pr_s "configdir" configdir; @@ -1130,17 +1203,17 @@ let write_configml f = pr "let gtk_platform = `%s\n" !idearchdef; pr_b "has_natdynlink" hasnatdynlink; pr_s "natdynlinkflag" natdynlinkflag; - pr_l "flambda_flags" !Prefs.flambda_flags; + pr_l "flambda_flags" !prefs.flambda_flags; pr_i "vo_magic_number" vo_magic; pr_i "state_magic_number" state_magic; pr_s "browser" browser; - pr_s "wwwcoq" !Prefs.coqwebsite; - pr_s "wwwbugtracker" (!Prefs.coqwebsite ^ "bugs/"); - pr_s "wwwrefman" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/"); - pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/"); + pr_s "wwwcoq" !prefs.coqwebsite; + pr_s "wwwbugtracker" (!prefs.coqwebsite ^ "bugs/"); + pr_s "wwwrefman" (!prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/"); + pr_s "wwwstdlib" (!prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/"); pr_s "localwwwrefman" ("file:/" ^ docdir ^ "/html/refman"); - pr_b "bytecode_compiler" !Prefs.bytecodecompiler; - pr_b "native_compiler" !Prefs.nativecompiler; + pr_b "bytecode_compiler" !prefs.bytecodecompiler; + pr_b "native_compiler" !prefs.nativecompiler; let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library"; "engine"; "pretyping"; "interp"; "parsing"; "proofs"; @@ -1197,7 +1270,7 @@ let write_makefile f = pr "#Variable used to detect whether ./configure has run successfully.\n"; pr "COQ_CONFIGURED=yes\n\n"; pr "# Local use (no installation)\n"; - pr "LOCAL=%B\n\n" !Prefs.local; + pr "LOCAL=%B\n\n" !prefs.local; pr "# Bytecode link flags : should we use -custom or not ?\n"; pr "CUSTOM=%s\n" custom_flag; pr "VMBYTEFLAGS=%s\n" (String.concat " " vmbyteflags); @@ -1226,7 +1299,7 @@ let write_makefile f = pr "# User compilation flag\n"; pr "USERFLAGS=\n\n"; (* XXX make this configurable *) - pr "FLAMBDA_FLAGS=%s\n" (String.concat " " !Prefs.flambda_flags); + pr "FLAMBDA_FLAGS=%s\n" (String.concat " " !prefs.flambda_flags); pr "# Flags for GCC\n"; pr "CFLAGS=%s\n\n" cflags; pr "# Compilation debug flags\n"; @@ -1271,7 +1344,7 @@ let write_makefile f = pr "# Option to control compilation and installation of the documentation\n"; pr "WITHDOC=%s\n\n" (if withdoc then "all" else "no"); pr "# Option to produce precompiled files for native_compute\n"; - pr "NATIVECOMPUTE=%s\n" (if !Prefs.nativecompiler then "-native-compiler" else ""); + pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler then "-native-compiler" else ""); close_out o; Unix.chmod f 0o444 diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat index 665d54176..ccf22cc86 100644 --- a/dev/build/windows/MakeCoq_MinGW.bat +++ b/dev/build/windows/MakeCoq_MinGW.bat @@ -78,6 +78,9 @@ SET GTK_FROM_SOURCES=N REM see -threads in ReadMe.txt SET MAKE_THREADS=8 +REM see -addon in ReadMe.txt +SET "COQ_ADDONS= " + REM ========== PARSE COMMAND LINE PARAMETERS ========== SHIFT @@ -233,6 +236,14 @@ IF "%~0" == "-threads" ( GOTO Parse ) +IF "%~0" == "-addon" ( + SET "COQ_ADDONS=%COQ_ADDONS% %~1" + SHIFT + SHIFT + GOTO Parse +) + + IF NOT "%~0" == "" ( ECHO Install cygwin and download, compile and install OCaml and Coq for MinGW ECHO !!! Illegal parameter %~0 @@ -426,6 +437,7 @@ ECHO ========== BATCH FUNCTIONS ========== ECHO -coqver ^<Coq version to install^> ECHO -gtksrc ^<Y or N^> build GTK ^(90 min^) or use cygwin version ECHO -threads ^<1..N^> Number of make threads + ECHO -addon ^<name^> Enable building selected addon (can be repeated) ECHO( ECHO See ReadMe.txt for a detailed description of all parameters ECHO( @@ -447,6 +459,7 @@ ECHO ========== BATCH FUNCTIONS ========== ECHO -coqver = %COQ_VERSION% ECHO -gtksrc = %GTK_FROM_SOURCES% ECHO -threads = %MAKE_THREADS% + ECHO -addon = %COQ_ADDONS% GOTO :EOF :CheckYN diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt index 7e80e33c6..93851aeb8 100644 --- a/dev/build/windows/ReadMe.txt +++ b/dev/build/windows/ReadMe.txt @@ -61,6 +61,7 @@ The Script MakeCoq_MinGW does: - either installs MinGW GTK via Cygwin or compiles it fom sources - download, compile and install OCaml, CamlP5, Menhir, lablgtk - download, compile and install Coq +- download, compile and install selected addons - create a Windows installer (NSIS based) The parameters are described below. Mostly paths and the HTTP proxy need to be @@ -335,6 +336,10 @@ Possible values: 1..N. Should not be more than 1.5x the number of cores. Should not be more than available RAM/2GB (e.g. 4 for 8GB) +===== -addon ===== + +Enable build and installation of selected Coq package (can be repeated for +selecting more packages) ==================== TODO ==================== diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index d8cde39f8..bea30b1a7 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -223,6 +223,12 @@ function get_expand_source_tar { cp "$SOURCE_LOCAL_CACHE_CFMT/$name.$3" $TARBALLS else wget $1/$2.$3 + if file -i $2.$3 | grep text/html; then + echo Download failed: $1/$2.$3 + echo The file wget downloaded is an html file: + cat $2.$3 + exit 1 + fi if [ ! "$2.$3" == "$name.$3" ] ; then mv $2.$3 $name.$3 fi @@ -1280,7 +1286,8 @@ function make_coq_installer { # Prepare the file lists for the installer. We created to file list dumps of the target folder during the build: # ocaml: ocaml + menhir + camlp5 + findlib - # ocal_coq: as above + coq + # ocaml_coq: as above + coq + # ocaml_coq_addons: as above + lib/user-contrib/* # Create coq file list as ocaml_coq / ocaml diff_files coq ocaml_coq ocaml @@ -1294,11 +1301,17 @@ function make_coq_installer { # Coq objects objects required for plugin development = coq objects except those for pre installed plugins diff_files coq_plugindev coq_objects coq_objects_plugins + # Addons (TODO: including objects that could go to the plugindev thing, but + # then one would have to make that package depend on this one, so not + # implemented yet) + diff_files coq_addons ocaml_coq_addons ocaml_coq + # Coq files, except objects needed only for plugin development diff_files coq_base coq coq_plugindev # Convert section files to NSIS format files_to_nsis coq_base + files_to_nsis coq_addons files_to_nsis coq_plugindev files_to_nsis ocaml @@ -1314,12 +1327,30 @@ function make_coq_installer { cp ../patches/ReplaceInFile.nsh dev/nsis VERSION=`grep '^VERSION=' config/Makefile | cut -d = -f 2 | tr -d '\r'` cd dev/nsis - logn nsis-installer "$NSIS" -DVERSION=$VERSION -DARCH=$ARCH -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico coq_new.nsi + logn nsis-installer "$NSIS" -DVERSION=$VERSION -DARCH=$ARCH -DCOQ_SRC_PATH="$PREFIXCOQ" -DCOQ_ICON=..\\..\\ide\\coq.ico -DCOQ_ADDONS="$COQ_ADDONS" coq_new.nsi build_post fi } +###################### ADDONS ##################### + +function make_addon_bignums { + if build_prep https://github.com/coq/bignums/archive/ master zip 1 bignums-8.8.0; then + # To make command lines shorter :-( + echo 'COQ_SRC_SUBDIRS:=$(filter-out plugins/%,$(COQ_SRC_SUBDIRS)) plugins/syntax' >> Makefile.coq.local + logn make make all + logn make-install make install + build_post + fi +} + +function make_addons { + for addon in $COQ_ADDONS; do + make_addon_$addon + done +} + ###################### TOP LEVEL BUILD ##################### make_sed @@ -1337,6 +1368,10 @@ fi list_files ocaml_coq +make_addons + +list_files ocaml_coq_addons + if [ "$MAKEINSTALLER" == "Y" ] ; then make_coq_installer fi diff --git a/dev/build/windows/patches_coq/coq_new.nsi b/dev/build/windows/patches_coq/coq_new.nsi index 2c2f0fa47..55fba6d5a 100644 --- a/dev/build/windows/patches_coq/coq_new.nsi +++ b/dev/build/windows/patches_coq/coq_new.nsi @@ -9,6 +9,7 @@ ; ARCH The target architecture, either x86_64 or i686 ; COQ_SRC_PATH path of Coq installation in Windows or MinGW format (either \\ or /, but with drive letter) ; COQ_ICON path of Coq icon file in Windows or MinGW format +; COQ_ADDONS list of addons that are shipped ; Enable compression after debugging. ; SetCompress off @@ -69,7 +70,8 @@ Var INSTDIR_DBS ; INSTDIR with \\ instead of \ ;Description LangString DESC_1 ${LANG_ENGLISH} "This package contains Coq and CoqIDE." - LangString DESC_2 ${LANG_ENGLISH} "This package contains an OCaml compiler for Coq native compute and plugin development." + LangString DESC_2 ${LANG_ENGLISH} "This package contains the following extra Coq packages: ${COQ_ADDONS}" + ;LangString DESC_2 ${LANG_ENGLISH} "This package contains an OCaml compiler for Coq native compute and plugin development." LangString DESC_3 ${LANG_ENGLISH} "This package contains the development files needed in order to build a plugin for Coq." LangString DESC_4 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for the current user." LangString DESC_5 ${LANG_ENGLISH} "Set the OCAMLLIB environment variable for all users." @@ -150,6 +152,11 @@ SectionEnd ;OCAML !insertmacro ReplaceInFile "$INSTDIR\etc\findlib.conf" "$COQ_SRC_PATH_DBS" "$INSTDIR_DBS" ;OCAML SectionEnd +Section "Coq packages" Sec2 + SetOutPath "$INSTDIR\" + !include "..\..\..\filelists\coq_addons.nsh" +SectionEnd + Section "Coq files for plugin developers" Sec3 SetOutPath "$INSTDIR\" !include "..\..\..\filelists\coq_plugindev.nsh" @@ -176,7 +183,7 @@ SectionEnd !insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN !insertmacro MUI_DESCRIPTION_TEXT ${Sec1} $(DESC_1) - ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2) + !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2) !insertmacro MUI_DESCRIPTION_TEXT ${Sec3} $(DESC_3) ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec4} $(DESC_4) ;OCAML !insertmacro MUI_DESCRIPTION_TEXT ${Sec5} $(DESC_5) diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat index dec6f0d18..85a71baf7 100644 --- a/dev/ci/appveyor.bat +++ b/dev/ci/appveyor.bat @@ -23,6 +23,7 @@ if %USEOPAM% == false ( call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^ -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^ -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^ + -addon=bignums -make=N ^ -setup %CYGROOT%\%SETUP% || GOTO ErrorExit copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit 7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 0003a2c21..c48c2d5d1 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -41,15 +41,15 @@ Building coqtop: cd ~/git/coq git checkout trunk make distclean - ./configure -annotate -local + ./configure -profile devel make clean make -j4 coqide printers -The "-annotate" option is essential when one wants to use Merlin. +The "-profile devel" enables all options recommended for developers (like +warnings, support for Merlin, etc). Moreover Coq is configured so that +it can be run without installing it (i.e. from the current directory). -The "-local" option is useful if one wants to run the coqtop and coqide binaries without running make install - -Then check if +Once the compilation is over check if - bin/coqtop - bin/coqide behave as expected. diff --git a/dev/header.c b/dev/header.c new file mode 100644 index 000000000..663c43b3d --- /dev/null +++ b/dev/header.c @@ -0,0 +1,9 @@ +/************************************************************************/ +/* * The Coq Proof Assistant / The Coq Development Team */ +/* v * INRIA, CNRS and contributors - Copyright 1999-2018 */ +/* <O___,, * (see CREDITS file for the list of authors) */ +/* \VV/ **************************************************************/ +/* // * This file is distributed under the terms of the */ +/* * GNU Lesser General Public License Version 2.1 */ +/* * (see LICENSE file for the text of the license) */ +/************************************************************************/ diff --git a/dev/header b/dev/header.ml index 7c3ee6004..7c3ee6004 100644 --- a/dev/header +++ b/dev/header.ml diff --git a/dev/header.py b/dev/header.py new file mode 100644 index 000000000..f81c8aa6a --- /dev/null +++ b/dev/header.py @@ -0,0 +1,9 @@ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## <O___,, # (see CREDITS file for the list of authors) ## +## \VV/ ############################################################### +## // # This file is distributed under the terms of the ## +## # GNU Lesser General Public License Version 2.1 ## +## # (see LICENSE file for the text of the license) ## +########################################################################## diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 04a8a25c1..5b73ac00a 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -241,6 +241,20 @@ The following command-line options are recognized by the commands {\tt Collapse the universe hierarchy of {\Coq}. Warning: this makes the logic inconsistent. +\item[{\tt -mangle-names} {\em ident}]\ % + + Experimental: Do not depend on this option. + + Replace Coq's auto-generated name scheme with names of the form + {\tt ident0}, {\tt ident1}, \ldots etc. + The command {\tt Set Mangle Names}\optindex{Mangle Names} turns + the behavior on in a document, and {\tt Set Mangle Names Prefix "ident"} + \optindex{Mangle Names Prefix} changes the used prefix. + + This feature is intended to be used as a linter for developments that want + to be robust to changes in the auto-generated name scheme. The options are + provided to facilitate tracking down problems. + \item[{\tt -compat} {\em version}]\ % Attempt to maintain some backward-compatibility with a previous version. diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index c4c0435c5..0a4d0ef9a 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1156,16 +1156,6 @@ without having to cut manually the proof in smaller lemmas. It may be useful to generate lemmas minimal w.r.t. the assumptions they depend on. This can be obtained thanks to the option below. -\begin{quote} -\optindex{Shrink Abstract} -{\tt Set Shrink Abstract} -\end{quote} -\emph{Deprecated since 8.7} - -When set (default), all lemmas generated through \texttt{abstract {\tacexpr}} -and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the -variables that appear in the term constructed by \texttt{\tacexpr}. - \begin{Variants} \item \texttt{abstract {\tacexpr} using {\ident}}.\\ Give explicitly the name of the auxiliary lemma. diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 6b24fdde7..bd74a40d7 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -298,15 +298,19 @@ subgoals which clutter your screen. \begin{Variant} \item {\tt Focus {\num}.}\\ This focuses the attention on the $\num^{th}$ subgoal to prove. - \end{Variant} +\emph{This command is deprecated since 8.8: prefer the use of bullets or + focusing brackets instead, including {\tt {\num}: \{}}. + \subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}} This command restores to focus the goal that were suspended by the last {\tt Focus} command. +\emph{This command is deprecated since 8.8.} + \subsection[\tt Unfocused.]{\tt Unfocused.\comindex{Unfocused}} -Succeeds in the proof is fully unfocused, fails is there are some +Succeeds in the proof if fully unfocused, fails if there are some goals out of focus. \subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}}\label{curlybacket} diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 7674cf67a..6b3ce048f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -89,15 +89,15 @@ let nf_evars_universes evm = (Evd.universe_subst evm) let nf_evars_and_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in evm, nf_evars_universes evm let e_nf_evars_and_universes evdref = - evdref := Evd.nf_constraints !evdref; + evdref := Evd.minimize_universes !evdref; nf_evars_universes !evdref, Evd.universe_subst !evdref let nf_evar_map_universes evm = - let evm = Evd.nf_constraints evm in + let evm = Evd.minimize_universes evm in let subst = Evd.universe_subst evm in if Univ.LMap.is_empty subst then evm, nf_evar0 evm else diff --git a/engine/evd.ml b/engine/evd.ml index e7d542d12..185cab101 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -253,21 +253,8 @@ let instantiate_evar_array info c args = | [] -> c | _ -> replace_vars inst c -type evar_universe_context = UState.t -type 'a in_evar_universe_context = 'a * evar_universe_context - -let empty_evar_universe_context = UState.empty -let union_evar_universe_context = UState.union -let evar_universe_context_set = UState.context_set -let evar_universe_context_constraints = UState.constraints -let evar_context_universe_context = UState.context -let evar_universe_context_of = UState.of_context_set -let evar_universe_context_subst = UState.subst -let add_constraints_context = UState.add_constraints -let add_universe_constraints_context = UState.add_universe_constraints -let constrain_variables = UState.constrain_variables -let evar_universe_context_of_binders = UState.of_binders +type 'a in_evar_universe_context = 'a * UState.t (*******************************************************************) (* Metamaps *) @@ -427,7 +414,7 @@ type evar_map = { undf_evars : evar_info EvMap.t; evar_names : EvNames.t; (** Universes *) - universes : evar_universe_context; + universes : UState.t; (** Conversion problems *) conv_pbs : evar_constraint list; last_mods : Evar.Set.t; @@ -558,10 +545,10 @@ let existential_type d (n, args) = instantiate_evar_array info info.evar_concl args let add_constraints d c = - { d with universes = add_constraints_context d.universes c } + { d with universes = UState.add_constraints d.universes c } let add_universe_constraints d c = - { d with universes = add_universe_constraints_context d.universes c } + { d with universes = UState.add_universe_constraints d.universes c } (*** /Lifting... ***) @@ -586,7 +573,7 @@ let create_evar_defs sigma = { sigma with let empty = { defn_evars = EvMap.empty; undf_evars = EvMap.empty; - universes = empty_evar_universe_context; + universes = UState.empty; conv_pbs = []; last_mods = Evar.Set.empty; metas = Metamap.empty; @@ -609,14 +596,14 @@ let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d = let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in let universes = if not with_univs then evd.universes - else union_evar_universe_context evd.universes d.universes + else UState.union evd.universes d.universes in { evd with metas = d.metas; last_mods; conv_pbs; universes } let merge_universe_context evd uctx' = - { evd with universes = union_evar_universe_context evd.universes uctx' } + { evd with universes = UState.union evd.universes uctx' } let set_universe_context evd uctx' = { evd with universes = uctx' } @@ -798,16 +785,6 @@ let make_flexible_variable evd ~algebraic u = { evd with universes = UState.make_flexible_variable evd.universes ~algebraic u } -let make_evar_universe_context e l = - let uctx = UState.make (Environ.universes e) in - match l with - | None -> uctx - | Some us -> - List.fold_left - (fun uctx { CAst.loc; v = id } -> - fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx)) - uctx us - (****************************************) (* Operations on constants *) (****************************************) @@ -910,10 +887,6 @@ let check_eq evd s s' = let check_leq evd s s' = UGraph.check_leq (UState.ugraph evd.universes) s s' -let normalize_evar_universe_context_variables = UState.normalize_variables - -let abstract_undefined_variables = UState.abstract_undefined_variables - let fix_undefined_variables evd = { evd with universes = UState.fix_undefined_variables evd.universes } @@ -922,16 +895,14 @@ let refresh_undefined_universes evd = let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in evd', subst -let normalize_evar_universe_context = UState.normalize - -let nf_univ_variables evd = - let subst, uctx' = normalize_evar_universe_context_variables evd.universes in +let nf_univ_variables evd = + let subst, uctx' = UState.normalize_variables evd.universes in let evd' = {evd with universes = uctx'} in evd', subst -let nf_constraints evd = - let subst, uctx' = normalize_evar_universe_context_variables evd.universes in - let uctx' = normalize_evar_universe_context uctx' in +let minimize_universes evd = + let subst, uctx' = UState.normalize_variables evd.universes in + let uctx' = UState.minimize uctx' in {evd with universes = uctx'} let universe_of_name evd s = UState.universe_of_name evd.universes s @@ -1076,7 +1047,7 @@ let clear_metas evd = {evd with metas = Metamap.empty} let meta_merge ?(with_univs = true) evd1 evd2 = let metas = Metamap.fold Metamap.add evd1.metas evd2.metas in let universes = - if with_univs then union_evar_universe_context evd2.universes evd1.universes + if with_univs then UState.union evd2.universes evd1.universes else evd2.universes in {evd2 with universes; metas; } @@ -1176,3 +1147,25 @@ module Monad = (* Failure explanation *) type unsolvability_explanation = SeveralInstancesFound of int + +(** Deprecated *) +type evar_universe_context = UState.t +let empty_evar_universe_context = UState.empty +let union_evar_universe_context = UState.union +let evar_universe_context_set = UState.context_set +let evar_universe_context_constraints = UState.constraints +let evar_context_universe_context = UState.context +let evar_universe_context_of = UState.of_context_set +let evar_universe_context_subst = UState.subst +let add_constraints_context = UState.add_constraints +let constrain_variables = UState.constrain_variables +let evar_universe_context_of_binders = UState.of_binders +let make_evar_universe_context e l = + let g = Environ.universes e in + match l with + | None -> UState.make g + | Some l -> UState.make_with_initial_binders g l +let normalize_evar_universe_context_variables = UState.normalize_variables +let abstract_undefined_variables = UState.abstract_undefined_variables +let normalize_evar_universe_context = UState.minimize +let nf_constraints = minimize_universes diff --git a/engine/evd.mli b/engine/evd.mli index ed3316c16..49c953f6d 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -493,22 +493,31 @@ val univ_flexible_alg : rigid type 'a in_evar_universe_context = 'a * UState.t val evar_universe_context_set : UState.t -> Univ.ContextSet.t +[@@ocaml.deprecated "Alias of UState.context_set"] val evar_universe_context_constraints : UState.t -> Univ.Constraint.t +[@@ocaml.deprecated "Alias of UState.constraints"] val evar_context_universe_context : UState.t -> Univ.UContext.t [@@ocaml.deprecated "alias of UState.context"] val evar_universe_context_of : Univ.ContextSet.t -> UState.t +[@@ocaml.deprecated "Alias of UState.of_context_set"] val empty_evar_universe_context : UState.t +[@@ocaml.deprecated "Alias of UState.empty"] val union_evar_universe_context : UState.t -> UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.union"] val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst +[@@ocaml.deprecated "Alias of UState.subst"] val constrain_variables : Univ.LSet.t -> UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.constrain_variables"] val evar_universe_context_of_binders : Universes.universe_binders -> UState.t +[@@ocaml.deprecated "Alias of UState.of_binders"] val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t +[@@ocaml.deprecated "Use UState.make or UState.make_with_initial_binders"] val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map (** Raises Not_found if not a name for a universe in this map. *) val universe_of_name : evar_map -> Id.t -> Univ.Level.t @@ -516,13 +525,15 @@ val universe_of_name : evar_map -> Id.t -> Univ.Level.t val universe_binders : evar_map -> Universes.universe_binders val add_constraints_context : UState.t -> Univ.Constraint.t -> UState.t +[@@ocaml.deprecated "Alias of UState.add_constraints"] val normalize_evar_universe_context_variables : UState.t -> Univ.universe_subst in_evar_universe_context +[@@ocaml.deprecated "Alias of UState.normalize_variables"] -val normalize_evar_universe_context : UState.t -> - UState.t +val normalize_evar_universe_context : UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.minimize"] val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t @@ -581,12 +592,16 @@ val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_co val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val abstract_undefined_variables : UState.t -> UState.t +[@@ocaml.deprecated "Alias of UState.abstract_undefined_variables"] val fix_undefined_variables : evar_map -> evar_map val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst +(** Universe minimization *) +val minimize_universes : evar_map -> evar_map val nf_constraints : evar_map -> evar_map +[@@ocaml.deprecated "Alias of Evd.minimize_universes"] val update_sigma_env : evar_map -> env -> evar_map diff --git a/engine/namegen.ml b/engine/namegen.ml index 33570ac73..d66b77b57 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -192,9 +192,45 @@ let it_mkLambda_or_LetIn_name env sigma b hyps = (**********************************************************************) (* Fresh names *) +(* Introduce a mode where auto-generated names are mangled + to test dependence of scripts on auto-generated names *) + +let mangle_names = ref false + +let _ = Goptions.( + declare_bool_option + { optdepr = false; + optname = "mangle auto-generated names"; + optkey = ["Mangle";"Names"]; + optread = (fun () -> !mangle_names); + optwrite = (:=) mangle_names; }) + +let mangle_names_prefix = ref (Id.of_string "_0") +let set_prefix x = mangle_names_prefix := forget_subscript x + +let set_mangle_names_mode x = begin + set_prefix x; + mangle_names := true + end + +let _ = Goptions.( + declare_string_option + { optdepr = false; + optname = "mangled names prefix"; + optkey = ["Mangle";"Names";"Prefix"]; + optread = (fun () -> Id.to_string !mangle_names_prefix); + optwrite = begin fun x -> + set_prefix + (try Id.of_string x + with CErrors.UserError _ -> CErrors.user_err Pp.(str ("Not a valid identifier: \"" ^ x ^ "\"."))) + end }) + +let mangle_id id = if !mangle_names then !mangle_names_prefix else id + (* Looks for next "good" name by lifting subscript *) let next_ident_away_from id bad = + let id = mangle_id id in let rec name_rec id = if bad id then name_rec (increment_subscript id) else id in name_rec id @@ -293,6 +329,7 @@ let next_global_ident_away id avoid = looks for same name with lower available subscript *) let next_ident_away id avoid = + let id = mangle_id id in if Id.Set.mem id avoid then next_ident_away_from (restart_subscript id) (fun id -> Id.Set.mem id avoid) else id @@ -423,23 +460,3 @@ let rename_bound_vars_as_displayed sigma avoid env c = | _ -> c in rename avoid env c - -(**********************************************************************) -(* "H"-based naming strategy introduced June 2014 for hypotheses in - Prop produced by case/elim/destruct/induction, in place of the - strategy that was using the first letter of the type, leading to - inelegant "n:~A", "e:t=u", etc. when eliminating sumbool or similar - types *) - -let h_based_elimination_names = ref false - -let use_h_based_elimination_names () = !h_based_elimination_names - -open Goptions - -let _ = declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "use of \"H\"-based proposition names in elimination tactics"; - optkey = ["Standard";"Proposition";"Elimination";"Names"]; - optread = (fun () -> !h_based_elimination_names); - optwrite = (:=) h_based_elimination_names } diff --git a/engine/namegen.mli b/engine/namegen.mli index d26634706..1b70ef68d 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -116,7 +116,6 @@ val compute_displayed_name_in_gen : (evar_map -> int -> 'a -> bool) -> evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t -(**********************************************************************) -(* Naming strategy for arguments in Prop when eliminating inductive types *) - -val use_h_based_elimination_names : unit -> bool +val set_mangle_names_mode : Id.t -> unit +(** Turn on mangled names mode and with the given prefix. + @raise UserError if the argument is invalid as an identifier. *) diff --git a/engine/termops.ml b/engine/termops.ml index c615155d1..35258762a 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -294,12 +294,11 @@ let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_cont let pr_evar_universe_context ctx = let open UState in - let open Evd in let prl = pr_uctx_level ctx in if UState.is_empty ctx then mt () else (str"UNIVERSES:"++brk(0,1)++ - h 0 (Univ.pr_universe_context_set prl (evar_universe_context_set ctx)) ++ fnl () ++ + h 0 (Univ.pr_universe_context_set prl (UState.context_set ctx)) ++ fnl () ++ str"ALGEBRAIC UNIVERSES:"++brk(0,1)++ h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++ str"UNDEFINED UNIVERSES:"++brk(0,1)++ diff --git a/engine/uState.ml b/engine/uState.ml index 00825208b..e57afd743 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -476,6 +476,13 @@ let new_univ_variable ?loc rigid name uctx_initial_universes = initial} in uctx', u +let make_with_initial_binders e us = + let uctx = make e in + List.fold_left + (fun uctx { CAst.loc; v = id } -> + fst (new_univ_variable ?loc univ_rigid (Some id) uctx)) + uctx us + let add_global_univ uctx u = let initial = UGraph.add_universe u true uctx.uctx_initial_universes @@ -578,7 +585,7 @@ let refresh_undefined_univ_variables uctx = uctx_initial_universes = initial } in uctx', subst -let normalize uctx = +let minimize uctx = let ((vars',algs'), us') = Universes.normalize_context_set uctx.uctx_local uctx.uctx_univ_variables uctx.uctx_univ_algebraic @@ -606,3 +613,6 @@ let update_sigma_env uctx env = uctx_universes = univs } in merge true univ_rigid eunivs eunivs.uctx_local + +(** Deprecated *) +let normalize = minimize diff --git a/engine/uState.mli b/engine/uState.mli index 68fe350c0..9a2bc706b 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -26,6 +26,8 @@ val empty : t val make : UGraph.t -> t +val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t + val is_empty : t -> bool val union : t -> t -> t @@ -131,7 +133,10 @@ val fix_undefined_variables : t -> t val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst +(** Universe minimization *) +val minimize : t -> t val normalize : t -> t +[@@ocaml.deprecated "Alias of UState.minimize"] type universe_decl = (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 40945939f..d6c340f69 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -8,27 +8,32 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +type arg_source = CmdLine | ProjectFile + +type 'a sourced = { thing : 'a; source : arg_source } + type project = { project_file : string option; makefile : string option; install_kind : install option; use_ocamlopt : bool; - v_files : string list; - mli_files : string list; - ml4_files : string list; - ml_files : string list; - mllib_files : string list; - mlpack_files : string list; - - ml_includes : path list; - r_includes : (path * logic_path) list; - q_includes : (path * logic_path) list; - extra_args : string list; - defs : (string * string) list; - - extra_targets : extra_target list; - subdirs : string list; + v_files : string sourced list; + mli_files : string sourced list; + ml4_files : string sourced list; + ml_files : string sourced list; + mllib_files : string sourced list; + mlpack_files : string sourced list; + + ml_includes : path sourced list; + r_includes : (path * logic_path) sourced list; + q_includes : (path * logic_path) sourced list; + extra_args : string sourced list; + defs : (string * string) sourced list; + + (* deprecated in favor of a Makefile.local using :: rules *) + extra_targets : extra_target sourced list; + subdirs : string sourced list; } and extra_target = { target : string; @@ -114,6 +119,7 @@ let exists_dir dir = let process_cmd_line orig_dir proj args = let parsing_project_file = ref (proj.project_file <> None) in + let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in let orig_dir = (* avoids turning foo.v in ./foo.v *) if orig_dir = "." then "" else orig_dir in let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in @@ -143,17 +149,17 @@ let process_cmd_line orig_dir proj args = aux { proj with install_kind = Some install } r | "-extra" :: target :: dependencies :: command :: r -> let tgt = { target; dependencies; phony = false; command } in - aux { proj with extra_targets = proj.extra_targets @ [tgt] } r + aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r | "-extra-phony" :: target :: dependencies :: command :: r -> let tgt = { target; dependencies; phony = true; command } in - aux { proj with extra_targets = proj.extra_targets @ [tgt] } r + aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r | "-Q" :: d :: lp :: r -> - aux { proj with q_includes = proj.q_includes @ [mk_path d,lp] } r + aux { proj with q_includes = proj.q_includes @ [sourced (mk_path d,lp)] } r | "-I" :: d :: r -> - aux { proj with ml_includes = proj.ml_includes @ [mk_path d] } r + aux { proj with ml_includes = proj.ml_includes @ [sourced (mk_path d)] } r | "-R" :: d :: lp :: r -> - aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r + aux { proj with r_includes = proj.r_includes @ [sourced (mk_path d,lp)] } r | "-f" :: file :: r -> if !parsing_project_file then @@ -178,20 +184,21 @@ let process_cmd_line orig_dir proj args = error "Option -o given more than once"; aux { proj with makefile = Some file } r | v :: "=" :: def :: r -> - aux { proj with defs = proj.defs @ [v,def] } r + aux { proj with defs = proj.defs @ [sourced (v,def)] } r | "-arg" :: a :: r -> - aux { proj with extra_args = proj.extra_args @ [a] } r + aux { proj with extra_args = proj.extra_args @ [sourced a] } r | f :: r -> let f = CUnix.correct_path f orig_dir in let proj = - if exists_dir f then { proj with subdirs = proj.subdirs @ [f] } + if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] } else match CUnix.get_extension f with - | ".v" -> { proj with v_files = proj.v_files @ [f] } - | ".ml" -> { proj with ml_files = proj.ml_files @ [f] } - | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [f] } - | ".mli" -> { proj with mli_files = proj.mli_files @ [f] } - | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [f] } - | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [f] } + | ".v" -> + { proj with v_files = proj.v_files @ [sourced f] } + | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] } + | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] } + | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] } + | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] } + | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced f] } | _ -> raise (Parsing_error ("Unknown option "^f)) in aux proj r in @@ -215,16 +222,34 @@ let rec find_project_file ~from ~projfile_name = else find_project_file ~from:newdir ~projfile_name ;; +let all_files { v_files; ml_files; mli_files; ml4_files; + mllib_files; mlpack_files } = + v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files + +let map_sourced_list f l = List.map (fun x -> f x.thing) l +;; + +let map_cmdline f l = CList.map_filter (function + | {thing=x; source=CmdLine} -> Some (f x) + | {source=ProjectFile} -> None) l + let coqtop_args_from_project { ml_includes; r_includes; q_includes; extra_args } = - let map = List.map in + let map = map_sourced_list in let args = map (fun { canonical_path = i } -> ["-I"; i]) ml_includes @ map (fun ({ canonical_path = i }, l) -> ["-Q"; i; l]) q_includes @ map (fun ({ canonical_path = p }, l) -> ["-R"; p; l]) r_includes @ - [extra_args] in + [map (fun x -> x) extra_args] in List.flatten args ;; +let filter_cmdline l = CList.map_filter + (function {thing; source=CmdLine} -> Some thing | {source=ProjectFile} -> None) + l +;; + +let forget_source {thing} = thing + (* vim:set ft=ocaml: *) diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli index 5a4dd3659..5780bb5d7 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -10,29 +10,32 @@ exception Parsing_error of string +type arg_source = CmdLine | ProjectFile + +type 'a sourced = { thing : 'a; source : arg_source } + type project = { project_file : string option; makefile : string option; install_kind : install option; use_ocamlopt : bool; - v_files : string list; - mli_files : string list; - ml4_files : string list; - ml_files : string list; - mllib_files : string list; - mlpack_files : string list; + v_files : string sourced list; + mli_files : string sourced list; + ml4_files : string sourced list; + ml_files : string sourced list; + mllib_files : string sourced list; + mlpack_files : string sourced list; - ml_includes : path list; - r_includes : (path * logic_path) list; - q_includes : (path * logic_path) list; - extra_args : string list; - defs : (string * string) list; + ml_includes : path sourced list; + r_includes : (path * logic_path) sourced list; + q_includes : (path * logic_path) sourced list; + extra_args : string sourced list; + defs : (string * string) sourced list; (* deprecated in favor of a Makefile.local using :: rules *) - extra_targets : extra_target list; - subdirs : string list; - + extra_targets : extra_target sourced list; + subdirs : string sourced list; } and extra_target = { target : string; @@ -52,3 +55,14 @@ val read_project_file : string -> project val coqtop_args_from_project : project -> string list val find_project_file : from:string -> projfile_name:string -> string option +val all_files : project -> string sourced list + +val map_sourced_list : ('a -> 'b) -> 'a sourced list -> 'b list + +(** Only uses the elements with source=CmdLine *) +val map_cmdline : ('a -> 'b) -> 'a sourced list -> 'b list + +(** Only uses the elements with source=CmdLine *) +val filter_cmdline : 'a sourced list -> 'a list + +val forget_source : 'a sourced -> 'a diff --git a/library/summary.ml b/library/summary.ml index 6ca871555..7ef19fbfb 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -89,6 +89,16 @@ let unfreeze_single name state = Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]); iraise e +let warn_summary_out_of_scope = + let name = "summary-out-of-scope" in + let category = "dev" in + let default = CWarnings.Disabled in + CWarnings.create ~name ~category ~default (fun name -> + Pp.str (Printf.sprintf + "A Coq plugin was loaded inside a local scope (such as a Section). It is recommended to load plugins at the start of the file. Summary entry: %s" + name) + ) + let unfreeze_summaries ?(partial=false) { summaries; ml_module } = (* The unfreezing of [ml_modules_summary] has to be anticipated since it * may modify the content of [summaries] by loading new ML modules *) @@ -101,7 +111,7 @@ let unfreeze_summaries ?(partial=false) { summaries; ml_module } = try decl.unfreeze_function String.Map.(find name summaries) with Not_found -> if not partial then begin - Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name); + warn_summary_out_of_scope name; decl.init_function () end; in diff --git a/man/coqdep.1 b/man/coqdep.1 index ed727db7c..c417402c2 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -80,6 +80,9 @@ Prints the dependencies of Caml modules. \" of each Coq file given as argument and complete (if needed) \" the list of Caml modules. The new command is printed on \" the standard output. No dependency is computed with this option. +.TP +.BI \-f \ file +Read filenames and options -I, -R and -Q from a _CoqProject FILE. .TP .BI \-I/\-Q/\-R \ options Have the same effects on load path and modules names as for other diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 430d18893..e393c2bbf 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -21,6 +21,24 @@ let thm_token = G_vernac.thm_token let hint = Gram.entry_create "hint" +let warn_deprecated_focus = + CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" + (fun () -> + Pp.strbrk + "The Focus command is deprecated; use bullets or focusing brackets instead" + ) + +let warn_deprecated_focus_n n = + CWarnings.create ~name:"deprecated-focus" ~category:"deprecated" + (fun () -> + Pp.(str "The Focus command is deprecated;" ++ spc () + ++ str "use '" ++ int n ++ str ": {' instead") + ) + +let warn_deprecated_unfocus = + CWarnings.create ~name:"deprecated-unfocus" ~category:"deprecated" + (fun () -> Pp.strbrk "The Unfocus command is deprecated") + (* Proof commands *) GEXTEND Gram GLOBAL: hint command; @@ -51,9 +69,15 @@ GEXTEND Gram | IDENT "Undo" -> VernacUndo 1 | IDENT "Undo"; n = natural -> VernacUndo n | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n - | IDENT "Focus" -> VernacFocus None - | IDENT "Focus"; n = natural -> VernacFocus (Some n) - | IDENT "Unfocus" -> VernacUnfocus + | IDENT "Focus" -> + warn_deprecated_focus ~loc:!@loc (); + VernacFocus None + | IDENT "Focus"; n = natural -> + warn_deprecated_focus_n n ~loc:!@loc (); + VernacFocus (Some n) + | IDENT "Unfocus" -> + warn_deprecated_unfocus ~loc:!@loc (); + VernacUnfocus | IDENT "Unfocused" -> VernacUnfocused | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 722b3990c..a4e8c44cd 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -137,22 +137,25 @@ let check_arity env cb = let t = cb.const_type in if Reduction.is_arity env t then raise Impossible -let check_fix env cb i = +let get_body lbody = + EConstr.of_constr (Mod_subst.force_constr lbody) + +let check_fix env sg cb i = match cb.const_body with | Def lbody -> - (match Constr.kind (Mod_subst.force_constr lbody) with - | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd) + (match EConstr.kind sg (get_body lbody) with + | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd) | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd) | _ -> raise Impossible) | Undef _ | OpaqueDef _ -> raise Impossible -let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) = +let prec_declaration_equal sg (na1, ca1, ta1) (na2, ca2, ta2) = Array.equal Name.equal na1 na2 && - Array.equal Constr.equal ca1 ca2 && - Array.equal Constr.equal ta1 ta2 + Array.equal (EConstr.eq_constr sg) ca1 ca2 && + Array.equal (EConstr.eq_constr sg) ta1 ta2 -let factor_fix env l cb msb = - let _,recd as check = check_fix env cb 0 in +let factor_fix env sg l cb msb = + let _,recd as check = check_fix env sg cb 0 in let n = Array.length (let fi,_,_ = recd in fi) in if Int.equal n 1 then [|l|], recd, msb else begin @@ -163,9 +166,9 @@ let factor_fix env l cb msb = (fun j -> function | (l,SFBconst cb') -> - let check' = check_fix env cb' (j+1) in - if not ((fst check : bool) == (fst check') && - prec_declaration_equal (snd check) (snd check')) + let check' = check_fix env sg cb' (j+1) in + if not ((fst check : bool) == (fst check') && + prec_declaration_equal sg (snd check) (snd check')) then raise Impossible; labels.(j+1) <- l; | _ -> raise Impossible) msb'; @@ -248,7 +251,9 @@ and extract_mexpr_spec env mp1 (me_struct_o,me_alg) = match me_alg with let me_struct,delta = flatten_modtype env mp1 me' me_struct_o in let env' = env_for_mtb_with_def env mp1 me_struct delta idl in let mt = extract_mexpr_spec env mp1 (None,me') in - (match extract_with_type env' c with (* cb may contain some kn *) + let sg = Evd.from_env env in + (match extract_with_type env' sg (EConstr.of_constr c) with + (* cb may contain some kn *) | None -> mt | Some (vl,typ) -> type_iter_references Visit.add_ref typ; @@ -299,12 +304,13 @@ let rec extract_structure env mp reso ~all = function | [] -> [] | (l,SFBconst cb) :: struc -> (try - let vl,recd,struc = factor_fix env l cb struc in + let sg = Evd.from_env env in + let vl,recd,struc = factor_fix env sg l cb struc in let vc = Array.map (make_cst reso mp) vl in let ms = extract_structure env mp reso ~all struc in let b = Array.exists Visit.needed_cst vc in if all || b then - let d = extract_fixpoint env vc recd in + let d = extract_fixpoint env sg vc recd in if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms @@ -572,8 +578,8 @@ let print_structure_to_file (fn,si,mo) dry struc = let reset () = Visit.reset (); reset_tables (); reset_renaming_tables Everything -let init ?(compute=false) modular library = - check_inside_section (); check_inside_module (); +let init ?(compute=false) ?(inner=false) modular library = + if not inner then (check_inside_section (); check_inside_module ()); set_keywords (descr ()).keywords; set_modular modular; set_library library; @@ -701,10 +707,9 @@ let flatten_structure struc = and flatten_elems l = List.flatten (List.map flatten_elem l) in flatten_elems (List.flatten (List.map snd struc)) -let structure_for_compute c = +let structure_for_compute env sg c = init false false ~compute:true; - let env = Global.env () in - let ast, mlt = Extraction.extract_constr env c in + let ast, mlt = Extraction.extract_constr env sg c in let ast = Mlutil.normalize ast in let refs = ref Refset.empty in let add_ref r = refs := Refset.add r !refs in @@ -744,3 +749,20 @@ let extract_and_compile l = let base = Filename.chop_suffix f ".ml" in let () = remove (base^".cmo"); remove (base^".cmi") in Feedback.msg_notice (str "Extracted code successfully compiled") + +(* Show the extraction of the current ongoing proof *) + +let show_extraction () = + init ~inner:true false false; + let prf = Proof_global.give_me_the_proof () in + let sigma, env = Pfedit.get_current_context () in + let trms = Proof.partial_proof prf in + let extr_term t = + let ast, ty = extract_constr env sigma t in + let mp = Lib.current_mp () in + let l = Label.of_id (Proof_global.get_current_proof_name ()) in + let fake_ref = ConstRef (Constant.make2 mp l) in + let decl = Dterm (fake_ref, ast, ty) in + print_one_decl [] mp decl + in + Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl extr_term trms) diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 464f109be..591d3bb86 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -36,4 +36,9 @@ val print_one_decl : (* Used by Extraction Compute *) val structure_for_compute : - Constr.t -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type + Environ.env -> Evd.evar_map -> EConstr.t -> + Miniml.ml_decl list * Miniml.ml_ast * Miniml.ml_type + +(* Show the extraction of the current ongoing proof *) + +val show_extraction : unit -> unit diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index ce4970056..f25f63624 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -13,7 +13,6 @@ open Util open Names open Term open Constr -open Vars open Declarations open Declareops open Environ @@ -36,20 +35,18 @@ exception I of inductive_kind (* A set of all fixpoint functions currently being extracted *) let current_fixpoints = ref ([] : Constant.t list) -let none = Evd.empty - (* NB: In OCaml, [type_of] and [get_of] might raise [SingletonInductiveBecomeProp]. This exception will be caught in late wrappers around the exported functions of this file, in order to display the location of the issue. *) -let type_of env c = +let type_of env sg c = let polyprop = (lang() == Haskell) in - EConstr.Unsafe.to_constr (Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c))) + Retyping.get_type_of ~polyprop env sg (strip_outer_cast sg c) -let sort_of env c = +let sort_of env sg c = let polyprop = (lang() == Haskell) in - Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)) + Retyping.get_sort_family_of ~polyprop env sg (strip_outer_cast sg c) (*S Generation of flags and signatures. *) @@ -73,61 +70,91 @@ type scheme = TypeScheme | Default type flag = info * scheme -let whd_all env t = - EConstr.Unsafe.to_constr (whd_all env none (EConstr.of_constr t)) - -let whd_betaiotazeta t = - EConstr.Unsafe.to_constr (whd_betaiotazeta none (EConstr.of_constr t)) - (*s [flag_of_type] transforms a type [t] into a [flag]. Really important function. *) -let rec flag_of_type env t : flag = - let t = whd_all env t in - match Constr.kind t with - | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c - | Sort s when Sorts.is_prop s -> (Logic,TypeScheme) +let rec flag_of_type env sg t : flag = + let t = whd_all env sg t in + match EConstr.kind sg t with + | Prod (x,t,c) -> flag_of_type (EConstr.push_rel (LocalAssum (x,t)) env) sg c + | Sort s when Sorts.is_prop (EConstr.ESorts.kind sg s) -> (Logic,TypeScheme) | Sort _ -> (Info,TypeScheme) - | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default) + | _ -> if (sort_of env sg t) == InProp then (Logic,Default) else (Info,Default) (*s Two particular cases of [flag_of_type]. *) -let is_default env t = match flag_of_type env t with +let is_default env sg t = match flag_of_type env sg t with | (Info, Default) -> true | _ -> false exception NotDefault of kill_reason -let check_default env t = - match flag_of_type env t with +let check_default env sg t = + match flag_of_type env sg t with | _,TypeScheme -> raise (NotDefault Ktype) | Logic,_ -> raise (NotDefault Kprop) | _ -> () -let is_info_scheme env t = match flag_of_type env t with +let is_info_scheme env sg t = match flag_of_type env sg t with | (Info, TypeScheme) -> true | _ -> false let push_rel_assum (n, t) env = - Environ.push_rel (LocalAssum (n, t)) env + EConstr.push_rel (LocalAssum (n, t)) env + +let push_rels_assum assums = + EConstr.push_rel_context (List.map (fun (x,t) -> LocalAssum (x,t)) assums) + +let get_body lconstr = EConstr.of_constr (Mod_subst.force_constr lconstr) + +let get_opaque env c = + EConstr.of_constr + (Opaqueproof.force_proof (Environ.opaque_tables env) c) + +let applistc c args = EConstr.mkApp (c, Array.of_list args) + +(* Same as [Environ.push_rec_types], but for [EConstr.t] *) +let push_rec_types (lna,typarray,_) env = + let ctxt = + Array.map2_i + (fun i na t -> LocalAssum (na, EConstr.Vars.lift i t)) lna typarray + in + Array.fold_left (fun e assum -> EConstr.push_rel assum e) env ctxt + +(* Same as [Termops.nb_lam], but for [EConstr.t] *) +let nb_lam sg c = List.length (fst (EConstr.decompose_lam sg c)) + +(* Same as [Term.decompose_lam_n] but for [EConstr.t] *) +let decompose_lam_n sg n = + let rec lamdec_rec l n c = + if n <= 0 then l,c + else match EConstr.kind sg c with + | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c + | Cast (c,_,_) -> lamdec_rec l n c + | _ -> raise Not_found + in + lamdec_rec [] n (*s [type_sign] gernerates a signature aimed at treating a type application. *) -let rec type_sign env c = - match Constr.kind (whd_all env c) with +let rec type_sign env sg c = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> - (if is_info_scheme env t then Keep else Kill Kprop) - :: (type_sign (push_rel_assum (n,t) env) d) + (if is_info_scheme env sg t then Keep else Kill Kprop) + :: (type_sign (push_rel_assum (n,t) env) sg d) | _ -> [] -let rec type_scheme_nb_args env c = - match Constr.kind (whd_all env c) with +let rec type_scheme_nb_args env sg c = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> - let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in - if is_info_scheme env t then n+1 else n + let n = type_scheme_nb_args (push_rel_assum (n,t) env) sg d in + if is_info_scheme env sg t then n+1 else n | _ -> 0 -let _ = Hook.set type_scheme_nb_args_hook type_scheme_nb_args +let type_scheme_nb_args' env c = + type_scheme_nb_args env (Evd.from_env env) (EConstr.of_constr c) + +let _ = Hook.set type_scheme_nb_args_hook type_scheme_nb_args' (*s [type_sign_vl] does the same, plus a type var list. *) @@ -147,19 +174,19 @@ let make_typvar n vl = let vl = Id.Set.of_list vl in next_ident_away id' vl -let rec type_sign_vl env c = - match Constr.kind (whd_all env c) with +let rec type_sign_vl env sg c = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> - let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in - if not (is_info_scheme env t) then Kill Kprop::s, vl - else Keep::s, (make_typvar n vl) :: vl + let s,vl = type_sign_vl (push_rel_assum (n,t) env) sg d in + if not (is_info_scheme env sg t) then Kill Kprop::s, vl + else Keep::s, (make_typvar n vl) :: vl | _ -> [],[] -let rec nb_default_params env c = - match Constr.kind (whd_all env c) with +let rec nb_default_params env sg c = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> - let n = nb_default_params (push_rel_assum (n,t) env) d in - if is_default env t then n+1 else n + let n = nb_default_params (push_rel_assum (n,t) env) sg d in + if is_default env sg t then n+1 else n | _ -> 0 (* Enriching a signature with implicit information *) @@ -226,62 +253,62 @@ let parse_ind_args si args relmax = generate ML type var anymore (in subterms for example). *) -let rec extract_type env db j c args = - match Constr.kind (whd_betaiotazeta c) with +let rec extract_type env sg db j c args = + match EConstr.kind sg (whd_betaiotazeta sg c) with | App (d, args') -> - (* We just accumulate the arguments. *) - extract_type env db j d (Array.to_list args' @ args) + (* We just accumulate the arguments. *) + extract_type env sg db j d (Array.to_list args' @ args) | Lambda (_,_,d) -> (match args with | [] -> assert false (* A lambda cannot be a type. *) - | a :: args -> extract_type env db j (subst1 a d) args) + | a :: args -> extract_type env sg db j (EConstr.Vars.subst1 a d) args) | Prod (n,t,d) -> assert (List.is_empty args); let env' = push_rel_assum (n,t) env in - (match flag_of_type env t with + (match flag_of_type env sg t with | (Info, Default) -> (* Standard case: two [extract_type] ... *) - let mld = extract_type env' (0::db) j d [] in + let mld = extract_type env' sg (0::db) j d [] in (match expand env mld with | Tdummy d -> Tdummy d - | _ -> Tarr (extract_type env db 0 t [], mld)) + | _ -> Tarr (extract_type env sg db 0 t [], mld)) | (Info, TypeScheme) when j > 0 -> (* A new type var. *) - let mld = extract_type env' (j::db) (j+1) d [] in + let mld = extract_type env' sg (j::db) (j+1) d [] in (match expand env mld with | Tdummy d -> Tdummy d | _ -> Tarr (Tdummy Ktype, mld)) | _,lvl -> - let mld = extract_type env' (0::db) j d [] in + let mld = extract_type env' sg (0::db) j d [] in (match expand env mld with | Tdummy d -> Tdummy d | _ -> let reason = if lvl == TypeScheme then Ktype else Kprop in Tarr (Tdummy reason, mld))) | Sort _ -> Tdummy Ktype (* The two logical cases. *) - | _ when sort_of env (applistc c args) == InProp -> Tdummy Kprop + | _ when sort_of env sg (applistc c args) == InProp -> Tdummy Kprop | Rel n -> - (match lookup_rel n env with - | LocalDef (_,t,_) -> extract_type env db j (lift n t) args + (match EConstr.lookup_rel n env with + | LocalDef (_,t,_) -> + extract_type env sg db j (EConstr.Vars.lift n t) args | _ -> (* Asks [db] a translation for [n]. *) if n > List.length db then Tunknown else let n' = List.nth db (n-1) in if Int.equal n' 0 then Tunknown else Tvar n') - | Const (kn,u as c) -> - let r = ConstRef kn in - let cb = lookup_constant kn env in - let typ = Typeops.type_of_constant_in env c in - (match flag_of_type env typ with + | Const (kn,u) -> + let r = ConstRef kn in + let typ = type_of env sg (EConstr.mkConstU (kn,u)) in + (match flag_of_type env sg typ with | (Logic,_) -> assert false (* Cf. logical cases above *) | (Info, TypeScheme) -> - let mlt = extract_type_app env db (r, type_sign env typ) args in - (match cb.const_body with + let mlt = extract_type_app env sg db (r, type_sign env sg typ) args in + (match (lookup_constant kn env).const_body with | Undef _ | OpaqueDef _ -> mlt - | Def _ when is_custom r -> mlt + | Def _ when is_custom (ConstRef kn) -> mlt | Def lbody -> - let newc = applistc (Mod_subst.force_constr lbody) args in - let mlt' = extract_type env db j newc [] in + let newc = applistc (get_body lbody) args in + let mlt' = extract_type env sg db j newc [] in (* ML type abbreviations interact badly with Coq *) (* reduction, so [mlt] and [mlt'] might be different: *) (* The more precise is [mlt'], extracted after reduction *) @@ -290,36 +317,51 @@ let rec extract_type env db j c args = if eq_ml_type (expand env mlt) (expand env mlt') then mlt else mlt') | (Info, Default) -> (* Not an ML type, for example [(c:forall X, X->X) Type nat] *) - (match cb.const_body with + (match (lookup_constant kn env).const_body with | Undef _ | OpaqueDef _ -> Tunknown (* Brutal approx ... *) | Def lbody -> (* We try to reduce. *) - let newc = applistc (Mod_subst.force_constr lbody) args in - extract_type env db j newc [])) + let newc = applistc (get_body lbody) args in + extract_type env sg db j newc [])) | Ind ((kn,i),u) -> - let s = (extract_ind env kn).ind_packets.(i).ip_sign in - extract_type_app env db (IndRef (kn,i),s) args + let s = (extract_ind env kn).ind_packets.(i).ip_sign in + extract_type_app env sg db (IndRef (kn,i),s) args | Proj (p,t) -> (* Let's try to reduce, if it hasn't already been done. *) if Projection.unfolded p then Tunknown - else extract_type env db j (mkProj (Projection.unfold p, t)) args + else + extract_type env sg db j (EConstr.mkProj (Projection.unfold p, t)) args | Case _ | Fix _ | CoFix _ -> Tunknown - | Var _ | Meta _ | Evar _ | Cast _ | LetIn _ | Construct _ -> assert false + | Evar _ | Meta _ -> Taxiom (* only possible during Show Extraction *) + | Var v -> + (* For Show Extraction *) + let open Context.Named.Declaration in + (match EConstr.lookup_named v env with + | LocalDef (_,body,_) -> + extract_type env sg db j (EConstr.applist (body,args)) [] + | LocalAssum (_,ty) -> + let r = VarRef v in + (match flag_of_type env sg ty with + | (Logic,_) -> assert false (* Cf. logical cases above *) + | (Info, TypeScheme) -> + extract_type_app env sg db (r, type_sign env sg ty) args + | (Info, Default) -> Tunknown)) + | Cast _ | LetIn _ | Construct _ -> assert false (*s Auxiliary function dealing with type application. Precondition: [r] is a type scheme represented by the signature [s], and is completely applied: [List.length args = List.length s]. *) -and extract_type_app env db (r,s) args = +and extract_type_app env sg db (r,s) args = let ml_args = List.fold_right (fun (b,c) a -> if b == Keep then - let p = List.length (fst (splay_prod env none (EConstr.of_constr (type_of env c)))) in + let p = List.length (fst (splay_prod env sg (type_of env sg c))) in let db = iterate (fun l -> 0 :: l) p db in - (extract_type_scheme env db c p) :: a + (extract_type_scheme env sg db c p) :: a else a) (List.combine s args) [] - in Tglob (r, ml_args) + in Tglob (r, ml_args) (*S Extraction of a type scheme. *) @@ -330,19 +372,18 @@ and extract_type_app env db (r,s) args = (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *) -and extract_type_scheme env db c p = - if Int.equal p 0 then extract_type env db 0 c [] +and extract_type_scheme env sg db c p = + if Int.equal p 0 then extract_type env sg db 0 c [] else - let c = whd_betaiotazeta c in - match Constr.kind c with + let c = whd_betaiotazeta sg c in + match EConstr.kind sg c with | Lambda (n,t,d) -> - extract_type_scheme (push_rel_assum (n,t) env) db d (p-1) + extract_type_scheme (push_rel_assum (n,t) env) sg db d (p-1) | _ -> - let rels = fst (splay_prod env none (EConstr.of_constr (type_of env c))) in - let rels = List.map (on_snd EConstr.Unsafe.to_constr) rels in + let rels = fst (splay_prod env sg (type_of env sg c)) in let env = push_rels_assum rels env in - let eta_args = List.rev_map mkRel (List.interval 1 p) in - extract_type env db 0 (lift p c) eta_args + let eta_args = List.rev_map EConstr.mkRel (List.interval 1 p) in + extract_type env sg db 0 (EConstr.Vars.lift p c) eta_args (*S Extraction of an inductive type. *) @@ -384,6 +425,7 @@ and extract_really_ind env kn mib = let mip0 = mib.mind_packets.(0) in let npar = mib.mind_nparams in let epar = push_rel_context mib.mind_params_ctxt env in + let sg = Evd.from_env env in (* First pass: we store inductive signatures together with *) (* their type var list. *) let packets = @@ -391,8 +433,9 @@ and extract_really_ind env kn mib = (fun i mip -> let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in let ar = Inductive.type_of_inductive env ((mib,mip),u) in - let info = (fst (flag_of_type env ar) = Info) in - let s,v = if info then type_sign_vl env ar else [],[] in + let ar = EConstr.of_constr ar in + let info = (fst (flag_of_type env sg ar) = Info) in + let s,v = if info then type_sign_vl env sg ar else [],[] in let t = Array.make (Array.length mip.mind_nf_lc) [] in { ip_typename = mip.mind_typename; ip_consnames = mip.mind_consnames; @@ -424,7 +467,8 @@ and extract_really_ind env kn mib = in let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in let db = db_from_ind dbmap npar in - p.ip_types.(j) <- extract_type_cons epar db dbmap t (npar+1) + p.ip_types.(j) <- + extract_type_cons epar sg db dbmap (EConstr.of_constr t) (npar+1) done done; (* Third pass: we determine special cases. *) @@ -477,10 +521,9 @@ and extract_really_ind env kn mib = (* Is this record officially declared with its projections ? *) (* If so, we use this information. *) begin try - let n = nb_default_params env - (Inductive.type_of_inductive env ((mib,mip0),u)) - in - let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip + let ty = Inductive.type_of_inductive env ((mib,mip0),u) in + let n = nb_default_params env sg (EConstr.of_constr ty) in + let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip in List.iter (Option.iter check_proj) (lookup_projections ip) with Not_found -> () @@ -505,13 +548,13 @@ and extract_really_ind env kn mib = - [i] is the rank of the current product (initially [params_nb+1]) *) -and extract_type_cons env db dbmap c i = - match Constr.kind (whd_all env c) with +and extract_type_cons env sg db dbmap c i = + match EConstr.kind sg (whd_all env sg c) with | Prod (n,t,d) -> let env' = push_rel_assum (n,t) env in let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in - let l = extract_type_cons env' db' dbmap d (i+1) in - (extract_type env db 0 t []) :: l + let l = extract_type_cons env' sg db' dbmap d (i+1) in + (extract_type env sg db 0 t []) :: l | _ -> [] (*s Recording the ML type abbreviation of a Coq type scheme constant. *) @@ -526,16 +569,17 @@ and mlt_env env r = match r with match lookup_typedef kn cb with | Some _ as o -> o | None -> - let typ = cb.const_type + let sg = Evd.from_env env in + let typ = EConstr.of_constr cb.const_type (* FIXME not sure if we should instantiate univs here *) in - match flag_of_type env typ with - | Info,TypeScheme -> - let body = Mod_subst.force_constr l_body in - let s = type_sign env typ in - let db = db_from_sign s in - let t = extract_type_scheme env db body (List.length s) - in add_typedef kn cb t; Some t - | _ -> None + match flag_of_type env sg typ with + | Info,TypeScheme -> + let body = get_body l_body in + let s = type_sign env sg typ in + let db = db_from_sign s in + let t = extract_type_scheme env sg db body (List.length s) + in add_typedef kn cb t; Some t + | _ -> None and expand env = type_expand (mlt_env env) and type2signature env = type_to_signature (mlt_env env) @@ -545,16 +589,16 @@ let type_expunge_from_sign env = type_expunge_from_sign (mlt_env env) (*s Extraction of the type of a constant. *) -let record_constant_type env kn opt_typ = +let record_constant_type env sg kn opt_typ = let cb = lookup_constant kn env in match lookup_cst_type kn cb with | Some schema -> schema | None -> let typ = match opt_typ with - | None -> cb.const_type + | None -> EConstr.of_constr cb.const_type | Some typ -> typ in - let mlt = extract_type env [] 1 typ [] in + let mlt = extract_type env sg [] 1 typ [] in let schema = (type_maxvar mlt, mlt) in let () = add_cst_type kn cb schema in schema @@ -566,75 +610,86 @@ let record_constant_type env kn opt_typ = (* [mle] is a ML environment [Mlenv.t]. *) (* [mlt] is the ML type we want our extraction of [(c args)] to have. *) -let rec extract_term env mle mlt c args = - match Constr.kind c with +let rec extract_term env sg mle mlt c args = + match EConstr.kind sg c with | App (f,a) -> - extract_term env mle mlt f (Array.to_list a @ args) + extract_term env sg mle mlt f (Array.to_list a @ args) | Lambda (n, t, d) -> let id = id_of_name n in (match args with | a :: l -> (* We make as many [LetIn] as possible. *) - let d' = mkLetIn (Name id,a,t,applistc d (List.map (lift 1) l)) - in extract_term env mle mlt d' [] + let l' = List.map (EConstr.Vars.lift 1) l in + let d' = EConstr.mkLetIn (Name id,a,t,applistc d l') in + extract_term env sg mle mlt d' [] | [] -> let env' = push_rel_assum (Name id, t) env in let id, a = - try check_default env t; Id id, new_meta() - with NotDefault d -> Dummy, Tdummy d + try check_default env sg t; Id id, new_meta() + with NotDefault d -> Dummy, Tdummy d in let b = new_meta () in (* If [mlt] cannot be unified with an arrow type, then magic! *) let magic = needs_magic (mlt, Tarr (a, b)) in - let d' = extract_term env' (Mlenv.push_type mle a) b d [] in + let d' = extract_term env' sg (Mlenv.push_type mle a) b d [] in put_magic_if magic (MLlam (id, d'))) | LetIn (n, c1, t1, c2) -> let id = id_of_name n in - let env' = push_rel (LocalDef (Name id, c1, t1)) env in + let env' = EConstr.push_rel (LocalDef (Name id, c1, t1)) env in (* We directly push the args inside the [LetIn]. TODO: the opt_let_app flag is supposed to prevent that *) - let args' = List.map (lift 1) args in + let args' = List.map (EConstr.Vars.lift 1) args in (try - check_default env t1; + check_default env sg t1; let a = new_meta () in - let c1' = extract_term env mle a c1 [] in + let c1' = extract_term env sg mle a c1 [] in (* The type of [c1'] is generalized and stored in [mle]. *) let mle' = if generalizable c1' then Mlenv.push_gen mle a else Mlenv.push_type mle a in - MLletin (Id id, c1', extract_term env' mle' mlt c2 args') + MLletin (Id id, c1', extract_term env' sg mle' mlt c2 args') with NotDefault d -> let mle' = Mlenv.push_std_type mle (Tdummy d) in - ast_pop (extract_term env' mle' mlt c2 args')) + ast_pop (extract_term env' sg mle' mlt c2 args')) | Const (kn,_) -> - extract_cst_app env mle mlt kn args + extract_cst_app env sg mle mlt kn args | Construct (cp,_) -> - extract_cons_app env mle mlt cp args + extract_cons_app env sg mle mlt cp args | Proj (p, c) -> - let term = Retyping.expand_projection env (Evd.from_env env) p (EConstr.of_constr c) [] in - let term = EConstr.Unsafe.to_constr term in - extract_term env mle mlt term args + let term = Retyping.expand_projection env (Evd.from_env env) p c [] in + extract_term env sg mle mlt term args | Rel n -> (* As soon as the expected [mlt] for the head is known, *) (* we unify it with an fresh copy of the stored type of [Rel n]. *) let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n) - in extract_app env mle mlt extract_rel args + in extract_app env sg mle mlt extract_rel args | Case ({ci_ind=ip},_,c0,br) -> - extract_app env mle mlt (extract_case env mle (ip,c0,br)) args + extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args | Fix ((_,i),recd) -> - extract_app env mle mlt (extract_fix env mle i recd) args + extract_app env sg mle mlt (extract_fix env sg mle i recd) args | CoFix (i,recd) -> - extract_app env mle mlt (extract_fix env mle i recd) args - | Cast (c,_,_) -> extract_term env mle mlt c args - | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false + extract_app env sg mle mlt (extract_fix env sg mle i recd) args + | Cast (c,_,_) -> extract_term env sg mle mlt c args + | Evar _ | Meta _ -> MLaxiom + | Var v -> + (* Only during Show Extraction *) + let open Context.Named.Declaration in + let ty = match EConstr.lookup_named v env with + | LocalAssum (_,ty) -> ty + | LocalDef (_,_,ty) -> ty + in + let vty = extract_type env sg [] 0 ty [] in + let extract_var mlt = put_magic (mlt,vty) (MLglob (VarRef v)) in + extract_app env sg mle mlt extract_var args + | Ind _ | Prod _ | Sort _ -> assert false (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) -and extract_maybe_term env mle mlt c = - try check_default env (type_of env c); - extract_term env mle mlt c [] +and extract_maybe_term env sg mle mlt c = + try check_default env sg (type_of env sg c); + extract_term env sg mle mlt c [] with NotDefault d -> put_magic (mlt, Tdummy d) (MLdummy d) @@ -644,28 +699,28 @@ and extract_maybe_term env mle mlt c = This gives us the expected type of the head. Then we use the [mk_head] to produce the ML head from this type. *) -and extract_app env mle mlt mk_head args = +and extract_app env sg mle mlt mk_head args = let metas = List.map new_meta args in let type_head = type_recomp (metas, mlt) in - let mlargs = List.map2 (extract_maybe_term env mle) metas args in + let mlargs = List.map2 (extract_maybe_term env sg mle) metas args in mlapp (mk_head type_head) mlargs (*s Auxiliary function used to extract arguments of constant or constructor. *) -and make_mlargs env e s args typs = +and make_mlargs env sg e s args typs = let rec f = function | [], [], _ -> [] - | a::la, t::lt, [] -> extract_maybe_term env e t a :: (f (la,lt,[])) - | a::la, t::lt, Keep::s -> extract_maybe_term env e t a :: (f (la,lt,s)) + | a::la, t::lt, [] -> extract_maybe_term env sg e t a :: (f (la,lt,[])) + | a::la, t::lt, Keep::s -> extract_maybe_term env sg e t a :: (f (la,lt,s)) | _::la, _::lt, _::s -> f (la,lt,s) | _ -> assert false in f (args,typs,s) (*s Extraction of a constant applied to arguments. *) -and extract_cst_app env mle mlt kn args = +and extract_cst_app env sg mle mlt kn args = (* First, the [ml_schema] of the constant, in expanded version. *) - let nb,t = record_constant_type env kn None in + let nb,t = record_constant_type env sg kn None in let schema = nb, expand env t in (* Can we instantiate types variables for this constant ? *) (* In Ocaml, inside the definition of this constant, the answer is no. *) @@ -691,7 +746,7 @@ and extract_cst_app env mle mlt kn args = let ls = List.length s in let la = List.length args in (* The ml arguments, already expunged from known logical ones *) - let mla = make_mlargs env mle s args metas in + let mla = make_mlargs env sg mle s args metas in let mla = if magic1 || lang () != Ocaml then mla else @@ -736,7 +791,7 @@ and extract_cst_app env mle mlt kn args = they are fixed, and thus are not used for the computation. \end{itemize} *) -and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = +and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args = (* First, we build the type of the constructor, stored in small pieces. *) let mi = extract_ind env kn in let params_nb = mi.ind_nparams in @@ -777,7 +832,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = put_magic_if magic2 (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la)) else - let mla = make_mlargs env mle s args' metas in + let mla = make_mlargs env sg mle s args' metas in if Int.equal la (ls + params_nb) then put_magic_if (magic2 && not magic1) (head mla) else (* [ params_nb <= la <= ls + params_nb ] *) @@ -788,7 +843,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = (*S Extraction of a case. *) -and extract_case env mle ((kn,i) as ip,c,br) mlt = +and extract_case env sg mle ((kn,i) as ip,c,br) mlt = (* [br]: bodies of each branch (in functional form) *) (* [ni]: number of arguments without parameters in each branch *) let ni = constructors_nrealargs_env env ip in @@ -799,9 +854,9 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = MLexn "absurd case" end else (* [c] has an inductive type, and is not a type scheme type. *) - let t = type_of env c in + let t = type_of env sg c in (* The only non-informative case: [c] is of sort [Prop] *) - if (sort_of env t) == InProp then + if (sort_of env sg t) == InProp then begin add_recursors env kn; (* May have passed unseen if logical ... *) (* Logical singleton case: *) @@ -809,7 +864,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = assert (Int.equal br_size 1); let s = iterate (fun l -> Kill Kprop :: l) ni.(0) [] in let mlt = iterate (fun t -> Tarr (Tdummy Kprop, t)) ni.(0) mlt in - let e = extract_maybe_term env mle mlt br.(0) in + let e = extract_maybe_term env sg mle mlt br.(0) in snd (case_expunge s e) end else @@ -818,7 +873,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = let metas = Array.init (List.length oi.ip_vars) new_meta in (* The extraction of the head. *) let type_head = Tglob (IndRef ip, Array.to_list metas) in - let a = extract_term env mle type_head c [] in + let a = extract_term env sg mle type_head c [] in (* The extraction of each branch. *) let extract_branch i = let r = ConstructRef (ip,i+1) in @@ -829,7 +884,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = let s = List.map (type2sign env) oi.ip_types.(i) in let s = sign_with_implicits r s mi.ind_nparams in (* Extraction of the branch (in functional form). *) - let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in + let e = extract_maybe_term env sg mle (type_recomp (l,mlt)) br.(i) in (* We suppress dummy arguments according to signature. *) let ids,e = case_expunge s e in (List.rev ids, Pusual r, e) @@ -851,12 +906,12 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = (*s Extraction of a (co)-fixpoint. *) -and extract_fix env mle i (fi,ti,ci as recd) mlt = +and extract_fix env sg mle i (fi,ti,ci as recd) mlt = let env = push_rec_types recd env in let metas = Array.map new_meta fi in metas.(i) <- mlt; let mle = Array.fold_left Mlenv.push_type mle metas in - let ei = Array.map2 (extract_maybe_term env mle) metas ci in + let ei = Array.map2 (extract_maybe_term env sg mle) metas ci in MLfix (i, Array.map id_of_name fi, ei) (*S ML declarations. *) @@ -864,34 +919,34 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt = (* [decomp_lams_eta env c t] finds the number [n] of products in the type [t], and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *) -let decomp_lams_eta_n n m env c t = - let rels = fst (splay_prod_n env none n (EConstr.of_constr t)) in - let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,EConstr.Unsafe.to_constr c)) rels in - let rels',c = decompose_lam c in +let decomp_lams_eta_n n m env sg c t = + let rels = fst (splay_prod_n env sg n t) in + let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in + let rels',c = EConstr.decompose_lam sg c in let d = n - m in (* we'd better keep rels' as long as possible. *) let rels = (List.firstn d rels) @ rels' in - let eta_args = List.rev_map mkRel (List.interval 1 d) in - rels, applistc (lift d c) eta_args + let eta_args = List.rev_map EConstr.mkRel (List.interval 1 d) in + rels, applistc (EConstr.Vars.lift d c) eta_args (* Let's try to identify some situation where extracted code will allow generalisation of type variables *) -let rec gentypvar_ok c = match Constr.kind c with +let rec gentypvar_ok sg c = match EConstr.kind sg c with | Lambda _ | Const _ -> true | App (c,v) -> (* if all arguments are variables, these variables will disappear after extraction (see [empty_s] below) *) - Array.for_all isRel v && gentypvar_ok c - | Cast (c,_,_) -> gentypvar_ok c + Array.for_all (EConstr.isRel sg) v && gentypvar_ok sg c + | Cast (c,_,_) -> gentypvar_ok sg c | _ -> false (*s From a constant to a ML declaration. *) -let extract_std_constant env kn body typ = +let extract_std_constant env sg kn body typ = reset_meta_count (); (* The short type [t] (i.e. possibly with abbreviations). *) - let t = snd (record_constant_type env kn (Some typ)) in + let t = snd (record_constant_type env sg kn (Some typ)) in (* The real type [t']: without head products, expanded, *) (* and with [Tvar] translated to [Tvar'] (not instantiable). *) let l,t' = type_decomp (expand env (var2var' t)) in @@ -906,14 +961,14 @@ let extract_std_constant env kn body typ = break user's clever let-ins and partial applications). *) let rels, c = let n = List.length s - and m = nb_lam Evd.empty (EConstr.of_constr body) (** FIXME *) in - if n <= m then decompose_lam_n n body + and m = nb_lam sg body in + if n <= m then decompose_lam_n sg n body else let s,s' = List.chop m s in if List.for_all ((==) Keep) s' && (lang () == Haskell || sign_kind s != UnsafeLogicalSig) - then decompose_lam_n m body - else decomp_lams_eta_n n m env body typ + then decompose_lam_n sg m body + else decomp_lams_eta_n n m env sg body typ in (* Should we do one eta-expansion to avoid non-generalizable '_a ? *) let rels, c = @@ -921,9 +976,9 @@ let extract_std_constant env kn body typ = let s,s' = List.chop n s in let k = sign_kind s in let empty_s = (k == EmptySig || k == SafeLogicalSig) in - if lang () == Ocaml && empty_s && not (gentypvar_ok c) + if lang () == Ocaml && empty_s && not (gentypvar_ok sg c) && not (List.is_empty s') && not (Int.equal (type_maxvar t) 0) - then decomp_lams_eta_n (n+1) n env body typ + then decomp_lams_eta_n (n+1) n env sg body typ else rels,c in let n = List.length rels in @@ -937,16 +992,16 @@ let extract_std_constant env kn body typ = (* The according Coq environment. *) let env = push_rels_assum rels env in (* The real extraction: *) - let e = extract_term env mle t' c [] in + let e = extract_term env sg mle t' c [] in (* Expunging term and type from dummy lambdas. *) let trm = term_expunge s (ids,e) in trm, type_expunge_from_sign env s t (* Extracts the type of an axiom, honors the Extraction Implicit declaration. *) -let extract_axiom env kn typ = +let extract_axiom env sg kn typ = reset_meta_count (); (* The short type [t] (i.e. possibly with abbreviations). *) - let t = snd (record_constant_type env kn (Some typ)) in + let t = snd (record_constant_type env sg kn (Some typ)) in (* The real type [t']: without head products, expanded, *) (* and with [Tvar] translated to [Tvar'] (not instantiable). *) let l,_ = type_decomp (expand env (var2var' t)) in @@ -955,18 +1010,19 @@ let extract_axiom env kn typ = let s = sign_with_implicits (ConstRef kn) s 0 in type_expunge_from_sign env s t -let extract_fixpoint env vkn (fi,ti,ci) = +let extract_fixpoint env sg vkn (fi,ti,ci) = let n = Array.length vkn in let types = Array.make n (Tdummy Kprop) and terms = Array.make n (MLdummy Kprop) in let kns = Array.to_list vkn in current_fixpoints := kns; (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *) - let sub = List.rev_map mkConst kns in + let sub = List.rev_map EConstr.mkConst kns in for i = 0 to n-1 do - if sort_of env ti.(i) != InProp then + if sort_of env sg ti.(i) != InProp then try - let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in + let e,t = extract_std_constant env sg vkn.(i) + (EConstr.Vars.substl sub ci.(i)) ti.(i) in terms.(i) <- e; types.(i) <- t; with SingletonInductiveBecomesProp id -> @@ -976,32 +1032,33 @@ let extract_fixpoint env vkn (fi,ti,ci) = Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) let extract_constant env kn cb = + let sg = Evd.from_env env in let r = ConstRef kn in - let typ = cb.const_type in + let typ = EConstr.of_constr cb.const_type in let warn_info () = if not (is_custom r) then add_info_axiom r in let warn_log () = if not (constant_has_body cb) then add_log_axiom r in let mk_typ_ax () = - let n = type_scheme_nb_args env typ in + let n = type_scheme_nb_args env sg typ in let ids = iterate (fun l -> anonymous_name::l) n [] in Dtype (r, ids, Taxiom) in let mk_typ c = - let s,vl = type_sign_vl env typ in + let s,vl = type_sign_vl env sg typ in let db = db_from_sign s in - let t = extract_type_scheme env db c (List.length s) + let t = extract_type_scheme env sg db c (List.length s) in Dtype (r, vl, t) in let mk_ax () = - let t = extract_axiom env kn typ in + let t = extract_axiom env sg kn typ in Dterm (r, MLaxiom, t) in let mk_def c = - let e,t = extract_std_constant env kn c typ in + let e,t = extract_std_constant env sg kn c typ in Dterm (r,e,t) in try - match flag_of_type env typ with + match flag_of_type env sg typ with | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype) | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop) | (Info,TypeScheme) -> @@ -1009,73 +1066,72 @@ let extract_constant env kn cb = | Undef _ -> warn_info (); mk_typ_ax () | Def c -> (match cb.const_proj with - | None -> mk_typ (Mod_subst.force_constr c) - | Some pb -> mk_typ pb.proj_body) + | None -> mk_typ (get_body c) + | Some pb -> mk_typ (EConstr.of_constr pb.proj_body)) | OpaqueDef c -> add_opaque r; - if access_opaque () then - mk_typ (Opaqueproof.force_proof (Environ.opaque_tables env) c) + if access_opaque () then mk_typ (get_opaque env c) else mk_typ_ax ()) | (Info,Default) -> (match cb.const_body with | Undef _ -> warn_info (); mk_ax () | Def c -> (match cb.const_proj with - | None -> mk_def (Mod_subst.force_constr c) - | Some pb -> mk_def pb.proj_body) + | None -> mk_def (get_body c) + | Some pb -> mk_def (EConstr.of_constr pb.proj_body)) | OpaqueDef c -> add_opaque r; - if access_opaque () then - mk_def (Opaqueproof.force_proof (Environ.opaque_tables env) c) + if access_opaque () then mk_def (get_opaque env c) else mk_ax ()) with SingletonInductiveBecomesProp id -> error_singleton_become_prop id (Some (ConstRef kn)) let extract_constant_spec env kn cb = + let sg = Evd.from_env env in let r = ConstRef kn in - let typ = cb.const_type in + let typ = EConstr.of_constr cb.const_type in try - match flag_of_type env typ with + match flag_of_type env sg typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) | (Logic, Default) -> Sval (r, Tdummy Kprop) | (Info, TypeScheme) -> - let s,vl = type_sign_vl env typ in + let s,vl = type_sign_vl env sg typ in (match cb.const_body with | Undef _ | OpaqueDef _ -> Stype (r, vl, None) | Def body -> let db = db_from_sign s in - let body = Mod_subst.force_constr body in - let t = extract_type_scheme env db body (List.length s) - in Stype (r, vl, Some t)) + let body = get_body body in + let t = extract_type_scheme env sg db body (List.length s) + in Stype (r, vl, Some t)) | (Info, Default) -> - let t = snd (record_constant_type env kn (Some typ)) in - Sval (r, type_expunge env t) + let t = snd (record_constant_type env sg kn (Some typ)) in + Sval (r, type_expunge env t) with SingletonInductiveBecomesProp id -> error_singleton_become_prop id (Some (ConstRef kn)) -let extract_with_type env c = +let extract_with_type env sg c = try - let typ = type_of env c in - match flag_of_type env typ with + let typ = type_of env sg c in + match flag_of_type env sg typ with | (Info, TypeScheme) -> - let s,vl = type_sign_vl env typ in - let db = db_from_sign s in - let t = extract_type_scheme env db c (List.length s) in - Some (vl, t) + let s,vl = type_sign_vl env sg typ in + let db = db_from_sign s in + let t = extract_type_scheme env sg db c (List.length s) in + Some (vl, t) | _ -> None with SingletonInductiveBecomesProp id -> error_singleton_become_prop id None -let extract_constr env c = +let extract_constr env sg c = reset_meta_count (); try - let typ = type_of env c in - match flag_of_type env typ with + let typ = type_of env sg c in + match flag_of_type env sg typ with | (_,TypeScheme) -> MLdummy Ktype, Tdummy Ktype | (Logic,_) -> MLdummy Kprop, Tdummy Kprop | (Info,Default) -> - let mlt = extract_type env [] 1 typ [] in - extract_term env Mlenv.empty mlt c [], mlt + let mlt = extract_type env sg [] 1 typ [] in + extract_term env sg Mlenv.empty mlt c [], mlt with SingletonInductiveBecomesProp id -> error_singleton_become_prop id None diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index a0f2885a4..d27c79cb6 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -11,9 +11,9 @@ (*s Extraction from Coq terms to Miniml. *) open Names -open Constr open Declarations open Environ +open Evd open Miniml val extract_constant : env -> Constant.t -> constant_body -> ml_decl @@ -22,16 +22,18 @@ val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec (** For extracting "module ... with ..." declaration *) -val extract_with_type : env -> constr -> ( Id.t list * ml_type ) option +val extract_with_type : + env -> evar_map -> EConstr.t -> ( Id.t list * ml_type ) option val extract_fixpoint : - env -> Constant.t array -> (constr, types) prec_declaration -> ml_decl + env -> evar_map -> Constant.t array -> + (EConstr.t, EConstr.types) Constr.prec_declaration -> ml_decl val extract_inductive : env -> MutInd.t -> ml_ind -(** For extraction compute *) +(** For Extraction Compute and Show Extraction *) -val extract_constr : env -> constr -> ml_ast * ml_type +val extract_constr : env -> evar_map -> EConstr.t -> ml_ast * ml_type (*s Is a [ml_decl] or a [ml_spec] logical ? *) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 468f2fe8c..93909f3e6 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -160,3 +160,9 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF mlname(id) "[" mlname_list(idl) "]" string_opt(o) ] -> [ extract_inductive x id idl o ] END +(* Show the extraction of the current proof *) + +VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY +| [ "Show" "Extraction" ] + -> [ show_extraction () ] +END diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 0bcda69d4..6c421491f 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -38,14 +38,13 @@ module Refset' = Refset_env let occur_kn_in_ref kn = function | IndRef (kn',_) | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' - | ConstRef _ -> false - | VarRef _ -> assert false + | ConstRef _ | VarRef _ -> false let repr_of_r = function | ConstRef kn -> Constant.repr3 kn | IndRef (kn,_) | ConstructRef ((kn,_),_) -> MutInd.repr3 kn - | VarRef _ -> assert false + | VarRef v -> KerName.repr (Lib.make_kn v) let modpath_of_r r = let mp,_,_ = repr_of_r r in mp @@ -279,7 +278,7 @@ let safe_basename_of_global r = | ConstructRef ((kn,i),j) -> (try (unsafe_lookup_ind kn).ind_packets.(i).ip_consnames.(j-1) with Not_found -> last_chance r) - | VarRef _ -> assert false + | VarRef v -> v let string_of_global r = try string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty r) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 6e38b4641..e0368153e 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1922,7 +1922,7 @@ let build_morphism_signature env sigma m = in let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in let evd = solve_constraints env !evd in - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m); Evd.evar_universe_context evd, m diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 543a37ff8..f066ea462 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -21,6 +21,7 @@ Require Import List. Require Import Bool. Require Import OrderedRing. Require Import Refl. +Require Coq.micromega.Tauto. Set Implicit Arguments. @@ -796,7 +797,7 @@ Definition xnormalise (t:Formula C) : list (NFormula) := | OpLe => (psub lhs rhs ,Strict) :: nil end. -Require Import Coq.micromega.Tauto. +Import Coq.micromega.Tauto. Definition cnf_normalise (t:Formula C) : cnf (NFormula) := List.map (fun x => x::nil) (xnormalise t). diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 85e2a5b23..c5a09d677 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -30,6 +30,7 @@ Require Export Ncring_initial. Require Export Ncring_tac. Require Export Integral_domain. Require Import DiscrR. +Require Import ZArith. Declare ML Module "nsatz_plugin". @@ -56,9 +57,8 @@ simpl. simpl; cring. Qed. (* adpatation du code de Benjamin aux setoides *) -Require Import ZArith. -Require Export Ring_polynom. -Require Export InitialRing. +Export Ring_polynom. +Export InitialRing. Definition PolZ := Pol Z. Definition PEZ := PExpr Z. diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 0f5417e7d..ad3afafd8 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -7,15 +7,14 @@ *************************************************************************) open Names -open Constr let module_refl_name = "ReflOmegaCore" let module_refl_path = ["Coq"; "romega"; module_refl_name] type result = | Kvar of string - | Kapp of string * constr list - | Kimp of constr * constr + | Kapp of string * EConstr.t list + | Kimp of EConstr.t * EConstr.t | Kufo let meaningful_submodule = [ "Z"; "N"; "Pos" ] @@ -30,9 +29,10 @@ let string_of_global r = in prefix^(Names.Id.to_string (Nametab.basename_of_global r)) -let destructurate t = - let c, args = decompose_app t in - match Constr.kind c, args with +let destructurate sigma t = + let c, args = EConstr.decompose_app sigma t in + let open Constr in + match EConstr.kind sigma c, args with | Const (sp,_), args -> Kapp (string_of_global (Globnames.ConstRef sp), args) | Construct (csp,_) , args -> @@ -45,10 +45,11 @@ let destructurate t = exception DestConstApp -let dest_const_apply t = - let f,args = decompose_app t in +let dest_const_apply sigma t = + let open Constr in + let f,args = EConstr.decompose_app sigma t in let ref = - match Constr.kind f with + match EConstr.kind sigma f with | Const (sp,_) -> Globnames.ConstRef sp | Construct (csp,_) -> Globnames.ConstructRef csp | Ind (isp,_) -> Globnames.IndRef isp @@ -66,10 +67,22 @@ let coq_modules = let bin_module = [["Coq";"Numbers";"BinNums"]] let z_module = [["Coq";"ZArith";"BinInt"]] -let init_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x -let constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" coq_modules x -let z_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" z_module x -let bin_constant x = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules "Omega" bin_module x +let init_constant x = + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "Omega" Coqlib.init_modules x +let constant x = + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "Omega" coq_modules x +let z_constant x = + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "Omega" z_module x +let bin_constant x = + EConstr.of_constr @@ + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "Omega" bin_module x (* Logic *) let coq_refl_equal = lazy(init_constant "eq_refl") @@ -130,62 +143,64 @@ let coq_O = lazy(init_constant "O") let rec mk_nat = function | 0 -> Lazy.force coq_O - | n -> mkApp (Lazy.force coq_S, [| mk_nat (n-1) |]) + | n -> EConstr.mkApp (Lazy.force coq_S, [| mk_nat (n-1) |]) (* Lists *) -let mkListConst c = - let r = +let mkListConst c = + let r = Coqlib.coq_reference "" ["Init";"Datatypes"] c - in - let inst = - if Global.is_polymorphic r then fun u -> Univ.Instance.of_array [|u|] - else fun _ -> Univ.Instance.empty in - fun u -> mkConstructU (Globnames.destConstructRef r, inst u) + let inst = + if Global.is_polymorphic r then + fun u -> EConstr.EInstance.make (Univ.Instance.of_array [|u|]) + else + fun _ -> EConstr.EInstance.empty + in + fun u -> EConstr.mkConstructU (Globnames.destConstructRef r, inst u) -let coq_cons univ typ = mkApp (mkListConst "cons" univ, [|typ|]) -let coq_nil univ typ = mkApp (mkListConst "nil" univ, [|typ|]) +let coq_cons univ typ = EConstr.mkApp (mkListConst "cons" univ, [|typ|]) +let coq_nil univ typ = EConstr.mkApp (mkListConst "nil" univ, [|typ|]) let mk_list univ typ l = let rec loop = function | [] -> coq_nil univ typ | (step :: l) -> - mkApp (coq_cons univ typ, [| step; loop l |]) in + EConstr.mkApp (coq_cons univ typ, [| step; loop l |]) in loop l -let mk_plist = +let mk_plist = let type1lev = Universes.new_univ_level () in - fun l -> mk_list type1lev mkProp l + fun l -> mk_list type1lev EConstr.mkProp l let mk_list = mk_list Univ.Level.set type parse_term = - | Tplus of constr * constr - | Tmult of constr * constr - | Tminus of constr * constr - | Topp of constr - | Tsucc of constr + | Tplus of EConstr.t * EConstr.t + | Tmult of EConstr.t * EConstr.t + | Tminus of EConstr.t * EConstr.t + | Topp of EConstr.t + | Tsucc of EConstr.t | Tnum of Bigint.bigint | Tother type parse_rel = - | Req of constr * constr - | Rne of constr * constr - | Rlt of constr * constr - | Rle of constr * constr - | Rgt of constr * constr - | Rge of constr * constr + | Req of EConstr.t * EConstr.t + | Rne of EConstr.t * EConstr.t + | Rlt of EConstr.t * EConstr.t + | Rle of EConstr.t * EConstr.t + | Rgt of EConstr.t * EConstr.t + | Rge of EConstr.t * EConstr.t | Rtrue | Rfalse - | Rnot of constr - | Ror of constr * constr - | Rand of constr * constr - | Rimp of constr * constr - | Riff of constr * constr + | Rnot of EConstr.t + | Ror of EConstr.t * EConstr.t + | Rand of EConstr.t * EConstr.t + | Rimp of EConstr.t * EConstr.t + | Riff of EConstr.t * EConstr.t | Rother -let parse_logic_rel c = match destructurate c with +let parse_logic_rel sigma c = match destructurate sigma c with | Kapp("True",[]) -> Rtrue | Kapp("False",[]) -> Rfalse | Kapp("not",[t]) -> Rnot t @@ -211,29 +226,29 @@ let rec mk_positive n = if Bigint.equal n Bigint.one then Lazy.force coq_xH else let (q,r) = Bigint.euclid n Bigint.two in - mkApp + EConstr.mkApp ((if Bigint.equal r Bigint.zero then Lazy.force coq_xO else Lazy.force coq_xI), [| mk_positive q |]) let mk_N = function | 0 -> Lazy.force coq_N0 - | n -> mkApp (Lazy.force coq_Npos, + | n -> EConstr.mkApp (Lazy.force coq_Npos, [| mk_positive (Bigint.of_int n) |]) module type Int = sig - val typ : constr Lazy.t - val is_int_typ : Proofview.Goal.t -> constr -> bool - val plus : constr Lazy.t - val mult : constr Lazy.t - val opp : constr Lazy.t - val minus : constr Lazy.t - - val mk : Bigint.bigint -> constr - val parse_term : constr -> parse_term - val parse_rel : Proofview.Goal.t -> constr -> parse_rel + val typ : EConstr.t Lazy.t + val is_int_typ : Proofview.Goal.t -> EConstr.t -> bool + val plus : EConstr.t Lazy.t + val mult : EConstr.t Lazy.t + val opp : EConstr.t Lazy.t + val minus : EConstr.t Lazy.t + + val mk : Bigint.bigint -> EConstr.t + val parse_term : Evd.evar_map -> EConstr.t -> parse_term + val parse_rel : Proofview.Goal.t -> EConstr.t -> parse_rel (* check whether t is built only with numbers and + * - *) - val get_scalar : constr -> Bigint.bigint option + val get_scalar : Evd.evar_map -> EConstr.t -> Bigint.bigint option end module Z : Int = struct @@ -244,9 +259,9 @@ let mult = lazy (z_constant "Z.mul") let opp = lazy (z_constant "Z.opp") let minus = lazy (z_constant "Z.sub") -let recognize_pos t = +let recognize_pos sigma t = let rec loop t = - let f,l = dest_const_apply t in + let f,l = dest_const_apply sigma t in match Id.to_string f,l with | "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t)) | "xO",[t] -> Bigint.mult Bigint.two (loop t) @@ -255,12 +270,12 @@ let recognize_pos t = in try Some (loop t) with DestConstApp -> None -let recognize_Z t = +let recognize_Z sigma t = try - let f,l = dest_const_apply t in + let f,l = dest_const_apply sigma t in match Id.to_string f,l with - | "Zpos",[t] -> recognize_pos t - | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos t) + | "Zpos",[t] -> recognize_pos sigma t + | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos sigma t) | "Z0",[] -> Some Bigint.zero | _ -> None with DestConstApp -> None @@ -268,14 +283,14 @@ let recognize_Z t = let mk_Z n = if Bigint.equal n Bigint.zero then Lazy.force coq_Z0 else if Bigint.is_strictly_pos n then - mkApp (Lazy.force coq_Zpos, [| mk_positive n |]) + EConstr.mkApp (Lazy.force coq_Zpos, [| mk_positive n |]) else - mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |]) + EConstr.mkApp (Lazy.force coq_Zneg, [| mk_positive (Bigint.neg n) |]) let mk = mk_Z -let parse_term t = - match destructurate t with +let parse_term sigma t = + match destructurate sigma t with | Kapp("Z.add",[t1;t2]) -> Tplus (t1,t2) | Kapp("Z.sub",[t1;t2]) -> Tminus (t1,t2) | Kapp("Z.mul",[t1;t2]) -> Tmult (t1,t2) @@ -283,35 +298,35 @@ let parse_term t = | Kapp("Z.succ",[t]) -> Tsucc t | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one)) | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> - (match recognize_Z t with Some t -> Tnum t | None -> Tother) + (match recognize_Z sigma t with Some t -> Tnum t | None -> Tother) | _ -> Tother let is_int_typ gl t = - Tacmach.New.pf_apply Reductionops.is_conv gl - (EConstr.of_constr t) (EConstr.of_constr (Lazy.force coq_Z)) + Tacmach.New.pf_apply Reductionops.is_conv gl t (Lazy.force coq_Z) let parse_rel gl t = - match destructurate t with + let sigma = Proofview.Goal.sigma gl in + match destructurate sigma t with | Kapp("eq",[typ;t1;t2]) when is_int_typ gl typ -> Req (t1,t2) | Kapp("Zne",[t1;t2]) -> Rne (t1,t2) | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2) | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2) | Kapp("Z.ge",[t1;t2]) -> Rge (t1,t2) | Kapp("Z.gt",[t1;t2]) -> Rgt (t1,t2) - | _ -> parse_logic_rel t + | _ -> parse_logic_rel sigma t -let rec get_scalar t = - match destructurate t with +let rec get_scalar sigma t = + match destructurate sigma t with | Kapp("Z.add", [t1;t2]) -> - Option.lift2 Bigint.add (get_scalar t1) (get_scalar t2) + Option.lift2 Bigint.add (get_scalar sigma t1) (get_scalar sigma t2) | Kapp ("Z.sub",[t1;t2]) -> - Option.lift2 Bigint.sub (get_scalar t1) (get_scalar t2) + Option.lift2 Bigint.sub (get_scalar sigma t1) (get_scalar sigma t2) | Kapp ("Z.mul",[t1;t2]) -> - Option.lift2 Bigint.mult (get_scalar t1) (get_scalar t2) - | Kapp("Z.opp", [t]) -> Option.map Bigint.neg (get_scalar t) - | Kapp("Z.succ", [t]) -> Option.map Bigint.add_1 (get_scalar t) - | Kapp("Z.pred", [t]) -> Option.map Bigint.sub_1 (get_scalar t) - | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> recognize_Z t + Option.lift2 Bigint.mult (get_scalar sigma t1) (get_scalar sigma t2) + | Kapp("Z.opp", [t]) -> Option.map Bigint.neg (get_scalar sigma t) + | Kapp("Z.succ", [t]) -> Option.map Bigint.add_1 (get_scalar sigma t) + | Kapp("Z.pred", [t]) -> Option.map Bigint.sub_1 (get_scalar sigma t) + | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> recognize_Z sigma t | _ -> None end diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index ecddc55de..64668df00 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -8,117 +8,116 @@ (** Coq objects used in romega *) -open Constr (* from Logic *) -val coq_refl_equal : constr lazy_t -val coq_and : constr lazy_t -val coq_not : constr lazy_t -val coq_or : constr lazy_t -val coq_True : constr lazy_t -val coq_False : constr lazy_t -val coq_I : constr lazy_t +val coq_refl_equal : EConstr.t lazy_t +val coq_and : EConstr.t lazy_t +val coq_not : EConstr.t lazy_t +val coq_or : EConstr.t lazy_t +val coq_True : EConstr.t lazy_t +val coq_False : EConstr.t lazy_t +val coq_I : EConstr.t lazy_t (* from ReflOmegaCore/ZOmega *) -val coq_t_int : constr lazy_t -val coq_t_plus : constr lazy_t -val coq_t_mult : constr lazy_t -val coq_t_opp : constr lazy_t -val coq_t_minus : constr lazy_t -val coq_t_var : constr lazy_t - -val coq_proposition : constr lazy_t -val coq_p_eq : constr lazy_t -val coq_p_leq : constr lazy_t -val coq_p_geq : constr lazy_t -val coq_p_lt : constr lazy_t -val coq_p_gt : constr lazy_t -val coq_p_neq : constr lazy_t -val coq_p_true : constr lazy_t -val coq_p_false : constr lazy_t -val coq_p_not : constr lazy_t -val coq_p_or : constr lazy_t -val coq_p_and : constr lazy_t -val coq_p_imp : constr lazy_t -val coq_p_prop : constr lazy_t - -val coq_s_bad_constant : constr lazy_t -val coq_s_divide : constr lazy_t -val coq_s_not_exact_divide : constr lazy_t -val coq_s_sum : constr lazy_t -val coq_s_merge_eq : constr lazy_t -val coq_s_split_ineq : constr lazy_t - -val coq_direction : constr lazy_t -val coq_d_left : constr lazy_t -val coq_d_right : constr lazy_t - -val coq_e_split : constr lazy_t -val coq_e_extract : constr lazy_t -val coq_e_solve : constr lazy_t - -val coq_interp_sequent : constr lazy_t -val coq_do_omega : constr lazy_t - -val mk_nat : int -> constr -val mk_N : int -> constr +val coq_t_int : EConstr.t lazy_t +val coq_t_plus : EConstr.t lazy_t +val coq_t_mult : EConstr.t lazy_t +val coq_t_opp : EConstr.t lazy_t +val coq_t_minus : EConstr.t lazy_t +val coq_t_var : EConstr.t lazy_t + +val coq_proposition : EConstr.t lazy_t +val coq_p_eq : EConstr.t lazy_t +val coq_p_leq : EConstr.t lazy_t +val coq_p_geq : EConstr.t lazy_t +val coq_p_lt : EConstr.t lazy_t +val coq_p_gt : EConstr.t lazy_t +val coq_p_neq : EConstr.t lazy_t +val coq_p_true : EConstr.t lazy_t +val coq_p_false : EConstr.t lazy_t +val coq_p_not : EConstr.t lazy_t +val coq_p_or : EConstr.t lazy_t +val coq_p_and : EConstr.t lazy_t +val coq_p_imp : EConstr.t lazy_t +val coq_p_prop : EConstr.t lazy_t + +val coq_s_bad_constant : EConstr.t lazy_t +val coq_s_divide : EConstr.t lazy_t +val coq_s_not_exact_divide : EConstr.t lazy_t +val coq_s_sum : EConstr.t lazy_t +val coq_s_merge_eq : EConstr.t lazy_t +val coq_s_split_ineq : EConstr.t lazy_t + +val coq_direction : EConstr.t lazy_t +val coq_d_left : EConstr.t lazy_t +val coq_d_right : EConstr.t lazy_t + +val coq_e_split : EConstr.t lazy_t +val coq_e_extract : EConstr.t lazy_t +val coq_e_solve : EConstr.t lazy_t + +val coq_interp_sequent : EConstr.t lazy_t +val coq_do_omega : EConstr.t lazy_t + +val mk_nat : int -> EConstr.t +val mk_N : int -> EConstr.t (** Precondition: the type of the list is in Set *) -val mk_list : constr -> constr list -> constr -val mk_plist : types list -> types +val mk_list : EConstr.t -> EConstr.t list -> EConstr.t +val mk_plist : EConstr.types list -> EConstr.types (** Analyzing a coq term *) (* The generic result shape of the analysis of a term. One-level depth, except when a number is found *) type parse_term = - Tplus of constr * constr - | Tmult of constr * constr - | Tminus of constr * constr - | Topp of constr - | Tsucc of constr + Tplus of EConstr.t * EConstr.t + | Tmult of EConstr.t * EConstr.t + | Tminus of EConstr.t * EConstr.t + | Topp of EConstr.t + | Tsucc of EConstr.t | Tnum of Bigint.bigint | Tother (* The generic result shape of the analysis of a relation. One-level depth. *) type parse_rel = - Req of constr * constr - | Rne of constr * constr - | Rlt of constr * constr - | Rle of constr * constr - | Rgt of constr * constr - | Rge of constr * constr + Req of EConstr.t * EConstr.t + | Rne of EConstr.t * EConstr.t + | Rlt of EConstr.t * EConstr.t + | Rle of EConstr.t * EConstr.t + | Rgt of EConstr.t * EConstr.t + | Rge of EConstr.t * EConstr.t | Rtrue | Rfalse - | Rnot of constr - | Ror of constr * constr - | Rand of constr * constr - | Rimp of constr * constr - | Riff of constr * constr + | Rnot of EConstr.t + | Ror of EConstr.t * EConstr.t + | Rand of EConstr.t * EConstr.t + | Rimp of EConstr.t * EConstr.t + | Riff of EConstr.t * EConstr.t | Rother (* A module factorizing what we should now about the number representation *) module type Int = sig (* the coq type of the numbers *) - val typ : constr Lazy.t + val typ : EConstr.t Lazy.t (* Is a constr expands to the type of these numbers *) - val is_int_typ : Proofview.Goal.t -> constr -> bool + val is_int_typ : Proofview.Goal.t -> EConstr.t -> bool (* the operations on the numbers *) - val plus : constr Lazy.t - val mult : constr Lazy.t - val opp : constr Lazy.t - val minus : constr Lazy.t + val plus : EConstr.t Lazy.t + val mult : EConstr.t Lazy.t + val opp : EConstr.t Lazy.t + val minus : EConstr.t Lazy.t (* building a coq number *) - val mk : Bigint.bigint -> constr + val mk : Bigint.bigint -> EConstr.t (* parsing a term (one level, except if a number is found) *) - val parse_term : constr -> parse_term + val parse_term : Evd.evar_map -> EConstr.t -> parse_term (* parsing a relation expression, including = < <= >= > *) - val parse_rel : Proofview.Goal.t -> constr -> parse_rel + val parse_rel : Proofview.Goal.t -> EConstr.t -> parse_rel (* Is a particular term only made of numbers and + * - ? *) - val get_scalar : constr -> Bigint.bigint option + val get_scalar : Evd.evar_map -> EConstr.t -> Bigint.bigint option end (* Currently, we only use Z numbers *) diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 54ff44fbd..d18249784 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -8,7 +8,6 @@ open Pp open Util -open Constr open Const_omega module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint) open OmegaSolver @@ -67,14 +66,14 @@ type comparaison = Eq | Leq | Geq | Gt | Lt | Neq (it could contains some [Term.Var] but no [Term.Rel]). So no need to lift when breaking or creating arrows. *) type oproposition = - Pequa of constr * oequation (* constr = copy of the Coq formula *) + Pequa of EConstr.t * oequation (* constr = copy of the Coq formula *) | Ptrue | Pfalse | Pnot of oproposition | Por of int * oproposition * oproposition | Pand of int * oproposition * oproposition | Pimp of int * oproposition * oproposition - | Pprop of constr + | Pprop of EConstr.t (* The equations *) and oequation = { @@ -101,9 +100,9 @@ and oequation = { type environment = { (* La liste des termes non reifies constituant l'environnement global *) - mutable terms : constr list; + mutable terms : EConstr.t list; (* La meme chose pour les propositions *) - mutable props : constr list; + mutable props : EConstr.t list; (* Traduction des indices utilisés ici en les indices finaux utilisés par * la tactique Omega après dénombrement des variables utiles *) real_indices : int IntHtbl.t; @@ -185,7 +184,7 @@ let print_env_reification env = | t :: l -> let sigma, env = Pfedit.get_current_context () in let s = Printf.sprintf "(%c%02d)" c i in - spc () ++ str s ++ str " := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ + spc () ++ str s ++ str " := " ++ Printer.pr_econstr_env env sigma t ++ fnl () ++ loop c (succ i) l in let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in @@ -218,8 +217,8 @@ let display_omega_var i = Printf.sprintf "OV%d" i l'environnement initial contenant tout. Il faudra le réduire après calcul des variables utiles. *) -let add_reified_atom t env = - try List.index0 Constr.equal t env.terms +let add_reified_atom sigma t env = + try List.index0 (EConstr.eq_constr sigma) t env.terms with Not_found -> let i = List.length env.terms in env.terms <- env.terms @ [t]; i @@ -236,8 +235,8 @@ let set_reified_atom v t env = (* \subsection{Gestion de l'environnement de proposition pour Omega} *) (* ajout d'une proposition *) -let add_prop env t = - try List.index0 Constr.equal t env.props +let add_prop sigma env t = + try List.index0 (EConstr.eq_constr sigma) t env.props with Not_found -> let i = List.length env.props in env.props <- env.props @ [t]; i @@ -290,7 +289,7 @@ let oformula_of_omega af = in loop af.body -let app f v = mkApp(Lazy.force f,v) +let app f v = EConstr.mkApp(Lazy.force f,v) (* \subsection{Oformula vers COQ reel} *) @@ -347,18 +346,19 @@ let reified_conn = function | Pimp _ -> app coq_p_imp | _ -> assert false -let rec reified_of_oprop env t = match t with +let rec reified_of_oprop sigma env t = match t with | Pequa (_,{ e_comp=cmp; e_left=t1; e_right=t2 }) -> reified_cmp cmp [| reified_of_formula env t1; reified_of_formula env t2 |] | Ptrue -> Lazy.force coq_p_true | Pfalse -> Lazy.force coq_p_false - | Pnot t -> app coq_p_not [| reified_of_oprop env t |] + | Pnot t -> app coq_p_not [| reified_of_oprop sigma env t |] | Por (_,t1,t2) | Pand (_,t1,t2) | Pimp (_,t1,t2) -> - reified_conn t [| reified_of_oprop env t1; reified_of_oprop env t2 |] - | Pprop t -> app coq_p_prop [| mk_nat (add_prop env t) |] + reified_conn t + [| reified_of_oprop sigma env t1; reified_of_oprop sigma env t2 |] + | Pprop t -> app coq_p_prop [| mk_nat (add_prop sigma env t) |] -let reified_of_proposition env f = - try reified_of_oprop env f +let reified_of_proposition sigma env f = + try reified_of_oprop sigma env f with reraise -> pprint stderr f; raise reraise let reified_of_eq env (l,r) = @@ -475,28 +475,28 @@ let mkPor i x y = Por (i,x,y) let mkPand i x y = Pand (i,x,y) let mkPimp i x y = Pimp (i,x,y) -let rec oformula_of_constr env t = - match Z.parse_term t with - | Tplus (t1,t2) -> binop env (fun x y -> Oplus(x,y)) t1 t2 - | Tminus (t1,t2) -> binop env (fun x y -> Ominus(x,y)) t1 t2 +let rec oformula_of_constr sigma env t = + match Z.parse_term sigma t with + | Tplus (t1,t2) -> binop sigma env (fun x y -> Oplus(x,y)) t1 t2 + | Tminus (t1,t2) -> binop sigma env (fun x y -> Ominus(x,y)) t1 t2 | Tmult (t1,t2) -> - (match Z.get_scalar t1 with - | Some n -> Omult (Oint n,oformula_of_constr env t2) + (match Z.get_scalar sigma t1 with + | Some n -> Omult (Oint n,oformula_of_constr sigma env t2) | None -> - match Z.get_scalar t2 with - | Some n -> Omult (oformula_of_constr env t1, Oint n) - | None -> Oatom (add_reified_atom t env)) - | Topp t -> Oopp(oformula_of_constr env t) - | Tsucc t -> Oplus(oformula_of_constr env t, Oint one) + match Z.get_scalar sigma t2 with + | Some n -> Omult (oformula_of_constr sigma env t1, Oint n) + | None -> Oatom (add_reified_atom sigma t env)) + | Topp t -> Oopp(oformula_of_constr sigma env t) + | Tsucc t -> Oplus(oformula_of_constr sigma env t, Oint one) | Tnum n -> Oint n - | Tother -> Oatom (add_reified_atom t env) + | Tother -> Oatom (add_reified_atom sigma t env) -and binop env c t1 t2 = - let t1' = oformula_of_constr env t1 in - let t2' = oformula_of_constr env t2 in +and binop sigma env c t1 t2 = + let t1' = oformula_of_constr sigma env t1 in + let t2' = oformula_of_constr sigma env t2 in c t1' t2' -and binprop env (neg2,depends,origin,path) +and binprop sigma env (neg2,depends,origin,path) add_to_depends neg1 gl c t1 t2 = let i = new_connector_id env in let depends1 = if add_to_depends then Left i::depends else depends in @@ -504,41 +504,41 @@ and binprop env (neg2,depends,origin,path) if add_to_depends then IntHtbl.add env.constructors i {o_hyp = origin; o_path = List.rev path}; let t1' = - oproposition_of_constr env (neg1,depends1,origin,O_left::path) gl t1 in + oproposition_of_constr sigma env (neg1,depends1,origin,O_left::path) gl t1 in let t2' = - oproposition_of_constr env (neg2,depends2,origin,O_right::path) gl t2 in + oproposition_of_constr sigma env (neg2,depends2,origin,O_right::path) gl t2 in (* On numérote le connecteur dans l'environnement. *) c i t1' t2' -and mk_equation env ctxt c connector t1 t2 = - let t1' = oformula_of_constr env t1 in - let t2' = oformula_of_constr env t2 in +and mk_equation sigma env ctxt c connector t1 t2 = + let t1' = oformula_of_constr sigma env t1 in + let t2' = oformula_of_constr sigma env t2 in (* On ajoute l'equation dans l'environnement. *) let omega = normalize_equation env ctxt connector t1' t2' in add_equation env omega; Pequa (c,omega) -and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c = +and oproposition_of_constr sigma env ((negated,depends,origin,path) as ctxt) gl c = match Z.parse_rel gl c with - | Req (t1,t2) -> mk_equation env ctxt c Eq t1 t2 - | Rne (t1,t2) -> mk_equation env ctxt c Neq t1 t2 - | Rle (t1,t2) -> mk_equation env ctxt c Leq t1 t2 - | Rlt (t1,t2) -> mk_equation env ctxt c Lt t1 t2 - | Rge (t1,t2) -> mk_equation env ctxt c Geq t1 t2 - | Rgt (t1,t2) -> mk_equation env ctxt c Gt t1 t2 + | Req (t1,t2) -> mk_equation sigma env ctxt c Eq t1 t2 + | Rne (t1,t2) -> mk_equation sigma env ctxt c Neq t1 t2 + | Rle (t1,t2) -> mk_equation sigma env ctxt c Leq t1 t2 + | Rlt (t1,t2) -> mk_equation sigma env ctxt c Lt t1 t2 + | Rge (t1,t2) -> mk_equation sigma env ctxt c Geq t1 t2 + | Rgt (t1,t2) -> mk_equation sigma env ctxt c Gt t1 t2 | Rtrue -> Ptrue | Rfalse -> Pfalse | Rnot t -> let ctxt' = (not negated, depends, origin,(O_mono::path)) in - Pnot (oproposition_of_constr env ctxt' gl t) - | Ror (t1,t2) -> binprop env ctxt (not negated) negated gl mkPor t1 t2 - | Rand (t1,t2) -> binprop env ctxt negated negated gl mkPand t1 t2 + Pnot (oproposition_of_constr sigma env ctxt' gl t) + | Ror (t1,t2) -> binprop sigma env ctxt (not negated) negated gl mkPor t1 t2 + | Rand (t1,t2) -> binprop sigma env ctxt negated negated gl mkPand t1 t2 | Rimp (t1,t2) -> - binprop env ctxt (not negated) (not negated) gl mkPimp t1 t2 + binprop sigma env ctxt (not negated) (not negated) gl mkPimp t1 t2 | Riff (t1,t2) -> (* No lifting here, since Omega only works on closed propositions. *) - binprop env ctxt negated negated gl mkPand - (Term.mkArrow t1 t2) (Term.mkArrow t2 t1) + binprop sigma env ctxt negated negated gl mkPand + (EConstr.mkArrow t1 t2) (EConstr.mkArrow t2 t1) | _ -> Pprop c (* Destructuration des hypothèses et de la conclusion *) @@ -553,27 +553,25 @@ let display_gl env t_concl t_lhyps = type defined = Defined | Assumed -let reify_hyp env gl i = +let reify_hyp sigma env gl i = let open Context.Named.Declaration in let ctxt = (false,[],i,[]) in match Tacmach.New.pf_get_hyp i gl with - | LocalDef (_,d,t) when Z.is_int_typ gl (EConstr.Unsafe.to_constr t) -> - let d = EConstr.Unsafe.to_constr d in + | LocalDef (_,d,t) when Z.is_int_typ gl t -> let dummy = Lazy.force coq_True in - let p = mk_equation env ctxt dummy Eq (mkVar i) d in + let p = mk_equation sigma env ctxt dummy Eq (EConstr.mkVar i) d in i,Defined,p | LocalDef (_,_,t) | LocalAssum (_,t) -> - let t = EConstr.Unsafe.to_constr t in - let p = oproposition_of_constr env ctxt gl t in + let p = oproposition_of_constr sigma env ctxt gl t in i,Assumed,p let reify_gl env gl = + let sigma = Proofview.Goal.sigma gl in let concl = Tacmach.New.pf_concl gl in - let concl = EConstr.Unsafe.to_constr concl in let hyps = Tacmach.New.pf_ids_of_hyps gl in let ctxt_concl = (true,[],id_concl,[O_mono]) in - let t_concl = oproposition_of_constr env ctxt_concl gl concl in - let t_lhyps = List.map (reify_hyp env gl) hyps in + let t_concl = oproposition_of_constr sigma env ctxt_concl gl concl in + let t_lhyps = List.map (reify_hyp sigma env gl) hyps in let () = if !debug then display_gl env t_concl t_lhyps in t_concl, t_lhyps @@ -684,8 +682,7 @@ let rec stated_in_tree = function | Tree(_,t1,t2) -> StateSet.union (stated_in_tree t1) (stated_in_tree t2) | Leaf s -> stated_in_trace s.s_trace -let mk_refl t = - EConstr.of_constr (app coq_refl_equal [|Lazy.force Z.typ; t|]) +let mk_refl t = app coq_refl_equal [|Lazy.force Z.typ; t|] let digest_stated_equations env tree = let do_equation st (vars,gens,eqns,ids) = @@ -775,7 +772,7 @@ let maximize_prop equas c = | t1', t2' -> Pand(i,t1',t2')) | Pimp(i,t1,t2) -> (match loop t1, loop t2 with - | Pprop p1, Pprop p2 -> Pprop (Term.mkArrow p1 p2) (* no lift (closed) *) + | Pprop p1, Pprop p2 -> Pprop (EConstr.mkArrow p1 p2) (* no lift (closed) *) | t1', t2' -> Pimp(i,t1',t2')) | Ptrue -> Pprop (app coq_True [||]) | Pfalse -> Pprop (app coq_False [||]) @@ -852,12 +849,15 @@ let hyp_idx env_hyp i = a O_SUM followed by a O_BAD_CONSTANT *) let sum_bad inv i1 i2 = + let open EConstr in mkApp (Lazy.force coq_s_sum, [| Z.mk Bigint.one; i1; Z.mk (if inv then negone else Bigint.one); i2; mkApp (Lazy.force coq_s_bad_constant, [| mk_nat 0 |])|]) -let rec reify_trace env env_hyp = function +let rec reify_trace env env_hyp = + let open EConstr in + function | CONSTANT_NOT_NUL(e,_) :: [] | CONSTANT_NEG(e,_) :: [] | CONSTANT_NUL e :: [] -> @@ -958,7 +958,7 @@ l'extraction d'un ensemble minimal de solutions permettant la résolution globale du système et enfin construit la trace qui permet de faire rejouer cette solution par la tactique réflexive. *) -let resolution unsafe env (reified_concl,reified_hyps) systems_list = +let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list = if !debug then Printf.printf "\n====================================\n"; let all_solutions = List.mapi (solve_system env) systems_list in let solution_tree = solve_with_constraints all_solutions [] in @@ -1006,15 +1006,15 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = (** The environment [env] (and especially [env.real_indices]) is now ready for the coming reifications: *) let l_reified_stated = List.map (reified_of_eq env) to_reify_stated in - let reified_concl = reified_of_proposition env reified_concl in + let reified_concl = reified_of_proposition sigma env reified_concl in let l_reified_terms = List.map (fun id -> match Id.Map.find id reified_hyps with | Defined,p -> - reified_of_proposition env p, mk_refl (mkVar id) + reified_of_proposition sigma env p, mk_refl (EConstr.mkVar id) | Assumed,p -> - reified_of_proposition env (maximize_prop useful_equa_ids p), + reified_of_proposition sigma env (maximize_prop useful_equa_ids p), EConstr.mkVar id | exception Not_found -> assert false) useful_hypnames @@ -1036,17 +1036,16 @@ let resolution unsafe env (reified_concl,reified_hyps) systems_list = let decompose_tactic = decompose_tree env context solution_tree in Tactics.generalize (l_generalize_arg @ l_reified_hypnames) >> - Tactics.convert_concl_no_check (EConstr.of_constr reified) Term.DEFAULTcast >> - Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic|])) >> + Tactics.convert_concl_no_check reified Term.DEFAULTcast >> + Tactics.apply (app coq_do_omega [|decompose_tactic|]) >> show_goal >> (if unsafe then (* Trust the produced term. Faster, but might fail later at Qed. Also handy when debugging, e.g. via a Show Proof after romega. *) - Tactics.convert_concl_no_check - (EConstr.of_constr (Lazy.force coq_True)) Term.VMcast + Tactics.convert_concl_no_check (Lazy.force coq_True) Term.VMcast else Tactics.normalise_vm_in_concl) >> - Tactics.apply (EConstr.of_constr (Lazy.force coq_I)) + Tactics.apply (Lazy.force coq_I) let total_reflexive_omega_tactic unsafe = Proofview.Goal.nf_enter begin fun gl -> @@ -1064,7 +1063,8 @@ let total_reflexive_omega_tactic unsafe = List.fold_left (fun s (id,d,p) -> Id.Map.add id (d,p) s) Id.Map.empty hyps in if !debug then display_systems systems_list; - resolution unsafe env (concl,hyps) systems_list + let sigma = Proofview.Goal.sigma gl in + resolution unsafe sigma env (concl,hyps) systems_list with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system") end diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index db17c0d65..06cdf76b4 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -11,7 +11,7 @@ Require Export List. Require Export Bintree. -Require Import Bool. +Require Import Bool BinPos. Declare ML Module "rtauto_plugin". @@ -98,8 +98,6 @@ match F with | F_push H hyps0 F0 => interp_ctx hyps0 F0 ([[H]] -> G) end. -Require Export BinPos. - Ltac wipe := intros;simpl;constructor. Lemma compose0 : @@ -257,122 +255,115 @@ Theorem interp_proof: forall p hyps F gl, check_proof hyps gl p = true -> interp_ctx hyps F [[gl]]. -induction p;intros hyps F gl. - -(* cas Axiom *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f nth_f e;rewrite <- (form_eq_refl e). -apply project with p;trivial. - -(* Cas Arrow_Intro *) -Focus 1. -destruct gl;clean. -simpl;intros. -change (interp_ctx (hyps\gl1) (F_push gl1 hyps F) [[gl2]]). -apply IHp;try constructor;trivial. - -(* Cas Arrow_Elim *) -Focus 1. -simpl check_proof;case_eq (get p hyps);clean. -intros f ef;case_eq (get p0 hyps);clean. -intros f0 ef0;destruct f0;clean. -case_eq (form_eq f f0_1);clean. -simpl;intros e check_p1. -generalize (project F ef) (project F ef0) -(IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1); -clear check_p1 IHp p p0 p1 ef ef0. -simpl. -apply compose3. -rewrite (form_eq_refl e). -auto. - -(* cas Arrow_Destruct *) -Focus 1. -simpl;case_eq (get p1 hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -case_eq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2);clean. -intros check_p1 check_p2. -generalize (project F ef) -(IHp1 (hyps \ f1_2 =>> f2 \ f1_1) -(F_push f1_1 (hyps \ f1_2 =>> f2) - (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1) -(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2). -simpl;apply compose3;auto. - -(* Cas False_Elim *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -intros _; generalize (project F ef). -apply compose1;apply False_ind. - -(* Cas And_Intro *) -Focus 1. -simpl;destruct gl;clean. -case_eq (check_proof hyps gl1 p1);clean. -intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2). -apply compose2 ;simpl;auto. - -(* cas And_Elim *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -intro check_p;generalize (project F ef) -(IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p). -simpl;apply compose2;intros [h1 h2];auto. - -(* cas And_Destruct *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -intro H;generalize (project F ef) -(IHp (hyps \ f1_1 =>> f1_2 =>> f2) -(F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H);clear H;simpl. -apply compose2;auto. - -(* cas Or_Intro_left *) -Focus 1. -destruct gl;clean. -intro Hp;generalize (IHp hyps F gl1 Hp). -apply compose1;simpl;auto. - -(* cas Or_Intro_right *) -Focus 1. -destruct gl;clean. -intro Hp;generalize (IHp hyps F gl2 Hp). -apply compose1;simpl;auto. - -(* cas Or_elim *) -Focus 1. -simpl;case_eq (get p1 hyps);clean. -intros f ef;destruct f;clean. -case_eq (check_proof (hyps \ f1) gl p2);clean. -intros check_p1 check_p2;generalize (project F ef) -(IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1) -(IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2); -simpl;apply compose3;simpl;intro h;destruct h;auto. - -(* cas Or_Destruct *) -Focus 1. -simpl;case_eq (get p hyps);clean. -intros f ef;destruct f;clean. -destruct f1;clean. -intro check_p0;generalize (project F ef) -(IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2) -(F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) - (F_push (f1_1 =>> f2) hyps F)) gl check_p0);simpl. -apply compose2;auto. - -(* cas Cut *) -Focus 1. -simpl;case_eq (check_proof hyps f p1);clean. -intros check_p1 check_p2; -generalize (IHp1 hyps F f check_p1) -(IHp2 (hyps\f) (F_push f hyps F) gl check_p2); -simpl; apply compose2;auto. +induction p; intros hyps F gl. + +- (* Axiom *) + simpl;case_eq (get p hyps);clean. + intros f nth_f e;rewrite <- (form_eq_refl e). + apply project with p;trivial. + +- (* Arrow_Intro *) + destruct gl; clean. + simpl; intros. + change (interp_ctx (hyps\gl1) (F_push gl1 hyps F) [[gl2]]). + apply IHp; try constructor; trivial. + +- (* Arrow_Elim *) + simpl check_proof; case_eq (get p hyps); clean. + intros f ef; case_eq (get p0 hyps); clean. + intros f0 ef0; destruct f0; clean. + case_eq (form_eq f f0_1); clean. + simpl; intros e check_p1. + generalize (project F ef) (project F ef0) + (IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1); + clear check_p1 IHp p p0 p1 ef ef0. + simpl. + apply compose3. + rewrite (form_eq_refl e). + auto. + +- (* Arrow_Destruct *) + simpl; case_eq (get p1 hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + case_eq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2); clean. + intros check_p1 check_p2. + generalize (project F ef) + (IHp1 (hyps \ f1_2 =>> f2 \ f1_1) + (F_push f1_1 (hyps \ f1_2 =>> f2) + (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1) + (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2). + simpl; apply compose3; auto. + +- (* False_Elim *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + intros _; generalize (project F ef). + apply compose1; apply False_ind. + +- (* And_Intro *) + simpl; destruct gl; clean. + case_eq (check_proof hyps gl1 p1); clean. + intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2). + apply compose2 ; simpl; auto. + +- (* And_Elim *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + intro check_p; + generalize (project F ef) + (IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p). + simpl; apply compose2; intros [h1 h2]; auto. + +- (* And_Destruct*) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + intro H; + generalize (project F ef) + (IHp (hyps \ f1_1 =>> f1_2 =>> f2) + (F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H); + clear H; simpl. + apply compose2; auto. + +- (* Or_Intro_left *) + destruct gl; clean. + intro Hp; generalize (IHp hyps F gl1 Hp). + apply compose1; simpl; auto. + +- (* Or_Intro_right *) + destruct gl; clean. + intro Hp; generalize (IHp hyps F gl2 Hp). + apply compose1; simpl; auto. + +- (* Or_elim *) + simpl; case_eq (get p1 hyps); clean. + intros f ef; destruct f; clean. + case_eq (check_proof (hyps \ f1) gl p2); clean. + intros check_p1 check_p2; + generalize (project F ef) + (IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1) + (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2); + simpl; apply compose3; simpl; intro h; destruct h; auto. + +- (* Or_Destruct *) + simpl; case_eq (get p hyps); clean. + intros f ef; destruct f; clean. + destruct f1; clean. + intro check_p0; + generalize (project F ef) + (IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2) + (F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2) + (F_push (f1_1 =>> f2) hyps F)) gl check_p0); + simpl. + apply compose2; auto. + +- (* Cut *) + simpl; case_eq (check_proof hyps f p1); clean. + intros check_p1 check_p2; + generalize (IHp1 hyps F f check_p1) + (IHp2 (hyps\f) (F_push f hyps F) gl check_p2); + simpl; apply compose2; auto. Qed. Theorem Reflect: forall gl prf, if check_proof empty gl prf then [[gl]] else True. diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 007d139a3..f049963f1 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -768,7 +768,7 @@ let discharge_hyp (id', (id, mode)) gl = let cl' = Vars.subst_var id (pf_concl gl) in match pf_get_hyp gl id, mode with | NamedDecl.LocalAssum (_, t), _ | NamedDecl.LocalDef (_, _, t), "(" -> - Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false (EConstr.of_constr (mkProd (Name id', t, cl'))) + Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true (EConstr.of_constr (mkProd (Name id', t, cl'))) [EConstr.of_constr (mkVar id)]) gl | NamedDecl.LocalDef (_, v, t), _ -> Proofview.V82.of_tactic @@ -1193,13 +1193,13 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = else let gl, ccl = pf_mkprod gl c cl in false, pat, ccl, c, clr,ucst,gl else if to_ind && occ = None then let nv, p, _, ucst' = pf_abs_evars gl (fst pat, c) in - let ucst = Evd.union_evar_universe_context ucst ucst' in + let ucst = UState.union ucst ucst' in if nv = 0 then anomaly "occur_existential but no evars" else let gl, pty = pfe_type_of gl p in false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl else CErrors.user_err ?loc:(loc_of_cpattern t) (str "generalized term didn't match") -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) +let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true x xs) let genclrtac cl cs clr = let tclmyORELSE tac1 tac2 gl = diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 7c16e1ba9..2b8f1d540 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -414,6 +414,8 @@ val clr_of_wgen : val unfold : EConstr.t list -> unit Proofview.tactic +val apply_type : EConstr.types -> EConstr.t list -> Proofview.V82.tac + (* New code ****************************************************************) (* To call old code *) diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 33ebe26b6..717657a24 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -30,8 +30,6 @@ module RelDecl = Context.Rel.Declaration (** The "case" and "elim" tactic *) -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) - (* TASSI: given the type of an elimination principle, it finds the higher order * argument (index), it computes it's arity and the arity of the eliminator and * checks if the eliminator is recursive or not *) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 00c971237..57635edac 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -216,7 +216,7 @@ let same_proj sigma t1 t2 = let all_ok _ _ = true let fake_pmatcher_end () = - mkProp, L2R, (Evd.empty, Evd.empty_evar_universe_context, mkProp) + mkProp, L2R, (Evd.empty, UState.empty, mkProp) let unfoldintac occ rdx t (kt,_) gl = let fs sigma x = Reductionops.nf_evar sigma x in @@ -372,8 +372,6 @@ let is_construct_ref sigma c r = EConstr.isConstruct sigma c && eq_gr (ConstructRef (fst(EConstr.destConstruct sigma c))) r let is_ind_ref sigma c r = EConstr.isInd sigma c && eq_gr (IndRef (fst(EConstr.destInd sigma c))) r -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) - let rwcltac cl rdx dir sr gl = let n, r_n,_, ucst = pf_abs_evars gl sr in let r_n' = pf_abs_cterm gl n r_n in diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index cdf1c6f95..9cc4f5cec 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -127,8 +127,6 @@ let endclausestac id_map clseq gl_id cl0 gl = if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else errorstrm Pp.(str "tampering with discharged assumptions of \"in\" tactical") -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) - let tclCLAUSES tac (gens, clseq) gl = if clseq = InGoal || clseq = InSeqGoal then tac gl else let clr_gens = pf_clauseids gl gens clseq in diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 62c35d6df..33b18001c 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -361,7 +361,7 @@ let unif_end env sigma0 ise0 pt ok = if ise2 == ise1 then (s, uc, t) else let s, uc', t = nf_open_term sigma0 ise2 t in - s, Evd.union_evar_universe_context uc uc', t + s, UState.union uc uc', t let unify_HO env sigma0 t1 t2 = let sigma = unif_HO env sigma0 t1 t2 in @@ -1268,7 +1268,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in sigma, [pat] in match pattern with - | None -> do_subst env0 concl0 concl0 1, Evd.empty_evar_universe_context + | None -> do_subst env0 concl0 concl0 1, UState.empty | Some (sigma, (T rp | In_T rp)) -> let rp = fs sigma rp in let ise = create_evar_defs sigma in diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml index d16f046fa..8864be576 100644 --- a/pretyping/univdecls.ml +++ b/pretyping/univdecls.ml @@ -38,7 +38,7 @@ let interp_univ_constraints env evd cstrs = let interp_univ_decl env decl = let open Misctypes in let pl : lident list = decl.univdecl_instance in - let evd = Evd.from_ctx (Evd.make_evar_universe_context env (Some pl)) in + let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in let decl = { univdecl_instance = pl; univdecl_extensible_instance = decl.univdecl_extensible_instance; diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 3682b7c25..9da94e42a 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -94,7 +94,7 @@ let print_ref reduce ref udecl = let env = Global.env () in let bl = Universes.universe_binders_with_opt_names ref (Array.to_list (Univ.Instance.to_array inst)) udecl in - let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in + let sigma = Evd.from_ctx (UState.of_binders bl) in let inst = if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs else mt () @@ -593,7 +593,7 @@ let print_constant with_values sep sp udecl = Array.to_list (Instance.to_array inst) in let ctx = - Evd.evar_universe_context_of_binders + UState.of_binders (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl) in let env = Global.env () and sigma = Evd.from_ctx ctx in diff --git a/printing/printer.ml b/printing/printer.ml index 917ee2021..e50d302b3 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -539,7 +539,7 @@ let pr_evgl_sign sigma evi = let ids = List.rev_map NamedDecl.get_id l in let warn = if List.is_empty ids then mt () else - (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") + (str " (" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") in let pc = pr_lconstr_env env sigma evi.evar_concl in let candidates = @@ -551,7 +551,7 @@ let pr_evgl_sign sigma evi = mt () in hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++ - candidates ++ spc () ++ warn) + candidates ++ warn) (* Print an existential variable *) @@ -560,15 +560,25 @@ let pr_evar sigma (evk, evi) = hov 0 (pr_existential_key sigma evk ++ str " : " ++ pegl) (* Print an enumerated list of existential variables *) -let rec pr_evars_int_hd head sigma i = function +let rec pr_evars_int_hd pr sigma i = function | [] -> mt () | (evk,evi)::rest -> - (hov 0 (head i ++ pr_evar sigma (evk,evi))) ++ - (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd head sigma (i+1) rest) - -let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ int i ++ str " =" ++ spc ()) sigma i (Evar.Map.bindings evs) - -let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs) + (hov 0 (pr i evk evi)) ++ + (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd pr sigma (i+1) rest) + +let pr_evars_int sigma ~shelf ~givenup i evs = + let pr_status i = + if List.mem i shelf then str " (shelved)" + else if List.mem i givenup then str " (given up)" + else mt () in + pr_evars_int_hd + (fun i evk evi -> + str "Existential " ++ int i ++ str " =" ++ + spc () ++ pr_evar sigma (evk,evi) ++ pr_status evk) + sigma i (Evar.Map.bindings evs) + +let pr_evars sigma evs = + pr_evars_int_hd (fun i evk evi -> pr_evar sigma (evk,evi)) sigma 1 (Evar.Map.bindings evs) (* Display a list of evars given by their name, with a prefix *) let pr_ne_evar_set hd tl sigma l = @@ -686,7 +696,7 @@ let print_dependent_evars gl sigma seeds = (* spiwack: [pr_first] is true when the first goal must be singled out and printed in its entirety. *) let default_pr_subgoals ?(pr_first=true) - close_cmd sigma seeds shelf stack unfocused goals = + close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals = (** Printing functions for the extra informations. *) let rec print_stack a = function | [] -> Pp.int a @@ -748,7 +758,7 @@ let default_pr_subgoals ?(pr_first=true) if Evar.Map.is_empty exl then (str"No more subgoals." ++ print_dependent_evars None sigma seeds) else - let pei = pr_evars_int sigma 1 exl in + let pei = pr_evars_int sigma ~shelf ~givenup:[] 1 exl in v 0 ((str "No more subgoals," ++ str " but there are non-instantiated existential variables:" ++ cut () ++ (hov 0 pei) @@ -775,7 +785,7 @@ let default_pr_subgoals ?(pr_first=true) type printer_pr = { - pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; + pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t; pr_subgoal : int -> evar_map -> goal list -> Pp.t; pr_goal : goal sigma -> Pp.t; } @@ -809,16 +819,16 @@ let pr_open_subgoals ~proof = begin match goals with | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in begin match bgoals,shelf,given_up with - | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack [] goals + | [] , [] , [] -> pr_subgoals None sigma ~seeds ~shelf ~stack ~unfocused:[] ~goals | [] , [] , _ -> Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); fnl () - ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] given_up + ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:given_up ++ fnl () ++ str "You need to go back and solve them." | [] , _ , _ -> Feedback.msg_info (str "All the remaining goals are on the shelf."); fnl () - ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] shelf + ++ pr_subgoals ~pr_first:false None bsigma ~seeds ~shelf:[] ~stack:[] ~unfocused:[] ~goals:shelf | _ , _, _ -> let end_cmd = str "This subproof is complete, but there are some unfocused goals." ++ @@ -826,13 +836,13 @@ let pr_open_subgoals ~proof = if Pp.ismt s then s else fnl () ++ s) ++ fnl () in - pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] [] bgoals + pr_subgoals ~pr_first:false (Some end_cmd) bsigma ~seeds ~shelf ~stack:[] ~unfocused:[] ~goals:bgoals end | _ -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in - pr_subgoals ~pr_first:true None bsigma seeds shelf [] unfocused_if_needed bgoals_focused + pr_subgoals ~pr_first:true None bsigma ~seeds ~shelf ~stack:[] ~unfocused:unfocused_if_needed ~goals:bgoals_focused end let pr_nth_open_subgoal ~proof n = diff --git a/printing/printer.mli b/printing/printer.mli index e32cb0921..41843680b 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -183,8 +183,7 @@ val pr_goal : goal sigma -> Pp.t focused goals unless the conrresponding option [enable_unfocused_goal_printing] is set. [seeds] is for printing dependent evars (mainly for emacs proof tree mode). *) -val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list - -> goal list -> goal list -> Pp.t +val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t val pr_subgoal : int -> evar_map -> goal list -> Pp.t val pr_concl : int -> evar_map -> goal -> Pp.t @@ -192,7 +191,7 @@ val pr_concl : int -> evar_map -> goal -> Pp.t val pr_open_subgoals : proof:Proof.t -> Pp.t val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t -val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> Pp.t +val pr_evars_int : evar_map -> shelf:goal list -> givenup:goal list -> int -> evar_info Evar.Map.t -> Pp.t val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t @@ -225,7 +224,8 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t type printer_pr = { - pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> Evar.t list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; + pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t; + pr_subgoal : int -> evar_map -> goal list -> Pp.t; pr_goal : goal sigma -> Pp.t; } diff --git a/printing/printmod.ml b/printing/printmod.ml index 43796ec61..e076c10f3 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -141,7 +141,7 @@ let print_mutual_inductive env mind mib udecl = else [] in let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in - let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in + let sigma = Evd.from_ctx (UState.of_binders bl) in hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ Printer.pr_cumulative (Declareops.inductive_is_polymorphic mib) @@ -185,7 +185,7 @@ let print_record env mind mib udecl = let envpar = push_rel_context params env in let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0)) (Array.to_list (Univ.Instance.to_array u)) udecl in - let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in + let sigma = Evd.from_ctx (UState.of_binders bl) in let keyword = let open Declarations in match mib.mind_finite with diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index d713b0999..8b5b739a3 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -341,7 +341,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let subst_evar k = Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in let nf = Universes.nf_evars_and_universes_opt_subst subst_evar - (Evd.evar_universe_context_subst universes) in + (UState.subst universes) in let make_body = if poly || now then let make_body t (c, eff) = @@ -436,7 +436,7 @@ let return_proof ?(allow_partial=false) () = | Proof.HasUnresolvedEvar-> error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in let eff = Evd.eval_side_effects evd in - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) diff --git a/stm/stm.ml b/stm/stm.ml index d878bbb30..b3da97c6e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2482,7 +2482,7 @@ let known_state ?(redefine_qed=false) ~cache id = match keep with | VtDrop -> None | VtKeepAsAxiom -> - let ctx = Evd.empty_evar_universe_context in + let ctx = UState.empty in let fp = Future.from_val ([],ctx) in qed.fproof <- Some (fp, ref false); None | VtKeep -> diff --git a/tactics/auto.ml b/tactics/auto.ml index 3eea1a74f..0c0d9bcfc 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -42,9 +42,9 @@ let compute_secvars gl = open Unification -let auto_core_unif_flags_of st1 st2 useeager = { +let auto_core_unif_flags_of st1 st2 = { modulo_conv_on_closed_terms = Some st1; - use_metas_eagerly_in_conv_on_closed_terms = useeager; + use_metas_eagerly_in_conv_on_closed_terms = false; use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = st2; modulo_delta_types = full_transparent_state; @@ -57,8 +57,8 @@ let auto_core_unif_flags_of st1 st2 useeager = { modulo_eta = true; } -let auto_unif_flags_of st1 st2 useeager = - let flags = auto_core_unif_flags_of st1 st2 useeager in { +let auto_unif_flags_of st1 st2 = + let flags = auto_core_unif_flags_of st1 st2 in { core_unify_flags = flags; merge_unify_flags = flags; subterm_unify_flags = { flags with modulo_delta = empty_transparent_state }; @@ -67,7 +67,7 @@ let auto_unif_flags_of st1 st2 useeager = } let auto_unif_flags = - auto_unif_flags_of full_transparent_state empty_transparent_state false + auto_unif_flags_of full_transparent_state empty_transparent_state (* Try unification with the precompiled clause, then use registered Apply *) @@ -291,10 +291,10 @@ let tclTRY_dbg d tac = de Hint impérative a été remplacée par plusieurs bases fonctionnelles *) let flags_of_state st = - auto_unif_flags_of st st false + auto_unif_flags_of st st let auto_flags_of_state st = - auto_unif_flags_of full_transparent_state st false + auto_unif_flags_of full_transparent_state st let hintmap_of sigma secvars hdc concl = match hdc with diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 45926551b..477de6452 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -214,7 +214,7 @@ let build_sym_scheme env ind = rel_vect (2*nrealargs+2) nrealargs])), mkRel 1 (* varH *), [|cstr (nrealargs+1)|])))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" @@ -285,7 +285,7 @@ let build_sym_involutive_scheme env ind = mkRel 1|])), mkRel 1 (* varH *), [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))) - in (c, Evd.evar_universe_context_of ctx), eff + in (c, UState.of_context_set ctx), eff let sym_involutive_scheme_kind = declare_individual_scheme_object "_sym_involutive" @@ -439,7 +439,7 @@ let build_l2r_rew_scheme dep env ind kind = [|main_body|]) else main_body)))))) - in (c, Evd.evar_universe_context_of ctx), + in (c, UState.of_context_set ctx), Safe_typing.concat_private eff' eff (**********************************************************************) @@ -528,7 +528,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s) (mkNamedLambda varHC applied_PC' (mkVar varHC))|]))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx (**********************************************************************) (* Build the right-to-left rewriting lemma for hypotheses associated *) @@ -601,7 +601,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = lift (nrealargs+3) applied_PC, mkRel 1)|]), [|mkVar varHC|])))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx (**********************************************************************) (* This function "repairs" the non-dependent r2l forward rewriting *) @@ -808,7 +808,7 @@ let build_congr env (eq,refl,ctx) ind = [|mkApp (refl, [|mkVar varB; mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|])))))) - in c, Evd.evar_universe_context_of ctx + in c, UState.of_context_set ctx let congr_scheme_kind = declare_individual_scheme_object "_congr" (fun _ ind -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 236db1dcc..98f627f21 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -56,18 +56,7 @@ type inj_flags = { injection_pattern_l2r_order : bool; } -let discriminate_introduction = ref true - -let discr_do_intro () = !discriminate_introduction - open Goptions -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "automatic introduction of hypotheses by discriminate"; - optkey = ["Discriminate";"Introduction"]; - optread = (fun () -> !discriminate_introduction); - optwrite = (:=) discriminate_introduction } let use_injection_pattern_l2r_order = function | None -> true @@ -1080,13 +1069,10 @@ let discrClause with_evars = onClause (discrSimpleClause with_evars) let discrEverywhere with_evars = tclTHEN (Proofview.tclUNIT ()) (* Delay the interpretation of side-effect *) - (if discr_do_intro () then - (tclTHEN - (tclREPEAT introf) - (tryAllHyps + (tclTHEN + (tclREPEAT introf) + (tryAllHyps (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings))))) - else (* <= 8.2 compat *) - tryAllHypsAndConcl (discrSimpleClause with_evars)) let discr_tac with_evars = function | None -> discrEverywhere with_evars diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index b960a845c..62ead57f3 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -122,8 +122,8 @@ let compute_name internal id = let define internal id c p univs = let fd = declare_constant ~internal in let id = compute_name internal id in - let ctx = Evd.normalize_evar_universe_context univs in - let c = Universes.subst_opt_univs_constr (Evd.evar_universe_context_subst ctx) c in + let ctx = UState.minimize univs in + let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in let univs = if p then Polymorphic_const_entry (UState.context ctx) else Monomorphic_const_entry (UState.context_set ctx) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 655283c20..a4cdc1592 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -218,7 +218,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = end in let avoid = ref Id.Set.empty in let _,_,_,_,sigma = Proof.proof pf in - let sigma = Evd.nf_constraints sigma in + let sigma = Evd.minimize_universes sigma in let rec fill_holes c = match EConstr.kind sigma c with | Evar (e,args) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b99a45103..12aef852d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -15,7 +15,6 @@ open CErrors open Util open Names open Nameops -open Term open Constr open Termops open Environ @@ -89,18 +88,6 @@ let _ = optread = (fun () -> !universal_lemma_under_conjunctions) ; optwrite = (fun b -> universal_lemma_under_conjunctions := b) } -(* Shrinking of abstract proofs. *) - -let shrink_abstract = ref true - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "shrinking of abstracted proofs"; - optkey = ["Shrink"; "Abstract"]; - optread = (fun () -> !shrink_abstract) ; - optwrite = (fun b -> shrink_abstract := b) } - (* The following boolean governs what "intros []" do on examples such as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]"; if false, it behaves as "intro H; case H; clear H" for fresh H. @@ -400,12 +387,11 @@ let find_name mayrepl decl naming gl = match naming with new_fresh_id idl (default_id env sigma decl) gl | NamingBasedOn (id,idl) -> new_fresh_id idl id gl | NamingMustBe (loc,id) -> - (* When name is given, we allow to hide a global name *) - let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in - let id' = next_ident_away id ids_of_hyps in - if not mayrepl && not (Id.equal id' id) then - user_err ?loc (Id.print id ++ str" is already used."); - id + (* When name is given, we allow to hide a global name *) + let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in + if not mayrepl && Id.Set.mem id ids_of_hyps then + user_err ?loc (Id.print id ++ str" is already used."); + id (**************************************************************) (* Computing position of hypotheses for replacing *) @@ -1339,46 +1325,6 @@ let index_of_ind_arg sigma t = | None -> error "Could not find inductive argument of elimination scheme." in aux None 0 t -let enforce_prop_bound_names rename tac = - let open Context.Rel.Declaration in - match rename with - | Some (isrec,nn) when Namegen.use_h_based_elimination_names () -> - (* Rename dependent arguments in Prop with name "H" *) - (* so as to avoid having hypothesis such as "t:True", "n:~A" when calling *) - (* elim or induction with schemes built by Indrec.build_induction_scheme *) - let rec aux env sigma i t = - if i = 0 then t else match EConstr.kind sigma t with - | Prod (Name _ as na,t,t') -> - let very_standard = true in - let na = - if Retyping.get_sort_family_of env sigma t = InProp then - (* "very_standard" says that we should have "H" names only, but - this would break compatibility even more... *) - let s = match Namegen.head_name sigma t with - | Some id when not very_standard -> Id.to_string id - | _ -> "" in - Name (add_suffix Namegen.default_prop_ident s) - else - na in - mkProd (na,t,aux (push_rel (LocalAssum (na,t)) env) sigma (i-1) t') - | Prod (Anonymous,t,t') -> - mkProd (Anonymous,t,aux (push_rel (LocalAssum (Anonymous,t)) env) sigma (i-1) t') - | LetIn (na,c,t,t') -> - mkLetIn (na,c,t,aux (push_rel (LocalDef (na,c,t)) env) sigma (i-1) t') - | _ -> assert false in - let rename_branch i = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let t = Proofview.Goal.concl gl in - change_concl (aux env sigma i t) - end in - (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) - tac - (Array.map rename_branch nn) - | _ -> - tac - let rec contract_letin_in_lam_header sigma c = match EConstr.kind sigma c with | Lambda (x,t,c) -> mkLambda (x,t,contract_letin_in_lam_header sigma c) @@ -1399,7 +1345,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags (str "The type of elimination clause is not well-formed.")) in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in - enforce_prop_bound_names rename (Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags) + Clenvtac.res_pf elimclause' ~with_evars ~with_classes ~flags end (* @@ -4221,7 +4167,7 @@ let induction_tac with_evars params indvars elim = let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in - enforce_prop_bound_names rename (Clenvtac.clenv_refine with_evars resolved) + Clenvtac.clenv_refine with_evars resolved end (* Apply induction "in place" taking into account dependent @@ -4986,10 +4932,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let (_, info) = CErrors.push src in iraise (e, info) in - let const, args = - if !shrink_abstract then shrink_entry sign const - else (const, List.rev (Context.Named.to_instance Constr.mkVar sign)) - in + let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v index 85ad41d1c..23a58501f 100644 --- a/test-suite/bugs/closed/2378.v +++ b/test-suite/bugs/closed/2378.v @@ -505,8 +505,6 @@ Qed. Require Export Coq.Logic.FunctionalExtensionality. Print PLanguage. -Unset Standard Proposition Elimination Names. - Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): Transformation (PLanguage l1) (PLanguage l2) := mkTransformation (PLanguage l1) (PLanguage l2) diff --git a/test-suite/bugs/closed/6634.v b/test-suite/bugs/closed/6634.v new file mode 100644 index 000000000..7f33afcc2 --- /dev/null +++ b/test-suite/bugs/closed/6634.v @@ -0,0 +1,6 @@ +From Coq Require Import ssreflect. + +Lemma normalizeP (p : tt = tt) : p = p. +Proof. +Fail move: {2} tt p. +Abort. diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v index 0b576db6b..820022d99 100644 --- a/test-suite/bugs/opened/1596.v +++ b/test-suite/bugs/opened/1596.v @@ -2,7 +2,6 @@ Require Import Relations. Require Import FSets. Require Import Arith. Require Import Omega. -Unset Standard Proposition Elimination Names. Set Keyed Unification. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 4df21ae35..e73312c67 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -11,7 +11,7 @@ notation scopes add ': clear scopes' [arguments-assert,vernacular] eq_refl : ?y = ?y where -?y : [ |- nat] +?y : [ |- nat] Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq_refl: Arguments are renamed to B, y diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out index 9680d2bbf..18f5d89f6 100644 --- a/test-suite/output/Existentials.out +++ b/test-suite/output/Existentials.out @@ -1,4 +1,4 @@ -Existential 1 = ?Goal : [p : nat q := S p : nat n : nat m : nat |- ?y = m] +Existential 1 = ?Goal : [p : nat q := S p : nat n : nat m : nat |- ?y = m] Existential 2 = -?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used) -Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y] +?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used) (shelved) +Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y] diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index e6a6e0288..864b6151a 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -33,24 +33,24 @@ fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f : (forall x : nat * (bool * unit), ?T) -> forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))} where -?T : [x : nat * (bool * unit) |- Type] +?T : [x : nat * (bool * unit) |- Type] fun f : forall x : bool * (nat * unit), ?T => CURRYINV (x : nat) (y : bool), f : (forall x : bool * (nat * unit), ?T) -> forall (x : nat) (y : bool), ?T@{x:=(y, (x, tt))} where -?T : [x : bool * (nat * unit) |- Type] +?T : [x : bool * (nat * unit) |- Type] fun f : forall x : unit * nat * bool, ?T => CURRYLEFT (x : nat) (y : bool), f : (forall x : unit * nat * bool, ?T) -> forall (x : nat) (y : bool), ?T@{x:=(tt, x, y)} where -?T : [x : unit * nat * bool |- Type] +?T : [x : unit * nat * bool |- Type] fun f : forall x : unit * bool * nat, ?T => CURRYINVLEFT (x : nat) (y : bool), f : (forall x : unit * bool * nat, ?T) -> forall (x : nat) (y : bool), ?T@{x:=(tt, y, x)} where -?T : [x : unit * bool * nat |- Type] +?T : [x : unit * bool * nat |- Type] forall n : nat, {#n | 1 > n} : Prop forall x : nat, {|x | x > 0|} diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index d28ee4276..5e9eff048 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -9,10 +9,10 @@ fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H fun n : nat => let y : T n := A n in ?t ?x : T n : forall n : nat, T n where -?t : [n : nat y := A n : T n |- ?T -> T n] -?x : [n : nat y := A n : T n |- ?T] +?t : [n : nat y := A n : T n |- ?T -> T n] +?x : [n : nat y := A n : T n |- ?T] fun n : nat => ?t ?x : T n : forall n : nat, T n where -?t : [n : nat |- ?T -> T n] -?x : [n : nat |- ?T] +?t : [n : nat |- ?T -> T n] +?x : [n : nat |- ?T] diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 6962e43e7..8d08f5975 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -172,3 +172,14 @@ Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e) Timeout 1 Fail apply _. (* 0.06s *) Abort. End HintCut. + + +(* Check that auto-like tactics do not prefer "eq_refl" over more complex solutions, *) +(* e.g. those tactics when considering a goal with existential varibles *) +(* like "m = ?n" won't pick "plus_n_O" hint over "eq_refl" hint. *) +(* See this Coq club post for more detail: *) +(* https://sympa.inria.fr/sympa/arc/coq-club/2017-12/msg00103.html *) + +Goal forall (m : nat), exists n, m = n /\ m = n. + intros m; eexists; split; [trivial | reflexivity]. +Qed. diff --git a/test-suite/success/ShowExtraction.v b/test-suite/success/ShowExtraction.v new file mode 100644 index 000000000..e34c240c5 --- /dev/null +++ b/test-suite/success/ShowExtraction.v @@ -0,0 +1,31 @@ + +Require Extraction. +Require Import List. + +Section Test. +Variable A : Type. +Variable decA : forall (x y:A), {x=y}+{x<>y}. + +(** Should fail when no proofs are started *) +Fail Show Extraction. + +Lemma decListA : forall (xs ys : list A), {xs=ys}+{xs<>ys}. +Proof. +Show Extraction. +fix 1. +destruct xs as [|x xs], ys as [|y ys]. +Show Extraction. +- now left. +- now right. +- now right. +- Show Extraction. + destruct (decA x y). + + destruct (decListA xs ys). + * left; now f_equal. + * Show Extraction. + right. congruence. + + right. congruence. +Show Extraction. +Defined. + +End Test. diff --git a/test-suite/success/name_mangling.v b/test-suite/success/name_mangling.v new file mode 100644 index 000000000..571dde880 --- /dev/null +++ b/test-suite/success/name_mangling.v @@ -0,0 +1,192 @@ +(* -*- coq-prog-args: ("-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. +Fail exact H. +exact _0. +Abort. + +Unset Mangle Names. +Goal True -> True. +intro; exact H. +Abort. + +Set Mangle Names. +Set Mangle Names Prefix "baz". +Goal True -> True. +intro. +Fail exact H. +Fail exact _0. +exact baz0. +Abort. + +Goal True -> True. +intro; assumption. +Abort. + +Goal True -> True. +intro x; exact x. +Abort. + +Goal forall x y, x+y=0. +intro x. +refine (fun x => _). +Fail Check x0. +Check x. +Abort. + +(* Example from Emilio *) + +Goal forall b : False, b = b. +intro b. +refine (let b := I in _). +Fail destruct b0. +Abort. + +(* Example from Cyprien *) + +Goal True -> True. +Proof. + refine (fun _ => _). + Fail exact t. +Abort. + +(* Example from Jason *) + +Goal False -> False. +intro H. +Fail abstract exact H. +Abort. + +(* Variant *) + +Goal False -> False. +intro. +Fail abstract exact H. +Abort. + +(* Example from Jason *) + +Goal 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'. +Qed. + +(* Variant *) + +Goal False -> False. +intro. +Fail let H' := H in abstract exact H'. +Abort. + +(* Indirectly testing preservation of names by move (derived from Jason) *) + +Inductive nat2 := S2 (_ _ : nat2). +Goal forall t : nat2, True. + intro t. + let IHt1 := fresh "IHt1" in + let IHt2 := fresh "IHt2" in + induction t as [? IHt1 ? IHt2]. + Fail exact IHt1. +Abort. + +(* Example on "pose proof" (from Jason) *) + +Goal False -> False. +intro; pose proof I as H0. +Fail exact H. +Abort. + +(* Testing the approach for which non alpha-renamed quantified names are user-generated *) + +Section foo. +Context (b : True). +Goal forall b : False, b = b. +Fail destruct b0. +Abort. + +Goal forall b : False, b = b. +now destruct b. +Qed. +End foo. + +(* Test stability of "fix" *) + +Lemma a : forall n, n = 0. +Proof. +fix a 1. +Check a. +fix 1. +Fail Check a0. +Abort. + +(* Test stability of "induction" *) + +Lemma a : forall n : nat, n = n. +Proof. +intro n; induction n as [ | n IHn ]. +- auto. +- Check n. + Check IHn. +Abort. + +Inductive I := C : I -> I -> I. + +Lemma a : forall n : I, n = n. +Proof. +intro n; induction n as [ n1 IHn1 n2 IHn2 ]. +Check n1. +Check n2. +apply f_equal2. ++ apply IHn1. ++ apply IHn2. +Qed. + +(* Testing remember *) + +Lemma c : 0 = 0. +Proof. +remember 0 as x eqn:Heqx. +Check Heqx. +Abort. + +Lemma c : forall Heqx, Heqx -> 0 = 0. +Proof. +intros Heqx X. +remember 0 as x. +Fail Check Heqx0. (* Heqx0 is not canonical *) +Abort. + +(* An example by Jason from the discussion for PR #268 *) + +Goal nat -> Set -> True. + intros x y. + match goal with + | [ x : _, y : _ |- _ ] + => let z := fresh "z" in + rename y into z, x into y; + let x' := fresh "x" in + rename z into x' + end. + revert y. (* x has been explicitly moved to y *) + Fail revert x. (* x comes from "fresh" *) +Abort. + +Goal nat -> Set -> True. + intros. + match goal with + | [ x : _, y : _ |- _ ] + => let z := fresh "z" in + rename y into z, x into y; + let x' := fresh "x" in + rename z into x' + end. + Fail revert y. (* generated by intros *) + Fail revert x. (* generated by intros *) +Abort. diff --git a/test-suite/success/shrink_abstract.v b/test-suite/success/shrink_abstract.v index 3f6b9cb39..916bb846a 100644 --- a/test-suite/success/shrink_abstract.v +++ b/test-suite/success/shrink_abstract.v @@ -1,5 +1,3 @@ -Set Shrink Abstract. - Definition foo : forall (n m : nat), bool. Proof. pose (p := 0). diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 683a442cb..72073bb4f 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -77,6 +77,7 @@ Reserved Notation "{ x | P & Q }" (at level 0, x at level 99). Reserved Notation "{ x : A | P }" (at level 0, x at level 99). Reserved Notation "{ x : A | P & Q }" (at level 0, x at level 99). +Reserved Notation "{ x & P }" (at level 0, x at level 99). Reserved Notation "{ x : A & P }" (at level 0, x at level 99). Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99). diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 73c8c5ef4..d5322d094 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -92,7 +92,9 @@ Lemma plus_n_O : forall n:nat, n = n + 0. Proof. induction n; simpl; auto. Qed. -Hint Resolve plus_n_O: core. + +Remove Hints eq_refl : core. +Hint Resolve plus_n_O eq_refl: core. (* We want eq_refl to have higher priority than plus_n_O *) Lemma plus_O_n : forall n:nat, 0 + n = n. Proof. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 137bd3a0f..b6afba29a 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -51,6 +51,7 @@ Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope. Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. +Notation "{ x & P }" := (sigT (fun x => P)) : type_scope. Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope. Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 9fd52866e..238ac7df0 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -28,6 +28,8 @@ intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. [[Werner97]] Benjamin Werner, Sets in Types, Types in Sets, TACS, 1997. *) +Require Import RelationClasses Logic. + Set Implicit Arguments. Local Unset Intuition Negation Unfolding. @@ -125,8 +127,6 @@ Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) := formulation of choice); Note also a typo in its intended formulation in [[Werner97]]. *) -Require Import RelationClasses Logic. - Definition RepresentativeFunctionalChoice_on := forall R:A->A->Prop, (Equivalence R) -> diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index 88ab4d6e1..afb78e1c8 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -29,46 +29,34 @@ Lemma f_incr_implies_g_incr_interv : forall f g:R->R, forall lb ub, (forall x , f lb <= x -> x <= f ub -> lb <= g x <= ub) -> (forall x y, f lb <= x -> x < y -> y <= f ub -> g x < g y). Proof. -intros f g lb ub lb_lt_ub f_incr f_eq_g g_ok x y lb_le_x x_lt_y y_le_ub. - assert (x_encad : f lb <= x <= f ub). - split ; [assumption | apply Rle_trans with (r2:=y) ; [apply Rlt_le|] ; assumption]. - assert (y_encad : f lb <= y <= f ub). - split ; [apply Rle_trans with (r2:=x) ; [|apply Rlt_le] ; assumption | assumption]. - assert (Temp1 : lb <= lb) by intuition ; assert (Temp2 : ub <= ub) by intuition. - assert (gx_encad := g_ok _ (proj1 x_encad) (proj2 x_encad)). - assert (gy_encad := g_ok _ (proj1 y_encad) (proj2 y_encad)). - clear Temp1 Temp2. - case (Rlt_dec (g x) (g y)). - intuition. + intros f g lb ub lb_lt_ub f_incr f_eq_g g_ok x y lb_le_x x_lt_y y_le_ub. + assert (x_encad : f lb <= x <= f ub) by lra. + assert (y_encad : f lb <= y <= f ub) by lra. + assert (gx_encad := g_ok _ (proj1 x_encad) (proj2 x_encad)). + assert (gy_encad := g_ok _ (proj1 y_encad) (proj2 y_encad)). + case (Rlt_dec (g x) (g y)); [ easy |]. intros Hfalse. - assert (Temp := Rnot_lt_le _ _ Hfalse). - assert (Hcontradiction : y <= x). - replace y with (id y) by intuition ; replace x with (id x) by intuition ; - rewrite <- f_eq_g. rewrite <- f_eq_g. - assert (f_incr2 : forall x y, lb <= x -> x <= y -> y < ub -> f x <= f y). + assert (Temp := Rnot_lt_le _ _ Hfalse). + enough (y <= x) by lra. + replace y with (id y) by easy. + replace x with (id x) by easy. + rewrite <- f_eq_g by easy. + rewrite <- f_eq_g by easy. + assert (f_incr2 : forall x y, lb <= x -> x <= y -> y < ub -> f x <= f y). { intros m n lb_le_m m_le_n n_lt_ub. case (m_le_n). - intros ; apply Rlt_le ; apply f_incr ; [| | apply Rlt_le] ; assumption. - intros Hyp ; rewrite Hyp ; apply Req_le ; reflexivity. - apply f_incr2. - intuition. intuition. - Focus 3. intuition. - Focus 2. intuition. - Focus 2. intuition. Focus 2. intuition. - assert (Temp2 : g x <> ub). - intro Hf. - assert (Htemp : (comp f g) x = f ub). - unfold comp ; rewrite Hf ; reflexivity. - rewrite f_eq_g in Htemp ; unfold id in Htemp. - assert (Htemp2 : x < f ub). - apply Rlt_le_trans with (r2:=y) ; intuition. - clear -Htemp Htemp2. fourier. - intuition. intuition. - clear -Temp2 gx_encad. - case (proj2 gx_encad). - intuition. - intro Hfalse ; apply False_ind ; apply Temp2 ; assumption. - apply False_ind. clear - Hcontradiction x_lt_y. fourier. + - intros; apply Rlt_le, f_incr, Rlt_le; assumption. + - intros Hyp; rewrite Hyp; apply Req_le; reflexivity. + } + apply f_incr2; intuition. + enough (g x <> ub) by lra. + intro Hf. + assert (Htemp : (comp f g) x = f ub). { + unfold comp; rewrite Hf; reflexivity. + } + rewrite f_eq_g in Htemp by easy. + unfold id in Htemp. + fourier. Qed. Lemma derivable_pt_id_interv : forall (lb ub x:R), diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index a50140628..a79ddead2 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -11,6 +11,7 @@ (* G. Huet 1-9-95 *) Require Import Permut Setoid. +Require Plus. (* comm. and ass. of plus *) Set Implicit Arguments. @@ -69,9 +70,6 @@ Section multiset_defs. unfold meq; unfold munion; simpl; auto. Qed. - - Require Plus. (* comm. and ass. of plus *) - Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x). Proof. unfold meq; unfold multiplicity; unfold munion. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 95ba93232..7940bda1a 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -13,7 +13,7 @@ (* G. Huet 1-9-95 *) (* Updated Papageno 12/98 *) -Require Import Bool. +Require Import Bool Permut. Set Implicit Arguments. @@ -140,8 +140,6 @@ Hint Resolve seq_right. (** Here we should make uniset an abstract datatype, by hiding [Charac], [union], [charac]; all further properties are proved abstractly *) -Require Import Permut. - Lemma union_rotate : forall x y z:uniset, seq (union x (union y z)) (union z (union x y)). Proof. diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 8f583be97..d9e5ad676 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -136,7 +136,7 @@ Section defs. (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) -> (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) -> merge_lem l1 l2. - Require Import Morphisms. + Import Morphisms. Instance: Equivalence (@meq A). Proof. constructor; auto with datatypes. red. apply meq_trans. Defined. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 727fd3ec3..e9f64542c 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -23,6 +23,7 @@ MLFILES := $(COQMF_MLFILES) ML4FILES := $(COQMF_ML4FILES) MLPACKFILES := $(COQMF_MLPACKFILES) MLLIBFILES := $(COQMF_MLLIBFILES) +CMDLINE_VFILES := $(COQMF_CMDLINE_VFILES) INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT) OTHERFLAGS := $(COQMF_OTHERFLAGS) COQ_SRC_SUBDIRS := $(COQMF_COQ_SRC_SUBDIRS) @@ -30,6 +31,7 @@ OCAMLLIBS := $(COQMF_OCAMLLIBS) SRC_SUBDIRS := $(COQMF_SRC_SUBDIRS) COQLIBS := $(COQMF_COQLIBS) COQLIBS_NOML := $(COQMF_COQLIBS_NOML) +CMDLINE_COQLIBS := $(COQMF_CMDLINE_COQLIBS) LOCAL := $(COQMF_LOCAL) COQLIB := $(COQMF_COQLIB) DOCDIR := $(COQMF_DOCDIR) @@ -724,9 +726,14 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack $(SHOW)'COQDEP $<' $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) +# If this makefile is created using a _CoqProject we have coqdep get +# options from it. This avoids argument length limits for pathological +# projects. Note that extra options might be on the command line. +VDFILE_FLAGS:=$(if @PROJECT_FILE@,-f @PROJECT_FILE@,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) + $(VDFILE).d: $(VFILES) $(SHOW)'COQDEP VFILES' - $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c $(VFILES) $(redir_if_ok) + $(HIDE)$(COQDEP) -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) # Misc ######################################################################## diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ef4428755..6cd520d60 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -13,6 +13,8 @@ open CoqProject_file open Printf +let (>) f g = fun x -> g (f x) + let output_channel = ref stdout let makefile_name = ref "Makefile" let make_name = ref "" @@ -175,21 +177,22 @@ let generate_conf_extra_target oc sps = in if sps <> [] then section oc "Extra targets. (-extra and -extra-phony, DEPRECATED)"; - List.iter pr_path sps + List.iter (forget_source > pr_path) sps let generate_conf_subdirs oc sds = if sds <> [] then section oc "Subdirectories. (DEPRECATED)"; - List.iter (fprintf oc ".PHONY:%s\n") sds; - List.iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds; - List.iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds; - List.iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds; - List.iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds + let iter f = List.iter (forget_source > f) in + iter (fprintf oc ".PHONY:%s\n") sds; + iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds; + iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds; + iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds; + iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds let generate_conf_includes oc { ml_includes; r_includes; q_includes } = section oc "Path directives (-I, -R, -Q)."; let module S = String in - let open List in + let map = map_sourced_list in let dash1 opt v = sprintf "-%s %s" opt (quote v) in let dash2 opt v1 v2 = sprintf "-%s %s %s" opt (quote v1) (quote v2) in fprintf oc "COQMF_OCAMLLIBS = %s\n" @@ -202,7 +205,11 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } = (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)); fprintf oc "COQMF_COQLIBS_NOML = %s %s\n" (S.concat " " (map (fun ({ path },l) -> dash2 "Q" path l) q_includes)) - (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)) + (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)); + fprintf oc "COQMF_CMDLINE_COQLIBS = %s %s %s\n" + (S.concat " " (map_cmdline (fun { path } -> dash1 "I" path) ml_includes)) + (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "Q" path l) q_includes)) + (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "R" path l) r_includes)); ;; let windrive s = @@ -219,10 +226,10 @@ let generate_conf_coq_config oc args = ;; let generate_conf_files oc - { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files } + { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files; } = let module S = String in - let open List in + let map = map_sourced_list in section oc "Project files."; fprintf oc "COQMF_VFILES = %s\n" (S.concat " " (map quote v_files)); fprintf oc "COQMF_MLIFILES = %s\n" (S.concat " " (map quote mli_files)); @@ -230,6 +237,8 @@ let generate_conf_files oc fprintf oc "COQMF_ML4FILES = %s\n" (S.concat " " (map quote ml4_files)); fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files)); fprintf oc "COQMF_MLLIBFILES = %s\n" (S.concat " " (map quote mllib_files)); + let cmdline_vfiles = filter_cmdline v_files in + fprintf oc "COQMF_CMDLINE_VFILES = %s\n" (S.concat " " (List.map quote cmdline_vfiles)); ;; let rec all_start_with prefix = function @@ -246,12 +255,12 @@ let rec logic_gcd acc = function else acc let generate_conf_doc oc { defs; q_includes; r_includes } = - let includes = List.map snd (q_includes @ r_includes) in + let includes = List.map (forget_source > snd) (q_includes @ r_includes) in let logpaths = List.map (CString.split '.') includes in let gcd = logic_gcd [] logpaths in let root = if gcd = [] then - if not (List.mem_assoc "INSTALLDEFAULTROOT" defs) then begin + if not (List.exists (fun x -> fst x.thing = "INSTALLDEFAULTROOT") defs) then begin let destination = "orphan_" ^ (String.concat "_" includes) in eprintf "Warning: no common logical root\n"; eprintf "Warning: in such case INSTALLDEFAULTROOT must be defined\n"; @@ -264,9 +273,9 @@ let generate_conf_doc oc { defs; q_includes; r_includes } = let generate_conf_defs oc { defs; extra_args } = section oc "Extra variables."; - List.iter (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v) defs; + List.iter (forget_source > (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v)) defs; Printf.fprintf oc "COQMF_OTHERFLAGS = %s\n" - (String.concat " " extra_args) + (String.concat " " (List.map forget_source extra_args)) let generate_conf oc project args = fprintf oc "# This configuration file was generated by running:\n"; @@ -284,10 +293,10 @@ let ensure_root_dir ({ ml_includes; r_includes; q_includes; v_files; ml_files; mli_files; ml4_files; mllib_files; mlpack_files } as project) -= - let open List in + = + let exists f = List.exists (forget_source > f) in let here = Sys.getcwd () in - let not_tops = List.for_all (fun s -> s <> Filename.basename s) in + let not_tops = List.for_all (fun s -> s.thing <> Filename.basename s.thing) in if exists (fun { canonical_path = x } -> x = here) ml_includes || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes @@ -297,29 +306,27 @@ let ensure_root_dir then project else + let source x = {thing=x; source=CmdLine} in let here_path = { path = "."; canonical_path = here } in { project with - ml_includes = here_path :: ml_includes; - r_includes = (here_path, "Top") :: r_includes } + ml_includes = source here_path :: ml_includes; + r_includes = source (here_path, "Top") :: r_includes } ;; let warn_install_at_root_directory - { q_includes; r_includes; - v_files; ml_files; mli_files; ml4_files; - mllib_files; mlpack_files } + ({ q_includes; r_includes; } as project) = let open CList in let inc_top_p = map_filter - (fun ({ path } ,ldir) -> if ldir = "" then Some path else None) + (fun {thing=({ path } ,ldir)} -> if ldir = "" then Some path else None) (r_includes @ q_includes) in - let files = - v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files in - let bad = filter (fun f -> mem (Filename.dirname f) inc_top_p) files in + let files = all_files project in + let bad = filter (fun f -> mem (Filename.dirname f.thing) inc_top_p) files in if bad <> [] then begin eprintf "Warning: No file should be installed at the root of Coq's library.\n"; eprintf "Warning: No logical path (-R, -Q) applies to these files:\n"; - List.iter (fun x -> eprintf "Warning: %s\n" x) bad; + List.iter (fun x -> eprintf "Warning: %s\n" x.thing) bad; eprintf "\n"; end ;; @@ -328,10 +335,10 @@ let check_overlapping_include { q_includes; r_includes } = let pwd = Sys.getcwd () in let aux = function | [] -> () - | ({ path; canonical_path }, _) :: l -> + | {thing = { path; canonical_path }, _} :: l -> if not (is_prefix pwd canonical_path) then eprintf "Warning: %s (used in -R or -Q) is not a subdirectory of the current directory\n\n" path; - List.iter (fun ({ path = p; canonical_path = cp }, _) -> + List.iter (fun {thing={ path = p; canonical_path = cp }, _} -> if is_prefix canonical_path cp || is_prefix cp canonical_path then eprintf "Warning: %s and %s overlap (used in -R or -Q)\n\n" path p) l @@ -354,7 +361,7 @@ let destination_of { ml_includes; q_includes; r_includes; } file = clean_path (physical_dir_of_logical_dir logic ^ "/" ^ chop_prefix canonical_path file_dir ^ "/") in let candidates = - CList.map_filter (fun ({ canonical_path }, logic) -> + CList.map_filter (fun {thing={ canonical_path }, logic} -> if is_prefix canonical_path file_dir then Some(mk_destination logic canonical_path) else None) includes @@ -364,10 +371,10 @@ let destination_of { ml_includes; q_includes; r_includes; } file = (* BACKWARD COMPATIBILITY: -I into the only logical root *) begin match r_includes, - List.find (fun { canonical_path = p } -> is_prefix p file_dir) + List.find (fun {thing={ canonical_path = p }} -> is_prefix p file_dir) ml_includes with - | [{ canonical_path }, logic], { canonical_path = p } -> + | [{thing={ canonical_path }, logic}], {thing={ canonical_path = p }} -> let destination = clean_path (physical_dir_of_logical_dir logic ^ "/" ^ chop_prefix p file_dir ^ "/") in diff --git a/tools/coqc.ml b/tools/coqc.ml index 3181ef910..90d8e67c1 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -111,7 +111,7 @@ let parse_args () = |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w" - |"-o"|"-profile-ltac-cutoff" + |"-o"|"-profile-ltac-cutoff"|"-mangle-names" as o) :: rem -> begin match rem with diff --git a/tools/coqdep.ml b/tools/coqdep.ml index f4f143b3b..12b5cab0a 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -446,6 +446,7 @@ let usage () = eprintf " -boot : For coq developers, prints dependencies over coq library files (omitted by default).\n"; eprintf " -sort : output the given file name ordered by dependencies\n"; eprintf " -noglob | -no-glob : \n"; + eprintf " -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE."; eprintf " -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n"; eprintf " -I dir : add (non recursively) dir to ocaml path\n"; eprintf " -R dir -as logname : add and import dir recursively to coq load path under logical name logname\n"; (* deprecate? *) @@ -462,6 +463,19 @@ let usage () = let split_period = Str.split (Str.regexp (Str.quote ".")) +let add_q_include path l = add_rec_dir_no_import add_known path (split_period l) + +let add_r_include path l = add_rec_dir_import add_known path (split_period l) + +let treat_coqproject f = + let open CoqProject_file in + let iter_sourced f = List.iter (fun {thing} -> f thing) in + let project = read_project_file f in + iter_sourced (fun { path } -> add_caml_dir path) project.ml_includes; + iter_sourced (fun ({ path }, l) -> add_q_include path l) project.q_includes; + iter_sourced (fun ({ path }, l) -> add_r_include path l) project.r_includes; + iter_sourced (fun f -> treat_file None f) (all_files project) + let rec parse = function | "-c" :: ll -> option_c := true; parse ll | "-D" :: ll -> option_D := true; parse ll @@ -469,10 +483,11 @@ let rec parse = function | "-boot" :: ll -> option_boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll + | "-f" :: f :: ll -> treat_coqproject f; parse ll | "-I" :: r :: ll -> add_caml_dir r; parse ll | "-I" :: [] -> usage () - | "-R" :: r :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll - | "-Q" :: r :: ln :: ll -> add_rec_dir_no_import add_known r (split_period ln); parse ll + | "-R" :: r :: ln :: ll -> add_r_include r ln; parse ll + | "-Q" :: r :: ln :: ll -> add_q_include r ln; parse ll | "-R" :: ([] | [_]) -> usage () | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 06b2ba41b..a1a07fce8 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -271,6 +271,11 @@ let get_cache opt = function | "force" -> Some Stm.AsyncOpts.Force | _ -> prerr_endline ("Error: force expected after "^opt); exit 1 +let get_identifier opt s = + try Names.Id.of_string s + with CErrors.UserError _ -> + prerr_endline ("Error: valid identifier expected after option "^opt); exit 1 + let is_not_dash_option = function | Some f when String.length f > 0 && f.[0] <> '-' -> true | _ -> false @@ -466,6 +471,9 @@ let parse_args arglist : coq_cmdopts * string list = |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular oval true (next ()) + |"-mangle-names" -> + Namegen.set_mangle_names_mode (get_identifier opt (next ())); oval + |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 07553a2ab..504ffa521 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -79,6 +79,7 @@ let print_usage_channel co command = \n -impredicative-set set sort Set impredicative\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ +\n -mangle-names x mangle auto-generated names using prefix x\ \n -time display the time taken by each command\ \n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 9b7b88b51..2879feba7 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -323,7 +323,7 @@ let build_beq_scheme mode kn = raise NoDecidabilityCoInductive; let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in create_input fix), - Evd.make_evar_universe_context (Global.env ()) None), + UState.make (Global.universes ())), !eff let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme @@ -671,7 +671,7 @@ let make_bl_scheme mode mind = let lnonparrec,lnamesparrec = (* TODO subst *) context_chop (nparams-nparrec) mib.mind_params_ctxt in let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in - let ctx = Evd.make_evar_universe_context (Global.env ()) None in + let ctx = UState.make (Global.universes ()) in let side_eff = side_effect_of_mode mode in let bl_goal = EConstr.of_constr bl_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal @@ -795,7 +795,7 @@ let make_lb_scheme mode mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in - let ctx = Evd.make_evar_universe_context (Global.env ()) None in + let ctx = UState.make (Global.universes ()) in let side_eff = side_effect_of_mode mode in let lb_goal = EConstr.of_constr lb_goal in let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal @@ -965,7 +965,7 @@ let make_eq_decidability mode mind = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let u = Univ.Instance.empty in - let ctx = Evd.make_evar_universe_context (Global.env ()) None in + let ctx = UState.make (Global.universes ()) in let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let side_eff = side_effect_of_mode mode in diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 1712634da..6a590758f 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -160,7 +160,7 @@ let do_assumptions kind nl l = in let sigma = solve_remaining_evars all_and_fail_flags env sigma Evd.empty in (* The universe constraints come from the whole telescope. *) - let sigma = Evd.nf_constraints sigma in + let sigma = Evd.minimize_universes sigma in let nf_evar c = EConstr.to_constr sigma c in let uvars, l = List.fold_left_map (fun uvars (coe,t,imps) -> let t = nf_evar t in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 01dbe0a0d..b18a60a1f 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -85,7 +85,7 @@ let interp_definition pl bl poly red_option c ctypopt = evd, c, imps1@Impargs.lift_implicits (Context.Rel.nhyps ctx) impsty, Some ty in (* universe minimization *) - let evd = Evd.nf_constraints evd in + let evd = Evd.minimize_universes evd in (* Substitute evars and universes, and add parameters. Note: in program mode some evars may remain. *) let ctx = List.map (EConstr.to_rel_decl evd) ctx in diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 41c44b126..27587416b 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -381,7 +381,7 @@ let do_mutual_induction_scheme lnamedepindsort = | None -> let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in let u, ctx = Universes.fresh_instance_from ctx None in - let evd = Evd.from_ctx (Evd.evar_universe_context_of ctx) in + let evd = Evd.from_ctx (UState.of_context_set ctx) in evd, (ind,u), Some u | Some ui -> evd, (ind, ui), inst in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 6447fc350..4f16e1cf6 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -472,7 +472,7 @@ let subst_body expand prg = let declare_definition prg = let body, typ = subst_body true prg in let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) - (Evd.evar_universe_context_subst prg.prg_ctx) in + (UState.subst prg.prg_ctx) in let opaque = prg.prg_opaque in let fix_exn = Hook.get get_fix_exn () in let typ = nf typ in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0ff6d9c17..4c9b41b21 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -66,13 +66,13 @@ let show_proof () = let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) let pfts = Proof_global.give_me_the_proof () in - let gls,_,_,_,sigma = Proof.proof pfts in - pr_evars_int sigma 1 (Evd.undefined_map sigma) + let gls,_,shelf,givenup,sigma = Proof.proof pfts in + pr_evars_int sigma ~shelf ~givenup 1 (Evd.undefined_map sigma) let show_universes () = let pfts = Proof_global.give_me_the_proof () in let gls,_,_,_,sigma = Proof.proof pfts in - let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in + let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx @@ -805,7 +805,14 @@ let vernac_end_segment ({v=id} as lid) = (* Libraries *) +let warn_require_in_section = + let name = "require-in-section" in + let category = "deprecated" in + CWarnings.create ~name ~category + (fun () -> strbrk "Use of “Require” inside a section is deprecated.") + let vernac_require from import qidl = + if Lib.sections_are_opened () then warn_require_in_section (); let qidl = List.map qualid_of_reference qidl in let root = match from with | None -> None |