* useless for the final user ... *)
exception NoWellTypedInterpretation of
int *
- ((Token.flocation list * string * string) list *
+ ((Stdpp.location list * string * string) list *
(DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
- Token.flocation option * string Lazy.t * bool) list
+ Stdpp.location option * string Lazy.t * bool) list
exception PathNotWellFormed
val interpretate_path :
type 'a disambiguator_input = string * int * 'a
+type domain = domain_tree list
+and domain_tree =
+ Node of Stdpp.location list * DisambiguateTypes.domain_item * domain
+type ('a,'m) test_result =
+ | Ok of 'a * 'm
+ | Ko of Stdpp.location option * string Lazy.t
+ | Uncertain of Stdpp.location option * string Lazy.t
+exception Try_again of string Lazy.t
+
+val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain
+
module type Disambiguator =
sig
+ val disambiguate_thing:
+ dbd:HSql.dbd ->
+ context:'context ->
+ metasenv:'metasenv ->
+ initial_ugraph:'ugraph ->
+ aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
+ universe:DisambiguateTypes.codomain_item list
+ DisambiguateTypes.Environment.t option ->
+ uri:'uri ->
+ pp_thing:('ast_thing -> string) ->
+ domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
+ interpretate_thing:(context:'context ->
+ env:DisambiguateTypes.codomain_item
+ DisambiguateTypes.Environment.t ->
+ uri:'uri ->
+ is_path:bool ->
+ 'ast_thing ->
+ localization_tbl:'cichash -> 'raw_thing) ->
+ refine_thing:('metasenv ->
+ 'context ->
+ 'uri ->
+ 'raw_thing ->
+ 'ugraph -> localization_tbl:'cichash -> ('refined_thing,
+ 'metasenv) test_result * 'ugraph) ->
+ localization_tbl:'cichash ->
+ string * int * 'ast_thing ->
+ ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
+ list * 'metasenv * 'refined_thing * 'ugraph)
+ list * bool
+
(** @param fresh_instances when set to true fresh instances will be generated
* for each number _and_ symbol in the disambiguation domain. Instances of the
* input AST will be ignored. Defaults to false. *)
val disambiguate_term :
?fresh_instances:bool ->
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
context:Cic.context ->
metasenv:Cic.metasenv ->
?initial_ugraph:CicUniv.universe_graph ->
(** @param fresh_instances as per disambiguate_term *)
val disambiguate_obj :
?fresh_instances:bool ->
- dbd:HMysql.dbd ->
+ dbd:HSql.dbd ->
aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
universe:DisambiguateTypes.multiple_environment option ->
uri:UriManager.uri option -> (* required only for inductive types *)
Cic.obj *
CicUniv.universe_graph) list * (* disambiguated obj *)
bool (* has interactive_interpretation_choice been invoked? *)
+
end
module Make (C : DisambiguateTypes.Callbacks) : Disambiguator