diff --git a/bin/dune b/bin/dune
index b712391..2082990 100644
--- a/bin/dune
+++ b/bin/dune
@@ -8,6 +8,6 @@
  (modules main)
  (flags
   (:standard -rectypes))
- (libraries lib1)
+ ; (libraries ...)
  (preprocess
   (pps OCanren-ppx.ppx_repr OCanren-ppx.ppx_fresh GT.ppx GT.ppx_all)))
diff --git a/lib/dune b/lib/dune
index 909c576..7791c5e 100644
--- a/lib/dune
+++ b/lib/dune
@@ -3,38 +3,6 @@
   (flags
    (:standard -warn-error +5))))
 
-(library
- (name lib1)
- (modules lib)
- (flags (-rectypes))
- (libraries OCanren OCanren.tester)
- (inline_tests)
- (wrapped false)
- (preprocess
-  (pps
-   OCanren-ppx.ppx_repr
-   OCanren-ppx.ppx_fresh
-   OCanren-ppx.ppx_distrib
-   GT.ppx
-   GT.ppx_all
-   ppx_inline_test)))
-
-; (library
-;  (name lib2)
-;  (modules lib_next)
-;  (flags (-rectypes))
-;  (libraries OCanren OCanren.tester)
-;  (inline_tests)
-;  (wrapped false)
-;  (preprocess
-;   (pps
-;    OCanren-ppx.ppx_repr
-;    OCanren-ppx.ppx_fresh
-;    OCanren-ppx.ppx_distrib
-;    GT.ppx
-;    GT.ppx_all
-;    ppx_inline_test)))
-
 (library
  (name semantic_interpreter)
  (modules semantic_interpreter)
@@ -51,3 +19,37 @@
    GT.ppx_all
    ppx_expect
    ppx_inline_test)))
