changed META dependency

- disambiguation should (and actually does) depend only on acic_content
- paramodulation does not need disambiguation! (except for a test)

diff --git a/helm/ocaml/METAS/meta.helm-cic_disambiguation.src b/helm/ocaml/METAS/meta.helm-cic_disambiguation.src
index d0a61cd513926b8c674f9f873d49874554bc7869..d2e467aae73a66bdf0a4933427dd80c09bef9c81 100644 (file)
--- 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 6fe6c989833c34e9014eb429eaa71845988db51b..34a25fef0e299f53cd5e7d808bfb82035766d8ff 100644 (file)
--- 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 e69099cb5d30dda0527de4f4403c4e8727de3255..3e6ce26e7c5a56971cd6e1369b516b0eb7daba16 100644 (file)
--- 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 bb506e8dc0dd6fbb3f7e269da49d3c686f41b849..f0ca92db00dc69d18addf9e84d66f9adf49a04cf 100644 (file)
--- 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 b65317cc2c540ed22021701a72632cc74b2d7c3a..ff724fa6c900fb048e92083ae0ac0f1871450e5e 100644 (file)
--- 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 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
 ;;