X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fdisambiguation%2FdisambiguateTypes.ml;h=4e74e4a3de8ba87f756a36521825db6f6ad43f91;hb=9aa2722ff4aa7868ffd14e5a820cd6dc79e2c8a6;hp=8db0c220d302e46bdd9b3a210880dff6a170ae90;hpb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git

diff --git a/matitaB/components/disambiguation/disambiguateTypes.ml b/matitaB/components/disambiguation/disambiguateTypes.ml
index 8db0c220d..4e74e4a3d 100644
--- a/matitaB/components/disambiguation/disambiguateTypes.ml
+++ b/matitaB/components/disambiguation/disambiguateTypes.ml
@@ -25,23 +25,31 @@
 
 (* $Id$ *)
 
+(*
 type domain_item =
  | Id of (string * string option)              (* literal, opt. uri *)
  | Symbol of string * (string option * string) option (* literal, opt. (uri,interp.) *)
  | Num of (string option * string) option             (* opt. uri, interpretation *)
+*)
 
-(*
 type domain_item =
  | Id of string     (* literal *)
  | Symbol of string (* literal *)
  | Num 
- *)
 
 exception Invalid_choice of (Stdpp.location * string) Lazy.t
 
 module OrderedDomain =
   struct
     type t = domain_item
+    (*
+    let compare a b = 
+      match a,b with
+      | Id (x,None), Id (y,_)
+      | Id (x,_), Id (y,None) when x = y -> 0
+      | Symbol (x,None), Symbol (y,_)
+      | Symbol (x,_), Symbol (y,None) when x = y -> 0
+      | _ -> Pervasives.compare a b *)
     let compare = Pervasives.compare
   end
 
@@ -54,40 +62,19 @@ struct
 
   let find k env =
     try find k env 
-    with Not_found -> 
+    with Not_found ->
+           (* 
       match k with
        | Symbol (sym,_) -> find (Symbol (sym,None)) env
        | Num _ -> find (Num None) env
        | Id (id,_) -> find (Id (id,None)) env 
+       *) raise Not_found
 
   let cons desc_of_alias k v env =
-    let default_dom_item = function
-    | Id (s,_) -> Id (s,None)
-    | Symbol (s,_) -> Symbol (s,None)
-    | Num _ -> Num None
-    in
-    (*
-    try
-      let current = find k env in
-      let dsc = desc_of_alias v in
-      let entry = v::(List.filter (fun x -> desc_of_alias x <> dsc) current) in
-      let id = match k with
-        | Id (id,_) -> id
-        | Symbol (sym,_) -> "SYMBOL:"^sym
-        | Num _ -> "NUM"
-      in
-      prerr_endline (Printf.sprintf "updated alias for %s with entry of length %d (was: %d)" id (List.length entry) (List.length current));
-      let res = add k entry env
-      in
-      let test = find k res in
-      prerr_endline (Printf.sprintf "so the current length of the entry is %d."
-        (List.length test));
-      res
-    with Not_found -> add k [v] env
-    *)
+    let default_dom_item x = x in
     let env' =
       try
-        let current = find k env in
+        let current = Environment'.find k env in
         let dsc = desc_of_alias v in
         add k (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env
       with Not_found ->
@@ -104,6 +91,14 @@ struct
 
 end
 
+module InterprOD =
+  struct
+    type t = Stdpp.location
+    let compare = Pervasives.compare
+  end
+
+module InterprEnv = Map.Make (InterprOD)
+
 type 'term codomain_item =
   string *  (* description *)
    [`Num_interp of string -> 'term
@@ -119,9 +114,12 @@ type interactive_user_uri_choice_type =
 type interactive_interpretation_choice_type = string -> int ->
   (Stdpp.location list * string * string) list list -> int list
 
+type interactive_ast_choice_type = string list -> int
+
 type input_or_locate_uri_type = 
   title:string -> ?id:string -> unit -> NReference.reference option
 
+(*
 let string_of_domain_item item =
   let f_opt f x default =
     match x with
@@ -131,7 +129,20 @@ let string_of_domain_item item =
   match item with
   | Id (s,huri) -> 
      Printf.sprintf "ID(%s,%s)" s (f_opt (fun x -> x) huri "_")
-  | Symbol (s,_) -> Printf.sprintf "SYMBOL(%s)" s
+  | Symbol (s,None) -> Printf.sprintf "SYMBOL(%s)" s
+  | Symbol (s,Some (_,dsc)) -> Printf.sprintf "SYMBOL(%s,%s)" s dsc
   | Num _ -> "NUM"
 ;;
-
+*)
+let string_of_domain_item item =
+  let f_opt f x default =
+    match x with
+    | None -> default
+    | Some y -> f y
+  in
+  match item with
+  | Id s -> 
+     Printf.sprintf "ID(%s)" s
+  | Symbol s -> Printf.sprintf "SYMBOL(%s)" s
+  | Num -> "NUM"
+;;