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 *)
in
aux dom1
-module type Disambiguator =
-sig
- 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 ->
- 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
-
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
let disambiguate_thing
~mk_implicit ~description_of_alias
~aliases ~universe ~lookup_in_library
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
- ~localization_tbl
+ ~mk_localization_tbl
(thing_txt,thing_txt_prefix_len,thing)
=
debug_print (lazy "DISAMBIGUATE INPUT");
| item -> item
in
Environment.find item e
- with Not_found ->
- lookup_in_library
- interactive_user_uri_choice
- input_or_locate_uri item)
+ with Not_found -> [])
in
(*
(* <benchmark> *)
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
(inner_dom@remaining_dom@rem_dom) base_univ
with
| Ok (thing, metasenv,subst,new_univ) ->
+(* prerr_endline "OK"; *)
let res =
(match inner_dom with
| [] ->
in
res @@ filter tl
| Uncertain loc_msg ->
+(* prerr_endline ("UNCERTAIN"); *)
let res =
(match inner_dom with
| [] -> [],[new_env,new_diff,loc_msg],[]
in
res @@ filter tl
| Ko loc_msg ->
+(* prerr_endline "KO"; *)
let res = [],[],[new_env,new_diff,loc_msg,true] in
res @@ filter tl)
in
) 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]
+ 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