X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.mli;h=78fe417683e33dd6e03cce852851cfa608cf86cd;hb=3007de3f032ea2349cb2f8fffc76b18d26895f36;hp=5dc0df28b164feaa1d89c880e7cdb3f5323ef0d7;hpb=683978a2627cf1ce15673360f26806593d22f7b5;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli
index 5dc0df28b..78fe41768 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.mli
+++ b/helm/software/components/cic_disambiguation/disambiguate.mli
@@ -45,8 +45,49 @@ val interpretate_path :
 
 type 'a disambiguator_input = string * int * 'a
     
+type domain = domain_tree list
+and domain_tree = 
+  Node of Stdpp.location list * DisambiguateTypes.domain_item * domain
+type ('a,'m) test_result =
+  | Ok of 'a * 'm
+  | Ko of Stdpp.location option * string Lazy.t
+  | Uncertain of Stdpp.location option * string Lazy.t
+exception Try_again of string Lazy.t
+
+val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain
+
 module type Disambiguator =
 sig
+  val disambiguate_thing:
+    dbd:HSql.dbd ->
+    context:'context ->
+    metasenv:'metasenv ->
+    initial_ugraph:'ugraph ->
+    aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
+    universe:DisambiguateTypes.codomain_item list
+             DisambiguateTypes.Environment.t option ->
+    uri:'uri ->
+    pp_thing:('ast_thing -> string) ->
+    domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
+    interpretate_thing:(context:'context ->
+                        env:DisambiguateTypes.codomain_item
+                            DisambiguateTypes.Environment.t ->
+                        uri:'uri ->
+                        is_path:bool -> 
+                        'ast_thing -> 
+                        localization_tbl:'cichash -> 'raw_thing) ->
+    refine_thing:('metasenv ->
+                  'context ->
+                  'uri ->
+                  'raw_thing ->
+                  'ugraph -> localization_tbl:'cichash -> ('refined_thing,
+                  'metasenv) test_result * 'ugraph) ->
+    localization_tbl:'cichash ->
+    string * int * 'ast_thing ->
+    ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
+     list * 'metasenv * 'refined_thing * 'ugraph)
+    list * bool
+
   (** @param fresh_instances when set to true fresh instances will be generated
    * for each number _and_ symbol in the disambiguation domain. Instances of the
    * input AST will be ignored. Defaults to false. *)
@@ -78,6 +119,7 @@ sig
      Cic.obj *
      CicUniv.universe_graph) list *  (* disambiguated obj *)
     bool  (* has interactive_interpretation_choice been invoked? *)
+
 end
 
 module Make (C : DisambiguateTypes.Callbacks) : Disambiguator