Skip to content
Browse files

Merge with recent trunk and new version of universe polymorphism.

Conflicts:
	kernel/declarations.ml
  • Loading branch information...
2 parents e83990d + 9441842 commit 44d41f23d011b8254156c8c150f6cf11260fb517 @mattam82 mattam82 committed Apr 3, 2013
Showing with 9,242 additions and 3,607 deletions.
  1. +1 −0 .gitignore
  2. +9 −0 CHANGES
  3. +1 −1 Makefile
  4. +8 −20 Makefile.build
  5. +10 −1 Makefile.common
  6. +0 −4 _tags
  7. +32 −31 checker/check.ml
  8. +4 −1 checker/check.mllib
  9. +12 −25 checker/checker.ml
  10. +37 −18 checker/declarations.ml
  11. +8 −1 checker/declarations.mli
  12. +8 −6 checker/environ.ml
  13. +2 −2 checker/environ.mli
  14. +1 −1 checker/include
  15. +8 −8 checker/indtypes.ml
  16. +7 −7 checker/inductive.ml
  17. +10 −5 checker/mod_checking.ml
  18. +7 −7 checker/modops.ml
  19. +3 −3 checker/reduction.ml
  20. +5 −5 checker/safe_typing.ml
  21. +2 −2 checker/subtyping.ml
  22. +38 −26 checker/term.ml
  23. +1 −1 checker/term.mli
  24. +3 −3 checker/typeops.ml
  25. +1 −2 checker/validate.ml
  26. +1 −0 config/coq_config.mli
  27. +13 −2 configure
  28. +5 −3 dev/base_include
  29. +1 −1 dev/db_printers.ml
  30. +9 −0 dev/doc/debugging.txt
  31. +31 −0 dev/doc/patch.ocaml-3.10.drop.rectypes
  32. +4 −2 dev/include
  33. +13 −3 dev/printers.mllib
  34. +20 −17 dev/top_printers.ml
  35. +43 −1 doc/refman/RefMan-ext.tex
  36. +14 −7 doc/refman/RefMan-gal.tex
  37. +16 −0 doc/refman/RefMan-mod.tex
  38. +2 −1 doc/refman/RefMan-pro.tex
  39. +7 −4 doc/refman/RefMan-tac.tex
  40. +5 −4 grammar/argextend.ml4
  41. +4 −1 grammar/grammar.mllib
  42. +3 −2 grammar/q_coqast.ml4
  43. +1 −1 grammar/q_util.ml4
  44. +3 −3 grammar/tacextend.ml4
  45. +2 −2 grammar/vernacextend.ml4
  46. +92 −57 ide/coq.ml
  47. +81 −60 ide/coq.mli
  48. +188 −148 ide/coqOps.ml
  49. +10 −9 ide/coqOps.mli
  50. +46 −39 ide/coqide.ml
  51. +0 −1 ide/coqide_ui.ml
  52. +1 −0 ide/ide.mllib
  53. +14 −9 ide/ideutils.ml
  54. +2 −1 ide/ideutils.mli
  55. +0 −1 ide/mac_default_accel_map
  56. +43 −39 ide/session.ml
  57. +1 −0 ide/tags.ml
  58. +1 −0 ide/tags.mli
  59. +6 −6 ide/wg_Command.ml
  60. +453 −0 ide/wg_Completion.ml
  61. +34 −0 ide/wg_Completion.mli
  62. +41 −14 ide/wg_Find.ml
  63. +9 −2 ide/wg_MessageView.ml
  64. +1 −0 ide/wg_MessageView.mli
  65. +271 −181 ide/wg_ScriptView.ml
  66. +1 −0 ide/wg_ScriptView.mli
  67. +1 −1 interp/constrexpr_ops.ml
  68. +21 −19 interp/constrextern.ml
  69. +6 −3 interp/constrextern.mli
  70. +28 −22 interp/constrintern.ml
  71. +1 −1 interp/constrintern.mli
  72. +35 −31 interp/coqlib.ml
  73. +3 −2 interp/coqlib.mli
  74. +11 −11 interp/dumpglob.ml
  75. +1 −1 interp/dumpglob.mli
  76. +2 −1 interp/genarg.ml
  77. +8 −15 interp/implicit_quantifiers.ml
  78. +9 −6 interp/notation.ml
  79. +1 −1 interp/notation.mli
  80. +6 −3 interp/smartlocate.mli
  81. +1 −1 interp/syntax_def.ml
  82. +1 −1 interp/topconstr.ml
  83. +1 −5 interp/topconstr.mli
  84. +2 −2 intf/constrexpr.mli
  85. +1 −1 intf/decl_kinds.mli
  86. +1 −0 intf/genredexpr.mli
  87. +1 −1 intf/glob_term.mli
  88. +1 −0 intf/misctypes.mli
  89. +1 −1 intf/tacexpr.mli
  90. +45 −17 intf/vernacexpr.mli
  91. +4 −4 kernel/cbytegen.ml
  92. +3 −4 kernel/cemitcodes.ml
  93. +2 −2 kernel/closure.ml
  94. +20 −13 kernel/cooking.ml
  95. +8 −5 kernel/cooking.mli
  96. +6 −1 kernel/csymtable.ml
  97. +0 −396 kernel/declarations.ml
  98. +31 −79 kernel/declarations.mli
  99. +187 −0 kernel/declareops.ml
  100. +56 −0 kernel/declareops.mli
  101. +7 −9 kernel/entries.mli
  102. +25 −17 kernel/environ.ml
  103. +6 −0 kernel/environ.mli
  104. +26 −23 kernel/indtypes.ml
  105. +32 −24 kernel/inductive.ml
  106. +4 −2 kernel/inductive.mli
  107. +8 −1 kernel/kernel.mllib
  108. +43 −0 kernel/lazyconstr.ml
  109. +34 −0 kernel/lazyconstr.mli
  110. +85 −90 kernel/mod_subst.ml
  111. +14 −5 kernel/mod_subst.mli
  112. +31 −30 kernel/mod_typing.ml
  113. +19 −18 kernel/modops.ml
  114. +2 −1 kernel/modops.mli
  115. +349 −262 kernel/names.ml
  116. +351 −107 kernel/names.mli
  117. +1,509 −0 kernel/nativecode.ml
  118. +66 −0 kernel/nativecode.mli
  119. +155 −0 kernel/nativeconv.ml
  120. +15 −0 kernel/nativeconv.mli
  121. +688 −0 kernel/nativelambda.ml
  122. +56 −0 kernel/nativelambda.mli
  123. +97 −0 kernel/nativelib.ml
  124. +34 −0 kernel/nativelib.mli
  125. +63 −0 kernel/nativelibrary.ml
  126. +20 −0 kernel/nativelibrary.mli
  127. +260 −0 kernel/nativevalues.ml
  128. +102 −0 kernel/nativevalues.mli
  129. +1 −1 kernel/pre_env.ml
  130. +74 −23 kernel/reduction.ml
  131. +15 −1 kernel/reduction.mli
  132. +74 −64 kernel/safe_typing.ml
  133. +16 −7 kernel/safe_typing.mli
  134. +48 −46 kernel/subtyping.ml
  135. +135 −65 kernel/term.ml
  136. +22 −4 kernel/term.mli
  137. +20 −51 kernel/term_typing.ml
  138. +9 −10 kernel/term_typing.mli
  139. +3 −3 kernel/type_errors.ml
  140. +2 −2 kernel/type_errors.mli
  141. +44 −54 kernel/typeops.ml
  142. +1,138 −458 kernel/univ.ml
  143. +202 −98 kernel/univ.mli
  144. +3 −3 kernel/vconv.ml
  145. +4 −4 kernel/vm.ml
  146. +98 −0 lib/backtrace.ml
  147. +89 −0 lib/backtrace.mli
  148. +2 −0 lib/bigint.mli
  149. +31 −16 lib/cArray.ml
  150. +3 −0 lib/cArray.mli
  151. +18 −51 lib/cList.ml
  152. +3 −3 lib/cList.mli
  153. +4 −1 lib/clib.mllib
  154. +1 −1 lib/dyn.ml
  155. +18 −21 lib/envars.ml
  156. +55 −21 lib/errors.ml
  157. +22 −13 lib/errors.mli
  158. +102 −0 lib/exninfo.ml
  159. +30 −0 lib/exninfo.mli
  160. +14 −2 lib/flags.ml
  161. +6 −0 lib/flags.mli
  162. +0 −1 lib/lib.mllib
  163. +12 −4 lib/loc.ml
  164. +11 −5 lib/loc.mli
  165. +4 −2 lib/pp.ml
  166. +15 −15 lib/profile.ml
  167. +3 −3 lib/serialize.ml
  168. +35 −23 lib/store.ml
  169. +32 −11 lib/store.mli
  170. +20 −15 lib/system.ml
  171. +3 −3 lib/system.mli
  172. +5 −3 lib/xml_parser.ml
  173. +10 −11 library/assumptions.ml
  174. +57 −33 library/declare.ml
  175. +3 −3 library/declare.mli
  176. +70 −88 library/declaremods.ml
  177. +7 −29 library/declaremods.mli
  178. +2 −2 library/decls.ml
  179. +3 −3 library/decls.mli
  180. +9 −9 library/global.ml
  181. +9 −6 library/global.mli
  182. +34 −30 library/globnames.ml
  183. +7 −4 library/globnames.mli
  184. +6 −6 library/goptions.ml
  185. +4 −4 library/heads.ml
  186. +10 −10 library/impargs.ml
  187. +41 −15 library/kindops.ml
  188. +36 −56 library/lib.ml
  189. +14 −14 library/lib.mli
  190. +31 −31 library/libnames.ml
  191. +25 −25 library/libnames.mli
  192. +8 −8 library/libobject.ml
  193. +76 −54 library/library.ml
  194. +16 −16 library/library.mli
  195. +2 −2 library/nameops.ml
