X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguator.ml;h=4f812ff2f032abae8448782165da6bdc544d5bea;hb=55ec3926f6fbb5dba13705659fe94d0db38b2666;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..4f812ff2f 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml @@ -30,14 +30,19 @@ open Printf 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 * + ((Token.flocation list * string * string) list * + (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * + Token.flocation 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 -> + (Token.flocation 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 +52,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 +68,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 +93,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 +111,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 = +(*prerr_endline ("Pass: " ^ string_of_int i);*) + match passes with + [ pass ] -> (try set_aliases pass (try_pass pass) with Disambiguate.NoWellTypedInterpretation (offset,newerrors) -> @@ -121,12 +130,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 +151,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 +164,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) =