(** {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
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) ->
[`Num_arg of string | `Args of 'term list] -> 'term
val find_in_context: string -> string option list -> int
-val domain_of_ast_term: context:
- string option list -> CicNotationPt.term -> domain
val domain_of_term: context:
string option list -> CicNotationPt.term -> domain
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 ->
+ expty: 'refined_thing option ->
+ mk_implicit:(bool -> 'alias) ->
+ description_of_alias:('alias -> string) ->
+ fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
+ 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 -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash ->
+ ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
+ mk_localization_tbl:(int -> 'cichash) ->
+ 'ast_thing disambiguator_input ->
+ ((DisambiguateTypes.Environment.key * 'alias) list *
+ 'metasenv * 'subst * 'refined_thing * 'ugraph)
+ list * bool