X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fdisambiguation%2FmultiPassDisambiguator.ml;fp=matitaB%2Fcomponents%2Fdisambiguation%2FmultiPassDisambiguator.ml;h=2edd1bd69c7bfdfe380a590418022008743465c0;hb=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;hp=f35b1d8d2e3ac5c94495330024f94194ed56bbf4;hpb=98f0fac6d03367be776303e7ba353b75878aaa40;p=helm.git

diff --git a/matitaB/components/disambiguation/multiPassDisambiguator.ml b/matitaB/components/disambiguation/multiPassDisambiguator.ml
index f35b1d8d2..2edd1bd69 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,6 +74,7 @@ let drop_aliases ?(minimize_instances=false) ~description_of_alias
    let rec aux =
     function
        [] -> []
+(* now it's ALWAYS None
      | (D.Symbol (s,n),ci1) as he::tl when n <> None ->
          if
           List.for_all
@@ -91,23 +93,23 @@ let drop_aliases ?(minimize_instances=false) ~description_of_alias
          then
           (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 ~visit ~f thing
+(*let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~visit ~f thing
 =
-  let library = false, DisambiguateTypes.Environment.empty,
+  let library = false, DisambiguateTypes.InterprEnv.empty,
                 DisambiguateTypes.Environment.empty in
-  let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
+  let multi_aliases = false, DisambiguateTypes.InterprEnv.empty, universe in
   let mono_aliases = true, aliases, DisambiguateTypes.Environment.empty in
   let passes =
     List.map
@@ -125,7 +127,7 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~visit ~
    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,7 +145,7 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~visit ~
     | [] -> assert false
   in
    aux 1 [] passes
-;;
+;;*)
 
 let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
   ~string_context_of_context ~initial_ugraph ~expty ~mk_implicit
@@ -151,7 +153,8 @@ let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
   ~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
@@ -162,3 +165,14 @@ let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
   in
   disambiguate_thing ~description_of_alias ~passes ~aliases
    ~universe ~visit ~f thing
+   *)
+     try
+      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.NoWellTypedInterpretation (offset,newerrors) ->
+          raise (DisambiguationError (offset, [newerrors]))