various updates, removed proofs for now because they are the real bottleneck!!

[helm.git] / helm / ocaml / paramodulation / test_indexing.ml

diff --git a/helm/ocaml/paramodulation/test_indexing.ml b/helm/ocaml/paramodulation/test_indexing.ml
index 2ef07a17cd18a38e2a03cab982d90a71e37dc2ea..0324f9e56b2700120503a83a94c675c2602bacec 100644 (file)
--- a/helm/ocaml/paramodulation/test_indexing.ml
+++ b/helm/ocaml/paramodulation/test_indexing.ml
@@ -140,8 +140,37 @@ let discrimination_tree_test () =
 ;;
 
 
+let test_subst () =
+  let module C = Cic in
+  let module M = CicMetaSubst in
+  let term = C.Appl [
+    C.Rel 1;
+    C.Appl [C.Rel 11;
+            C.Meta (43, []);
+            C.Appl [C.Rel 15; C.Rel 12; C.Meta (41, [])]];
+    C.Appl [C.Rel 11;
+            C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])];
+            C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (12, [])]]
+  ] in
+  let subst1 = [
+    (43, ([], C.Appl [C.Rel 15; C.Meta (10, []); C.Meta (11, [])], C.Rel 16));
+    (10, ([], C.Rel 12, C.Rel 16));
+    (12, ([], C.Meta (41, []), C.Rel 16))
+  ]
+  and subst2 = [
+    (43, ([], C.Appl [C.Rel 15; C.Rel 12; C.Meta (11, [])], C.Rel 16));
+    (10, ([], C.Rel 12, C.Rel 16));
+    (12, ([], C.Meta (41, []), C.Rel 16))
+  ] in
+  let t1 = M.apply_subst subst1 term
+  and t2 = M.apply_subst subst2 term in
+  Printf.printf "t1 = %s\nt2 = %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2);
+;;
+
+
 (* differing ();; *)
 (* next_after ();; *)
-discrimination_tree_test ();;
+(* discrimination_tree_test ();; *)
 (* path_indexing_test ();; *)
+test_subst ();;