X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=85f05aa1c8700048224840ed34f262f21e0e29f8;hb=9c9e979d4c45cf3b1ee01688b2c36fe49190ce98;hp=667c50770536bb7187df52a2cc460991b32cf20f;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 667c50770..85f05aa1c 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -39,6 +39,7 @@ exception PathNotWellFormed
 exception Try_again of string Lazy.t
 
 type aliases = bool * DisambiguateTypes.environment
+type 'a disambiguator_input = string * int * 'a
 
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
@@ -505,10 +506,13 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
   | CicNotationPt.Theorem (flavour, name, ty, bo) ->
      let attrs = [`Flavour flavour] in
      let ty' = interpretate_term [] env None false ty in
-     (match bo with
-        None ->
+     (match bo,flavour with
+        None,`Axiom ->
+         Cic.Constant (name,None,ty',[],attrs)
+      | Some bo,`Axiom -> assert false
+      | None,_ ->
          Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
-      | Some bo ->
+      | Some bo,_ ->
          let bo' = Some (interpretate_term [] env None false bo) in
           Cic.Constant (name,bo',ty',[],attrs))
           
@@ -521,19 +525,25 @@ let rev_uniq =
       let compare = Pervasives.compare
     end
   in
-  let module Set = Set.Make (SortedItem) in
+  let module Map = Map.Make (SortedItem) in
   fun l ->
     let rev_l = List.rev l in
-    let (_, uniq_rev_l) =
+    let (members, uniq_rev_l) =
       List.fold_left
-        (fun (members, rev_l) elt ->
-          if Set.mem elt members then
-            (members, rev_l)
-          else
-            Set.add elt members, elt :: rev_l)
-        (Set.empty, []) rev_l
+        (fun (members, rev_l) (loc,elt) ->
+          try 
+            let locs = Map.find elt members in
+            if List.mem loc locs then
+              members, rev_l
+            else
+              Map.add elt (loc::locs) members, rev_l
+          with
+          | Not_found -> Map.add elt [loc] members, elt :: rev_l)
+        (Map.empty, []) rev_l
     in
-    List.rev uniq_rev_l
+    List.rev_map 
+      (fun e -> try Map.find e members,e with Not_found -> assert false)
+      uniq_rev_l
 
 (* "aux" keeps domain in reverse order and doesn't care about duplicates.
  * Domain item more in deep in the list will be processed first.
@@ -549,7 +559,7 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
   | CicNotationPt.Binder (kind, (var, typ), body) ->
       let kind_dom =
         match kind with
-        | `Exists -> [ Symbol ("exists", 0) ]
+        | `Exists -> [ loc, Symbol ("exists", 0) ]
         | _ -> []
       in
       let type_dom = domain_rev_of_term_option loc context typ in
@@ -563,7 +573,7 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
       let outtype_dom = domain_rev_of_term_option loc context outtype in
       let get_first_constructor = function
         | [] -> []
-        | ((head, _, _), _) :: _ -> [ Id head ]
+        | ((head, _, _), _) :: _ -> [ loc, Id head ]
       in
       let do_branch ((head, _, args), term) =
         let (term_context, args_domain) =
@@ -583,7 +593,7 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
       branches_dom @ outtype_dom @ term_dom @
       (match indty_ident with
        | None -> get_first_constructor branches
-       | Some (ident, _) -> [ Id ident ])
+       | Some (ident, _) -> [ loc, Id ident ])
   | CicNotationPt.Cast (term, ty) ->
       let term_dom = domain_rev_of_term ~loc context term in
       let ty_dom = domain_rev_of_term ~loc context ty in
@@ -622,22 +632,22 @@ let rec domain_rev_of_term ?(loc = HExtlib.dummy_floc) context = function
           []
       with Not_found ->
         (match subst with
-        | None -> [Id name]
+        | None -> [loc, Id name]
         | Some subst ->
             List.fold_left
               (fun dom (_, term) ->
                 let dom' = domain_rev_of_term ~loc context term in
                 dom' @ dom)
-              [Id name] subst))
+              [loc, Id name] subst))
   | CicNotationPt.Uri _ -> []
   | CicNotationPt.Implicit -> []
-  | CicNotationPt.Num (num, i) -> [ Num i ]
+  | CicNotationPt.Num (num, i) -> [loc, Num i ]
   | CicNotationPt.Meta (index, local_context) ->
       List.fold_left
        (fun dom term -> domain_rev_of_term_option loc context term @ dom) []
         local_context
   | CicNotationPt.Sort _ -> []
-  | CicNotationPt.Symbol (symbol, instance) -> [ Symbol (symbol, instance) ]
+  | CicNotationPt.Symbol (symbol, instance) -> [loc, Symbol (symbol, instance) ]
   | CicNotationPt.UserInput
   | CicNotationPt.Literal _
   | CicNotationPt.Layout _
@@ -658,7 +668,7 @@ let domain_of_obj ~context ast =
       (match bo with
           None -> []
         | Some bo -> domain_rev_of_term [] bo) @
-      domain_of_term [] ty
+      domain_rev_of_term [] ty
    | CicNotationPt.Inductive (params,tyl) ->
       let dom =
        List.flatten (
@@ -675,7 +685,7 @@ let domain_of_obj ~context ast =
         ) dom params
       in
        List.filter
-        (fun name ->
+        (fun (_,name) ->
           not (  List.exists (fun (name',_) -> name = Id name') params
               || List.exists (fun (name',_,_,_) -> name = Id name') tyl)
         ) dom
@@ -690,7 +700,7 @@ let domain_of_obj ~context ast =
         ) (dom @ domain_rev_of_term [] ty) params
       in
        List.filter
-        (fun name->
+        (fun (_,name) ->
           not (  List.exists (fun (name',_) -> name = Id name') params
               || List.exists (fun (name',_,_) -> name = Id name') fields)
         ) dom
@@ -704,7 +714,7 @@ let domain_diff dom1 dom2 =
     List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
       (fun _ -> false) dom2
   in
-  List.filter (fun elt -> not (is_in_dom2 elt)) dom1
+  List.filter (fun (_,elt) -> not (is_in_dom2 elt)) dom1
 
 module type Disambiguator =
 sig
@@ -716,7 +726,7 @@ sig
     ?initial_ugraph:CicUniv.universe_graph -> 
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
-    CicNotationPt.term ->
+    CicNotationPt.term disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.term*
@@ -729,7 +739,7 @@ sig
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
-    CicNotationPt.obj ->
+    CicNotationPt.obj disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.obj *
@@ -744,8 +754,12 @@ module Make (C: Callbacks) =
       let uris =
        match uris with
         | [] ->
-           [(C.input_or_locate_uri
-            ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
+           (match 
+             (C.input_or_locate_uri 
+               ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ()) 
+           with
+           | None -> []
+           | Some uri -> [uri])
         | [uri] -> [uri]
         | _ ->
             C.interactive_user_uri_choice ~selection_mode:`MULTIPLE
@@ -773,7 +787,8 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
     let disambiguate_thing ~dbd ~context ~metasenv
       ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
-      ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing thing
+      ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
+      (thing_txt,thing_txt_prefix_len,thing)
     =
       debug_print (lazy "DISAMBIGUATE INPUT");
       let disambiguate_context =  (* cic context -> disambiguate context *)
@@ -784,7 +799,7 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
       debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
       let thing_dom = domain_of_thing ~context:disambiguate_context thing in
       debug_print (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"
-        (string_of_domain thing_dom)));
+        (string_of_domain (List.map snd thing_dom))));
 (*
       debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
         (DisambiguatePp.pp_environment aliases)));
@@ -852,7 +867,7 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
       let test_env aliases todo_dom ugraph = 
         let filled_env =
           List.fold_left
-            (fun env item ->
+            (fun env (_,item) ->
                Environment.add item
                ("Implicit",
                  (match item with
@@ -886,7 +901,7 @@ in refine_profiler.HExtlib.profile foo ()
             | Ok (thing, metasenv),new_univ -> 
                [ aliases, diff, metasenv, thing, new_univ ], []
             | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg])
-        | item :: remaining_dom ->
+        | (locs,item) :: remaining_dom ->
             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
              (string_of_domain_item item)));
             let choices =
@@ -895,7 +910,8 @@ in refine_profiler.HExtlib.profile foo ()
               | Some choices -> choices in
             match choices with
                [] ->
-                [], [None,lazy ("No choices for " ^ string_of_domain_item item)]
+                [], [Some (List.hd locs),
+                     lazy ("No choices for " ^ string_of_domain_item item)]
              | [codomain_item] ->
                  (* just one choice. We perform a one-step look-up and
                     if the next set of choices is also a singleton we
@@ -906,7 +922,7 @@ in refine_profiler.HExtlib.profile foo ()
                  let lookup_in_todo_dom,next_choice_is_single =
                   match remaining_dom with
                      [] -> None,false
-                   | he::_ ->
+                   | (_,he)::_ ->
                       let choices = lookup_choices he in
                        Some choices,List.length choices = 1
                  in
@@ -962,20 +978,24 @@ in refine_profiler.HExtlib.profile foo ()
              debug_print (lazy "SINGLE INTERPRETATION");
              [diff,metasenv,t,ugraph], false
          | l,_ ->
-             debug_print (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
+             debug_print 
+               (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
              let choices =
                List.map
                  (fun (env, _, _, _, _) ->
                    List.map
-                     (fun domain_item ->
+                     (fun (locs,domain_item) ->
                        let description =
                          fst (Environment.find domain_item env)
                        in
-                       (descr_of_domain_item domain_item, description))
+                       locs,descr_of_domain_item domain_item, description)
                      thing_dom)
                  l
              in
-             let choosed = C.interactive_interpretation_choice choices in
+             let choosed = 
+               C.interactive_interpretation_choice 
+                 thing_txt thing_txt_prefix_len choices 
+             in
              (List.map (fun n->let _,d,m,t,u= List.nth l n in d,m,t,u) choosed),
               true
         in
@@ -985,7 +1005,8 @@ in refine_profiler.HExtlib.profile foo ()
         failwith "Disambiguate: circular dependency"
 
     let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
-      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe term
+      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe 
+      (text,prefix_len,term)
     =
       let term =
         if fresh_instances then CicNotationUtil.freshen_term term else term
@@ -993,10 +1014,10 @@ in refine_profiler.HExtlib.profile foo ()
       disambiguate_thing ~dbd ~context ~metasenv ~initial_ugraph ~aliases
         ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
         ~domain_of_thing:domain_of_term ~interpretate_thing:interpretate_term
-        ~refine_thing:refine_term term
+        ~refine_thing:refine_term (text,prefix_len,term)
 
     let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri
-     obj
+     (text,prefix_len,obj)
     =
       let obj =
         if fresh_instances then CicNotationUtil.freshen_obj obj else obj
@@ -1004,6 +1025,6 @@ in refine_profiler.HExtlib.profile foo ()
       disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~aliases ~universe ~uri
         ~pp_thing:CicNotationPp.pp_obj ~domain_of_thing:domain_of_obj
         ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj
-        obj
+        (text,prefix_len,obj)
   end