From a1b3b062ef799002baf9f21c6e5850b190af5977 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 22 Apr 2005 15:05:52 +0000
Subject: [PATCH] added Trivial module with a disambiguate_term implementation
 which took a string as input and return a Cic.term (if the input is not
 ambiguous)

---
 helm/ocaml/cic_disambiguation/disambiguate.ml | 22 +++++++++++++++++++
 .../ocaml/cic_disambiguation/disambiguate.mli | 20 +++++++++++++++++
 2 files changed, 42 insertions(+)

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 9f4c41d2e..1812285e0 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -608,3 +608,25 @@ module Make (C: Callbacks) =
         failwith "Disambiguate: circular dependency"
   end
 
+module Trivial =
+struct
+  exception Ambiguous_term of string
+  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 = Make (Callbacks)
+  let disambiguate_string ~dbd context metasenv ?initial_ugraph
+        ?(aliases = DisambiguateTypes.Environment.empty) term =
+    let ast = CicTextualParser2.parse_term (Stream.of_string term) in
+    try
+      Disambiguator.disambiguate_term ~dbd context metasenv ast ?initial_ugraph
+        ~aliases
+    with Exit -> raise (Ambiguous_term term)
+end
+
diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index b0fe0fcd3..4db990283 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -44,3 +44,23 @@ module Make (C : Callbacks) :
        CicUniv.universe_graph) list    (* disambiguated term *)
   end
 
+module Trivial:
+sig
+  exception Ambiguous_term of string
+
+  (** 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:Mysql.dbd ->
+    Cic.context ->
+    Cic.metasenv ->
+    ?initial_ugraph:CicUniv.universe_graph -> 
+    ?aliases:environment ->         (* previous interpretation status *)
+    string ->
+    (environment *                  (* new interpretation status *)
+     Cic.metasenv *                 (* new metasenv *)
+     Cic.term *
+     CicUniv.universe_graph) list   (* disambiguated term *)
+end
+
-- 
2.39.2