From e5141edaab98baafa31173da8164fa5d87b808c5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 4 Jan 2008 20:48:01 +0000
Subject: [PATCH] missing files added

---
 components/library/librarian.ml  | 113 +++++++++++++++++++++++++++++++
 components/library/librarian.mli |  13 ++++
 2 files changed, 126 insertions(+)
 create mode 100644 components/library/librarian.ml
 create mode 100644 components/library/librarian.mli

diff --git a/components/library/librarian.ml b/components/library/librarian.ml
new file mode 100644
index 000000000..4c25bc309
--- /dev/null
+++ b/components/library/librarian.ml
@@ -0,0 +1,113 @@
+exception UnableToQualify
+
+let find_root path =
+  let paths = List.rev (Str.split (Str.regexp "/") path) in
+  let rec build = function
+    | he::tl as l -> ("/" ^ String.concat "/" (List.rev l) ^ "/") :: build tl
+    | [] -> ["/"]
+  in
+  let paths = List.map HExtlib.normalize_path (build paths) in
+  HExtlib.find_in paths "root"
+;;
+  
+let is_prefix_of d1 d2 =
+    let len1 = String.length d1 in
+    let len2 = String.length d2 in
+    if len2 < len1 then 
+      false
+    else
+      let pref = String.sub d2 0 len1 in
+      pref = d1 && (len1 = len2 || d2.[len1] = '/')
+;;
+
+let ensure_trailing_slash s = 
+  if s = "" then "/" else
+  if s.[String.length s-1] <> '/' then s^"/" else s
+;;
+
+let remove_trailing_slash s = 
+  if s = "" then "" else
+  let len = String.length s in
+  if s.[len-1] = '/' then String.sub s 0 (len-1) else s
+;;
+
+let find_root_for ~include_paths file = 
+ let include_paths = "" :: Sys.getcwd () :: include_paths in
+ let path = HExtlib.find_in include_paths file in
+ (* HLog.debug ("file "^file^" resolved as "^path); *)
+ let rootpath, root, buri = 
+   try
+     let mburi = Helm_registry.get "matita.baseuri" in
+     match Str.split (Str.regexp " ") mburi with
+     | [root; buri] when is_prefix_of root path -> ":registry:", root, buri
+     | _ -> raise (Helm_registry.Key_not_found "matita.baseuri")
+   with Helm_registry.Key_not_found "matita.baseuri" -> 
+     let rootpath = find_root path in
+     let data = HExtlib.input_file rootpath in
+     let buri = 
+       let lines = Str.split (Str.regexp "\n") data in
+       let lines = 
+         List.map (fun l -> 
+           match Str.split (Str.regexp "=") l with
+           | [k;v] -> Pcre.replace ~pat:" " k, Pcre.replace ~pat:" " v
+           | _ -> raise (Failure ("Malformed root file: " ^ rootpath)))
+           lines
+       in
+       List.assoc "baseuri" lines
+     in
+     rootpath, Filename.dirname rootpath, buri
+ in
+ (* HLog.debug ("file "^file^" rooted by "^rootpath^""); *)
+ let uri = Http_getter_misc.strip_trailing_slash buri in
+ if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then
+   HLog.error (rootpath ^ " sets an incorrect baseuri: " ^ buri);
+ ensure_trailing_slash root, remove_trailing_slash uri, path
+;;
+
+let filename () =
+  try
+    Helm_registry.get "matita.filename"
+  with Helm_registry.Key_not_found "matita.filename" ->
+    try
+      match Helm_registry.get_list Helm_registry.string "matita.args" with
+      | [x] -> 
+         HLog.warn ("Using matita.args as filename: "^x);
+         Helm_registry.set "matita.filename" x;
+         x
+      | _ -> raise (Failure "no (or more than one) filename to compile")
+    with Helm_registry.Key_not_found "matita.filename" -> 
+      raise (Failure "Unable to get current file name")
+;;  
+  
+let baseuri_of_script ?(include_paths=[]) file = 
+  let root, buri, path = find_root_for ~include_paths file in
+  let path = HExtlib.normalize_path path in
+  let root = HExtlib.normalize_path root in
+  let lpath = Str.split (Str.regexp "/") path in
+  let lroot = Str.split (Str.regexp "/") root in
+  let rec substract l1 l2 =
+    match l1, l2 with
+    | h1::tl1,h2::tl2 when h1 = h2 -> substract tl1 tl2
+    | l,[] -> l
+    | _ -> raise UnableToQualify
+  in
+  let extra_buri = substract lpath lroot in
+  let chop name = 
+    assert(Filename.check_suffix name ".ma");
+    try Filename.chop_extension name
+    with Invalid_argument "Filename.chop_extension" -> name
+  in
+   root,
+   remove_trailing_slash (HExtlib.normalize_path 
+    (buri ^ "/" ^ chop (String.concat "/" extra_buri))),
+   path
+;;
+
+let find_roots_in_dir dir =
+  HExtlib.find ~test:(fun f ->
+    Filename.basename f = "root" &&
+    try (Unix.stat f).Unix.st_kind = Unix.S_REG 
+    with Unix.Unix_error _ -> false)
+    dir
+;;
+
diff --git a/components/library/librarian.mli b/components/library/librarian.mli
new file mode 100644
index 000000000..a8e10bf5a
--- /dev/null
+++ b/components/library/librarian.mli
@@ -0,0 +1,13 @@
+exception UnableToQualify
+val find_root : string -> string
+val is_prefix_of : string -> string -> bool
+val filename : unit -> string
+
+(* baseuri_of_script ?(inc:REG[matita.includes] fname -> root, buri, fullpath 
+ * sample: baseuri_of_script a.ma -> /home/pippo/devel/, cic:/matita/a,
+ * /home/pippo/devel/a.ma *)
+val baseuri_of_script: 
+  ?include_paths:string list -> string -> string * string * string
+
+(* finds all the roots files in the specified dir *)
+val find_roots_in_dir: string -> string list
-- 
2.39.2