X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=ca6146e5614011db63632dbea398e7a9bca109a4;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=12b7b01a9a126c14fec188c03d9b02897e84b78f;hpb=3323758b99384afb5c7a70aa31bc006a78af64dd;p=helm.git diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml index 12b7b01a9..ca6146e56 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 '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 [] -> "" @@ -108,9 +135,13 @@ type ('term,'metasenv,'subst,'graph) test_result = | Ko of (Stdpp.location * string) Lazy.t | Uncertain of (Stdpp.location * string) Lazy.t -let resolve (env: 'term codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = +let resolve ~env ~mk_choice (item: domain_item) arg = try - snd (Environment.find item env) env num args + match snd (mk_choice (Environment.find item env)), arg with + `Num_interp f, `Num_arg n -> f n + | `Sym_interp f, `Args l -> f l + | `Sym_interp f, `Num_arg n -> (* Implicit number! *) f [] + | _,_ -> assert false with Not_found -> failwith ("Domain item not found: " ^ (DisambiguateTypes.string_of_domain_item item)) @@ -279,6 +310,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function [] subst in [ Node ([loc], Id name, terms) ])) | Ast.Uri _ -> [] + | Ast.NRef _ -> [] | Ast.Implicit -> [] | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ] | Ast.Meta (index, local_context) -> @@ -327,7 +359,7 @@ let domain_of_obj ~context ast = List.map (fun (_,ty) -> domain_of_term context_w_types ty) cl)) tyl) - | CicNotationPt.Record (params,var,ty,fields) -> + | Ast.Record (params,var,ty,fields) -> let context, dom = List.fold_left (fun (context, dom) (var, ty) -> @@ -348,8 +380,6 @@ let domain_of_obj ~context ast = let domain_of_obj ~context obj = uniq_domain (domain_of_obj ~context obj) -let domain_of_ast_term = domain_of_term;; - (* dom1 \ dom2 *) let domain_diff dom1 dom2 = (* let domain_diff = Domain.diff *) @@ -375,107 +405,47 @@ let domain_diff dom1 dom2 = in aux dom1 -module type Disambiguator = -sig - val disambiguate_thing: - context:'context -> - metasenv:'metasenv -> - subst:'subst -> - use_coercions:bool -> - mk_implicit:(bool -> 'refined_term) -> - 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) -> - aliases:'refined_term DisambiguateTypes.codomain_item - DisambiguateTypes.Environment.t -> - universe:'refined_term DisambiguateTypes.codomain_item list - DisambiguateTypes.Environment.t option -> - lookup_in_library:( - DisambiguateTypes.interactive_user_uri_choice_type -> - DisambiguateTypes.input_or_locate_uri_type -> - DisambiguateTypes.Environment.key -> - 'refined_term DisambiguateTypes.codomain_item list) -> - uri:'uri -> - pp_thing:('ast_thing -> string) -> - domain_of_thing:(context: string option list -> 'ast_thing -> domain) -> - interpretate_thing:( - context:'context -> - env:'refined_term DisambiguateTypes.codomain_item - 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 * - 'refined_term DisambiguateTypes.codomain_item) list * - 'metasenv * 'subst * 'refined_thing * 'ugraph) - 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 - ~mk_implicit ~string_context_of_context - ~initial_ugraph:base_univ ~hint - ~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 -> - let choices = - 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 - choices - in +let disambiguate_thing + ~context ~metasenv ~subst ~use_coercions + ~string_context_of_context + ~initial_ugraph:base_univ ~expty + ~mk_implicit ~description_of_alias + ~aliases ~universe ~lookup_in_library + ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing + ~mk_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 -> []) + in (* (* *) let _ = @@ -501,225 +471,223 @@ 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 = - let rec aux env = function - | [] -> env - | Node (_, item, l) :: tl -> - let env = - Environment.add item - ("Implicit", - (match item with - | Id _ | Num _ -> - (fun _ _ _ -> mk_implicit true) - | Symbol _ -> (fun _ _ _ -> mk_implicit false))) - env in - aux (aux env l) tl in - let filled_env = aux aliases todo_dom in - try - 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 localization_tbl = mk_localization_tbl 503 in + let cic_thing = + interpretate_thing ~context ~env:filled_env + ~uri ~is_path:false thing ~localization_tbl + 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 + refine_thing metasenv subst context uri + ~use_coercions cic_thing expty ugraph ~localization_tbl 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) -> +(* prerr_endline "OK"; *) + 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 -> +(* prerr_endline ("UNCERTAIN"); *) + 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 -> +(* prerr_endline "KO"; *) + 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 = - fst (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,fst 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 = - fst (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 = + if todo_dom = [] then + aux aliases diff lookup_in_todo_dom todo_dom [] + else + 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