implemented interface for gTopLevel

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate_types.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate_types.ml b/helm/ocaml/cic_disambiguation/disambiguate_types.ml
index 545099da1ee362c73cf348ed4ee40df41d8f0f6b..522a08dc0adf4140ae77f6a5826f0bcb1df34b87 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate_types.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate_types.ml
@@ -45,3 +45,47 @@ let string_of_domain dom =
     dom;
   Buffer.contents buf
 
+module EnvironmentP3 =
+  struct
+    type t = environment
+    let empty = ""
+
+    let to_string env =
+     Environment.fold
+      (fun i v s ->
+        match i with
+        | Id id ->s ^ Printf.sprintf "alias %s %s\n" id (fst v)
+        | _ -> "")
+      env ""
+
+    let of_string inputtext =
+     let regexpr =
+      let alfa = "[a-zA-Z_-]" in
+      let digit = "[0-9]" in
+      let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
+      let blanks = "\( \|\t\|\n\)+" in
+      let nonblanks = "[^ \t\n]+" in
+      let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
+       Str.regexp
+        ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
+     in
+      let rec aux n =
+       try
+        let n' = Str.search_forward regexpr inputtext n in
+         let id = Id (Str.matched_group 2 inputtext) in
+         let uri = "cic:" ^ (Str.matched_group 5 inputtext) in
+          let resolve_id = aux (n' + 1) in
+           if Environment.mem id resolve_id then
+            resolve_id
+           else
+             let term =
+               HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri)
+             in
+             (Environment.add id (uri, (fun _ _ _ -> term))
+               resolve_id)
+       with
+        Not_found -> Environment.empty
+      in
+       aux 0
+  end
+