]> matita.cs.unibo.it Git - helm.git/commitdiff
housekeeping:
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 4 Dec 2008 13:06:29 +0000 (13:06 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 4 Dec 2008 13:06:29 +0000 (13:06 +0000)
- unused functions removed from Enviconment
- unused file disambiguatePp removed
- disambiguation callbacks pushed down to Disambiguate
  from MultiPassDisambiguator

13 files changed:
helm/software/components/disambiguation/disambiguate.ml
helm/software/components/disambiguation/disambiguate.mli
helm/software/components/disambiguation/disambiguateTypes.ml
helm/software/components/disambiguation/disambiguateTypes.mli
helm/software/components/disambiguation/multiPassDisambiguator.ml
helm/software/components/disambiguation/multiPassDisambiguator.mli
helm/software/components/lexicon/.depend
helm/software/components/lexicon/.depend.opt
helm/software/components/lexicon/Makefile
helm/software/components/lexicon/disambiguatePp.ml [deleted file]
helm/software/components/lexicon/disambiguatePp.mli [deleted file]
helm/software/matita/matitaGui.ml
helm/software/matita/matitaScript.ml

index 748722f5de36f764265e5e513edaeaa97eb4ee59..0b73296e789da2f2adc7993b930da2f489b075a8 100644 (file)
@@ -32,6 +32,8 @@ open UriManager
 
 module Ast = CicNotationPt
 
+(* the integer is an offset to be added to each location *)
+exception Ambiguous_input
 (* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
  int *
@@ -43,12 +45,37 @@ exception PathNotWellFormed
   (** raised when an environment is not enough informative to decide *)
 exception Try_again of string Lazy.t
 
-type ('alias,'term) aliases= bool * 'term DisambiguateTypes.environment
+type ('alias,'term) aliases =
+ bool * 'term DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t
 type 'a disambiguator_input = string * int * 'a
 
 type domain = domain_tree list
 and domain_tree = Node of Stdpp.location list * domain_item * domain
 
+let mono_uris_callback ~selection_mode ?ok
+          ?(enable_button_for_non_vars = true) ~title ~msg ~id =
+ if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
+      "matita.auto_disambiguation"
+ then
+  function l -> l
+ else
+  raise Ambiguous_input
+
+let mono_interp_callback _ _ _ = raise Ambiguous_input
+
+let _choose_uris_callback = ref mono_uris_callback
+let _choose_interp_callback = ref mono_interp_callback
+let set_choose_uris_callback f = _choose_uris_callback := f
+let set_choose_interp_callback f = _choose_interp_callback := f
+
+let interactive_user_uri_choice = !_choose_uris_callback
+let interactive_interpretation_choice interp = !_choose_interp_callback interp
+let input_or_locate_uri ~(title:string) ?id () = None
+  (* Zack: I try to avoid using this callback. I therefore assume that
+  * the presence of an identifier that can't be resolved via "locate"
+  * query is a syntax error *)
+  
+
 let rec string_of_domain =
  function
     [] -> ""
@@ -423,58 +450,50 @@ sig
     list * bool
 end
 
-module Make (C: Callbacks) =
-  struct
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
-    let disambiguate_thing 
-      ~context ~metasenv ~subst ~use_coercions
-      ~string_context_of_context
-      ~initial_ugraph:base_univ ~hint
-      ~mk_implicit ~description_of_alias
-      ~aliases ~universe ~lookup_in_library 
-      ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
-      ~localization_tbl
-      (thing_txt,thing_txt_prefix_len,thing)
-    =
-      debug_print (lazy "DISAMBIGUATE INPUT");
-      debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
-      let thing_dom =
-        domain_of_thing ~context:(string_context_of_context context) thing in
-      debug_print
-       (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
-(*
-      debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s"
-        (DisambiguatePp.pp_environment aliases)));
-      debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s"
-        (match universe with None -> "None" | Some _ -> "Some _")));
-*)
-      let current_dom =
-        Environment.fold (fun item _ dom -> item :: dom) aliases [] in
-      let todo_dom = domain_diff thing_dom current_dom in
-      debug_print
-       (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
-      (* (2) lookup function for any item (Id/Symbol/Num) *)
-      let lookup_choices =
-        fun item ->
-         match universe with
-         | None -> 
-             lookup_in_library 
-               C.interactive_user_uri_choice 
-               C.input_or_locate_uri item
-         | Some e ->
-             (try
-               let item =
-                 match item with
-                 | Symbol (symb, _) -> Symbol (symb, 0)
-                 | item -> item
-               in
-               Environment.find item e
-             with Not_found -> 
-               lookup_in_library 
-                 C.interactive_user_uri_choice 
-                 C.input_or_locate_uri item)
-      in
+let disambiguate_thing 
+  ~context ~metasenv ~subst ~use_coercions
+  ~string_context_of_context
+  ~initial_ugraph:base_univ ~hint
+  ~mk_implicit ~description_of_alias
+  ~aliases ~universe ~lookup_in_library 
+  ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
+  ~localization_tbl
+  (thing_txt,thing_txt_prefix_len,thing)
+=
+  debug_print (lazy "DISAMBIGUATE INPUT");
+  debug_print (lazy ("TERM IS: " ^ (pp_thing thing)));
+  let thing_dom =
+    domain_of_thing ~context:(string_context_of_context context) thing in
+  debug_print
+   (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom)));
+   let current_dom =
+     Environment.fold (fun item _ dom -> item :: dom) aliases [] in
+   let todo_dom = domain_diff thing_dom current_dom in
+   debug_print
+    (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom)));
+   (* (2) lookup function for any item (Id/Symbol/Num) *)
+   let lookup_choices =
+     fun item ->
+      match universe with
+      | None -> 
+          lookup_in_library 
+            interactive_user_uri_choice 
+            input_or_locate_uri item
+      | Some e ->
+          (try
+            let item =
+              match item with
+              | Symbol (symb, _) -> Symbol (symb, 0)
+              | item -> item
+            in
+            Environment.find item e
+          with Not_found -> 
+            lookup_in_library 
+              interactive_user_uri_choice 
+              input_or_locate_uri item)
+   in
 (*
       (* <benchmark> *)
       let _ =
@@ -500,223 +519,221 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
       (* </benchmark> *)
 *)
 
