From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 23 Jan 2004 16:38:17 +0000 (+0000)
Subject: implemented interface for gTopLevel
X-Git-Tag: V_0_2_3~160
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=308d03101d84a4d62465bb3ff7c0cd9ca866c659;p=helm.git

implemented interface for gTopLevel
---

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index 5f797ab5d..94690373a 100644
--- 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 545099da1..522a08dc0 100644
--- 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 525a7e33f..a8dda6c39 100644
--- 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
+