diff --git a/lib/dune b/lib/dune
index aa69dad..42fe277 100644
--- a/lib/dune
+++ b/lib/dune
@@ -11,32 +11,32 @@
  (inline_tests)
  (wrapped false)
  (preprocess
-  (pps GT.ppx GT.ppx_all ppx_expect ppx_inline_test)))
+  (pps
+   OCanren-ppx.ppx_repr
+   OCanren-ppx.ppx_fresh
+   OCanren-ppx.ppx_distrib
+   GT.ppx
+   GT.ppx_all
+   ppx_expect
+   ppx_inline_test)))
 
 (library
- (name relational_interpreter_oc_tests)
- (modules relational_interpreter_oc_tests)
- (flags (-rectypes))
- (libraries
-  relational_semantic_interpreter_oc
-  relational_interpreter_oc_tests_f)
- (inline_tests)
- (wrapped false)
- (preprocess
-  (pps ppx_expect ppx_inline_test)))
-
-(library
- (name relational_interpreter_oc_tests_f)
- (modules relational_interpreter_oc_tests_f)
- (flags (-rectypes))
- (libraries OCanren OCanren.tester relational_semantic_interpreter_oc)
+ (name relational_semantic_interpreter)
+ (modules relational_semantic_interpreter)
+ (flags
+  ; (-dsource)
+  (:standard -rectypes))
+ (libraries OCanren OCanren.tester)
  (preprocessor_deps ./pp5+gt+plugins+ocanren+dump.exe)
+ ; (inline_tests)
  (wrapped false)
  (preprocess
   (pps
    OCanren-ppx.ppx_repr
    OCanren-ppx.ppx_deriving_reify
    OCanren-ppx.ppx_fresh
+   ppx_expect
+   ppx_inline_test
    GT.ppx
    GT.ppx_all
    OCanren-ppx.ppx_distrib
@@ -52,12 +52,15 @@
   (:standard -rectypes))
  (libraries OCanren OCanren.tester)
  (preprocessor_deps ./pp5+gt+plugins+ocanren+dump.exe)
+ (inline_tests)
  (wrapped false)
  (preprocess
   (pps
    OCanren-ppx.ppx_repr
    OCanren-ppx.ppx_deriving_reify
    OCanren-ppx.ppx_fresh
+   ppx_expect
+   ppx_inline_test
    GT.ppx
    GT.ppx_all
    OCanren-ppx.ppx_distrib
@@ -65,6 +68,29 @@
    -pp
    lib/pp5+gt+plugins+ocanren+dump.exe)))
 
+; (library
+;  (name test)
+;  (modules test)
+;  (flags
+;   (-dsource)
+;   (:standard -rectypes))
+;  (libraries OCanren OCanren.tester)
+;  (preprocessor_deps ./pp5+gt+plugins+ocanren+dump.exe)
+;  (wrapped false)
+;  (preprocess
+;   (pps
+;    ppx_expect
+;    ppx_inline_test
+;    GT.ppx
+;    GT.ppx_all
+;    OCanren-ppx.ppx_repr
+;    OCanren-ppx.ppx_deriving_reify
+;    OCanren-ppx.ppx_fresh
+;    OCanren-ppx.ppx_distrib
+;    --
+;    -pp
+;    lib/pp5+gt+plugins+ocanren+dump.exe)))
+
 (rule
  (targets pp5+gt+plugins+ocanren+dump.exe)
  (action
diff --git a/lib/relational_interpreter_oc_tests.ml b/lib/relational_interpreter_oc_tests.ml
deleted file mode 100644
index c888c92..0000000
--- a/lib/relational_interpreter_oc_tests.ml
+++ /dev/null
@@ -1,61 +0,0 @@
-open Relational_interpreter_oc_tests_f
-open Relational_semantic_interpreter_oc
-open Relational
-
-let%expect_test "inv id: test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}]
-let%expect_test "some test" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}]
-let%expect_test "some test" = print_endline (inv_id_t3 ()); [%expect {| [S (O)] |}]
-let%expect_test "some test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}]
-let%expect_test "some test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}]
-let%expect_test "some test" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}]
-let%expect_test "some test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}]
-let%expect_test "some test" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Unit], S (S (O)), [O])] |}]
-let%expect_test "some test" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Bot], S (S (O)), [S (O)])] |}]
-let%expect_test "some test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Unit], S (S (O)), [S (O); O])] |}]
-let%expect_test "some test" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, O)], [Bot], S (O), [])] |}]
-let%expect_test "some test" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Bot], S (S (O)), [])] |}]
-let%expect_test "some test" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Unit], S (S (O)), [])] |}]
-let%expect_test "some test" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Bot], S (S (O)), [])] |}]
-let%expect_test "some test" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Bot], S (S (O)), [])] |}]
-let%expect_test "some test" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, O)], [Unit], S (O), [O])] |}]
-let%expect_test "some test" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, O)], [Bot], S (O), [O])] |}]
-let%expect_test "some test" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, S (O))], [Bot; Unit], S (S (O)), [O])] |}]
-let%expect_test "some test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}]
-let%expect_test "some test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}]
-let%expect_test "some test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}]
-let%expect_test "some test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "some test" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "some test" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "some test" = print_endline (fun_eval_t3 ()); [%expect {| [] |}]
-let%expect_test "some test" = print_endline (fun_eval_t4 ()); [%expect {| [] |}]
-let%expect_test "some test" = print_endline (fun_eval_t5 ()); [%expect {| [] |}]
-let%expect_test "some test" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "some test" = print_endline (prog_eeal_t2 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "some test" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "some test" = print_endline (prog_eval_t4 ()); [%expect {| [] |}]
-let%expect_test "some test" = print_endline (synt_t1 ()); [%expect {| [Val] |}]
-let%expect_test "some test" = print_endline (synt_t2 ()); [%expect {| [Ref; Val] |}]
-let%expect_test "some test" = print_endline (synt_t3 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}]
-let%expect_test "some test" = print_endline (synt_t4 ()); [%expect {| [[Val]] |}]
-let%expect_test "some test" = print_endline (synt_t5 ()); [%expect {| [[Ref; Ref]; [Ref; Val]; [Val; Ref]; [Val; Val]] |}]
-let%expect_test "some test" = print_endline (synt_t6 ()); [%expect {| [[Ref; Ref]; [Val; Ref]; [Ref; Val]; [Val; Val]] |}]
-let%expect_test "some test" = print_endline (synt_t7 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}]
-let%expect_test "some test" = print_endline (synt_t8 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}]
-(* TODO: test with assymetric args order *)
-(* TODO: tests names *)
-
-let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Ref] |}]
-let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}]
-let%expect_test "Stmt type test (2)" = print_endline (Stmt.Test.test2 ()); [%expect {| [Call (S (O), [S (S (O))])] |}]
-let%expect_test "FunDecl type test" = print_endline (FunDecl.Test.test ()); [%expect {| [FunDecl ([Ref; Val], [Call (S (O), [O]); Write (S (O))])] |}]
-let%expect_test "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Val], [Write (O); Read (O)]))] |}]
-let%expect_test "Arg type test" = print_endline (Arg.Test.test ()); [%expect {| [LValue (S (S (S (O))))] |}]
-let%expect_test "Value type test" = print_endline (Value.Test.test ()); [%expect {| [Bot; Unit] |}]
-let%expect_test "St type test" = print_endline (St.Test.test ()); [%expect {| [St ([(O, O)], [Bot], S (O), [O])] |}]
-
-
-
-
-
-
-
diff --git a/lib/relational_interpreter_oc_tests_f.ml b/lib/relational_interpreter_oc_tests_f.ml
deleted file mode 100644
index f33e1e5..0000000
--- a/lib/relational_interpreter_oc_tests_f.ml
+++ /dev/null
@@ -1,418 +0,0 @@
-open Relational_semantic_interpreter_oc
-open Relational
-open GT
-open OCanren
-open OCanren.Std
-
-@type answer  = St.ground GT.list with show
-@type answerArgs = (Arg.ground List.ground) GT.list with show
-@type answerValue = Value.ground GT.list with show
-@type answerNat = Nat.ground GT.list with show
-@type answerNats = (Nat.ground List.ground) GT.list with show
-@type answerTag = Tag.ground GT.list with show
-@type answerTags = (Tag.ground List.ground) GT.list with show
-
-let inv_id_t _ = show(answerNat) (Stream.take (run q
-  (fun q -> ocanren { inv_ido 2 1 q })
-  (fun q -> q#reify Nat.prj_exn)))
-
-let inv_id_t2 _ = show(answerNat) (Stream.take (run q
-  (fun q -> ocanren { inv_ido 2 0 q })
-  (fun q -> q#reify Nat.prj_exn)))
-
-let inv_id_t3 _ = show(answerNat) (Stream.take (run q
-  (fun q -> ocanren { inv_ido 2 q 0 })
-  (fun q -> q#reify Nat.prj_exn)))
-
-let list_drop_t _ = show(answerNats) (Stream.take (run q
-  (fun q -> ocanren { list_dropo 2 [1; 2; 3] q })
-  (fun q -> q#reify (List.prj_exn Nat.prj_exn))))
-
-let list_replace_t  _ = show(answerNats) (Stream.take (run q
-  (fun q -> ocanren { list_replaceo [1; 2; 3; 4] 1 0 q })
-  (fun q -> q#reify (List.prj_exn Nat.prj_exn))))
-
-let arg_to_value_t _ = show(answerValue) (Stream.take (run q
-  (fun q -> let open Arg in
-            ocanren {
-    fresh s in
-      empty_stateo s &
-      arg_to_valueo s RValue q })
-  (fun q -> q#reify (Value.prj_exn))))
-
-let st_add_arg_t _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            ocanren {
-    fresh s, s', cnt in
-      empty_stateo s &
-      empty_stateo s' &
-      st_add_argo s  s' Nat.o Val RValue q })
-  (fun q -> q#reify (St.prj_exn))))
-
-let write_eval_t1 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmt in
-      s == St ([Std.pair 1 1; Std.pair 0 0], [Bot; Bot], 2, []) &
-      p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
-      stmt == Write 0 &
-      eval_stmto s p stmt q})
-  (fun q -> q#reify (St.prj_exn))))
-
-let write_eval_t2 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmt in
-      s == St ([Std.pair 1 1; Std.pair 0 0], [Bot; Bot], 2, []) &
-      p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
-      stmt == Write 1 &
-      eval_stmto s p stmt q})
-  (fun q -> q#reify (St.prj_exn))))
-
-let writes_eval_t _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmts in
-      s == St ([Std.pair 1 1; Std.pair 0 0], [Bot; Bot], 2, []) &
-      p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
-      stmts == [Write 0; Write 1] &
-      eval_bodyo s p stmts q})
-  (fun q -> q#reify (St.prj_exn))))
-
-let call_eval_t1 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmt in
-      s == St ([Std.pair 0 0], [Unit], 1, []) &
-      p == [FunDecl ([Ref], [Write 0])] &
-      stmt == Call (0, [0]) &
-      eval_stmto s p stmt q})
-  (fun q -> q#reify (St.prj_exn))))
-
-let call_eval_t2 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmt in
-      s == St ([Std.pair 1 1; Std.pair 0 0], [Unit; Unit], 2, []) &
-      p == [FunDecl ([Ref], [Write 0])] &
-      stmt == Call (0, [0]) &
-      eval_stmto s p stmt q})
-  (fun q -> q#reify (St.prj_exn))))
-
-let call_eval_t3 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmt in
-      s == St ([Std.pair 1 1; Std.pair 0 0], [Unit; Unit], 2, []) &
-      p == [FunDecl ([Ref], [Write 0])] &
-      stmt == Call (0, [1]) &
-      eval_stmto s p stmt q})
-  (fun q -> q#reify (St.prj_exn))))
-
-let call_eval_t4 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmt in
-      s == St ([Std.pair 1 1; Std.pair 0 0], [Unit; Unit], 2, []) &
-      p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
-      stmt == Call (0, [0; 1]) &
-      eval_stmto s p stmt q})
-  (fun q -> q#reify (St.prj_exn))))
-
-let call_eval_t5 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            let open Stmt in
-            let open FunDecl in
-            ocanren {
-    fresh s, p, stmt in
-      s == St ([Std.pair 1 1; Std.pair 0 0], [Unit; Unit], 2, []) &
-      p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
-      stmt == Call (0, [1; 0]) &
-      eval_stmto s p stmt q})
-  (fun q -> q#reify (St.prj_exn))))
-
-let mem_set_t1 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            ocanren {
-    fresh s in
-      s == St ([Std.pair 0 0], [Bot], 1, []) &
-      mem_seto s 0 Unit q})
-  (fun q -> q#reify (St.prj_exn))))
-
-let mem_set_t2 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            ocanren {
-    fresh s in
-      s == St ([Std.pair 0 0], [Unit], 1, []) &
-      mem_seto s 0 Bot q})
-  (fun q -> q#reify (St.prj_exn))))
-
-let meem_set_t3 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            let open Value in
-            let open St in
-            ocanren {
-    fresh s in
-      s == St ([Std.pair 0 1], [Unit; Unit], 2, []) &
-      mem_seto s 0 Bot q})
-  (fun q -> q#reify (St.prj_exn))))
-
-let add_arg_folder_t _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            ocanren {
-    fresh s, s', cnt in
-      empty_stateo s &
-      empty_stateo s' &
-      add_arg_foldero s (Std.pair s' Nat.o) Val RValue (Std.pair q cnt) })
-  (fun q -> q#reify (St.prj_exn))))
-
-let foldl2_t _ = show(answer) (Stream.take (run q
-  (fun q -> let open Arg in
-            let open Tag in
-            ocanren {
-    fresh s, s', cnt, arg_tags, args in
-      arg_tags == [Val] &
-      args == [RValue] &
-      empty_stateo s &
-      empty_stateo s' &
-      list_foldl2o (add_arg_foldero s) (Std.pair s' Nat.o) arg_tags args (Std.pair q cnt) })
-  (fun q -> q#reify (St.prj_exn))))
-
-
-let rvalue_t _ = show(answerArgs) (Stream.take ~n:3 (run q
-  (fun q -> let open Arg in
-            ocanren {fresh v in List.mapo arg_to_rvalueo v q})
-  (fun q -> q#reify (List.prj_exn Arg.prj_exn))))
-
-(* empty state test *)
-let empty_state_t _ = show(answer) (Stream.take (run q
-  (fun q -> ocanren {empty_stateo q})
-  (fun q -> q#reify (St.prj_exn))))
-
-(* fun eval test *)
-let fun_eval_t1 _ = show(answer) (Stream.take (run q
-  (fun q -> (* let open Prog in *)
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren { fresh s, p, d in
-                        empty_stateo s &
-                        p == [] &
-                        d == FunDecl ([], []) &
-                        eval_fun_empty_argso s p d q })
-  (fun q -> q#reify (St.prj_exn))))
-
-(* fun eval test *)
-let fun_eval_t2 _ = show(answer) (Stream.take (run q
-  (fun q -> (* let open Prog in *)
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren { fresh s, p, d in
-                        empty_stateo s &
-                        p == [] &
-                        d == FunDecl ([Val], [Write 0; Read 0]) &
-                        eval_fun_empty_argso s p d q })
-  (fun q -> q#reify (St.prj_exn))))
-
-(* fun eval test *)
-let fun_eval_t3 _ = show(answer) (Stream.take (run q
-  (fun q -> (* let open Prog in *)
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren { fresh s, p, d in
-                        empty_stateo s &
-                        p == [FunDecl ([Ref], [Write 0])] &
-                        d == FunDecl ([Val], [Call (0, [0]); Read 0]) &
-                        eval_fun_empty_argso s p d q })
-  (fun q -> q#reify (St.prj_exn))))
-
-(* fun eval test *)
-let fun_eval_t4 _ = show(answer) (Stream.take (run q
-  (fun q -> (* let open Prog in *)
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren { fresh s, p, d in
-                        empty_stateo s &
-                        p == [FunDecl ([Ref], [Write 0])] &
-                        d == FunDecl ([Val; Val], [Call (0, [1]); Write 0; Read 1]) &
-                        eval_fun_empty_argso s p d q })
-  (fun q -> q#reify (St.prj_exn))))
-
-(* fun eval test *)
-let fun_eval_t5 _ = show(answer) (Stream.take (run q
-  (fun q -> (* let open Prog in *)
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren { fresh s, p, d in
-                        empty_stateo s &
-                        p == [FunDecl ([Ref; Ref], [Write 0; Write 1])] &
-                        d == FunDecl ([Val; Val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]) &
-                        eval_fun_empty_argso s p d q })
-  (fun q -> q#reify (St.prj_exn))))
-
-(* prog eval test *)
-let prog_eval_t1 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren {eval_progo (Prog ([], FunDecl ([Val], [Write 0; Read 0]))) q})
-  (fun q -> q#reify (St.prj_exn))))
-
-(* prog with func eval test *)
-let prog_eeal_t2 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren {eval_progo (Prog ([FunDecl ([Val], [Write 0; Read 0])], FunDecl ([Val], [Write 0; Read 0; Call (0, [0])]))) q})
-  (fun q -> q#reify (St.prj_exn))))
-
-(* prog with func eval test *)
-let prog_eval_t3 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren {eval_progo (Prog ([FunDecl ([Ref], [Write 0; Read 0])], FunDecl ([Val], [Write 0; Read 0; Call (0, [0])]))) q})
-  (fun q -> q#reify (St.prj_exn))))
-
-(* prog with func eval test *)
-let prog_eval_t4 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            ocanren {eval_progo (Prog ([FunDecl ([Ref], [Write 0])], FunDecl ([Val], [Call (0, [0]); Read 0]))) q})
-  (fun q -> q#reify (St.prj_exn))))
-
-(* annotation gen prog test *)
-let synt_t1 _ = show(answerTag) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val], [Call (0, [0]); Read 0]))) (St ([], [], 0, []))})
-  (fun q -> q#reify (Tag.prj_exn))))
-
-(* annotation gen prog test *)
-let synt_t2 _ = show(answerTag) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))})
-  (fun q -> q#reify (Tag.prj_exn))))
-
-(* annotation gen prog test *)
-let synt_t3 _ = show(answerTags) (Stream.take (run qr
-  (fun q r -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))})
-  (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
-
-(* annotation gen prog test *)
-let synt_t4 _ = show(answerTags) (Stream.take (run q
-  (fun q -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val; Val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, []))})
-  (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *)
-
-(* annotation gen prog test *)
-let synt_t5 _ = show(answerTags) (Stream.take (run qr
-  (fun q r -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, []))})
-  (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *)
-
-(* annotation gen prog test *)
-let synt_t6 _ = show(answerTags) (Stream.take (run qr
-  (fun q r -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0])], FunDecl ([Val; Val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, []))})
-  (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) (* all variants *)
-
-(* annotation gen prog test *)
-let synt_t7 _ = show(answerTags) (Stream.take (run qr
-  (fun q r -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], FunDecl ([Val; Val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))})
-  (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
-
-(* annotation gen prog test *)
-let synt_t8 _ = show(answerTags) (Stream.take (run qr
-  (fun q r -> let open Prog in
-            let open FunDecl in
-            let open Tag in
-            let open Stmt in
-            let open St in
-            ocanren {eval_progo (Prog ([FunDecl ([q; r], [Write 0; Write 1])], FunDecl ([Val; Val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, []))})
-  (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
diff --git a/lib/relational_semantic_interpreter.ml b/lib/relational_semantic_interpreter.ml
new file mode 100644
index 0000000..6ab270d
--- /dev/null
+++ b/lib/relational_semantic_interpreter.ml
@@ -0,0 +1,376 @@
+module Relational =
+struct
+  open GT
+  open OCanren
+  open OCanren.Std
+
+  type data_ground = Nat.ground (* with show, gmap *)
+  [@@deriving gt ~options:{ show; gmap }]
+  type data_logic = Nat.logic
+  [@@deriving gt ~options:{ show; gmap }]
+  type data_injected = Nat.injected
+
+  module Tag = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%distrib
+      type nonrec t = Ref | Value
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = t
+    ]
+
+    let ref = inj Ref
+    let value = inj Value
+  end
+
+  module Stmt = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%distrib
+      type nonrec ('d, 'dl) t = Call of 'd * 'dl | Read of 'd | Write of 'd
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = (Nat.ground, Nat.ground List.ground) t
+    ]
+
+    let call f args = inj (Call (f, args))
+    let read id = inj (Read id)
+    let write id = inj (Write id)
+  end
+
+  module Body = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%distrib
+      type nonrec ('stmt, 'l) t = T of ('stmt, 'l) List.t
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = (Stmt.ground, Stmt.ground List.ground) t
+    ]
+
+    let make stmts = inj (T stmts)
+  end
+
+  module FunDecl = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%distrib
+      type nonrec ('l, 'b) t = T of 'l * 'b
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = (Tag.ground List.ground, Body.ground) t
+    ]
+
+    let make args body = inj (T (args, body))
+  end
+
+  module Prog = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%distrib
+      type nonrec ('l, 'f) t = T of 'l * 'f
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = (FunDecl.ground List.ground, FunDecl.ground) t
+    ]
+
+    let make decls main_decl = inj (T (decls, main_decl))
+  end
+
+  module Arg = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%distrib
+      type nonrec 'd t = RValue | LValue of 'd
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = Nat.ground t
+    ]
+
+    let rvalue = inj RValue
+    let lvalue x = inj (LValue x) 
+  end
+
+  module Value = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%distrib
+      type nonrec t = Unit | Bot
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = t
+    ]
+
+    let unit = inj Unit
+    let bot = inj Bot
+  end
+
+  (* module Envr = struct *)
+    (* [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"] *)
+    (* [%%distrib *)
+      (* type nonrec ('d, 'l) t = T of ('d * 'd, 'l) List.t *)
+      (* [@@deriving gt ~options:{ show; gmap }] *)
+      (* type nonrec ground = (Nat.ground, Nat.ground List.ground) t *)
+    (* ] *)
+
+    (* let make elems = inj (T elems) *)
+  (* end *)
+
+  module State = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%distrib
+      type nonrec ('env, 'mem, 'last_mem, 'assignments) t = T of 'env * 'mem * 'last_mem * 'assignments
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = (((Nat.ground, Nat.ground) Pair.ground) List.ground,
+                            Value.ground List.ground, Nat.ground, Nat.ground List.ground) t
+    ]
+
+    let make env mem last_mem assignments = inj (T (env, mem, last_mem, assignments))
+  end
+
+  let rec list_replace xs id value ys =
+    conde
+    [ (xs === Std.nil ()) &&& (ys === Std.nil ()) (* TODO: error *)
+    ; fresh (x xs') (xs === List.cons x xs') (id === Nat.o) (ys === List.cons value xs)
+    ; fresh (x xs' id' ys') (xs === List. cons x xs') (id === Nat.s id') (ys === List.cons x ys')
+                            (list_replace xs' id' value ys')
+    ]
+
+  let rec list_assoc a xs v' =
+    conde
+    [ fresh (a' b' xs')
+      (xs === List.cons (a', b') xs')
+      (a =/= a')
+      (list_assoc a xs' v')
+    ; fresh (a' b' xs')
+      (xs === List.cons (a', b') xs')
+      (a === a')
+      (v' === b')
+    ]
+  (* TODO: difference from List.assoco ?? *)
+
+  let env_get state id mem_id' =
+    fresh (env mem mem_len assignments)
+    (state === State.make env mem mem_len assignments)
+    (list_assoc id env mem_id')
+    (* (List.assoco id env mem_id') *)
+
+  let env_add state id mem_id state' =
+    fresh (env env' mem mem_len assignments)
+    (state === State.make env mem mem_len assignments)
+    (state' === State.make env' mem mem_len assignments)
+    (env' === List.cons (id, mem_id) env)
+
+  let inv_id mem_len id id' =
+    fresh (inv_id_inc)
+    (Nat.addo inv_id_inc id mem_len)
+    (Nat.addo id' (Nat.s Nat.o) inv_id_inc)
+
+  (* --- *)
+
+  let rec list_nth xs id x' =
+   conde
+   [ (xs === Std.nil ()) (* TODO: error *)
+   ; fresh (y' xs') (id === Nat.o) (List.cons y' xs' === xs) (x' === y')
+   ; fresh (id' y' xs') (Nat.s id' === id) (List.cons y' xs' === xs) (list_nth xs' id' x')
+   ]
+
+  (* TODO: use real holes *)
+  let mem_get state id value' =
+    fresh (mem mem_len mem_id mem_id_inv _env _assignments)
+    (state === inj (State.T (_env, mem, mem_len, _assignments)))
+    (env_get state id mem_id)
+    (inv_id mem_len mem_id mem_id_inv)
+    (list_nth mem mem_id_inv value')
+
+  let mem_set state id value state'=
+    fresh (env mem mem_len assignments mem_id inv_mem_id mem' assignments')
+    (state === State.make env mem mem_len assignments)
+    (env_get state id mem_id)
+    (inv_id mem_len mem_id inv_mem_id)
+    (list_replace mem mem_id value mem')
+    (assignments' === List.cons id assignments)
+    (state' === State.make env mem' mem_len assignments')
+
+  let mem_add state value state' =
+    fresh (env mem mem_len mem_len' assignments mem')
+    (state === State.make env mem mem_len assignments)
+    (mem' === List.cons value mem)
+    (mem_len' === Nat.s mem_len)
+    (state' === State.make env mem mem_len' assignments)
+
+  let mem_check state id state' =
+    conde
+    [ (mem_get state id Value.bot) &&& (state' === state)
+    ; (mem_get state id Value.unit) &&& (state' === state)
+    ]
+
+  (* --- *)
+
+  let rec list_foldl f acc xs acc' =
+    conde
+    [ (xs === Std.nil ()) &&& (acc' === acc)
+    ; fresh (x' xs' acc_upd)
+      (xs === List.cons x' xs')
+      (list_foldl f acc xs' acc_upd)
+      (f acc_upd x' acc')
+    ]
+
+
+  let rec list_foldr2 f acc xs ys acc' =
+    conde
+    [ (xs === Std.nil ()) &&& (ys === Std.nil ()) &&& (acc' === acc)
+    ; fresh (x' xs' y' ys' acc_upd)
+      (xs === List.cons x' xs')
+      (ys === List.cons y' ys')
+      (f acc x' y' acc_upd)
+      (list_foldr2 f acc_upd xs' ys' acc')
+    ]
+
+  let rec list_foldl2 f acc xs ys acc' =
+    conde
+    [ (xs === Std.nil ()) &&& (ys === Std.nil ()) &&& (acc' === acc)
+    ; fresh (x' xs' y' ys' acc_upd)
+      (xs === List.cons x' xs')
+      (ys === List.cons y' ys')
+      (list_foldl2 f acc xs' ys' acc_upd)
+      (f acc_upd x' y' acc')
+    ]
+
+  let arg_to_value state arg value' =
+    conde
+    [ (arg === Arg.rvalue) &&& (value' === Value.unit)
+    ; fresh (id) (arg === Arg.lvalue id) (mem_get state id value')
+    ]
+
+  let arg_to_rvalue _arg value' = (value' === inj Arg.RValue)
+
+  let st_mem_len state mem_len' =
+    fresh (_env _mem _assignments) (* TODO: replace with real placeholder ? *)
+    (state === State.make _env _mem mem_len' _assignments)
+
+  let st_add_arg state state_before id arg_tag arg state'' =
+    conde
+    [ (arg_tag === Tag.ref) &&& (arg === Arg.rvalue) &&& (state'' === state)
+      (* TODO: error, TODO: allow later ?? *)
+    ; fresh (arg' value')
+      (arg_tag === Tag.ref)
+      (arg === Arg.lvalue arg')
+      (env_get state_before arg' value')
+      (env_add state id value' state'')
+    ; fresh (value' state' mem_len_dec')
+      (arg_tag === Tag.value)
+      (arg_to_value state_before arg value')
+      (mem_add state value' state')
+      (st_mem_len state (Nat.s mem_len_dec'))
+      (env_add state' id mem_len_dec' state'')
+    ]
+
+  let st_spoil_folder mem_len state mem id mem' =
+    fresh (mem_id' mem_id_inv')
+    (env_get state id mem_id')
+    (inv_id mem_len mem_id' mem_id_inv')
+    (list_replace mem mem_id_inv' (inj Value.Bot) mem')
+
+  let st_spoil_assignments state state' =
+    fresh (env mem mem' mem_len assignments nil')
+    (state === State.make env mem mem_len assignments)
+    (list_foldl (st_spoil_folder mem_len state) mem assignments mem')
+    (* (List.fold_left (fun mem id -> list_replace mem (inv_id mem_len @@ env_get state id) BotV) mem assignments mem') *)
+    (nil' === Std.nil ())
+    (state' === State.make env mem' mem_len nil')
+
+  (* --- *)
+
+  let arg_to_lvalue arg arg' = (arg' === inj (Arg.LValue arg))
+
+  let rec list_drop n xs xs' =
+    conde
+    [ (xs === Std.nil ()) &&& (xs' === Std.nil ())
+    ; n === Nat.o &&& (xs === xs')
+    ; fresh (n' y ys) (Nat.s n' === n) (xs === List.cons y ys) (list_drop n' ys xs')
+    ]
+
+  let rec eval_stmt state prog stmt state' =
+    conde
+    [ fresh (f_id args f args')
+      (stmt === Stmt.call f_id args)
+      (list_nth prog f_id f)
+      (List.mapo arg_to_lvalue args args')
+      (eval_fun state prog f args' state')
+    ; fresh (id) (stmt === Stmt.read id) (mem_check state id state')
+    ; fresh (id) (stmt === Stmt.write id) (mem_set state id Value.unit state')
+    ]
+
+  and eval_body_folder prog state stmt state' = eval_stmt state prog stmt state'
+
+  and eval_body state prog body state' =
+    list_foldl (eval_body_folder prog) state body state' 
+    (* (List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body) *)
+
+  and add_arg_folder state_before state_c arg_tag arg state_c' =
+    fresh (state id state' id')
+    (state_c === inj (state, id))
+    (st_add_arg state state_before id arg_tag arg state')
+    (id' === Nat.s id)
+    (state_c' === inj (state', id'))
+
+  and eval_fun state prog decl args state' =
+    fresh (arg_tags body
+           env_before mem_before len_before assignments_before
+           state_clean
+           state_with_vars _counter
+           state_evaled
+           state_spoiled
+           _env mem_spoiled len _assignments
+           mem_updated len_to_drop
+           nil_env nil_assignments)
+    (nil_env === Std.nil ())
+    (nil_assignments === Std.nil ())
+    (decl === FunDecl.make arg_tags body)
+    (state === State.make env_before mem_before len_before assignments_before)
+    (state_clean === State.make nil_env mem_before len_before nil_assignments)
+    (list_foldl2 (add_arg_folder state) (inj (state, Nat.o)) arg_tags args (inj (state_with_vars, _counter))) (* TODO: replace with real placeholder *)
+    (eval_body state_with_vars prog body state_evaled)
+    (st_spoil_assignments state_evaled state_spoiled)
+    (state_spoiled === State.make _env mem_spoiled len _assignments)
+    (Nat.addo len_to_drop len_before len)
+    (list_drop len_to_drop mem_spoiled mem_updated)
+    (state' === State.make env_before mem_updated len_before assignments_before)
+
+  and eval_fun_empty_args state prog decl state' =
+    fresh (arg_tags args _hole) (* TODO: replace with real placeholder *)
+    (decl === FunDecl.make arg_tags _hole)
+    (List.mapo arg_to_rvalue arg_tags args)
+    (eval_fun state prog decl args state')
+
+  (* --- *)
+
+  let empty_state state =
+    fresh (nil_env nil_mem nil_assignments)
+    (nil_env === Std.nil ())
+    (nil_assignments === Std.nil ())
+    (nil_mem === Std.nil ())
+    (state === State.make nil_env nil_mem Nat.o nil_assignments)
+
+  let eval_prog all_prog state' =
+    fresh (prog main_decl state)
+    (all_prog === Prog.make prog main_decl)
+    (empty_state state)
+    (eval_fun_empty_args state prog main_decl state')
+
+  (* TODO: fix *)
+  (* let eval_prog_fwd all_prog = *)
+    (* Stream.hd @@ *)
+    (* run q (fun q -> eval_prog (inj all_prog) q) *)
+          (* (fun qs -> qs#reify prj_exn) *)
+
+  (* TODO: fix *)
+  (* let empty_prog = (Prog.T (List.Nil, FunDecl.T (List.Nil, Body.T List.Nil))) *)
+  (* let empty_prog = Prog.make (Std.nil ()) (FunDecl.make (Std.nil ()) (Body.make (Std.nil ()))) *)
+
+  (* TODO: fix *)
+  (* let%expect_test "empty" = *)
+    (* eval_prog_fwd empty_prog; *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  let eval_test =
+    Stream.hd @@
+    run q (fun q -> ocanren { List.assoco 0 [(0, 0)] q })
+          (fun qs -> qs#reify Nat.prj_exn)
+
+(* ((show (GT.list) (show Nat.ground)) x *)
+  let%expect_test "empty" =
+    let x = eval_test in
+    Printf.printf "done! %s" ((show (Nat.ground)) x);
+    [%expect {| done! 0 |}]
+
+end
diff --git a/lib/relational_semantic_interpreter_oc.ml b/lib/relational_semantic_interpreter_oc.ml
index 4c8f0bd..aa633cf 100644
--- a/lib/relational_semantic_interpreter_oc.ml
+++ b/lib/relational_semantic_interpreter_oc.ml
@@ -21,8 +21,8 @@ struct
     module Test = struct
       @type answer = logic GT.list with show
 
-      let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == Ref})
-                                                    (fun q -> q#reify reify)))
+      let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> ocanren {q == Ref})
+                                                                       (fun q -> q#reify reify)))
     end
   end
 
@@ -38,11 +38,11 @@ struct
       @type answer = Nat.ground List.ground GT.list with show
       @type answer'  = ground GT.list with show
 
-      let test1 _ = show(answer) (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == Call (1, q)})
-                                                     (fun q -> q#reify (List.prj_exn Nat.prj_exn))))
+      let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == Call (1, q)})
+                                                                       (fun q -> q#reify (List.prj_exn Nat.prj_exn))))
 
-      let test2 _ = show(answer') (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == q})
-                                                      (fun q -> q#reify (prj_exn))))
+      let _ = Printf.printf "%s\n" @@ show(answer') (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == q})
+                                                                        (fun q -> q#reify (prj_exn))))
     end
   end
 
@@ -56,10 +56,10 @@ struct
 
     module Test = struct
       @type answer  = ground GT.list with show
-      let test _ = show(answer) (Stream.take (run q (fun q -> let open Tag in
-                                                              let open Stmt in
-                                                              ocanren {FunDecl ([Ref; Val], [Call (1, [0]); Write 1]) == q})
-                                                    (fun q -> q#reify (prj_exn))))
+      let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> let open Tag in
+                                                                                 let open Stmt in
+                                                                                 ocanren {FunDecl ([Ref; Val], [Call (1, [0]); Write 1]) == q})
+                                                                       (fun q -> q#reify (prj_exn))))
     end
   end
 
@@ -73,11 +73,11 @@ struct
 
     module Test = struct
       @type answer  = ground GT.list with show
-      let test _ = show(answer) (Stream.take (run q (fun q -> let open FunDecl in
-                                                              let open Tag in
-                                                              let open Stmt in
-                                                              ocanren {Prog ([], FunDecl ([Val], [Write 0; Read 0])) == q})
-                                                    (fun q -> q#reify (prj_exn))))
+      let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> let open FunDecl in
+                                                                                 let open Tag in
+                                                                                 let open Stmt in
+                                                                                 ocanren {Prog ([], FunDecl ([Val], [Write 0; Read 0])) == q})
+                                                                       (fun q -> q#reify (prj_exn))))
     end
   end
 
@@ -91,8 +91,8 @@ struct
 
     module Test = struct
       @type answer = logic GT.list with show
-      let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == LValue 3})
-                                                    (fun q -> q#reify reify)))
+      let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> ocanren {q == LValue 3})
+                                                                       (fun q -> q#reify reify)))
     end
   end
 
@@ -106,8 +106,8 @@ struct
 
     module Test = struct
       @type answer = logic GT.list with show
-      let test _ = show(answer) (Stream.take (run q (fun q -> ocanren {q == Bot | q == Unit})
-                                                    (fun q -> q#reify reify)))
+      let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> ocanren {q == Bot | q == Unit})
+                                                                       (fun q -> q#reify reify)))
     end
   end
 
@@ -122,9 +122,9 @@ struct
 
     module Test = struct
       @type answer  = ground GT.list with show
-      let test _ = show(answer) (Stream.take (run q (fun q -> let open Value in
-                                                              ocanren {St ([Std.pair 0 0], [Bot], 1, [0]) == q})
-                                                    (fun q -> q#reify (prj_exn))))
+      let _ = Printf.printf "%s\n" @@ show(answer) (Stream.take (run q (fun q -> let open Value in
+                                                                                 ocanren {St ([Std.pair 0 0], [Bot], 1, [0]) == q})
+                                                                       (fun q -> q#reify (prj_exn))))
     end
   end
 
@@ -204,7 +204,7 @@ struct
       state == St (env, mem, mem_len, assignments) &
       env_geto state id mem_id &
       inv_ido mem_len mem_id inv_mem_id &
-      list_replaceo mem inv_mem_id value mem' &
+      list_replaceo mem mem_id value mem' &
       assignments' == id :: assignments &
       state' == St (env, mem', mem_len, assignments')
   }
@@ -239,8 +239,8 @@ struct
     xs == [] & acc' == acc |
     { fresh x', xs', acc_upd in
       xs == x' :: xs' &
-      f acc x' acc_upd &
-      list_foldro f acc_upd xs' acc' }
+      f acc x' acc' &
+      list_foldro f acc' xs' acc_upd }
     (* TODO: inf search on swap, investigate *)
   }
 
@@ -304,18 +304,23 @@ struct
       env_addo state' id mem_len_prev' state'' }
   }
 
-  let st_spoil_foldero state id state' =
+  let st_spoil_foldero mem_len state mem id mem' =
     let open Value in
     ocanren {
-    mem_seto state id Bot state'
+    fresh mem_id', mem_id_inv' in
+      env_geto state id mem_id' &
+      inv_ido mem_len mem_id' mem_id_inv' &
+      list_replaceo mem mem_id_inv' Bot mem'
   }
 
   let st_spoil_assignmentso state state' =
     let open St in
     ocanren {
-    fresh _env, _mem, _mem_len, assignments in
-      state == St (_env, _mem, _mem_len, assignments) &
-      list_foldlo st_spoil_foldero state assignments state'
+    fresh env, mem, mem', mem_len, assignments, nil' in
+      state == St (env, mem, mem_len, assignments) &
+      list_foldlo (st_spoil_foldero mem_len state) mem assignments mem' &
+      nil' == [] &
+      state' == St (env, mem', mem_len, nil')
   }
 
   (* --- *)
@@ -380,7 +385,7 @@ struct
       decl == FunDecl (arg_tags, body) &
       state == St (env_before, mem_before, len_before, assignments_before) &
       state_clean == St (nil_env, mem_before, len_before, nil_assignments) &
-      list_foldl2o (add_arg_foldero state) (Std.pair state Nat.o) arg_tags args (Std.pair state_with_vars _counter) & (* TODO: or foldr2o ?? *)
+      list_foldl2o (add_arg_foldero state) (Std.pair state Nat.o) arg_tags args (Std.pair state_with_vars _counter) &
       eval_bodyo state_with_vars prog body state_evaled &
       st_spoil_assignmentso state_evaled state_spoiled &
       state_spoiled == St (_env, mem_spoiled, len, _assignments) &
@@ -418,4 +423,204 @@ struct
       empty_stateo state &
       eval_fun_empty_argso state prog main_decl state'
   }
+
+  module Test = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    @type answer  = St.ground GT.list with show
+    @type answerArgs = (Arg.ground List.ground) GT.list with show
+    @type answerValue = Value.ground GT.list with show
+    @type answerNats = (Nat.ground List.ground) GT.list with show
+    @type answerTag = Tag.ground GT.list with show
+
+    let _ = Printf.printf "list drop test: %s\n" @@ show(answerNats) (Stream.take (run q
+      (fun q -> ocanren { list_dropo 2 [1; 2; 3] q })
+      (fun q -> q#reify (List.prj_exn Nat.prj_exn))))
+
+    let _ = Printf.printf "list replace test: %s\n" @@ show(answerNats) (Stream.take (run q
+      (fun q -> ocanren { list_replaceo [1; 2; 3] 1 0 q })
+      (fun q -> q#reify (List.prj_exn Nat.prj_exn))))
+
+    let _ = Printf.printf "arg to value test: %s\n" @@ show(answerValue) (Stream.take (run q
+      (fun q -> let open Arg in
+                ocanren {
+        fresh s in
+          empty_stateo s &
+          arg_to_valueo s RValue q })
+      (fun q -> q#reify (Value.prj_exn))))
+
+    let _ = Printf.printf "st add arg test: %s\n" @@ show(answer) (Stream.take (run q
+      (fun q -> let open Arg in
+                let open Tag in
+                ocanren {
+        fresh s, s', cnt in
+          empty_stateo s &
+          empty_stateo s' &
+          st_add_argo s  s' Nat.o Val RValue q })
+      (fun q -> q#reify (St.prj_exn))))
+
+    let _ = Printf.printf "call stmt eval test: %s\n" @@ show(answer) (Stream.take (run q
+      (fun q -> let open Arg in
+                let open Tag in
+                let open Value in
+                let open St in
+                let open Stmt in
+                let open FunDecl in
+                ocanren {
+        fresh s, p, stmt in
+          s == St ([Std.pair 0 0], [Unit], 1, []) &
+          p == [FunDecl ([Ref], [Write 0])] &
+          stmt == Call (0, [0]) &
+          eval_stmto s p stmt q})
+      (fun q -> q#reify (St.prj_exn))))
+
+    let _ = Printf.printf "mem set test: %s\n" @@ show(answer) (Stream.take (run q
+      (fun q -> let open Arg in
+                let open Tag in
+                let open Value in
+                let open St in
+                ocanren {
+        fresh s in
+          s == St ([Std.pair 0 0], [Unit], 1, []) &
+          mem_seto s 0 Unit q})
+      (fun q -> q#reify (St.prj_exn))))
+
+    let _ = Printf.printf "add arg folder test: %s\n" @@ show(answer) (Stream.take (run q
+      (fun q -> let open Arg in
+                let open Tag in
+                ocanren {
+        fresh s, s', cnt in
+          empty_stateo s &
+          empty_stateo s' &
+          add_arg_foldero s (Std.pair s' Nat.o) Val RValue (Std.pair q cnt) })
+      (fun q -> q#reify (St.prj_exn))))
+
+    let _ = Printf.printf "foldl2 test: %s\n" @@ show(answer) (Stream.take (run q
+      (fun q -> let open Arg in
+                let open Tag in
+                ocanren {
+        fresh s, s', cnt, arg_tags, args in
+          arg_tags == [Val] &
+          args == [RValue] &
+          empty_stateo s &
+          empty_stateo s' &
+          list_foldl2o (add_arg_foldero s) (Std.pair s' Nat.o) arg_tags args (Std.pair q cnt) })
+      (fun q -> q#reify (St.prj_exn))))
+
+
+    let _ = Printf.printf "rvalue test: %s\n" @@ show(answerArgs) (Stream.take ~n:3 (run q
+      (fun q -> let open Arg in
+                ocanren {fresh v in List.mapo arg_to_rvalueo v q})
+      (fun q -> q#reify (List.prj_exn Arg.prj_exn))))
+
+    (* empty state test *)
+    let _ = Printf.printf "empty state: %s\n" @@ show(answer) (Stream.take (run q
+      (fun q -> ocanren {empty_stateo q})
+      (fun q -> q#reify (St.prj_exn))))
+
+    (* fun eval test *)
+    let _ = Printf.printf "fun eval test (empty): %s\n" @@ show(answer) (Stream.take (run q
+      (fun q -> (* let open Prog in *)
+                let open FunDecl in
+                let open Tag in
+                let open Stmt in
+                ocanren { fresh s, p, d in
+                            empty_stateo s &
+                            p == [] &
+                            d == FunDecl ([], []) &
+                            eval_fun_empty_argso s p d q })
+      (fun q -> q#reify (St.prj_exn))))
+
+    (* fun eval test *)
+    let _ = Printf.printf "fun eval tist (args): %s\n" @@ show(answer) (Stream.take (run q
+      (fun q -> (* let open Prog in *)
+                let open FunDecl in
+                let open Tag in
+                let open Stmt in
+                ocanren { fresh s, p, d in
+                            empty_stateo s &
+                            p == [] &
+                            d == FunDecl ([Val], [Write 0; Read 0]) &
+                            eval_fun_empty_argso s p d q })
+      (fun q -> q#reify (St.prj_exn))))
+
+    (* fun eval test *)
+    let _ = Printf.printf "fun eval test (wrong call): %s\n" @@ show(answer) (Stream.take (run q
+      (fun q -> (* let open Prog in *)
+                let open FunDecl in
+                let open Tag in
+                let open Stmt in
+                ocanren { fresh s, p, d in
+                            empty_stateo s &
+                            p == [FunDecl ([Ref], [Write 0])] &
+                            d == FunDecl ([Val], [Call (0, [0]); Read 0]) &
+                            eval_fun_empty_argso s p d q })
+      (fun q -> q#reify (St.prj_exn))))
+
+    (* prog eval test *)
+    let _ = Printf.printf "prog eval test: %s\n" @@ show(answer) (Stream.take (run q
+      (fun q -> let open Prog in
+                let open FunDecl in
+                let open Tag in
+                let open Stmt in
+                ocanren {eval_progo (Prog ([], FunDecl ([Val], [Write 0; Read 0]))) q})
+      (fun q -> q#reify (St.prj_exn))))
+
+    (* prog with func eval test *)
+    let _ = Printf.printf "prog with func eval test: %s\n" @@ show(answer) (Stream.take (run q
+      (fun q -> let open Prog in
+                let open FunDecl in
+                let open Tag in
+                let open Stmt in
+                ocanren {eval_progo (Prog ([FunDecl ([Val], [Write 0; Read 0])], FunDecl ([Val], [Write 0; Read 0; Call (0, [0])]))) q})
+      (fun q -> q#reify (St.prj_exn))))
+
+    (* prog with func eval test *)
+    let _ = Printf.printf "prog with func eval test 2: %s\n" @@ show(answer) (Stream.take (run q
+      (fun q -> let open Prog in
+                let open FunDecl in
+                let open Tag in
+                let open Stmt in
+                ocanren {eval_progo (Prog ([FunDecl ([Ref], [Write 0; Read 0])], FunDecl ([Val], [Write 0; Read 0; Call (0, [0])]))) q})
+      (fun q -> q#reify (St.prj_exn))))
+
+    (* prog with func eval test *)
+    let _ = Printf.printf "prog with func eval test 3: %s\n" @@ show(answer) (Stream.take (run q
+      (fun q -> let open Prog in
+                let open FunDecl in
+                let open Tag in
+                let open Stmt in
+                ocanren {eval_progo (Prog ([FunDecl ([Ref], [Write 0])], FunDecl ([Val], [Call (0, [0]); Read 0]))) q})
+      (fun q -> q#reify (St.prj_exn))))
+
+    (* annotation gen prog test *)
+    let _ = Printf.printf "synt test: %s\n" @@ show(answerTag) (Stream.take (run q
+      (fun q -> let open Prog in
+                let open FunDecl in
+                let open Tag in
+                let open Stmt in
+                let open St in
+                ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val], [Call (0, [0]); Read 0]))) (St ([], [], 0, []))})
+      (fun q -> q#reify (Tag.prj_exn))))
+
+    (* annotation gen prog test *)
+    let _ = Printf.printf "synt test 2: %s\n" @@ show(answerTag) (Stream.take (run q
+      (fun q -> let open Prog in
+                let open FunDecl in
+                let open Tag in
+                let open Stmt in
+                let open St in
+                ocanren {eval_progo (Prog ([FunDecl ([q], [Write 0])], FunDecl ([Val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, []))})
+      (fun q -> q#reify (Tag.prj_exn))))
+  end
+
+  (* let eval_test () = *)
+    (* Stream.hd @@ *)
+    (* run q (fun q -> ocanren { List.assoco 0 [(0, 0)] q }) *)
+          (* (fun qs -> qs#reify Nat.prj_exn) *)
+
+  (* TODO: launch tests *)
+  (* let%expect_test "empty" = *)
+    (* let x = eval_test () in *)
+    (* Printf.printf "done! %s" ((show (Nat.ground)) x); *)
+    (* [%expect {| done! 0 |}] *)
 end