-      (* (3) test an interpretation filling with meta uninterpreted identifiers
-       *)
-      let test_env aliases todo_dom ugraph = 
-        try
-         let rec aux env = function
-          | [] -> env
-          | Node (_, item, l) :: tl ->
-              let env =
-                Environment.add item
-                 (mk_implicit
-                   (match item with | Id _ | Num _ -> true | Symbol _ -> false))
-                 env in
-              aux (aux env l) tl in
-         let filled_env = aux aliases todo_dom in
-          let cic_thing =
-            interpretate_thing ~context ~env:filled_env
-             ~uri ~is_path:false thing ~localization_tbl
-          in
-          let cic_thing = (fst hint) metasenv cic_thing in
+   (* (3) test an interpretation filling with meta uninterpreted identifiers
+    *)
+   let test_env aliases todo_dom ugraph = 
+     try
+      let rec aux env = function
+       | [] -> env
+       | Node (_, item, l) :: tl ->
+           let env =
+             Environment.add item
+              (mk_implicit
+                (match item with | Id _ | Num _ -> true | Symbol _ -> false))
+              env in
+           aux (aux env l) tl in
+      let filled_env = aux aliases todo_dom in
+       let cic_thing =
+         interpretate_thing ~context ~env:filled_env
+          ~uri ~is_path:false thing ~localization_tbl
+       in
+       let cic_thing = (fst hint) metasenv cic_thing in
 let foo () =
-          let k =
-           refine_thing metasenv subst context uri
-            ~use_coercions cic_thing ugraph ~localization_tbl
-          in
-          let k = (snd hint) k in
-            k
+       let k =
+        refine_thing metasenv subst context uri
+         ~use_coercions cic_thing ugraph ~localization_tbl
+       in
+       let k = (snd hint) k in
+         k
 in refine_profiler.HExtlib.profile foo ()
