X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=655747365a5ff834218ec2a1fc68a86362f7d8cb;hb=1d212933a86f2820a151555516f7a53ab1c9f8e7;hp=47e9c182189efb83e9b8be3518ed448dff80553f;hpb=92c4af96b3c1e4918bdc10b7cbdb3a37038de074;p=helm.git diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 47e9c1821..655747365 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -36,14 +36,14 @@ module Ast = CicNotationPt exception NoWellTypedInterpretation of int * ((Stdpp.location list * string * string) list * - (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * + (DisambiguateTypes.domain_item * string) list * (Stdpp.location * string) Lazy.t * bool) list exception PathNotWellFormed (** raised when an environment is not enough informative to decide *) exception Try_again of string Lazy.t -type aliases = bool * DisambiguateTypes.environment +type 'term aliases = bool * 'term DisambiguateTypes.environment type 'a disambiguator_input = string * int * 'a type domain = domain_tree list @@ -159,7 +159,7 @@ let refine_obj metasenv subst context uri obj ugraph ~localization_tbl = in process_exn Stdpp.dummy_loc exn -let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = +let resolve (env: 'term codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = try snd (Environment.find item env) env num args with Not_found -> @@ -932,22 +932,32 @@ let domain_diff dom1 dom2 = module type Disambiguator = sig val disambiguate_thing: - dbd:HSql.dbd -> context:'context -> metasenv:'metasenv -> subst:'subst -> + mk_implicit:([ `Closed ] option -> 'refined_thing) -> initial_ugraph:'ugraph -> hint: ('metasenv -> 'raw_thing -> 'raw_thing) * (('refined_thing,'metasenv,'subst,'ugraph) test_result -> ('refined_thing,'metasenv,'subst,'ugraph) test_result) -> - aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t -> - universe:DisambiguateTypes.codomain_item list + aliases:'refined_thing DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t -> + universe:'refined_thing DisambiguateTypes.codomain_item list DisambiguateTypes.Environment.t option -> + lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] -> + ?ok:string -> + ?enable_button_for_non_vars:bool -> + title:string -> + msg:string -> + id:string -> + UriManager.uri list -> UriManager.uri list) -> + (title:string -> ?id:string -> unit -> UriManager.uri option) -> + DisambiguateTypes.Environment.key -> + 'refined_thing DisambiguateTypes.codomain_item list) -> uri:'uri -> pp_thing:('ast_thing -> string) -> domain_of_thing:(context:'context -> 'ast_thing -> domain) -> interpretate_thing:(context:'context -> - env:DisambiguateTypes.codomain_item + env:'refined_thing DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t -> uri:'uri -> is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) -> @@ -960,22 +970,32 @@ sig ('refined_thing, 'metasenv,'subst,'ugraph) test_result) -> localization_tbl:'cichash -> string * int * 'ast_thing -> - ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item) - list * 'metasenv * 'subst * 'refined_thing * 'ugraph) - list * bool + ((DisambiguateTypes.Environment.key * + 'refined_thing DisambiguateTypes.codomain_item) list * + 'metasenv * 'subst * 'refined_thing * 'ugraph) + list * bool val disambiguate_term : ?fresh_instances:bool -> - dbd:HSql.dbd -> context:Cic.context -> metasenv:Cic.metasenv -> subst:Cic.substitution -> ?goal:int -> ?initial_ugraph:CicUniv.universe_graph -> - aliases:DisambiguateTypes.environment ->(* previous interpretation status *) - universe:DisambiguateTypes.multiple_environment option -> + aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *) + universe:Cic.term DisambiguateTypes.multiple_environment option -> + lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] -> + ?ok:string -> + ?enable_button_for_non_vars:bool -> + title:string -> + msg:string -> + id:string -> + UriManager.uri list -> UriManager.uri list) -> + (title:string -> ?id:string -> unit -> UriManager.uri option) -> + DisambiguateTypes.Environment.key -> + Cic.term DisambiguateTypes.codomain_item list) -> CicNotationPt.term disambiguator_input -> - ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * + ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.substitution * Cic.term* @@ -984,12 +1004,21 @@ sig val disambiguate_obj : ?fresh_instances:bool -> - dbd:HSql.dbd -> - aliases:DisambiguateTypes.environment ->(* previous interpretation status *) - universe:DisambiguateTypes.multiple_environment option -> + aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *) + universe:Cic.term DisambiguateTypes.multiple_environment option -> uri:UriManager.uri option -> (* required only for inductive types *) + lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] -> + ?ok:string -> + ?enable_button_for_non_vars:bool -> + title:string -> + msg:string -> + id:string -> + UriManager.uri list -> UriManager.uri list) -> + (title:string -> ?id:string -> unit -> UriManager.uri option) -> + DisambiguateTypes.Environment.key -> + Cic.term DisambiguateTypes.codomain_item list) -> CicNotationPt.term CicNotationPt.obj disambiguator_input -> - ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * + ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list * Cic.metasenv * (* new metasenv *) Cic.substitution * Cic.obj * @@ -999,45 +1028,12 @@ end module Make (C: Callbacks) = struct - let choices_of_id dbd id = - let uris = Whelp.locate ~dbd id in - let uris = - match uris with - | [] -> - (match - (C.input_or_locate_uri - ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ()) - with - | None -> [] - | Some uri -> [uri]) - | [uri] -> [uri] - | _ -> - C.interactive_user_uri_choice ~selection_mode:`MULTIPLE - ~ok:"Try selected." ~enable_button_for_non_vars:true - ~title:"Ambiguous input." ~id - ~msg: ("Ambiguous input \"" ^ id ^ - "\". Please, choose one or more interpretations:") - uris - in - List.map - (fun uri -> - (UriManager.string_of_uri uri, - let term = - try - CicUtil.term_of_uri uri - with exn -> - debug_print (lazy (UriManager.string_of_uri uri)); - debug_print (lazy (Printexc.to_string exn)); - assert false - in - fun _ _ _ -> term)) - uris - let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" - let disambiguate_thing ~dbd ~context ~metasenv ~subst + let disambiguate_thing + ~context ~metasenv ~subst ~mk_implicit ~initial_ugraph:base_univ ~hint - ~aliases ~universe + ~aliases ~universe ~lookup_in_library ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing ~localization_tbl (thing_txt,thing_txt_prefix_len,thing) @@ -1062,20 +1058,11 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" let lookup_choices = fun item -> let choices = - let lookup_in_library () = - match item with - | Id id -> choices_of_id dbd id - | Symbol (symb, _) -> - (try - List.map DisambiguateChoices.mk_choice - (TermAcicContent.lookup_interpretations symb) - with - TermAcicContent.Interpretation_not_found -> []) - | Num instance -> - DisambiguateChoices.lookup_num_choices () - in match universe with - | None -> lookup_in_library () + | None -> + lookup_in_library + C.interactive_user_uri_choice + C.input_or_locate_uri item | Some e -> (try let item = @@ -1084,7 +1071,10 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" | item -> item in Environment.find item e - with Not_found -> lookup_in_library ()) + with Not_found -> + lookup_in_library + C.interactive_user_uri_choice + C.input_or_locate_uri item) in choices in @@ -1124,8 +1114,8 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing" ("Implicit", (match item with | Id _ | Num _ -> - (fun _ _ _ -> Cic.Implicit (Some `Closed)) - | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) + (fun _ _ _ -> mk_implicit (Some `Closed)) + | Symbol _ -> (fun _ _ _ -> mk_implicit None))) env in aux (aux env l) tl in let filled_env = aux aliases todo_dom in @@ -1302,6 +1292,7 @@ in refine_profiler.HExtlib.profile foo () Not_found -> None) thing_dom in + let diff= List.map (fun a,b -> a,fst b) diff in env',diff,loc_msg,significant ) errors in @@ -1337,14 +1328,16 @@ in refine_profiler.HExtlib.profile foo () CicEnvironment.CircularDependency s -> failwith "Disambiguate: circular dependency" - let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv + let disambiguate_term ?(fresh_instances=false) ~context ~metasenv ~subst ?goal ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe + ~lookup_in_library (text,prefix_len,term) = let term = if fresh_instances then CicNotationUtil.freshen_term term else term in + let mk_implicit x = Cic.Implicit x in let hint = match goal with | None -> (fun _ x -> x), fun k -> k | Some i -> @@ -1360,18 +1353,21 @@ in refine_profiler.HExtlib.profile foo () | k -> k in let localization_tbl = Cic.CicHash.create 503 in - disambiguate_thing ~dbd ~context ~metasenv ~subst - ~initial_ugraph ~aliases - ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term + disambiguate_thing ~context ~metasenv ~subst + ~initial_ugraph ~aliases ~mk_implicit + ~universe ~lookup_in_library + ~uri:None ~pp_thing:CicNotationPp.pp_term ~domain_of_thing:domain_of_term ~interpretate_thing:(interpretate_term (?create_dummy_ids:None)) ~refine_thing:refine_term (text,prefix_len,term) ~localization_tbl ~hint - let disambiguate_obj ?(fresh_instances=false) ~dbd ~aliases ~universe ~uri - (text,prefix_len,obj) + let disambiguate_obj + ?(fresh_instances=false) ~aliases ~universe ~uri ~lookup_in_library + (text,prefix_len,obj) = + let mk_implicit x = Cic.Implicit x in let obj = if fresh_instances then CicNotationUtil.freshen_obj obj else obj in @@ -1380,9 +1376,11 @@ in refine_profiler.HExtlib.profile foo () fun k -> k in let localization_tbl = Cic.CicHash.create 503 in - disambiguate_thing ~dbd ~context:[] ~metasenv:[] ~subst:[] - ~aliases ~universe ~uri - ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) ~domain_of_thing:domain_of_obj + disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] + ~aliases ~universe ~uri ~mk_implicit + ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term) + ~domain_of_thing:domain_of_obj + ~lookup_in_library ~initial_ugraph:CicUniv.empty_ugraph ~interpretate_thing:interpretate_obj ~refine_thing:refine_obj ~localization_tbl