From 45192ccb907349f0ec51c3d2ac577920c4016119 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 28 Nov 2017 20:23:54 +0100
Subject: Allow to pass physical files to coqchk.

---
 checker/check.ml   | 22 ++++++++++++++++------
 checker/check.mli  | 10 +++++++---
 checker/checker.ml | 11 ++++++-----
 3 files changed, 29 insertions(+), 14 deletions(-)

(limited to 'checker')

diff --git a/checker/check.ml b/checker/check.ml
index 525c84c2f..21fdba1fa 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
diff --git a/checker/check.mli b/checker/check.mli
index ef87e3efa..28ae385b5 100644
--- a/checker/check.mli
+++ b/checker/check.mli
@@ -14,6 +14,10 @@ type section_path = {
   basename : string;
 }
 
+type object_file =
+| PhysicalFile of physical_path
+| LogicalFile of section_path
+
 type logical_path = DirPath.t
 
 val default_root_prefix : DirPath.t
@@ -21,6 +25,6 @@ val default_root_prefix : DirPath.t
 val add_load_path : physical_path * logical_path -> unit
 
 val recheck_library :
-  norec:section_path list ->
-  admit:section_path list ->
-  check:section_path list -> unit
+  norec:object_file list ->
+  admit:object_file list ->
+  check:object_file list -> unit
diff --git a/checker/checker.ml b/checker/checker.ml
index e960a55fd..b2433ee36 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
 
-- 
cgit v1.2.3