-        with
-        | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
-        | Invalid_choice loc_msg -> Ko loc_msg
-      in
-      (* (4) build all possible interpretations *)
-      let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
-      (* aux returns triples Ok/Uncertain/Ko *)
-      (* rem_dom is the concatenation of all the remainin domains *)
-      let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom =
-        debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
-        match todo_dom with
-        | [] ->
-            assert (lookup_in_todo_dom = None);
-            (match test_env aliases rem_dom base_univ with
-            | Ok (thing, metasenv,subst,new_univ) -> 
-               [ aliases, diff, metasenv, subst, thing, new_univ ], [], []
-            | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true]
-            | Uncertain loc_msg ->
-               [],[aliases,diff,loc_msg],[])
-        | Node (locs,item,inner_dom) :: remaining_dom ->
-            debug_print (lazy (sprintf "CHOOSED ITEM: %s"
-             (string_of_domain_item item)));
-            let choices =
-             match lookup_in_todo_dom with
-                None -> lookup_choices item
-              | Some choices -> choices in
-            match choices with
-               [] ->
-                [], [],
-                 [aliases, diff, 
-                  (lazy (List.hd locs,
-                    "No choices for " ^ string_of_domain_item item)),
-                  true]
+     with
+     | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
+     | Invalid_choice loc_msg -> Ko loc_msg
+   in
+   (* (4) build all possible interpretations *)
+   let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
+   (* aux returns triples Ok/Uncertain/Ko *)
+   (* rem_dom is the concatenation of all the remainin domains *)
+   let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom =
+     debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom));
+     match todo_dom with
+     | [] ->
+         assert (lookup_in_todo_dom = None);
+         (match test_env aliases rem_dom base_univ with
+         | Ok (thing, metasenv,subst,new_univ) -> 
+            [ aliases, diff, metasenv, subst, thing, new_univ ], [], []
+         | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true]
+         | Uncertain loc_msg ->
+            [],[aliases,diff,loc_msg],[])
+     | Node (locs,item,inner_dom) :: remaining_dom ->
+         debug_print (lazy (sprintf "CHOOSED ITEM: %s"
+          (string_of_domain_item item)));
+         let choices =
+          match lookup_in_todo_dom with
+             None -> lookup_choices item
+           | Some choices -> choices in
+         match choices with
+            [] ->
+             [], [],
+              [aliases, diff, 
+               (lazy (List.hd locs,
+                 "No choices for " ^ string_of_domain_item item)),
+               true]
 (*
-             | [codomain_item] ->
-                 (* just one choice. We perform a one-step look-up and
-                    if the next set of choices is also a singleton we
-                    skip this refinement step *)
-                 debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
-                 let new_env = Environment.add item codomain_item aliases in
-                 let new_diff = (item,codomain_item)::diff in
-                 let lookup_in_todo_dom,next_choice_is_single =
-                  match remaining_dom with
-                     [] -> None,false
-                   | (_,he)::_ ->
-                      let choices = lookup_choices he in
-                       Some choices,List.length choices = 1
-                 in
-                  if next_choice_is_single then
-                   aux new_env new_diff lookup_in_todo_dom remaining_dom
-                    base_univ
-                  else
-                    (match test_env new_env remaining_dom base_univ with
-                    | Ok (thing, metasenv),new_univ ->
-                        (match remaining_dom with
-                        | [] ->
-                           [ new_env, new_diff, metasenv, thing, new_univ ], []
-                        | _ ->
-                           aux new_env new_diff lookup_in_todo_dom
-                            remaining_dom new_univ)
-                    | Uncertain (loc,msg),new_univ ->
-                        (match remaining_dom with
-                        | [] -> [], [new_env,new_diff,loc,msg,true]
-                        | _ ->
-                           aux new_env new_diff lookup_in_todo_dom
-                            remaining_dom new_univ)
-                    | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
+          | [codomain_item] ->
+              (* just one choice. We perform a one-step look-up and
+                 if the next set of choices is also a singleton we
+                 skip this refinement step *)
+              debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));
+              let new_env = Environment.add item codomain_item aliases in
+              let new_diff = (item,codomain_item)::diff in
+              let lookup_in_todo_dom,next_choice_is_single =
+               match remaining_dom with
+                  [] -> None,false
+                | (_,he)::_ ->
+                   let choices = lookup_choices he in
+                    Some choices,List.length choices = 1
+              in
+               if next_choice_is_single then
+                aux new_env new_diff lookup_in_todo_dom remaining_dom
+                 base_univ
+               else
+                 (match test_env new_env remaining_dom base_univ with
+                 | Ok (thing, metasenv),new_univ ->
+                     (match remaining_dom with
+                     | [] ->
+                        [ new_env, new_diff, metasenv, thing, new_univ ], []
+                     | _ ->
+                        aux new_env new_diff lookup_in_todo_dom
+                         remaining_dom new_univ)
+                 | Uncertain (loc,msg),new_univ ->
+                     (match remaining_dom with
+                     | [] -> [], [new_env,new_diff,loc,msg,true]
+                     | _ ->
+                        aux new_env new_diff lookup_in_todo_dom
+                         remaining_dom new_univ)
+                 | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true])
 *)
-             | _::_ ->
-                 let mark_not_significant failures =
-                   List.map
-                    (fun (env, diff, loc_msg, _b) ->
-                      env, diff, loc_msg, false)
-                    failures in
-                 let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
-                  if ok_l <> [] || uncertain_l <> [] then
-                   ok_l,uncertain_l,mark_not_significant error_l
-                  else
-                   outcome in
-               let rec filter = function 
-                | [] -> [],[],[]
-                | codomain_item :: tl ->
-                    (*debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));*)
-                    let new_env = Environment.add item codomain_item aliases in
-                    let new_diff = (item,codomain_item)::diff in
-                    (match
-                      test_env new_env 
-                        (inner_dom@remaining_dom@rem_dom) base_univ
-                     with
-                    | Ok (thing, metasenv,subst,new_univ) ->
-                        let res = 
-                          (match inner_dom with
-                          | [] ->
-                             [new_env,new_diff,metasenv,subst,thing,new_univ],
-                             [], []
-                          | _ ->
-                             aux new_env new_diff None inner_dom
-                              (remaining_dom@rem_dom) 
-                          ) 
-                        in
-                         res @@ filter tl
-                    | Uncertain loc_msg ->
-                        let res =
-                          (match inner_dom with
-                          | [] -> [],[new_env,new_diff,loc_msg],[]
-                          | _ ->
-                             aux new_env new_diff None inner_dom
-                              (remaining_dom@rem_dom) 
-                          )
-                        in
-                         res @@ filter tl
-                    | Ko loc_msg ->
-                        let res = [],[],[new_env,new_diff,loc_msg,true] in
-                         res @@ filter tl)
-               in
-                let ok_l,uncertain_l,error_l =
-                 classify_errors (filter choices)
-                in
-                 let res_after_ok_l =
-                  List.fold_right
-                   (fun (env,diff,_,_,_,_) res ->
-                     aux env diff None remaining_dom rem_dom @@ res
-                   ) ok_l ([],[],error_l)
-                in
-                 List.fold_right
-                  (fun (env,diff,_) res ->
-                    aux env diff None remaining_dom rem_dom @@ res
-                  ) uncertain_l res_after_ok_l
-      in
-      let aux' aliases diff lookup_in_todo_dom todo_dom =
-       match test_env aliases todo_dom base_univ with
-        | Ok _
-        | Uncertain _ ->
-           aux aliases diff lookup_in_todo_dom todo_dom [] 
-        | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true]
-      in
-        let res =
-         match aux' aliases [] None todo_dom with
-         | [],uncertain,errors ->
-            let errors =
-             List.map
-              (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true)
-              ) uncertain @ errors
+          | _::_ ->
+              let mark_not_significant failures =
+                List.map
+                 (fun (env, diff, loc_msg, _b) ->
+                   env, diff, loc_msg, false)
+                 failures in
+              let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
+               if ok_l <> [] || uncertain_l <> [] then
+                ok_l,uncertain_l,mark_not_significant error_l
+               else
+                outcome in
+            let rec filter = function 
+             | [] -> [],[],[]
+             | codomain_item :: tl ->
+                 (*debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));*)
+                let new_env = Environment.add item codomain_item aliases in
+                let new_diff = (item,codomain_item)::diff in
+                (match
+                  test_env new_env 
+                    (inner_dom@remaining_dom@rem_dom) base_univ
+                 with
+                | Ok (thing, metasenv,subst,new_univ) ->
+                    let res = 
+                      (match inner_dom with
+                      | [] ->
+                         [new_env,new_diff,metasenv,subst,thing,new_univ],
+                         [], []
+                      | _ ->
+                         aux new_env new_diff None inner_dom
+                          (remaining_dom@rem_dom) 
+                      ) 
+                    in
+                     res @@ filter tl
+                | Uncertain loc_msg ->
+                    let res =
+                      (match inner_dom with
+                      | [] -> [],[new_env,new_diff,loc_msg],[]
+                      | _ ->
+                         aux new_env new_diff None inner_dom
+                          (remaining_dom@rem_dom) 
+                      )
+                    in
+                     res @@ filter tl
+                | Ko loc_msg ->
+                    let res = [],[],[new_env,new_diff,loc_msg,true] in
+                     res @@ filter tl)
+           in
+            let ok_l,uncertain_l,error_l =
+             classify_errors (filter choices)
             in
