(** {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 * (Token.flocation option * string Lazy.t) list
+ int *
+ ((Stdpp.location list * string * string) list *
+ (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+ Stdpp.location option * 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
* 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 *)
- CicNotationPt.obj disambiguator_input ->
+ CicNotationPt.term CicNotationPt.obj disambiguator_input ->
((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
Cic.metasenv * (* new metasenv *)
Cic.obj *