Matitaweb:

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

diff --git a/matitaB/components/disambiguation/disambiguate.mli b/matitaB/components/disambiguation/disambiguate.mli
index 2e6677d727f7996bf60b813363b78079c4c1b95f..ab347e1640eb5aed4461f4e57076eefcb3f2d62f 100644 (file)
--- a/matitaB/components/disambiguation/disambiguate.mli
+++ b/matitaB/components/disambiguation/disambiguate.mli
@@ -25,20 +25,16 @@
 
 (** {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 ... *)
+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
@@ -125,17 +121,21 @@ val disambiguate_thing:
       ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
   visit:(pp_term:(NotationPt.term -> string) ->
          (NotationPt.term -> bool) -> 'ast_thing -> 
-        ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) -> 
+        ((NotationPt.term -> 'ast_thing) * NotationPt.term * Stdpp.location) option) -> 
   mk_localization_tbl:(int -> 'cichash) ->
   'ast_thing disambiguator_input ->
-  ('ast_thing * '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 -> NotationPt.term) * NotationPt.term) option
+   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.term NotationPt.obj) * NotationPt.term) option
+   NotationPt.term NotationPt.obj -> 
+  ((NotationPt.term NotationPt.obj) marked_ast) option