From: Stefano Zacchiroli Date: Fri, 22 Apr 2005 15:05:52 +0000 (+0000) Subject: added Trivial module with a disambiguate_term implementation which took X-Git-Tag: after_svn_merge~21 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a1b3b062ef799002baf9f21c6e5850b190af5977;p=helm.git 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) --- 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 +