X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguator.ml;h=4b647c780541b6ff54fa72d5d5cf4e2520e32a7d;hb=649a897eeea9908ff6a438dcf6a6969894f9bd7f;hp=4f812ff2f032abae8448782165da6bdc544d5bea;hpb=8b20a402003f57320cb9f0cc2eedebbceb16d3fc;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
index 4f812ff2f..4b647c780 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
@@ -27,13 +27,17 @@
 
 open Printf
 
+let debug = false;;
+let debug_print s =
+ if debug then prerr_endline (Lazy.force s);;
+
 exception Ambiguous_input
 (* the integer is an offset to be added to each location *)
 exception DisambiguationError of
  int *
- ((Token.flocation list * string * string) list *
-  (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-  Token.flocation option * string Lazy.t * bool) list list
+ ((Stdpp.location list * string * string) list *
+  (DisambiguateTypes.domain_item * string) list * 
+  (Stdpp.location * string) Lazy.t * bool) list list
   (** parameters are: option name, error message *)
 exception Unbound_identifier of string
 
@@ -42,7 +46,7 @@ type choose_uris_callback =
 
 type choose_interp_callback = 
   string -> int -> 
-    (Token.flocation list * string * string) list list -> int list
+    (Stdpp.location list * string * string) list list -> int list
 
 let mono_uris_callback ~id =
  if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
@@ -82,8 +86,8 @@ let only_one_pass = ref false;;
 
 let disambiguate_thing ~aliases ~universe
   ~(f:?fresh_instances:bool ->
-      aliases:DisambiguateTypes.environment ->
-      universe:DisambiguateTypes.multiple_environment option ->
+      aliases:'term DisambiguateTypes.environment ->
+      universe:'term DisambiguateTypes.multiple_environment option ->
       'a -> 'b)
   ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b)
   ~(drop_aliases_and_clear_diff: 'b -> 'b)
@@ -119,7 +123,7 @@ let disambiguate_thing ~aliases ~universe
     drop_aliases_and_clear_diff res
   in
   let rec aux i errors passes =
-(*prerr_endline ("Pass: " ^ string_of_int i);*)
+  debug_print (lazy ("Pass: " ^ string_of_int i));
    match passes with
       [ pass ] ->
         (try
@@ -144,12 +148,12 @@ let disambiguate_thing ~aliases ~universe
 
 type disambiguator_thing =
  { do_it :
-    'a 'b.
-    aliases:DisambiguateTypes.environment ->
-    universe:DisambiguateTypes.multiple_environment option ->
+    'a 'b 'term.
+    aliases:'term DisambiguateTypes.environment ->
+    universe:'term DisambiguateTypes.multiple_environment option ->
     f:(?fresh_instances:bool ->
-       aliases:DisambiguateTypes.environment ->
-       universe:DisambiguateTypes.multiple_environment option ->
+       aliases:'term DisambiguateTypes.environment ->
+       universe:'term DisambiguateTypes.multiple_environment option ->
        'a -> 'b * bool) ->
     drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) ->
     drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
@@ -196,25 +200,26 @@ let drop_aliases ?(minimize_instances=false) (choices, user_asked) =
    in
     aux d
  in
-  (List.map (fun (d, a, b, c) -> minimize d, a, b, c) choices),
+  (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices),
   user_asked
 
 let drop_aliases_and_clear_diff (choices, user_asked) =
-  (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
+  (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
   user_asked
 
-let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph
-  ~aliases ~universe term
+let disambiguate_term ?fresh_instances ~context ~metasenv ~subst ?goal ?initial_ugraph ~aliases ~universe ~lookup_in_library term
  =
   assert (fresh_instances = None);
   let f =
-    Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph
+    Disambiguator.disambiguate_term ~lookup_in_library ~context ~metasenv ~subst ?goal ?initial_ugraph
   in
   disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
    ~drop_aliases_and_clear_diff term
 
-let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj =
+let disambiguate_obj ?fresh_instances ~aliases ~universe ~uri ~lookup_in_library  obj =
   assert (fresh_instances = None);
-  let f = Disambiguator.disambiguate_obj ~dbd ~uri in
+  let f = Disambiguator.disambiguate_obj ~lookup_in_library ~uri in
   disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
    ~drop_aliases_and_clear_diff obj
+
+let disambiguate_thing ~context = assert false