diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-11-28 20:23:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-11-29 10:56:36 +0100 |
| commit | 45192ccb907349f0ec51c3d2ac577920c4016119 (patch) | |
| tree | dcda1c5bd25c2d1946cfbc9672a2d6a457659188 /checker/check.ml | |
| parent | 0168f040e29c3bbaeb666f0b793f41627f154e12 (diff) | |
Allow to pass physical files to coqchk.
Diffstat (limited to 'checker/check.ml')
| -rw-r--r-- | checker/check.ml | 22 |
1 files changed, 16 insertions, 6 deletions
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 |