1 (* Copyright (C) 2004-2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
30 exception Ambiguous_input
31 exception DisambiguationError of string Lazy.t list list
33 type choose_uris_callback =
34 id:string -> UriManager.uri list -> UriManager.uri list
36 type choose_interp_callback = (string * string) list list -> int list
38 let mono_uris_callback ~id =
39 if Helm_registry.get_bool "matita.auto_disambiguation" then
44 let mono_interp_callback _ = raise Ambiguous_input
46 let _choose_uris_callback = ref mono_uris_callback
47 let _choose_interp_callback = ref mono_interp_callback
48 let set_choose_uris_callback f = _choose_uris_callback := f
49 let set_choose_interp_callback f = _choose_interp_callback := f
53 let interactive_user_uri_choice ~selection_mode ?ok
54 ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
55 !_choose_uris_callback ~id uris
57 let interactive_interpretation_choice interp =
58 !_choose_interp_callback interp
60 let input_or_locate_uri ~(title:string) ?id =
61 (* Zack: I try to avoid using this callback. I therefore assume that
62 * the presence of an identifier that can't be resolved via "locate"
63 * query is a syntax error *)
64 let msg = match id with Some id -> id | _ -> "_" in
65 raise (Unbound_identifier msg)
68 module Disambiguator = Disambiguate.Make (Callbacks)
70 (* implement module's API *)
72 let disambiguate_thing ~aliases ~universe
73 ~(f:?fresh_instances:bool ->
74 aliases:DisambiguateTypes.environment ->
75 universe:DisambiguateTypes.multiple_environment option ->
77 ~(drop_aliases: 'b -> 'b)
78 ~(drop_aliases_and_clear_diff: 'b -> 'b)
81 assert (universe <> None);
82 let library = false, DisambiguateTypes.Environment.empty, None in
83 let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
84 let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
85 let passes = (* <fresh_instances?, aliases, coercions?> *)
86 [ (false, mono_aliases, false);
87 (false, multi_aliases, false);
88 (true, mono_aliases, false);
89 (true, multi_aliases, false);
90 (true, mono_aliases, true);
91 (true, multi_aliases, true);
92 (true, library, true);
95 let try_pass (fresh_instances, (_, aliases, universe), use_coercions) =
96 CoercDb.use_coercions := use_coercions;
97 f ~fresh_instances ~aliases ~universe thing
99 let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
100 if use_mono_aliases && not instances then
102 else if user_asked then
103 drop_aliases res (* one shot aliases *)
105 drop_aliases_and_clear_diff res
111 set_aliases pass (try_pass pass)
112 with Disambiguate.NoWellTypedInterpretation newerrors ->
113 raise (DisambiguationError (errors @ [newerrors])))
116 set_aliases hd (try_pass hd)
117 with Disambiguate.NoWellTypedInterpretation newerrors ->
118 aux (errors @ [newerrors]) tl)
121 let saved_use_coercions = !CoercDb.use_coercions in
123 let res = aux [] passes in
124 CoercDb.use_coercions := saved_use_coercions;
127 CoercDb.use_coercions := saved_use_coercions;
130 type disambiguator_thing =
133 aliases:DisambiguateTypes.environment ->
134 universe:DisambiguateTypes.multiple_environment option ->
135 f:(?fresh_instances:bool ->
136 aliases:DisambiguateTypes.environment ->
137 universe:DisambiguateTypes.multiple_environment option ->
139 drop_aliases:('b * bool -> 'b * bool) ->
140 drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
143 let disambiguate_thing =
144 let profiler = HExtlib.profile "disambiguate_thing" in
146 fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing
147 -> profiler.HExtlib.profile
148 (disambiguate_thing ~aliases ~universe ~f ~drop_aliases
149 ~drop_aliases_and_clear_diff) thing
152 let drop_aliases (choices, user_asked) =
153 (List.map (fun (d, a, b, c) -> d, a, b, c) choices),
156 let drop_aliases_and_clear_diff (choices, user_asked) =
157 (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
160 let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph
161 ~aliases ~universe term
163 assert (fresh_instances = None);
165 Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph
167 disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
168 ~drop_aliases_and_clear_diff term
170 let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj =
171 assert (fresh_instances = None);
172 let f = Disambiguator.disambiguate_obj ~dbd ~uri in
173 disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
174 ~drop_aliases_and_clear_diff obj