X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2FdisambiguateTypes.ml;h=23c16cff28e620e388f259c15e4bf6a44e0face4;hb=57c7d6ef239b4c2b070721715887684adf41159c;hp=0ed285af0bd057c8e15c589184499c7cf10c99cf;hpb=f4d41a527321e5fbdc10054b46ad60fe9f7f54a1;p=helm.git

diff --git a/helm/software/components/disambiguation/disambiguateTypes.ml b/helm/software/components/disambiguation/disambiguateTypes.ml
index 0ed285af0..23c16cff2 100644
--- a/helm/software/components/disambiguation/disambiguateTypes.ml
+++ b/helm/software/components/disambiguation/disambiguateTypes.ml
@@ -25,16 +25,6 @@
 
 (* $Id$ *)
 
-(*
-type term = CicNotationPt.term
-type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic
-type tactical = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactical
-type script_entry =
-  | Command of tactical
-  | Comment of CicNotationPt.location * string
-type script = CicNotationPt.location * script_entry list
-*)
-
 type domain_item =
   | Id of string               (* literal *)
   | Symbol of string * int     (* literal, instance num *)
@@ -65,46 +55,19 @@ struct
         with Not_found -> find (Num 0) env)
     | _ -> find k env
 
-  let cons k v env =
+  let cons desc_of_alias k v env =
     try
       let current = find k env in
-      let dsc, _ = v in
-      add k (v :: (List.filter (fun (dsc', _) -> dsc' <> dsc) current)) env
+      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
-
-  let hd list_env =
-    try
-      map List.hd list_env
-    with Failure _ -> assert false
-
-  let fold_flatten f env base =
-    fold
-      (fun k l acc -> List.fold_right (fun v acc -> f k v acc) l acc)
-      env base
-
 end
 
 type 'term codomain_item =
   string *  (* description *)
-  ('term environment -> string -> 'term list -> 'term)
-    (* environment, literal number, arguments as needed *)
-
-and 'term environment = 'term codomain_item Environment.t
-
-type 'term multiple_environment = 'term codomain_item list Environment.t
-
-
-(** adds a (name,uri) list l to a disambiguation environment e **)
-let multiple_env_of_list l e = 
-  List.fold_left
-   (fun e (name,descr,t) -> Environment.cons (Id name) (descr,fun _ _ _ -> t) e)
-   e l
-
-let env_of_list l e = 
-  List.fold_left
-   (fun e (name,descr,t) -> Environment.add (Id name) (descr,fun _ _ _ -> t) e)
-   e l
+   [`Num_interp of string -> 'term
+   |`Sym_interp of 'term list -> 'term]
 
 type interactive_user_uri_choice_type =
   selection_mode:[`SINGLE | `MULTIPLE] ->
@@ -119,20 +82,7 @@ type interactive_interpretation_choice_type = string -> int ->
 type input_or_locate_uri_type = 
   title:string -> ?id:string -> unit -> UriManager.uri option
 
-module type Callbacks =
-  sig
-    val interactive_user_uri_choice : interactive_user_uri_choice_type
-
-    val interactive_interpretation_choice : 
-       interactive_interpretation_choice_type
-
-    val input_or_locate_uri: input_or_locate_uri_type
-  end
-
 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 dom =
-  String.concat "; " (List.map string_of_domain_item dom)