X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguator.ml;fp=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguator.ml;h=0000000000000000000000000000000000000000;hb=13bfd154ade0996d34e7e723398ac7ab76a51717;hp=4b647c780541b6ff54fa72d5d5cf4e2520e32a7d;hpb=a8b95f91af568cfe587b3f05b9c111c6ebe8b0a8;p=helm.git diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml deleted file mode 100644 index 4b647c780..000000000 --- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml +++ /dev/null @@ -1,225 +0,0 @@ -(* 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 * string) list * - (Stdpp.location * 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:'term DisambiguateTypes.environment -> - universe:'term 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 'term. - aliases:'term DisambiguateTypes.environment -> - universe:'term DisambiguateTypes.multiple_environment option -> - f:(?fresh_instances:bool -> - aliases:'term DisambiguateTypes.environment -> - universe:'term 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, e) -> minimize d, a, b, c, e) choices), - user_asked - -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_term ?fresh_instances ~context ~metasenv ~subst ?goal ?initial_ugraph ~aliases ~universe ~lookup_in_library term - = - assert (fresh_instances = None); - let f = - Disambiguator.disambiguate_term ~lookup_in_library ~context ~metasenv ~subst ?goal ?initial_ugraph - in - disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases - ~drop_aliases_and_clear_diff term - -let disambiguate_obj ?fresh_instances ~aliases ~universe ~uri ~lookup_in_library obj = - assert (fresh_instances = None); - let f = Disambiguator.disambiguate_obj ~lookup_in_library ~uri in - disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases - ~drop_aliases_and_clear_diff obj - -let disambiguate_thing ~context = assert false