From 7de3df9930d3f77464030d7d1c82b8d8ec0495d2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sat, 20 Jan 2024 17:47:59 +0000
Subject: [PATCH] wip

---
 coq/files.ml                  | 30 ++++++++++++++++++++++--------
 coq/files.mli                 |  1 +
 examples/ex0.v                | 10 ++++++++++
 test/compiler/basic/proj1/a.v |  8 ++++++--
 test/compiler/basic/proj1/b.v |  6 +++++-
 5 files changed, 44 insertions(+), 11 deletions(-)

diff --git a/coq/files.ml b/coq/files.ml
index 0100395b..91fa811a 100644
--- a/coq/files.ml
+++ b/coq/files.ml
@@ -35,17 +35,31 @@ module Require_result = struct
     | Wait of CUnix.physical_path list
 end
 
+let pp_bind fmt (file, dp) = Stdlib.Format.fprintf fmt "@[%s / %s@]" file (Names.DirPath.to_string dp)
+
+let pp_partials fmt lp = Stdlib.Format.(fprintf fmt "@[%a@]" (pp_print_list pp_bind) lp)
+
 let check_file_ready ?root (m, _imports) =
-  match Loadpath.locate_qualified_library ?root m with
-  | Ok (dirpath, file) ->
+  let dir, _base = Libnames.repr_qualid m in
+  match Loadpath.expand_path ?root dir with
+  | [], [] -> Error "file not found in loadpath, both empty"
+  | [], partials ->
+    Stdlib.Format.eprintf "partial match:@\n @[%a@]%!" pp_partials partials;
+    Error "weird stuff happened in expand path"
+  | (file, dp) :: rr, _ -> (
     let () =
-      Stdlib.Format.eprintf "found file: %s for library %s@\n%!" file
-        (Names.DirPath.to_string dirpath)
+      Stdlib.Format.eprintf "exact match: %a@\n%!" pp_partials ((file, dp) :: rr)
     in
-    let ready = true in
-    (* Hook for the document manager *)
-    if ready then Ok (Ok (dirpath, file)) else Error file
-  | Error e -> Ok (Error e)
+    match Loadpath.locate_qualified_library ?root m with
+    | Ok (dirpath, file) ->
+      let () =
+        Stdlib.Format.eprintf "found object file: %s for library %s@\n%!" file
+          (Names.DirPath.to_string dirpath)
+      in
+      let ready = true in
+      (* Hook for the document manager *)
+      if ready then Ok (Ok (dirpath, file)) else Error file
+    | Error e -> Ok (Error e))
 
 let requires_are_ready ~files:_ { Ast.Require.from; export = _; mods; _ } =
   let root = Option.map ~f:qualid_to_dirpath from in
diff --git a/coq/files.mli b/coq/files.mli
index 37fd94d0..0b38e082 100644
--- a/coq/files.mli
+++ b/coq/files.mli
@@ -31,3 +31,4 @@ module Require_result : sig
 end
 
 val requires_are_ready : files:t -> Ast.Require.t -> Require_result.t
+val intern : Names.DirPath.t -> Library.library_t
diff --git a/examples/ex0.v b/examples/ex0.v
index 0a675e5a..f750cc36 100644
--- a/examples/ex0.v
+++ b/examples/ex0.v
@@ -11,6 +11,16 @@ Proof. by elim: n. Qed.
 
 Definition m := addn0.
 
+Theorem foo n : n = n :> nat.
+Proof.
+aa.
+bb. slkjd. skl . skj .
+cc.
+dd.
+Qed.
+
+About foo.
+
 Print m.
 
 Definition a := 2.
diff --git a/test/compiler/basic/proj1/a.v b/test/compiler/basic/proj1/a.v
index 66ba5335..a1077535 100644
--- a/test/compiler/basic/proj1/a.v
+++ b/test/compiler/basic/proj1/a.v
@@ -1,7 +1,11 @@
+From Coq Require Reals.
+
 Definition aa := 3.
 
 Lemma foo : True.
-Proof.
+Proof. 
 (* Some comment *)
-auto.
+auto .
 Qed.
+
+Optimize Heap.
\ No newline at end of file
diff --git a/test/compiler/basic/proj1/b.v b/test/compiler/basic/proj1/b.v
index bb7730cb..8acef497 100644
--- a/test/compiler/basic/proj1/b.v
+++ b/test/compiler/basic/proj1/b.v
@@ -1,2 +1,6 @@
+From Coq Require Reals.
+
 Require a.
-Definition bb := a.aa.
+Definition bb := a.aa. 
+
+Optimize Heap.