aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/.depend58
-rw-r--r--checker/analyze.ml423
-rw-r--r--checker/analyze.mli51
-rw-r--r--checker/check.ml421
-rw-r--r--checker/check.mli33
-rw-r--r--checker/check.mllib11
-rw-r--r--checker/checkInductive.ml162
-rw-r--r--checker/checkInductive.mli19
-rw-r--r--checker/checkTypes.ml36
-rw-r--r--checker/checkTypes.mli20
-rw-r--r--checker/check_stat.ml55
-rw-r--r--checker/check_stat.mli13
-rw-r--r--checker/checker.ml408
-rw-r--r--checker/checker.mli11
-rw-r--r--checker/coqchk.ml2
-rw-r--r--checker/coqchk.mli12
-rw-r--r--checker/dune28
-rw-r--r--checker/include192
-rw-r--r--checker/mod_checking.ml143
-rw-r--r--checker/mod_checking.mli11
-rw-r--r--checker/safe_checking.ml23
-rw-r--r--checker/safe_checking.mli16
-rw-r--r--checker/validate.ml150
-rw-r--r--checker/validate.mli11
-rw-r--r--checker/values.ml375
-rw-r--r--checker/values.mli48
-rw-r--r--checker/votour.ml404
-rw-r--r--checker/votour.mli12
28 files changed, 3148 insertions, 0 deletions
diff --git a/checker/.depend b/checker/.depend
new file mode 100644
index 0000000000..09ab6bdd13
--- /dev/null
+++ b/checker/.depend
@@ -0,0 +1,58 @@
+checker.cmo: type_errors.cmi term.cmo safe_typing.cmi indtypes.cmi \
+ declarations.cmi check_stat.cmi check.cmo
+checker.cmx: type_errors.cmx term.cmx safe_typing.cmx indtypes.cmx \
+ declarations.cmx check_stat.cmx check.cmx
+check.cmo: safe_typing.cmi
+check.cmx: safe_typing.cmx
+check_stat.cmo: term.cmo safe_typing.cmi indtypes.cmi environ.cmo \
+ declarations.cmi check_stat.cmi
+check_stat.cmx: term.cmx safe_typing.cmx indtypes.cmx environ.cmx \
+ declarations.cmx check_stat.cmi
+closure.cmo: term.cmo environ.cmo closure.cmi
+closure.cmx: term.cmx environ.cmx closure.cmi
+closure.cmi: term.cmo environ.cmo
+declarations.cmo: term.cmo declarations.cmi
+declarations.cmx: term.cmx declarations.cmi
+declarations.cmi: term.cmo
+environ.cmo: term.cmo declarations.cmi
+environ.cmx: term.cmx declarations.cmx
+indtypes.cmo: typeops.cmi term.cmo reduction.cmi inductive.cmi environ.cmo \
+ declarations.cmi indtypes.cmi
+indtypes.cmx: typeops.cmx term.cmx reduction.cmx inductive.cmx environ.cmx \
+ declarations.cmx indtypes.cmi
+indtypes.cmi: typeops.cmi term.cmo environ.cmo declarations.cmi
+inductive.cmo: type_errors.cmi term.cmo reduction.cmi environ.cmo \
+ declarations.cmi inductive.cmi
+inductive.cmx: type_errors.cmx term.cmx reduction.cmx environ.cmx \
+ declarations.cmx inductive.cmi
+inductive.cmi: term.cmo environ.cmo declarations.cmi
+main.cmo: checker.cmo
+main.cmx: checker.cmx
+mod_checking.cmo: typeops.cmi term.cmo subtyping.cmi reduction.cmi modops.cmi \
+ inductive.cmi indtypes.cmi environ.cmo declarations.cmi
+mod_checking.cmx: typeops.cmx term.cmx subtyping.cmx reduction.cmx modops.cmx \
+ inductive.cmx indtypes.cmx environ.cmx declarations.cmx
+modops.cmo: term.cmo environ.cmo declarations.cmi modops.cmi
+modops.cmx: term.cmx environ.cmx declarations.cmx modops.cmi
+modops.cmi: term.cmo environ.cmo declarations.cmi
+reduction.cmo: term.cmo environ.cmo closure.cmi reduction.cmi
+reduction.cmx: term.cmx environ.cmx closure.cmx reduction.cmi
+reduction.cmi: term.cmo environ.cmo
+safe_typing.cmo: validate.cmo modops.cmi mod_checking.cmo environ.cmo \
+ declarations.cmi safe_typing.cmi
+safe_typing.cmx: validate.cmx modops.cmx mod_checking.cmx environ.cmx \
+ declarations.cmx safe_typing.cmi
+safe_typing.cmi: term.cmo environ.cmo declarations.cmi
+subtyping.cmo: typeops.cmi term.cmo reduction.cmi modops.cmi inductive.cmi \
+ environ.cmo declarations.cmi subtyping.cmi
+subtyping.cmx: typeops.cmx term.cmx reduction.cmx modops.cmx inductive.cmx \
+ environ.cmx declarations.cmx subtyping.cmi
+subtyping.cmi: term.cmo environ.cmo declarations.cmi
+type_errors.cmo: term.cmo environ.cmo type_errors.cmi
+type_errors.cmx: term.cmx environ.cmx type_errors.cmi
+type_errors.cmi: term.cmo environ.cmo
+typeops.cmo: type_errors.cmi term.cmo reduction.cmi inductive.cmi environ.cmo \
+ declarations.cmi typeops.cmi
+typeops.cmx: type_errors.cmx term.cmx reduction.cmx inductive.cmx environ.cmx \
+ declarations.cmx typeops.cmi
+typeops.cmi: term.cmo environ.cmo declarations.cmi
diff --git a/checker/analyze.ml b/checker/analyze.ml
new file mode 100644
index 0000000000..63324bff20
--- /dev/null
+++ b/checker/analyze.ml
@@ -0,0 +1,423 @@
+(** Headers *)
+
+let prefix_small_block = 0x80
+let prefix_small_int = 0x40
+let prefix_small_string = 0x20
+
+[@@@ocaml.warning "-32"]
+let code_int8 = 0x00
+let code_int16 = 0x01
+let code_int32 = 0x02
+let code_int64 = 0x03
+let code_shared8 = 0x04
+let code_shared16 = 0x05
+let code_shared32 = 0x06
+let code_double_array32_little = 0x07
+let code_block32 = 0x08
+let code_string8 = 0x09
+let code_string32 = 0x0A
+let code_double_big = 0x0B
+let code_double_little = 0x0C
+let code_double_array8_big = 0x0D
+let code_double_array8_little = 0x0E
+let code_double_array32_big = 0x0F
+let code_codepointer = 0x10
+let code_infixpointer = 0x11
+let code_custom = 0x12
+let code_block64 = 0x13
+
+[@@@ocaml.warning "-37"]
+type code_descr =
+| CODE_INT8
+| CODE_INT16
+| CODE_INT32
+| CODE_INT64
+| CODE_SHARED8
+| CODE_SHARED16
+| CODE_SHARED32
+| CODE_DOUBLE_ARRAY32_LITTLE
+| CODE_BLOCK32
+| CODE_STRING8
+| CODE_STRING32
+| CODE_DOUBLE_BIG
+| CODE_DOUBLE_LITTLE
+| CODE_DOUBLE_ARRAY8_BIG
+| CODE_DOUBLE_ARRAY8_LITTLE
+| CODE_DOUBLE_ARRAY32_BIG
+| CODE_CODEPOINTER
+| CODE_INFIXPOINTER
+| CODE_CUSTOM
+| CODE_BLOCK64
+
+let code_max = 0x13
+
+let magic_number = "\132\149\166\190"
+
+(** Memory reification *)
+
+module LargeArray :
+sig
+ type 'a t
+ val empty : 'a t
+ val length : 'a t -> int
+ val make : int -> 'a -> 'a t
+ val get : 'a t -> int -> 'a
+ val set : 'a t -> int -> 'a -> unit
+end =
+struct
+
+ let max_length = Sys.max_array_length
+
+ type 'a t = 'a array array * 'a array
+ (** Invariants:
+ - All subarrays of the left array have length [max_length].
+ - The right array has length < [max_length].
+ *)
+
+ let empty = [||], [||]
+
+ let length (vl, vr) =
+ (max_length * Array.length vl) + Array.length vr
+
+ let make n x =
+ let k = n / max_length in
+ let r = n mod max_length in
+ let vl = Array.init k (fun _ -> Array.make max_length x) in
+ let vr = Array.make r x in
+ (vl, vr)
+
+ let get (vl, vr) n =
+ let k = n / max_length in
+ let r = n mod max_length in
+ let len = Array.length vl in
+ if k < len then vl.(k).(r)
+ else if k == len then vr.(r)
+ else invalid_arg "index out of bounds"
+
+ let set (vl, vr) n x =
+ let k = n / max_length in
+ let r = n mod max_length in
+ let len = Array.length vl in
+ if k < len then vl.(k).(r) <- x
+ else if k == len then vr.(r) <- x
+ else invalid_arg "index out of bounds"
+
+end
+
+type repr =
+| RInt of int
+| RBlock of (int * int) (* tag × len *)
+| RString of string
+| RPointer of int
+| RCode of int
+
+type data =
+| Int of int (* value *)
+| Ptr of int (* pointer *)
+| Atm of int (* tag *)
+| Fun of int (* address *)
+
+type obj =
+| Struct of int * data array (* tag × data *)
+| String of string
+
+module type Input =
+sig
+ type t
+ val input_byte : t -> int
+ val input_binary_int : t -> int
+end
+
+module type S =
+sig
+ type input
+ val parse : input -> (data * obj LargeArray.t)
+end
+
+module Make(M : Input) =
+struct
+
+open M
+
+type input = M.t
+
+let current_offset = ref 0
+
+let input_byte chan =
+ let () = incr current_offset in
+ input_byte chan
+
+let input_binary_int chan =
+ let () = current_offset := !current_offset + 4 in
+ input_binary_int chan
+
+let input_char chan = Char.chr (input_byte chan)
+let input_string len chan = String.init len (fun _ -> input_char chan)
+
+let parse_header chan =
+ let () = current_offset := 0 in
+ let magic = input_string 4 chan in
+ let length = input_binary_int chan in
+ let objects = input_binary_int chan in
+ let size32 = input_binary_int chan in
+ let size64 = input_binary_int chan in
+ (magic, length, size32, size64, objects)
+
+let input_int8s chan =
+ let i = input_byte chan in
+ if i land 0x80 = 0
+ then i
+ else i lor ((-1) lsl 8)
+
+let input_int8u = input_byte
+
+let input_int16s chan =
+ let i = input_byte chan in
+ let j = input_byte chan in
+ let ans = (i lsl 8) lor j in
+ if i land 0x80 = 0
+ then ans
+ else ans lor ((-1) lsl 16)
+
+let input_int16u chan =
+ let i = input_byte chan in
+ let j = input_byte chan in
+ (i lsl 8) lor j
+
+let input_int32s chan =
+ let i = input_byte chan in
+ let j = input_byte chan in
+ let k = input_byte chan in
+ let l = input_byte chan in
+ let ans = (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l in
+ if i land 0x80 = 0
+ then ans
+ else ans lor ((-1) lsl 31)
+
+let input_int32u chan =
+ let i = input_byte chan in
+ let j = input_byte chan in
+ let k = input_byte chan in
+ let l = input_byte chan in
+ (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l
+
+let input_int64s chan =
+ let i = input_byte chan in
+ let j = input_byte chan in
+ let k = input_byte chan in
+ let l = input_byte chan in
+ let m = input_byte chan in
+ let n = input_byte chan in
+ let o = input_byte chan in
+ let p = input_byte chan in
+ let ans =
+ (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor
+ (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor p
+ in
+ if i land 0x80 = 0
+ then ans
+ else ans lor ((-1) lsl 63)
+
+let input_int64u chan =
+ let i = input_byte chan in
+ let j = input_byte chan in
+ let k = input_byte chan in
+ let l = input_byte chan in
+ let m = input_byte chan in
+ let n = input_byte chan in
+ let o = input_byte chan in
+ let p = input_byte chan in
+ (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor
+ (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor p
+
+let input_header32 chan =
+ let i = input_byte chan in
+ let j = input_byte chan in
+ let k = input_byte chan in
+ let l = input_byte chan in
+ let tag = l in
+ let len = (i lsl 14) lor (j lsl 6) lor (k lsr 2) in
+ (tag, len)
+
+let input_header64 chan =
+ let i = input_byte chan in
+ let j = input_byte chan in
+ let k = input_byte chan in
+ let l = input_byte chan in
+ let m = input_byte chan in
+ let n = input_byte chan in
+ let o = input_byte chan in
+ let p = input_byte chan in
+ let tag = p in
+ let len =
+ (i lsl 46) lor (j lsl 38) lor (k lsl 30) lor (l lsl 22) lor
+ (m lsl 14) lor (n lsl 6) lor (o lsr 2)
+ in
+ (tag, len)
+
+let parse_object chan =
+ let data = input_byte chan in
+ if prefix_small_block <= data then
+ let tag = data land 0x0F in
+ let len = (data lsr 4) land 0x07 in
+ RBlock (tag, len)
+ else if prefix_small_int <= data then
+ RInt (data land 0x3F)
+ else if prefix_small_string <= data then
+ let len = data land 0x1F in
+ RString (input_string len chan)
+ else if data > code_max then
+ assert false
+ else match (Obj.magic data) with
+ | CODE_INT8 ->
+ RInt (input_int8s chan)
+ | CODE_INT16 ->
+ RInt (input_int16s chan)
+ | CODE_INT32 ->
+ RInt (input_int32s chan)
+ | CODE_INT64 ->
+ RInt (input_int64s chan)
+ | CODE_SHARED8 ->
+ RPointer (input_int8u chan)
+ | CODE_SHARED16 ->
+ RPointer (input_int16u chan)
+ | CODE_SHARED32 ->
+ RPointer (input_int32u chan)
+ | CODE_BLOCK32 ->
+ RBlock (input_header32 chan)
+ | CODE_BLOCK64 ->
+ RBlock (input_header64 chan)
+ | CODE_STRING8 ->
+ let len = input_int8u chan in
+ RString (input_string len chan)
+ | CODE_STRING32 ->
+ let len = input_int32u chan in
+ RString (input_string len chan)
+ | CODE_CODEPOINTER ->
+ let addr = input_int32u chan in
+ for _i = 0 to 15 do ignore (input_byte chan); done;
+ RCode addr
+ | CODE_DOUBLE_ARRAY32_LITTLE
+ | CODE_DOUBLE_BIG
+ | CODE_DOUBLE_LITTLE
+ | CODE_DOUBLE_ARRAY8_BIG
+ | CODE_DOUBLE_ARRAY8_LITTLE
+ | CODE_DOUBLE_ARRAY32_BIG
+ | CODE_INFIXPOINTER
+ | CODE_CUSTOM ->
+ Printf.eprintf "Unhandled code %04x\n%!" data; assert false
+
+let parse chan =
+ let (magic, len, _, _, size) = parse_header chan in
+ let () = assert (magic = magic_number) in
+ let memory = LargeArray.make size (Struct ((-1), [||])) in
+ let current_object = ref 0 in
+ let fill_obj = function
+ | RPointer n ->
+ let data = Ptr (!current_object - n) in
+ data, None
+ | RInt n ->
+ let data = Int n in
+ data, None
+ | RString s ->
+ let data = Ptr !current_object in
+ let () = LargeArray.set memory !current_object (String s) in
+ let () = incr current_object in
+ data, None
+ | RBlock (tag, 0) ->
+ (* Atoms are never shared *)
+ let data = Atm tag in
+ data, None
+ | RBlock (tag, len) ->
+ let data = Ptr !current_object in
+ let nblock = Array.make len (Atm (-1)) in
+ let () = LargeArray.set memory !current_object (Struct (tag, nblock)) in
+ let () = incr current_object in
+ data, Some nblock
+ | RCode addr ->
+ let data = Fun addr in
+ data, None
+ in
+
+ let rec fill block off accu =
+ if Array.length block = off then
+ match accu with
+ | [] -> ()
+ | (block, off) :: accu -> fill block off accu
+ else
+ let data, nobj = fill_obj (parse_object chan) in
+ let () = block.(off) <- data in
+ let block, off, accu = match nobj with
+ | None -> block, succ off, accu
+ | Some nblock -> nblock, 0, ((block, succ off) :: accu)
+ in
+ fill block off accu
+ in
+ let ans = [|Atm (-1)|] in
+ let () = fill ans 0 [] in
+ (ans.(0), memory)
+
+end
+
+module IChannel =
+struct
+ type t = in_channel
+ let input_byte = Pervasives.input_byte
+ let input_binary_int = Pervasives.input_binary_int
+end
+
+module IString =
+struct
+ type t = (string * int ref)
+
+ let input_byte (s, off) =
+ let ans = Char.code (s.[!off]) in
+ let () = incr off in
+ ans
+
+ let input_binary_int chan =
+ let i = input_byte chan in
+ let j = input_byte chan in
+ let k = input_byte chan in
+ let l = input_byte chan in
+ let ans = (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l in
+ if i land 0x80 = 0
+ then ans
+ else ans lor ((-1) lsl 31)
+
+end
+
+module PChannel = Make(IChannel)
+module PString = Make(IString)
+
+let parse_channel = PChannel.parse
+let parse_string s = PString.parse (s, ref 0)
+
+let instantiate (p, mem) =
+ let len = LargeArray.length mem in
+ let ans = LargeArray.make len (Obj.repr 0) in
+ (* First pass: initialize the subobjects *)
+ for i = 0 to len - 1 do
+ let obj = match LargeArray.get mem i with
+ | Struct (tag, blk) -> Obj.new_block tag (Array.length blk)
+ | String str -> Obj.repr str
+ in
+ LargeArray.set ans i obj
+ done;
+ let get_data = function
+ | Int n -> Obj.repr n
+ | Ptr p -> LargeArray.get ans p
+ | Atm tag -> Obj.new_block tag 0
+ | Fun _ -> assert false (* We shouldn't serialize closures *)
+ in
+ (* Second pass: set the pointers *)
+ for i = 0 to len - 1 do
+ match LargeArray.get mem i with
+ | Struct (_, blk) ->
+ let obj = LargeArray.get ans i in
+ for k = 0 to Array.length blk - 1 do
+ Obj.set_field obj k (get_data blk.(k))
+ done
+ | String _ -> ()
+ done;
+ get_data p
diff --git a/checker/analyze.mli b/checker/analyze.mli
new file mode 100644
index 0000000000..d7770539df
--- /dev/null
+++ b/checker/analyze.mli
@@ -0,0 +1,51 @@
+type data =
+| Int of int
+| Ptr of int
+| Atm of int (* tag *)
+| Fun of int (* address *)
+
+type obj =
+| Struct of int * data array (* tag × data *)
+| String of string
+
+module LargeArray :
+sig
+ type 'a t
+ val empty : 'a t
+ val length : 'a t -> int
+ val make : int -> 'a -> 'a t
+ val get : 'a t -> int -> 'a
+ val set : 'a t -> int -> 'a -> unit
+end
+(** A data structure similar to arrays but allowing to overcome the 2^22 length
+ limitation on 32-bit architecture. *)
+
+val parse_channel : in_channel -> (data * obj LargeArray.t)
+val parse_string : string -> (data * obj LargeArray.t)
+
+(** {6 Functorized version} *)
+
+module type Input =
+sig
+ type t
+ val input_byte : t -> int
+ (** Input a single byte *)
+
+ val input_binary_int : t -> int
+ (** Input a big-endian 31-bits signed integer *)
+end
+(** Type of inputs *)
+
+module type S =
+sig
+ type input
+ val parse : input -> (data * obj LargeArray.t)
+ (** Return the entry point and the reification of the memory out of a
+ marshalled structure. *)
+end
+
+module Make (M : Input) : S with type input = M.t
+(** Functorized version of the previous code. *)
+
+val instantiate : data * obj LargeArray.t -> Obj.t
+(** Create the OCaml object out of the reified representation. *)
diff --git a/checker/check.ml b/checker/check.ml
new file mode 100644
index 0000000000..30437e8bd0
--- /dev/null
+++ b/checker/check.ml
@@ -0,0 +1,421 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open Names
+
+let chk_pp = Feedback.msg_notice
+
+let pr_dirpath dp = str (DirPath.to_string dp)
+let default_root_prefix = DirPath.empty
+let split_dirpath d =
+ 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 }
+
+type object_file =
+| PhysicalFile of CUnix.physical_path
+| LogicalFile of section_path
+
+let dir_of_path p =
+ DirPath.make (List.map Id.of_string p.dirpath)
+let path_of_dirpath dir =
+ match DirPath.repr dir with
+ [] -> failwith "path_of_dirpath"
+ | l::dir ->
+ {dirpath=List.map Id.to_string dir;basename=Id.to_string l}
+let pr_dirlist dp =
+ prlist_with_sep (fun _ -> str".") str (List.rev dp)
+let pr_path sp =
+ match sp.dirpath with
+ [] -> str sp.basename
+ | sl -> pr_dirlist sl ++ str"." ++ str sp.basename
+
+(************************************************************************)
+
+(*s Modules loaded in memory contain the following informations. They are
+ kept in the global table [libraries_table]. *)
+
+type compilation_unit_name = DirPath.t
+
+type seg_proofs = Constr.constr Future.computation array
+
+type library_t = {
+ library_name : compilation_unit_name;
+ library_filename : CUnix.physical_path;
+ library_compiled : Safe_typing.compiled_library;
+ library_opaques : seg_proofs;
+ library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
+ library_digest : Safe_typing.vodigest;
+ library_extra_univs : Univ.ContextSet.t }
+
+module LibraryOrdered =
+ struct
+ type t = DirPath.t
+ let compare d1 d2 =
+ Pervasives.compare
+ (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2))
+ end
+
+module LibrarySet = Set.Make(LibraryOrdered)
+module LibraryMap = Map.Make(LibraryOrdered)
+
+(* This is a map from names to loaded libraries *)
+let libraries_table = ref LibraryMap.empty
+
+(* various requests to the tables *)
+
+let find_library dir =
+ LibraryMap.find dir !libraries_table
+
+let library_full_filename dir = (find_library dir).library_filename
+
+ (* If a library is loaded several time, then the first occurrence must
+ be performed first, thus the libraries_loaded_list ... *)
+
+let register_loaded_library m =
+ libraries_table := LibraryMap.add m.library_name m !libraries_table
+
+(* Map from library names to table of opaque terms *)
+let opaque_tables = ref LibraryMap.empty
+let opaque_univ_tables = ref LibraryMap.empty
+
+let access_opaque_table dp i =
+ let t =
+ try LibraryMap.find dp !opaque_tables
+ with Not_found -> assert false
+ in
+ assert (i < Array.length t);
+ t.(i)
+
+let access_opaque_univ_table dp i =
+ try
+ let t = LibraryMap.find dp !opaque_univ_tables in
+ assert (i < Array.length t);
+ Some t.(i)
+ with Not_found -> None
+
+let () =
+ Opaqueproof.set_indirect_opaque_accessor access_opaque_table;
+ Opaqueproof.set_indirect_univ_accessor access_opaque_univ_table
+
+let check_one_lib admit senv (dir,m) =
+ let md = m.library_compiled in
+ let dig = m.library_digest in
+ (* Look up if the library is to be admitted correct. We could
+ also check if it carries a validation certificate (yet to
+ be implemented). *)
+ let senv =
+ if LibrarySet.mem dir admit then
+ (Flags.if_verbose Feedback.msg_notice
+ (str "Admitting library: " ++ pr_dirpath dir);
+ Safe_checking.unsafe_import senv md m.library_extra_univs dig)
+ else
+ (Flags.if_verbose Feedback.msg_notice
+ (str "Checking library: " ++ pr_dirpath dir);
+ Safe_checking.import senv md m.library_extra_univs dig)
+ in
+ register_loaded_library m; senv
+
+(*************************************************************************)
+(*s Load path. Mapping from physical to logical paths etc.*)
+
+type logical_path = DirPath.t
+
+let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list)
+
+
+let find_logical_path phys_dir =
+ let phys_dir = CUnix.canonical_path_name phys_dir in
+ let physical, logical = !load_paths in
+ match List.filter2 (fun p d -> p = phys_dir) physical logical with
+ | _,[dir] -> dir
+ | _,[] -> default_root_prefix
+ | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir^"."))
+
+let remove_load_path dir =
+ let physical, logical = !load_paths in
+ load_paths := List.filter2 (fun p d -> p <> dir) physical logical
+
+let add_load_path (phys_path,coq_path) =
+ if !Flags.debug then
+ Feedback.msg_notice (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
+ str phys_path);
+ let phys_path = CUnix.canonical_path_name phys_path in
+ let physical, logical = !load_paths in
+ match List.filter2 (fun p d -> p = phys_path) physical logical with
+ | _,[dir] ->
+ if coq_path <> dir
+ (* If this is not the default -I . to coqtop *)
+ && not
+ (phys_path = CUnix.canonical_path_name Filename.current_dir_name
+ && coq_path = default_root_prefix)
+ then
+ begin
+ (* Assume the user is concerned by library naming *)
+ if dir <> default_root_prefix then
+ Feedback.msg_warning
+ (str phys_path ++ strbrk " was previously bound to " ++
+ pr_dirpath dir ++ strbrk "; it is remapped to " ++
+ pr_dirpath coq_path);
+ remove_load_path phys_path;
+ load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
+ end
+ | _,[] ->
+ load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
+ | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path^"."))
+
+let load_paths_of_dir_path dir =
+ let physical, logical = !load_paths in
+ fst (List.filter2 (fun p d -> d = dir) physical logical)
+
+(************************************************************************)
+(*s Locate absolute or partially qualified library names in the path *)
+
+exception LibUnmappedDir
+exception LibNotFound
+
+let locate_absolute_library dir =
+ (* Search in loadpath *)
+ let pref, base = split_dirpath dir in
+ let loadpath = load_paths_of_dir_path pref in
+ if loadpath = [] then raise LibUnmappedDir;
+ try
+ let name = Id.to_string base^".vo" in
+ let _, file = System.where_in_path ~warn:false loadpath name in
+ (dir, file)
+ with Not_found ->
+ (* Last chance, removed from the file system but still in memory *)
+ try
+ (dir, library_full_filename dir)
+ with Not_found ->
+ raise LibNotFound
+
+let locate_qualified_library qid =
+ try
+ (* we assume qid is an absolute dirpath *)
+ let loadpath = load_paths_of_dir_path (dir_of_path qid) in
+ if loadpath = [] then raise LibUnmappedDir;
+ let name = qid.basename^".vo" in
+ let path, file = System.where_in_path loadpath name in
+ let dir =
+ extend_dirpath (find_logical_path path) (Id.of_string qid.basename) in
+ (* Look if loaded *)
+ try
+ (dir, library_full_filename dir)
+ with Not_found ->
+ (dir, file)
+ with Not_found -> raise LibNotFound
+
+let error_unmapped_dir qid =
+ let prefix = qid.dirpath in
+ user_err ~hdr:"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 =
+ user_err ~hdr:"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
+ | LibUnmappedDir -> error_unmapped_dir (path_of_dirpath dir)
+ | LibNotFound -> error_lib_not_found (path_of_dirpath dir)
+
+let try_locate_qualified_library lib = match lib with
+| PhysicalFile f ->
+ let () =
+ if not (System.file_exists_respecting_case "" f) then
+ error_lib_not_found { dirpath = []; basename = f; }
+ in
+ let dir = Filename.dirname f in
+ let base = Filename.chop_extension (Filename.basename f) in
+ let dir = extend_dirpath (find_logical_path dir) (Id.of_string base) in
+ (dir, f)
+| LogicalFile qid ->
+ try
+ locate_qualified_library qid
+ with
+ | LibUnmappedDir -> error_unmapped_dir qid
+ | LibNotFound -> error_lib_not_found qid
+
+(************************************************************************)
+(*s Low-level interning of libraries from files *)
+
+let raw_intern_library f =
+ System.raw_intern_state Coq_config.vo_magic_number f
+
+(************************************************************************)
+(* Internalise libraries *)
+
+type summary_disk = {
+ md_name : compilation_unit_name;
+ md_imports : compilation_unit_name array;
+ md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
+}
+
+module Dyn = Dyn.Make ()
+type obj = Dyn.t (* persistent dynamic objects *)
+type lib_objects = (Id.t * obj) list
+type library_objects = lib_objects * lib_objects
+
+type library_disk = {
+ md_compiled : Safe_typing.compiled_library;
+ md_objects : library_objects;
+}
+
+let mk_library sd md f table digest cst = {
+ library_name = sd.md_name;
+ library_filename = f;
+ library_compiled = md.md_compiled;
+ library_opaques = table;
+ library_deps = sd.md_deps;
+ library_digest = digest;
+ library_extra_univs = cst }
+
+let name_clash_message dir mdir f =
+ str ("The file " ^ f ^ " contains library") ++ spc () ++
+ pr_dirpath mdir ++ spc () ++ str "and not library" ++ spc() ++
+ pr_dirpath dir
+
+(* Dependency graph *)
+let depgraph = ref LibraryMap.empty
+
+let marshal_in_segment f ch =
+ try
+ let stop = input_binary_int ch in
+ let v = Analyze.instantiate (Analyze.parse_channel ch) in
+ let digest = Digest.input ch in
+ Obj.obj v, stop, digest
+ with _ ->
+ user_err (str "Corrupted file " ++ quote (str f))
+
+let intern_from_file (dir, f) =
+ Flags.if_verbose chk_pp (str"[intern "++str f++str" ...");
+ let (sd,md,table,opaque_csts,digest) =
+ try
+ let ch = System.with_magic_number_check raw_intern_library f in
+ let (sd:summary_disk), _, digest = marshal_in_segment f ch in
+ let (md:library_disk), _, digest = marshal_in_segment f ch in
+ let (opaque_csts:'a option), _, udg = marshal_in_segment f ch in
+ let (discharging:'a option), _, _ = marshal_in_segment f ch in
+ let (tasks:'a option), _, _ = marshal_in_segment f ch in
+ let (table:seg_proofs), pos, checksum =
+ marshal_in_segment f ch in
+ (* Verification of the final checksum *)
+ let () = close_in ch in
+ let ch = open_in_bin f in
+ if not (String.equal (Digest.channel ch pos) checksum) then
+ user_err ~hdr:"intern_from_file" (str "Checksum mismatch");
+ let () = close_in ch in
+ if dir <> sd.md_name then
+ user_err ~hdr:"intern_from_file"
+ (name_clash_message dir sd.md_name f);
+ if tasks <> None || discharging <> None then
+ user_err ~hdr:"intern_from_file"
+ (str "The file "++str f++str " contains unfinished tasks");
+ if opaque_csts <> None then begin
+ chk_pp (str " (was a vio file) ");
+ Option.iter (fun (_,_,b) -> if not b then
+ user_err ~hdr:"intern_from_file"
+ (str "The file "++str f++str " is still a .vio"))
+ opaque_csts;
+ Validate.validate !Flags.debug Values.v_univopaques opaque_csts;
+ end;
+ (* Verification of the unmarshalled values *)
+ Validate.validate !Flags.debug Values.v_libsum sd;
+ Validate.validate !Flags.debug Values.v_lib md;
+ Validate.validate !Flags.debug Values.v_opaques table;
+ Flags.if_verbose chk_pp (str" done]" ++ fnl ());
+ let digest =
+ if opaque_csts <> None then Safe_typing.Dvivo (digest,udg)
+ else (Safe_typing.Dvo_or_vi digest) in
+ sd,md,table,opaque_csts,digest
+ with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in
+ depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
+ opaque_tables := LibraryMap.add sd.md_name table !opaque_tables;
+ Option.iter (fun (opaque_csts,_,_) ->
+ opaque_univ_tables :=
+ LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables)
+ opaque_csts;
+ let extra_cst =
+ Option.default Univ.ContextSet.empty
+ (Option.map (fun (_,cs,_) -> cs) opaque_csts) in
+ mk_library sd md f table digest extra_cst
+
+let get_deps (dir, f) =
+ try LibraryMap.find dir !depgraph
+ with Not_found ->
+ let _ = intern_from_file (dir,f) in
+ LibraryMap.find dir !depgraph
+
+(* Read a compiled library and all dependencies, in reverse order.
+ Do not include files that are already in the context. *)
+let rec intern_library seen (dir, f) needed =
+ if LibrarySet.mem dir seen then failwith "Recursive dependencies!";
+ (* Look if in the current logical environment *)
+ try let _ = find_library dir in needed
+ with Not_found ->
+ (* Look if already listed and consequently its dependencies too *)
+ if List.mem_assoc_f DirPath.equal dir needed then needed
+ else
+ (* [dir] is an absolute name which matches [f] which must be in loadpath *)
+ let m = intern_from_file (dir,f) in
+ let seen' = LibrarySet.add dir seen in
+ let deps =
+ Array.map (fun (d,_) -> try_locate_absolute_library d) m.library_deps
+ in
+ (dir,m) :: Array.fold_right (intern_library seen') deps needed
+
+(* Compute the reflexive transitive dependency closure *)
+let rec fold_deps seen ff (dir,f) (s,acc) =
+ if LibrarySet.mem dir seen then failwith "Recursive dependencies!";
+ if LibrarySet.mem dir s then (s,acc)
+ else
+ let deps = get_deps (dir,f) in
+ let deps = Array.map (fun (d,_) -> try_locate_absolute_library d) deps in
+ let seen' = LibrarySet.add dir seen in
+ let (s',acc') = Array.fold_right (fold_deps seen' ff) deps (s,acc) in
+ (LibrarySet.add dir s', ff dir acc')
+
+and fold_deps_list seen ff modl needed =
+ List.fold_right (fold_deps seen ff) modl needed
+
+let fold_deps_list ff modl acc =
+ snd (fold_deps_list LibrarySet.empty ff modl (LibrarySet.empty,acc))
+
+let recheck_library senv ~norec ~admit ~check =
+ let ml = List.map try_locate_qualified_library check in
+ let nrl = List.map try_locate_qualified_library norec in
+ let al = List.map try_locate_qualified_library admit in
+ let needed = List.rev
+ (List.fold_right (intern_library LibrarySet.empty) (ml@nrl) []) in
+ (* first compute the closure of norec, remove closure of check,
+ add closure of admit, and finally remove norec and check *)
+ let nochk = fold_deps_list LibrarySet.add nrl LibrarySet.empty in
+ let nochk = fold_deps_list LibrarySet.remove ml nochk in
+ let nochk = fold_deps_list LibrarySet.add al nochk in
+ (* explicitly required modules cannot be skipped... *)
+ let nochk =
+ List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in
+ (* *)
+ Flags.if_verbose Feedback.msg_notice (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
+ prlist
+ (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
+ let senv = List.fold_left (check_one_lib nochk) senv needed in
+ Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked");
+ senv
diff --git a/checker/check.mli b/checker/check.mli
new file mode 100644
index 0000000000..39cc93c060
--- /dev/null
+++ b/checker/check.mli
@@ -0,0 +1,33 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open CUnix
+open Names
+open Safe_typing
+
+type section_path = {
+ dirpath : string list;
+ basename : string;
+}
+
+type object_file =
+| PhysicalFile of physical_path
+| LogicalFile of section_path
+
+type logical_path = DirPath.t
+
+val default_root_prefix : DirPath.t
+
+val add_load_path : physical_path * logical_path -> unit
+
+val recheck_library : safe_environment ->
+ norec:object_file list ->
+ admit:object_file list ->
+ check:object_file list -> safe_environment
diff --git a/checker/check.mllib b/checker/check.mllib
new file mode 100644
index 0000000000..d47a93c70d
--- /dev/null
+++ b/checker/check.mllib
@@ -0,0 +1,11 @@
+Analyze
+
+CheckInductive
+Mod_checking
+CheckTypes
+Safe_checking
+Values
+Validate
+Check
+Check_stat
+Checker
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
new file mode 100644
index 0000000000..c823db956d
--- /dev/null
+++ b/checker/checkInductive.ml
@@ -0,0 +1,162 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Declarations
+open Environ
+open Names
+open Univ
+open Util
+
+[@@@ocaml.warning "+9+27"]
+
+exception InductiveMismatch of MutInd.t * string
+
+let check mind field b = if not b then raise (InductiveMismatch (mind,field))
+
+let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
+ let open Entries in
+ let nparams = List.length mb.mind_params_ctxt in (* include letins *)
+ let mind_entry_record = match mb.mind_record with
+ | NotRecord -> None | FakeRecord -> Some None
+ | PrimRecord data -> Some (Some (Array.map pi1 data))
+ in
+ let mind_entry_universes = match mb.mind_universes with
+ | Monomorphic_ind univs -> Monomorphic_ind_entry univs
+ | Polymorphic_ind auctx -> Polymorphic_ind_entry (AUContext.names auctx, AUContext.repr auctx)
+ | Cumulative_ind auctx ->
+ Cumulative_ind_entry (AUContext.names (ACumulativityInfo.univ_context auctx),
+ ACumulativityInfo.repr auctx)
+ in
+ let mind_entry_inds = Array.map_to_list (fun ind ->
+ let mind_entry_arity, mind_entry_template = match ind.mind_arity with
+ | RegularArity ar ->
+ let ctx, arity = Term.decompose_prod_n_assum nparams ar.mind_user_arity in
+ ignore ctx; (* we will check that the produced user_arity is equal to the input *)
+ arity, false
+ | TemplateArity ar ->
+ let ctx = ind.mind_arity_ctxt in
+ let ctx = List.firstn (List.length ctx - nparams) ctx in
+ Term.mkArity (ctx, Sorts.sort_of_univ ar.template_level), true
+ in
+ {
+ mind_entry_typename = ind.mind_typename;
+ mind_entry_arity;
+ mind_entry_template;
+ mind_entry_consnames = Array.to_list ind.mind_consnames;
+ mind_entry_lc = Array.map_to_list (fun c ->
+ let ctx, c = Term.decompose_prod_n_assum nparams c in
+ ignore ctx; (* we will check that the produced user_lc is equal to the input *)
+ c
+ ) ind.mind_user_lc;
+ })
+ mb.mind_packets
+ in
+ {
+ mind_entry_record;
+ mind_entry_finite = mb.mind_finite;
+ mind_entry_params = mb.mind_params_ctxt;
+ mind_entry_inds;
+ mind_entry_universes;
+ mind_entry_private = mb.mind_private;
+ }
+
+let check_arity env ar1 ar2 = match ar1, ar2 with
+ | RegularArity ar, RegularArity {mind_user_arity;mind_sort} ->
+ Constr.equal ar.mind_user_arity mind_user_arity &&
+ Sorts.equal ar.mind_sort mind_sort
+ | TemplateArity ar, TemplateArity {template_param_levels;template_level} ->
+ List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels &&
+ UGraph.check_leq (universes env) template_level ar.template_level
+ (* template_level is inferred by indtypes, so functor application can produce a smaller one *)
+ | (RegularArity _ | TemplateArity _), _ -> false
+
+(* Use [eq_ind_chk] because when we rebuild the recargs we have lost
+ the knowledge of who is the canonical version.
+ Try with to see test-suite/coqchk/include.v *)
+let eq_recarg a1 a2 = match a1, a2 with
+ | Norec, Norec -> true
+ | Mrec i1, Mrec i2 -> eq_ind_chk i1 i2
+ | Imbr i1, Imbr i2 -> eq_ind_chk i1 i2
+ | (Norec | Mrec _ | Imbr _), _ -> false
+
+let eq_reloc_tbl = Array.equal (fun x y -> Int.equal (fst x) (fst y) && Int.equal (snd x) (snd y))
+
+let check_packet env mind ind
+ { mind_typename; mind_arity_ctxt; mind_arity; mind_consnames; mind_user_lc;
+ mind_nrealargs; mind_nrealdecls; mind_kelim; mind_nf_lc;
+ mind_consnrealargs; mind_consnrealdecls; mind_recargs; mind_nb_constant;
+ mind_nb_args; mind_reloc_tbl } =
+ let check = check mind in
+
+ ignore mind_typename; (* passed through *)
+ check "mind_arity_ctxt" (Context.Rel.equal Constr.equal ind.mind_arity_ctxt mind_arity_ctxt);
+ check "mind_arity" (check_arity env ind.mind_arity mind_arity);
+ ignore mind_consnames; (* passed through *)
+ check "mind_user_lc" (Array.equal Constr.equal ind.mind_user_lc mind_user_lc);
+ check "mind_nrealargs" Int.(equal ind.mind_nrealargs mind_nrealargs);
+ check "mind_nrealdecls" Int.(equal ind.mind_nrealdecls mind_nrealdecls);
+ check "mind_kelim" (List.equal Sorts.family_equal ind.mind_kelim mind_kelim);
+
+ check "mind_nf_lc" (Array.equal Constr.equal ind.mind_nf_lc mind_nf_lc);
+ (* NB: here syntactic equality is not just an optimisation, we also
+ care about the shape of the terms *)
+
+ check "mind_consnrealargs" (Array.equal Int.equal ind.mind_consnrealargs mind_consnrealargs);
+ check "mind_consnrealdecls" (Array.equal Int.equal ind.mind_consnrealdecls mind_consnrealdecls);
+
+ check "mind_recargs" (Rtree.equal eq_recarg ind.mind_recargs mind_recargs);
+
+ check "mind_nb_args" Int.(equal ind.mind_nb_args mind_nb_args);
+ check "mind_nb_constant" Int.(equal ind.mind_nb_constant mind_nb_constant);
+ check "mind_reloc_tbl" (eq_reloc_tbl ind.mind_reloc_tbl mind_reloc_tbl);
+
+ ()
+
+let check_same_record r1 r2 = match r1, r2 with
+ | NotRecord, NotRecord | FakeRecord, FakeRecord -> true
+ | PrimRecord r1, PrimRecord r2 ->
+ (* The kernel doesn't care about the names, we just need to check
+ that the saved types are correct. *)
+ Array.for_all2 (fun (_,_,tys1) (_,_,tys2) ->
+ Array.equal Constr.equal tys1 tys2)
+ r1 r2
+ | (NotRecord | FakeRecord | PrimRecord _), _ -> false
+
+let check_inductive env mind mb =
+ let entry = to_entry mb in
+ let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps;
+ mind_nparams; mind_nparams_rec; mind_params_ctxt; mind_universes;
+ mind_private; mind_typing_flags; }
+ =
+ (* Locally set the oracle for further typechecking *)
+ let env = Environ.set_oracle env mb.mind_typing_flags.conv_oracle in
+ Indtypes.check_inductive env mind entry
+ in
+ let check = check mind in
+
+ Array.iter2 (check_packet env mind) mb.mind_packets mind_packets;
+ check "mind_record" (check_same_record mb.mind_record mind_record);
+ check "mind_finite" (mb.mind_finite == mind_finite);
+ check "mind_ntypes" Int.(equal mb.mind_ntypes mind_ntypes);
+ check "mind_hyps" (Context.Named.equal Constr.equal mb.mind_hyps mind_hyps);
+ check "mind_nparams" Int.(equal mb.mind_nparams mind_nparams);
+
+ check "mind_nparams_rec" (mb.mind_nparams_rec <= mind_nparams_rec);
+ (* module substitution can increase the real number of recursively
+ uniform parameters, so be tolerant and use [<=]. *)
+
+ check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt);
+ ignore mind_universes; (* Indtypes did the necessary checking *)
+ ignore mind_private; (* passed through Indtypes *)
+
+ ignore mind_typing_flags;
+ (* TODO non oracle flags *)
+
+ add_mind mind mb env
diff --git a/checker/checkInductive.mli b/checker/checkInductive.mli
new file mode 100644
index 0000000000..ab54190967
--- /dev/null
+++ b/checker/checkInductive.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Names
+open Environ
+
+exception InductiveMismatch of MutInd.t * string
+(** Some field of the inductive is different from what the kernel infers. *)
+
+(*s The following function does checks on inductive declarations. *)
+
+val check_inductive : env -> MutInd.t -> Declarations.mutual_inductive_body -> env
diff --git a/checker/checkTypes.ml b/checker/checkTypes.ml
new file mode 100644
index 0000000000..7eaa5eedd5
--- /dev/null
+++ b/checker/checkTypes.ml
@@ -0,0 +1,36 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Util
+open Term
+open Constr
+open Declarations
+open Reduction
+open Environ
+
+(* Polymorphic arities utils *)
+
+let check_kind env ar u =
+ match Constr.kind (snd (dest_prod env ar)) with
+ | Sort (Type u') when Univ.Universe.equal u' (Univ.Universe.make u) -> ()
+ | _ -> failwith "not the correct sort"
+
+let check_polymorphic_arity env params par =
+ let pl = par.template_param_levels in
+ let rec check_p env pl params =
+ let open Context.Rel.Declaration in
+ match pl, params with
+ Some u::pl, LocalAssum (na,ty)::params ->
+ check_kind env ty u;
+ check_p (push_rel (LocalAssum (na,ty)) env) pl params
+ | None::pl,d::params -> check_p (push_rel d env) pl params
+ | [], _ -> ()
+ | _ -> failwith "check_poly: not the right number of params" in
+ check_p env pl (List.rev params)
diff --git a/checker/checkTypes.mli b/checker/checkTypes.mli
new file mode 100644
index 0000000000..022f9bc603
--- /dev/null
+++ b/checker/checkTypes.mli
@@ -0,0 +1,20 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+(*i*)
+open Declarations
+open Constr
+open Environ
+(*i*)
+
+(*s Typing functions (not yet tagged as safe) *)
+
+val check_polymorphic_arity :
+ env -> rel_context -> template_arity -> unit
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
new file mode 100644
index 0000000000..57adc79475
--- /dev/null
+++ b/checker/check_stat.ml
@@ -0,0 +1,55 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Pp
+open Names
+open Declarations
+open Environ
+
+let memory_stat = ref false
+
+let print_memory_stat () =
+ if !memory_stat then begin
+ Format.printf "total heap size = %d kbytes\n" (CObj.heap_size_kb ());
+ Format.print_newline();
+ Format.print_flush()
+ end
+
+let output_context = ref false
+
+let pr_engagement env =
+ begin
+ match engagement env with
+ | ImpredicativeSet -> str "Theory: Set is impredicative"
+ | PredicativeSet -> str "Theory: Set is predicative"
+ end
+
+let is_ax _ cb = not (Declareops.constant_has_body cb)
+
+let pr_ax env =
+ let axs = fold_constants (fun c ce acc -> if is_ax c ce then c::acc else acc) env [] in
+ if axs = [] then
+ str "Axioms: <none>"
+ else
+ hv 2 (str "Axioms:" ++ fnl() ++ prlist_with_sep fnl Constant.print axs)
+
+let print_context env =
+ if !output_context then begin
+ Feedback.msg_notice
+ (hov 0
+ (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
+ str"===============" ++ fnl() ++ fnl() ++
+ str "* " ++ hov 0 (pr_engagement env ++ fnl()) ++ fnl() ++
+ str "* " ++ hov 0 (pr_ax env)));
+ end
+
+let stats env =
+ print_context env;
+ print_memory_stat ()
diff --git a/checker/check_stat.mli b/checker/check_stat.mli
new file mode 100644
index 0000000000..b094da1c44
--- /dev/null
+++ b/checker/check_stat.mli
@@ -0,0 +1,13 @@
+(************************************************************************)
+(* * 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 memory_stat : bool ref
+val output_context : bool ref
+
+val stats : Environ.env -> unit
diff --git a/checker/checker.ml b/checker/checker.ml
new file mode 100644
index 0000000000..167258f8bb
--- /dev/null
+++ b/checker/checker.ml
@@ -0,0 +1,408 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open System
+open Names
+open Check
+open Environ
+
+let () = at_exit flush_all
+
+let fatal_error info anomaly =
+ flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]@\n%!" Pp.pp_with info; flush_all ();
+ exit (if anomaly then 129 else 1)
+
+let coq_root = Id.of_string "Coq"
+let parse_dir s =
+ let len = String.length s in
+ let rec decoupe_dirs dirs n =
+ if n>=len then dirs else
+ let pos =
+ try
+ String.index_from s n '.'
+ with Not_found -> len
+ in
+ let dir = String.sub s n (pos-n) in
+ decoupe_dirs (dir::dirs) (pos+1)
+ in
+ decoupe_dirs [] 0
+let dirpath_of_string s =
+ match parse_dir s with
+ [] -> Check.default_root_prefix
+ | dir -> DirPath.make (List.map Id.of_string dir)
+let path_of_string s =
+ if Filename.check_suffix s ".vo" then PhysicalFile s
+ else match parse_dir s with
+ [] -> invalid_arg "path_of_string"
+ | l::dir -> LogicalFile {dirpath=dir; basename=l}
+
+let ( / ) = Filename.concat
+
+let get_version_date () =
+ try
+ let ch = open_in (Envars.coqlib () / "revision") in
+ let ver = input_line ch in
+ let rev = input_line ch in
+ let () = close_in ch in
+ (ver,rev)
+ with _ -> (Coq_config.version,Coq_config.date)
+
+let print_header () =
+ let (ver,rev) = (get_version_date ()) in
+ Printf.printf "Welcome to Chicken %s (%s)\n" ver rev;
+ flush stdout
+
+(* Adding files to Coq loadpath *)
+
+let add_path ~unix_path:dir ~coq_root:coq_dirpath =
+ if exists_dir dir then
+ begin
+ Check.add_load_path (dir,coq_dirpath)
+ end
+ else
+ Feedback.msg_warning (str "Cannot open " ++ str dir)
+
+let convert_string d =
+ try Id.of_string d
+ with CErrors.UserError _ ->
+ Flags.if_verbose Feedback.msg_warning
+ (str "Directory " ++ str d ++ str " 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 = DirPath.repr coq_root in
+ let convert_dirs (lp, cp) =
+ try
+ 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
+ List.iter Check.add_load_path dirs;
+ Check.add_load_path (unix_path, coq_root)
+ else
+ Feedback.msg_warning (str "Cannot open " ++ str unix_path)
+
+(* By the option -include -I or -R of the command line *)
+let includes = ref []
+let push_include (s, alias) = includes := (s,alias) :: !includes
+
+let set_default_include d =
+ push_include (d, Check.default_root_prefix)
+let set_include d p =
+ let p = dirpath_of_string p in
+ push_include (d,p)
+
+(* Initializes the LoadPath *)
+let init_load_path () =
+ let coqlib = Envars.coqlib () in
+ let user_contrib = coqlib/"user-contrib" in
+ let xdg_dirs = Envars.xdg_dirs in
+ let coqpath = Envars.coqpath in
+ 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.DirPath.make[coq_root]);
+ (* then plugins *)
+ 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;
+ (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *)
+ List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix)
+ (xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)));
+ (* then directories in COQPATH *)
+ List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath;
+ (* then current directory *)
+ add_path ~unix_path:"." ~coq_root:Check.default_root_prefix;
+ (* additional loadpath, given with -I -include -R options *)
+ List.iter
+ (fun (unix_path, coq_root) -> add_rec_path ~unix_path ~coq_root)
+ (List.rev !includes);
+ includes := []
+
+
+let set_debug () = Flags.debug := true
+
+let impredicative_set = ref Declarations.PredicativeSet
+let set_impredicative_set () = impredicative_set := Declarations.ImpredicativeSet
+
+let indices_matter = ref false
+
+let make_senv () =
+ let senv = Safe_typing.empty_environment in
+ let senv = Safe_typing.set_engagement !impredicative_set senv in
+ let senv = Safe_typing.set_indices_matter !indices_matter senv in
+ let senv = Safe_typing.set_VM false senv in
+ Safe_typing.set_native_compiler false senv
+
+let admit_list = ref ([] : object_file list)
+let add_admit s =
+ admit_list := path_of_string s :: !admit_list
+
+let norec_list = ref ([] : object_file list)
+let add_norec s =
+ norec_list := path_of_string s :: !norec_list
+
+let compile_list = ref ([] : object_file list)
+let add_compile s =
+ compile_list := path_of_string s :: !compile_list
+
+(*s Parsing of the command line.
+ We no longer use [Arg.parse], in order to use share [Usage.print_usage]
+ between coqtop and coqc. *)
+
+let compile_files senv =
+ Check.recheck_library senv
+ ~norec:(List.rev !norec_list)
+ ~admit:(List.rev !admit_list)
+ ~check:(List.rev !compile_list)
+
+let version () =
+ Printf.printf "The Coq Proof Checker, version %s (%s)\n"
+ Coq_config.version Coq_config.date;
+ Printf.printf "compiled on %s\n" Coq_config.compile_date;
+ exit 0
+
+(* print the usage of coqtop (or coqc) on channel co *)
+
+let print_usage_channel co command =
+ output_string co command;
+ output_string co "coqchk options are:\n";
+ output_string co
+" -Q dir coqdir map physical dir to logical coqdir\
+\n -R dir coqdir synonymous for -Q\
+\n\
+\n\
+\n -admit module load module and dependencies without checking\
+\n -norec module check module but admit dependencies without checking\
+\n\
+\n -where print coqchk's standard library location and exit\
+\n -v print coqchk version and exit\
+\n -boot boot mode\
+\n -o, --output-context print the list of assumptions\
+\n -m, --memory print the maximum heap size\
+\n -silent disable trace of constants being checked\
+\n\
+\n -impredicative-set set sort Set impredicative\
+\n\
+\n -h, --help print this list of options\
+\n"
+
+(* print the usage on standard error *)
+
+let print_usage = print_usage_channel stderr
+
+let print_usage_coqtop () =
+ print_usage "Usage: coqchk <options> modules\n\n"
+
+let usage () =
+ print_usage_coqtop ();
+ flush stderr;
+ exit 1
+
+open Type_errors
+
+let anomaly_string () = str "Anomaly: "
+let report () = strbrk (". Please report at " ^ Coq_config.wwwbugtracker ^ ".")
+
+let guill s = str "\"" ++ str s ++ str "\""
+
+let where = function
+| None -> mt ()
+| Some s ->
+ if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
+
+let explain_exn = function
+ | Stream.Failure ->
+ hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
+ | Stream.Error txt ->
+ hov 0 (str "Syntax error: " ++ str txt)
+ | Sys_error msg ->
+ hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ guill msg ++ report() )
+ | UserError(s,pps) ->
+ hov 1 (str "User error: " ++ where s ++ pps)
+ | Out_of_memory ->
+ hov 0 (str "Out of memory")
+ | Stack_overflow ->
+ hov 0 (str "Stack overflow")
+ | Match_failure(filename,pos1,pos2) ->
+ hov 1 (anomaly_string () ++ str "Match failure in file " ++
+ guill filename ++ str " at line " ++ int pos1 ++
+ str " character " ++ int pos2 ++ report ())
+ | Not_found ->
+ hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ())
+ | Failure s ->
+ hov 0 (str "Failure: " ++ str s ++ report ())
+ | Invalid_argument s ->
+ hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ guill s ++ report ())
+ | Sys.Break ->
+ hov 0 (fnl () ++ str "User interrupt.")
+ | Univ.UniverseInconsistency i ->
+ let msg =
+ if !Flags.debug then
+ str "." ++ spc() ++
+ Univ.explain_universe_inconsistency Univ.Level.pr i
+ else
+ mt() in
+ hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".")
+ | TypeError(ctx,te) ->
+ hov 0 (str "Type error: " ++
+ (match te with
+ | UnboundRel i -> str"UnboundRel " ++ int i
+ | UnboundVar v -> str"UnboundVar" ++ str(Names.Id.to_string v)
+ | NotAType _ -> str"NotAType"
+ | BadAssumption _ -> str"BadAssumption"
+ | ReferenceVariables _ -> str"ReferenceVariables"
+ | ElimArity _ -> str"ElimArity"
+ | CaseNotInductive _ -> str"CaseNotInductive"
+ | WrongCaseInfo _ -> str"WrongCaseInfo"
+ | NumberBranches _ -> str"NumberBranches"
+ | IllFormedBranch _ -> str"IllFormedBranch"
+ | Generalization _ -> str"Generalization"
+ | ActualType _ -> str"ActualType"
+ | CantApplyBadType ((n,a,b),{uj_val = hd; uj_type = hdty},args) ->
+ let pp_arg i judge =
+ hv 1 (str"arg " ++ int (i+1) ++ str"= " ++
+ Constr.debug_print judge.uj_val ++
+ str ",type= " ++ Constr.debug_print judge.uj_type) ++ fnl ()
+ in
+ Feedback.msg_notice (str"====== ill-typed term ====" ++ fnl () ++
+ hov 2 (str"application head= " ++ Constr.debug_print hd) ++ fnl () ++
+ hov 2 (str"head type= " ++ Constr.debug_print hdty) ++ fnl () ++
+ str"arguments:" ++ fnl () ++ hv 1 (prvecti pp_arg args));
+ Feedback.msg_notice (str"====== type error ====@" ++ fnl () ++
+ Constr.debug_print b ++ fnl () ++
+ str"is not convertible with" ++ fnl () ++
+ Constr.debug_print a ++ fnl ());
+ Feedback.msg_notice (str"====== universes ====" ++ fnl () ++
+ (UGraph.pr_universes Univ.Level.pr
+ (ctx.Environ.env_stratification.Environ.env_universes)));
+ str "CantApplyBadType at argument " ++ int n
+ | CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
+ | IllFormedRecBody _ -> str"IllFormedRecBody"
+ | IllTypedRecBody _ -> str"IllTypedRecBody"
+ | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"
+ | UndeclaredUniverse _ -> str"UndeclaredUniverse"))
+
+ | Indtypes.InductiveError e ->
+ hov 0 (str "Error related to inductive types")
+(* let ctx = Check.get_env() in
+ hov 0
+ (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*)
+
+ | CheckInductive.InductiveMismatch (mind,field) ->
+ hov 0 (MutInd.print mind ++ str ": field " ++ str field ++ str " is incorrect.")
+
+ | Assert_failure (s,b,e) ->
+ hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
+ (if s = "" then mt ()
+ else
+ (str "(file \"" ++ str s ++ str "\", line " ++ int b ++
+ str ", characters " ++ int e ++ str "-" ++
+ int (e+6) ++ str ")")) ++
+ report ())
+ | e -> CErrors.print e (* for anomalies and other uncaught exceptions *)
+
+let deprecated flag =
+ Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag))
+
+let parse_args argv =
+ let rec parse = function
+ | [] -> ()
+ | "-impredicative-set" :: rem ->
+ set_impredicative_set (); parse rem
+
+ | "-indices-matter" :: rem ->
+ indices_matter:=true; parse rem
+
+ | "-coqlib" :: s :: rem ->
+ if not (exists_dir s) then
+ fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false;
+ Envars.set_user_coqlib s;
+ parse rem
+
+ | ("-I"|"-include") :: d :: "-as" :: p :: rem -> deprecated "-I"; set_include d p; parse rem
+ | ("-I"|"-include") :: d :: "-as" :: [] -> usage ()
+ | ("-I"|"-include") :: d :: rem -> deprecated "-I"; set_default_include d; parse rem
+ | ("-I"|"-include") :: [] -> usage ()
+
+ | "-Q" :: d :: p :: rem -> set_include d p;parse rem
+ | "-Q" :: ([] | [_]) -> usage ()
+
+ | "-R" :: d :: p :: rem -> set_include d p;parse rem
+ | "-R" :: ([] | [_]) -> usage ()
+
+ | "-debug" :: rem -> set_debug (); parse rem
+
+ | "-where" :: _ ->
+ Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
+ print_endline (Envars.coqlib ());
+ exit 0
+
+ | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
+
+ | ("-v"|"--version") :: _ -> version ()
+ | "-boot" :: rem -> Flags.boot := true; parse rem
+ | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem
+ | ("-o" | "--output-context") :: rem ->
+ Check_stat.output_context := true; parse rem
+
+ | "-admit" :: s :: rem -> add_admit s; parse rem
+ | "-admit" :: [] -> usage ()
+
+ | "-norec" :: s :: rem -> add_norec s; parse rem
+ | "-norec" :: [] -> usage ()
+
+ | "-silent" :: rem ->
+ Flags.quiet := true; parse rem
+
+ | s :: _ when s<>"" && s.[0]='-' ->
+ fatal_error (str "Unknown option " ++ str s) false
+ | s :: rem -> add_compile s; parse rem
+ in
+ parse (List.tl (Array.to_list argv))
+
+
+(* XXX: At some point we need to either port the checker to use the
+ feedback system or to remove its use completely. *)
+let init_with_argv argv =
+ Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
+ let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in
+ try
+ parse_args argv;
+ if !Flags.debug then Printexc.record_backtrace true;
+ Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
+ Flags.if_verbose print_header ();
+ init_load_path ();
+ make_senv ()
+ with e ->
+ fatal_error (str "Error during initialization :" ++ (explain_exn e)) (is_anomaly e)
+
+let init() = init_with_argv Sys.argv
+
+let run senv =
+ try
+ let senv = compile_files senv in
+ flush_all(); senv
+ with e ->
+ if !Flags.debug then Printexc.print_backtrace stderr;
+ fatal_error (explain_exn e) (is_anomaly e)
+
+let start () =
+ let senv = init() in
+ let senv = run senv in
+ Check_stat.stats (Safe_typing.env_of_safe_env senv);
+ exit 0
diff --git a/checker/checker.mli b/checker/checker.mli
new file mode 100644
index 0000000000..582f42589c
--- /dev/null
+++ b/checker/checker.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 start : unit -> unit
diff --git a/checker/coqchk.ml b/checker/coqchk.ml
new file mode 100644
index 0000000000..83b4ddd2d5
--- /dev/null
+++ b/checker/coqchk.ml
@@ -0,0 +1,2 @@
+
+let _ = Checker.start ()
diff --git a/checker/coqchk.mli b/checker/coqchk.mli
new file mode 100644
index 0000000000..9db9ecd12e
--- /dev/null
+++ b/checker/coqchk.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+ that does not have a corresponding .mli file *)
diff --git a/checker/dune b/checker/dune
new file mode 100644
index 0000000000..ee427d26c5
--- /dev/null
+++ b/checker/dune
@@ -0,0 +1,28 @@
+; Careful with bug https://github.com/ocaml/odoc/issues/148
+;
+; If we don't pack checker we will have a problem here due to
+; duplicate module names in the whole build.
+(library
+ (name checklib)
+ (public_name coq.checklib)
+ (synopsis "Coq's Standalone Proof Checker")
+ (modules :standard \ coqchk votour)
+ (wrapped true)
+ (libraries coq.kernel))
+
+(executable
+ (name coqchk)
+ (public_name coqchk)
+ (package coq)
+ (modules coqchk)
+ (flags :standard -open Checklib)
+ (libraries coq.checklib))
+
+(executable
+ (name votour)
+ (public_name votour)
+ (package coq)
+ (modules votour)
+ (flags :standard -open Checklib)
+ (libraries coq.checklib))
+
diff --git a/checker/include b/checker/include
new file mode 100644
index 0000000000..3ffc301724
--- /dev/null
+++ b/checker/include
@@ -0,0 +1,192 @@
+(* -*-tuareg-*- *)
+
+(* Caml script to include for debugging the checker.
+ Usage: from the checker/ directory launch ocaml toplevel and then
+ type #use"include";;
+ This command loads the relevent modules, defines some pretty
+ printers, and provides functions to interactively check modules
+ (mainly run_l and norec).
+ *)
+
+#cd "..";;
+#directory "lib";;
+#directory "kernel";;
+#directory "checker";;
+#directory "+threads";;
+
+#load "unix.cma";;
+#load"threads.cma";;
+#load "str.cma";;
+#load "gramlib.cma";;
+(*#load "toplevellib.cma";;
+
+#directory "/usr/lib/ocaml/compiler-libs/utils";;
+let _ = Clflags.recursive_types:=true;;
+*)
+#load "check.cma";;
+
+open Typeops;;
+open Check;;
+
+open Pp;;
+open CErrors;;
+open Util;;
+open Names;;
+open Term;;
+open Environ;;
+open Declarations;;
+open Mod_checking;;
+open Cic;;
+
+let pr_id id = str(string_of_id id)
+let pr_na = function Name id -> pr_id id | _ -> str"_";;
+let prdp dp = pp(str(string_of_dirpath dp));;
+(*
+let prc c = pp(Himsg.pr_lconstr_env (Check.get_env()) c);;
+let prcs cs = prc (Declarations.force cs);;
+let pru u = pp(str(Univ.string_of_universe u));;*)
+let pru u = pp(Univ.pr_uni u);;
+let prlab l = pp(str(string_of_label l));;
+let prid id = pp(pr_id id);;
+let prcon c = pp(Indtypes.prcon c);;
+let prkn kn = pp(Indtypes.prkn kn);;
+
+
+let prus g = pp(Univ.pr_universes g);;
+
+let prcstrs c =
+ let g = Univ.merge_constraints c Univ.initial_universes in
+ pp(Univ.pr_universes g);;
+(*let prcstrs c = pp(Univ.pr_constraints c);; *)
+(*
+let prenvu e =
+ let u = universes e in
+ let pu =
+ str "UNIVERSES:"++fnl()++str" "++hov 0 (Univ.pr_universes u) ++fnl() in
+ pp pu;;
+
+let prenv e =
+ let ctx1 = named_context e in
+ let ctx2 = rel_context e in
+ let pe =
+ hov 1 (str"[" ++
+ prlist_with_sep spc (fun (na,_,_) -> pr_id na) (List.rev ctx1)++
+ str"]") ++ spc() ++
+ hov 1 (str"[" ++
+ prlist_with_sep spc (fun (na,_,_) -> pr_na na) (List.rev ctx2)++
+ str"]") in
+ pp pe;;
+*)
+
+(*
+let prsub s =
+ let string_of_mp mp =
+ let s = string_of_mp mp in
+ (match mp with MPbound _ -> "#bound."|_->"")^s in
+ pp (hv 0
+ (fold_subst
+ (fun msid mp strm ->
+ str "S " ++ str (debug_string_of_msid msid) ++ str " |-> " ++
+ str (string_of_mp mp) ++ fnl() ++ strm)
+ (fun mbid mp strm ->
+ str"B " ++ str (debug_string_of_mbid mbid) ++ str " |-> " ++
+ str (string_of_mp mp) ++ fnl() ++ strm)
+ (fun mp1 mp strm ->
+ str"P " ++ str (string_of_mp mp1) ++ str " |-> " ++
+ str (string_of_mp mp) ++ fnl() ++ strm) s (mt())))
+;;
+*)
+
+#install_printer prid;;
+#install_printer prcon;;
+#install_printer prlab;;
+#install_printer prdp;;
+#install_printer prkn;;
+#install_printer pru;;
+(*
+#install_printer prc;;
+#install_printer prcs;;
+*)
+#install_printer prcstrs;;
+(*#install_printer prus;;*)
+(*#install_printer prenv;;*)
+(*#install_printer prenvu;;
+#install_printer prsub;;*)
+
+Checker.init_with_argv [|"";"-coqlib";"."|];;
+Flags.quiet := false;;
+Flags.debug := true;;
+Sys.catch_break true;;
+
+let module_of_file f =
+ let (_,mb,_,_) = Obj.magic ((intern_from_file f).library_compiled) in
+ (mb:Cic.module_body)
+;;
+let deref_mod md s =
+ let l = match md.mod_expr with
+ Struct(NoFunctor l) -> l
+ | FullStruct ->
+ (match md.mod_type with
+ NoFunctor l -> l)
+ in
+ List.assoc (label_of_id(id_of_string s)) l
+;;
+(*
+let mod_access m fld =
+ match m.mod_expr with
+ Some(SEBstruct l) -> List.assoc fld l
+ | _ -> failwith "bad structure type"
+;;
+*)
+let parse_dp 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
+ {dirpath=List.tl l; basename=List.hd l};;
+let parse_kn s =
+ let l = List.rev (Str.split(Str.regexp"\\.") s) in
+ let dp = make_dirpath(List.map id_of_string(List.tl l)) in
+ make_kn(MPfile dp) empty_dirpath (label_of_id (id_of_string (List.hd l)))
+;;
+let parse_con s =
+ let l = List.rev (Str.split(Str.regexp"\\.") s) in
+ let dp = make_dirpath(List.map id_of_string(List.tl l)) in
+ make_con(MPfile dp) empty_dirpath (label_of_id (id_of_string (List.hd l)))
+;;
+let get_mod dp =
+ lookup_module dp (Safe_typing.get_env())
+;;
+let get_mod_type dp =
+ lookup_modtype dp (Safe_typing.get_env())
+;;
+let get_cst kn =
+ lookup_constant kn (Safe_typing.get_env())
+;;
+
+let read_mod s f =
+ let lib = intern_from_file (parse_dp s,f) in
+ ((Obj.magic lib.library_compiled):
+ dir_path *
+ module_body *
+ (dir_path * Digest.t) list *
+ engagement option);;
+
+
+let expln f x =
+ try f x
+ with UserError(_,strm) as e ->
+ msgnl strm; raise e
+
+let admit_l l =
+ let l = List.map parse_sp l in
+ Check.recheck_library ~admit:l ~check:l;;
+let run_l l =
+ Check.recheck_library ~admit:[] ~check:(List.map parse_sp l);;
+let norec q =
+ Check.recheck_library ~norec:[parse_sp q] ~admit:[] ~check:[];;
+
+(*
+admit_l["Bool";"OrderedType";"DecidableType"];;
+run_l["FSetInterface"];;
+*)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
new file mode 100644
index 0000000000..086dd17e39
--- /dev/null
+++ b/checker/mod_checking.ml
@@ -0,0 +1,143 @@
+open Pp
+open Util
+open Names
+open Reduction
+open Typeops
+open Declarations
+open Environ
+
+(** {6 Checking constants } *)
+
+let check_constant_declaration env kn cb =
+ Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn);
+ (* Locally set the oracle for further typechecking *)
+ let oracle = env.env_typing_flags.conv_oracle in
+ let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in
+ (* [env'] contains De Bruijn universe variables *)
+ let poly, env' =
+ match cb.const_universes with
+ | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env
+ | Polymorphic_const auctx ->
+ let ctx = Univ.AUContext.repr auctx in
+ let env = push_context ~strict:false ctx env in
+ true, env
+ in
+ let env' = match cb.const_private_poly_univs, (cb.const_body, poly) with
+ | None, _ -> env'
+ | Some local, (OpaqueDef _, true) -> push_subgraph local env'
+ | Some _, _ -> assert false
+ in
+ let ty = cb.const_type in
+ let _ = infer_type env' ty in
+ let () =
+ match Environ.body_of_constant_body env cb with
+ | Some bd ->
+ let j = infer env' (fst bd) in
+ conv_leq env' j.uj_type ty
+ | None -> ()
+ in
+ let env =
+ if poly then add_constant kn cb env
+ else add_constant kn cb env'
+ in
+ (* Reset the value of the oracle *)
+ Environ.set_oracle env oracle
+
+(** {6 Checking modules } *)
+
+(** We currently ignore the [mod_type_alg] and [typ_expr_alg] fields.
+ The only delicate part is when [mod_expr] is an algebraic expression :
+ we need to expand it before checking it is indeed a subtype of [mod_type].
+ Fortunately, [mod_expr] cannot contain any [MEwith]. *)
+
+let lookup_module mp env =
+ try Environ.lookup_module mp env
+ with Not_found ->
+ failwith ("Unknown module: "^ModPath.to_string mp)
+
+let mk_mtb mp sign delta =
+ { mod_mp = mp;
+ mod_expr = ();
+ mod_type = sign;
+ mod_type_alg = None;
+ mod_constraints = Univ.ContextSet.empty;
+ mod_delta = delta;
+ mod_retroknowledge = ModTypeRK; }
+
+let rec check_module env mp mb =
+ Flags.if_verbose Feedback.msg_notice (str " checking module: " ++ str (ModPath.to_string mp));
+ let (_:module_signature) =
+ check_signature env mb.mod_type mb.mod_mp mb.mod_delta
+ in
+ let optsign = match mb.mod_expr with
+ |Struct sign -> Some (check_signature env sign mb.mod_mp mb.mod_delta, mb.mod_delta)
+ |Algebraic me -> Some (check_mexpression env me mb.mod_mp mb.mod_delta)
+ |Abstract|FullStruct -> None
+ in
+ match optsign with
+ |None -> ()
+ |Some (sign,delta) ->
+ let mtb1 = mk_mtb mp sign delta
+ and mtb2 = mk_mtb mp mb.mod_type mb.mod_delta in
+ let env = Modops.add_module_type mp mtb1 env in
+ let cu = Subtyping.check_subtypes env mtb1 mtb2 in
+ if not (Environ.check_constraints cu env) then
+ CErrors.user_err Pp.(str "Incorrect universe constraints for module subtyping");
+
+and check_module_type env mty =
+ Flags.if_verbose Feedback.msg_notice (str " checking module type: " ++ str (ModPath.to_string mty.mod_mp));
+ let (_:module_signature) =
+ check_signature env mty.mod_type mty.mod_mp mty.mod_delta in
+ ()
+
+and check_structure_field env mp lab res = function
+ | SFBconst cb ->
+ let c = Constant.make2 mp lab in
+ check_constant_declaration env c cb
+ | SFBmind mib ->
+ let kn = KerName.make mp lab in
+ let kn = Mod_subst.mind_of_delta_kn res kn in
+ CheckInductive.check_inductive env kn mib
+ | SFBmodule msb ->
+ let () = check_module env (MPdot(mp,lab)) msb in
+ Modops.add_module msb env
+ | SFBmodtype mty ->
+ check_module_type env mty;
+ add_modtype mty env
+
+and check_mexpr env mse mp_mse res = match mse with
+ | MEident mp ->
+ let mb = lookup_module mp env in
+ let mb = Modops.strengthen_and_subst_mb mb mp_mse false in
+ mb.mod_type, mb.mod_delta
+ | MEapply (f,mp) ->
+ let sign, delta = check_mexpr env f mp_mse res in
+ let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
+ let mtb = Modops.module_type_of_module (lookup_module mp env) in
+ let cu = Subtyping.check_subtypes env mtb farg_b in
+ if not (Environ.check_constraints cu env) then
+ CErrors.user_err Pp.(str "Incorrect universe constraints for module subtyping");
+ let subst = Mod_subst.map_mbid farg_id mp Mod_subst.empty_delta_resolver in
+ Modops.subst_signature subst fbody_b, Mod_subst.subst_codom_delta_resolver subst delta
+ | MEwith _ -> CErrors.user_err Pp.(str "Unsupported 'with' constraint in module implementation")
+
+
+and check_mexpression env sign mp_mse res = match sign with
+ | MoreFunctor (arg_id, mtb, body) ->
+ check_module_type env mtb;
+ let env' = Modops.add_module_type (MPbound arg_id) mtb env in
+ let body, delta = check_mexpression env' body mp_mse res in
+ MoreFunctor(arg_id,mtb,body), delta
+ | NoFunctor me -> check_mexpr env me mp_mse res
+
+and check_signature env sign mp_mse res = match sign with
+ | MoreFunctor (arg_id, mtb, body) ->
+ check_module_type env mtb;
+ let env' = Modops.add_module_type (MPbound arg_id) mtb env in
+ let body = check_signature env' body mp_mse res in
+ MoreFunctor(arg_id,mtb,body)
+ | NoFunctor struc ->
+ let (_:env) = List.fold_left (fun env (lab,mb) ->
+ check_structure_field env mp_mse lab res mb) env struc
+ in
+ NoFunctor struc
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
new file mode 100644
index 0000000000..6cff3e6b8c
--- /dev/null
+++ b/checker/mod_checking.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 check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit
diff --git a/checker/safe_checking.ml b/checker/safe_checking.ml
new file mode 100644
index 0000000000..6dc2953060
--- /dev/null
+++ b/checker/safe_checking.ml
@@ -0,0 +1,23 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Declarations
+open Environ
+
+let import senv clib univs digest =
+ let mb = Safe_typing.module_of_library clib in
+ let env = Safe_typing.env_of_safe_env senv in
+ let env = push_context_set ~strict:true mb.mod_constraints env in
+ let env = push_context_set ~strict:true univs env in
+ Mod_checking.check_module env mb.mod_mp mb;
+ let (_,senv) = Safe_typing.import clib univs digest senv in senv
+
+let unsafe_import senv clib univs digest =
+ let (_,senv) = Safe_typing.import clib univs digest senv in senv
diff --git a/checker/safe_checking.mli b/checker/safe_checking.mli
new file mode 100644
index 0000000000..44cd2b3a2e
--- /dev/null
+++ b/checker/safe_checking.mli
@@ -0,0 +1,16 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+(*i*)
+open Safe_typing
+(*i*)
+
+val import : safe_environment -> compiled_library -> Univ.ContextSet.t -> vodigest -> safe_environment
+val unsafe_import : safe_environment -> compiled_library -> Univ.ContextSet.t -> vodigest -> safe_environment
diff --git a/checker/validate.ml b/checker/validate.ml
new file mode 100644
index 0000000000..b85944f94f
--- /dev/null
+++ b/checker/validate.ml
@@ -0,0 +1,150 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+(* This module defines validation functions to ensure an imported
+ value (using input_value) has the correct structure. *)
+
+let rec pr_obj_rec o =
+ if Obj.is_int o then
+ Format.print_int(Obj.magic o)
+ else if Obj.is_block o then
+ let t = Obj.tag o in
+ if t > Obj.no_scan_tag then
+ if t = Obj.string_tag then
+ Format.print_string ("\""^String.escaped(Obj.magic o)^"\"")
+ else
+ Format.print_string "?"
+ else
+ (let n = Obj.size o in
+ Format.print_string ("#"^string_of_int t^"(");
+ Format.open_hvbox 0;
+ for i = 0 to n-1 do
+ pr_obj_rec (Obj.field o i);
+ if i<>n-1 then (Format.print_string ","; Format.print_cut())
+ done;
+ Format.close_box();
+ Format.print_string ")")
+ else Format.print_string "?"
+
+let pr_obj o = pr_obj_rec o; Format.print_newline()
+
+(**************************************************************************)
+(* Obj low-level validators *)
+
+type error_frame =
+| CtxAnnot of string
+| CtxType of string
+| CtxField of int
+| CtxTag of int
+
+type error_context = error_frame list
+let mt_ec : error_context = []
+let (/) (ctx:error_context) s : error_context = s::ctx
+
+exception ValidObjError of string * error_context * Obj.t
+let fail ctx o s = raise (ValidObjError(s,ctx,o))
+
+(* Check that object o is a block with tag t *)
+let val_tag t ctx o =
+ if Obj.is_block o && Obj.tag o = t then ()
+ else fail ctx o ("expected tag "^string_of_int t)
+
+let val_block ctx o =
+ if Obj.is_block o then
+ (if Obj.tag o > Obj.no_scan_tag then
+ fail ctx o "block: found no scan tag")
+ else fail ctx o "expected block obj"
+
+let val_dyn ctx o =
+ let fail () = fail ctx o "expected a Dyn.t" in
+ if not (Obj.is_block o) then fail ()
+ else if not (Obj.size o = 2) then fail ()
+ else if not (Obj.tag (Obj.field o 0) = Obj.int_tag) then fail ()
+ else ()
+
+open Values
+
+let rec val_gen v ctx o = match v with
+ | Tuple (name,vs) -> val_tuple ~name vs ctx o
+ | Sum (name,cc,vv) -> val_sum name cc vv ctx o
+ | Array v -> val_array v ctx o
+ | List v0 -> val_sum "list" 1 [|[|Annot ("elem",v0);v|]|] ctx o
+ | Opt v -> val_sum "option" 1 [|[|v|]|] ctx o
+ | Int -> if not (Obj.is_int o) then fail ctx o "expected an int"
+ | String ->
+ (try val_tag Obj.string_tag ctx o
+ with Failure _ -> fail ctx o "expected a string")
+ | Any -> ()
+ | Fail s -> fail ctx o ("unexpected object " ^ s)
+ | Annot (s,v) -> val_gen v (ctx/CtxAnnot s) o
+ | Dyn -> val_dyn ctx o
+ | Proxy { contents = v } -> val_gen v ctx o
+
+(* Check that an object is a tuple (or a record). vs is an array of
+ value representation for each field. Its size corresponds to the
+ expected size of the object. *)
+and val_tuple ?name vs ctx o =
+ let ctx = match name with
+ | Some n -> ctx/CtxType n
+ | _ -> ctx
+ in
+ let n = Array.length vs in
+ let val_fld i v =
+ val_gen v (ctx/(CtxField i)) (Obj.field o i) in
+ val_block ctx o;
+ if Obj.size o = n then Array.iteri val_fld vs
+ else
+ fail ctx o
+ ("tuple size: found "^string_of_int (Obj.size o)^
+ ", expected "^string_of_int n)
+
+(* Check that the object is either a constant constructor of tag < cc,
+ or a constructed variant. each element of vv is an array of
+ value representations of the constructor arguments.
+ The size of vv corresponds to the number of non-constant
+ constructors, and the size of vv.(i) is the expected arity of the
+ i-th non-constant constructor. *)
+and val_sum name cc vv ctx o =
+ let ctx = ctx/CtxType name in
+ if Obj.is_block o then
+ (val_block ctx o;
+ let n = Array.length vv in
+ let i = Obj.tag o in
+ let ctx' = if n=1 then ctx else ctx/CtxTag i in
+ if i < n then val_tuple vv.(i) ctx' o
+ else fail ctx' o ("sum: unexpected tag"))
+ else if Obj.is_int o then
+ let (n:int) = Obj.magic o in
+ (if n<0 || n>=cc then
+ fail ctx o ("bad constant constructor "^string_of_int n))
+ else fail ctx o "not a sum"
+
+(* Check the o is an array of values satisfying f. *)
+and val_array v ctx o =
+ val_block (ctx/CtxType "array") o;
+ for i = 0 to Obj.size o - 1 do
+ val_gen v ctx (Obj.field o i)
+ done
+
+let print_frame = function
+| CtxType t -> t
+| CtxAnnot t -> t
+| CtxField i -> Printf.sprintf "fld=%i" i
+| CtxTag i -> Printf.sprintf "tag=%i" i
+
+let validate debug v x =
+ let o = Obj.repr x in
+ try val_gen v mt_ec o
+ with ValidObjError(msg,ctx,obj) ->
+ (if debug then
+ let ctx = List.rev_map print_frame ctx in
+ print_endline ("Context: "^String.concat"/"ctx);
+ pr_obj obj);
+ failwith ("Validation failed: "^msg^" (in "^(print_frame (List.hd ctx))^")")
diff --git a/checker/validate.mli b/checker/validate.mli
new file mode 100644
index 0000000000..6c2ab8d348
--- /dev/null
+++ b/checker/validate.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 validate : bool -> Values.value -> 'a -> unit
diff --git a/checker/values.ml b/checker/values.ml
new file mode 100644
index 0000000000..1afe764ca4
--- /dev/null
+++ b/checker/values.ml
@@ -0,0 +1,375 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+(** Abstract representations of values in a vo *)
+
+(** NB: This needs updating when the types in declarations.ml and
+ their dependencies are changed. *)
+
+(** We reify here the types of values present in a vo.
+ in order to validate its structure. Maybe this reification
+ could become automatically generated someday ?
+
+ See values.mli for the meaning of each constructor.
+*)
+
+type value =
+ | Any
+ | Fail of string
+ | Tuple of string * value array
+ | Sum of string * int * value array array
+ | Array of value
+ | List of value
+ | Opt of value
+ | Int
+ | String
+ | Annot of string * value
+ | Dyn
+
+ | Proxy of value ref
+
+let fix (f : value -> value) : value =
+ let self = ref Any in
+ let ans = f (Proxy self) in
+ let () = self := ans in
+ ans
+
+(** Some pseudo-constructors *)
+
+let v_tuple name v = Tuple(name,v)
+let v_sum name cc vv = Sum(name,cc,vv)
+let v_enum name n = Sum(name,n,[||])
+
+(** Ocaml standard library *)
+
+let v_pair v1 v2 = v_tuple "*" [|v1; v2|]
+let v_bool = v_enum "bool" 2
+let v_unit = v_enum "unit" 1
+let v_ref v = v_tuple "ref" [|v|]
+
+let v_set v =
+ let rec s = Sum ("Set.t",1,
+ [|[|s; Annot("elem",v); s; Annot("bal",Int)|]|])
+ in s
+
+let v_map vk vd =
+ let rec m = Sum ("Map.t",1,
+ [|[|m; Annot("key",vk); Annot("data",vd); m; Annot("bal",Int)|]|])
+ in m
+
+let v_hset v = v_map Int (v_set v)
+let v_hmap vk vd = v_map Int (v_map vk vd)
+
+let v_pred v = v_pair v_bool (v_set v)
+
+(* lib/future *)
+let v_computation f =
+ Annot ("Future.computation",
+ v_ref
+ (v_sum "Future.comput" 0
+ [| [| Fail "Future.ongoing" |]; [| f |] |]))
+
+(** kernel/names *)
+
+let v_id = String
+let v_dp = Annot ("dirpath", List v_id)
+let v_name = v_sum "name" 1 [|[|v_id|]|]
+let v_uid = v_tuple "uniq_ident" [|Int;String;v_dp|]
+let rec v_mp = Sum("module_path",0,
+ [|[|v_dp|];
+ [|v_uid|];
+ [|v_mp;v_id|]|])
+let v_kn = v_tuple "kernel_name" [|v_mp;v_id;Int|]
+let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|]
+let v_ind = v_tuple "inductive" [|v_cst;Int|]
+let v_cons = v_tuple "constructor" [|v_ind;Int|]
+
+
+(** kernel/univ *)
+let v_level_global = v_tuple "Level.Global.t" [|v_dp;Int|]
+let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *)
+ [|(*Level*)[|v_level_global|]; (*Var*)[|Int|]|]
+let v_level = v_tuple "level" [|Int;v_raw_level|]
+let v_expr = v_tuple "levelexpr" [|v_level;Int|]
+let v_univ = List v_expr
+
+let v_cstrs =
+ Annot
+ ("Univ.constraints",
+ v_set
+ (v_tuple "univ_constraint"
+ [|v_level;v_enum "order_request" 3;v_level|]))
+
+let v_variance = v_enum "variance" 3
+
+let v_instance = Annot ("instance", Array v_level)
+let v_abs_context = v_tuple "abstract_universe_context" [|Array v_name; v_cstrs|]
+let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|]
+let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
+
+(** kernel/term *)
+
+let v_sort = v_sum "sort" 2 (*Prop, Set*) [|[|v_univ(*Type*)|]|]
+let v_sortfam = v_enum "sorts_family" 3
+
+let v_puniverses v = v_tuple "punivs" [|v;v_instance|]
+
+let v_boollist = List v_bool
+
+let v_caseinfo =
+ let v_cstyle = v_enum "case_style" 5 in
+ let v_cprint = v_tuple "case_printing" [|v_boollist;Array v_boollist;v_cstyle|] in
+ v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
+
+let v_cast = v_enum "cast_kind" 4
+
+let v_proj_repr = v_tuple "projection_repr" [|v_ind;Int;Int;v_id|]
+let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]
+
+let rec v_constr =
+ Sum ("constr",0,[|
+ [|Int|]; (* Rel *)
+ [|Fail "Var"|]; (* Var *)
+ [|Fail "Meta"|]; (* Meta *)
+ [|Fail "Evar"|]; (* Evar *)
+ [|v_sort|]; (* Sort *)
+ [|v_constr;v_cast;v_constr|]; (* Cast *)
+ [|v_name;v_constr;v_constr|]; (* Prod *)
+ [|v_name;v_constr;v_constr|]; (* Lambda *)
+ [|v_name;v_constr;v_constr;v_constr|]; (* LetIn *)
+ [|v_constr;Array v_constr|]; (* App *)
+ [|v_puniverses v_cst|]; (* Const *)
+ [|v_puniverses v_ind|]; (* Ind *)
+ [|v_puniverses v_cons|]; (* Construct *)
+ [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *)
+ [|v_fix|]; (* Fix *)
+ [|v_cofix|]; (* CoFix *)
+ [|v_proj;v_constr|] (* Proj *)
+ |])
+
+and v_prec = Tuple ("prec_declaration",
+ [|Array v_name; Array v_constr; Array v_constr|])
+and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|])
+and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|])
+
+let v_rdecl = v_sum "rel_declaration" 0 [| [|v_name; v_constr|]; (* LocalAssum *)
+ [|v_name; v_constr; v_constr|] |] (* LocalDef *)
+let v_rctxt = List v_rdecl
+
+let v_section_ctxt = v_enum "emptylist" 1
+
+
+(** kernel/mod_subst *)
+
+let v_univ_abstracted v = v_tuple "univ_abstracted" [|v;v_abs_context|]
+
+let v_delta_hint =
+ v_sum "delta_hint" 0 [|[|Int; Opt (v_univ_abstracted v_constr)|];[|v_kn|]|]
+
+let v_resolver =
+ v_tuple "delta_resolver"
+ [|v_map v_mp v_mp;
+ v_hmap v_kn v_delta_hint|]
+
+let v_mp_resolver = v_tuple "" [|v_mp;v_resolver|]
+
+let v_subst =
+ Annot ("substitution", v_map v_mp v_mp_resolver)
+
+(** kernel/lazyconstr *)
+
+let v_substituted v_a =
+ v_tuple "substituted" [|v_a; List v_subst|]
+
+let v_cstr_subst = v_substituted v_constr
+
+(** NB: Second constructor [Direct] isn't supposed to appear in a .vo *)
+let v_lazy_constr =
+ v_sum "lazy_constr" 0 [|[|List v_subst;v_dp;Int|]|]
+
+
+(** kernel/declarations *)
+
+let v_impredicative_set = v_enum "impr-set" 2
+let v_engagement = v_impredicative_set
+
+let v_conv_level =
+ v_sum "conv_level" 2 [|[|Int|]|]
+
+let v_oracle =
+ v_tuple "oracle" [|
+ v_map v_id v_conv_level;
+ v_hmap v_cst v_conv_level;
+ v_pred v_id;
+ v_pred v_cst;
+ |]
+
+let v_pol_arity =
+ v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
+
+let v_cst_def =
+ v_sum "constant_def" 0
+ [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
+
+let v_typing_flags =
+ v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
+
+let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
+
+let v_cb = v_tuple "constant_body"
+ [|v_section_ctxt;
+ v_cst_def;
+ v_constr;
+ Any;
+ v_const_univs;
+ Opt v_context_set;
+ v_bool;
+ v_typing_flags|]
+
+let v_recarg = v_sum "recarg" 1 (* Norec *)
+ [|[|v_ind|] (* Mrec *);[|v_ind|] (* Imbr *)|]
+
+let rec v_wfp = Sum ("wf_paths",0,
+ [|[|Int;Int|]; (* Rtree.Param *)
+ [|v_recarg;Array v_wfp|]; (* Rtree.Node *)
+ [|Int;Array v_wfp|] (* Rtree.Rec *)
+ |])
+
+let v_mono_ind_arity =
+ v_tuple "monomorphic_inductive_arity" [|v_constr;v_sort|]
+
+let v_ind_arity = v_sum "inductive_arity" 0
+ [|[|v_mono_ind_arity|];[|v_pol_arity|]|]
+
+let v_one_ind = v_tuple "one_inductive_body"
+ [|v_id;
+ v_rctxt;
+ v_ind_arity;
+ Array v_id;
+ Array v_constr;
+ Int;
+ Int;
+ List v_sortfam;
+ Array v_constr;
+ Array Int;
+ Array Int;
+ v_wfp;
+ Int;
+ Int;
+ Any|]
+
+let v_finite = v_enum "recursivity_kind" 3
+
+let v_record_info =
+ v_sum "record_info" 2
+ [| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_constr |]) |] |]
+
+let v_ind_pack_univs =
+ v_sum "abstract_inductive_universes" 0
+ [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|]
+
+let v_ind_pack = v_tuple "mutual_inductive_body"
+ [|Array v_one_ind;
+ v_record_info;
+ v_finite;
+ Int;
+ v_section_ctxt;
+ Int;
+ Int;
+ v_rctxt;
+ v_ind_pack_univs; (* universes *)
+ Opt v_bool;
+ v_typing_flags|]
+
+let rec v_mae =
+ Sum ("module_alg_expr",0,
+ [|[|v_mp|]; (* SEBident *)
+ [|v_mae;v_mp|]; (* SEBapply *)
+ [|v_mae; Any|] (* SEBwith *)
+ |])
+
+let rec v_sfb =
+ Sum ("struct_field_body",0,
+ [|[|v_cb|]; (* SFBconst *)
+ [|v_ind_pack|]; (* SFBmind *)
+ [|v_module|]; (* SFBmodule *)
+ [|v_modtype|] (* SFBmodtype *)
+ |])
+and v_struc = List (Tuple ("label*sfb",[|v_id;v_sfb|]))
+and v_sign =
+ Sum ("module_sign",0,
+ [|[|v_struc|]; (* NoFunctor *)
+ [|v_uid;v_modtype;v_sign|]|]) (* MoreFunctor *)
+and v_mexpr =
+ Sum ("module_expr",0,
+ [|[|v_mae|]; (* NoFunctor *)
+ [|v_uid;v_modtype;v_mexpr|]|]) (* MoreFunctor *)
+and v_impl =
+ Sum ("module_impl",2, (* Abstract, FullStruct *)
+ [|[|v_mexpr|]; (* Algebraic *)
+ [|v_sign|]|]) (* Struct *)
+and v_noimpl = v_unit
+and v_module =
+ Tuple ("module_body",
+ [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
+and v_modtype =
+ Tuple ("module_type_body",
+ [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|])
+
+(** kernel/safe_typing *)
+
+let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
+let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
+let v_compiled_lib =
+ v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|]
+
+(** Library objects *)
+
+let v_obj = Dyn
+let v_libobj = Tuple ("libobj", [|v_id;v_obj|])
+let v_libobjs = List v_libobj
+let v_libraryobjs = Tuple ("library_objects",[|v_libobjs;v_libobjs|])
+
+(** STM objects *)
+
+let v_frozen = Tuple ("frozen", [|List (v_pair Int Dyn); Opt Dyn|])
+let v_states = v_pair Any v_frozen
+let v_state = Tuple ("state", [|v_states; Any; v_bool|])
+
+let v_vcs =
+ let vcs self =
+ Tuple ("vcs",
+ [|Any; Any;
+ Tuple ("dag",
+ [|Any; Any; v_map Any (Tuple ("state_info",
+ [|Any; Any; Opt v_state; v_pair (Opt self) Any|]))
+ |])
+ |])
+ in
+ fix vcs
+
+let v_uuid = Any
+let v_request id doc =
+ Tuple ("request", [|Any; Any; doc; Any; id; String|])
+let v_tasks = List (v_pair (v_request v_uuid v_vcs) v_bool)
+let v_counters = Any
+let v_stm_seg = v_pair v_tasks v_counters
+
+(** Toplevel structures in a vo (see Cic.mli) *)
+
+let v_libsum =
+ Tuple ("summary", [|v_dp;Array v_dp;v_deps|])
+
+let v_lib =
+ Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
+
+let v_opaques = Array (v_computation v_constr)
+let v_univopaques =
+ Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|]))
diff --git a/checker/values.mli b/checker/values.mli
new file mode 100644
index 0000000000..616b69907f
--- /dev/null
+++ b/checker/values.mli
@@ -0,0 +1,48 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+type value =
+ | Any
+ (** A value that we won't check, *)
+
+ | Fail of string
+ (** A value that shouldn't be there at all, *)
+
+ | Tuple of string * value array
+ (** A debug name and sub-values in this block *)
+
+ | Sum of string * int * value array array
+ (** A debug name, a number of constant constructors, and sub-values
+ at each position of each possible constructed variant *)
+
+ | Array of value
+ | List of value
+ | Opt of value
+ | Int
+ | String
+ (** Builtin Ocaml types. *)
+
+ | Annot of string * value
+ (** Adds a debug note to the inner value *)
+
+ | Dyn
+ (** Coq's Dyn.t *)
+
+ | Proxy of value ref
+ (** Same as the inner value, used to define recursive types *)
+
+(** NB: List and Opt have their own constructors to make it easy to
+ define eg [let rec foo = List foo]. *)
+
+val v_univopaques : value
+val v_libsum : value
+val v_lib : value
+val v_opaques : value
+val v_stm_seg : value
diff --git a/checker/votour.ml b/checker/votour.ml
new file mode 100644
index 0000000000..3c088b59b5
--- /dev/null
+++ b/checker/votour.ml
@@ -0,0 +1,404 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+open Values
+
+(** {6 Interactive visit of a vo} *)
+
+let max_string_length = 1024
+
+let rec read_num max =
+ let quit () =
+ Printf.printf "\nGoodbye!\n%!";
+ exit 0 in
+ Printf.printf "# %!";
+ let l = try read_line () with End_of_file -> quit () in
+ if l = "u" then None
+ else if l = "x" then quit ()
+ else
+ match int_of_string l with
+ | v ->
+ if v < 0 || v >= max then
+ let () =
+ Printf.printf "Out-of-range input! (only %d children)\n%!" max in
+ read_num max
+ else Some v
+ | exception Failure _ ->
+ Printf.printf "Unrecognized input! <n> enters the <n>-th child, u goes up 1 level, x exits\n%!";
+ read_num max
+
+type 'a repr =
+| INT of int
+| STRING of string
+| BLOCK of int * 'a array
+| OTHER
+
+module type S =
+sig
+ type obj
+ val input : in_channel -> obj
+ val repr : obj -> obj repr
+ val size : obj -> int
+ val oid : obj -> int option
+end
+
+module ReprObj : S =
+struct
+ type obj = Obj.t * int list
+
+ let input chan =
+ let obj = input_value chan in
+ let () = CObj.register_shared_size obj in
+ (obj, [])
+
+ let repr (obj, pos) =
+ if Obj.is_block obj then
+ let tag = Obj.tag obj in
+ if tag = Obj.string_tag then STRING (Obj.magic obj)
+ else if tag < Obj.no_scan_tag then
+ let init i = (Obj.field obj i, i :: pos) in
+ let data = Array.init (Obj.size obj) init in
+ BLOCK (tag, Obj.magic data)
+ else OTHER
+ else INT (Obj.magic obj)
+
+ let size (_, p) = CObj.shared_size_of_pos p
+ let oid _ = None
+end
+
+module ReprMem : S =
+struct
+ open Analyze
+
+ type obj = data
+
+ let memory = ref LargeArray.empty
+ let sizes = ref LargeArray.empty
+ (** size, in words *)
+
+ let ws = Sys.word_size / 8
+
+ let rec init_size seen k = function
+ | Int _ | Atm _ | Fun _ -> k 0
+ | Ptr p ->
+ if LargeArray.get seen p then k 0
+ else
+ let () = LargeArray.set seen p true in
+ match LargeArray.get !memory p with
+ | Struct (tag, os) ->
+ let len = Array.length os in
+ let rec fold i accu k =
+ if i == len then k accu
+ else
+ init_size seen (fun n -> fold (succ i) (accu + 1 + n) k) os.(i)
+ in
+ fold 0 1 (fun size -> let () = LargeArray.set !sizes p size in k size)
+ | String s ->
+ let size = 2 + (String.length s / ws) in
+ let () = LargeArray.set !sizes p size in
+ k size
+
+ let size = function
+ | Int _ | Atm _ | Fun _ -> 0
+ | Ptr p -> LargeArray.get !sizes p
+
+ let repr = function
+ | Int i -> INT i
+ | Atm t -> BLOCK (t, [||])
+ | Fun _ -> OTHER
+ | Ptr p ->
+ match LargeArray.get !memory p with
+ | Struct (tag, os) -> BLOCK (tag, os)
+ | String s -> STRING s
+
+ let input ch =
+ let obj, mem = parse_channel ch in
+ let () = memory := mem in
+ let () = sizes := LargeArray.make (LargeArray.length mem) (-1) in
+ let seen = LargeArray.make (LargeArray.length mem) false in
+ let () = init_size seen ignore obj in
+ obj
+
+ let oid = function
+ | Int _ | Atm _ | Fun _ -> None
+ | Ptr p -> Some p
+end
+
+module Visit (Repr : S) :
+sig
+ val init : unit -> unit
+ val visit : Values.value -> Repr.obj -> int list -> unit
+end =
+struct
+
+(** Name of a value *)
+
+let rec get_name ?(extra=false) = function
+ |Any -> "?"
+ |Fail s -> "Invalid node: "^s
+ |Tuple (name,_) -> name
+ |Sum (name,_,_) -> name
+ |Array v -> "array"^(if extra then "/"^get_name ~extra v else "")
+ |List v -> "list"^(if extra then "/"^get_name ~extra v else "")
+ |Opt v -> "option"^(if extra then "/"^get_name ~extra v else "")
+ |Int -> "int"
+ |String -> "string"
+ |Annot (s,v) -> s^"/"^get_name ~extra v
+ |Dyn -> "<dynamic>"
+ | Proxy v -> get_name ~extra !v
+
+(** For tuples, its quite handy to display the inner 1st string (if any).
+ Cf. [structure_body] for instance *)
+
+exception TupleString of string
+let get_string_in_tuple o =
+ try
+ for i = 0 to Array.length o - 1 do
+ match Repr.repr o.(i) with
+ | STRING s ->
+ let len = min max_string_length (String.length s) in
+ raise (TupleString (Printf.sprintf " [..%s..]" (String.sub s 0 len)))
+ | _ -> ()
+ done;
+ ""
+ with TupleString s -> s
+
+(** Some details : tags, integer value for non-block, etc etc *)
+
+let rec get_details v o = match v, Repr.repr o with
+ | (String | Any), STRING s ->
+ let len = min max_string_length (String.length s) in
+ Printf.sprintf " [%s]" (String.escaped (String.sub s 0 len))
+ |Tuple (_,v), BLOCK (_, o) -> get_string_in_tuple o
+ |(Sum _|Any), BLOCK (tag, _) ->
+ Printf.sprintf " [tag=%i]" tag
+ |(Sum _|Any), INT i ->
+ Printf.sprintf " [imm=%i]" i
+ |Int, INT i -> Printf.sprintf " [imm=%i]" i
+ |Annot (s,v), _ -> get_details v o
+ |_ -> ""
+
+let get_oid obj = match Repr.oid obj with
+| None -> ""
+| Some id -> Printf.sprintf " [0x%08x]" id
+
+let node_info (v,o,p) =
+ get_name ~extra:true v ^ get_details v o ^
+ " (size "^ string_of_int (Repr.size o)^"w)" ^ get_oid o
+
+(** Children of a block : type, object, position.
+ For lists, we collect all elements of the list at once *)
+
+let access_children vs os pos =
+ if Array.length os = Array.length vs then
+ Array.mapi (fun i v -> v, os.(i), i::pos) vs
+ else raise Exit
+
+let access_list v o pos =
+ let rec loop o pos accu = match Repr.repr o with
+ | INT 0 -> List.rev accu
+ | BLOCK (0, [|hd; tl|]) ->
+ loop tl (1 :: pos) ((v, hd, 0 :: pos) :: accu)
+ | _ -> raise Exit
+ in
+ Array.of_list (loop o pos [])
+
+let access_block o = match Repr.repr o with
+| BLOCK (tag, os) -> (tag, os)
+| _ -> raise Exit
+
+(** raises Exit if the object has not the expected structure *)
+exception Forbidden
+let rec get_children v o pos = match v with
+ |Tuple (_, v) ->
+ let (_, os) = access_block o in
+ access_children v os pos
+ |Sum (_, _, vv) ->
+ begin match Repr.repr o with
+ | BLOCK (tag, os) -> access_children vv.(tag) os pos
+ | INT _ -> [||]
+ | _ -> raise Exit
+ end
+ |Array v ->
+ let (_, os) = access_block o in
+ access_children (Array.make (Array.length os) v) os pos
+ |List v -> access_list v o pos
+ |Opt v ->
+ begin match Repr.repr o with
+ | INT 0 -> [||]
+ | BLOCK (0, [|x|]) -> [|(v, x, 0 :: pos)|]
+ | _ -> raise Exit
+ end
+ | String ->
+ begin match Repr.repr o with
+ | STRING _ -> [||]
+ | _ -> raise Exit
+ end
+ | Int ->
+ begin match Repr.repr o with
+ | INT _ -> [||]
+ | _ -> raise Exit
+ end
+ |Annot (s,v) -> get_children v o pos
+ |Any -> raise Exit
+ |Dyn ->
+ begin match Repr.repr o with
+ | BLOCK (0, [|id; o|]) ->
+ let tpe = Any in
+ [|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|]
+ | _ -> raise Exit
+ end
+ |Fail s -> raise Forbidden
+ | Proxy v -> get_children !v o pos
+
+let get_children v o pos =
+ try get_children v o pos
+ with Exit -> match Repr.repr o with
+ | BLOCK (_, os) -> Array.mapi (fun i o -> Any, o, i :: pos) os
+ | _ -> [||]
+
+type info = {
+ nam : string;
+ typ : value;
+ obj : Repr.obj;
+ pos : int list
+}
+
+let stk = ref ([] : info list)
+
+let init () = stk := []
+
+let push name v o p = stk := { nam = name; typ = v; obj = o; pos = p } :: !stk
+
+exception EmptyStack
+let pop () = match !stk with
+ | i::s -> stk := s; i
+ | _ -> raise EmptyStack
+
+let rec visit v o pos =
+ Printf.printf "\nDepth %d Pos %s Context %s\n"
+ (List.length !stk)
+ (String.concat "." (List.rev_map string_of_int pos))
+ (String.concat "/" (List.rev_map (fun i -> i.nam) !stk));
+ Printf.printf "-------------\n";
+ let children = get_children v o pos in
+ let nchild = Array.length children in
+ Printf.printf "Here: %s, %d child%s\n"
+ (node_info (v,o,pos)) nchild (if nchild = 0 then "" else "ren:");
+ Array.iteri
+ (fun i vop -> Printf.printf " %d: %s\n" i (node_info vop))
+ children;
+ Printf.printf "-------------\n";
+ try
+ match read_num (Array.length children) with
+ | None -> let info = pop () in visit info.typ info.obj info.pos
+ | Some child ->
+ let v',o',pos' = children.(child) in
+ push (get_name v) v o pos;
+ visit v' o' pos'
+ with
+ | EmptyStack -> ()
+ | Forbidden -> let info = pop () in visit info.typ info.obj info.pos
+ | Failure _ | Invalid_argument _ -> visit v o pos
+
+end
+
+(** Loading the vo *)
+
+type header = {
+ magic : string;
+ (** Magic number of the marshaller *)
+ length : int;
+ (** Size on disk in bytes *)
+ size32 : int;
+ (** Size in words when loaded on 32-bit systems *)
+ size64 : int;
+ (** Size in words when loaded on 64-bit systems *)
+ objects : int;
+ (** Number of blocks defined in the marshalled structure *)
+}
+
+let dummy_header = {
+ magic = "\000\000\000\000";
+ length = 0;
+ size32 = 0;
+ size64 = 0;
+ objects = 0;
+}
+
+let parse_header chan =
+ let magic = really_input_string chan 4 in
+ let length = input_binary_int chan in
+ let objects = input_binary_int chan in
+ let size32 = input_binary_int chan in
+ let size64 = input_binary_int chan in
+ { magic; length; size32; size64; objects }
+
+type segment = {
+ name : string;
+ mutable pos : int;
+ typ : Values.value;
+ mutable header : header;
+}
+
+let make_seg name typ = { name; typ; pos = 0; header = dummy_header }
+
+let visit_vo f =
+ Printf.printf "\nWelcome to votour !\n";
+ Printf.printf "Enjoy your guided tour of a Coq .vo or .vi file\n";
+ Printf.printf "Object sizes are in words (%d bits)\n" Sys.word_size;
+ Printf.printf
+ "At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits\n\n%!";
+ let segments = [|
+ make_seg "summary" Values.v_libsum;
+ make_seg "library" Values.v_lib;
+ make_seg "univ constraints of opaque proofs" Values.v_univopaques;
+ make_seg "discharging info" (Opt Any);
+ make_seg "STM tasks" (Opt Values.v_stm_seg);
+ make_seg "opaque proofs" Values.v_opaques;
+ |] in
+ let repr =
+ if Sys.word_size = 64 then (module ReprMem : S) else (module ReprObj : S)
+ (* On 32-bit machines, representation may exceed the max size of arrays *)
+ in
+ let module Repr = (val repr : S) in
+ let module Visit = Visit(Repr) in
+ while true do
+ let ch = open_in_bin f in
+ let magic = input_binary_int ch in
+ Printf.printf "File format: %d\n%!" magic;
+ for i=0 to Array.length segments - 1 do
+ let pos = input_binary_int ch in
+ segments.(i).pos <- pos_in ch;
+ let header = parse_header ch in
+ segments.(i).header <- header;
+ seek_in ch pos;
+ ignore(Digest.input ch);
+ done;
+ Printf.printf "The file has %d segments, choose the one to visit:\n"
+ (Array.length segments);
+ Array.iteri (fun i { name; pos; header } ->
+ let size = if Sys.word_size = 64 then header.size64 else header.size32 in
+ Printf.printf " %d: %s, starting at byte %d (size %iw)\n" i name pos size)
+ segments;
+ match read_num (Array.length segments) with
+ | Some seg ->
+ seek_in ch segments.(seg).pos;
+ let o = Repr.input ch in
+ let () = Visit.init () in
+ Visit.visit segments.(seg).typ o []
+ | None -> ()
+ done
+
+let () =
+ if not !Sys.interactive then
+ Arg.parse [] visit_vo
+ ("votour: guided tour of a Coq .vo or .vi file\n"^
+ "Usage: votour file.v[oi]")
diff --git a/checker/votour.mli b/checker/votour.mli
new file mode 100644
index 0000000000..9db9ecd12e
--- /dev/null
+++ b/checker/votour.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+ that does not have a corresponding .mli file *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 09:47:36 +0000