First commit with new (incomplete) disambiguation engine.

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

diff --git a/matitaB/components/disambiguation/disambiguate.mli b/matitaB/components/disambiguation/disambiguate.mli
index 167de714bf39b91d6338afc619530aaf47c41760..43fe7a717e039f8e51e622c4419d9fe96b9d3890 100644 (file)
--- a/matitaB/components/disambiguation/disambiguate.mli
+++ b/matitaB/components/disambiguation/disambiguate.mli
@@ -86,6 +86,33 @@ 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 ->
@@ -98,7 +125,7 @@ val disambiguate_thing:
   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 ->
+  universe:GrafiteAst.alias_spec list DisambiguateTypes.Environment.t ->
   lookup_in_library:(
     DisambiguateTypes.interactive_user_uri_choice_type ->
     DisambiguateTypes.input_or_locate_uri_type ->
@@ -106,6 +133,7 @@ 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 ->
@@ -119,8 +147,21 @@ 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) option) -> 
   mk_localization_tbl:(int -> 'cichash) ->
   'ast_thing disambiguator_input ->
   ((DisambiguateTypes.Environment.key * 'alias) list * 
    'metasenv * 'subst * 'refined_thing * 'ugraph)
   list * bool
+
+val bfvisit :
+  pp_term:(NotationPt.term -> string) -> 
+  (NotationPt.term -> bool) ->
+   NotationPt.term -> ((NotationPt.term -> NotationPt.term) * NotationPt.term) 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