X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_disambiguation%2FgrafiteDisambiguate.ml;h=d6e4e0c354f305f107fd79e09e16cff9e4eefa4d;hb=3c8da07d7a5d7cf0432a83732a6d103f527afaef;hp=30bd9b83497417ef9e3737827620de485e3b0ba2;hpb=6c702f5054d7975f76911ba62da9bfa33d3ed0fa;p=helm.git

diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
index 30bd9b834..d6e4e0c35 100644
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -48,18 +48,24 @@ let initial_status = {
 class type g_status =
   object
    inherit Interpretations.g_status
+   inherit NCicLibrary.g_status
    method disambiguate_db: db
   end
 
 class virtual status uid =
  object (self)
   inherit Interpretations.status uid
+  inherit NCicLibrary.status uid
   val disambiguate_db = initial_status
   method disambiguate_db = disambiguate_db
   method set_disambiguate_db v = {< disambiguate_db = v >}
+  method reset_disambiguate_db () = 
+    {< disambiguate_db = { self#disambiguate_db with interpr =
+            DisambiguateTypes.InterprEnv.empty } >}
   method set_disambiguate_status
    : 'status. #g_status as 'status -> 'self
-      = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db)
+      = fun o -> ((self#set_interp_status o)#set_disambiguate_db
+      o#disambiguate_db)#set_lib_status o
  end
 
 (* let eval_with_new_aliases status f =
@@ -70,6 +76,21 @@ class virtual status uid =
   new_aliases,res
 ;;*)
 
+(* reports the first source of ambiguity and its possible interpretations *)
+exception Ambiguous_input of (Stdpp.location * GrafiteAst.alias_spec list)
+
+(* reports disambiguation errors *)
+exception Error of 
+  (* location of a choice point *)
+  (Stdpp.location * 
+    (* one possible choice (or no valid choice) *)
+    (GrafiteAst.alias_spec option *
+      (* list of asts together with the failing location and error msg *)  
+      ((Stdpp.location * GrafiteAst.alias_spec) list * 
+        Stdpp.location * string) list) 
+      list) 
+  list
+
 let dump_aliases out msg status =
    out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
    DisambiguateTypes.InterprEnv.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
@@ -85,7 +106,23 @@ let add_to_interpr status new_aliases =
      {status#disambiguate_db with interpr = interpr }
    in
     status#set_disambiguate_db new_status
-   
+
+(*
+let print_interpr status =
+   DisambiguateTypes.InterprEnv.iter
+     (fun loc alias ->
+        let start,stop = HExtlib.loc_of_floc loc in
+        let strpos = Printf.sprintf "@(%d,%d):" start stop in
+        match alias with
+        | GrafiteAst.Ident_alias (id,uri) -> 
+            Printf.printf "%s   [%s;%s]\n" strpos id uri
+        | GrafiteAst.Symbol_alias (name,_ouri,desc) ->
+            Printf.printf "%s  <%s:%s>\n" strpos name desc
+        | GrafiteAst.Number_alias (_ouri,desc) ->
+            Printf.printf "%s  <NUM:%s>\n" strpos desc)
+     status#disambiguate_db.interpr
+*)
+
 let add_to_disambiguation_univ status new_aliases =
    let multi_aliases =
     List.fold_left (fun acc (d,c) -> 
@@ -101,15 +138,6 @@ let add_to_disambiguation_univ status new_aliases =
 
 exception BaseUriNotSetYet
 
-let singleton msg = function
-  | [x], _ -> x
-  | l, _   ->
-      let debug = 
-         Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
-         msg (List.length l)
-      in
-      prerr_endline debug; assert false
-
 let __Implicit = "__Implicit__"
 let __Closed_Implicit = "__Closed_Implicit__"
 
@@ -155,13 +183,13 @@ let mk_implicit b =
       GrafiteAst.Symbol_alias (__Closed_Implicit,None,"Fake Closed Implicit")
 ;;
 
-let nlookup_in_library 
+let nlookup_in_library status
   interactive_user_uri_choice input_or_locate_uri item 
 =
   match item with
   | DisambiguateTypes.Id id -> 
      (try
-       let references = NCicLibrary.resolve id in
+       let references = NCicLibrary.resolve status id in
         List.map
          (fun u -> 
            GrafiteAst.Ident_alias (id,NReference.string_of_reference u)
@@ -291,29 +319,61 @@ let diff_obj loc o1 o2 = match o1,o2 with
  | _ -> assert false
 ;;
 
+(* this function, called on a list of choices that must
+ * be different, never fails and returns the location of
+ * the first ambiguity (and its possible interpretations) *)
+let rec find_diffs l =
+  let loc,_ = List.hd (List.hd l) in
+  let hds = List.map (fun x -> snd (List.hd x)) l in
+  let uniq_hds = HExtlib.list_uniq (List.sort Pervasives.compare hds) in
+
+  if List.length uniq_hds > 1
+    then loc, uniq_hds
+  else 
+    let tls = List.map List.tl l in
+    find_diffs tls
+;;
+
+(* clusterize a list of errors according to the last chosen interpretation *)
+let clusterize diff (eframe,loc0) =
+  let rec aux = function
+  | [] -> []
+  | (_,choice,_,_ as x)::l0 -> 
+       let matches,others = List.partition (fun (_,c,_,_) -> c = choice) l0 in
+       (choice,List.map (fun (a,_,l,e) -> diff a,l,e) (x::matches)) ::
+               aux others
+  in loc0, aux eframe
+
 let disambiguate_nterm status expty context metasenv subst thing
 =
-  let newast, metasenv, subst, cic =
-    singleton "first"
-      (NCicDisambiguate.disambiguate_term
+  let _,_,thing' = thing in
+  match NCicDisambiguate.disambiguate_term
         status
         ~aliases:status#disambiguate_db.interpr
         ~expty 
         ~universe:(status#disambiguate_db.multi_aliases)
-        ~lookup_in_library:nlookup_in_library
+        ~lookup_in_library:(nlookup_in_library status)
         ~mk_choice:(ncic_mk_choice status)
         ~mk_implicit ~fix_instance
         ~description_of_alias:GrafiteAst.description_of_alias
-        ~context ~metasenv ~subst thing)
-  in
-  let _,_,thing' = thing in
-  let diff = diff_term Stdpp.dummy_loc thing' newast in
-  let status = add_to_interpr status diff
-  in
-   metasenv, subst, status, cic
+        ~context ~metasenv ~subst thing
+  with
+  | Disambiguate.Disamb_success [newast,metasenv,subst,cic,_] ->
+      let diff = diff_term Stdpp.dummy_loc thing' newast in
+      let status = add_to_interpr status diff 
+      in
+      metasenv, subst, status, cic
+  | Disambiguate.Disamb_success (_::_ as choices) ->
+      let diffs = 
+        List.map (fun (ast,_,_,_,_) -> 
+          diff_term Stdpp.dummy_loc thing' ast) choices 
+      in 
+      raise (Ambiguous_input (find_diffs diffs)) 
+  | Disambiguate.Disamb_failure l ->
+      raise (Error (List.map (clusterize (diff_term Stdpp.dummy_loc thing')) l))
+  | _ -> assert false
 ;;
 
-
 type pattern = 
   NotationPt.term Disambiguate.disambiguator_input option * 
   (string * NCic.term) list * NCic.term option
@@ -361,7 +421,7 @@ let disambiguate_just disambiguate_term context metasenv =
        metasenv, `Auto params
 ;;
       
-let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
+let disambiguate_nobj status ?baseuri (text,prefix_len,obj as obj') =
   let uri =
    let baseuri = 
      match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
@@ -375,21 +435,30 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
    in
      NUri.uri_of_string (baseuri ^ "/" ^ name)
   in
-  let ast, _, _, cic =
-   singleton "third"
-    (NCicDisambiguate.disambiguate_obj
+
+  match NCicDisambiguate.disambiguate_obj
       status
-      ~lookup_in_library:nlookup_in_library
+      ~lookup_in_library:(nlookup_in_library status)
       ~description_of_alias:GrafiteAst.description_of_alias
       ~mk_choice:(ncic_mk_choice status)
       ~mk_implicit ~fix_instance ~uri
       ~aliases:status#disambiguate_db.interpr
       ~universe:(status#disambiguate_db.multi_aliases) 
-      (text,prefix_len,obj)) in
-  let diff = diff_obj Stdpp.dummy_loc obj ast in
-  let status = add_to_interpr status diff
-  in
-   status, cic
+      obj'
+  with
+  | Disambiguate.Disamb_success [newast,_,_,cic,_] ->
+      let diff = diff_obj Stdpp.dummy_loc obj newast in
+      let status = add_to_interpr status diff 
+      in status, cic
+  | Disambiguate.Disamb_success (_::_ as choices) ->
+      let diffs = 
+        List.map (fun (ast,_,_,_,_) -> 
+          diff_obj Stdpp.dummy_loc obj ast) choices 
+      in
+      raise (Ambiguous_input (find_diffs diffs)) 
+  | Disambiguate.Disamb_failure l -> 
+      raise (Error (List.map (clusterize (diff_obj Stdpp.dummy_loc obj)) l))
+  | _ -> assert false
 ;;
 
 let disambiguate_cic_appl_pattern status args =
@@ -432,7 +501,7 @@ let aliases_for_objs status refs =
  List.concat
   (List.map
     (fun nref ->
-      let references = NCicLibrary.aliases_of nref in
+      let references = NCicLibrary.aliases_of status nref in
        List.map
         (fun u ->
           let name = NCicPp.r2s status true u in