From c04f852241510515f06e3bec8eb79acac6e4952e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 4 Dec 2008 13:06:29 +0000 Subject: [PATCH] housekeeping: - unused functions removed from Enviconment - unused file disambiguatePp removed - disambiguation callbacks pushed down to Disambiguate from MultiPassDisambiguator --- .../components/disambiguation/disambiguate.ml | 545 +++++++++--------- .../disambiguation/disambiguate.mli | 102 ++-- .../disambiguation/disambiguateTypes.ml | 26 - .../disambiguation/disambiguateTypes.mli | 33 -- .../disambiguation/multiPassDisambiguator.ml | 35 +- .../disambiguation/multiPassDisambiguator.mli | 19 - helm/software/components/lexicon/.depend | 19 +- helm/software/components/lexicon/.depend.opt | 19 +- helm/software/components/lexicon/Makefile | 1 - .../components/lexicon/disambiguatePp.ml | 47 -- .../components/lexicon/disambiguatePp.mli | 29 - helm/software/matita/matitaGui.ml | 14 +- helm/software/matita/matitaScript.ml | 1 - 13 files changed, 369 insertions(+), 521 deletions(-) delete mode 100644 helm/software/components/lexicon/disambiguatePp.ml delete mode 100644 helm/software/components/lexicon/disambiguatePp.mli diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml index 748722f5d..0b73296e7 100644 --- a/helm/software/components/disambiguation/disambiguate.ml +++ b/helm/software/components/disambiguation/disambiguate.ml @@ -32,6 +32,8 @@ open UriManager module Ast = CicNotationPt +(* the integer is an offset to be added to each location *) +exception Ambiguous_input (* the integer is an offset to be added to each location *) exception NoWellTypedInterpretation of int * @@ -43,12 +45,37 @@ exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) exception Try_again of string Lazy.t -type ('alias,'term) aliases= bool * 'term DisambiguateTypes.environment +type ('alias,'term) aliases = + bool * 'term DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t type 'a disambiguator_input = string * int * 'a type domain = domain_tree list and domain_tree = Node of Stdpp.location list * domain_item * domain +let mono_uris_callback ~selection_mode ?ok + ?(enable_button_for_non_vars = true) ~title ~msg ~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 + +let interactive_user_uri_choice = !_choose_uris_callback +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 *) + + let rec string_of_domain = function [] -> "" @@ -423,58 +450,50 @@ sig list * bool end -module Make (C: Callbacks) = - struct let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" - let disambiguate_thing - ~context ~metasenv ~subst ~use_coercions - ~string_context_of_context - ~initial_ugraph:base_univ ~hint - ~mk_implicit ~description_of_alias - ~aliases ~universe ~lookup_in_library - ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing - ~localization_tbl - (thing_txt,thing_txt_prefix_len,thing) - = - debug_print (lazy "DISAMBIGUATE INPUT"); - debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); - let thing_dom = - domain_of_thing ~context:(string_context_of_context context) thing in - debug_print - (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom))); -(* - debug_print (lazy (sprintf "DISAMBIGUATION ENVIRONMENT: %s" - (DisambiguatePp.pp_environment aliases))); - debug_print (lazy (sprintf "DISAMBIGUATION UNIVERSE: %s" - (match universe with None -> "None" | Some _ -> "Some _"))); -*) - let current_dom = - Environment.fold (fun item _ dom -> item :: dom) aliases [] in - let todo_dom = domain_diff thing_dom current_dom in - debug_print - (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom))); - (* (2) lookup function for any item (Id/Symbol/Num) *) - let lookup_choices = - fun item -> - match universe with - | None -> - lookup_in_library - C.interactive_user_uri_choice - C.input_or_locate_uri item - | Some e -> - (try - let item = - match item with - | Symbol (symb, _) -> Symbol (symb, 0) - | item -> item - in - Environment.find item e - with Not_found -> - lookup_in_library - C.interactive_user_uri_choice - C.input_or_locate_uri item) - in +let disambiguate_thing + ~context ~metasenv ~subst ~use_coercions + ~string_context_of_context + ~initial_ugraph:base_univ ~hint + ~mk_implicit ~description_of_alias + ~aliases ~universe ~lookup_in_library + ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing + ~localization_tbl + (thing_txt,thing_txt_prefix_len,thing) += + debug_print (lazy "DISAMBIGUATE INPUT"); + debug_print (lazy ("TERM IS: " ^ (pp_thing thing))); + let thing_dom = + domain_of_thing ~context:(string_context_of_context context) thing in + debug_print + (lazy (sprintf "DISAMBIGUATION DOMAIN: %s"(string_of_domain thing_dom))); + let current_dom = + Environment.fold (fun item _ dom -> item :: dom) aliases [] in + let todo_dom = domain_diff thing_dom current_dom in + debug_print + (lazy (sprintf "DISAMBIGUATION DOMAIN AFTER DIFF: %s"(string_of_domain todo_dom))); + (* (2) lookup function for any item (Id/Symbol/Num) *) + let lookup_choices = + fun item -> + match universe with + | None -> + lookup_in_library + interactive_user_uri_choice + input_or_locate_uri item + | Some e -> + (try + let item = + match item with + | Symbol (symb, _) -> Symbol (symb, 0) + | item -> item + in + Environment.find item e + with Not_found -> + lookup_in_library + interactive_user_uri_choice + input_or_locate_uri item) + in (* (* *) let _ = @@ -500,223 +519,221 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" (* *) *) - (* (3) test an interpretation filling with meta uninterpreted identifiers - *) - let test_env aliases todo_dom ugraph = - try - let rec aux env = function - | [] -> env - | Node (_, item, l) :: tl -> - let env = - Environment.add item - (mk_implicit - (match item with | Id _ | Num _ -> true | Symbol _ -> false)) - env in - aux (aux env l) tl in - let filled_env = aux aliases todo_dom in - let cic_thing = - interpretate_thing ~context ~env:filled_env - ~uri ~is_path:false thing ~localization_tbl - in - let cic_thing = (fst hint) metasenv cic_thing in + (* (3) test an interpretation filling with meta uninterpreted identifiers + *) + let test_env aliases todo_dom ugraph = + try + let rec aux env = function + | [] -> env + | Node (_, item, l) :: tl -> + let env = + Environment.add item + (mk_implicit + (match item with | Id _ | Num _ -> true | Symbol _ -> false)) + env in + aux (aux env l) tl in + let filled_env = aux aliases todo_dom in + let cic_thing = + interpretate_thing ~context ~env:filled_env + ~uri ~is_path:false thing ~localization_tbl + in + let cic_thing = (fst hint) metasenv cic_thing in let foo () = - let k = - refine_thing metasenv subst context uri - ~use_coercions cic_thing ugraph ~localization_tbl - in - let k = (snd hint) k in - k + let k = + refine_thing metasenv subst context uri + ~use_coercions cic_thing ugraph ~localization_tbl + in + let k = (snd hint) k in + k in refine_profiler.HExtlib.profile foo () - with - | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) - | Invalid_choice loc_msg -> Ko loc_msg - in - (* (4) build all possible interpretations *) - let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in - (* aux returns triples Ok/Uncertain/Ko *) - (* rem_dom is the concatenation of all the remainin domains *) - let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom = - debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom)); - match todo_dom with - | [] -> - assert (lookup_in_todo_dom = None); - (match test_env aliases rem_dom base_univ with - | Ok (thing, metasenv,subst,new_univ) -> - [ aliases, diff, metasenv, subst, thing, new_univ ], [], [] - | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true] - | Uncertain loc_msg -> - [],[aliases,diff,loc_msg],[]) - | Node (locs,item,inner_dom) :: remaining_dom -> - debug_print (lazy (sprintf "CHOOSED ITEM: %s" - (string_of_domain_item item))); - let choices = - match lookup_in_todo_dom with - None -> lookup_choices item - | Some choices -> choices in - match choices with - [] -> - [], [], - [aliases, diff, - (lazy (List.hd locs, - "No choices for " ^ string_of_domain_item item)), - true] + with + | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg)) + | Invalid_choice loc_msg -> Ko loc_msg + in + (* (4) build all possible interpretations *) + let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in + (* aux returns triples Ok/Uncertain/Ko *) + (* rem_dom is the concatenation of all the remainin domains *) + let rec aux aliases diff lookup_in_todo_dom todo_dom rem_dom = + debug_print (lazy ("ZZZ: " ^ string_of_domain todo_dom)); + match todo_dom with + | [] -> + assert (lookup_in_todo_dom = None); + (match test_env aliases rem_dom base_univ with + | Ok (thing, metasenv,subst,new_univ) -> + [ aliases, diff, metasenv, subst, thing, new_univ ], [], [] + | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true] + | Uncertain loc_msg -> + [],[aliases,diff,loc_msg],[]) + | Node (locs,item,inner_dom) :: remaining_dom -> + debug_print (lazy (sprintf "CHOOSED ITEM: %s" + (string_of_domain_item item))); + let choices = + match lookup_in_todo_dom with + None -> lookup_choices item + | Some choices -> choices in + match choices with + [] -> + [], [], + [aliases, diff, + (lazy (List.hd locs, + "No choices for " ^ string_of_domain_item item)), + true] (* - | [codomain_item] -> - (* just one choice. We perform a one-step look-up and - if the next set of choices is also a singleton we - skip this refinement step *) - debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item))); - let new_env = Environment.add item codomain_item aliases in - let new_diff = (item,codomain_item)::diff in - let lookup_in_todo_dom,next_choice_is_single = - match remaining_dom with - [] -> None,false - | (_,he)::_ -> - let choices = lookup_choices he in - Some choices,List.length choices = 1 - in - if next_choice_is_single then - aux new_env new_diff lookup_in_todo_dom remaining_dom - base_univ - else - (match test_env new_env remaining_dom base_univ with - | Ok (thing, metasenv),new_univ -> - (match remaining_dom with - | [] -> - [ new_env, new_diff, metasenv, thing, new_univ ], [] - | _ -> - aux new_env new_diff lookup_in_todo_dom - remaining_dom new_univ) - | Uncertain (loc,msg),new_univ -> - (match remaining_dom with - | [] -> [], [new_env,new_diff,loc,msg,true] - | _ -> - aux new_env new_diff lookup_in_todo_dom - remaining_dom new_univ) - | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true]) + | [codomain_item] -> + (* just one choice. We perform a one-step look-up and + if the next set of choices is also a singleton we + skip this refinement step *) + debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item))); + let new_env = Environment.add item codomain_item aliases in + let new_diff = (item,codomain_item)::diff in + let lookup_in_todo_dom,next_choice_is_single = + match remaining_dom with + [] -> None,false + | (_,he)::_ -> + let choices = lookup_choices he in + Some choices,List.length choices = 1 + in + if next_choice_is_single then + aux new_env new_diff lookup_in_todo_dom remaining_dom + base_univ + else + (match test_env new_env remaining_dom base_univ with + | Ok (thing, metasenv),new_univ -> + (match remaining_dom with + | [] -> + [ new_env, new_diff, metasenv, thing, new_univ ], [] + | _ -> + aux new_env new_diff lookup_in_todo_dom + remaining_dom new_univ) + | Uncertain (loc,msg),new_univ -> + (match remaining_dom with + | [] -> [], [new_env,new_diff,loc,msg,true] + | _ -> + aux new_env new_diff lookup_in_todo_dom + remaining_dom new_univ) + | Ko (loc,msg),_ -> [], [new_env,new_diff,loc,msg,true]) *) - | _::_ -> - let mark_not_significant failures = - List.map - (fun (env, diff, loc_msg, _b) -> - env, diff, loc_msg, false) - failures in - let classify_errors ((ok_l,uncertain_l,error_l) as outcome) = - if ok_l <> [] || uncertain_l <> [] then - ok_l,uncertain_l,mark_not_significant error_l - else - outcome in - let rec filter = function - | [] -> [],[],[] - | codomain_item :: tl -> - (*debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));*) - let new_env = Environment.add item codomain_item aliases in - let new_diff = (item,codomain_item)::diff in - (match - test_env new_env - (inner_dom@remaining_dom@rem_dom) base_univ - with - | Ok (thing, metasenv,subst,new_univ) -> - let res = - (match inner_dom with - | [] -> - [new_env,new_diff,metasenv,subst,thing,new_univ], - [], [] - | _ -> - aux new_env new_diff None inner_dom - (remaining_dom@rem_dom) - ) - in - res @@ filter tl - | Uncertain loc_msg -> - let res = - (match inner_dom with - | [] -> [],[new_env,new_diff,loc_msg],[] - | _ -> - aux new_env new_diff None inner_dom - (remaining_dom@rem_dom) - ) - in - res @@ filter tl - | Ko loc_msg -> - let res = [],[],[new_env,new_diff,loc_msg,true] in - res @@ filter tl) - in - let ok_l,uncertain_l,error_l = - classify_errors (filter choices) - in - let res_after_ok_l = - List.fold_right - (fun (env,diff,_,_,_,_) res -> - aux env diff None remaining_dom rem_dom @@ res - ) ok_l ([],[],error_l) - in - List.fold_right - (fun (env,diff,_) res -> - aux env diff None remaining_dom rem_dom @@ res - ) uncertain_l res_after_ok_l - in - let aux' aliases diff lookup_in_todo_dom todo_dom = - match test_env aliases todo_dom base_univ with - | Ok _ - | Uncertain _ -> - aux aliases diff lookup_in_todo_dom todo_dom [] - | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] - in - let res = - match aux' aliases [] None todo_dom with - | [],uncertain,errors -> - let errors = - List.map - (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true) - ) uncertain @ errors + | _::_ -> + let mark_not_significant failures = + List.map + (fun (env, diff, loc_msg, _b) -> + env, diff, loc_msg, false) + failures in + let classify_errors ((ok_l,uncertain_l,error_l) as outcome) = + if ok_l <> [] || uncertain_l <> [] then + ok_l,uncertain_l,mark_not_significant error_l + else + outcome in + let rec filter = function + | [] -> [],[],[] + | codomain_item :: tl -> + (*debug_print(lazy (sprintf "%s CHOSEN" (fst codomain_item)));*) + let new_env = Environment.add item codomain_item aliases in + let new_diff = (item,codomain_item)::diff in + (match + test_env new_env + (inner_dom@remaining_dom@rem_dom) base_univ + with + | Ok (thing, metasenv,subst,new_univ) -> + let res = + (match inner_dom with + | [] -> + [new_env,new_diff,metasenv,subst,thing,new_univ], + [], [] + | _ -> + aux new_env new_diff None inner_dom + (remaining_dom@rem_dom) + ) + in + res @@ filter tl + | Uncertain loc_msg -> + let res = + (match inner_dom with + | [] -> [],[new_env,new_diff,loc_msg],[] + | _ -> + aux new_env new_diff None inner_dom + (remaining_dom@rem_dom) + ) + in + res @@ filter tl + | Ko loc_msg -> + let res = [],[],[new_env,new_diff,loc_msg,true] in + res @@ filter tl) + in + let ok_l,uncertain_l,error_l = + classify_errors (filter choices) in - let errors = - List.map - (fun (env,diff,loc_msg,significant) -> - let env' = - filter_map_domain - (fun locs domain_item -> - try - let description = - description_of_alias (Environment.find domain_item env) - in - Some (locs,descr_of_domain_item domain_item,description) - with - Not_found -> None) - thing_dom - in - let diff= List.map (fun a,b -> a,description_of_alias b) diff in - env',diff,loc_msg,significant - ) errors + let res_after_ok_l = + List.fold_right + (fun (env,diff,_,_,_,_) res -> + aux env diff None remaining_dom rem_dom @@ res + ) ok_l ([],[],error_l) in - raise (NoWellTypedInterpretation (0,errors)) - | [_,diff,metasenv,subst,t,ugraph],_,_ -> - debug_print (lazy "SINGLE INTERPRETATION"); - [diff,metasenv,subst,t,ugraph], false - | l,_,_ -> - debug_print - (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); - let choices = - List.map - (fun (env, _, _, _, _, _) -> - map_domain - (fun locs domain_item -> - let description = - description_of_alias (Environment.find domain_item env) - in - locs,descr_of_domain_item domain_item, description) - thing_dom) - l - in - let choosed = - C.interactive_interpretation_choice - thing_txt thing_txt_prefix_len choices - in - (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u) - choosed), - true + List.fold_right + (fun (env,diff,_) res -> + aux env diff None remaining_dom rem_dom @@ res + ) uncertain_l res_after_ok_l + in + let aux' aliases diff lookup_in_todo_dom todo_dom = + match test_env aliases todo_dom base_univ with + | Ok _ + | Uncertain _ -> + aux aliases diff lookup_in_todo_dom todo_dom [] + | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] + in + let res = + match aux' aliases [] None todo_dom with + | [],uncertain,errors -> + let errors = + List.map + (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true) + ) uncertain @ errors in - res - - end + let errors = + List.map + (fun (env,diff,loc_msg,significant) -> + let env' = + filter_map_domain + (fun locs domain_item -> + try + let description = + description_of_alias (Environment.find domain_item env) + in + Some (locs,descr_of_domain_item domain_item,description) + with + Not_found -> None) + thing_dom + in + let diff= List.map (fun a,b -> a,description_of_alias b) diff in + env',diff,loc_msg,significant + ) errors + in + raise (NoWellTypedInterpretation (0,errors)) + | [_,diff,metasenv,subst,t,ugraph],_,_ -> + debug_print (lazy "SINGLE INTERPRETATION"); + [diff,metasenv,subst,t,ugraph], false + | l,_,_ -> + debug_print + (lazy (sprintf "MANY INTERPRETATIONS (%d)" (List.length l))); + let choices = + List.map + (fun (env, _, _, _, _, _) -> + map_domain + (fun locs domain_item -> + let description = + description_of_alias (Environment.find domain_item env) + in + locs,descr_of_domain_item domain_item, description) + thing_dom) + l + in + let choosed = + interactive_interpretation_choice + thing_txt thing_txt_prefix_len choices + in + (List.map (fun n->let _,d,m,s,t,u= List.nth l n in d,m,s,t,u) + choosed), + true + in + res diff --git a/helm/software/components/disambiguation/disambiguate.mli b/helm/software/components/disambiguation/disambiguate.mli index 5088f8a5f..cb1882a7d 100644 --- a/helm/software/components/disambiguation/disambiguate.mli +++ b/helm/software/components/disambiguation/disambiguate.mli @@ -25,6 +25,10 @@ (** {2 Disambiguation interface} *) +(** raised when ambiguous input is found but not expected (e.g. in the batch + * compiler) *) +exception Ambiguous_input + (* the integer is an offset to be added to each location *) (* list of located error messages, each list is a tuple: * - environment in string form @@ -54,6 +58,22 @@ type ('term,'metasenv,'subst,'graph) test_result = exception Try_again of string Lazy.t +val set_choose_uris_callback: + DisambiguateTypes.interactive_user_uri_choice_type -> unit + +val set_choose_interp_callback: + DisambiguateTypes.interactive_interpretation_choice_type -> unit + +(** @raise Ambiguous_input if called, default value for internal + * choose_uris_callback if not set otherwise with set_choose_uris_callback + * above *) +val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type + +(** @raise Ambiguous_input if called, default value for internal + * choose_interp_callback if not set otherwise with set_choose_interp_callback + * above *) +val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type + val resolve : env:'alias DisambiguateTypes.Environment.t -> mk_choice:('alias -> 'term DisambiguateTypes.codomain_item) -> @@ -68,49 +88,43 @@ val domain_of_term: context: val domain_of_obj: context:string option list -> CicNotationPt.term CicNotationPt.obj -> domain -module type Disambiguator = -sig - val disambiguate_thing: +val disambiguate_thing: + context:'context -> + metasenv:'metasenv -> + subst:'subst -> + use_coercions:bool -> + string_context_of_context:('context -> string option list) -> + initial_ugraph:'ugraph -> + hint: + ('metasenv -> 'raw_thing -> 'raw_thing) * + (('refined_thing,'metasenv,'subst,'ugraph) test_result -> + ('refined_thing,'metasenv,'subst,'ugraph) test_result) -> + mk_implicit:(bool -> 'alias) -> + description_of_alias:('alias -> string) -> + aliases:'alias DisambiguateTypes.Environment.t -> + universe:'alias list DisambiguateTypes.Environment.t option -> + lookup_in_library:( + DisambiguateTypes.interactive_user_uri_choice_type -> + DisambiguateTypes.input_or_locate_uri_type -> + DisambiguateTypes.Environment.key -> + 'alias list) -> + uri:'uri -> + pp_thing:('ast_thing -> string) -> + domain_of_thing:(context: string option list -> 'ast_thing -> domain) -> + interpretate_thing:( context:'context -> - metasenv:'metasenv -> - subst:'subst -> - use_coercions:bool -> - string_context_of_context:('context -> string option list) -> - initial_ugraph:'ugraph -> - hint: - ('metasenv -> 'raw_thing -> 'raw_thing) * - (('refined_thing,'metasenv,'subst,'ugraph) test_result -> - ('refined_thing,'metasenv,'subst,'ugraph) test_result) -> - mk_implicit:(bool -> 'alias) -> - description_of_alias:('alias -> string) -> - aliases:'alias DisambiguateTypes.Environment.t -> - universe:'alias list DisambiguateTypes.Environment.t option -> - lookup_in_library:( - DisambiguateTypes.interactive_user_uri_choice_type -> - DisambiguateTypes.input_or_locate_uri_type -> - DisambiguateTypes.Environment.key -> - 'alias list) -> + env:'alias DisambiguateTypes.Environment.t -> uri:'uri -> - pp_thing:('ast_thing -> string) -> - domain_of_thing:(context: string option list -> 'ast_thing -> domain) -> - interpretate_thing:( - context:'context -> - env:'alias DisambiguateTypes.Environment.t -> - uri:'uri -> - is_path:bool -> - 'ast_thing -> - localization_tbl:'cichash -> - 'raw_thing) -> - refine_thing:( - 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool -> - 'raw_thing -> 'ugraph -> localization_tbl:'cichash -> - ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> - localization_tbl:'cichash -> - string * int * 'ast_thing -> - ((DisambiguateTypes.Environment.key * 'alias) list * - 'metasenv * 'subst * 'refined_thing * 'ugraph) - list * bool -end - -module Make (C : DisambiguateTypes.Callbacks) : Disambiguator - + is_path:bool -> + 'ast_thing -> + localization_tbl:'cichash -> + 'raw_thing) -> + refine_thing:( + 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool -> + 'raw_thing -> 'ugraph -> localization_tbl:'cichash -> + ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> + localization_tbl:'cichash -> + string * int * 'ast_thing -> + ((DisambiguateTypes.Environment.key * 'alias) list * + 'metasenv * 'subst * 'refined_thing * 'ugraph) + list * bool diff --git a/helm/software/components/disambiguation/disambiguateTypes.ml b/helm/software/components/disambiguation/disambiguateTypes.ml index eb1239523..496c7db35 100644 --- a/helm/software/components/disambiguation/disambiguateTypes.ml +++ b/helm/software/components/disambiguation/disambiguateTypes.ml @@ -62,17 +62,6 @@ struct add k (v :: (List.filter (fun x -> desc_of_alias x <> dsc) current)) env with Not_found -> add k [v] env - - let hd list_env = - try - map List.hd list_env - with Failure _ -> assert false - - let fold_flatten f env base = - fold - (fun k l acc -> List.fold_right (fun v acc -> f k v acc) l acc) - env base - end type 'term codomain_item = @@ -80,11 +69,6 @@ type 'term codomain_item = [`Num_interp of string -> 'term |`Sym_interp of 'term list -> 'term] -and 'term environment = 'term codomain_item Environment.t - -type 'term multiple_environment = - 'term codomain_item list Environment.t - type interactive_user_uri_choice_type = selection_mode:[`SINGLE | `MULTIPLE] -> ?ok:string -> @@ -98,16 +82,6 @@ type interactive_interpretation_choice_type = string -> int -> type input_or_locate_uri_type = title:string -> ?id:string -> unit -> UriManager.uri option -module type Callbacks = - sig - val interactive_user_uri_choice : interactive_user_uri_choice_type - - val interactive_interpretation_choice : - interactive_interpretation_choice_type - - val input_or_locate_uri: input_or_locate_uri_type - end - let string_of_domain_item = function | Id s -> Printf.sprintf "ID(%s)" s | Symbol (s, i) -> Printf.sprintf "SYMBOL(%s,%d)" s i diff --git a/helm/software/components/disambiguation/disambiguateTypes.mli b/helm/software/components/disambiguation/disambiguateTypes.mli index 15f9d8d30..43cfc2316 100644 --- a/helm/software/components/disambiguation/disambiguateTypes.mli +++ b/helm/software/components/disambiguation/disambiguateTypes.mli @@ -33,10 +33,6 @@ module Environment: sig include Map.S with type key = domain_item val cons: ('b -> 'a) -> domain_item -> 'b -> 'b list t -> 'b list t - val hd: 'a list t -> 'a t - - (** last alias cons-ed will be processed first *) - val fold_flatten: (domain_item -> 'a -> 'b -> 'b) -> 'a list t -> 'b -> 'b end (** to be raised when a choice is invalid due to some given parameter (e.g. @@ -48,11 +44,6 @@ type 'term codomain_item = [`Num_interp of string -> 'term |`Sym_interp of 'term list -> 'term] -and 'term environment = 'term codomain_item Environment.t - -type 'term multiple_environment = - 'term codomain_item list Environment.t - type interactive_user_uri_choice_type = selection_mode:[`SINGLE | `MULTIPLE] -> ?ok:string -> @@ -66,29 +57,5 @@ type interactive_interpretation_choice_type = string -> int -> type input_or_locate_uri_type = title:string -> ?id:string -> unit -> UriManager.uri option -module type Callbacks = - sig - - val interactive_user_uri_choice : interactive_user_uri_choice_type - - val interactive_interpretation_choice : - interactive_interpretation_choice_type - - val input_or_locate_uri: input_or_locate_uri_type - end - val string_of_domain_item: domain_item -> string val string_of_domain: domain_item list -> string - -(** {3 type shortands} *) - -(* -type term = CicNotationPt.term -type tactic = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactic -type tactical = (term, term, GrafiteAst.reduction, string) GrafiteAst.tactical - -type script_entry = - | Command of tactical - | Comment of CicNotationPt.location * string -type script = CicNotationPt.location * script_entry list -*) diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml index 039fdd57a..07bbdeba2 100644 --- a/helm/software/components/disambiguation/multiPassDisambiguator.ml +++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml @@ -31,8 +31,6 @@ 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 * @@ -40,37 +38,6 @@ exception DisambiguationError of (Stdpp.location * string) Lazy.t * bool) list list (** parameters are: option name, error message *) -let mono_uris_callback ~selection_mode ?ok - ?(enable_button_for_non_vars = true) ~title ~msg ~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 = !_choose_uris_callback - - 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;; @@ -180,7 +147,7 @@ let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) = let thing = if fresh_instances then freshen_thing thing else thing in - Disambiguator.disambiguate_thing + Disambiguate.disambiguate_thing ~context ~metasenv ~subst ~use_coercions ~string_context_of_context ~initial_ugraph ~hint ~mk_implicit ~description_of_alias ~aliases ~universe ~lookup_in_library diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.mli b/helm/software/components/disambiguation/multiPassDisambiguator.mli index 27d5ca618..777fedafd 100644 --- a/helm/software/components/disambiguation/multiPassDisambiguator.mli +++ b/helm/software/components/disambiguation/multiPassDisambiguator.mli @@ -23,9 +23,6 @@ * http://helm.cs.unibo.it/ *) -(** raised when ambiguous input is found but not expected (e.g. in the batch - * compiler) *) -exception Ambiguous_input (* the integer is an offset to be added to each location *) exception DisambiguationError of int * @@ -39,22 +36,6 @@ val only_one_pass: bool ref val passes : unit -> (bool * [> `Library | `Mono | `Multi ] * bool) list -val set_choose_uris_callback: - DisambiguateTypes.interactive_user_uri_choice_type -> unit - -val set_choose_interp_callback: - DisambiguateTypes.interactive_interpretation_choice_type -> unit - -(** @raise Ambiguous_input if called, default value for internal - * choose_uris_callback if not set otherwise with set_choose_uris_callback - * above *) -val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type - -(** @raise Ambiguous_input if called, default value for internal - * choose_interp_callback if not set otherwise with set_choose_interp_callback - * above *) -val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type - val disambiguate_thing: passes:(bool * [ `Library | `Mono | `Multi ] * bool) list -> freshen_thing: ('ast_thing -> 'ast_thing) -> diff --git a/helm/software/components/lexicon/.depend b/helm/software/components/lexicon/.depend index 452167c72..33e89a7d9 100644 --- a/helm/software/components/lexicon/.depend +++ b/helm/software/components/lexicon/.depend @@ -1,20 +1,19 @@ lexiconAstPp.cmi: lexiconAst.cmo -disambiguatePp.cmi: lexiconAst.cmo lexiconMarshal.cmi: lexiconAst.cmo cicNotation.cmi: lexiconAst.cmo lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmo cicNotation.cmi -lexiconSync.cmi: lexiconEngine.cmi +lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmo lexiconAstPp.cmo: lexiconAst.cmo lexiconAstPp.cmi lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi -disambiguatePp.cmo: lexiconAstPp.cmi lexiconAst.cmo disambiguatePp.cmi -disambiguatePp.cmx: lexiconAstPp.cmx lexiconAst.cmx disambiguatePp.cmi lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmo lexiconMarshal.cmi lexiconMarshal.cmx: lexiconAstPp.cmx lexiconAst.cmx lexiconMarshal.cmi cicNotation.cmo: lexiconAst.cmo cicNotation.cmi cicNotation.cmx: lexiconAst.cmx cicNotation.cmi -lexiconEngine.cmo: lexiconMarshal.cmi lexiconAst.cmo disambiguatePp.cmi \ - cicNotation.cmi lexiconEngine.cmi -lexiconEngine.cmx: lexiconMarshal.cmx lexiconAst.cmx disambiguatePp.cmx \ - cicNotation.cmx lexiconEngine.cmi -lexiconSync.cmo: lexiconEngine.cmi cicNotation.cmi lexiconSync.cmi -lexiconSync.cmx: lexiconEngine.cmx cicNotation.cmx lexiconSync.cmi +lexiconEngine.cmo: lexiconMarshal.cmi lexiconAst.cmo cicNotation.cmi \ + lexiconEngine.cmi +lexiconEngine.cmx: lexiconMarshal.cmx lexiconAst.cmx cicNotation.cmx \ + lexiconEngine.cmi +lexiconSync.cmo: lexiconEngine.cmi lexiconAst.cmo cicNotation.cmi \ + lexiconSync.cmi +lexiconSync.cmx: lexiconEngine.cmx lexiconAst.cmx cicNotation.cmx \ + lexiconSync.cmi diff --git a/helm/software/components/lexicon/.depend.opt b/helm/software/components/lexicon/.depend.opt index 7fec1d3b5..1b4992009 100644 --- a/helm/software/components/lexicon/.depend.opt +++ b/helm/software/components/lexicon/.depend.opt @@ -1,20 +1,19 @@ lexiconAstPp.cmi: lexiconAst.cmx -disambiguatePp.cmi: lexiconAst.cmx lexiconMarshal.cmi: lexiconAst.cmx cicNotation.cmi: lexiconAst.cmx lexiconEngine.cmi: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi -lexiconSync.cmi: lexiconEngine.cmi +lexiconSync.cmi: lexiconEngine.cmi lexiconAst.cmx lexiconAstPp.cmo: lexiconAst.cmx lexiconAstPp.cmi lexiconAstPp.cmx: lexiconAst.cmx lexiconAstPp.cmi -disambiguatePp.cmo: lexiconAstPp.cmi lexiconAst.cmx disambiguatePp.cmi -disambiguatePp.cmx: lexiconAstPp.cmx lexiconAst.cmx disambiguatePp.cmi lexiconMarshal.cmo: lexiconAstPp.cmi lexiconAst.cmx lexiconMarshal.cmi lexiconMarshal.cmx: lexiconAstPp.cmx lexiconAst.cmx lexiconMarshal.cmi cicNotation.cmo: lexiconAst.cmx cicNotation.cmi cicNotation.cmx: lexiconAst.cmx cicNotation.cmi -lexiconEngine.cmo: lexiconMarshal.cmi lexiconAst.cmx disambiguatePp.cmi \ - cicNotation.cmi lexiconEngine.cmi -lexiconEngine.cmx: lexiconMarshal.cmx lexiconAst.cmx disambiguatePp.cmx \ - cicNotation.cmx lexiconEngine.cmi -lexiconSync.cmo: lexiconEngine.cmi cicNotation.cmi lexiconSync.cmi -lexiconSync.cmx: lexiconEngine.cmx cicNotation.cmx lexiconSync.cmi +lexiconEngine.cmo: lexiconMarshal.cmi lexiconAst.cmx cicNotation.cmi \ + lexiconEngine.cmi +lexiconEngine.cmx: lexiconMarshal.cmx lexiconAst.cmx cicNotation.cmx \ + lexiconEngine.cmi +lexiconSync.cmo: lexiconEngine.cmi lexiconAst.cmx cicNotation.cmi \ + lexiconSync.cmi +lexiconSync.cmx: lexiconEngine.cmx lexiconAst.cmx cicNotation.cmx \ + lexiconSync.cmi diff --git a/helm/software/components/lexicon/Makefile b/helm/software/components/lexicon/Makefile index b8582baca..d5b16e924 100644 --- a/helm/software/components/lexicon/Makefile +++ b/helm/software/components/lexicon/Makefile @@ -3,7 +3,6 @@ PREDICATES = INTERFACE_FILES = \ lexiconAstPp.mli \ - disambiguatePp.mli \ lexiconMarshal.mli \ cicNotation.mli \ lexiconEngine.mli \ diff --git a/helm/software/components/lexicon/disambiguatePp.ml b/helm/software/components/lexicon/disambiguatePp.ml deleted file mode 100644 index a8590cfdf..000000000 --- a/helm/software/components/lexicon/disambiguatePp.ml +++ /dev/null @@ -1,47 +0,0 @@ -(* Copyright (C) 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 DisambiguateTypes - -let alias_of_domain_and_desc domain_item dsc = - match domain_item with - Id id -> LexiconAst.Ident_alias (id, dsc) - | Symbol (symb, i) -> LexiconAst.Symbol_alias (symb, i, dsc) - | Num i -> LexiconAst.Number_alias (i, dsc) - -let aliases_of_environment env = - Environment.fold - (fun domain_item codomain_item acc -> - alias_of_domain_and_desc domain_item (fst codomain_item)::acc - ) env [] - -let pp_environment env = - let aliases = aliases_of_environment env in - let strings = - List.map (fun alias -> LexiconAstPp.pp_alias alias ^ ".") aliases - in - String.concat "\n" (List.sort compare strings) diff --git a/helm/software/components/lexicon/disambiguatePp.mli b/helm/software/components/lexicon/disambiguatePp.mli deleted file mode 100644 index c41bf6d78..000000000 --- a/helm/software/components/lexicon/disambiguatePp.mli +++ /dev/null @@ -1,29 +0,0 @@ -(* Copyright (C) 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/ - *) - -val alias_of_domain_and_desc: - DisambiguateTypes.domain_item -> string -> LexiconAst.alias_spec - -val pp_environment: Cic.term DisambiguateTypes.environment -> string diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 5200a21ba..f68421e0c 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -328,7 +328,15 @@ let rec interactive_error_interp ~all_passes ("" :: List.map (fun k,desc -> - let alias = DisambiguatePp.alias_of_domain_and_desc k desc in + let alias = + match k with + | DisambiguateTypes.Id id -> + LexiconAst.Ident_alias (id, desc) + | DisambiguateTypes.Symbol (symb, i)-> + LexiconAst.Symbol_alias (symb, i, desc) + | DisambiguateTypes.Num i -> + LexiconAst.Number_alias (i, desc) + in LexiconAstPp.pp_alias alias) diff) ^ "\n" in @@ -1567,10 +1575,10 @@ let interactive_interp_choice () text prefix_len choices = let _ = (* disambiguator callbacks *) - MultiPassDisambiguator.set_choose_uris_callback + Disambiguate.set_choose_uris_callback (fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg -> interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ()); - MultiPassDisambiguator.set_choose_interp_callback (interactive_interp_choice ()); + Disambiguate.set_choose_interp_callback (interactive_interp_choice ()); (* gtk initialization *) GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf; diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index fe82e939c..a5e24d315 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -76,7 +76,6 @@ let eval_with_engine include_paths guistuff lexicon_status grafite_status user_g = let module TAPp = GrafiteAstPp in let module DTE = DisambiguateTypes.Environment in - let module DP = DisambiguatePp in let parsed_text_length = String.length skipped_txt + String.length nonskipped_txt in -- 2.39.2