aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml28
-rw-r--r--checker/check.mli30
-rw-r--r--checker/checker.ml11
-rw-r--r--checker/cic.mli4
-rw-r--r--checker/mod_checking.ml2
-rw-r--r--checker/values.ml6
-rw-r--r--checker/votour.ml48
7 files changed, 90 insertions, 39 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 180ca1ece1..21fdba1faf 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -22,6 +22,11 @@ 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 =
@@ -69,11 +74,6 @@ let libraries_table = ref LibraryMap.empty
let find_library dir =
LibraryMap.find dir !libraries_table
-let try_find_library dir =
- try find_library dir
- with Not_found ->
- user_err Pp.(str ("Unknown library " ^ (DirPath.to_string dir)))
-
let library_full_filename dir = (find_library dir).library_filename
(* If a library is loaded several time, then the first occurrence must
@@ -263,7 +263,17 @@ let try_locate_absolute_library dir =
| LibUnmappedDir -> error_unmapped_dir (path_of_dirpath dir)
| LibNotFound -> error_lib_not_found (path_of_dirpath dir)
-let try_locate_qualified_library qid =
+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
@@ -412,9 +422,3 @@ let recheck_library ~norec ~admit ~check =
(fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
List.iter (check_one_lib nochk) needed;
Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked")
-
-open Printf
-
-let mem s =
- let m = try_find_library s in
- h 0 (str (sprintf "%dk" (CObj.size_kb m)))
diff --git a/checker/check.mli b/checker/check.mli
new file mode 100644
index 0000000000..28ae385b5b
--- /dev/null
+++ b/checker/check.mli
@@ -0,0 +1,30 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open CUnix
+open Names
+
+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 :
+ norec:object_file list ->
+ admit:object_file list ->
+ check:object_file list -> unit
diff --git a/checker/checker.ml b/checker/checker.ml
index e960a55fd2..b2433ee364 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -40,9 +40,10 @@ let dirpath_of_string s =
[] -> Check.default_root_prefix
| dir -> DirPath.make (List.map Id.of_string dir)
let path_of_string s =
- match parse_dir s with
+ if Filename.check_suffix s ".vo" then PhysicalFile s
+ else match parse_dir s with
[] -> invalid_arg "path_of_string"
- | l::dir -> {dirpath=dir; basename=l}
+ | l::dir -> LogicalFile {dirpath=dir; basename=l}
let ( / ) = Filename.concat
@@ -144,15 +145,15 @@ let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet
let engage () = Safe_typing.set_engagement (!impredicative_set)
-let admit_list = ref ([] : section_path list)
+let admit_list = ref ([] : object_file list)
let add_admit s =
admit_list := path_of_string s :: !admit_list
-let norec_list = ref ([] : section_path list)
+let norec_list = ref ([] : object_file list)
let add_norec s =
norec_list := path_of_string s :: !norec_list
-let compile_list = ref ([] : section_path list)
+let compile_list = ref ([] : object_file list)
let add_compile s =
compile_list := path_of_string s :: !compile_list
diff --git a/checker/cic.mli b/checker/cic.mli
index 3546509641..4a0e706aa1 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -208,7 +208,7 @@ type constant_def =
| OpaqueDef of lazy_constr
type constant_universes =
- | Monomorphic_const of Univ.universe_context
+ | Monomorphic_const of Univ.ContextSet.t
| Polymorphic_const of Univ.abstract_universe_context
(** The [typing_flags] are instructions to the type-checker which
@@ -303,7 +303,7 @@ type one_inductive_body = {
}
type abstract_inductive_universes =
- | Monomorphic_ind of Univ.universe_context
+ | Monomorphic_ind of Univ.ContextSet.t
| Polymorphic_ind of Univ.abstract_universe_context
| Cumulative_ind of Univ.abstract_cumulativity_info
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 63e28448f9..4357a690ef 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -29,7 +29,7 @@ let check_constant_declaration env kn cb =
(** [env'] contains De Bruijn universe variables *)
let env' =
match cb.const_universes with
- | Monomorphic_const ctx -> push_context ~strict:true ctx env
+ | Monomorphic_const ctx -> push_context_set ~strict:true ctx env
| Polymorphic_const auctx ->
let ctx = Univ.AUContext.repr auctx in
push_context ~strict:false ctx env
diff --git a/checker/values.ml b/checker/values.ml
index 9e16c8435e..5a371164c6 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 f4b00c567a972ae950b9ed10c533fda5 checker/cic.mli
+MD5 56ac4cade33eff3d26ed5cdadb580c7e checker/cic.mli
*)
@@ -215,7 +215,7 @@ let v_projbody =
let v_typing_flags =
v_tuple "typing_flags" [|v_bool; v_bool|]
-let v_const_univs = v_sum "constant_universes" 0 [|[|v_context|]; [|v_abs_context|]|]
+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;
@@ -265,7 +265,7 @@ let v_mind_record = Annot ("mind_record",
let v_ind_pack_univs =
v_sum "abstract_inductive_universes" 0
- [|[|v_context|]; [|v_abs_context|]; [|v_abs_cum_info|]|]
+ [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|]
let v_ind_pack = v_tuple "mutual_inductive_body"
[|Array v_one_ind;
diff --git a/checker/votour.ml b/checker/votour.ml
index 0998bb94b1..b7c898232b 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -10,6 +10,8 @@ open Values
(** {6 Interactive visit of a vo} *)
+let max_string_length = 1024
+
let rec read_num max =
let quit () =
Printf.printf "\nGoodbye!\n%!";
@@ -81,22 +83,25 @@ struct
let ws = Sys.word_size / 8
- let rec init_size seen = function
- | Int _ | Atm _ | Fun _ -> 0
+ let rec init_size seen k = function
+ | Int _ | Atm _ | Fun _ -> k 0
| Ptr p ->
- if seen.(p) then 0
+ if seen.(p) then k 0
else
let () = seen.(p) <- true in
match (!memory).(p) with
| Struct (tag, os) ->
- let fold accu o = accu + 1 + init_size seen o in
- let size = Array.fold_left fold 1 os in
- let () = (!sizes).(p) <- size in
- size
+ 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 () = (!sizes).(p) <- size in k size)
| String s ->
let size = 2 + (String.length s / ws) in
let () = (!sizes).(p) <- size in
- size
+ k size
let size = function
| Int _ | Atm _ | Fun _ -> 0
@@ -116,7 +121,7 @@ struct
let () = memory := mem in
let () = sizes := Array.make (Array.length mem) (-1) in
let seen = Array.make (Array.length mem) false in
- let _ = init_size seen obj in
+ let () = init_size seen ignore obj in
obj
let oid = function
@@ -155,7 +160,8 @@ let get_string_in_tuple o =
for i = 0 to Array.length o - 1 do
match Repr.repr o.(i) with
| STRING s ->
- raise (TupleString (Printf.sprintf " [..%s..]" s))
+ let len = min max_string_length (String.length s) in
+ raise (TupleString (Printf.sprintf " [..%s..]" (String.sub s 0 len)))
| _ -> ()
done;
""
@@ -165,7 +171,8 @@ let get_string_in_tuple o =
let rec get_details v o = match v, Repr.repr o with
| (String | Any), STRING s ->
- Printf.sprintf " [%s]" (String.escaped 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
@@ -192,13 +199,13 @@ let access_children vs os pos =
else raise Exit
let access_list v o pos =
- let rec loop o pos = match Repr.repr o with
- | INT 0 -> []
+ let rec loop o pos accu = match Repr.repr o with
+ | INT 0 -> List.rev accu
| BLOCK (0, [|hd; tl|]) ->
- (v, hd, 0 :: pos) :: loop tl (1 :: pos)
+ loop tl (1 :: pos) ((v, hd, 0 :: pos) :: accu)
| _ -> raise Exit
in
- Array.of_list (loop o pos)
+ Array.of_list (loop o pos [])
let access_block o = match Repr.repr o with
| BLOCK (tag, os) -> (tag, os)
@@ -227,7 +234,16 @@ let rec get_children v o pos = match v with
| BLOCK (0, [|x|]) -> [|(v, x, 0 :: pos)|]
| _ -> raise Exit
end
- |String | Int -> [||]
+ | 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 ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 21:35:32 +0000