X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2FmultiPassDisambiguator.ml;h=86d037742652c99085ff07092dceaf371447d5dd;hb=7f9e313fe5ae4200f080f481a6b8b795a0618093;hp=af4a9e49e7b459788912eb59da394e555573d62e;hpb=3323758b99384afb5c7a70aa31bc006a78af64dd;p=helm.git diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml index af4a9e49e..86d037742 100644 --- a/helm/software/components/disambiguation/multiPassDisambiguator.ml +++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml @@ -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,57 +38,32 @@ 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;; +let use_library = ref false;; let passes () = (* *) if !only_one_pass then [ (true, `Mono, false) ] + else if !use_library then + [ (true, `Library, false); + (* for demo to reduce the number of interpretations *) + (true, `Library, true); + ] else [ (true, `Mono, false); (true, `Multi, false); (true, `Mono, true); (true, `Multi, true); - (true, `Library, false); - (* for demo to reduce the number of interpretations *) - (true, `Library, true); ] ;; -let drop_aliases ?(minimize_instances=false) (choices, user_asked) = +let drop_aliases ?(minimize_instances=false) ~description_of_alias + (choices, user_asked) += let module D = DisambiguateTypes in + let compare ci1 ci2 = description_of_alias ci1 = description_of_alias ci2 in let minimize d = if not minimize_instances then d @@ -98,23 +71,23 @@ let drop_aliases ?(minimize_instances=false) (choices, user_asked) = let rec aux = function [] -> [] - | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 -> + | (D.Symbol (s,n),ci1) as he::tl when n > 0 -> if List.for_all (function - (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2 + (D.Symbol (s2,_),ci2) -> s2 <> s || compare ci1 ci2 | _ -> true ) d then - (D.Symbol (s,0),ci)::(aux tl) + (D.Symbol (s,0),ci1)::(aux tl) else he::(aux tl) - | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 -> + | (D.Num n,ci1) as he::tl when n > 0 -> if List.for_all - (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d + (function (D.Num _,ci2) -> compare ci1 ci2 | _ -> true) d then - (D.Num 0,ci)::(aux tl) + (D.Num 0,ci1)::(aux tl) else he::(aux tl) | he::tl -> he::(aux tl) @@ -128,7 +101,8 @@ let drop_aliases_and_clear_diff (choices, user_asked) = (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices), user_asked -let disambiguate_thing ~passes ~aliases ~universe ~f thing = +let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing += assert (universe <> None); let library = false, DisambiguateTypes.Environment.empty, None in let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in @@ -145,9 +119,9 @@ let disambiguate_thing ~passes ~aliases ~universe ~f thing = in let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) = if use_mono_aliases then - drop_aliases ~minimize_instances:true res (* one shot aliases *) + drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *) else if user_asked then - drop_aliases ~minimize_instances:true res (* one shot aliases *) + drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *) else drop_aliases_and_clear_diff res in @@ -169,19 +143,17 @@ let disambiguate_thing ~passes ~aliases ~universe ~f thing = aux 1 [] passes let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst - ~mk_implicit ~string_context_of_context ~initial_ugraph ~hint ~aliases - ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing - ~interpretate_thing ~refine_thing ~localization_tbl thing + ~string_context_of_context ~initial_ugraph ~expty ~mk_implicit + ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing + ~domain_of_thing ~interpretate_thing ~refine_thing ~mk_localization_tbl thing = 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 - ~context ~metasenv ~subst ~use_coercions - ~mk_implicit ~string_context_of_context - ~initial_ugraph ~hint + let thing = if fresh_instances then freshen_thing thing else thing in + Disambiguate.disambiguate_thing + ~context ~metasenv ~subst ~use_coercions ~string_context_of_context + ~initial_ugraph ~expty ~mk_implicit ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing - ~localization_tbl (txt,len,thing) + ~mk_localization_tbl (txt,len,thing) in - disambiguate_thing ~passes ~aliases ~universe ~f thing + disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing