2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 exception Ambiguous_input
15 exception DisambiguationError of
17 ((Stdpp.location list * string * string) list *
18 (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
19 (Stdpp.location * string) Lazy.t * bool) list list
20 (** parameters are: option name, error message *)
21 type choose_uris_callback = id:string -> NUri.uri list -> NUri.uri list
22 type choose_interp_callback =
23 string -> int -> (Stdpp.location list * string * string) list list ->
30 if debug then prerr_endline (Lazy.force s);;
32 let mono_uris_callback ~id =
33 if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
34 "matita.auto_disambiguation"
36 else raise Ambiguous_input
38 let mono_interp_callback _ _ _ = raise Ambiguous_input
40 let _choose_uris_callback = ref mono_uris_callback
41 let _choose_interp_callback = ref mono_interp_callback
42 let set_choose_uris_callback f = _choose_uris_callback := f
43 let set_choose_interp_callback f = _choose_interp_callback := f
47 let interactive_user_uri_choice ~selection_mode ?ok
48 ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
49 !_choose_uris_callback ~id uris
51 let interactive_interpretation_choice interp =
52 !_choose_interp_callback interp
54 let input_or_locate_uri ~(title:string) ?id () = None
55 (* Zack: I try to avoid using this callback. I therefore assume that
56 * the presence of an identifier that can't be resolved via "locate"
57 * query is a syntax error *)
60 module Disambiguator = NDisambiguate.Make (Callbacks)
62 let only_one_pass = ref false;;
64 let disambiguate_thing ~aliases ~universe
65 ~(f:?fresh_instances:bool ->
66 aliases:DisambiguateTypes.environment ->
67 universe:DisambiguateTypes.multiple_environment option ->
69 ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b)
70 ~(drop_aliases_and_clear_diff: 'b -> 'b)
73 assert (universe <> None);
74 let library = false, DisambiguateTypes.Environment.empty, None in
75 let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
76 let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
77 let passes = (* <fresh_instances?, aliases, coercions?> *)
78 if !only_one_pass then
79 [ (true, mono_aliases, false) ]
81 [ (true, mono_aliases, false);
82 (true, multi_aliases, false);
83 (true, mono_aliases, true);
84 (true, multi_aliases, true);
85 (true, library, false);
86 (* for demo to reduce the number of interpretations *)
87 (true, library, true);
90 let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) =
91 CicRefine.insert_coercions := insert_coercions;
92 f ~fresh_instances ~aliases ~universe thing
94 let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
95 if use_mono_aliases then
96 drop_aliases ~minimize_instances:true res (* one shot aliases *)
97 else if user_asked then
98 drop_aliases ~minimize_instances:true res (* one shot aliases *)
100 drop_aliases_and_clear_diff res
102 let rec aux i errors passes =
103 debug_print (lazy ("Pass: " ^ string_of_int i));
107 set_aliases pass (try_pass pass)
108 with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
109 raise (DisambiguationError (offset, errors @ [newerrors])))
112 set_aliases hd (try_pass hd)
113 with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
114 aux (i+1) (errors @ [newerrors]) tl)
117 let saved_insert_coercions = !CicRefine.insert_coercions in
119 let res = aux 1 [] passes in
120 CicRefine.insert_coercions := saved_insert_coercions;
123 CicRefine.insert_coercions := saved_insert_coercions;
126 type disambiguator_thing =
129 aliases:DisambiguateTypes.environment ->
130 universe:DisambiguateTypes.multiple_environment option ->
131 f:(?fresh_instances:bool ->
132 aliases:DisambiguateTypes.environment ->
133 universe:DisambiguateTypes.multiple_environment option ->
135 drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) ->
136 drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
139 let disambiguate_thing =
140 let profiler = HExtlib.profile "disambiguate_thing" in
142 fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
143 -> profiler.HExtlib.profile
144 (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
145 ~drop_aliases_and_clear_diff) thing
148 let drop_aliases ?(minimize_instances=false) (choices, user_asked) =
149 let module D = DisambiguateTypes in
151 if not minimize_instances then
157 | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 ->
161 (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2
165 (D.Symbol (s,0),ci)::(aux tl)
168 | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 ->
171 (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d
173 (D.Num 0,ci)::(aux tl)
176 | he::tl -> he::(aux tl)
180 (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices),
183 let drop_aliases_and_clear_diff (choices, user_asked) =
184 (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
187 let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph
188 ~aliases ~universe term
190 assert (fresh_instances = None);
192 Disambiguator.disambiguate_term ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph
194 disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
195 ~drop_aliases_and_clear_diff term
197 let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj =
198 assert (fresh_instances = None);
199 let f = Disambiguator.disambiguate_obj ~dbd ~uri in
200 disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
201 ~drop_aliases_and_clear_diff obj
203 let disambiguate_thing ~dbd = assert false