-            let errors =
-             List.map
-              (fun (env,diff,loc_msg,significant) ->
-                let env' =
-                 filter_map_domain
-                   (fun locs domain_item ->
-                     try
-                      let description =
-                       description_of_alias (Environment.find domain_item env)
-                      in
-                       Some (locs,descr_of_domain_item domain_item,description)
-                     with
-                      Not_found -> None)
-                   thing_dom
-                in
-                let diff= List.map (fun a,b -> a,description_of_alias b) diff in
-                 env',diff,loc_msg,significant
-              ) errors
+             let res_after_ok_l =
+              List.fold_right
+               (fun (env,diff,_,_,_,_) res ->
+                 aux env diff None remaining_dom rem_dom @@ res
+               ) ok_l ([],[],error_l)
             in
-             raise (NoWellTypedInterpretation (0,errors))
-         | [_,diff,metasenv,subst,t,ugraph],_,_ ->
-             debug_print (lazy "SINGLE INTERPRETATION");
-             [diff,metasenv,subst,t,ugraph], false
-         | l,_,_ ->
-             debug_print 
-               (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
-             let choices =
-               List.map
-                 (fun (env, _, _, _, _, _) ->
-                   map_domain
-                     (fun locs domain_item ->
-                       let description =
-                         description_of_alias (Environment.find domain_item env)
-                       in
-                       locs,descr_of_domain_item domain_item, description)
-                     thing_dom)
-                 l
-             in
-             let choosed = 
-               C.interactive_interpretation_choice 
-                 thing_txt thing_txt_prefix_len choices 
-             in
-             (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u)
-               choosed),
-              true
+             List.fold_right
+              (fun (env,diff,_) res ->
+                aux env diff None remaining_dom rem_dom @@ res
+              ) uncertain_l res_after_ok_l
+  in
+  let aux' aliases diff lookup_in_todo_dom todo_dom =
+   match test_env aliases todo_dom base_univ with
+    | Ok _
+    | Uncertain _ ->
+       aux aliases diff lookup_in_todo_dom todo_dom [] 
+    | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true]
+  in
+    let res =
+     match aux' aliases [] None todo_dom with
+     | [],uncertain,errors ->
+        let errors =
+         List.map
+          (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true)
+          ) uncertain @ errors
         in
-         res
-
-  end
+        let errors =
+         List.map
+          (fun (env,diff,loc_msg,significant) ->
+            let env' =
+             filter_map_domain
+               (fun locs domain_item ->
+                 try
+                  let description =
+                   description_of_alias (Environment.find domain_item env)
+                  in
+                   Some (locs,descr_of_domain_item domain_item,description)
+                 with
+                  Not_found -> None)
+               thing_dom
+            in
+            let diff= List.map (fun a,b -> a,description_of_alias b) diff in
+             env',diff,loc_msg,significant
+          ) errors
+        in
+         raise (NoWellTypedInterpretation (0,errors))
+     | [_,diff,metasenv,subst,t,ugraph],_,_ ->
+         debug_print (lazy "SINGLE INTERPRETATION");
+         [diff,metasenv,subst,t,ugraph], false
+     | l,_,_ ->
+         debug_print 
+           (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l)));
+         let choices =
+           List.map
+             (fun (env, _, _, _, _, _) ->
+               map_domain
+                 (fun locs domain_item ->
+                   let description =
+                     description_of_alias (Environment.find domain_item env)
+                   in
+                   locs,descr_of_domain_item domain_item, description)
+                 thing_dom)
+             l
+         in
+         let choosed = 
+           interactive_interpretation_choice 
+             thing_txt thing_txt_prefix_len choices 
+         in
+         (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u)
+           choosed),
+          true
+    in
+     res
index 5088f8a5f57e17259b586ee9c4a112f8b88c9147..cb1882a7d12a900b0e51a39c4e943c32786c623d 100644 (file)
 
 (** {2 Disambiguation interface} *)
 
