diff options
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | Makefile | 28 | ||||
| -rw-r--r-- | Makefile.build | 14 | ||||
| -rw-r--r-- | Makefile.ide | 12 | ||||
| -rwxr-xr-x | dev/tools/change-header | 2 | ||||
| -rw-r--r-- | engine/termops.ml | 2 | ||||
| -rw-r--r-- | engine/termops.mli | 2 | ||||
| -rw-r--r-- | ide/coqide_QUARTZ.ml.in | 37 | ||||
| -rw-r--r-- | ide/coqide_WIN32.ml.in | 50 | ||||
| -rw-r--r-- | ide/coqide_X11.ml.in | 11 | ||||
| -rw-r--r-- | ide/coqide_main.ml (renamed from ide/coqide_main.ml4) | 84 | ||||
| -rw-r--r-- | ide/coqide_os_specific.mli | 11 | ||||
| -rw-r--r-- | ide/dune | 6 | ||||
| -rw-r--r-- | kernel/environ.ml | 26 | ||||
| -rw-r--r-- | kernel/environ.mli | 8 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 6 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 3 | ||||
| -rw-r--r-- | library/global.ml | 46 | ||||
| -rw-r--r-- | library/global.mli | 4 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 8 | ||||
| -rw-r--r-- | proofs/logic.ml | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
24 files changed, 200 insertions, 172 deletions
diff --git a/.gitignore b/.gitignore index 709e87cc9c..f9e43a0eb7 100644 --- a/.gitignore +++ b/.gitignore @@ -139,7 +139,7 @@ plugins/ltac/coretactics.ml plugins/ltac/extratactics.ml plugins/ltac/extraargs.ml plugins/ltac/profile_ltac_tactics.ml -ide/coqide_main.ml +ide/coqide_os_specific.ml plugins/ssrmatching/ssrmatching.ml plugins/ssr/ssrparser.ml plugins/ssr/ssrvernac.ml @@ -78,7 +78,6 @@ LEXFILES := $(call find, '*.mll') YACCFILES := $(call find, '*.mly') export MLLIBFILES := $(call find, '*.mllib') export MLPACKFILES := $(call find, '*.mlpack') -export ML4FILES := $(call find, '*.ml4') export MLGFILES := $(call find, '*.mlg') export CFILES := $(call findindir, 'kernel/byterun', '*.c') @@ -94,19 +93,14 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated -GENML4FILES:= $(ML4FILES:.ml4=.ml) GENMLGFILES:= $(MLGFILES:.mlg=.ml) -export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) kernel/copcodes.ml +export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) -# NB: all files in $(GENFILES) can be created initially, while -# .ml files in $(GENML4FILES) might need some intermediate building. -# That's why we keep $(GENML4FILES) out of $(GENFILES) - ## More complex file lists -export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES) $(GENMLGFILES), $(EXISTINGML)) +export MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML)) export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) include Makefile.common @@ -194,7 +188,7 @@ META.coq: META.coq.in # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean alienclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean clean: objclean cruftclean depclean docclean camldevfilesclean @@ -202,7 +196,7 @@ cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean objclean: archclean indepclean -cruftclean: ml4clean +cruftclean: mlgclean find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} + rm -f gmon.out core @@ -252,8 +246,8 @@ clean-ide: rm -f ide/utf8_convert.ml rm -rf $(COQIDEAPP) -ml4clean: - rm -f $(GENML4FILES) $(GENMLGFILES) +mlgclean: + rm -f $(GENMLGFILES) depclean: find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} + @@ -286,7 +280,7 @@ KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa') -KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \ +KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(MLPACKFILES:.mlpack=.ml) \ $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ $(MLIFILES:.mli=.cmi) \ @@ -308,7 +302,7 @@ include Makefile.ci .PHONY: tags printenv tags: - echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \ + echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ etags --language=none\ "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ @@ -317,12 +311,12 @@ tags: "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ "--regex=/module[ \t]+\([^ \t]+\)/\1/" - echo $(ML4FILES) | sort -r | xargs \ + echo $(MLGFILES) | sort -r | xargs \ etags --append --language=none\ "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" checker-tags: - echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \ + echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ etags --language=none\ "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ @@ -331,7 +325,7 @@ checker-tags: "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ "--regex=/module[ \t]+\([^ \t]+\)/\1/" - echo $(ML4FILES) | sort -r | xargs \ + echo $(MLGFILES) | sort -r | xargs \ etags --append --language=none\ "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" diff --git a/Makefile.build b/Makefile.build index 08863014ea..fb84a131c7 100644 --- a/Makefile.build +++ b/Makefile.build @@ -86,7 +86,7 @@ byte: coqbyte coqide-byte pluginsbyte printers # This list of ml files used to be in the main Makefile, we moved it here # to avoid exhausting the variable env in Win32 -MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml) +MLFILES := $(MLSTATICFILES) $(GENMLFILES) include Makefile.common include Makefile.vofiles @@ -148,7 +148,7 @@ endif # This include below will lauch the build of all .d. # The - at front is for disabling warnings about currently missing ones. # For creating the missing .d, make will recursively build things like -# coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d). +# coqdep_boot (for the .v.d files) or coqpp (for .mlg -> .ml -> .ml.d). VDFILE := .vfiles MLDFILE := .mlfiles @@ -166,7 +166,7 @@ DEPENDENCIES := \ # of include, and they will then be automatically deleted, leading to an # infinite loop. -.SECONDARY: $(DEPENDENCIES) $(GENFILES) $(ML4FILES:.ml4=.ml) +.SECONDARY: $(DEPENDENCIES) $(GENFILES) $(MLGFILES:.mlg=.ml) ########################################################################### # Compilation options @@ -259,6 +259,7 @@ CAMLP5DEPS:=grammar/grammar.cma CAMLP5USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) +# XXX unused but should be used for mlp files # Main packages linked by Coq. SYSMOD:=-package num,str,unix,dynlink,threads @@ -768,11 +769,6 @@ kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50 $(SHOW)'OCAMLYACC $<' $(HIDE)$(OCAMLYACC) --strict "$*.mly" -%.ml: %.ml4 $(CAMLP5DEPS) $(COQPP) - $(SHOW)'CAMLP5O $<' - $(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) \ - $(CAMLP5DEPS) $(CAMLP5USE) $(CAMLP5COMPAT) -impl $< -o $@ - %.ml: %.mlg $(COQPP) $(SHOW)'COQPP $<' $(HIDE)$(COQPP) $< @@ -782,7 +778,7 @@ kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50 ########################################################################### # Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12) -OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack +OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .mlpack MAINMLFILES := $(filter-out checker/% plugins/%, $(MLFILES) $(MLIFILES)) MAINMLLIBFILES := $(filter-out checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES)) diff --git a/Makefile.ide b/Makefile.ide index 6c069a1e50..39af1f8545 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -49,8 +49,8 @@ IDETOPEXE=bin/coqidetop$(EXE) IDETOP=bin/coqidetop.opt$(EXE) IDETOPBYTE=bin/coqidetop.byte$(EXE) -LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.mli ide/coqide_main.ml -LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.mli ide/coqide_main.ml +LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_os_specific.cmo ide/coqide_main.mli ide/coqide_main.ml +LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_os_specific.cmx ide/coqide_main.mli ide/coqide_main.ml IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map @@ -110,10 +110,10 @@ $(COQIDEBYTE): $(LINKIDE) $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ \ -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS) $(IDECDEPSFLAGS) $^ -ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp5deps here - $(SHOW)'CAMLP5O $<' - $(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) $(CAMLP5USE) -D$(IDEINT) -impl $< -o $@ - +ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile + @rm -f $@ + cp $< $@ + @chmod -w $@ ide/%.cmi: ide/%.mli $(SHOW)'OCAMLC $<' diff --git a/dev/tools/change-header b/dev/tools/change-header index 61cc866602..687c02f4f1 100755 --- a/dev/tools/change-header +++ b/dev/tools/change-header @@ -22,7 +22,7 @@ lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)' modified=0 kept=0 -for i in `find . -name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do +for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do headline=`head -n 1 $i` if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then # Has emacs header diff --git a/engine/termops.ml b/engine/termops.ml index 181efa0ade..52880846f8 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1179,7 +1179,7 @@ let isGlobalRef sigma c = | Const _ | Ind _ | Construct _ | Var _ -> true | _ -> false -let is_template_polymorphic env sigma f = +let is_template_polymorphic_ind env sigma f = match EConstr.kind sigma f with | Ind (ind, u) -> if not (EConstr.EInstance.is_empty u) then false diff --git a/engine/termops.mli b/engine/termops.mli index 1054fbbc5e..07c9541f25 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -282,7 +282,7 @@ val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool val isGlobalRef : Evd.evar_map -> constr -> bool -val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool +val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool val is_Prop : Evd.evar_map -> constr -> bool val is_Set : Evd.evar_map -> constr -> bool diff --git a/ide/coqide_QUARTZ.ml.in b/ide/coqide_QUARTZ.ml.in new file mode 100644 index 0000000000..a08bac5772 --- /dev/null +++ b/ide/coqide_QUARTZ.ml.in @@ -0,0 +1,37 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +let osx = GosxApplication.osxapplication () + +let () = + let _ = osx#connect#ns_application_open_file + ~callback:(fun x -> Coqide.do_load x; true) + in + let _ = osx#connect#ns_application_block_termination + ~callback:Coqide.forbid_quit + in + let _ = osx#connect#ns_application_will_terminate + ~callback:Coqide.close_and_quit + in () + +let init () = + let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication + (GtkMenu.MenuShell.cast + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget) + in + let () = GtkosxApplication.Application.insert_app_menu_item + osx#as_osxapplication + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1 + in + let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication + (Some (GtkMenu.MenuItem.cast + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget)) + in + osx#ready () diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in new file mode 100644 index 0000000000..8c4649fc39 --- /dev/null +++ b/ide/coqide_WIN32.ml.in @@ -0,0 +1,50 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(* On win32, we add the directory of coqide to the PATH at launch-time + (this used to be done in a .bat script). *) + +let set_win32_path () = + Unix.putenv "PATH" + (Filename.dirname Sys.executable_name ^ ";" ^ + (try Sys.getenv "PATH" with _ -> "")) + +(* On win32, since coqide is now console-free, we re-route stdout/stderr + to avoid Sys_error if someone writes to them. We write to a pipe which + is never read (by default) or to a temp log file (when in debug mode). +*) + +let reroute_stdout_stderr () = + (* We anticipate a bit the argument parsing and look for -debug *) + let debug = List.mem "-debug" (Array.to_list Sys.argv) in + Minilib.debug := debug; + let out_descr = + if debug then + let (name,chan) = Filename.open_temp_file "coqide_" ".log" in + Coqide.logfile := Some name; + Unix.descr_of_out_channel chan + else + snd (Unix.pipe ()) + in + Unix.set_close_on_exec out_descr; + Unix.dup2 out_descr Unix.stdout; + Unix.dup2 out_descr Unix.stderr + +(* We also provide specific kill and interrupt functions. *) + +external win32_kill : int -> unit = "win32_kill" +external win32_interrupt : int -> unit = "win32_interrupt" +let () = + Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; + set_win32_path (); + Coq.interrupter := win32_interrupt; + reroute_stdout_stderr () + +let init () = () diff --git a/ide/coqide_X11.ml.in b/ide/coqide_X11.ml.in new file mode 100644 index 0000000000..6a5784eac3 --- /dev/null +++ b/ide/coqide_X11.ml.in @@ -0,0 +1,11 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +let init () = () diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml index 3a92e1bc91..91e8be875a 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml @@ -49,88 +49,6 @@ let catch_gtk_messages () = let () = catch_gtk_messages () - - -(** System-dependent settings *) - -let os_specific_init () = () - -(** Win32 *) - -IFDEF WIN32 THEN - -(* On win32, we add the directory of coqide to the PATH at launch-time - (this used to be done in a .bat script). *) - -let set_win32_path () = - Unix.putenv "PATH" - (Filename.dirname Sys.executable_name ^ ";" ^ - (try Sys.getenv "PATH" with _ -> "")) - -(* On win32, since coqide is now console-free, we re-route stdout/stderr - to avoid Sys_error if someone writes to them. We write to a pipe which - is never read (by default) or to a temp log file (when in debug mode). -*) - -let reroute_stdout_stderr () = - (* We anticipate a bit the argument parsing and look for -debug *) - let debug = List.mem "-debug" (Array.to_list Sys.argv) in - Minilib.debug := debug; - let out_descr = - if debug then - let (name,chan) = Filename.open_temp_file "coqide_" ".log" in - Coqide.logfile := Some name; - Unix.descr_of_out_channel chan - else - snd (Unix.pipe ()) - in - Unix.set_close_on_exec out_descr; - Unix.dup2 out_descr Unix.stdout; - Unix.dup2 out_descr Unix.stderr - -(* We also provide specific kill and interrupt functions. *) - -external win32_kill : int -> unit = "win32_kill" -external win32_interrupt : int -> unit = "win32_interrupt" -let () = - Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; - set_win32_path (); - Coq.interrupter := win32_interrupt; - reroute_stdout_stderr () -END - -(** MacOSX *) - -IFDEF QUARTZ THEN -let osx = GosxApplication.osxapplication () - -let () = - let _ = osx#connect#ns_application_open_file - ~callback:(fun x -> Coqide.do_load x; true) - in - let _ = osx#connect#ns_application_block_termination - ~callback:Coqide.forbid_quit - in - let _ = osx#connect#ns_application_will_terminate - ~callback:Coqide.close_and_quit - in () - -let os_specific_init () = - let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication - (GtkMenu.MenuShell.cast - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget) - in - let () = GtkosxApplication.Application.insert_app_menu_item - osx#as_osxapplication - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1 - in - let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication - (Some (GtkMenu.MenuItem.cast - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget)) - in - osx#ready () -END - let load_prefs () = try Preferences.load_pref () with e -> Ideutils.flash_info @@ -145,7 +63,7 @@ let () = Coq.check_connection args; Coqide.sup_args := args; Coqide.main files; - os_specific_init (); + Coqide_os_specific.init (); try GMain.main (); failwith "Gtk loop ended" diff --git a/ide/coqide_os_specific.mli b/ide/coqide_os_specific.mli new file mode 100644 index 0000000000..ebd09099f0 --- /dev/null +++ b/ide/coqide_os_specific.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +val init : unit -> unit @@ -33,9 +33,9 @@ (libraries coqide-server.protocol coqide-server.core lablgtk2.sourceview2)) (rule - (targets coqide_main.ml) - (deps (:ml4-file coqide_main.ml4)) - (action (run coqmlp5 -loc loc -impl %{ml4-file} -o %{targets}))) + (targets coqide_os_specific.ml) + (deps (:in-file coqide_X11.ml.in)) ; TODO support others + (action (run cp %{in-file} %{targets}))) (executable (name coqide_main) diff --git a/kernel/environ.ml b/kernel/environ.ml index 3b7e3ae544..e341412294 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -440,6 +440,16 @@ let constant_value_and_type env (kn, u) = | Undef _ -> None in b', cb.const_type, Univ.Constraint.empty +let body_of_constant_body env cb = + let otab = opaque_tables env in + match cb.const_body with + | Undef _ -> + None + | Def c -> + Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb) + | OpaqueDef o -> + Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb) + (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) @@ -694,6 +704,22 @@ let is_polymorphic env r = | IndRef ind -> polymorphic_ind ind env | ConstructRef cstr -> polymorphic_ind (inductive_of_constructor cstr) env +let is_template_polymorphic env r = + let open Names.GlobRef in + match r with + | VarRef _id -> false + | ConstRef _c -> false + | IndRef ind -> template_polymorphic_ind ind env + | ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env + +let is_type_in_type env r = + let open Names.GlobRef in + match r with + | VarRef _id -> false + | ConstRef c -> type_in_type_constant c env + | IndRef ind -> type_in_type_ind ind env + | ConstructRef cstr -> type_in_type_ind (inductive_of_constructor cstr) env + (*spiwack: the following functions assemble the pieces of the retroknowledge note that the "consistent" register function is available in the module Safetyping, Environ only synchronizes the proactive and the reactive parts*) diff --git a/kernel/environ.mli b/kernel/environ.mli index 43bfe7c2fb..0255581749 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -211,6 +211,12 @@ val constant_value_and_type : env -> Constant.t puniverses -> polymorphic *) val constant_context : env -> Constant.t -> Univ.AUContext.t +(** Returns the body of the constant if it has any, and the polymorphic context + it lives in. For monomorphic constant, the latter is empty, and for + polymorphic constants, the term contains De Bruijn universe variables that + need to be instantiated. *) +val body_of_constant_body : env -> constant_body -> (Constr.constr * Univ.AUContext.t) option + (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) @@ -320,6 +326,8 @@ val apply_to_hyp : named_context_val -> variable -> val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val val is_polymorphic : env -> Names.GlobRef.t -> bool +val is_template_polymorphic : env -> GlobRef.t -> bool +val is_type_in_type : env -> GlobRef.t -> bool open Retroknowledge (** functions manipulating the retroknowledge diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 12f9592ab7..779e05ee0c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -194,6 +194,10 @@ let set_engagement c senv = let set_typing_flags c senv = { senv with env = Environ.set_typing_flags c senv.env } +let set_share_reduction b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with share_reduction = b } senv + (** Check that the engagement [c] expected by a library matches the current (initial) one *) let check_engagement env expected_impredicative_set = @@ -1190,7 +1194,7 @@ loaded by side-effect once and for all (like it is done in OCaml). Would this be correct with respect to undo's and stuff ? *) -let set_strategy e k l = { e with env = +let set_strategy k l e = { e with env = (Environ.set_oracle e.env (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) } diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 26fa91adbd..443b5cfd73 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -137,6 +137,7 @@ val add_constraints : (** Setting the type theory flavor *) val set_engagement : Declarations.engagement -> safe_transformer0 val set_typing_flags : Declarations.typing_flags -> safe_transformer0 +val set_share_reduction : bool -> safe_transformer0 (** {6 Interactive module functions } *) @@ -217,4 +218,4 @@ val register : val register_inline : Constant.t -> safe_transformer0 val set_strategy : - safe_environment -> Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_environment + Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0 diff --git a/library/global.ml b/library/global.ml index 3781ff3230..bfea6d3dea 100644 --- a/library/global.ml +++ b/library/global.ml @@ -128,19 +128,7 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) let opaque_tables () = Environ.opaque_tables (env ()) -let instantiate cb c = - let open Declarations in - match cb.const_universes with - | Monomorphic_const _ -> c, Univ.AUContext.empty - | Polymorphic_const ctx -> c, ctx - -let body_of_constant_body cb = - let open Declarations in - let otab = opaque_tables () in - match cb.const_body with - | Undef _ -> None - | Def c -> Some (instantiate cb (Mod_subst.force_constr c)) - | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o)) +let body_of_constant_body ce = body_of_constant_body (env ()) ce let body_of_constant cst = body_of_constant_body (lookup_constant cst) @@ -165,8 +153,6 @@ let import c u d = globalize (Safe_typing.import c u d) let env_of_context hyps = reset_with_named_context hyps (env()) -open Globnames - let constr_of_global_in_context = Typeops.constr_of_global_in_context let type_of_global_in_context = Typeops.type_of_global_in_context @@ -175,21 +161,9 @@ let universes_of_global gr = let is_polymorphic r = Environ.is_polymorphic (env()) r -let is_template_polymorphic r = - let env = env() in - match r with - | VarRef id -> false - | ConstRef c -> false - | IndRef ind -> Environ.template_polymorphic_ind ind env - | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env - -let is_type_in_type r = - let env = env() in - match r with - | VarRef id -> false - | ConstRef c -> Environ.type_in_type_constant c env - | IndRef ind -> Environ.type_in_type_ind ind env - | ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env +let is_template_polymorphic r = is_template_polymorphic (env ()) r + +let is_type_in_type r = is_type_in_type (env ()) r let current_modpath () = Safe_typing.current_modpath (safe_env ()) @@ -208,11 +182,7 @@ let register field value = let register_inline c = globalize0 (Safe_typing.register_inline c) let set_strategy k l = - GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l) - -let set_reduction_sharing b = - let env = safe_env () in - let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in - let flags = { flags with Declarations.share_reduction = b } in - let env = Safe_typing.set_typing_flags flags env in - GlobalSafeEnv.set_safe_env env + globalize0 (Safe_typing.set_strategy k l) + +let set_share_reduction b = + globalize0 (Safe_typing.set_share_reduction b) diff --git a/library/global.mli b/library/global.mli index 42a8005a4f..762a3f006d 100644 --- a/library/global.mli +++ b/library/global.mli @@ -150,7 +150,9 @@ val register_inline : Constant.t -> unit val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit -val set_reduction_sharing : bool -> unit +(** {6 Conversion settings } *) + +val set_share_reduction : bool -> unit (* Modifies the global state, registering new universes *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index dd38ec6f64..96213af9c6 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -83,7 +83,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) (** Refresh the types of evars under template polymorphic references *) let rec refresh_term_evars ~onevars ~top t = match EConstr.kind !evdref t with - | App (f, args) when is_template_polymorphic env !evdref f -> + | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f -> let pos = get_polymorphic_positions !evdref f in refresh_polymorphic_positions args pos; t | App (f, args) when top && isEvar !evdref f -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 24767ca4d1..cba1533da5 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -692,7 +692,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma let sigma, resj = match EConstr.kind sigma resj.uj_val with | App (f,args) -> - if is_template_polymorphic !!env sigma f then + if Termops.is_template_polymorphic_ind !!env sigma f then (* Special case for inductive type applications that must be refreshed right away. *) let c = mkApp (f, args) in diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 7e43c5e41d..62ad296ecb 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -130,7 +130,7 @@ let retype ?(polyprop=true) sigma = subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2) | Fix ((_,i),(_,tys,_)) -> tys.(i) | CoFix (i,(_,tys,_)) -> tys.(i) - | App(f,args) when is_template_polymorphic env sigma f -> + | App(f,args) when Termops.is_template_polymorphic_ind env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in strip_outer_cast sigma (subst_type env sigma t (Array.to_list args)) | App(f,args) -> @@ -156,7 +156,7 @@ let retype ?(polyprop=true) sigma = let dom = sort_of env t in let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in Typeops.sort_of_product env dom rang - | App(f,args) when is_template_polymorphic env sigma f -> + | App(f,args) when Termops.is_template_polymorphic_ind env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in sort_of_atomic_type env sigma t args | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args @@ -190,14 +190,14 @@ let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t = let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in if not (is_impredicative_set env) && s2 == InSet && sort_family_of env t == InType then InType else s2 - | App(f,args) when is_template_polymorphic env sigma f -> + | App(f,args) when Termops.is_template_polymorphic_ind env sigma f -> if truncation_style then InType else let t = type_of_global_reference_knowing_parameters env f args in Sorts.family (sort_of_atomic_type env sigma t args) | App(f,args) -> Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> retype_error NotAType - | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType + | Ind _ when truncation_style && Termops.is_template_polymorphic_ind env sigma t -> InType | _ -> Sorts.family (decomp_sort env sigma (type_of env t)) in sort_family_of env t diff --git a/proofs/logic.ml b/proofs/logic.ml index b8612cd2c0..4d5711c195 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -384,7 +384,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env sigma (EConstr.of_constr f) then + if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f) then let ty = (* Template polymorphism of definitions and inductive types *) let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in @@ -447,7 +447,7 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env sigma (EConstr.of_constr f) + if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f) then let l' = meta_free_prefix sigma l in (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1190d73258..5eace14cbf 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1536,7 +1536,7 @@ let _ = optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction); - optwrite = (fun b -> Global.set_reduction_sharing b) } + optwrite = Global.set_share_reduction } let _ = declare_bool_option |