Matitaweb: first attempt at web UI for disambiguation.

[helm.git] / matitaB / components / ng_disambiguation / grafiteDisambiguate.ml

diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
index 9c7ea4768ceb4152cf35839d2cda60fcfb3f90a6..b1dc98a1e23e46cde8c3e265fed0061327a2af2b 100644 (file)
--- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -76,6 +76,9 @@ 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)
+
 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))
@@ -107,15 +110,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__"
 
@@ -297,11 +291,24 @@ 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 hds in
+
+  if List.length uniq_hds > 1
+    then loc, uniq_hds
+  else 
+    let tls = List.map List.tl l in
+    find_diffs tls
+;;
+
 let disambiguate_nterm status expty context metasenv subst thing
-= 
-  let newast, metasenv, subst, cic =
-    singleton "first"
-      (NCicDisambiguate.disambiguate_term
+=
+  let choices, _ = NCicDisambiguate.disambiguate_term
         status
         ~aliases:status#disambiguate_db.interpr
         ~expty 
@@ -310,16 +317,24 @@ let disambiguate_nterm status expty context metasenv subst thing
         ~mk_choice:(ncic_mk_choice status)
         ~mk_implicit ~fix_instance
         ~description_of_alias:GrafiteAst.description_of_alias
-        ~context ~metasenv ~subst thing)
+        ~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
+  match choices with
+  | [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
+  | [] -> assert false
+  | _ -> 
+      let diffs = 
+        List.map (fun (ast,_,_,_) -> 
+          diff_term Stdpp.dummy_loc thing' ast) choices 
+      in
+      raise (Ambiguous_input (find_diffs diffs))
 ;;
 
-
 type pattern = 
   NotationPt.term Disambiguate.disambiguator_input option * 
   (string * NCic.term) list * NCic.term option
@@ -367,7 +382,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
@@ -381,9 +396,8 @@ 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
+
+  let choices, _ = NCicDisambiguate.disambiguate_obj
       status
       ~lookup_in_library:(nlookup_in_library status)
       ~description_of_alias:GrafiteAst.description_of_alias
@@ -391,11 +405,21 @@ let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
       ~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
+      obj'
   in
-   status, cic
+  match choices with
+  | [ast, _, _, cic] -> 
+      let diff = diff_obj Stdpp.dummy_loc obj ast in
+      let status = add_to_interpr status diff
+      in
+      status, cic
+  | [] -> assert false
+  | _ -> 
+      let diffs = 
+        List.map (fun (ast,_,_,_) -> 
+          diff_obj Stdpp.dummy_loc obj ast) choices 
+      in
+      raise (Ambiguous_input (find_diffs diffs))
 ;;
 
 let disambiguate_cic_appl_pattern status args =