X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguator.ml;h=8827e709b42328072edcb01591e9422ef73ba9e1;hb=a677e0d09755766c61ce9b30a98bec10cb8902b3;hp=abe8c1de1f75373c33fbfdf018eaaf3984d4c785;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml index abe8c1de1..8827e709b 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml @@ -27,17 +27,26 @@ 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 * (Token.flocation option * string Lazy.t) list list + 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 * string) list list -> int 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 @@ -47,7 +56,7 @@ let mono_uris_callback ~id = else raise Ambiguous_input -let mono_interp_callback _ = 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 @@ -63,24 +72,24 @@ module Callbacks = let interactive_interpretation_choice interp = !_choose_interp_callback interp - let input_or_locate_uri ~(title:string) ?id = + 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 *) - let msg = match id with Some id -> id | _ -> "_" in - raise (Unbound_identifier msg) 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: 'b -> 'b) + ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b) ~(drop_aliases_and_clear_diff: 'b -> 'b) (thing: 'a) = @@ -88,13 +97,16 @@ let disambiguate_thing ~aliases ~universe 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 = (* *) - [ (false, mono_aliases, false); - (false, multi_aliases, false); - (true, mono_aliases, false); + 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 @@ -103,16 +115,17 @@ let disambiguate_thing ~aliases ~universe f ~fresh_instances ~aliases ~universe thing in let set_aliases (instances,(use_mono_aliases,_,_),_) (_, user_asked as res) = - if use_mono_aliases && not instances then - drop_aliases res + if use_mono_aliases then + drop_aliases ~minimize_instances:true res (* one shot aliases *) else if user_asked then - drop_aliases res (* one shot aliases *) + drop_aliases ~minimize_instances:true res (* one shot aliases *) else drop_aliases_and_clear_diff res in - let rec aux errors = - function - | [ pass ] -> + 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) -> @@ -121,12 +134,12 @@ let disambiguate_thing ~aliases ~universe (try set_aliases hd (try_pass hd) with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) -> - aux (errors @ [newerrors]) tl) + aux (i+1) (errors @ [newerrors]) tl) | [] -> assert false in let saved_insert_coercions = !CicRefine.insert_coercions in try - let res = aux [] passes in + let res = aux 1 [] passes in CicRefine.insert_coercions := saved_insert_coercions; res with exn -> @@ -142,7 +155,7 @@ type disambiguator_thing = aliases:DisambiguateTypes.environment -> universe:DisambiguateTypes.multiple_environment option -> 'a -> 'b * bool) -> - drop_aliases:('b * bool -> 'b * bool) -> + drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) -> drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool } @@ -155,8 +168,39 @@ let disambiguate_thing = ~drop_aliases_and_clear_diff) thing } -let drop_aliases (choices, user_asked) = - (List.map (fun (d, a, b, c) -> d, a, b, c) choices), +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) =