X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fdisambiguation%2Fdisambiguate.mli;h=2e6677d727f7996bf60b813363b78079c4c1b95f;hb=04cd2181640b3828b3d193a8e819c849ef574236;hp=43fe7a717e039f8e51e622c4419d9fe96b9d3890;hpb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git

diff --git a/matitaB/components/disambiguation/disambiguate.mli b/matitaB/components/disambiguation/disambiguate.mli
index 43fe7a717..2e6677d72 100644
--- a/matitaB/components/disambiguation/disambiguate.mli
+++ b/matitaB/components/disambiguation/disambiguate.mli
@@ -25,10 +25,6 @@
 
 (** {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
@@ -58,12 +54,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 +73,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
@@ -86,33 +88,6 @@ val domain_of_term: context:
 val domain_of_obj: 
   context:string option list -> NotationPt.term NotationPt.obj -> domain
 
-(* val disambiguate_list :
-  context:'context ->
-  metasenv:'metasenv ->
-  subst:'subst ->
-  use_coercions:bool ->
-  expty:'refined_thing option ->
-  env:GrafiteAst.alias_spec DisambiguateTypes.Environment.t ->
-  uri:'uri ->
-  interpretate_thing:(context:'context ->
-                      env:GrafiteAst.alias_spec DisambiguateTypes.Environment.t ->
-                      uri:'uri ->
-                      is_path:bool ->
-                      'ast_thing -> localization_tbl:'cic_hash -> 'raw_thing) ->
-  refine_thing:('metasenv -> 'subst -> 'context -> 'uri ->
-                use_coercions:bool -> 'raw_thing -> 'refined_thing option ->
-                'ugraph -> localization_tbl:'cic_hash -> 
-                ('refined_thing, 'metasenv, 'subst, 'ugraph) test_result) ->
-  ugraph:'ugraph ->
-  visit:((NotationPt.term -> bool) -> 'ast_thing -> 
-        ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) ->
-  universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
-  mk_localization_tbl:(int -> 'cic_hash) ->
-  'ast_thing list -> ('ast_thing * 'ast_thing list) option
-*)
-
-(* val initialize_ast : unit *)
-
 val disambiguate_thing:
   context:'context ->
   metasenv:'metasenv ->
@@ -124,7 +99,7 @@ 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 ->
+  aliases:'alias DisambiguateTypes.InterprEnv.t ->
   universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
   lookup_in_library:(
     DisambiguateTypes.interactive_user_uri_choice_type ->
@@ -137,7 +112,8 @@ val disambiguate_thing:
   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 -> 
@@ -152,9 +128,7 @@ val disambiguate_thing:
         ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) -> 
   mk_localization_tbl:(int -> 'cichash) ->
   'ast_thing disambiguator_input ->
-  ((DisambiguateTypes.Environment.key * 'alias) list * 
-   'metasenv * 'subst * 'refined_thing * 'ugraph)
-  list * bool
+  ('ast_thing * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool
 
 val bfvisit :
   pp_term:(NotationPt.term -> string) ->