+(** raised when ambiguous input is found but not expected (e.g. in the batch
+  * compiler) *)
+exception Ambiguous_input
+
 (* the integer is an offset to be added to each location *)
 (* list of located error messages, each list is a tuple:
   * - environment in string form
@@ -54,6 +58,22 @@ type ('term,'metasenv,'subst,'graph) test_result =
 
 exception Try_again of string Lazy.t
 
+val set_choose_uris_callback:
+  DisambiguateTypes.interactive_user_uri_choice_type -> unit
+
+val set_choose_interp_callback:
+  DisambiguateTypes.interactive_interpretation_choice_type -> unit
+
+(** @raise Ambiguous_input if called, default value for internal
+  * choose_uris_callback if not set otherwise with set_choose_uris_callback
+  * above *)
+val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type
+
+(** @raise Ambiguous_input if called, default value for internal
+  * choose_interp_callback if not set otherwise with set_choose_interp_callback
+  * above *)
+val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type
+
 val resolve : 
   env:'alias DisambiguateTypes.Environment.t ->
   mk_choice:('alias -> 'term DisambiguateTypes.codomain_item) ->
@@ -68,49 +88,43 @@ val domain_of_term: context:
 val domain_of_obj: 
   context:string option list -> CicNotationPt.term CicNotationPt.obj -> domain
 
-module type Disambiguator =
-sig
-  val disambiguate_thing:
+val disambiguate_thing:
+  context:'context ->
+  metasenv:'metasenv ->
+  subst:'subst ->
+  use_coercions:bool ->
+  string_context_of_context:('context -> string option list) ->
+  initial_ugraph:'ugraph ->
+  hint: 
+    ('metasenv -> 'raw_thing -> 'raw_thing) * 
+    (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
+       ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
+  mk_implicit:(bool -> 'alias) ->
+  description_of_alias:('alias -> string) ->
+  aliases:'alias DisambiguateTypes.Environment.t ->
+  universe:'alias list DisambiguateTypes.Environment.t option ->
+  lookup_in_library:(
+    DisambiguateTypes.interactive_user_uri_choice_type ->
+    DisambiguateTypes.input_or_locate_uri_type ->
+    DisambiguateTypes.Environment.key ->
+    'alias list) ->
+  uri:'uri ->
+  pp_thing:('ast_thing -> string) ->
+  domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
+  interpretate_thing:(
     context:'context ->
-    metasenv:'metasenv ->
-    subst:'subst ->
-    use_coercions:bool ->
-    string_context_of_context:('context -> string option list) ->
-    initial_ugraph:'ugraph ->
-    hint: 
-      ('metasenv -> 'raw_thing -> 'raw_thing) * 
-      (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
-         ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
-    mk_implicit:(bool -> 'alias) ->
-    description_of_alias:('alias -> string) ->
-    aliases:'alias DisambiguateTypes.Environment.t ->
-    universe:'alias list DisambiguateTypes.Environment.t option ->
-    lookup_in_library:(
-      DisambiguateTypes.interactive_user_uri_choice_type ->
-      DisambiguateTypes.input_or_locate_uri_type ->
-      DisambiguateTypes.Environment.key ->
-      'alias list) ->
+    env:'alias DisambiguateTypes.Environment.t ->
     uri:'uri ->
-    pp_thing:('ast_thing -> string) ->
-    domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
-    interpretate_thing:(
-      context:'context ->
-      env:'alias DisambiguateTypes.Environment.t ->
-      uri:'uri ->
-      is_path:bool -> 
-      'ast_thing -> 
-      localization_tbl:'cichash -> 
-        'raw_thing) ->
-    refine_thing:(
-      'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
-      'raw_thing -> 'ugraph -> localization_tbl:'cichash -> 
-        ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
-    localization_tbl:'cichash ->
-    string * int * 'ast_thing ->
-    ((DisambiguateTypes.Environment.key * 'alias) list * 
-     'metasenv * 'subst * 'refined_thing * 'ugraph)
-    list * bool
-end
-
-module Make (C : DisambiguateTypes.Callbacks) : Disambiguator
-
+    is_path:bool -> 
+    'ast_thing -> 
+    localization_tbl:'cichash -> 
+      'raw_thing) ->
+  refine_thing:(
+    'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
+    'raw_thing -> 'ugraph -> localization_tbl:'cichash -> 
+      ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
+  localization_tbl:'cichash ->
+  string * int * 'ast_thing ->
+  ((DisambiguateTypes.Environment.key * 'alias) list * 
+   'metasenv * 'subst * 'refined_thing * 'ugraph)
+  list * bool
index eb12395230cc3479028b2395cfc4120eacade6c5..496c7db35203476b25a3656a01da0e6f7958da36 100644 (file)
@@ -62,17 +62,6 @@ struct
       add k (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env
     with Not_found ->
       add k [v] env
-
-  let hd list_env =
-    try
-      map List.hd list_env
-    with Failure _ -> assert false
-
-  let fold_flatten f env base =
-    fold
-      (fun k l acc -> List.fold_right (fun v acc -> f k v acc) l acc)
-      env base
-
 end
 
 type 'term codomain_item =
@@ -80,11 +69,6 @@ type 'term codomain_item =
    [`Num_interp of string -> 'term
    |`Sym_interp of 'term list -> 'term]
 
-and 'term environment = 'term codomain_item Environment.t
-
-type 'term multiple_environment =
- 'term codomain_item list Environment.t
-
 type interactive_user_uri_choice_type =
   selection_mode:[`SINGLE | `MULTIPLE] ->
   ?ok:string ->
@@ -98,16 +82,6 @@ type interactive_interpretation_choice_type = string -> int ->
 type input_or_locate_uri_type = 
   title:string -> ?id:string -> unit -> UriManager.uri option
 
-module type Callbacks =
-  sig
-    val interactive_user_uri_choice : interactive_user_uri_choice_type
-
-    val interactive_interpretation_choice : 
-       interactive_interpretation_choice_type
-
-    val input_or_locate_uri: input_or_locate_uri_type
-  end
-
 let string_of_domain_item = function
   | Id s -> Printf.sprintf "ID(%s)" s
   | Symbol (s, i) -> Printf.sprintf "SYMBOL(%s,%d)" s i
index 15f9d8d30bec0545beb7b40b73e406bbc7480c36..43cfc2316120c2fd05f15e492284d7af439ed5b6 100644 (file)
@@ -33,10 +33,6 @@ module Environment:
 sig
   include Map.S with type key = domain_item
   val cons: ('b -> 'a) -> domain_item -> 'b -> 'b list t -> 'b list t
-  val hd: 'a list t -> 'a t
-
-    (** last alias cons-ed will be processed first *)
-  val fold_flatten: (domain_item -> 'a -> 'b -> 'b) -> 'a list t -> 'b -> 'b
 end
 
   (** to be raised when a choice is invalid due to some given parameter (e.g.
@@ -48,11 +44,6 @@ type 'term codomain_item =
    [`Num_interp of string -> 'term
    |`Sym_interp of 'term list -> 'term]
 
-and 'term environment = 'term codomain_item Environment.t
-
-type 'term multiple_environment =
- 'term codomain_item list Environment.t
-
 type interactive_user_uri_choice_type =
   selection_mode:[`SINGLE | `MULTIPLE] ->
   ?ok:string ->
@@ -66,29 +57,5 @@ type interactive_interpretation_choice_type = string -> int ->
 type input_or_locate_uri_type = 
   title:string -> ?id:string -> unit -> UriManager.uri option
 
-module type Callbacks =
-  sig
-
-    val interactive_user_uri_choice : interactive_user_uri_choice_type
-
-    val interactive_interpretation_choice : 
-       interactive_interpretation_choice_type
-
-    val input_or_locate_uri: input_or_locate_uri_type
-  end
-
 val string_of_domain_item: domain_item -> string
 val string_of_domain: domain_item list -> string
-
-(** {3 type shortands} *)
-
-(*
-type term = CicNotationPt.term
-type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic
-type tactical = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactical
-
-type script_entry =
-  | Command of tactical
-  | Comment of CicNotationPt.location * string
-type script = CicNotationPt.location * script_entry list
-*)
index 039fdd57a0518f0c06912e64f108fece9b2b0498..07bbdeba29d68e389590bd3b72650ac1bbe63d2f 100644 (file)
@@ -31,8 +31,6 @@ let debug = false;;
 let debug_print s =
  if debug then prerr_endline (Lazy.force s);;
 
-exception Ambiguous_input
-(* the integer is an offset to be added to each location *)
 exception DisambiguationError of
  int *
  ((Stdpp.location list * string * string) list *
@@ -40,37 +38,6 @@ exception DisambiguationError of
   (Stdpp.location * string) Lazy.t * bool) list list
   (** parameters are: option name, error message *)
 
-let mono_uris_callback ~selection_mode ?ok
-          ?(enable_button_for_non_vars = true) ~title ~msg ~id =
- if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
-      "matita.auto_disambiguation"
- then
-  function l -> l
- else
-  raise Ambiguous_input
-
-let mono_interp_callback _ _ _ = raise Ambiguous_input
-
-let _choose_uris_callback = ref mono_uris_callback
-let _choose_interp_callback = ref mono_interp_callback
-let set_choose_uris_callback f = _choose_uris_callback := f
-let set_choose_interp_callback f = _choose_interp_callback := f
-
-module Callbacks =
-  struct
-    let interactive_user_uri_choice = !_choose_uris_callback
-
-    let interactive_interpretation_choice interp =
-      !_choose_interp_callback interp
-
-    let input_or_locate_uri ~(title:string) ?id () = None
-      (* Zack: I try to avoid using this callback. I therefore assume that
-      * the presence of an identifier that can't be resolved via "locate"
-      * query is a syntax error *)
-  end
-  
-module Disambiguator = Disambiguate.Make (Callbacks)
-
 (* implement module's API *)
 
 let only_one_pass = ref false;;
@@ -180,7 +147,7 @@ let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
   let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) =
     let thing = if fresh_instances then freshen_thing thing else thing
     in
-     Disambiguator.disambiguate_thing
+     Disambiguate.disambiguate_thing
       ~context ~metasenv ~subst ~use_coercions ~string_context_of_context
       ~initial_ugraph ~hint ~mk_implicit ~description_of_alias
       ~aliases ~universe ~lookup_in_library 
index 27d5ca618fabde013d7e542684f814f805074a4f..777fedafd1d3353617c38094b62303970c59a4dc 100644 (file)
@@ -23,9 +23,6 @@
  * http://helm.cs.unibo.it/
  *)
 
-(** raised when ambiguous input is found but not expected (e.g. in the batch
-  * compiler) *)
-exception Ambiguous_input
 (* the integer is an offset to be added to each location *)
 exception DisambiguationError of
  int *
@@ -39,22 +36,6 @@ val only_one_pass: bool ref
 
 val passes : unit -> (bool * [> `Library | `Mono | `Multi ] * bool) list
 
-val set_choose_uris_callback:
-  DisambiguateTypes.interactive_user_uri_choice_type -> unit
-
-val set_choose_interp_callback:
-  DisambiguateTypes.interactive_interpretation_choice_type -> unit
-
-(** @raise Ambiguous_input if called, default value for internal
-  * choose_uris_callback if not set otherwise with set_choose_uris_callback
-  * above *)
-val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type
-
-(** @raise Ambiguous_input if called, default value for internal
-  * choose_interp_callback if not set otherwise with set_choose_interp_callback
-  * above *)
-val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type
-
 val disambiguate_thing:
   passes:(bool * [ `Library | `Mono | `Multi ] * bool) list ->
   freshen_thing: ('ast_thing -> 'ast_thing) ->
index 452167c72d320ba2037698d1a4ab8f836752a6db..33e89a7d9cbc750f0e8ac70a2243407fe6319437 100644 (file)
@@ -1,20 +1,19 @@
 lexiconAstPp.cmi: lexiconAst.cmo 
-disambiguatePp.cmi: lexiconAst.cmo 
 lexiconMarshal.cmi: lexiconAst.cmo 
 cicNotation.cmi: lexiconAst.cmo 
 lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmo cicNotation.cmi 
-lexiconSync.cmi: lexiconEngine.cmi 
+lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmo 
 lexiconAstPp.cmo: lexiconAst.cmo lexiconAstPp.cmi 
 lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi 
-disambiguatePp.cmo: lexiconAstPp.cmi lexiconAst.cmo disambiguatePp.cmi 
-disambiguatePp.cmx: lexiconAstPp.cmx lexiconAst.cmx disambiguatePp.cmi 
 lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmo lexiconMarshal.cmi 
 lexiconMarshal.cmx: lexiconAstPp.cmx lexiconAst.cmx lexiconMarshal.cmi 
 cicNotation.cmo: lexiconAst.cmo cicNotation.cmi 
 cicNotation.cmx: lexiconAst.cmx cicNotation.cmi 
-lexiconEngine.cmo: lexiconMarshal.cmi lexiconAst.cmo disambiguatePp.cmi \
-    cicNotation.cmi lexiconEngine.cmi 
-lexiconEngine.cmx: lexiconMarshal.cmx lexiconAst.cmx disambiguatePp.cmx \
-    cicNotation.cmx lexiconEngine.cmi 
-lexiconSync.cmo: lexiconEngine.cmi cicNotation.cmi lexiconSync.cmi 
-lexiconSync.cmx: lexiconEngine.cmx cicNotation.cmx lexiconSync.cmi 
+lexiconEngine.cmo: lexiconMarshal.cmi lexiconAst.cmo cicNotation.cmi \
+    lexiconEngine.cmi 
+lexiconEngine.cmx: lexiconMarshal.cmx lexiconAst.cmx cicNotation.cmx \
+    lexiconEngine.cmi 
+lexiconSync.cmo: lexiconEngine.cmi lexiconAst.cmo cicNotation.cmi \
+    lexiconSync.cmi 
+lexiconSync.cmx: lexiconEngine.cmx lexiconAst.cmx cicNotation.cmx \
+    lexiconSync.cmi 
index 7fec1d3b5a10d92a8f93860958432115df75d218..1b4992009ef8f70fb79e2ba7de86aefceef5513f 100644 (file)
@@ -1,20 +1,19 @@
 lexiconAstPp.cmi: lexiconAst.cmx 
-disambiguatePp.cmi: lexiconAst.cmx 
 lexiconMarshal.cmi: lexiconAst.cmx 
 cicNotation.cmi: lexiconAst.cmx 
 lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi 
-lexiconSync.cmi: lexiconEngine.cmi 
+lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmx 
 lexiconAstPp.cmo: lexiconAst.cmx lexiconAstPp.cmi 
 lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi 
-disambiguatePp.cmo: lexiconAstPp.cmi lexiconAst.cmx disambiguatePp.cmi 
-disambiguatePp.cmx: lexiconAstPp.cmx lexiconAst.cmx disambiguatePp.cmi 
 lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmx lexiconMarshal.cmi 
 lexiconMarshal.cmx: lexiconAstPp.cmx lexiconAst.cmx lexiconMarshal.cmi 
 cicNotation.cmo: lexiconAst.cmx cicNotation.cmi 
 cicNotation.cmx: lexiconAst.cmx cicNotation.cmi 
-lexiconEngine.cmo: lexiconMarshal.cmi lexiconAst.cmx disambiguatePp.cmi \
-    cicNotation.cmi lexiconEngine.cmi 
-lexiconEngine.cmx: lexiconMarshal.cmx lexiconAst.cmx disambiguatePp.cmx \
-    cicNotation.cmx lexiconEngine.cmi 
-lexiconSync.cmo: lexiconEngine.cmi cicNotation.cmi lexiconSync.cmi 
-lexiconSync.cmx: lexiconEngine.cmx cicNotation.cmx lexiconSync.cmi 
+lexiconEngine.cmo: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi \
+    lexiconEngine.cmi 
+lexiconEngine.cmx: lexiconMarshal.cmx lexiconAst.cmx cicNotation.cmx \
+    lexiconEngine.cmi 
+lexiconSync.cmo: lexiconEngine.cmi lexiconAst.cmx cicNotation.cmi \
+    lexiconSync.cmi 
+lexiconSync.cmx: lexiconEngine.cmx lexiconAst.cmx cicNotation.cmx \
+    lexiconSync.cmi 
index b8582bacac18d5103e3130f09a6cd556d5199440..d5b16e92446f793f79cdf417bccc2ad32548e30e 100644 (file)
@@ -3,7 +3,6 @@ PREDICATES =
 
 INTERFACE_FILES =              \
        lexiconAstPp.mli                \
-       disambiguatePp.mli      \
        lexiconMarshal.mli      \
        cicNotation.mli         \
        lexiconEngine.mli       \
diff --git a/helm/software/components/lexicon/disambiguatePp.ml b/helm/software/components/lexicon/disambiguatePp.ml
deleted file mode 100644 (file)
index a8590cf..0000000
+++ /dev/null
@@ -1,47 +0,0 @@
-(* Copyright (C) 2005, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-(* $Id$ *)
-
-open DisambiguateTypes
-
-let alias_of_domain_and_desc domain_item dsc =
- match domain_item with
-    Id id -> LexiconAst.Ident_alias (id, dsc)
-  | Symbol (symb, i) -> LexiconAst.Symbol_alias (symb, i, dsc)
-  | Num i -> LexiconAst.Number_alias (i, dsc)
-
-let aliases_of_environment env =
-  Environment.fold
-    (fun domain_item codomain_item acc ->
-      alias_of_domain_and_desc domain_item (fst codomain_item)::acc
-    ) env []
-
-let pp_environment env =
-  let aliases = aliases_of_environment env in
-  let strings =
-    List.map (fun alias -> LexiconAstPp.pp_alias alias ^ ".") aliases
-  in
-  String.concat "\n" (List.sort compare strings)
diff --git a/helm/software/components/lexicon/disambiguatePp.mli b/helm/software/components/lexicon/disambiguatePp.mli
deleted file mode 100644 (file)
index c41bf6d..0000000
+++ /dev/null
@@ -1,29 +0,0 @@
-(* Copyright (C) 2005, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://helm.cs.unibo.it/
- *)
-
-val alias_of_domain_and_desc:
-  DisambiguateTypes.domain_item -> string -> LexiconAst.alias_spec
-
-val pp_environment: Cic.term DisambiguateTypes.environment -> string
index 5200a21baf371011478d6e840da52f61d3dd74f2..f68421e0cfe5483c7be23a2f989d42352852c5bc 100644 (file)
@@ -328,7 +328,15 @@ let rec interactive_error_interp ~all_passes
              ("" ::
                List.map
                 (fun k,desc -> 
-                  let alias = DisambiguatePp.alias_of_domain_and_desc k desc in
+                  let alias =
+                   match k with
+                   | DisambiguateTypes.Id id ->
+                       LexiconAst.Ident_alias (id, desc)
+                   | DisambiguateTypes.Symbol (symb, i)-> 
+                       LexiconAst.Symbol_alias (symb, i, desc)
+                   | DisambiguateTypes.Num i ->
+                       LexiconAst.Number_alias (i, desc)
+                  in
                    LexiconAstPp.pp_alias alias)
                 diff) ^ "\n"
            in
@@ -1567,10 +1575,10 @@ let interactive_interp_choice () text prefix_len choices =
 
 let _ =
   (* disambiguator callbacks *)
-  MultiPassDisambiguator.set_choose_uris_callback
+  Disambiguate.set_choose_uris_callback
    (fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg ->
      interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ());
-  MultiPassDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
+  Disambiguate.set_choose_interp_callback (interactive_interp_choice ());
   (* gtk initialization *)
   GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
   GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf;
index fe82e939cc01926ff000950bfb375a8e401309b2..a5e24d3150853ce71cf11e5662c31b480ecf0f30 100644 (file)
@@ -76,7 +76,6 @@ let eval_with_engine include_paths guistuff lexicon_status grafite_status user_g
 =
   let module TAPp = GrafiteAstPp in
   let module DTE = DisambiguateTypes.Environment in
-  let module DP = DisambiguatePp in
   let parsed_text_length =
     String.length skipped_txt + String.length nonskipped_txt 
   in