(** {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
- * - environment patch
- * - location
- * - error message
- * - significancy of the error message, if false the error is likely to be
- * useless for the final user ... *)
-exception NoWellTypedInterpretation of
- int *
- ((Stdpp.location list * string * string) list *
- (DisambiguateTypes.domain_item * string) list *
- (Stdpp.location * string) Lazy.t *
- bool) list
+type ('alias,'ast_thing,'metasenv,'subst,'thing,'ugraph) disamb_result =
+ | Disamb_success of ('ast_thing * 'metasenv * 'subst * 'thing * 'ugraph) list
+ | Disamb_failure of
+ (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list
+
+exception NoWellTypedInterpretation of (Stdpp.location * string)
+
exception PathNotWellFormed
type 'a disambiguator_input = string * int * 'a
exception Try_again of string Lazy.t
+(*
val set_choose_uris_callback:
DisambiguateTypes.interactive_user_uri_choice_type -> unit
* 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:'alias1 DisambiguateTypes.InterprEnv.t ->
('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
visit:(pp_term:(NotationPt.term -> string) ->
(NotationPt.term -> bool) -> 'ast_thing ->
- ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) ->
+ ((NotationPt.term -> 'ast_thing) * NotationPt.term * Stdpp.location) option) ->
mk_localization_tbl:(int -> 'cichash) ->
'ast_thing disambiguator_input ->
- ('ast_thing * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool
+ (GrafiteAst.alias_spec,'ast_thing,'metasenv,'subst,'refined_thing,'ugraph) disamb_result
+
+type 'ast marked_ast =
+ (NotationPt.term -> 'ast) * NotationPt.term * Stdpp.location
val bfvisit :
pp_term:(NotationPt.term -> string) ->
(NotationPt.term -> bool) ->
- NotationPt.term -> ((NotationPt.term -> NotationPt.term) * NotationPt.term) option
+ NotationPt.term -> (NotationPt.term marked_ast) option
val bfvisit_obj :
pp_term:(NotationPt.term -> string) ->
(NotationPt.term -> bool) ->
- NotationPt.term NotationPt.obj -> ((NotationPt.term -> NotationPt.term NotationPt.obj) * NotationPt.term) option
+ NotationPt.term NotationPt.obj ->
+ ((NotationPt.term NotationPt.obj) marked_ast) option