X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fdisambiguation%2FdisambiguateTypes.ml;h=4e74e4a3de8ba87f756a36521825db6f6ad43f91;hb=513c4a61f11ce03888a8a0f9d8e513de6e3a7c8b;hp=f6e03d098ccd555de2bab69a0b4f41bb417cf4b5;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/disambiguation/disambiguateTypes.ml b/matitaB/components/disambiguation/disambiguateTypes.ml
index f6e03d098..4e74e4a3d 100644
--- a/matitaB/components/disambiguation/disambiguateTypes.ml
+++ b/matitaB/components/disambiguation/disambiguateTypes.ml
@@ -25,16 +25,31 @@
 
 (* $Id$ *)
 
+(*
 type domain_item =
-  | Id of string               (* literal *)
-  | Symbol of string * int     (* literal, instance num *)
-  | Num of int                 (* instance num *)
+ | 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
 
@@ -46,24 +61,44 @@ struct
   include Environment'
 
   let find k env =
-   match k with
-      Symbol (sym,n) ->
-       (try find k env
-        with Not_found -> find (Symbol (sym,0)) env)
-    | Num n ->
-       (try find k env
-        with Not_found -> find (Num 0) env)
-    | _ -> find k env
+    try find k env 
+    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 x = x in
+    let env' =
+      try
+        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 ->
+        add k [v] env
+    in
+    (* we also add default aliases *)
+    let k' = default_dom_item k in
     try
-      let current = find k env in
+      let current = 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
+      add k' (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env'
     with Not_found ->
-      add k [v] env
+      add k' [v] env'
+
 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
@@ -79,10 +114,35 @@ 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 = function
-  | Id s -> Printf.sprintf "ID(%s)" s
-  | Symbol (s, i) -> Printf.sprintf "SYMBOL(%s,%d)" s i
-  | Num i -> Printf.sprintf "NUM(instance %d)" i
+(*
+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,huri) -> 
+     Printf.sprintf "ID(%s,%s)" s (f_opt (fun x -> x) huri "_")
+  | 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"
+;;