X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Ftest_indexing.ml;h=0324f9e56b2700120503a83a94c675c2602bacec;hb=e67aacd065c5f2bb90dc6b07850b4f4c2bc865fc;hp=2ef07a17cd18a38e2a03cab982d90a71e37dc2ea;hpb=969fb8763a6d4afb88aef1eaa4a4d1ce7d626264;p=helm.git

diff --git a/helm/ocaml/paramodulation/test_indexing.ml b/helm/ocaml/paramodulation/test_indexing.ml
index 2ef07a17c..0324f9e56 100644
--- 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 ();;