X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.mli;h=5c74b857b49077bd1d68048af460252e5bc023a3;hb=62f476a05884d451bfb90d845ea2b1c0a1c77f96;hp=92e11870fae27428f5cb61adb63058c1c625a823;hpb=f4d41a527321e5fbdc10054b46ad60fe9f7f54a1;p=helm.git

diff --git a/helm/software/components/disambiguation/disambiguate.mli b/helm/software/components/disambiguation/disambiguate.mli
index 92e11870f..5c74b857b 100644
--- a/helm/software/components/disambiguation/disambiguate.mli
+++ b/helm/software/components/disambiguation/disambiguate.mli
@@ -25,6 +25,10 @@
 
 (** {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
@@ -54,64 +58,73 @@ 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
+
+(** @raise Ambiguous_input if called, default value for internal
+  * choose_uris_callback if not set otherwise with set_choose_uris_callback
+  * above *)
+val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type
+
+(** @raise Ambiguous_input if called, default value for internal
+  * choose_interp_callback if not set otherwise with set_choose_interp_callback
+  * above *)
+val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type
+
 val resolve : 
-  'term DisambiguateTypes.environment ->
+  env:'alias DisambiguateTypes.Environment.t ->
+  mk_choice:('alias -> 'term DisambiguateTypes.codomain_item) ->
   DisambiguateTypes.Environment.key ->
-    ?num:string -> ?args:'term list -> unit -> 'term
-
-val find_in_context: string -> Cic.name list -> int
+   [`Num_arg of string | `Args of 'term list] -> 'term
 
-val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain
+val find_in_context: string -> string option list -> int
+val domain_of_ast_term: context:
+  string option list -> CicNotationPt.term -> domain
 val domain_of_term: context:
-  (Cic.name * 'a) option list -> CicNotationPt.term -> domain
+  string option list -> CicNotationPt.term -> domain
 val domain_of_obj: 
-  context:(Cic.name * 'a) option list -> 
-    CicNotationPt.term CicNotationPt.obj -> domain
+  context:string option list -> CicNotationPt.term CicNotationPt.obj -> domain
 
-module type Disambiguator =
-sig
-  val disambiguate_thing:
+val disambiguate_thing:
+  context:'context ->
+  metasenv:'metasenv ->
+  subst:'subst ->
+  use_coercions:bool ->
+  string_context_of_context:('context -> string option list) ->
+  initial_ugraph:'ugraph ->
+  hint: 
+    ('metasenv -> 'raw_thing -> 'raw_thing) * 
+    (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
+       ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
+  mk_implicit:(bool -> 'alias) ->
+  description_of_alias:('alias -> string) ->
+  aliases:'alias DisambiguateTypes.Environment.t ->
+  universe:'alias list DisambiguateTypes.Environment.t option ->
+  lookup_in_library:(
+    DisambiguateTypes.interactive_user_uri_choice_type ->
+    DisambiguateTypes.input_or_locate_uri_type ->
+    DisambiguateTypes.Environment.key ->
+    'alias list) ->
+  uri:'uri ->
+  pp_thing:('ast_thing -> string) ->
+  domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
+  interpretate_thing:(
     context:'context ->
-    metasenv:'metasenv ->
-    subst:'subst ->
-    mk_implicit:(bool -> 'refined_term) ->
-    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_term DisambiguateTypes.codomain_item 
-      DisambiguateTypes.Environment.t ->
-    universe:'refined_term DisambiguateTypes.codomain_item list
-      DisambiguateTypes.Environment.t option ->
-    lookup_in_library:(
-      DisambiguateTypes.interactive_user_uri_choice_type ->
-      DisambiguateTypes.input_or_locate_uri_type ->
-      DisambiguateTypes.Environment.key ->
-      'refined_term DisambiguateTypes.codomain_item list) ->
+    env:'alias DisambiguateTypes.Environment.t ->
     uri:'uri ->
-    pp_thing:('ast_thing -> string) ->
-    domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
-    interpretate_thing:(
-      context:'context ->
-      env:'refined_term 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_term DisambiguateTypes.codomain_item) list * 
-     'metasenv * 'subst * 'refined_thing * 'ugraph)
-    list * bool
-end
-
-module Make (C : DisambiguateTypes.Callbacks) : Disambiguator
-
+    is_path:bool -> 
+    'ast_thing -> 
+    localization_tbl:'cichash -> 
+      'raw_thing) ->
+  refine_thing:(
+    'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
+    'raw_thing -> 'ugraph -> localization_tbl:'cichash -> 
+      ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
+  mk_localization_tbl:(int -> 'cichash) ->
+  string * int * 'ast_thing ->
+  ((DisambiguateTypes.Environment.key * 'alias) list * 
+   'metasenv * 'subst * 'refined_thing * 'ugraph)
+  list * bool