Sorry, we could not display the entire diff because too many files (473) changed.
View
1 .gitignore
@@ -36,6 +36,7 @@
*.v.ps
*.v.html
*.stamp
+*.native
revision
TAGS
.DS_Store
View
9 CHANGES
@@ -8,12 +8,15 @@ Vernacular commands
A flag "Set/Unset Record Elimination Schemes" allows to change this.
The tactic "induction" on a record is now actually doing "destruct".
- The "Open Scope" command can now be given also a delimiter (e.g. Z).
+- The "Definition" command now allows the "Local" modifier.
+- The "Let" command can now define local (co)fixpoints.
Specification Language
- The syntax "x -> y" is now declared at level 99. In particular, it has
now a lower priority than "<->": "A -> B <-> C" is now "A -> (B <-> C)"
(possible source of incompatibilities)
+- Slight changes in unification error messages.
Tactics
@@ -27,6 +30,12 @@ Tactics
- Similarly, "intuition" has been made more uniform and, where it now
fails, "dintuition" can be used. (possible source of incompatibilities)
- Tactic notations can now be defined locally to a module (use "Local" prefix).
+- Tactic "red" now reduces head beta-iota redexes (potential source of
+ rare incompatibilities).
+- Tactic "hnf" now reduces inner beta-iota redexes
+ (potential source of rare incompatibilities).
+- Tactic "intro H" now reduces beta-iota redexes if these hide a product
+ (potential source of rare incompatibilities).
Program
View
2 Makefile
@@ -222,7 +222,7 @@ cleanconfig:
distclean: clean cleanconfig
voclean:
- find theories plugins test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f
+ find theories plugins test-suite -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" | xargs rm -f
devdocclean:
find . -name '*.dep.ps' -o -name '*.dot' | xargs rm -f
View
28 Makefile.build
@@ -125,7 +125,7 @@ endif
PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4
-SYSMOD:=str unix
+SYSMOD:=str unix dynlink
SYSCMA:=$(addsuffix .cma,$(SYSMOD))
SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD))
@@ -370,7 +370,8 @@ install-ide-info:
.PHONY: validate check test-suite $(ALLSTDLIB).v
-VALIDOPTS=-silent -o -m
+
+VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m
validate:: $(CHICKEN) $(ALLVO)
$(SHOW)'COQCHK <theories & plugins>'
@@ -675,12 +676,12 @@ install-latex:
source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
$(OCAMLDOCDIR)/coq.tex:: $(DOCMLIS:.mli=.cmi)
- $(OCAMLDOC) -latex -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+ $(OCAMLDOC) -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
$(DOCMLIS) -t "Coq mlis documentation" \
-intro $(OCAMLDOCDIR)/docintro -o $@
mli-doc:: $(DOCMLIS:.mli=.cmi)
- $(OCAMLDOC) -html -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+ $(OCAMLDOC) -html -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
-css-style style.css
@@ -693,9 +694,9 @@ ml-dot:: $(MLEXTRAFILES)
$(DOT) -Tpng $< -o $@
%_types.dot: %.mli
- $(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<
+ $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $<
-OCAMLDOC_MLLIBD = $(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
+OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
$(foreach lib,$(|:.mllib.d=_MLLIB_DEPENDENCIES),$(addsuffix .ml,$($(lib))))
%.dot: | %.mllib.d
@@ -714,7 +715,7 @@ tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d
$(OCAMLDOC_MLLIBD)
%.dot: %.mli
- $(OCAMLDOC) $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $<
+ $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $<
$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
(cd $(OCAMLDOCDIR) ; pdflatex $*.tex && pdflatex $*.tex)
@@ -746,19 +747,6 @@ ide/coqide_main_opt.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here
$(SHOW)'CAMLP4O $<'
$(HIDE)$(CAMLP4O) $(PR_O) $(CAMLP4USE) -D$(IDEOPTINT) -impl $< -o $@
-# Specific rule for term.ml which uses -rectypes
-# Since term.mli doesn't need -rectypes, this doesn't impact the other ml files
-
-TERM:=kernel/term
-
-$(TERM).cmo: $(TERM).ml | $(TERM).ml.d
- $(SHOW)'OCAMLC -rectypes $<'
- $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -rectypes -c $<
-
-$(TERM).cmx: $(TERM).ml | $(TERM).ml.d
- $(SHOW)'OCAMLOPT -rectypes $<'
- $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -intf-suffix .cmi -rectypes -c $<
-
# pretty printing of the revision number when compiling a checked out
# source tree
.PHONY: revision
View
11 Makefile.common
@@ -323,9 +323,18 @@ ALLSTDLIB := test-suite/misc/universes/all_stdlib
# remove .vo, replace theories and plugins by Coq, and replace slashes by dots
vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$(1:.vo=))))
+# Converting a stdlib filename into native compiler filenames
+# Used for install targets
+vo_to_cm = $(foreach vo,$(1),$(dir $(vo))$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*)))))
+
+vo_to_obj = $(foreach vo,$(1),$(dir $(vo))$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o)))))
+
ALLMODS:=$(call vo_to_mod,$(ALLVO))
-LIBFILES:=$(THEORIESVO) $(PLUGINSVO)
+LIBFILES:=$(THEORIESVO) $(PLUGINSVO) $(call vo_to_cm,$(THEORIESVO)) \
+ $(call vo_to_cm,$(PLUGINSVO)) $(call vo_to_obj,$(THEORIESVO)) \
+ $(call vo_to_obj,$(PLUGINSVO))
+
LIBFILESLIGHT:=$(THEORIESLIGHTVO)
###########################################################################
View
4 _tags
@@ -22,10 +22,6 @@
<grammar/grammar.{cma,cmxa}> : use_unix
-## tags for ml files
-
-"kernel/term.ml": rectypes
-
## tags for camlp4 files
"toplevel/whelp.ml4": use_grammar
View
63 checker/check.ml
@@ -11,19 +11,19 @@ open Errors
open Util
open Names
-let pr_dirpath dp = str (Dir_path.to_string dp)
-let default_root_prefix = Dir_path.make []
+let pr_dirpath dp = str (DirPath.to_string dp)
+let default_root_prefix = DirPath.empty
let split_dirpath d =
- let l = Dir_path.repr d in (Dir_path.make (List.tl l), List.hd l)
-let extend_dirpath p id = Dir_path.make (id :: Dir_path.repr p)
+ let l = DirPath.repr d in (DirPath.make (List.tl l), List.hd l)
+let extend_dirpath p id = DirPath.make (id :: DirPath.repr p)
type section_path = {
dirpath : string list ;
basename : string }
let dir_of_path p =
- Dir_path.make (List.map Id.of_string p.dirpath)
+ DirPath.make (List.map Id.of_string p.dirpath)
let path_of_dirpath dir =
- match Dir_path.repr dir with
+ match DirPath.repr dir with
[] -> failwith "path_of_dirpath"
| l::dir ->
{dirpath=List.map Id.to_string dir;basename=Id.to_string l}
@@ -36,7 +36,7 @@ let pr_path sp =
type library_objects
-type compilation_unit_name = Dir_path.t
+type compilation_unit_name = DirPath.t
type library_disk = {
md_name : compilation_unit_name;
@@ -61,10 +61,10 @@ type library_t = {
module LibraryOrdered =
struct
- type t = Dir_path.t
+ type t = DirPath.t
let compare d1 d2 =
Pervasives.compare
- (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2))
+ (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2))
end
module LibrarySet = Set.Make(LibraryOrdered)
@@ -81,7 +81,7 @@ let find_library dir =
let try_find_library dir =
try find_library dir
with Not_found ->
- error ("Unknown library " ^ (Dir_path.to_string dir))
+ error ("Unknown library " ^ (DirPath.to_string dir))
let library_full_filename dir = (find_library dir).library_filename
@@ -113,7 +113,7 @@ let check_one_lib admit (dir,m) =
(*************************************************************************)
(*s Load path. Mapping from physical to logical paths etc.*)
-type logical_path = Dir_path.t
+type logical_path = DirPath.t
let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list)
@@ -153,7 +153,7 @@ let find_logical_path phys_dir =
match List.filter2 (fun p d -> p = phys_dir) physical logical with
| _,[dir] -> dir
| _,[] -> default_root_prefix
- | _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
+ | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir))
let remove_load_path dir =
let physical, logical = !load_paths in
@@ -185,7 +185,7 @@ let add_load_path (phys_path,coq_path) =
end
| _,[] ->
load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
- | _ -> anomaly ("Two logical paths are associated to "^phys_path)
+ | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path))
let load_paths_of_dir_path dir =
let physical, logical = !load_paths in
@@ -234,36 +234,37 @@ let locate_qualified_library qid =
(dir, file)
with Not_found -> raise LibNotFound
-let explain_locate_library_error qid = function
- | LibUnmappedDir ->
- let prefix = qid.dirpath in
- errorlabstrm "load_absolute_library_from"
- (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++
- str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ())
- | LibNotFound ->
- errorlabstrm "load_absolute_library_from"
- (str"Cannot find library " ++ pr_path qid ++ str" in loadpath")
- | e -> raise e
+let error_unmapped_dir qid =
+ let prefix = qid.dirpath in
+ errorlabstrm "load_absolute_library_from"
+ (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++
+ str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ())
+
+let error_lib_not_found qid =
+ errorlabstrm "load_absolute_library_from"
+ (str"Cannot find library " ++ pr_path qid ++ str" in loadpath")
let try_locate_absolute_library dir =
try
locate_absolute_library dir
- with e ->
- explain_locate_library_error (path_of_dirpath dir) e
+ with
+ | LibUnmappedDir -> error_unmapped_dir (path_of_dirpath dir)
+ | LibNotFound -> error_lib_not_found (path_of_dirpath dir)
let try_locate_qualified_library qid =
try
locate_qualified_library qid
- with e ->
- explain_locate_library_error qid e
+ with
+ | LibUnmappedDir -> error_unmapped_dir qid
+ | LibNotFound -> error_lib_not_found qid
(************************************************************************)
(*s Low-level interning/externing of libraries to files *)
(*s Loading from disk to cache (preparation phase) *)
let raw_intern_library =
- snd (System.raw_extern_intern Coq_config.vo_magic_number ".vo")
+ snd (System.raw_extern_intern Coq_config.vo_magic_number)
let with_magic_number_check f a =
try f a
@@ -296,9 +297,9 @@ let intern_from_file (dir, f) =
let (md,table,digest) =
try
let ch = with_magic_number_check raw_intern_library f in
- let (md:library_disk) = System.marshal_in ch in
- let digest = System.marshal_in ch in
- let table = (System.marshal_in ch : Safe_typing.LightenLibrary.table) in
+ let (md:library_disk) = System.marshal_in f ch in
+ let digest = System.marshal_in f ch in
+ let table = (System.marshal_in f ch : Safe_typing.LightenLibrary.table) in
close_in ch;
if dir <> md.md_name then
errorlabstrm "load_physical_library"
View
5 checker/check.mllib
@@ -1,5 +1,9 @@
Coq_config
Int
+Option
+Store
+Exninfo
+Backtrace
Pp_control
Flags
Pp
@@ -15,7 +19,6 @@ CList
CString
CArray
Util
-Option
CUnix
System
Envars
View
37 checker/checker.ml
@@ -17,7 +17,7 @@ open Check
let () = at_exit flush_all
let fatal_error info =
- pperrnl info; flush_all (); exit 1
+ flush_all (); pperrnl info; flush_all (); exit 1
let coq_root = Id.of_string "Coq"
let parse_dir s =
@@ -36,7 +36,7 @@ let parse_dir s =
let dirpath_of_string s =
match parse_dir s with
[] -> Check.default_root_prefix
- | dir -> Dir_path.make (List.map Id.of_string dir)
+ | dir -> DirPath.make (List.map Id.of_string dir)
let path_of_string s =
match parse_dir s with
[] -> invalid_arg "path_of_string"
@@ -70,18 +70,19 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
let convert_string d =
try Id.of_string d
- with _ ->
- if_verbose msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
+ with Errors.UserError _ ->
+ if_verbose msg_warning
+ (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
raise Exit
let add_rec_path ~unix_path ~coq_root =
if exists_dir unix_path then
let dirs = all_subdirs ~unix_path in
- let prefix = Dir_path.repr coq_root in
+ let prefix = DirPath.repr coq_root in
let convert_dirs (lp, cp) =
try
- let path = List.map convert_string (List.rev cp) @ prefix in
- Some (lp, Names.Dir_path.make path)
+ let path = List.rev_map convert_string cp @ prefix in
+ Some (lp, Names.DirPath.make path)
with Exit -> None
in
let dirs = List.map_filter convert_dirs dirs in
@@ -113,9 +114,9 @@ let init_load_path () =
let plugins = coqlib/"plugins" in
(* NOTE: These directories are searched from last to first *)
(* first standard library *)
- add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.Dir_path.make[coq_root]);
+ add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.DirPath.make[coq_root]);
(* then plugins *)
- add_rec_path ~unix_path:plugins ~coq_root:(Names.Dir_path.make [coq_root]);
+ add_rec_path ~unix_path:plugins ~coq_root:(Names.DirPath.make [coq_root]);
(* then user-contrib *)
if Sys.file_exists user_contrib then
add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
@@ -238,8 +239,6 @@ let rec explain_exn = function
hov 0 (str "Out of memory")
| Stack_overflow ->
hov 0 (str "Stack overflow")
- | Anomaly (s,pps) ->
- hov 1 (anomaly_string () ++ where s ++ pps ++ report ())
| Match_failure(filename,pos1,pos2) ->
hov 1 (anomaly_string () ++ str "Match failure in file " ++
str (guill filename) ++ str " at line " ++ int pos1 ++
@@ -271,10 +270,6 @@ let rec explain_exn = function
(* let ctx = Check.get_env() in
hov 0
(str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*)
- | Loc.Exc_located (loc, exc) ->
- hov 0 ((if loc = Loc.ghost then (mt ())
- else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
- ++ explain_exn exc)
| Assert_failure (s,b,e) ->
hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
(if s = "" then mt ()
@@ -283,9 +278,7 @@ let rec explain_exn = function
str ", characters " ++ int e ++ str "-" ++
int (e+6) ++ str ")")) ++
report ())
- | reraise ->
- hov 0 (anomaly_string () ++ str "Uncaught exception " ++
- str (Printexc.to_string reraise)++report())
+ | e -> Errors.print e (* for anomalies and other uncaught exceptions *)
let parse_args argv =
let rec parse = function
@@ -338,13 +331,7 @@ let parse_args argv =
fatal_error (str "Unknown option " ++ str s)
| s :: rem -> add_compile s; parse rem
in
- try
- parse (List.tl (Array.to_list argv))
- with
- | UserError(_, s) as e ->
- if Pp.is_empty s then exit 1
- else fatal_error (explain_exn e)
- | e -> begin fatal_error (explain_exn e) end
+ parse (List.tl (Array.to_list argv))
(* To prevent from doing the initialization twice *)
View
55 checker/declarations.ml
@@ -7,6 +7,8 @@ open Validate
type values
type reloc_table
type to_patch_substituted
+(* Native code *)
+type native_name
(*Retroknowledge *)
type action
type retroknowledge
@@ -26,6 +28,7 @@ type delta_hint =
module Deltamap = struct
type t = module_path MPmap.t * delta_hint KNmap.t
let empty = MPmap.empty, KNmap.empty
+ let is_empty (mm, km) = MPmap.is_empty mm && KNmap.is_empty km
let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km)
let add_mp mp mp' (mm,km) = (MPmap.add mp mp' mm, km)
let remove_mp mp (mm,km) = (MPmap.remove mp mm, km)
@@ -123,10 +126,8 @@ let solve_delta_kn resolve kn =
make_kn new_mp dir l
let gen_of_delta resolve x kn fix_can =
- try
- let new_kn = solve_delta_kn resolve kn in
- if kn == new_kn then x else fix_can new_kn
- with _ -> x
+ let new_kn = solve_delta_kn resolve kn in
+ if kn == new_kn then x else fix_can new_kn
let constant_of_delta resolve con =
let kn = user_con con in
@@ -208,6 +209,11 @@ let gen_subst_mp f sub mp1 mp2 =
| None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve
| Some (mp1',_), Some (mp2',resolve2) -> Canonical, (f mp1' mp2'), resolve2
+let make_mind_equiv mpu mpc dir l =
+ let knu = make_kn mpu dir l in
+ if mpu == mpc then mind_of_kn knu
+ else mind_of_kn_equiv knu (make_kn mpc dir l)
+
let subst_ind sub mind =
let kn1,kn2 = user_mind mind, canonical_mind mind in
let mp1,dir,l = repr_kn kn1 in
@@ -220,6 +226,11 @@ let subst_ind sub mind =
| Canonical -> mind_of_delta2 resolve mind'
with No_subst -> mind
+let make_con_equiv mpu mpc dir l =
+ let knu = make_kn mpu dir l in
+ if mpu == mpc then constant_of_kn knu
+ else constant_of_kn_equiv knu (make_kn mpc dir l)
+
let subst_con0 sub con =
let kn1,kn2 = user_con con,canonical_con con in
let mp1,dir,l = repr_kn kn1 in
@@ -322,7 +333,7 @@ let from_val a = ref (LSval a)
let rec replace_mp_in_mp mpfrom mpto mp =
match mp with
- | _ when mp = mpfrom -> mpto
+ | _ when ModPath.equal mp mpfrom -> mpto
| MPdot (mp1,l) ->
let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
if mp1==mp1' then mp
@@ -331,7 +342,7 @@ let rec replace_mp_in_mp mpfrom mpto mp =
let rec mp_in_mp mp mp1 =
match mp1 with
- | _ when mp1 = mp -> true
+ | _ when ModPath.equal mp1 mp -> true
| MPdot (mp2,l) -> mp_in_mp mp mp2
| _ -> false
@@ -404,14 +415,14 @@ let update_delta_resolver resolver1 resolver2 =
let add_delta_resolver resolver1 resolver2 =
if resolver1 == resolver2 then
resolver2
- else if resolver2 = empty_delta_resolver then
+ else if Deltamap.is_empty resolver2 then
resolver1
else
Deltamap.join (update_delta_resolver resolver1 resolver2) resolver2
let substition_prefixed_by k mp subst =
let mp_prefixmp kmp (mp_to,reso) sub =
- if mp_in_mp mp kmp && mp <> kmp then
+ if mp_in_mp mp kmp && not (ModPath.equal mp kmp) then
let new_key = replace_mp_in_mp mp k kmp in
Umap.add_mp new_key (mp_to,reso) sub
else sub
@@ -508,7 +519,9 @@ type constant_body = {
const_body : constant_def;
const_type : constr;
const_body_code : to_patch_substituted;
- const_constraints : Univ.constraints }
+ const_constraints : Univ.constraints;
+ const_native_name : native_name ref;
+ const_inline_code : bool }
let body_of_constant cb = match cb.const_body with
| Undef _ -> None
@@ -528,7 +541,9 @@ let val_cb = val_tuple ~name:"constant_body"
val_cst_def;
val_cst_type;
no_val;
- val_cstrs|]
+ val_cstrs;
+ no_val;
+ val_bool|]
let subst_rel_declaration sub (id,copt,t as x) =
let copt' = Option.smartmap (subst_mps sub) copt in
@@ -673,21 +688,24 @@ type mutual_inductive_body = {
(* Universes constraints enforced by the inductive declaration *)
mind_constraints : Univ.constraints;
+ (* Data for native compilation *)
+ mind_native_name : native_name ref;
+
}
let val_ind_pack = val_tuple ~name:"mutual_inductive_body"
[|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt;
- val_int; val_int; val_rctxt;val_cstrs|]
+ val_int; val_int; val_rctxt;val_cstrs;no_val|]
let subst_arity sub s = (subst_mps sub s)
(* TODO: should be changed to non-coping after Term.subst_mps *)
-let subst_const_body sub cb = {
- const_hyps = (assert (cb.const_hyps=[]); []);
+(* NB: we leave bytecode and native code fields untouched *)
+let subst_const_body sub cb =
+ { cb with
+ const_hyps = (assert (List.is_empty cb.const_hyps); []);
const_body = subst_constant_def sub cb.const_body;
- const_type = subst_arity sub cb.const_type;
- const_body_code = (*Cemitcodes.subst_to_patch_subst sub*) cb.const_body_code;
- const_constraints = cb.const_constraints}
+ const_type = subst_arity sub cb.const_type }
let subst_arity sub s =
{ mind_user_arity = subst_mps sub s.mind_user_arity;
@@ -715,13 +733,14 @@ let subst_mind sub mib =
{ mind_record = mib.mind_record ;
mind_finite = mib.mind_finite ;
mind_ntypes = mib.mind_ntypes ;
- mind_hyps = (assert (mib.mind_hyps=[]); []) ;
+ mind_hyps = (assert (List.is_empty mib.mind_hyps); []) ;
mind_nparams = mib.mind_nparams;
mind_nparams_rec = mib.mind_nparams_rec;
mind_params_ctxt =
map_rel_context (subst_mps sub) mib.mind_params_ctxt;
mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
- mind_constraints = mib.mind_constraints }
+ mind_constraints = mib.mind_constraints;
+ mind_native_name = mib.mind_native_name}
(* Modules *)
View
9 checker/declarations.mli
@@ -5,6 +5,8 @@ open Term
type values
type reloc_table
type to_patch_substituted
+(* Native code *)
+type native_name
(*Retroknowledge *)
type action
type retroknowledge
@@ -50,7 +52,9 @@ type constant_body = {
const_body : constant_def;
const_type : constr;
const_body_code : to_patch_substituted;
- const_constraints : Univ.constraints }
+ const_constraints : Univ.constraints;
+ const_native_name : native_name ref;
+ const_inline_code : bool }
val body_of_constant : constant_body -> constr_substituted option
val constant_has_body : constant_body -> bool
@@ -156,6 +160,9 @@ type mutual_inductive_body = {
(* Universes constraints enforced by the inductive declaration *)
mind_constraints : Univ.constraints;
+ (* Data for native compilation *)
+ mind_native_name : native_name ref;
+
}
(* Modules *)
View
14 checker/environ.ml
@@ -99,7 +99,7 @@ let named_type id env =
(* Universe constraints *)
let add_constraints c env =
- if c == empty_constraint then
+ if c == Constraint.empty then
env
else
let s = env.env_stratification in
@@ -111,9 +111,11 @@ let add_constraints c env =
let lookup_constant kn env =
Cmap_env.find kn env.env_globals.env_constants
+let anomaly s = anomaly (Pp.str s)
+
let add_constant kn cs env =
if Cmap_env.mem kn env.env_globals.env_constants then
- Printf.ksprintf anomaly "Constant %s is already defined"
+ Printf.ksprintf anomaly ("Constant %s is already defined")
(string_of_con kn);
let new_constants =
Cmap_env.add kn cs env.env_globals.env_constants in
@@ -155,7 +157,7 @@ let lookup_mind kn env =
let add_mind kn mib env =
if Mindmap_env.mem kn env.env_globals.env_inductives then
- Printf.ksprintf anomaly "Inductive %s is already defined"
+ Printf.ksprintf anomaly ("Inductive %s is already defined")
(string_of_mind kn);
let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
let kn1,kn2 = user_mind kn,canonical_mind kn in
@@ -174,7 +176,7 @@ let add_mind kn mib env =
let add_modtype ln mtb env =
if MPmap.mem ln env.env_globals.env_modtypes then
- Printf.ksprintf anomaly "Module type %s is already defined"
+ Printf.ksprintf anomaly ("Module type %s is already defined")
(string_of_mp ln);
let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
let new_globals =
@@ -184,7 +186,7 @@ let add_modtype ln mtb env =
let shallow_add_module mp mb env =
if MPmap.mem mp env.env_globals.env_modules then
- Printf.ksprintf anomaly "Module %s is already defined"
+ Printf.ksprintf anomaly ("Module %s is already defined")
(string_of_mp mp);
let new_mods = MPmap.add mp mb env.env_globals.env_modules in
let new_globals =
@@ -194,7 +196,7 @@ let shallow_add_module mp mb env =
let shallow_remove_module mp env =
if not (MPmap.mem mp env.env_globals.env_modules) then
- Printf.ksprintf anomaly "Module %s is unknown"
+ Printf.ksprintf anomaly ("Module %s is unknown")
(string_of_mp mp);
let new_mods = MPmap.remove mp env.env_globals.env_modules in
let new_globals =
View
4 checker/environ.mli
@@ -27,8 +27,8 @@ val engagement : env -> Declarations.engagement option
val set_engagement : Declarations.engagement -> env -> env
(* Digests *)
-val add_digest : env -> Dir_path.t -> Digest.t -> env
-val lookup_digest : env -> Dir_path.t -> Digest.t
+val add_digest : env -> DirPath.t -> Digest.t -> env
+val lookup_digest : env -> DirPath.t -> Digest.t
(* de Bruijn variables *)
val rel_context : env -> rel_context
View
2 checker/include
@@ -127,7 +127,7 @@ let mod_access m fld =
;;
let parse_dp s =
- make_dirpath(List.map id_of_string (List.rev (Str.split(Str.regexp"\\.") s)))
+ make_dirpath(List.rev_map id_of_string (Str.split(Str.regexp"\\.") s))
;;
let parse_sp s =
let l = List.rev (Str.split(Str.regexp"\\.") s) in
View
16 checker/indtypes.ml
@@ -19,12 +19,12 @@ open Declarations
open Environ
let rec debug_string_of_mp = function
- | MPfile sl -> Dir_path.to_string sl
+ | MPfile sl -> DirPath.to_string sl
| MPbound uid -> "bound("^MBId.to_string uid^")"
| MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ Label.to_string l
let rec string_of_mp = function
- | MPfile sl -> Dir_path.to_string sl
+ | MPfile sl -> DirPath.to_string sl
| MPbound uid -> MBId.to_string uid
| MPdot (mp,l) -> string_of_mp mp ^ "." ^ Label.to_string l
@@ -100,7 +100,7 @@ let rec sorts_of_constr_args env t =
let env1 = push_rel (name,Some def,ty) env in
sorts_of_constr_args env1 c
| _ when is_constructor_head t -> []
- | _ -> anomaly "infos_and_sort: not a positive constructor"
+ | _ -> anomaly ~label:"infos_and_sort" (Pp.str "not a positive constructor")
(* Prop and Set are small *)
@@ -299,11 +299,11 @@ let failwith_non_pos n ntypes c =
let failwith_non_pos_vect n ntypes v =
Array.iter (failwith_non_pos n ntypes) v;
- anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur"
+ anomaly ~label:"failwith_non_pos_vect" (Pp.str "some k in [n;n+ntypes-1] should occur")
let failwith_non_pos_list n ntypes l =
List.iter (failwith_non_pos n ntypes) l;
- anomaly "failwith_non_pos_list: some k in [n;n+ntypes-1] should occur"
+ anomaly ~label:"failwith_non_pos_list" (Pp.str "some k in [n;n+ntypes-1] should occur")
(* Conclusion of constructors: check the inductive type is called with
the expected parameters *)
@@ -355,8 +355,8 @@ let abstract_mind_lc env ntyps npars lc =
lc
else
let make_abs =
- List.tabulate
- (function i -> lambda_implicit_lift npars (Rel (i+1))) ntyps
+ List.init ntyps
+ (function i -> lambda_implicit_lift npars (Rel (i+1)))
in
Array.map (substl make_abs) lc
@@ -514,7 +514,7 @@ let check_positivity env_ar mind params nrecp inds =
let lparams = rel_context_length params in
let check_one i mip =
let ra_env =
- List.tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
+ List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
in
View
14 checker/inductive.ml
@@ -58,7 +58,7 @@ let inductive_params (mib,_) = mib.mind_nparams
let ind_subst mind mib =
let ntypes = mib.mind_ntypes in
let make_Ik k = Ind (mind,ntypes-k-1) in
- List.tabulate make_Ik ntypes
+ List.init ntypes make_Ik
(* Instantiate inductives in constructor type *)
let constructor_instantiate mind mib c =
@@ -67,7 +67,7 @@ let constructor_instantiate mind mib c =
let instantiate_params full t args sign =
let fail () =
- anomaly "instantiate_params: type, ctxt and args mismatch" in
+ anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
let (rem_args, subs, ty) =
fold_rel_context
(fun (_,copt,_) (largs,subs,ty) ->
@@ -523,7 +523,7 @@ let branches_specif renv c_spec ci =
vra
| Dead_code -> Array.make nca Dead_code
| _ -> Array.make nca Not_subterm) in
- List.tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
+ List.init nca (fun j -> lazy (Lazy.force lvra).(j)))
car
(* [subterm_specif renv t] computes the recursive structure of [t] and
@@ -774,7 +774,7 @@ let check_one_fix renv recpos def =
check_rec_call renv [] a;
let renv' = push_var_renv renv (x,a) in
check_nested_fix_body renv' (decr-1) recArgsDecrArg b
- | _ -> anomaly "Not enough abstractions in fix body"
+ | _ -> anomaly (Pp.str "Not enough abstractions in fix body")
in
check_rec_call renv [] def
@@ -788,7 +788,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
or Array.length names <> nbfix
or bodynum < 0
or bodynum >= nbfix
- then anomaly "Ill-formed fix term";
+ then anomaly (Pp.str "Ill-formed fix term");
let fixenv = push_rec_types recdef env in
let raise_err env i err =
error_ill_formed_rec_body env err names i in
@@ -809,7 +809,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
raise_err env i (RecursionNotOnInductiveType a) in
(mind, (env', b))
else check_occur env' (n+1) b
- else anomaly "check_one_fix: Bad occurrence of recursive call"
+ else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call")
| _ -> raise_err env i NotEnoughAbstractionInFixBody in
check_occur fixenv 1 def in
(* Do it on every fixpoint *)
@@ -838,7 +838,7 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
exception CoFixGuardError of env * guard_error
let anomaly_ill_typed () =
- anomaly "check_one_cofix: too many arguments applied to constructor"
+ anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor")
let rec codomain_is_coind env c =
let b = whd_betadeltaiota env c in
View
15 checker/mod_checking.ml
@@ -133,6 +133,11 @@ let lookup_modtype mp env =
with Not_found ->
failwith ("Unknown module type: "^string_of_mp mp)
+let lookup_module mp env =
+ try Environ.lookup_module mp env
+ with Not_found ->
+ failwith ("Unknown module: "^string_of_mp mp)
+
let rec check_with env mtb with_decl mp=
match with_decl with
| With_definition_body (idl,c) ->
@@ -199,7 +204,7 @@ and check_with_mod env mtb (idl,mp1) mp =
SFBmodule msb -> msb
| _ -> error_not_a_module l
in
- let (_:module_body) = (lookup_module mp1 env) in ()
+ let (_:module_body) = (Environ.lookup_module mp1 env) in ()
else
let old = match spec with
SFBmodule msb -> msb
@@ -239,24 +244,24 @@ and check_module env mp mb =
{typ_mp=mp;
typ_expr=sign;
typ_expr_alg=None;
- typ_constraints=Univ.empty_constraint;
+ typ_constraints=Univ.Constraint.empty;
typ_delta = mb.mod_delta;}
and mtb2 =
{typ_mp=mp;
typ_expr=mb.mod_type;
typ_expr_alg=None;
- typ_constraints=Univ.empty_constraint;
+ typ_constraints=Univ.Constraint.empty;
typ_delta = mb.mod_delta;}
in
let env = add_module (module_body_of_type mp mtb1) env in
check_subtypes env mtb1 mtb2
and check_structure_field env mp lab res = function
| SFBconst cb ->
- let c = make_con mp Dir_path.empty lab in
+ let c = Constant.make2 mp lab in
check_constant_declaration env c cb
| SFBmind mib ->
- let kn = make_mind mp Dir_path.empty lab in
+ let kn = MutInd.make2 mp lab in
let kn = mind_of_delta res kn in
Indtypes.check_inductive env kn mib
| SFBmodule msb ->
View
14 checker/modops.ml
@@ -67,9 +67,9 @@ let module_body_of_type mp mtb =
let rec add_signature mp sign resolver env =
let add_one env (l,elem) =
- let kn = make_kn mp Dir_path.empty l in
- let con = constant_of_kn kn in
- let mind = mind_of_delta resolver (mind_of_kn kn) in
+ let kn = KerName.make2 mp l in
+ let con = Constant.make1 kn in
+ let mind = mind_of_delta resolver (MutInd.make1 kn) in
match elem with
| SFBconst cb ->
(* let con = constant_of_delta resolver con in*)
@@ -90,14 +90,14 @@ and add_module mb env =
| SEBstruct (sign) ->
add_signature mp sign mb.mod_delta env
| SEBfunctor _ -> env
- | _ -> anomaly "Modops:the evaluation of the structure failed "
+ | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
let strengthen_const mp_from l cb resolver =
match cb.const_body with
| Def _ -> cb
| _ ->
- let con = make_con mp_from Dir_path.empty l in
+ let con = Constant.make2 mp_from l in
(* let con = constant_of_delta resolver con in*)
{ cb with const_body = Def (Declarations.from_val (Const con)) }
@@ -118,7 +118,7 @@ let rec strengthen_mod mp_from mp_to mb =
(add_delta_resolver mb.mod_delta resolve_out)*);
mod_retroknowledge = mb.mod_retroknowledge}
| SEBfunctor _ -> mb
- | _ -> anomaly "Modops:the evaluation of the structure failed "
+ | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
and strengthen_sig mp_from sign mp_to resolver =
match sign with
@@ -152,7 +152,7 @@ let strengthen mtb mp =
typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
(add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)}
| SEBfunctor _ -> mtb
- | _ -> anomaly "Modops:the evaluation of the structure failed "
+ | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
let subst_and_strengthen mb mp =
strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb)
View
6 checker/reduction.ml
@@ -287,13 +287,13 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(* Eta-expansion on the fly *)
| (FLambda _, _) ->
if v1 <> [] then
- anomaly "conversion was given unreduced term (FLambda)";
+ anomaly (Pp.str "conversion was given unreduced term (FLambda)");
let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
eqappr univ CONV infos
(el_lift lft1,(bd1,[])) (el_lift lft2,(hd2,eta_expand_stack v2))
| (_, FLambda _) ->
if v2 <> [] then
- anomaly "conversion was given unreduced term (FLambda)";
+ anomaly (Pp.str "conversion was given unreduced term (FLambda)");
let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
eqappr univ CONV infos
(el_lift lft1,(hd1,eta_expand_stack v1)) (el_lift lft2,(bd2,[]))
@@ -398,7 +398,7 @@ let vm_conv = fconv
let hnf_prod_app env t n =
match whd_betadeltaiota env t with
| Prod (_,_,b) -> subst1 n b
- | _ -> anomaly "hnf_prod_app: Need a product"
+ | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
let hnf_prod_applist env t nl =
List.fold_left (hnf_prod_app env) t nl
View
10 checker/safe_typing.ml
@@ -43,9 +43,9 @@ let check_engagement env c =
let report_clash f caller dir =
let msg =
- str "compiled library " ++ str(Dir_path.to_string caller) ++
+ str "compiled library " ++ str(DirPath.to_string caller) ++
spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++
- str(Dir_path.to_string dir) ++ fnl() in
+ str(DirPath.to_string dir) ++ fnl() in
f msg
@@ -55,15 +55,15 @@ let check_imports f caller env needed =
let actual_stamp = lookup_digest env dp in
if stamp <> actual_stamp then report_clash f caller dp
with Not_found ->
- error ("Reference to unknown module " ^ (Dir_path.to_string dp))
+ error ("Reference to unknown module " ^ (DirPath.to_string dp))
in
List.iter check needed
type compiled_library =
- Dir_path.t *
+ DirPath.t *
module_body *
- (Dir_path.t * Digest.t) list *
+ (DirPath.t * Digest.t) list *
engagement option
(* Store the body of modules' opaque constants inside a table.
View
4 checker/subtyping.ml
@@ -35,7 +35,7 @@ type namedmodule =
constructors *)
let add_mib_nameobjects mp l mib map =
- let ind = make_mind mp Dir_path.empty l in
+ let ind = MutInd.make2 mp l in
let add_mip_nameobjects j oib map =
let ip = (ind,j) in
let map =
@@ -83,7 +83,7 @@ let check_conv_error error f env a1 a2 =
(* for now we do not allow reorderings *)
let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
- let kn = make_mind mp1 Dir_path.empty l in
+ let kn = MutInd.make2 mp1 l in
let error () = error_not_match l spec2 in
let check_conv f = check_conv_error error f in
let mib1 =
View
64 checker/term.ml
@@ -80,8 +80,8 @@ let val_fix f =
[|val_tuple~name:"fix2"[|val_array val_int;val_int|];val_prec f|]
let val_cofix f = val_tuple ~name:"pcofixpoint"[|val_int;val_prec f|]
-type cast_kind = VMcast | DEFAULTcast
-let val_cast = val_enum "cast_kind" 2
+type cast_kind = VMcast | NATIVEcast | DEFAULTcast
+let val_cast = val_enum "cast_kind" 3
(*s*******************************************************************)
(* The type of constructions *)
@@ -197,7 +197,7 @@ let closed0 = closedn 0
let noccurn n term =
let rec occur_rec n c = match c with
- | Rel m -> if m = n then raise LocalOccur
+ | Rel m -> if Int.equal m n then raise LocalOccur
| _ -> iter_constr_with_binders succ occur_rec n c
in
try occur_rec n term; true with LocalOccur -> false
@@ -221,7 +221,7 @@ let noccur_between n m term =
let noccur_with_meta n m term =
let rec occur_rec n c = match c with
- | Rel p -> if n<=p & p<n+m then raise LocalOccur
+ | Rel p -> if n<=p && p<n+m then raise LocalOccur
| App(f,cl) ->
(match f with
| (Cast (Meta _,_,_)| Meta _) -> ()
@@ -291,7 +291,7 @@ let make_substituend c = { sinfo=Unknown; sit=c }
let substn_many lamv n c =
let lv = Array.length lamv in
- if lv = 0 then c
+ if Int.equal lv 0 then c
else
let rec substrec depth c = match c with
| Rel k ->
@@ -383,7 +383,7 @@ let decompose_lam_n_assum n =
if n < 0 then
error "decompose_lam_n_assum: integer parameter must be positive";
let rec lamdec_rec l n c =
- if n=0 then l,c
+ if Int.equal n 0 then l,c
else match c with
| Lambda (x,t,c) -> lamdec_rec ((x,None,t) :: l) (n-1) c
| LetIn (x,b,t,c) -> lamdec_rec ((x,Some b,t) :: l) n c
@@ -416,7 +416,7 @@ let decompose_prod_n_assum n =
if n < 0 then
error "decompose_prod_n_assum: integer parameter must be positive";
let rec prodec_rec l n c =
- if n=0 then l,c
+ if Int.equal n 0 then l,c
else match c with
| Prod (x,t,c) -> prodec_rec ((x,None,t) :: l) (n-1) c
| LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t) :: l) (n-1) c
@@ -441,7 +441,7 @@ let destArity =
| LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
| Cast (c,_,_) -> prodec_rec l c
| Sort s -> l,s
- | _ -> anomaly "destArity: not an arity"
+ | _ -> anomaly ~label:"destArity" (Pp.str "not an arity")
in
prodec_rec []
@@ -459,40 +459,52 @@ let rec isArity c =
(* alpha conversion : ignore print names and casts *)
+let compare_sorts s1 s2 = match s1, s2 with
+| Prop c1, Prop c2 ->
+ begin match c1, c2 with
+ | Pos, Pos | Null, Null -> true
+ | Pos, Null -> false
+ | Null, Pos -> false
+ end
+| Type u1, Type u2 -> Universe.eq u1 u2
+| Prop _, Type _ -> false
+| Type _, Prop _ -> false
+
let compare_constr f t1 t2 =
match t1, t2 with
- | Rel n1, Rel n2 -> n1 = n2
- | Meta m1, Meta m2 -> m1 = m2
- | Var id1, Var id2 -> id1 = id2
- | Sort s1, Sort s2 -> s1 = s2
+ | Rel n1, Rel n2 -> Int.equal n1 n2
+ | Meta m1, Meta m2 -> Int.equal m1 m2
+ | Var id1, Var id2 -> Id.equal id1 id2
+ | Sort s1, Sort s2 -> compare_sorts s1 s2
| Cast (c1,_,_), _ -> f c1 t2
| _, Cast (c2,_,_) -> f t1 c2
- | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 & f c1 c2
- | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 & f c1 c2
- | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2
+ | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2
+ | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 && f c1 c2
+ | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 && f t1 t2 && f c1 c2
| App (c1,l1), App (c2,l2) ->
- if Array.length l1 = Array.length l2 then
- f c1 c2 & Array.for_all2 f l1 l2
+ if Int.equal (Array.length l1) (Array.length l2) then
+ f c1 c2 && Array.for_all2 f l1 l2
else
let (h1,l1) = decompose_app t1 in
let (h2,l2) = decompose_app t2 in
- if List.length l1 = List.length l2 then
- f h1 h2 & List.for_all2 f l1 l2
+ if Int.equal (List.length l1) (List.length l2) then
+ f h1 h2 && List.for_all2 f l1 l2
else false
- | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & Array.for_all2 f l1 l2
+ | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2
| Const c1, Const c2 -> eq_con_chk c1 c2
| Ind c1, Ind c2 -> eq_ind_chk c1 c2
- | Construct (c1,i1), Construct (c2,i2) -> i1=i2 && eq_ind_chk c1 c2
+ | Construct (c1,i1), Construct (c2,i2) -> Int.equal i1 i2 && eq_ind_chk c1 c2
| Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
- f p1 p2 & f c1 c2 & Array.for_all2 f bl1 bl2
- | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
- ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2
+ f p1 p2 && f c1 c2 && Array.equal f bl1 bl2
+ | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
+ Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 &&
+ Array.equal f tl1 tl2 && Array.equal f bl1 bl2
| CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
- ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2
+ Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
| _ -> false
let rec eq_constr m n =
- (m==n) or
+ (m == n) ||
compare_constr eq_constr m n
let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
View
2 checker/term.mli
@@ -23,7 +23,7 @@ type 'a pexistential = existential_key * 'a array
type 'a prec_declaration = name array * 'a array * 'a array
type 'a pfixpoint = (int array * int) * 'a prec_declaration
type 'a pcofixpoint = int * 'a prec_declaration
-type cast_kind = VMcast | DEFAULTcast
+type cast_kind = VMcast | NATIVEcast | DEFAULTcast
type constr =
Rel of int
| Var of Id.t
View
6 checker/typeops.ml
@@ -166,7 +166,7 @@ let sort_of_product env domsort rangsort =
let judge_of_cast env (c,cj) k tj =
let conversion =
match k with
- | VMcast -> vm_conv CUMUL
+ | VMcast | NATIVEcast -> vm_conv CUMUL
| DEFAULTcast -> conv_leq in
try
conversion env cj tj
@@ -350,10 +350,10 @@ let rec execute env cstr =
(* Partial proofs: unsupported by the kernel *)
| Meta _ ->
- anomaly "the kernel does not support metavariables"
+ anomaly (Pp.str "the kernel does not support metavariables")
| Evar _ ->
- anomaly "the kernel does not support existential variables"
+ anomaly (Pp.str "the kernel does not support existential variables")
and execute_type env constr =
let j = execute env constr in
View
3 checker/validate.ml
@@ -188,8 +188,7 @@ let val_mp =
let val_kn = val_tuple ~name:"kernel_name" [|val_mp;val_dp;val_id|]
-let val_con =
- val_tuple ~name:"constant/mutind" [|val_kn;val_kn|]
+let val_con = val_sum "constant/mutind" 0 [|[|val_kn|];[|val_kn;val_kn|]|]
let val_ind = val_tuple ~name:"inductive"[|val_con;val_int|]
let val_cstr = val_tuple ~name:"constructor"[|val_ind;val_int|]
View
1 config/coq_config.mli
@@ -69,3 +69,4 @@ val wwwrefman : string
val wwwstdlib : string
val localwwwrefman : string
+val no_native_compiler : bool
View
15 configure
@@ -89,7 +89,9 @@ usage () {
echo "-typerex"
printf "\tCompiles Coq using typerex wrapper\n"
echo "-makecmd <command>"
- printf "\tName of GNU Make command.\n"
+ printf "\tName of GNU Make command\n"
+ echo "-no-native-compiler"
+ printf "\tDisables compilation to native code for conversion and normalization\n"
}
@@ -142,6 +144,7 @@ with_doc_spec=no
force_caml_version=no
force_caml_version_spec=no
usecamlp5=yes
+no_native_compiler=false
# Parse command-line arguments
@@ -249,6 +252,7 @@ while : ; do
-profile|--profile) coq_profile_flag=-p;;
-annotate|--annotate) coq_annotate_flag=-dtypes;;
-typerex|--typerex) coq_typerex_wrapper=$default_typerex_wrapper;;
+ -no-native-compiler|--no-native-compiler) no_native_compiler=true;;
-force-caml-version|--force-caml-version|-force-ocaml-version|--force-ocaml-version)
force_caml_version_spec=yes
force_caml_version=yes;;
@@ -901,6 +905,11 @@ echo " Web browser : $BROWSER"
echo " Coq web site : $WWWCOQ"
echo ""
+if test "$no_native_compiler" = "true"; then
+echo " Native compiler for conversion and normalization disabled"
+echo ""
+fi
+
if test "$local" = "true"; then
echo " Local build, no installation..."
echo ""
@@ -1051,6 +1060,8 @@ let wwwcoq = "$WWWCOQ"
let wwwrefman = wwwcoq ^ "distrib/" ^ version ^ "/refman/"
let wwwstdlib = wwwcoq ^ "distrib/" ^ version ^ "/stdlib/"
let localwwwrefman = "file:/" ^ docdir ^ "html/refman"
+let no_native_compiler = $no_native_compiler
+
END_OF_COQ_CONFIG
@@ -1142,7 +1153,7 @@ CAMLLINK="$bytecamlc"
CAMLOPTLINK="$nativecamlc"
# Caml flags
-CAMLFLAGS=$coq_annotate_flag
+CAMLFLAGS=-rectypes $coq_annotate_flag
TYPEREX=$coq_typerex_wrapper
# Compilation debug flags
View
8 dev/base_include
@@ -88,6 +88,7 @@ open Reductionops
open Evarconv
open Retyping
open Evarutil
+open Evarsolve
open Tacred
open Evd
open Universes
@@ -192,10 +193,11 @@ let constr_of_string s =
(* get the body of a constant *)
open Declarations;;
+open Declareops;;
let constbody_of_string s =
let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in
- Option.get (body_of_constant b);;
+ Option.get (Declareops.body_of_constant b);;
(* Get the current goal *)
(*
@@ -209,8 +211,8 @@ let pf_e gl s =
(* Set usual printing since the global env is available from the tracer *)
let _ = Constrextern.in_debugger := false
-let _ = Constrextern.set_debug_global_reference_printer
- (fun loc r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
+let _ = Constrextern.set_extern_reference
+ (fun loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
open Toplevel
let go = loop
View
2 dev/db_printers.ml
@@ -11,6 +11,6 @@ open Names
let pp s = pp (hov 0 s)
let prid id = Format.print_string (Id.to_string id)
-let prsp sp = Format.print_string (string_of_path sp)
+let prsp sp = Format.print_string (DirPath.to_string sp)
View
9 dev/doc/debugging.txt
@@ -21,6 +21,15 @@ Debugging from Coq toplevel using Caml trace mechanism
notations, ...), use "Set Printing All". It will affect the #trace
printers too.
+Note for Ocaml 3.10.x: Ocaml 3.10.x requires that modules compiled
+with -rectypes are loaded in an environment with -rectypes set but
+there is no way to tell the toplevel to support -rectypes. To make it
+works, use "patch -p0 < dev/doc/patch.ocaml-3.10.drop.rectypes" to
+hack script/coqmktop.ml, then recompile coqtop.byte. The procedure
+above then works as soon as coqtop.byte is called with at least one
+argument (add neutral option -byte to ensure at least one argument).
+
+
Debugging from Caml debugger
============================
View
31 dev/doc/patch.ocaml-3.10.drop.rectypes
@@ -0,0 +1,31 @@
+Index: scripts/coqmktop.ml
+===================================================================
+--- scripts/coqmktop.ml (révision 12084)
++++ scripts/coqmktop.ml (copie de travail)
+@@ -231,12 +231,25 @@
+ end;;
+
+ let ppf = Format.std_formatter;;
++ let set_rectypes_hack () =
++ if String.length (Sys.ocaml_version) >= 4 &
++ String.sub (Sys.ocaml_version) 0 4 = \"3.10\"
++ then
++ (* ocaml 3.10 does not have #rectypes but needs it *)
++ (* simulate a call with option -rectypes before *)
++ (* jumping to the ocaml toplevel *)
++ for i = 1 to Array.length Sys.argv - 1 do
++ Sys.argv.(i) <- \"-rectypes\"
++ done
++ else
++ () in
++
+ Mltop.set_top
+ {Mltop.load_obj=
+ (fun f -> if not (Topdirs.load_file ppf f) then failwith \"error\");
+ Mltop.use_file=Topdirs.dir_use ppf;
+ Mltop.add_dir=Topdirs.dir_directory;
+- Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n"
++ Mltop.ml_loop=(fun () -> set_rectypes_hack(); Topmain.main()) };;\n"
+
+ (* create a temporary main file to link *)
+ let create_tmp_main_file modules =
View
6 dev/include
@@ -32,23 +32,25 @@
#install_printer (* constr *) ppconstr;;
#install_printer (* constr_substituted *) ppsconstr;;
#install_printer (* constraints *) ppconstraints;;
+#install_printer (* univ constraints *) ppuniverseconstraints;;
#install_printer (* universe *) ppuni;;
#install_printer (* universes *) ppuniverses;;
#install_printer (* univ level *) ppuni_level;;
#install_printer (* univ context *) ppuniverse_context;;
#install_printer (* univ context set *) ppuniverse_context_set;;
#install_printer (* univ set *) ppuniverse_set;;
+#install_printer (* univ instance *) ppuniverse_instance;;
#install_printer (* univ list *) ppuniverse_list;;
#install_printer (* univ subst *) ppuniverse_subst;;
-#install_printer (* univ full subst *) ppuniverse_full_subst;;
+#install_printer (* univ full subst *) ppuniverse_level_subst;;
#install_printer (* univ opt subst *) ppuniverse_opt_subst;;
#install_printer (* evar univ ctx *) ppevar_universe_context;;
#install_printer (* inductive *) ppind;;
#install_printer (* 'a scheme_kind *) ppscheme;;
#install_printer (* type_judgement *) pptype;;
#install_printer (* judgement *) ppj;;
-#install_printer (* hint_db *) print_hint_db;;
+(*#install_printer (* hint_db *) print_hint_db;;*)
(*#install_printer (* hints_path *) pphintspath;;*)
#install_printer (* goal *) ppgoal;;
(*#install_printer (* sigma goal *) ppsigmagoal;;*)
View
16 dev/printers.mllib
@@ -1,6 +1,10 @@
Coq_config
Int
+Option
+Store
+Exninfo
+Backtrace
Pp_control
Loc
Compat
@@ -22,7 +26,6 @@ Dyn
CUnix
System
Envars
-Store
Gmap
Fset
Fmap
@@ -32,7 +35,6 @@ Explore
Predicate
Rtree
Heap
-Option
Dnet
Names
@@ -44,14 +46,20 @@ Sign
Cbytecodes
Copcodes
Cemitcodes
-Declarations
+Nativevalues
+Lazyconstr
+Declareops
Retroknowledge
Pre_env
+Nativelambda
+Nativecode
+Nativelib
Cbytegen
Environ
Conv_oracle
Closure
Reduction
+Nativeconv
Type_errors
Modops
Inductive
@@ -61,6 +69,7 @@ Cooking
Term_typing
Subtyping
Mod_typing
+Nativelibrary
Safe_typing
Unionfind
@@ -90,6 +99,7 @@ Retyping
Cbv
Pretype_errors
Evarutil
+Evarsolve
Term_dnet
Recordops
Evarconv
View
37 dev/top_printers.ml
@@ -53,7 +53,7 @@ let ppconstr x = pp (Termops.print_constr x)
let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x)
let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x)
let ppterm = ppconstr
-let ppsconstr x = ppconstr (Declarations.force x)