+
+(library
+ (name relational_semantic_interpreter)
+ (modules relational_semantic_interpreter)
+ (flags
+  (:standard -rectypes))
+ (libraries OCanren OCanren.tester)
+ (preprocessor_deps %{project_root}/lib/pp5+gt+plugins+ocanren+dump.exe)
+ (inline_tests)
+ (wrapped false)
+ (preprocess
+   (pps
+   OCanren-ppx.ppx_repr
+   OCanren-ppx.ppx_distrib
+   OCanren-ppx.ppx_deriving_reify
+   OCanren-ppx.ppx_fresh
+   ppx_expect
+   ppx_inline_test
+   --
+   -pp
+   lib/pp5+gt+plugins+ocanren+dump.exe)
+  ))
+
+(rule
+ (targets pp5+gt+plugins+ocanren+dump.exe)
+ (action
+  (run
+   mkcamlp5.opt
+   -package
+   camlp5,camlp5.pa_o,camlp5.macro,camlp5.pr_dump,logger.syntax
+   -package
+   logger.syntax,GT.syntax,GT.syntax.all,OCanren.syntax
+   -o
+   %{targets})))
diff --git a/lib/relational_semantic_interpreter.ml b/lib/relational_semantic_interpreter.ml
new file mode 100644
index 0000000..651eec1
--- /dev/null
+++ b/lib/relational_semantic_interpreter.ml
@@ -0,0 +1,44 @@
+(* (,,) -< Pair.inj _ (Pair.inj _ _) *)
+
+module Relational =
+struct
+  open GT
+  open OCanren
+  open OCanren.Std
+
+  @type data_ground = Nat.ground with show, gmap
+  @type data_logic = Nat.logic with show, gmap
+  type data_injected = Nat.injected
+
+  @type tag_ground = Ref | Value with show, gmap
+  @type tag_logic = tag_ground logic with show, gmap
+  type tag_injected = tag_ground ilogic
+
+  @type ('d, 'dl) stmt_abs = Call of 'd * 'dl | Read of 'd | Write of 'd with show, gmap
+  @type stmt_ground = (data_ground, data_ground List.ground) stmt_abs with show, gmap
+  @type stmt_logic = (data_logic, data_logic List.logic) stmt_abs logic with show, gmap
+  type stmt_injected = (data_injected, data_injected List.injected) stmt_abs ilogic
+
+  @type body_ground = stmt_ground List.ground with show, gmap
+  @type body_logic = stmt_logic List.logic with show, gmap
+  type body_injected = stmt_injected List.injected
+
+  @type fun_decl_ground = tag_ground List.ground * body_ground with show, gmap
+  @type fun_decl_logic = (tag_logic List.logic * body_logic) logic with show, gmap
+  type fun_decl_injected = (tag_injected List.injected * body_injected) ilogic
+
+  @type prog_ground = fun_decl_ground List.ground * fun_decl_ground with show, gmap
+  @type prog_logic = (fun_decl_logic List.logic * fun_decl_logic) logic with show, gmap
+  type prog_injected = (fun_decl_injected List.injected * fun_decl_injected) ilogic
+
+  @type 'd arg_abs = RValue | LValue of 'd with show, gmap
+  @type arg_ground = data_ground arg_abs with show, gmap
+  @type arg_logic = data_logic arg_abs logic with show, gmap
+  type arg_injected = data_injected arg_abs ilogic
+
+  @type value_ground = UnitV | BotV with show, gmap
+  @type value_logic = value_ground logic with show, gmap
+  type value_injected = value_ground ilogic
+
+  (* ocanren type 'a lst = Nil | Cons of 'a * 'a lst *)
+end
diff --git a/lib/semantic_interpreter.ml b/lib/semantic_interpreter.ml
index 0c75ee5..539f98c 100644
--- a/lib/semantic_interpreter.ml
+++ b/lib/semantic_interpreter.ml
@@ -1,316 +1,323 @@
-open OCanren
+(* (,,) -< Pair.inj _ (Pair.inj _ _) *)
 
-(* --- types --- *)
+module Functional =
+struct
 
-type data = int
+  (* --- types --- *)
 
-type tag = Ref | Value
-type stmt = Call of data * data list | Read of data | Write of data
+  type data = int
 
-type body = stmt list
+  type tag = Ref | Value
+  type stmt = Call of data * data list | Read of data | Write of data
 
-type fun_decl = tag list * body
+  type body = stmt list
 
-type prog = fun_decl list * fun_decl
+  type fun_decl = tag list * body
 
-(* --- exceptions --- *)
+  type prog = fun_decl list * fun_decl
 
-exception Incorrect_memory_access of int
-exception Ref_rvalue_argument of int
+  (* --- exceptions --- *)
 
-(* --- static interpreter (no rec) --- *)
+  exception Incorrect_memory_access of int
+  exception Ref_rvalue_argument of int
 
-module M = Map.Make (Int);;
+  (* --- static interpreter (no rec) --- *)
 
-type arg = RValue | LValue of data (* TODO: data in calls ?? *)
-type value = UnitV | BotV (* NOTE: RefV of data - not needed for now *)
+  module M = Map.Make (Int);;
 
-(* env * memory * last unused memory * assignments  *)
-type state = data M.t * value Array.t * int * data list
+  (* TODO: allow data (rvalue) in calls ?? *)
+  type arg = RValue | LValue of data
+  type value = UnitV | BotV (* NOTE: RefV of data - not needed for now *)
 
-let rec list_replace xs id value = match (xs, id) with
- | (x :: xs, 0) -> value :: xs
- | (x :: xs, n) -> x :: list_replace xs (id - 1) value 
- | ([], _) -> raise Not_found
+  (* TODO: replace env map with pairs *)
+  (* env * memory * last unused memory * assignments *) 
+  type state = data M.t * value list * int * data list
 
+  (* TODO: replace with pairs *)
+  let rec list_replace xs id value = match (xs, id) with
+   | (_x :: xs, 0) -> value :: xs
+   | (x :: xs, _n) -> x :: list_replace xs (id - 1) value 
+   | ([], _) -> raise Not_found
 
-let env_get state id = match state with
-  (env, mem, mem_len, assignments) -> M.find id env
 
-let env_add state id mem_id = match state with
-  (env, mem, mem_len, assignments) -> let env = M.add id mem_id env in
-                                      (env, mem, mem_len, assignments)
+  let env_get state id = match state with
+    (env, _mem, _mem_len, _assignments) -> M.find id env
 
-let inv_id mem_len id = mem_len - id - 1
+  let env_add state id mem_id = match state with
+    (env, mem, mem_len, assignments) -> let env = M.add id mem_id env in
+                                        (env, mem, mem_len, assignments)
 
-let mem_get state id = match state with
-  (env, mem, mem_len, _) -> List.nth mem @@ inv_id mem_len @@ env_get state id
+  let inv_id mem_len id = mem_len - id - 1
 
-let mem_set state id value= match state with
-  (env, mem, mem_len, assignments) -> let mem_id = inv_id mem_len @@ env_get state id in
-                                      let mem = list_replace mem mem_id value in (env, mem, mem_len, id :: assignments)
+  let mem_get state id = match state with
+    (_env, mem, mem_len, _assignments) -> List.nth mem @@ inv_id mem_len @@ env_get state id
 
-let mem_add state value = match state with
-  (env, mem, mem_len, assignments) -> let mem = value :: mem in (env, mem, mem_len + 1, assignments)
+  let mem_set state id value= match state with
+    (env, mem, mem_len, assignments) -> let mem_id = inv_id mem_len @@ env_get state id in
+                                        let mem = list_replace mem mem_id value in (env, mem, mem_len, id :: assignments)
 
-let mem_check state id = if mem_get state id == BotV then raise @@ Incorrect_memory_access id else state
+  let mem_add state value = match state with
+    (env, mem, mem_len, assignments) -> let mem = value :: mem in (env, mem, mem_len + 1, assignments)
 
+  let mem_check state id = if mem_get state id == BotV then raise @@ Incorrect_memory_access id else state
 
-let arg_to_value state arg = match arg with
-  | RValue -> UnitV
-  | LValue id -> mem_get state id
 
-let st_mem_len state =
-  match state with (_, _, mem_len, _) -> mem_len
+  let arg_to_value state arg = match arg with
+    | RValue -> UnitV
+    | LValue id -> mem_get state id
 
-let st_add_arg state state_before id arg_tag arg =
-  (* match state with (env, mem, mem_len, assignments) -> *)
-  match (arg_tag, arg) with
-    | (Ref, RValue) -> raise @@ Ref_rvalue_argument id (* TODO: allow later ?? *) 
-    | (Ref, LValue arg) -> env_add state id (env_get state_before arg)
-    | (Value, arg) -> let state = mem_add state (arg_to_value state_before arg) in
-                      let state = env_add state id (st_mem_len state - 1) in
-                      state
+  let st_mem_len state =
+    match state with (_, _, mem_len, _) -> mem_len
 
-let st_spoil_assignments state =
-  match state with (env, mem, mem_len, assignments) ->
-  (* TODO: use env var ids instead of mem_ids ?? *)
-  (env, List.fold_left (fun mem id -> list_replace mem (inv_id mem_len @@ env_get state id) BotV) mem assignments, mem_len, [])
+  let st_add_arg state state_before id arg_tag arg =
+    match (arg_tag, arg) with
+      | (Ref, RValue) -> raise @@ Ref_rvalue_argument id (* TODO: allow later ?? *) 
+      | (Ref, LValue arg) -> env_add state id (env_get state_before arg)
+      | (Value, arg) -> let state = mem_add state (arg_to_value state_before arg) in
+                        let state = env_add state id (st_mem_len state - 1) in
+                        state
 
-let rec eval_stmt state prog stmt =
-  match stmt with
-    | Call (f_id, args) -> eval_fun state prog (List.nth prog f_id) (List.map (fun arg -> LValue arg) args)
-    | Read id -> mem_check state id
-    | Write id -> mem_set state id UnitV
+  let st_spoil_assignments state =
+    match state with (env, mem, mem_len, assignments) ->
+    (* TODO: use env var ids instead of mem_ids ?? *)
+    (env, List.fold_left (fun mem id -> list_replace mem (inv_id mem_len @@ env_get state id) BotV) mem assignments, mem_len, [])
 
-and eval_body state prog body = List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body
+  let rec eval_stmt state prog stmt =
+    match stmt with
+      | Call (f_id, args) -> eval_fun state prog (List.nth prog f_id) (List.map (fun arg -> LValue arg) args)
+      | Read id -> mem_check state id
+      | Write id -> mem_set state id UnitV
 
-and eval_fun state prog decl args =
-  match decl with (arg_tags, body) ->
-  match state with (env_before, mem_before, len_before, assignments_before) as state_before ->
-  let state = (M.empty, mem_before, len_before, []) in
-  let (state, _) = List.fold_left2 (fun (state, id) arg_tag arg -> (st_add_arg state state_before id arg_tag arg, id + 1)) (state, 0) arg_tags args in
-  let state = eval_body state prog body in
-  let state = st_spoil_assignments state in
-  match state with (env, mem, len, assignments) ->
-  (env_before, List.drop (len - len_before) mem, len_before, assignments_before) (* TODO: save some assignments ?? *)
+  and eval_body state prog body = List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body
 
-and eval_fun_empty_args state prog decl =
-  match decl with (arg_tags, _) ->
-  let args = List.map (fun _ -> RValue) arg_tags in
-  eval_fun state prog decl args
+  and eval_fun state prog decl args =
+    match decl with (arg_tags, body) ->
+    match state with (env_before, mem_before, len_before, assignments_before) as state_before ->
+    let state = (M.empty, mem_before, len_before, []) in
+    let (state, _) = List.fold_left2 (fun (state, id) arg_tag arg -> (st_add_arg state state_before id arg_tag arg, id + 1)) (state, 0) arg_tags args in
+    let state = eval_body state prog body in
+    let state = st_spoil_assignments state in
+    match state with (_env, mem, len, _assignments) ->
+    (env_before, List.drop (len - len_before) mem, len_before, assignments_before) (* TODO: save some assignments ?? *)
 
-let empty_state = (M.empty, [], 0, [])
+  and eval_fun_empty_args state prog decl =
+    match decl with (arg_tags, _) ->
+    let args = List.map (fun _ -> RValue) arg_tags in
+    eval_fun state prog decl args
 
-let eval_prog (prog, main_decl) = ignore @@ eval_fun_empty_args empty_state prog main_decl
+  let empty_state = (M.empty, [], 0, [])
 
-(* tests *)
+  let eval_prog (prog, main_decl) = ignore @@ eval_fun_empty_args empty_state prog main_decl
 
-(* >> tests without functions *)
+  (* tests *)
 
-let%expect_test "empty" =
-  eval_prog ([], ([], []));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "ref param in main failure" =
-  try (eval_prog ([], ([Ref], []));
-       [%expect.unreachable])
-  with Ref_rvalue_argument id -> Printf.printf "%i" id;
-  [%expect {| 0 |}]
-
-let%expect_test "read empty args" =
-  try (eval_prog ([], ([], [Read 0]));
-       [%expect.unreachable])
-  with Not_found -> Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "write empty args" =
-  try (eval_prog ([], ([], [Write 0]));
-       [%expect.unreachable])
-  with Not_found -> Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "simple write" =
-  eval_prog ([], ([Value], [Write 0]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "simple read" = (* NOTE: should not work with read-before-write check*)
-  eval_prog ([], ([Value], [Read 0]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "multiple read & write" =
-  eval_prog ([], ([Value], [Write 0; Read 0; Write 0; Write 0; Read 0; Read 0]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "multiple read & write, multiple args" =
-  eval_prog ([], ([Value; Value; Value], [Write 0; Read 0; Write 1; Write 0; Write 2; Read 1; Write 2; Read 0; Read 2]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "main, access out of range" =
-  try(eval_prog ([], ([Value], [Write 0; Read 5 ]));
-       [%expect.unreachable])
-  with Not_found -> Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "main, access out of range" =
-  try(eval_prog ([], ([Value], [Write 0; Write 5 ]));
-       [%expect.unreachable])
-  with Not_found -> Printf.printf "done!";
-  [%expect {| done! |}]
-
-(* >> tests with one function *)
-
-let%expect_test "simple function call with value arg" =
-  eval_prog ([([Value], [Write 0; Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]) ]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "simple function call with ref arg" =
-  eval_prog ([([Ref], [Write 0; Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]) ]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "function with value arg & read" =
-  eval_prog ([([Value], [Write 0; Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]); Read 0 ]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-(* --- *)
-
-let%expect_test "function with ref arg & read" =
-  try (eval_prog ([([Ref], [Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]); Read 0 ]));
-       [%expect.unreachable])
-  with Incorrect_memory_access id -> Printf.printf "%i" id;
-  [%expect {| 0 |}]
-
-let%expect_test "function with ref arg & call twice" =
-  try (eval_prog ([([Ref], [Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]); Call (0, [0]) ]));
-       [%expect.unreachable])
-  with Incorrect_memory_access id -> Printf.printf "%i" id;
-  [%expect {| 0 |}]
-
-let%expect_test "function with ref arg, write first & call twice" =
-  eval_prog ([([Ref], [Write 0; Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]); Call (0, [0]) ]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "function with ref arg & read, write" =
-  try (eval_prog ([([Ref], [Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]); Read 0; Write 0 ]));
-       [%expect.unreachable])
-  with Incorrect_memory_access id -> Printf.printf "%i" id;
-  [%expect {| 0 |}]
-
-let%expect_test "function with ref arg & write, read" =
-  eval_prog ([([Ref], [Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]); Write 0; Read 0 ]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "function with ref arg, no write inside & read" =
-  eval_prog ([([Ref], [Read 0; Read 0])], ([Value], [Write 0; Call (0, [0]); Read 0 ]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-(* --- *)
-
-let%expect_test "function with value arg, read out of range" =
-  try(eval_prog ([([Value], [Read 0; Read 1])], ([Value; Value], [Write 0; Call (0, [0]); Read 0 ]));
-       [%expect.unreachable])
-  with Not_found -> Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "function with ref arg, read out of range" =
-  try(eval_prog ([([Ref], [Read 0; Read 1])], ([Value; Value], [Write 0; Call (0, [0]); Read 0 ]));
-       [%expect.unreachable])
-  with Not_found -> Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "function with value arg, write out of range" =
-  try(eval_prog ([([Value], [Read 0; Write 1])], ([Value; Value], [Write 0; Call (0, [0]); Read 0 ]));
-       [%expect.unreachable])
-  with Not_found -> Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "function with value arg, call out of range" =
-  try(eval_prog ([([Value], [Read 0])], ([Value; Value], [Write 0; Call (0, [2]); Read 0 ]));
-       [%expect.unreachable])
-  with Not_found -> Printf.printf "done!";
-  [%expect {| done! |}]
-
-(* --- *)
-
-let%expect_test "function with ref & value args, no write inside & read" =
-  eval_prog (
-    [([Ref; Value], [Read 0; Read 1])],
-    ([Value; Value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "function with ref & value args, write value inside & read" =
-  eval_prog (
-    [([Ref; Value], [Read 0; Read 1; Write 1; Read 1])],
-    ([Value; Value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "function with ref & value args, write both inside & read" =
-  try (eval_prog (
-    [([Ref; Value],[Read 0; Read 1; Write 0; Write 1; Read 1])],
-    ([Value; Value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ]));
-       [%expect.unreachable])
-  with Incorrect_memory_access id -> Printf.printf "%i" id;
-  [%expect {| 0 |}]
-
-(* --- *)
-
-(* NOTE: maybe important case in the future *)
-let%expect_test "function with ref two same ref args, read both & read" =
-  eval_prog (
-    [([Ref; Ref],[Read 0; Read 1; Read 1])],
-    ([Value], [Write 0; Call (0, [0; 0]); Read 0 ]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-(* NOTE: maybe important case in the future *)
-let%expect_test "function with ref two same ref args, read both & nothing" =
-  eval_prog (
-    [([Ref; Ref],[Read 0; Read 1; Write 0; Write 1; Read 1])],
-    ([Value], [Write 0; Call (0, [0; 0]); ]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-(* >> tests with several functions *)
-
-let%expect_test "two functions with ref arg, read func -> write func" =
-  eval_prog (
-    [([Ref], [Read 0]); ([Ref], [Write 0])],
-    ([Value], [Write 0; Call (0, [0]); Read 0; Call (1, [0]) ]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "two functions with ref arg, write func -> read func" =
-  try (eval_prog (
-    [([Ref], [Read 0]); ([Ref], [Write 0])],
-    ([Value], [Write 0; Call (1, [0]); Call (0, [0]) ]));
-       [%expect.unreachable])
-  with Incorrect_memory_access id -> Printf.printf "%i" id;
-  [%expect {| 0 |}]
-
-let%expect_test "two functions: ref arg after value arg" =
-  eval_prog (
-    [([Ref], [Read 0; Write 0]); ([Value], [Read 0; Write 0])],
-    ([Value], [Write 0; Call (1, [0]); Read 0; Call (0, [0]) ]));
-  Printf.printf "done!";
-  [%expect {| done! |}]
-
-let%expect_test "two functions: value arg after spoiled ref arg" =
-  try (eval_prog (
-    [([Ref], [Read 0; Write 0]); ([Value], [Read 0; Write 0])],
-    ([Value], [Write 0; Call (0, [0]); Call (1, [0]) ]));
-       [%expect.unreachable])
-  with Incorrect_memory_access id -> Printf.printf "%i" id;
-  [%expect {| 0 |}]
+  (* >> tests without functions *)
+
+  let%expect_test "empty" =
+    eval_prog ([], ([], []));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "ref param in main failure" =
+    try (eval_prog ([], ([Ref], []));
+         [%expect.unreachable])
+    with Ref_rvalue_argument id -> Printf.printf "%i" id;
+    [%expect {| 0 |}]
+
+  let%expect_test "read empty args" =
+    try (eval_prog ([], ([], [Read 0]));
+         [%expect.unreachable])
+    with Not_found -> Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "write empty args" =
+    try (eval_prog ([], ([], [Write 0]));
+         [%expect.unreachable])
+    with Not_found -> Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple write" =
+    eval_prog ([], ([Value], [Write 0]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple read" = (* NOTE: should not work with read-before-write check*)
+    eval_prog ([], ([Value], [Read 0]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "multiple read & write" =
+    eval_prog ([], ([Value], [Write 0; Read 0; Write 0; Write 0; Read 0; Read 0]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "multiple read & write, multiple args" =
+    eval_prog ([], ([Value; Value; Value], [Write 0; Read 0; Write 1; Write 0; Write 2; Read 1; Write 2; Read 0; Read 2]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "main, access out of range" =
+    try(eval_prog ([], ([Value], [Write 0; Read 5 ]));
+         [%expect.unreachable])
+    with Not_found -> Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "main, access out of range" =
+    try(eval_prog ([], ([Value], [Write 0; Write 5 ]));
+         [%expect.unreachable])
+    with Not_found -> Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* >> tests with one function *)
+
+  let%expect_test "simple function call with value arg" =
+    eval_prog ([([Value], [Write 0; Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]) ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple function call with ref arg" =
+    eval_prog ([([Ref], [Write 0; Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]) ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "function with value arg & read" =
+    eval_prog ([([Value], [Write 0; Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]); Read 0 ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* --- *)
+
+  let%expect_test "function with ref arg & read" =
+    try (eval_prog ([([Ref], [Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]); Read 0 ]));
+         [%expect.unreachable])
+    with Incorrect_memory_access id -> Printf.printf "%i" id;
+    [%expect {| 0 |}]
+
+  let%expect_test "function with ref arg & call twice" =
+    try (eval_prog ([([Ref], [Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]); Call (0, [0]) ]));
+         [%expect.unreachable])
+    with Incorrect_memory_access id -> Printf.printf "%i" id;
+    [%expect {| 0 |}]
+
+  let%expect_test "function with ref arg, write first & call twice" =
+    eval_prog ([([Ref], [Write 0; Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]); Call (0, [0]) ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "function with ref arg & read, write" =
+    try (eval_prog ([([Ref], [Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]); Read 0; Write 0 ]));
+         [%expect.unreachable])
+    with Incorrect_memory_access id -> Printf.printf "%i" id;
+    [%expect {| 0 |}]
+
+  let%expect_test "function with ref arg & write, read" =
+    eval_prog ([([Ref], [Read 0; Write 0])], ([Value], [Write 0; Call (0, [0]); Write 0; Read 0 ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "function with ref arg, no write inside & read" =
+    eval_prog ([([Ref], [Read 0; Read 0])], ([Value], [Write 0; Call (0, [0]); Read 0 ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* --- *)
+
+  let%expect_test "function with value arg, read out of range" =
+    try(eval_prog ([([Value], [Read 0; Read 1])], ([Value; Value], [Write 0; Call (0, [0]); Read 0 ]));
+         [%expect.unreachable])
+    with Not_found -> Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "function with ref arg, read out of range" =
+    try(eval_prog ([([Ref], [Read 0; Read 1])], ([Value; Value], [Write 0; Call (0, [0]); Read 0 ]));
+         [%expect.unreachable])
+    with Not_found -> Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "function with value arg, write out of range" =
+    try(eval_prog ([([Value], [Read 0; Write 1])], ([Value; Value], [Write 0; Call (0, [0]); Read 0 ]));
+         [%expect.unreachable])
+    with Not_found -> Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "function with value arg, call out of range" =
+    try(eval_prog ([([Value], [Read 0])], ([Value; Value], [Write 0; Call (0, [2]); Read 0 ]));
+         [%expect.unreachable])
+    with Not_found -> Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* --- *)
+
+  let%expect_test "function with ref & value args, no write inside & read" =
+    eval_prog (
+      [([Ref; Value], [Read 0; Read 1])],
+      ([Value; Value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "function with ref & value args, write value inside & read" =
+    eval_prog (
+      [([Ref; Value], [Read 0; Read 1; Write 1; Read 1])],
+      ([Value; Value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "function with ref & value args, write both inside & read" =
+    try (eval_prog (
+      [([Ref; Value],[Read 0; Read 1; Write 0; Write 1; Read 1])],
+      ([Value; Value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ]));
+         [%expect.unreachable])
+    with Incorrect_memory_access id -> Printf.printf "%i" id;
+    [%expect {| 0 |}]
+
+  (* --- *)
+
+  (* NOTE: maybe important case in the future *)
+  let%expect_test "function with ref two same ref args, read both & read" =
+    eval_prog (
+      [([Ref; Ref],[Read 0; Read 1; Read 1])],
+      ([Value], [Write 0; Call (0, [0; 0]); Read 0 ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* NOTE: maybe important case in the future *)
+  let%expect_test "function with ref two same ref args, read both & nothing" =
+    eval_prog (
+      [([Ref; Ref],[Read 0; Read 1; Write 0; Write 1; Read 1])],
+      ([Value], [Write 0; Call (0, [0; 0]); ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* >> tests with several functions *)
+
+  let%expect_test "two functions with ref arg, read func -> write func" =
+    eval_prog (
+      [([Ref], [Read 0]); ([Ref], [Write 0])],
+      ([Value], [Write 0; Call (0, [0]); Read 0; Call (1, [0]) ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "two functions with ref arg, write func -> read func" =
+    try (eval_prog (
+      [([Ref], [Read 0]); ([Ref], [Write 0])],
+      ([Value], [Write 0; Call (1, [0]); Call (0, [0]) ]));
+         [%expect.unreachable])
+    with Incorrect_memory_access id -> Printf.printf "%i" id;
+    [%expect {| 0 |}]
+
+  let%expect_test "two functions: ref arg after value arg" =
+    eval_prog (
+      [([Ref], [Read 0; Write 0]); ([Value], [Read 0; Write 0])],
+      ([Value], [Write 0; Call (1, [0]); Read 0; Call (0, [0]) ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "two functions: value arg after spoiled ref arg" =
+    try (eval_prog (
+      [([Ref], [Read 0; Write 0]); ([Value], [Read 0; Write 0])],
+      ([Value], [Write 0; Call (0, [0]); Call (1, [0]) ]));
+         [%expect.unreachable])
+    with Incorrect_memory_access id -> Printf.printf "%i" id;
+    [%expect {| 0 |}]
+
+end
diff --git a/test/dune b/test/dune
deleted file mode 100644
index abea2c4..0000000
--- a/test/dune
+++ /dev/null
@@ -1,2 +0,0 @@
-(test
- (name test_pass_strategy_synthesis))
diff --git a/test/test_pass_strategy_synthesis.ml b/test/test_pass_strategy_synthesis.ml
deleted file mode 100644
index e69de29..0000000