X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fdisambiguation%2FmultiPassDisambiguator.ml;h=da0cee2d4c64867b51eb6dbecfb233ce5546da3c;hb=3800a841aa7115b10432f588d31b77129b3a0dc9;hp=b1cf9aed0ec55f13e3317489b8e9f63e044d1ffe;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/disambiguation/multiPassDisambiguator.ml b/matitaB/components/disambiguation/multiPassDisambiguator.ml
index b1cf9aed0..da0cee2d4 100644
--- a/matitaB/components/disambiguation/multiPassDisambiguator.ml
+++ b/matitaB/components/disambiguation/multiPassDisambiguator.ml
@@ -61,6 +61,7 @@ let passes () = (* <fresh_instances?, aliases, coercions?> *)
   ]
 ;;
 
+(* XXX is this useful anymore? *)
 let drop_aliases ?(minimize_instances=false) ~description_of_alias
  (choices, user_asked)
 =
@@ -73,7 +74,8 @@ let drop_aliases ?(minimize_instances=false) ~description_of_alias
    let rec aux =
     function
        [] -> []
-     | (D.Symbol (s,n),ci1) as he::tl when n > 0 ->
+(* now it's ALWAYS None
+     | (D.Symbol (s,n),ci1) as he::tl when n <> None ->
          if
           List.for_all
            (function
@@ -81,34 +83,34 @@ let drop_aliases ?(minimize_instances=false) ~description_of_alias
              | _ -> true
            ) d
          then
-          (D.Symbol (s,0),ci1)::(aux tl)
+          (D.Symbol (s,None),ci1)::(aux tl)
          else
           he::(aux tl)
-     | (D.Num n,ci1) as he::tl when n > 0 ->
+     | (D.Num n,ci1) as he::tl when n <> None ->
          if
           List.for_all
            (function (D.Num _,ci2) -> compare ci1 ci2 | _ -> true) d
          then
-          (D.Num 0,ci1)::(aux tl)
+          (D.Num None,ci1)::(aux tl)
          else
-          he::(aux tl)
+          he::(aux tl) *)
       | he::tl -> he::(aux tl)
    in
     aux d
  in
-  (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices),
+  (List.map (fun (t, d, a, b, c, e) -> t, minimize d, a, b, c, e) choices),
   user_asked
 
 let drop_aliases_and_clear_diff (choices, user_asked) =
-  (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
+  (List.map (fun (t,_, a, b, c, d) -> t,[], a, b, c, d) choices),
   user_asked
 
-let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
+(*let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~visit ~f thing
 =
-  assert (universe <> None);
-  let library = false, DisambiguateTypes.Environment.empty, None in
-  let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
-  let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
+  let library = false, DisambiguateTypes.InterprEnv.empty,
+                DisambiguateTypes.Environment.empty in
+  let multi_aliases = false, DisambiguateTypes.InterprEnv.empty, universe in
+  let mono_aliases = true, aliases, DisambiguateTypes.Environment.empty in
   let passes =
     List.map
      (function (fresh_instances,env,use_coercions) ->
@@ -125,7 +127,7 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
    else if user_asked then
     drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *)
    else
-    drop_aliases_and_clear_diff res
+    drop_aliases_and_clear_diff res 
   in
   let rec aux i errors passes =
   debug_print (lazy ("Pass: " ^ string_of_int i));
@@ -143,22 +145,37 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
     | [] -> assert false
   in
    aux 1 [] passes
-;;
+;;*)
 
 let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
   ~string_context_of_context ~initial_ugraph ~expty ~mk_implicit
   ~description_of_alias ~fix_instance ~aliases ~universe ~lookup_in_library
-  ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
+  ~uri ~pp_thing ~pp_term ~domain_of_thing ~interpretate_thing ~refine_thing ~visit
   ~mk_localization_tbl thing
  =
-  let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) =
+(*  
+    let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) =
     let thing = if fresh_instances then freshen_thing thing else thing in
      Disambiguate.disambiguate_thing
       ~context ~metasenv ~subst ~use_coercions ~string_context_of_context
       ~initial_ugraph ~expty ~mk_implicit ~description_of_alias ~fix_instance
       ~aliases ~universe ~lookup_in_library 
-      ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
-      ~mk_localization_tbl (txt,len,thing)
+      ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~visit 
+      ~mk_localization_tbl ~pp_term (txt,len,thing)
   in
   disambiguate_thing ~description_of_alias ~passes ~aliases
-   ~universe ~f thing
+   ~universe ~visit ~f thing
+   *)
+     match
+      Disambiguate.disambiguate_thing
+      ~context ~metasenv ~subst ~use_coercions:true ~string_context_of_context
+      ~initial_ugraph ~expty ~mk_implicit ~description_of_alias ~fix_instance
+      ~aliases ~universe ~lookup_in_library 
+      ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~visit 
+      ~mk_localization_tbl ~pp_term thing
+     with
+     | Disambiguate.Disamb_success res -> res
+     | Disambiguate.Disamb_failure (herrors, serrors) ->
+          (* temporary *)
+          let offset = 0 in
+          raise (DisambiguationError (offset, newerrors))