implemented interface for gTopLevel

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index 5f797ab5dbbfb1ef12b0096aba811a541ac53a77..94690373af3abe9f368b230225e43cab3e61de18 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -25,9 +25,6 @@
 
 open Disambiguate_types
 
-  (* TODO move to  CicSomething *)
-val term_of_uri: string -> Cic.term
-
 (** {2 Choice registration interface} *)
 
   (** to be raised when a choice is invalid due to some given parameter (e.g.

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
+

diff --git a/helm/ocaml/cic_disambiguation/disambiguate_types.mli b/helm/ocaml/cic_disambiguation/disambiguate_types.mli
index 525a7e33f8a1f1bb044d4e00190e7b0f6d0b25f5..a8dda6c39b66c53057e273532a1c0f9cf8aa6039 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate_types.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate_types.mli
@@ -54,3 +54,13 @@ module type Callbacks =
 val string_of_domain_item: domain_item -> string
 val string_of_domain: Domain.t -> string
 
+(**/**)
+
+module EnvironmentP3:
+  sig
+    type t = environment
+    val empty : string
+    val to_string : t -> string
+    val of_string : string -> t
+  end
+