1. grafiteDisambiguator => multiPassDisambiguator

[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 201bdb3b7bb7178f7f4c11111b0062426dbfe5bc..92e11870fae27428f5cb61adb63058c1c625a823 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.mli
+++ b/helm/software/components/cic_disambiguation/disambiguate.mli
@@ -41,9 +41,6 @@ exception NoWellTypedInterpretation of
   bool) list
 exception PathNotWellFormed
 
-val interpretate_path :
-  context:Cic.name list -> CicNotationPt.term -> Cic.term
-
 type 'a disambiguator_input = string * int * 'a
     
 type domain = domain_tree list
@@ -57,7 +54,19 @@ type ('term,'metasenv,'subst,'graph) test_result =
 
 exception Try_again of string Lazy.t
 
+val resolve : 
+  'term DisambiguateTypes.environment ->
+  DisambiguateTypes.Environment.key ->
+    ?num:string -> ?args:'term list -> unit -> 'term
+
+val find_in_context: string -> Cic.name list -> int
+
 val domain_of_ast_term: context:Cic.name list -> CicNotationPt.term -> domain
+val domain_of_term: context:
+  (Cic.name * 'a) option list -> CicNotationPt.term -> domain
+val domain_of_obj: 
+  context:(Cic.name * 'a) option list -> 
+    CicNotationPt.term CicNotationPt.obj -> domain
 
 module type Disambiguator =
 sig
@@ -65,95 +74,43 @@ sig
     context:'context ->
     metasenv:'metasenv ->
     subst:'subst ->
-    mk_implicit:([ `Closed ] option -> 'refined_thing) ->
+    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_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) ->
+    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) ->
     uri:'uri ->
     pp_thing:('ast_thing -> string) ->
     domain_of_thing:(context:'context -> 'ast_thing -> domain) ->
-    interpretate_thing:(context:'context ->
-                        env:'refined_thing 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) ->
+    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_thing DisambiguateTypes.codomain_item) list * 
+      'refined_term DisambiguateTypes.codomain_item) list * 
      'metasenv * 'subst * 'refined_thing * 'ugraph)
-     list * bool
-
-  val disambiguate_term :
-    ?fresh_instances:bool ->
-    context:Cic.context ->
-    metasenv:Cic.metasenv -> 
-    subst:Cic.substitution ->
-    ?goal:int ->
-    ?initial_ugraph:CicUniv.universe_graph -> 
-    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 * Cic.term DisambiguateTypes.codomain_item) list *
-     Cic.metasenv *                  (* new metasenv *)
-     Cic.substitution *
-     Cic.term*
-     CicUniv.universe_graph) list *  (* disambiguated term *)
-    bool
-
-  val disambiguate_obj :
-    ?fresh_instances:bool ->
-    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 * Cic.term DisambiguateTypes.codomain_item) list *
-     Cic.metasenv *                  (* new metasenv *)
-     Cic.substitution *
-     Cic.obj *
-     CicUniv.universe_graph) list *  (* disambiguated obj *)
-    bool
+    list * bool
 end
 
 module Make (C : DisambiguateTypes.Callbacks) : Disambiguator