X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteDisambiguator.ml;fp=components%2Fgrafite_parser%2FgrafiteDisambiguator.ml;h=8827e709b42328072edcb01591e9422ef73ba9e1;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/grafite_parser/grafiteDisambiguator.ml b/components/grafite_parser/grafiteDisambiguator.ml new file mode 100644 index 000000000..8827e709b --- /dev/null +++ b/components/grafite_parser/grafiteDisambiguator.ml @@ -0,0 +1,224 @@ +(* Copyright (C) 2004-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 Printf + +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 * + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * + Stdpp.location option * string Lazy.t * bool) list list + (** parameters are: option name, error message *) +exception Unbound_identifier of string + +type choose_uris_callback = + id:string -> UriManager.uri list -> UriManager.uri list + +type choose_interp_callback = + string -> int -> + (Stdpp.location list * string * string) list list -> int list + +let mono_uris_callback ~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 ~selection_mode ?ok + ?(enable_button_for_non_vars = true) ~title ~msg ~id uris = + !_choose_uris_callback ~id uris + + 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 disambiguate_thing ~aliases ~universe + ~(f:?fresh_instances:bool -> + aliases:DisambiguateTypes.environment -> + universe:DisambiguateTypes.multiple_environment option -> + 'a -> 'b) + ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b) + ~(drop_aliases_and_clear_diff: 'b -> 'b) + (thing: 'a) += + assert (universe <> None); + let library = false, DisambiguateTypes.Environment.empty, None in + let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in + let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in + let passes = (* *) + if !only_one_pass then + [ (true, mono_aliases, false) ] + else + [ (true, mono_aliases, false); + (true, multi_aliases, false); + (true, mono_aliases, true); + (true, multi_aliases, true); + (true, library, false); + (* for demo to reduce the number of interpretations *) + (true, library, true); + ] + in + let try_pass (fresh_instances, (_, aliases, universe), insert_coercions) = + CicRefine.insert_coercions := insert_coercions; + f ~fresh_instances ~aliases ~universe 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 *) + else if user_asked then + drop_aliases ~minimize_instances:true res (* one shot aliases *) + else + drop_aliases_and_clear_diff res + in + let rec aux i errors passes = + debug_print (lazy ("Pass: " ^ string_of_int i)); + match passes with + [ pass ] -> + (try + set_aliases pass (try_pass pass) + with Disambiguate.NoWellTypedInterpretation (offset,newerrors) -> + raise (DisambiguationError (offset, errors @ [newerrors]))) + | hd :: tl -> + (try + set_aliases hd (try_pass hd) + with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) -> + aux (i+1) (errors @ [newerrors]) tl) + | [] -> assert false + in + let saved_insert_coercions = !CicRefine.insert_coercions in + try + let res = aux 1 [] passes in + CicRefine.insert_coercions := saved_insert_coercions; + res + with exn -> + CicRefine.insert_coercions := saved_insert_coercions; + raise exn + +type disambiguator_thing = + { do_it : + 'a 'b. + aliases:DisambiguateTypes.environment -> + universe:DisambiguateTypes.multiple_environment option -> + f:(?fresh_instances:bool -> + aliases:DisambiguateTypes.environment -> + universe:DisambiguateTypes.multiple_environment option -> + 'a -> 'b * bool) -> + drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) -> + drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool + } + +let disambiguate_thing = + let profiler = HExtlib.profile "disambiguate_thing" in + { do_it = + fun ~aliases ~universe ~f ~drop_aliases ~drop_aliases_and_clear_diff thing + -> profiler.HExtlib.profile + (disambiguate_thing ~aliases ~universe ~f ~drop_aliases + ~drop_aliases_and_clear_diff) thing + } + +let drop_aliases ?(minimize_instances=false) (choices, user_asked) = + let module D = DisambiguateTypes in + let minimize d = + if not minimize_instances then + d + else + let rec aux = + function + [] -> [] + | (D.Symbol (s,n),((descr,_) as ci)) as he::tl when n > 0 -> + if + List.for_all + (function + (D.Symbol (s2,_),(descr2,_)) -> s2 <> s || descr = descr2 + | _ -> true + ) d + then + (D.Symbol (s,0),ci)::(aux tl) + else + he::(aux tl) + | (D.Num n,((descr,_) as ci)) as he::tl when n > 0 -> + if + List.for_all + (function (D.Num _,(descr2,_)) -> descr = descr2 | _ -> true) d + then + (D.Num 0,ci)::(aux tl) + else + he::(aux tl) + | he::tl -> he::(aux tl) + in + aux d + in + (List.map (fun (d, a, b, c) -> minimize d, a, b, c) choices), + user_asked + +let drop_aliases_and_clear_diff (choices, user_asked) = + (List.map (fun (_, a, b, c) -> [], a, b, c) choices), + user_asked + +let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ?initial_ugraph + ~aliases ~universe term + = + assert (fresh_instances = None); + let f = + Disambiguator.disambiguate_term ~dbd ~context ~metasenv ?initial_ugraph + in + disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases + ~drop_aliases_and_clear_diff term + +let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj = + assert (fresh_instances = None); + let f = Disambiguator.disambiguate_obj ~dbd ~uri in + disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases + ~drop_aliases_and_clear_diff obj