Matitaweb:

[helm.git] / matitaB / components / disambiguation / disambiguate.mli

diff --git a/matitaB/components/disambiguation/disambiguate.mli b/matitaB/components/disambiguation/disambiguate.mli
index 167de714bf39b91d6338afc619530aaf47c41760..ab347e1640eb5aed4461f4e57076eefcb3f2d62f 100644 (file)
--- a/matitaB/components/disambiguation/disambiguate.mli
+++ b/matitaB/components/disambiguation/disambiguate.mli
@@ -25,24 +25,16 @@
 
 (** {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 ... *)
+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 *
+      (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list
+
 exception NoWellTypedInterpretation of
- int *
- ((Stdpp.location list * string * string) list *
-  (DisambiguateTypes.domain_item * string) list *
-  (Stdpp.location * string) Lazy.t *
-  bool) list
+ ((Stdpp.location * string) list *
+  (Stdpp.location * string) list)
+
 exception PathNotWellFormed
 
 type 'a disambiguator_input = string * int * 'a
@@ -58,12 +50,16 @@ type ('term,'metasenv,'subst,'graph) test_result =
 
 exception Try_again of string Lazy.t
 
+(*
 val set_choose_uris_callback:
   DisambiguateTypes.interactive_user_uri_choice_type -> unit
 
 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 *)
@@ -73,11 +69,13 @@ val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type
   * 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:'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
@@ -97,8 +95,8 @@ val disambiguate_thing:
   mk_implicit:(bool -> 'alias) ->
   description_of_alias:('alias -> string) ->
   fix_instance:(DisambiguateTypes.domain_item -> 'alias list -> 'alias list) ->
-  aliases:'alias DisambiguateTypes.Environment.t ->
-  universe:'alias list DisambiguateTypes.Environment.t option ->
+  aliases:'alias DisambiguateTypes.InterprEnv.t ->
+  universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
   lookup_in_library:(
     DisambiguateTypes.interactive_user_uri_choice_type ->
     DisambiguateTypes.input_or_locate_uri_type ->
@@ -106,10 +104,12 @@ val disambiguate_thing:
     'alias list) ->
   uri:'uri ->
   pp_thing:('ast_thing -> string) ->
+  pp_term:(NotationPt.term -> string) ->
   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 -> 
@@ -119,8 +119,23 @@ val disambiguate_thing:
     'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
     'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash -> 
       ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
+  visit:(pp_term:(NotationPt.term -> string) ->
+         (NotationPt.term -> bool) -> 'ast_thing -> 
+        ((NotationPt.term -> 'ast_thing) * NotationPt.term * Stdpp.location) option) -> 
   mk_localization_tbl:(int -> 'cichash) ->
   'ast_thing disambiguator_input ->
-  ((DisambiguateTypes.Environment.key * 'alias) list * 
-   '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 marked_ast) option
+
+val bfvisit_obj :
+  pp_term:(NotationPt.term -> string) -> 
+  (NotationPt.term -> bool) ->
+   NotationPt.term NotationPt.obj -> 
+  ((NotationPt.term NotationPt.obj) marked_ast) option