val set_choose_interp_callback:
DisambiguateTypes.interactive_interpretation_choice_type -> unit
+val set_choose_disamb_callback:
+ DisambiguateTypes.interactive_ast_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_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type
val resolve :
- env:'alias DisambiguateTypes.Environment.t ->
- mk_choice:('alias -> 'term DisambiguateTypes.codomain_item) ->
- DisambiguateTypes.Environment.key ->
+ env:'alias1 DisambiguateTypes.InterprEnv.t ->
+ universe: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
+ mk_choice:('alias1 -> 'term DisambiguateTypes.codomain_item) ->
+ DisambiguateTypes.InterprEnv.key -> 'alias1 option ->
[`Num_arg of string | `Args of 'term list] -> 'term
val find_in_context: string -> string option list -> int
val domain_of_obj:
context:string option list -> NotationPt.term NotationPt.obj -> domain
-(* val disambiguate_list :
- context:'context ->
- metasenv:'metasenv ->
- subst:'subst ->
- use_coercions:bool ->
- expty:'refined_thing option ->
- env:GrafiteAst.alias_spec DisambiguateTypes.Environment.t ->
- uri:'uri ->
- interpretate_thing:(context:'context ->
- env:GrafiteAst.alias_spec DisambiguateTypes.Environment.t ->
- uri:'uri ->
- is_path:bool ->
- 'ast_thing -> localization_tbl:'cic_hash -> 'raw_thing) ->
- refine_thing:('metasenv -> 'subst -> 'context -> 'uri ->
- use_coercions:bool -> 'raw_thing -> 'refined_thing option ->
- 'ugraph -> localization_tbl:'cic_hash ->
- ('refined_thing, 'metasenv, 'subst, 'ugraph) test_result) ->
- ugraph:'ugraph ->
- visit:((NotationPt.term -> bool) -> 'ast_thing ->
- ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) ->
- universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
- mk_localization_tbl:(int -> 'cic_hash) ->
- 'ast_thing list -> ('ast_thing * 'ast_thing list) option
-*)
-
-(* val initialize_ast : unit *)
-
val disambiguate_thing:
context:'context ->
metasenv:'metasenv ->
mk_implicit:(bool -> 'alias) ->
description_of_alias:('alias -> string) ->
fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
- aliases:'alias DisambiguateTypes.Environment.t ->
+ aliases:'alias DisambiguateTypes.InterprEnv.t ->
universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
lookup_in_library:(
DisambiguateTypes.interactive_user_uri_choice_type ->
domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
interpretate_thing:(
context:'context ->
- env:'alias DisambiguateTypes.Environment.t ->
+ env:'alias DisambiguateTypes.InterprEnv.t ->
+ universe: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
uri:'uri ->
is_path:bool ->
'ast_thing ->
((NotationPt.term -> 'ast_thing) * NotationPt.term) option) ->
mk_localization_tbl:(int -> 'cichash) ->
'ast_thing disambiguator_input ->
- ((DisambiguateTypes.Environment.key * 'alias) list *
- 'metasenv * 'subst * 'refined_thing * 'ugraph)
- list * bool
+ ('ast_thing * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool
val bfvisit :
pp_term:(NotationPt.term -> string) ->