some makefile work

diff --git a/helm/ocaml/Makefile.common.in b/helm/ocaml/Makefile.common.in
index da539d460f3a4d9c2790bee888656df145797bf5..2dc345235a59af72613cfc7935b3e1b4cb1c0d7e 100644 (file)
--- a/helm/ocaml/Makefile.common.in
+++ b/helm/ocaml/Makefile.common.in
@@ -1,3 +1,5 @@
+H=@
+
 # This Makefile must be included by another one defining:
 #  $PACKAGE
 #  $PREDICATES
@@ -29,11 +31,13 @@ OCAMLOPT_P4 = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(SYNTAXOPTIONS)
 
 LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
 LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
-LIBRARIES_DEPS = $(foreach X,$(LIBRARIES),$(wildcard \
-       $(shell dirname $(X))/*.mli \
-       $(shell dirname $(X))/*.ml \
-       $(shell dirname $(X))/*/*.ml \
-       $(shell dirname $(X))/*/*.mli))
+LIBRARIES_DEPS = \
+       $(foreach X,$(filter-out /usr/lib/ocaml%,$(LIBRARIES)),\
+               $(wildcard \
+                       $(shell dirname $(X))/*.mli \
+                       $(shell dirname $(X))/*.ml \
+                       $(shell dirname $(X))/paramodulation/*.ml \
+                       $(shell dirname $(X))/paramodultation/*.mli))
 
 
 ARCHIVE = $(PACKAGE).cma
@@ -44,20 +48,22 @@ OBJECTS_TO_INSTALL = $(ARCHIVE) $(ARCHIVE_OPT) $(ARCHIVE_OPT:%.cmxa=%.a) \
 DEPEND_FILES = $(INTERFACE_FILES) $(IMPLEMENTATION_FILES)
 
 $(ARCHIVE): $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(LIBRARIES)
-       @if [ $(PACKAGE) != dummy ]; then \
-       echo OCAMLC $@;\
+       $(H)if [ $(PACKAGE) != dummy ]; then \
+       echo "  OCAMLC -a $@";\
        $(OCAMLC) $(OCAMLARCHIVEOPTIONS) -a -o $@ \
                $(IMPLEMENTATION_FILES:%.ml=%.cmo); fi
 
 $(ARCHIVE_OPT): $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(LIBRARIES_OPT)
-       @if [ $(PACKAGE) != dummy ]; then \
-       echo OCAMLOPT $@;\
+       $(H)if [ $(PACKAGE) != dummy ]; then \
+       echo "  OCAMLOPT -a $@";\
        $(OCAMLOPT) $(OCAMLARCHIVEOPTIONS) -a -o $@ \
                $(IMPLEMENTATION_FILES:%.ml=%.cmx); fi
 
 prereq: $(PREREQ)
 all: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(ARCHIVE)
+       @echo -n 
 opt: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(ARCHIVE_OPT)
+       @echo -n 
 world: all opt
 test: test.ml $(ARCHIVE)
        $(OCAMLC) $(ARCHIVE) -linkpkg -o $@ $<
@@ -74,14 +80,14 @@ $(PACKAGE).ps: .dep.dot
        ocamldot < .depend > $@
 
 %.cmi: %.mli
-       @echo OCAMLC $<
-       @$(OCAMLC) -c $<
+       @echo "  OCAMLC $<"
+       $(H)$(OCAMLC) -c $<
 %.cmo %.cmi: %.ml
-       @echo OCAMLC $<
-       @$(OCAMLC) -c $<
+       @echo "  OCAMLC $<"
+       $(H)$(OCAMLC) -c $<
 %.cmx: %.ml
-       @echo OCAMLOPT $<
-       @$(OCAMLOPT) -c $<
+       @echo "  OCAMLOPT $<"
+       $(H)$(OCAMLOPT) -c $<
 %.annot: %.ml
        $(OCAMLC) -dtypes $(PKGS) -c $<
 %.ml %.mli: %.mly

diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in
index 19624a460bccead111f99450e2a4682d38d04558..2b1783b3ce852202bcebdef260a8ae7279f37ea6 100644 (file)
--- a/helm/ocaml/Makefile.in
+++ b/helm/ocaml/Makefile.in
@@ -57,14 +57,19 @@ distclean: clean clean_metas
 .PHONY: all opt world metas depend install uninstall clean clean_metas distclean
 
 %.all:
-       @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* all
+       @echo building module: $*
+       @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* all --no-print-directory
 %.opt:
-       @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* opt
+       @echo building module: $*
+       @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* opt --no-print-directory
 %.clean:
-       @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* clean
+       @echo cleaning module: $*
+       @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* clean --no-print-directory
 %.depend:
-       @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* depend
+       @echo calculating dependencies for module: $*
+       @OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* depend --no-print-directory
 %.stats:
+       @echo generating stats for module: $*
        @$(MAKE) -C $* .stats
 
 $(MODULES:%=%.install):

diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile
index 729590da59a7d9b138495c5baeb1d9a060e9d847..9c231dd873950690d04ff72ad266c7d95dcd346d 100644 (file)
--- a/helm/ocaml/cic_disambiguation/Makefile
+++ b/helm/ocaml/cic_disambiguation/Makefile
@@ -19,9 +19,12 @@ include ../Makefile.common
 OCAMLARCHIVEOPTIONS += -linkall
 
 disambiguateTypes.cmi: disambiguateTypes.mli
-       $(OCAMLC) -c -rectypes $<
+       @echo "  OCAMLC -rectypes $<"
+       @$(OCAMLC) -c -rectypes $<
 disambiguateTypes.cmo: disambiguateTypes.ml disambiguateTypes.cmi
-       $(OCAMLC) -c -rectypes $<
+       @echo "  OCAMLC -rectypes $<"
+       @$(OCAMLC) -c -rectypes $<
 disambiguateTypes.cmx: disambiguateTypes.ml disambiguateTypes.cmi
-       $(OCAMLOPT) -c -rectypes $<
+       @echo "  OCAMLOPT -rectypes $<"
+       @$(OCAMLOPT) -c -rectypes $<
 

diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile
index 28462e58e5140d8f98ac0c1c1c3abedbce79ef50..c81573f5175cbe1ce578bbbf0f488a973bdf0114 100644 (file)
--- a/helm/ocaml/cic_proof_checking/Makefile
+++ b/helm/ocaml/cic_proof_checking/Makefile
@@ -32,11 +32,14 @@ all: all_utilities
 opt: opt_utilities
 
 all_utilities:
-       $(MAKE) -C utilities/ all
+       @echo "  building: utilities"
+       @$(MAKE) -C utilities/ all --no-print-directory
 opt_utilities:
-       $(MAKE) -C utilities/ opt
+       @echo "  building: utilities"
+       @$(MAKE) -C utilities/ opt --no-print-directory
 
 clean: clean_utilities
 clean_utilities:
-       $(MAKE) -C utilities/ clean
+       @echo "  cleaning: utilities"
+       @$(MAKE) -C utilities/ clean --no-print-directory
 

diff --git a/helm/ocaml/cic_proof_checking/utilities/Makefile b/helm/ocaml/cic_proof_checking/utilities/Makefile
index 2cd98f894b65c3b9952b92c04332d640e0a70fcd..174546634a91bf2181bb0718513332c80c049347 100644 (file)
--- a/helm/ocaml/cic_proof_checking/utilities/Makefile
+++ b/helm/ocaml/cic_proof_checking/utilities/Makefile
@@ -5,11 +5,15 @@ LIBS = helm-cic_proof_checking
 OCAMLC = ocamlfind ocamlc $(LINKOPTS) -package $(LIBS)
 OCAMLOPT = ocamlfind opt $(LINKOPTS) -package $(LIBS)
 all: $(UTILITIES)
+       @echo -n
 opt: $(UTILITIES_OPT)
+       @echo -n
 %: %.ml
-       $(OCAMLC) -o $@ $<
+       @echo "    OCAMLC $<"
+       @$(OCAMLC) -o $@ $<
 %.opt: %.ml
-       $(OCAMLOPT) -o $@ $<
+       @echo "    OCAMLOPT $<"
+       @$(OCAMLOPT) -o $@ $<
 clean:
        rm -f $(UTILITIES) $(UTILITIES_OPT) *.cm[iox] *.o
 

diff --git a/helm/ocaml/content_pres/Makefile b/helm/ocaml/content_pres/Makefile
index 642e3ce0e4b4f20b8bc36999c124560bb1d0db92..459b793f0fc497db3dd6c483d1b3f36d490fb653 100644 (file)
--- a/helm/ocaml/content_pres/Makefile
+++ b/helm/ocaml/content_pres/Makefile
@@ -27,7 +27,8 @@ clean: clean_tests
 LOCAL_LINKOPTS = -package helm-content_pres -linkpkg
 test: test_lexer
 test_lexer: test_lexer.ml $(PACKAGE).cma
-       $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
+       @echo "  OCAMLC $<"
+       @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
 
 clean_tests:
        rm -f test_lexer{,.opt}

diff --git a/helm/ocaml/grafite_parser/Makefile b/helm/ocaml/grafite_parser/Makefile
index 4b04b597ee4917f19c9160c32d69b3321e758eb5..25896da87d32039ba5c95774d3a89af9d8e85840 100644 (file)
--- a/helm/ocaml/grafite_parser/Makefile
+++ b/helm/ocaml/grafite_parser/Makefile
@@ -33,10 +33,13 @@ clean_tests:
 LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg
 test: test_parser print_grammar test_dep
 test_parser: test_parser.ml $(PACKAGE).cma
-       $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
+       @echo "  OCAMLC $<"
+       @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
 print_grammar: print_grammar.ml $(PACKAGE).cma
-       $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
+       @echo "  OCAMLC $<"
+       @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
 test_dep: test_dep.ml $(PACKAGE).cma
-       $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
+       @echo "  OCAMLC $<"
+       @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
 
 include ../Makefile.common

diff --git a/helm/ocaml/metadata/Makefile b/helm/ocaml/metadata/Makefile
index 29ca2d3bce9862f90f841ea1c04387fb7fdb9cb6..80dc4133ec8df144beacc4dbb5f09ea44e849c06 100644 (file)
--- a/helm/ocaml/metadata/Makefile
+++ b/helm/ocaml/metadata/Makefile
@@ -18,20 +18,26 @@ all: all_table_creator all_extractor
 opt: opt_table_creator opt_extractor
 
 all_table_creator:
-       make -C table_creator/ all
+       @echo "  building: table_creator"
+       @make -C table_creator/ all --no-print-directory
 opt_table_creator:
-       make -C table_creator/ opt
+       @echo "  building: table_creator"
+       @make -C table_creator/ opt --no-print-directory
 
 all_extractor:
-       make -C extractor/ all
+       @echo "  building: extractor"
+       @make -C extractor/ all --no-print-directory
 opt_extractor:
-       make -C extractor/ opt
+       @echo "  building: extractor"
+       @make -C extractor/ opt --no-print-directory
 
 clean: clean_table_creator clean_extractor
 
 clean_table_creator:
-       make -C table_creator/ clean
+       @echo "  cleaning: table_creator"
+       @make -C table_creator/ clean --no-print-directory
        
 clean_extractor:
-       make -C extractor/ clean
+       @echo "  cleaning: extractor"
+       @make -C extractor/ clean --no-print-directory
        

diff --git a/helm/ocaml/metadata/extractor/Makefile b/helm/ocaml/metadata/extractor/Makefile
index e58064b4159f322148772bf8e62f77300d48b9c4..7c2aec0e555e316822d111bf4f3d93cf0a669ff7 100644 (file)
--- a/helm/ocaml/metadata/extractor/Makefile
+++ b/helm/ocaml/metadata/extractor/Makefile
@@ -1,25 +1,31 @@
 OCAMLFIND=ocamlfind
 
 all: extractor extractor_manager 
+       @echo -n
 opt: extractor.opt extractor_manager.opt
+       @echo -n
 
 clean:
        rm -f *.cm[ixo] *.[ao] extractor extractor.opt *.err *.out extractor_manager extractor_manager.opt
 
 extractor: extractor.ml
-       $(OCAMLFIND) ocamlc \
+       @echo "    OCAMLC $<"
+       @$(OCAMLFIND) ocamlc \
                -thread -package mysql,helm-metadata -linkpkg -o $@ $<
 
 extractor.opt: extractor.ml
-       $(OCAMLFIND) ocamlopt \
+       @echo "    OCAMLOPT $<"
+       @$(OCAMLFIND) ocamlopt \
                -thread -package mysql,helm-metadata -linkpkg -o $@ $<
 
 extractor_manager: extractor_manager.ml
-       $(OCAMLFIND) ocamlc \
+       @echo "    OCAMLC $<"
+       @$(OCAMLFIND) ocamlc \
                -thread -package mysql,helm-metadata -linkpkg -o $@ $<
 
 extractor_manager.opt: extractor_manager.ml
-       $(OCAMLFIND) ocamlopt \
+       @echo "    OCAMLOPT $<"
+       @$(OCAMLFIND) ocamlopt \
                -thread -package mysql,helm-metadata -linkpkg -o $@ $<
 
 export: extractor.opt extractor_manager.opt

diff --git a/helm/ocaml/metadata/table_creator/Makefile b/helm/ocaml/metadata/table_creator/Makefile
index cb8ab763672186e6c6097f34d31cfa5f15e53dc3..06335681c0db4f7b5e3f220d5796150f17c56292 100644 (file)
--- a/helm/ocaml/metadata/table_creator/Makefile
+++ b/helm/ocaml/metadata/table_creator/Makefile
@@ -8,21 +8,25 @@ EXTRA_OBJECTS_TO_CLEAN = \
        table_creator table_creator.opt table_destructor table_destructor.opt
 
 all: table_creator table_destructor
+       @echo -n
 opt: table_creator.opt table_destructor.opt
+       @echo -n
 
 table_creator: table_creator.ml ../metadata.cma
-       $(OCAMLFIND) ocamlc \
+       @echo "    OCAMLC $<"
+       @$(OCAMLFIND) ocamlc \
                -thread -package mysql,helm-metadata -linkpkg -o $@ $<
 
 table_destructor: table_creator
-       ln -f $< $@
+       @ln -f $< $@
 
 table_creator.opt: table_creator.ml ../metadata.cmxa
-       $(OCAMLFIND) ocamlopt \
+       @echo "    OCAMLOPT $<"
+       @$(OCAMLFIND) ocamlopt \
                -thread -package mysql,helm-metadata -linkpkg -o $@ $<
 
 table_destructor.opt: table_creator.opt
-       ln  -f $< $@
+       @ln  -f $< $@
 
 clean:
        rm -f *.cm[iox] *.a *.o

diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend
index dd623b9ae7c560c662bd7b2851086319c209ec9b..6ad9ccf254888c31324e049aeb9266f85416346d 100644 (file)
--- a/helm/ocaml/tactics/.depend
+++ b/helm/ocaml/tactics/.depend
@@ -6,7 +6,6 @@ proofEngineStructuralRules.cmi: proofEngineTypes.cmi
 primitiveTactics.cmi: proofEngineTypes.cmi 
 metadataQuery.cmi: proofEngineTypes.cmi 
 paramodulation/inference.cmi: proofEngineTypes.cmi 
-paramodulation/indexing.cmi: proofEngineTypes.cmi 
 paramodulation/saturation.cmi: proofEngineTypes.cmi 
 variousTactics.cmi: proofEngineTypes.cmi 
 autoTactic.cmi: proofEngineTypes.cmi 
@@ -51,22 +50,22 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     hashtbl_equiv.cmi metadataQuery.cmi 
 metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
     hashtbl_equiv.cmx metadataQuery.cmi 
-paramodulation/utils.cmo: paramodulation/utils.cmi 
-paramodulation/utils.cmx: paramodulation/utils.cmi 
+paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi 
+paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi 
 paramodulation/inference.cmo: proofEngineReduction.cmi proofEngineHelpers.cmi \
     metadataQuery.cmi paramodulation/inference.cmi 
 paramodulation/inference.cmx: proofEngineReduction.cmx proofEngineHelpers.cmx \
     metadataQuery.cmx paramodulation/inference.cmi 
 paramodulation/equality_indexing.cmo: paramodulation/equality_indexing.cmi 
 paramodulation/equality_indexing.cmx: paramodulation/equality_indexing.cmi 
-paramodulation/indexing.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
-    paramodulation/indexing.cmi 
-paramodulation/indexing.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
-    paramodulation/indexing.cmi 
-paramodulation/saturation.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \
-    primitiveTactics.cmi paramodulation/saturation.cmi 
-paramodulation/saturation.cmx: proofEngineTypes.cmx proofEngineReduction.cmx \
-    primitiveTactics.cmx paramodulation/saturation.cmi 
+paramodulation/indexing.cmo: paramodulation/indexing.cmi 
+paramodulation/indexing.cmx: paramodulation/indexing.cmi 
+paramodulation/saturation.cmo: reductionTactics.cmi proofEngineTypes.cmi \
+    proofEngineReduction.cmi primitiveTactics.cmi \
+    paramodulation/saturation.cmi 
+paramodulation/saturation.cmx: reductionTactics.cmx proofEngineTypes.cmx \
+    proofEngineReduction.cmx primitiveTactics.cmx \
+    paramodulation/saturation.cmi 
 variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
     proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
     variousTactics.cmi 

diff --git a/helm/ocaml/tactics/paramodulation/Makefile b/helm/ocaml/tactics/paramodulation/Makefile
index 880b959533c805b0a539c52a2b5cf6595cf2bb05..ba8bd40aa8e0d66590c475ce4bade1ba607aafd0 100644 (file)
--- a/helm/ocaml/tactics/paramodulation/Makefile
+++ b/helm/ocaml/tactics/paramodulation/Makefile
@@ -5,12 +5,16 @@ LOCALLINKOPTS = -package helm-cic_disambiguation,helm-content_pres,helm-grafite,
 include ../../Makefile.common
 
 all $(PACKAGE).cma :saturate 
+       @echo -n
 opt $(PACKAGE).cmxa:saturate.opt
+       @echo -n
 
 saturate: saturate_main.ml $(LIBRARIES)
-       $(OCAMLC) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $<
+       @echo "  OCAMLC $<"
+       @$(OCAMLC) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $<
 saturate.opt: saturate_main.ml $(LIBRARIES)
-       $(OCAMLOPT) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $<
+       @echo "  OCAMLOPT $<"
+       @$(OCAMLOPT) $(LOCALLINKOPTS) -thread -linkpkg -o $@ $<
 
 clean:
        rm -f saturate saturate.opt

diff --git a/helm/ocaml/tactics/paramodulation/indexing.ml b/helm/ocaml/tactics/paramodulation/indexing.ml
index 207fb94338b64e37b078c9cc1de6a77e94edf3ce..8ffde4bdf14569fb22706538151d3554c3af77ec 100644 (file)
--- a/helm/ocaml/tactics/paramodulation/indexing.ml
+++ b/helm/ocaml/tactics/paramodulation/indexing.ml
@@ -130,7 +130,6 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   let cmp = !Utils.compare_terms in
-  ignore(CicTypeChecker.type_of_aux' metasenv context term);
   let check = match termty with C.Implicit None -> false | _ -> true in
   function
     | [] -> None
@@ -157,7 +156,8 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
                   raise e
                | CicUtil.Meta_not_found _ as exn ->
-                   prerr_endline "siam qua"; raise exn
+                   prerr_endline "zurg"; 
+                   raise exn
             in
             Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
                   (candidate, eq_URI))
@@ -354,7 +354,7 @@ let rec demodulation_aux ?(typecheck=false)
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
-  let candidates = get_candidates Matching table term in
+  let candidates = get_candidates Matching table term  in
   match term with
   | C.Meta _ -> None
   | term ->
@@ -546,6 +546,19 @@ let rec demodulation_equality newmeta env table sign target =
     in
     !maxmeta, res
   in
+  let _ =
+    try
+      CicTypeChecker.type_of_aux' metasenv' context left ugraph;
+      CicTypeChecker.type_of_aux' metasenv' context right ugraph;
+    with 
+       CicUtil.Meta_not_found _ as exn ->
+         begin
+           prerr_endline "siamo in demodulation_equality 1"; 
+           prerr_endline (CicPp.ppterm left);
+            prerr_endline (CicPp.ppterm right);
+           raise exn
+         end 
+  in
   let res = demodulation_aux metasenv' context ugraph table 0 left in
   let newmeta, newtarget = 
     match res with
@@ -949,7 +962,8 @@ let rec demodulation_goal newmeta env table goal =
       bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
     in
     let m = Inference.metas_of_term newterm in
-    let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv')in
+    (* QUA *)
+    let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (menv @ menv')in
     !maxmeta, (newproof, newmetasenv, newterm)
   in  
   let res =

diff --git a/helm/ocaml/tactics/paramodulation/saturation.ml b/helm/ocaml/tactics/paramodulation/saturation.ml
index 07fbaa41c5a2e5b0a6c35557bcbfccbfaa561e7b..9c4dce4603cd055d9db0709beb7d2ad18caaceeb 100644 (file)
--- a/helm/ocaml/tactics/paramodulation/saturation.ml
+++ b/helm/ocaml/tactics/paramodulation/saturation.ml
@@ -483,6 +483,22 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
   
   let demodulate table current = 
     let newmeta, newcurrent =
+      let _ =
+        let w, proof, (eq_ty, left, right, order), metas, args = current in
+       let metasenv, context, ugraph = env in
+       let metasenv' = metasenv @ metas in
+       try
+         CicTypeChecker.type_of_aux' metasenv' context left ugraph;
+         CicTypeChecker.type_of_aux' metasenv' context right ugraph;
+       with 
+           CicUtil.Meta_not_found _ as exn ->
+             begin
+               prerr_endline "siamo in forward_simplify"; 
+               prerr_endline (CicPp.ppterm left);
+               prerr_endline (CicPp.ppterm right);
+               raise exn
+             end 
+      in
       Indexing.demodulation_equality !maxmeta env table sign current in
     maxmeta := newmeta;
     if is_identity env newcurrent then
@@ -568,6 +584,22 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   
   let demodulate sign table target =
     let newmeta, newtarget =
+      let _ =
+        let w, proof, (eq_ty, left, right, order), metas, args = target in
+       let metasenv, context, ugraph = env in
+       let metasenv' = metasenv @ metas in
+       try
+         CicTypeChecker.type_of_aux' metasenv' context left ugraph;
+         CicTypeChecker.type_of_aux' metasenv' context right ugraph;
+       with 
+           CicUtil.Meta_not_found _ as exn ->
+             begin
+               prerr_endline "siamo in forward_simplify_new"; 
+               prerr_endline (CicPp.ppterm left);
+               prerr_endline (CicPp.ppterm right);
+               raise exn
+             end 
+      in
       Indexing.demodulation_equality !maxmeta env table sign target in
     maxmeta := newmeta;
     newtarget

diff --git a/helm/ocaml/thread/Makefile b/helm/ocaml/thread/Makefile
index 24a96b6e988de3c516e141b85b89d68ff4fbe3e7..db722abaa32435f5cbd14835903e251063c7f8fe 100644 (file)
--- a/helm/ocaml/thread/Makefile
+++ b/helm/ocaml/thread/Makefile
@@ -9,14 +9,17 @@ opt: thread_fake.cmxa
 include ../Makefile.common
 
 fake/threadSafe.cmi: fake/threadSafe.mli
-       cd fake/        \
+       @echo "  OCAMLC $<"
+       @cd fake/       \
                && ocamlfind ocamlc -c threadSafe.mli
 thread_fake.cma: fake/threadSafe.cmi
-       cd fake/        \
+       @echo "  OCAMLC -a $@"
+       @cd fake/       \
                && ocamlfind ocamlc -a -o $@ threadSafe.ml      \
                && cp $@ ../
 thread_fake.cmxa: fake/threadSafe.cmi
-       cd fake/        \
+       @echo "  OCAMLOPT -a $@"
+       @cd fake/       \
                && ocamlfind opt -a -o $@ threadSafe.ml \
                && cp $@ ../
 

diff --git a/helm/ocaml/utf8_macros/Makefile b/helm/ocaml/utf8_macros/Makefile
index 018f58cefffa3a58efe6d193c47b6c7fe33f4bc1..952b9f597c3fd13dca2490975c9f7a85acfc35b7 100644 (file)
--- a/helm/ocaml/utf8_macros/Makefile
+++ b/helm/ocaml/utf8_macros/Makefile
@@ -11,17 +11,21 @@ EXTRA_OBJECTS_TO_CLEAN =
 all: utf8_macros.cma pa_unicode_macro.cma
 
 make_table: make_table.ml
-       $(OCAMLFIND) ocamlc -package $(MAKE_TABLE_PACKAGES) -linkpkg -o $@ $^
+       @echo "  OCAMLC $<"
+       @$(OCAMLFIND) ocamlc -package $(MAKE_TABLE_PACKAGES) -linkpkg -o $@ $^
 
 utf8MacroTable.ml:
        ./make_table $@
 utf8MacroTable.cmo: utf8MacroTable.ml
-       $(OCAMLFIND) ocamlc -c $<
+       @echo "  OCAMLC $<"
+       @$(OCAMLFIND) ocamlc -c $<
 
 pa_unicode_macro.cmo: pa_unicode_macro.ml utf8Macro.cmo
-       $(OCAMLFIND) ocamlc -package camlp4 -pp "camlp4o q_MLast.cmo pa_extend.cmo -loc loc" -c $<
+       @echo "  OCAMLC $<"
+       @$(OCAMLFIND) ocamlc -package camlp4 -pp "camlp4o q_MLast.cmo pa_extend.cmo -loc loc" -c $<
 pa_unicode_macro.cma: utf8MacroTable.cmo utf8Macro.cmo pa_unicode_macro.cmo
-       $(OCAMLFIND) ocamlc -a -o $@ $^
+       @echo "  OCAMLC -a $@"
+       @$(OCAMLFIND) ocamlc -a -o $@ $^
 
 .PHONY: test
 test: test.ml