(** {2 Disambiguation interface} *)
(* 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 * ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list * Token.flocation option * string Lazy.t) list
+ int *
+ ((Stdpp.location list * string * string) list *
+ (DisambiguateTypes.domain_item * string) list *
+ (Stdpp.location * string) Lazy.t *
+ bool) list
exception PathNotWellFormed
val interpretate_path :
- context:Cic.name list -> CicNotationPt.term ->
- Cic.term
+ context:Cic.name list -> CicNotationPt.term -> Cic.term
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 ('term,'metasenv,'subst,'graph) test_result =
+ | Ok of 'term * 'metasenv * 'subst * 'graph
+ | Ko of (Stdpp.location * string) Lazy.t
+ | Uncertain of (Stdpp.location * 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
- (** @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_thing:
+ context:'context ->
+ metasenv:'metasenv ->
+ subst:'subst ->
+ mk_implicit:([ `Closed ] option -> 'refined_thing) ->
+ initial_ugraph:'ugraph ->
+ hint: ('metasenv -> 'raw_thing -> 'raw_thing) *
+ (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
+ ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
+ aliases:'refined_thing DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
+ universe:'refined_thing DisambiguateTypes.codomain_item list
+ DisambiguateTypes.Environment.t option ->
+ lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
+ ?ok:string ->
+ ?enable_button_for_non_vars:bool ->
+ title:string ->
+ msg:string ->
+ id:string ->
+ UriManager.uri list -> UriManager.uri list) ->
+ (title:string -> ?id:string -> unit -> UriManager.uri option) ->
+ DisambiguateTypes.Environment.key ->
+ 'refined_thing DisambiguateTypes.codomain_item list) ->
+ uri:'uri ->
+ pp_thing:('ast_thing -> string) ->
+ domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
+ interpretate_thing:(context:'context ->
+ env:'refined_thing DisambiguateTypes.codomain_item
+ DisambiguateTypes.Environment.t ->
+ uri:'uri ->
+ is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
+ refine_thing:('metasenv ->
+ 'subst ->
+ 'context ->
+ 'uri ->
+ 'raw_thing ->
+ 'ugraph -> localization_tbl:'cichash ->
+ ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
+ localization_tbl:'cichash ->
+ string * int * 'ast_thing ->
+ ((DisambiguateTypes.Environment.key *
+ 'refined_thing DisambiguateTypes.codomain_item) list *
+ 'metasenv * 'subst * 'refined_thing * 'ugraph)
+ list * bool
+
val disambiguate_term :
?fresh_instances:bool ->
- dbd:HMysql.dbd ->
context:Cic.context ->
- metasenv:Cic.metasenv ->
+ metasenv:Cic.metasenv ->
+ subst:Cic.substitution ->
+ ?goal:int ->
?initial_ugraph:CicUniv.universe_graph ->
- aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
- universe:DisambiguateTypes.multiple_environment option ->
+ aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *)
+ universe:Cic.term DisambiguateTypes.multiple_environment option ->
+ lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
+ ?ok:string ->
+ ?enable_button_for_non_vars:bool ->
+ title:string ->
+ msg:string ->
+ id:string ->
+ UriManager.uri list -> UriManager.uri list) ->
+ (title:string -> ?id:string -> unit -> UriManager.uri option) ->
+ DisambiguateTypes.Environment.key ->
+ Cic.term DisambiguateTypes.codomain_item list) ->
CicNotationPt.term disambiguator_input ->
- ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
- Cic.term *
+ Cic.substitution *
+ Cic.term*
CicUniv.universe_graph) list * (* disambiguated term *)
- bool (* has interactive_interpretation_choice been invoked? *)
+ bool
- (** @param fresh_instances as per disambiguate_term *)
val disambiguate_obj :
?fresh_instances:bool ->
- dbd:HMysql.dbd ->
- aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
- universe:DisambiguateTypes.multiple_environment option ->
+ aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *)
+ universe:Cic.term DisambiguateTypes.multiple_environment option ->
uri:UriManager.uri option -> (* required only for inductive types *)
- CicNotationPt.obj disambiguator_input ->
- ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
+ ?ok:string ->
+ ?enable_button_for_non_vars:bool ->
+ title:string ->
+ msg:string ->
+ id:string ->
+ UriManager.uri list -> UriManager.uri list) ->
+ (title:string -> ?id:string -> unit -> UriManager.uri option) ->
+ DisambiguateTypes.Environment.key ->
+ Cic.term DisambiguateTypes.codomain_item list) ->
+ CicNotationPt.term CicNotationPt.obj disambiguator_input ->
+ ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
+ Cic.substitution *
Cic.obj *
CicUniv.universe_graph) list * (* disambiguated obj *)
- bool (* has interactive_interpretation_choice been invoked? *)
+ bool
end
module Make (C : DisambiguateTypes.Callbacks) : Disambiguator