disambiguation even more abstracted

[helm.git] / helm / software / components / cic_disambiguation / disambiguate.mli

diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli
index bb4c726403d8db3ee08c242e274985bf01954c19..201bdb3b7bb7178f7f4c11111b0062426dbfe5bc 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.mli
+++ b/helm/software/components/cic_disambiguation/disambiguate.mli
@@ -36,8 +36,9 @@
 exception NoWellTypedInterpretation of
  int *
  ((Stdpp.location list * string * string) list *
-  (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-  (Stdpp.location * string) Lazy.t * bool) list
+  (DisambiguateTypes.domain_item * string) list *
+  (Stdpp.location * string) Lazy.t *
+  bool) list
 exception PathNotWellFormed
 
 val interpretate_path :
@@ -61,22 +62,32 @@ 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 ->
     subst:'subst ->
+    mk_implicit:([ `Closed ] option -> 'refined_thing) ->
     initial_ugraph:'ugraph ->
     hint: ('metasenv -> 'raw_thing -> 'raw_thing) * 
           (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
               ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
-    aliases:DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
-    universe:DisambiguateTypes.codomain_item list
+    aliases:'refined_thing DisambiguateTypes.codomain_item DisambiguateTypes.Environment.t ->
+    universe:'refined_thing DisambiguateTypes.codomain_item list
              DisambiguateTypes.Environment.t option ->
+    lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
+                        ?ok:string ->
+                        ?enable_button_for_non_vars:bool ->
+                        title:string ->
+                        msg:string ->
+                        id:string ->
+                        UriManager.uri list -> UriManager.uri list) ->
+                       (title:string -> ?id:string -> unit -> UriManager.uri option) ->
+                       DisambiguateTypes.Environment.key ->
+                       'refined_thing DisambiguateTypes.codomain_item list) ->
     uri:'uri ->
     pp_thing:('ast_thing -> string) ->
     domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
     interpretate_thing:(context:'context ->
-                        env:DisambiguateTypes.codomain_item
+                        env:'refined_thing DisambiguateTypes.codomain_item
                             DisambiguateTypes.Environment.t ->
                         uri:'uri ->
                         is_path:bool -> 'ast_thing -> localization_tbl:'cichash -> 'raw_thing) ->
@@ -89,22 +100,32 @@ sig
                   ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
     localization_tbl:'cichash ->
     string * int * 'ast_thing ->
-    ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
-     list * 'metasenv * 'subst * 'refined_thing * 'ugraph)
-    list * bool
+    ((DisambiguateTypes.Environment.key * 
+    'refined_thing DisambiguateTypes.codomain_item) list * 
+     'metasenv * 'subst * 'refined_thing * 'ugraph)
+     list * bool
 
   val disambiguate_term :
     ?fresh_instances:bool ->
-    dbd:HSql.dbd ->
     context:Cic.context ->
     metasenv:Cic.metasenv -> 
     subst:Cic.substitution ->
     ?goal:int ->
     ?initial_ugraph:CicUniv.universe_graph -> 
-    aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
-    universe:DisambiguateTypes.multiple_environment option ->
+    aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *)
+    universe:Cic.term DisambiguateTypes.multiple_environment option ->
+    lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
+                        ?ok:string ->
+                        ?enable_button_for_non_vars:bool ->
+                        title:string ->
+                        msg:string ->
+                        id:string ->
+                        UriManager.uri list -> UriManager.uri list) ->
+                       (title:string -> ?id:string -> unit -> UriManager.uri option) ->
+                       DisambiguateTypes.Environment.key ->
+                       Cic.term DisambiguateTypes.codomain_item list) ->
     CicNotationPt.term disambiguator_input ->
-    ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+    ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.substitution *
      Cic.term*
@@ -113,12 +134,21 @@ sig
 
   val disambiguate_obj :
     ?fresh_instances:bool ->
-    dbd:HSql.dbd ->
-    aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
-    universe:DisambiguateTypes.multiple_environment option ->
+    aliases:Cic.term DisambiguateTypes.environment ->(* previous interpretation status *)
+    universe:Cic.term DisambiguateTypes.multiple_environment option ->
     uri:UriManager.uri option ->     (* required only for inductive types *)
+    lookup_in_library:((selection_mode:[ `MULTIPLE | `SINGLE ] ->
+                        ?ok:string ->
+                        ?enable_button_for_non_vars:bool ->
+                        title:string ->
+                        msg:string ->
+                        id:string ->
+                        UriManager.uri list -> UriManager.uri list) ->
+                       (title:string -> ?id:string -> unit -> UriManager.uri option) ->
+                       DisambiguateTypes.Environment.key ->
+                       Cic.term DisambiguateTypes.codomain_item list) ->
     CicNotationPt.term CicNotationPt.obj disambiguator_input ->
-    ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+    ((DisambiguateTypes.domain_item * Cic.term DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
      Cic.substitution *
      Cic.obj *