changed META dependency

[helm.git] / helm / ocaml / paramodulation / saturate_main.ml

diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml
index ce4182e1ac6ac8620ef002181ef16e0097fe06df..69d50e3a0cd7264ea84685d06417f9792bea4fb8 100644 (file)
--- a/helm/ocaml/paramodulation/saturate_main.ml
+++ b/helm/ocaml/paramodulation/saturate_main.ml
@@ -23,6 +23,49 @@
  * http://cs.unibo.it/helm/.
  *)
 
+module Trivial_disambiguate:
+sig
+  exception Ambiguous_term of string Lazy.t
+  (** disambiguate an _unanmbiguous_ term using dummy callbacks which fail if a
+    * choice from the user is needed to disambiguate the term
+    * @raise Ambiguous_term for ambiguous term *)
+  val disambiguate_string:
+    dbd:HMysql.dbd ->
+    ?context:Cic.context ->
+    ?metasenv:Cic.metasenv ->
+    ?initial_ugraph:CicUniv.universe_graph -> 
+    ?aliases:DisambiguateTypes.environment ->(* previous interpretation status*)
+    string ->
+    ((DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+     Cic.metasenv *                 (* new metasenv *)
+     Cic.term *
+     CicUniv.universe_graph) list   (* disambiguated term *)
+end
+=
+struct
+  exception Ambiguous_term of string Lazy.t
+  exception Exit
+  module Callbacks =
+  struct
+    let interactive_user_uri_choice ~selection_mode ?ok
+          ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
+              raise Exit
+    let interactive_interpretation_choice interp = raise Exit
+    let input_or_locate_uri ~(title:string) ?id = raise Exit
+  end
+  module Disambiguator = Disambiguate.Make (Callbacks)
+  let disambiguate_string ~dbd ?(context = []) ?(metasenv = []) ?initial_ugraph
+    ?(aliases = DisambiguateTypes.Environment.empty) term
+  =
+    let ast =
+      CicNotationParser.parse_level2_ast (Ulexing.from_utf8_string term)
+    in
+    try
+      fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast
+        ?initial_ugraph ~aliases ~universe:None)
+    with Exit -> raise (Ambiguous_term (lazy term))
+end
+
 let configuration_file = ref "../../matita/matita.conf.xml";;
 
 let core_notation_script = "../../matita/core_notation.moo";;
@@ -35,7 +78,7 @@ let get_from_user ~(dbd:HMysql.dbd) =
   in
   let term_string = String.concat "\n" (get ()) in
   let env, metasenv, term, ugraph =
-    List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
+    List.nth (Trivial_disambiguate.disambiguate_string dbd term_string) 0
   in
   term, metasenv, ugraph
 ;;