disambiguation now returns and takes in input the substitution

[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 c94273804e70a1f0bdafc7409bb282dfa9f7d377..b21c2bbe0f2480b996a44e3bef3379fc5a9c0cae 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.mli
+++ b/helm/software/components/cic_disambiguation/disambiguate.mli
@@ -48,10 +48,12 @@ 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
+
+type ('term,'metasenv,'subst,'graph) test_result =
+  | Ok of 'term * 'metasenv * 'subst * 'graph
   | 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
@@ -61,11 +63,12 @@ sig
   val disambiguate_thing:
     dbd:HSql.dbd ->
     context:'context ->
-    metasenv:'metasenv -> 
+    metasenv:'metasenv ->
+    subst:'subst ->
     initial_ugraph:'ugraph ->
     hint: ('metasenv -> 'raw_thing -> 'raw_thing) * 
-          (('refined_thing,'metasenv) test_result -> 'ugraph ->
-              ('refined_thing,'metasenv) test_result * 'ugraph) ->
+          (('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
              DisambiguateTypes.Environment.t option ->
@@ -76,40 +79,38 @@ sig
                         env:DisambiguateTypes.codomain_item
                             DisambiguateTypes.Environment.t ->
                         uri:'uri ->
-                        is_path:bool -> 
-                        'ast_thing -> 
-                        localization_tbl:'cichash -> 'raw_thing) ->
+                        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) test_result * 'ugraph) ->
+                  'ugraph -> localization_tbl:'cichash -> 
+                  ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
     localization_tbl:'cichash ->
     string * int * 'ast_thing ->
     ((DisambiguateTypes.Environment.key * DisambiguateTypes.codomain_item)
-     list * 'metasenv * 'refined_thing * 'ugraph)
+     list * 'metasenv * 'subst * '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. *)
   val disambiguate_term :
     ?fresh_instances:bool ->
     dbd:HSql.dbd ->
     context:Cic.context ->
-    metasenv:Cic.metasenv -> ?goal:int ->
+    metasenv:Cic.metasenv -> 
+    subst:Cic.substitution ->
+    ?goal:int ->
     ?initial_ugraph:CicUniv.universe_graph -> 
     aliases:DisambiguateTypes.environment ->(* previous interpretation status *)
     universe:DisambiguateTypes.multiple_environment option ->
     CicNotationPt.term disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
-     Cic.term *
+     Cic.substitution *
+     Cic.term*
      CicUniv.universe_graph) list *  (* disambiguated term *)
-    bool  (* has interactive_interpretation_choice been invoked? *)
+    bool
 
-  (** @param fresh_instances as per disambiguate_term *)
   val disambiguate_obj :
     ?fresh_instances:bool ->
     dbd:HSql.dbd ->
@@ -119,10 +120,10 @@ sig
     CicNotationPt.term CicNotationPt.obj disambiguator_input ->
     ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
      Cic.metasenv *                  (* new metasenv *)
+     Cic.substitution *
      Cic.obj *
      CicUniv.universe_graph) list *  (* disambiguated obj *)
-    bool  (* has interactive_interpretation_choice been invoked? *)
-
+    bool
 end
 
 module Make (C : DisambiguateTypes.Callbacks) : Disambiguator