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/
32 if debug then prerr_endline (Lazy.force s);;
34 exception DisambiguationError of
36 ((Stdpp.location list * string * string) list *
37 (DisambiguateTypes.domain_item * string) list *
38 (Stdpp.location * string) Lazy.t * bool) list list
39 (** parameters are: option name, error message *)
41 (* implement module's API *)
43 let only_one_pass = ref false;;
45 let passes () = (* <fresh_instances?, aliases, coercions?> *)
46 if !only_one_pass then
47 [ (true, `Mono, false) ]
49 [ (true, `Mono, false);
50 (true, `Multi, false);
53 (true, `Library, false);
54 (* for demo to reduce the number of interpretations *)
55 (true, `Library, true);
59 let drop_aliases ?(minimize_instances=false) ~description_of_alias
62 let module D = DisambiguateTypes in
63 let compare ci1 ci2 = description_of_alias ci1 = description_of_alias ci2 in
65 if not minimize_instances then
71 | (D.Symbol (s,n),ci1) as he::tl when n > 0 ->
75 (D.Symbol (s2,_),ci2) -> s2 <> s || compare ci1 ci2
79 (D.Symbol (s,0),ci1)::(aux tl)
82 | (D.Num n,ci1) as he::tl when n > 0 ->
85 (function (D.Num _,ci2) -> compare ci1 ci2 | _ -> true) d
87 (D.Num 0,ci1)::(aux tl)
90 | he::tl -> he::(aux tl)
94 (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices),
97 let drop_aliases_and_clear_diff (choices, user_asked) =
98 (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
101 let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
103 assert (universe <> None);
104 let library = false, DisambiguateTypes.Environment.empty, None in
105 let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
106 let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
109 (function (fresh_instances,env,use_coercions) ->
111 (match env with `Mono -> mono_aliases | `Multi -> multi_aliases |
112 `Library -> library),
113 use_coercions) passes in
114 let try_pass (fresh_instances, (_, aliases, universe), use_coercions) =
115 f ~fresh_instances ~aliases ~universe ~use_coercions thing
117 let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) =
118 if use_mono_aliases then
119 drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *)
120 else if user_asked then
121 drop_aliases ~minimize_instances:true ~description_of_alias res (* one shot aliases *)
123 drop_aliases_and_clear_diff res
125 let rec aux i errors passes =
126 debug_print (lazy ("Pass: " ^ string_of_int i));
130 set_aliases pass (try_pass pass)
131 with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
132 raise (DisambiguationError (offset, errors @ [newerrors])))
135 set_aliases hd (try_pass hd)
136 with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
137 aux (i+1) (errors @ [newerrors]) tl)
142 let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
143 ~string_context_of_context ~initial_ugraph ~hint ~mk_implicit
144 ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing
145 ~domain_of_thing ~interpretate_thing ~refine_thing ~mk_localization_tbl thing
147 let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) =
148 let thing = if fresh_instances then freshen_thing thing else thing in
149 Disambiguate.disambiguate_thing
150 ~context ~metasenv ~subst ~use_coercions ~string_context_of_context
151 ~initial_ugraph ~hint ~mk_implicit ~description_of_alias
152 ~aliases ~universe ~lookup_in_library
153 ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
154 ~mk_localization_tbl (txt,len,thing)
156 disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing