From d065a590ca5c4aec5ab505f2cf9e295e6c900942 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 25 Nov 2005 10:30:33 +0000 Subject: [PATCH] changed META dependency - disambiguation should (and actually does) depend only on acic_content - paramodulation does not need disambiguation! (except for a test) --- .../METAS/meta.helm-cic_disambiguation.src | 2 +- helm/ocaml/METAS/meta.helm-paramodulation.src | 2 +- helm/ocaml/cic_disambiguation/disambiguate.ml | 25 ----------- .../ocaml/cic_disambiguation/disambiguate.mli | 20 --------- helm/ocaml/paramodulation/Makefile | 18 ++++---- helm/ocaml/paramodulation/saturate_main.ml | 45 ++++++++++++++++++- 6 files changed, 54 insertions(+), 58 deletions(-) diff --git a/helm/ocaml/METAS/meta.helm-cic_disambiguation.src b/helm/ocaml/METAS/meta.helm-cic_disambiguation.src index d0a61cd51..d2e467aae 100644 --- a/helm/ocaml/METAS/meta.helm-cic_disambiguation.src +++ b/helm/ocaml/METAS/meta.helm-cic_disambiguation.src @@ -1,4 +1,4 @@ -requires="helm-whelp helm-content_pres helm-cic_unification" +requires="helm-whelp helm-acic_content helm-cic_unification" version="0.0.1" archive(byte)="cic_disambiguation.cma" archive(native)="cic_disambiguation.cmxa" diff --git a/helm/ocaml/METAS/meta.helm-paramodulation.src b/helm/ocaml/METAS/meta.helm-paramodulation.src index 6fe6c9898..34a25fef0 100644 --- a/helm/ocaml/METAS/meta.helm-paramodulation.src +++ b/helm/ocaml/METAS/meta.helm-paramodulation.src @@ -1,4 +1,4 @@ -requires="helm-registry helm-tactics helm-cic_disambiguation mysql" +requires="helm-registry helm-tactics" version="0.0.1" archive(byte)="paramodulation.cma" archive(native)="paramodulation.cmxa" diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index e69099cb5..3e6ce26e7 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -947,28 +947,3 @@ in refine_profiler.HExtlib.profile foo () obj end -module Trivial = -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 = 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 - diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index bb506e8dc..f0ca92db0 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -69,23 +69,3 @@ end module Make (C : DisambiguateTypes.Callbacks) : Disambiguator -module Trivial: -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 - diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index b65317cc2..ff724fa6c 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -28,13 +28,11 @@ $(ARCHIVE_OPT): paramodulation.cmx $(LIBRARIES_OPT) $(OCAMLOPT) $(OCAMLARCHIVEOPTIONS) -a -o $@ \ paramodulation.cmx -PARAMOD_OBJS = $(IMPLEMENTATION_FILES:%.ml=%.cmo) \ - saturate_main.cmo -PARAMOD_OBJS_OPT = $(IMPLEMENTATION_FILES:%.ml=%.cmx) \ - saturate_main.cmx - -saturate: $(PARAMOD_OBJS) $(LIBRARIES) - $(OCAMLC) -thread -linkpkg -o $@ $(PARAMOD_OBJS) - -saturate.opt: $(PARAMOD_OBJS_OPT) $(LIBRARIES) - $(OCAMLOPT) -thread -linkpkg -o $@ $(PARAMOD_OBJS_OPT) +PARAMOD_OBJS = $(IMPLEMENTATION_FILES:%.ml=%.cmo) +PARAMOD_OBJS_OPT = $(IMPLEMENTATION_FILES:%.ml=%.cmx) + +LOCALLINKOPTS = -package helm-cic_disambiguation,helm-content_pres,helm-grafite +saturate: saturate_main.ml $(PARAMOD_OBJS) $(LIBRARIES) + $(OCAMLC) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $(PARAMOD_OBJS) $< +saturate.opt: saturate_main.ml $(PARAMOD_OBJS_OPT) $(LIBRARIES) + $(OCAMLOPT) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $(PARAMOD_OBJS_OPT) $< diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index ce4182e1a..69d50e3a0 100644 --- 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 ;; -- 2.39.2