]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/components/disambiguation/disambiguateTypes.ml
First commit with new (incomplete) disambiguation engine.
[helm.git] / matitaB / components / disambiguation / disambiguateTypes.ml
index f6e03d098ccd555de2bab69a0b4f41bb417cf4b5..8db0c220d302e46bdd9b3a210880dff6a170ae90 100644 (file)
 (* $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
 
@@ -46,22 +53,55 @@ 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 
 
   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
-      add k (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env
+      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 env' =
+      try
+        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
+      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 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
+      add k' [v] env'
+
 end
 
 type 'term codomain_item =
@@ -82,7 +122,16 @@ type interactive_interpretation_choice_type = string -> 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,_) -> Printf.sprintf "SYMBOL(%s)" s
+  | Num _ -> "NUM"
+;;
+