diff --git a/simplest_model/analyzer.ml b/simplest_model/analyzer.ml
index 2480d75..e0a9c1e 100644
--- a/simplest_model/analyzer.ml
+++ b/simplest_model/analyzer.ml
@@ -37,61 +37,59 @@ struct
    | ([], _) -> raise Not_found
 
 
-  let env_get (state : state) (id : data) : data = match state with
+  let env_get state id = match state with
     (env, _mem, _mem_len, _assignments) -> List.assoc id env
 
-  let env_add (state : state) (id : data) (mem_id : data) : state = match state with
+  let env_add state id mem_id = match state with
     (env, mem, mem_len, assignments) -> let env = (id, mem_id) :: env in
                                         (env, mem, mem_len, assignments)
 
-  let inv_id (mem_len : int) (id : data) : data = mem_len - id - 1
+  let inv_id mem_len id = mem_len - id - 1
 
-  let mem_get (state : state) (id : data) : value = match state with
+  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_set (state : state) (id : data) (value : value) : state = match state with
+  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_add (state : state) (value : value) : state = match state with
+  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 : state) (id : data) : state =
-    if mem_get state id == BotV then raise @@ Incorrect_memory_access id else state
+  let mem_check state id = if mem_get state id == BotV then raise @@ Incorrect_memory_access id else state
 
 
-  let arg_to_value (state : state) (arg : arg) : value = match arg with
+  let arg_to_value state arg = match arg with
     | RValue -> UnitV
     | LValue id -> mem_get state id
 
-  let st_mem_len (state : state) : int =
+  let st_mem_len state =
     match state with (_, _, mem_len, _) -> mem_len
 
-  let st_add_arg (state : state) (state_before : state)
-      (id : data) (arg_tag : tag) (arg : arg) : state =
+  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
                         env_add state id (st_mem_len state - 1)
 
-  let st_spoil_assignments (state : state) : state =
+  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 list_drop n xs = List.of_seq @@ Seq.drop n @@ List.to_seq xs
 
-  let rec eval_stmt (state : state) (prog : fun_decl list) (stmt : stmt) : 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
 
-  and eval_body (state : state) (prog : fun_decl list) (body : body) : state =
+  and eval_body state prog body =
     List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body
 
-  and eval_fun (state : state) (prog : fun_decl list) (decl : fun_decl) (args : arg list) : state =
+  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 = ([], mem_before, len_before, []) in
@@ -101,14 +99,14 @@ struct
     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_fun_empty_args (state : state) (prog : fun_decl list) (decl : fun_decl) : state =
+  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 empty_state : state = ([], [], 0, [])
+  let empty_state = ([], [], 0, [])
 
-  let eval_prog ((prog, main_decl) : prog) = ignore @@ eval_fun_empty_args empty_state prog main_decl
+  let eval_prog (prog, main_decl) = ignore @@ eval_fun_empty_args empty_state prog main_decl
 
   (* tests *)
 
diff --git a/simplest_model/synthesizer.ml b/simplest_model/synthesizer.ml
index aa2e4da..4c8f0bd 100644
--- a/simplest_model/synthesizer.ml
+++ b/simplest_model/synthesizer.ml
@@ -380,7 +380,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_foldr2o (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) & (* TODO: or foldr2o ?? *)
       eval_bodyo state_with_vars prog body state_evaled &
       st_spoil_assignmentso state_evaled state_spoiled &
       state_spoiled == St (_env, mem_spoiled, len, _assignments) &
diff --git a/simplest_model/tests.ml b/simplest_model/tests.ml
index 6e7452f..5da7fe0 100644
--- a/simplest_model/tests.ml
+++ b/simplest_model/tests.ml
@@ -2,7 +2,48 @@ open Tests_f
 open Synthesizer
 open Relational
 
-(* type tests *)
+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))])] |}]
@@ -12,48 +53,9 @@ let%expect_test "Arg type test" = print_endline (Arg.Test.test ()); [%expect {|
 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])] |}]
 
-(* function tests *)
-let%expect_test "inv_id test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}]
-let%expect_test "inv_id test 2" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}]
-let%expect_test "inv_id test 3" = print_endline (inv_id_t3 ()); [%expect {| [S (O)] |}]
-let%expect_test "list_drop test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}]
-let%expect_test "list_replace test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}]
-let%expect_test "arG_to_value test 1" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}]
-let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}]
-let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Unit], S (S (O)), [O])] |}]
-let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Bot], S (S (O)), [S (O)])] |}]
-let%expect_test "multiple writes eval 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 "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, O)], [Bot], S (O), [])] |}]
-let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Bot], S (S (O)), [])] |}]
-let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Unit], S (S (O)), [])] |}]
-let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Bot], S (S (O)), [])] |}]
-let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Bot], S (S (O)), [])] |}]
-let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, O)], [Unit], S (O), [O])] |}]
-let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, O)], [Bot], S (O), [O])] |}]
-let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, S (O))], [Bot; Unit], S (S (O)), [O])] |}]
-let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}]
-let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}]
-let%expect_test "rvalue test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}]
-let%expect_test "empty_state test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "function eval test 1" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "function eval test 2" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "function eval test 3" = print_endline (fun_eval_t3 ()); [%expect {| [] |}]
-let%expect_test "function eval test 4" = print_endline (fun_eval_t4 ()); [%expect {| [] |}]
-let%expect_test "function eval test 5" = print_endline (fun_eval_t5 ()); [%expect {| [] |}]
-let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "prog eval test 2" = print_endline (prog_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}]
-let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Val] |}]
-let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Ref; Val] |}]
-let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}]
-let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Val]] |}]
-let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Ref; Ref]; [Ref; Val]; [Val; Ref]; [Val; Val]] |}]
-let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Ref; Ref]; [Val; Ref]; [Ref; Val]; [Val; Val]] |}]
-let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}]
-let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}]
-let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}]
 
-(* NOTE: inf test in current model (without additional functional interfaces and ) *)
-(* let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [])] |}] *)
+
+
+
+
 
diff --git a/simplest_model/tests_f.ml b/simplest_model/tests_f.ml
index 18ea63f..3c1a8a0 100644
--- a/simplest_model/tests_f.ml
+++ b/simplest_model/tests_f.ml
@@ -311,7 +311,7 @@ let prog_eval_t1 _ = show(answer) (Stream.take (run q
   (fun q -> q#reify (St.prj_exn))))
 
 (* prog with func eval test *)
-let prog_eval_t2 _ = show(answer) (Stream.take (run q
+let prog_eeal_t2 _ = show(answer) (Stream.take (run q
   (fun q -> let open Prog in
             let open FunDecl in
             let open Tag in
@@ -416,23 +416,3 @@ let synt_t8 _ = show(answerTags) (Stream.take (run qr
             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)])))
-
-(* annotation gen prog test *)
-let synt_t9 _ = 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; Read 1])], FunDecl ([Val; Val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, []))})
-  (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
-
-(* prog with recursive function call *)
-let rec_eval_t _ = 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; Call (0, [0])])], FunDecl ([Val], [Call (0, [0]); Write 0; Read 0]))) q})
-  (fun q -> q#reify (St.prj_exn))))
-
diff --git a/simplest_model_with_mods/.gitignore b/simplest_model_with_mods/.gitignore
deleted file mode 100644
index a136337..0000000
--- a/simplest_model_with_mods/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-*.pdf
diff --git a/simplest_model_with_mods/analyzer.ml b/simplest_model_with_mods/analyzer.ml
deleted file mode 100644
index 311add0..0000000
--- a/simplest_model_with_mods/analyzer.ml
+++ /dev/null
@@ -1,339 +0,0 @@
-module Functional =
-struct
-
-  (* --- types --- *)
-
-  type data = int
-
-  type tag = Ref | Value
-  type mode = Const | Mut
-  type stmt = Call of data * data list | Read of data | Write of data
-
-  type body = stmt list
-
-  type fun_decl = (mode * tag) list * body
-
-  type prog = fun_decl list * fun_decl
-
-  (* --- exceptions --- *)
-
-  exception Incorrect_memory_access of int
-  exception Ref_rvalue_argument of int
-  exception Incorrect_const_cast of int
-
-  (* --- static interpreter (no rec) --- *)
-
-  (* TODO: allow data (rvalue) in calls ?? *)
-  type arg = RValue | LValue of data
-  type value = UnitV | BotV (* NOTE: RefV of data - not needed for now *)
-
-  type env = (int * (mode * data)) list
-
-  (* env * memory * last unused memory *) 
-  type state = env * value list * int
-
-  (* 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 : state) (id : data) : (mode * data) = match state with
-    (env, _mem, _mem_len) -> List.assoc id env
-
-  let env_add (state : state) (id : data) (mode : mode) (mem_id : data) : state = match state with
-    (env, mem, mem_len) -> let env = (id, (mode, mem_id)) :: env in
-                           (env, mem, mem_len)
-
-  let inv_id (mem_len : int) (id : data) : data = mem_len - id - 1
-
-  let mem_get (state : state) (id : data) : value = match state with
-    (_env, mem, mem_len) -> List.nth mem @@ inv_id mem_len @@ snd @@ env_get state id
-
-  let mem_set (state : state) (id : data) (value : value) : state = match state with
-    (env, mem, mem_len) -> let mem_id = inv_id mem_len @@ snd @@ env_get state id in
-                                        let mem = list_replace mem mem_id value in (env, mem, mem_len)
-
-  let mem_add (state : state) (value : value) : state = match state with
-    (env, mem, mem_len) -> let mem = value :: mem in (env, mem, mem_len + 1)
-
-  let mem_check (state : state) (id : data) : state =
-    if mem_get state id == BotV then raise @@ Incorrect_memory_access id else state
-
-
-  let arg_to_value (state : state) (arg : arg) : value = match arg with
-    | RValue -> UnitV
-    | LValue id -> mem_get state id
-
-  let st_mem_len (state : state) : int =
-    match state with (_, _, mem_len) -> mem_len
-
-  let st_add_arg (state : state) (state_before : state)
-      (id : data) (arg_tag : mode * tag) (arg : arg) : state =
-    match (arg_tag, arg) with
-      | ((mode, Ref), RValue) -> raise @@ Ref_rvalue_argument id (* TODO: allow later ?? *) 
-      | ((mode, Ref), LValue arg) -> let (parent_mode, mem_id) = env_get state_before arg in
-                                     if mode == Mut && parent_mode == Const
-                                     then raise @@ Incorrect_const_cast id
-                                     else env_add state id mode mem_id
-      | ((mode, Value), arg) -> let state = mem_add state (arg_to_value state_before arg) in
-                                env_add state id mode (st_mem_len state - 1)
-
-  let st_spoil_by_args (state : state) (arg_tags : (mode * tag) list) (args : data list) : state =
-    match state with (env, mem, mem_len) ->
-    let spoilFolder state tag id =
-      match tag with
-      | (Mut, Ref) -> if fst (env_get state id) == Const
-                      then raise @@ Incorrect_const_cast id
-                      else mem_set state id BotV
-      | _ -> state
-    in 
-    List.fold_left2 spoilFolder state arg_tags args
-
-  let list_drop n xs = List.of_seq @@ Seq.drop n @@ List.to_seq xs
-
-  let rec eval_stmt (state : state) (prog : fun_decl list) (stmt : stmt) : state =
-    match stmt with
-      | Call (f_id, args) -> let (arg_tags, _) as f_decl = List.nth prog f_id in
-                             ignore @@ eval_fun state prog f_decl (List.map (fun arg -> LValue arg) args); (* TODO: memoisation, etc ?? *)
-                             st_spoil_by_args state arg_tags args
-      | Read id -> mem_check state id
-      | Write id -> if fst (env_get state id) == Const
-                    then raise @@ Incorrect_const_cast id
-                    else mem_set state id UnitV
-
-  and eval_body (state : state) (prog : fun_decl list) (body : body) : state =
-    List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body
-
-  and eval_fun (state : state) (prog : fun_decl list) (decl : fun_decl) (args : arg list) : state =
-    match decl with (arg_tags, body) ->
-    match state with (env_before, mem_before, len_before) as state_before ->
-    let state = ([], 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
-    match state with (_env, mem, len) ->
-    (env_before, list_drop (len - len_before) mem, len_before) (* TODO: save some assignments ?? *)
-
-  and eval_fun_empty_args (state : state) (prog : fun_decl list) (decl : fun_decl) : state =
-    match decl with (arg_tags, _) ->
-    let args = List.map (fun _ -> RValue) arg_tags in
-    eval_fun state prog decl args
-
-  let empty_state : state = ([], [], 0)
-
-  let eval_prog ((prog, main_decl) : prog) = ignore @@ eval_fun_empty_args empty_state prog main_decl
-
-  (* tests *)
-
-  (* >> 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 ([], ([(Const, 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 ([], ([(Mut, Value)], [Write 0]));
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "simple read" = (* NOTE: should not work with read-before-write check*)
-    eval_prog ([], ([(Const, Value)], [Read 0]));
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "multiple read & write" =
-    eval_prog ([], ([(Mut, 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 ([], ([(Mut, Value); (Mut, Value); (Mut, 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 ([], ([(Mut, 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 ([], ([(Mut, 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 ([([(Mut, Value)], [Write 0; Read 0; Write 0])], ([(Mut, Value)], [Write 0; Call (0, [0]) ]));
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "simple function call with ref arg" =
-    eval_prog ([([(Mut, Ref)], [Write 0; Read 0; Write 0])], ([(Mut, Value)], [Write 0; Call (0, [0]) ]));
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "function with value arg & read" =
-    eval_prog ([([(Mut, Value)], [Write 0; Read 0; Write 0])], ([(Mut, Value)], [Write 0; Call (0, [0]); Read 0 ]));
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  (* --- *)
-
-  let%expect_test "function with ref arg & read" =
-    try (eval_prog ([([(Mut, Ref)], [Read 0; Write 0])], ([(Mut, 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 ([([(Mut, Ref)], [Read 0; Write 0])], ([(Mut, 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 ([([(Mut, Ref)], [Write 0; Read 0; Write 0])], ([(Mut, 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 ([([(Mut, Ref)], [Read 0; Write 0])], ([(Mut, 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 ([([(Mut, Ref)], [Read 0; Write 0])], ([(Mut, 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 ([([(Const, Ref)], [Read 0; Read 0])], ([(Mut, 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 ([([(Const, Value)], [Read 0; Read 1])], ([(Mut, Value); (Const, 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 ([([(Const, Ref)], [Read 0; Read 1])], ([(Mut, Value); (Const, 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 ([([(Mut, Value)], [Read 0; Write 1])], ([(Mut, Value); (Const, 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 ([([(Const, Value)], [Read 0])], ([(Mut, Value); (Mut, 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 (
-      [([(Const, Ref); (Const, Value)], [Read 0; Read 1])],
-      ([(Mut, Value); (Mut, 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 (
-      [([(Const, Ref); (Mut, Value)], [Read 0; Read 1; Write 1; Read 1])],
-      ([(Mut, Value); (Mut, 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 (
-      [([(Mut, Ref); (Mut, Value)],[Read 0; Read 1; Write 0; Write 1; Read 1])],
-      ([(Mut, Value); (Mut, 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 (
-      [([(Const, Ref); (Const, Ref)],[Read 0; Read 1; Read 1])],
-      ([(Mut, 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 (
-      [([(Mut, Ref); (Mut, Ref)],[Read 0; Read 1; Write 0; Write 1; Read 1])],
-      ([(Mut, 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 (
-      [([(Const, Ref)], [Read 0]); ([(Mut, Ref)], [Write 0])],
-      ([(Mut, 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 (
-      [([(Const, Ref)], [Read 0]); ([(Mut, Ref)], [Write 0])],
-      ([(Mut, 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 (
-      [([(Mut, Ref)], [Read 0; Write 0]); ([(Mut, Value)], [Read 0; Write 0])],
-      ([(Mut, 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 (
-      [([(Mut, Ref)], [Read 0; Write 0]); ([(Mut, Value)], [Read 0; Write 0])],
-      ([(Mut, 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/simplest_model_with_mods/dune b/simplest_model_with_mods/dune
deleted file mode 100644
index fb1ff19..0000000
--- a/simplest_model_with_mods/dune
+++ /dev/null
@@ -1,64 +0,0 @@
-; (env
-;  (_
-;   (flags
-;    (:standard -warn-error +5))))
-
-(library
- (name analyzer_mods)
- (modules analyzer)
- (flags (-rectypes))
- (libraries OCanren OCanren.tester)
- (inline_tests)
- (wrapped false)
- (preprocess
-  (pps GT.ppx GT.ppx_all ppx_expect ppx_inline_test)))
-
-(library
- (name tests_modt)
- (modules tests)
- (flags (-rectypes))
- (libraries synthesizer_mods tests_f_mods)
- (inline_tests)
- (wrapped false)
- (preprocess
-  (pps ppx_expect ppx_inline_test)))
-
-(library
- (name tests_f_mods)
- (modules tests_f)
- (flags (-rectypes))
- (libraries OCanren OCanren.tester synthesizer_mods)
- (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
- (wrapped false)
- (preprocess
-  (pps
-   OCanren-ppx.ppx_repr
-   OCanren-ppx.ppx_deriving_reify
-   OCanren-ppx.ppx_fresh
-   GT.ppx
-   GT.ppx_all
-   OCanren-ppx.ppx_distrib
-   --
-   -pp
-   camlp5/pp5+gt+plugins+ocanren+dump.exe)))
-
-(library
- (name synthesizer_mods)
- (modules synthesizer)
- (flags
-  ; (-dsource)
-  (:standard -rectypes))
- (libraries OCanren OCanren.tester)
- (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
- (wrapped false)
- (preprocess
-  (pps
-   OCanren-ppx.ppx_repr
-   OCanren-ppx.ppx_deriving_reify
-   OCanren-ppx.ppx_fresh
-   GT.ppx
-   GT.ppx_all
-   OCanren-ppx.ppx_distrib
-   --
-   -pp
-   camlp5/pp5+gt+plugins+ocanren+dump.exe)))
diff --git a/simplest_model_with_mods/synthesizer.ml b/simplest_model_with_mods/synthesizer.ml
deleted file mode 100644
index aa2e4da..0000000
--- a/simplest_model_with_mods/synthesizer.ml
+++ /dev/null
@@ -1,421 +0,0 @@
-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"]
-    [%%ocanren_inject
-      type nonrec t = Ref | Val
-      [@@deriving gt ~options:{ show; gmap }]
-      type nonrec ground = t
-    ]
-
-    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)))
-    end
-  end
-
-  module Stmt = struct
-    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
-    [%%ocanren_inject
-      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
-    ]
-
-    module Test = 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 test2 _ = show(answer') (Stream.take (run q (fun q -> ocanren {Call (1, [2]) == q})
-                                                      (fun q -> q#reify (prj_exn))))
-    end
-  end
-
-  module FunDecl = struct
-    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
-    [%%ocanren_inject
-      type nonrec ('l, 'b) t = FunDecl of 'l * 'b
-      [@@deriving gt ~options:{ show; gmap }]
-      type nonrec ground = (Tag.ground List.ground, Stmt.ground List.ground) t
-    ]
-
-    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))))
-    end
-  end
-
-  module Prog = struct
-    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
-    [%%ocanren_inject
-      type nonrec ('l, 'f) t = Prog of 'l * 'f
-      [@@deriving gt ~options:{ show; gmap }]
-      type nonrec ground = (FunDecl.ground List.ground, FunDecl.ground) t
-    ]
-
-    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))))
-    end
-  end
-
-  module Arg = struct
-    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
-    [%%ocanren_inject
-      type nonrec 'd t = RValue | LValue of 'd
-      [@@deriving gt ~options:{ show; gmap }]
-      type nonrec ground = Nat.ground t
-    ]
-
-    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)))
-    end
-  end
-
-  module Value = struct
-    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
-    [%%ocanren_inject
-      type nonrec t = Unit | Bot
-      [@@deriving gt ~options:{ show; gmap }]
-      type nonrec ground = t
-    ]
-
-    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)))
-    end
-  end
-
-  module St = struct
-    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
-    [%%ocanren_inject
-      type nonrec ('env, 'mem, 'last_mem, 'assignments) t = St 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
-    ]
-
-    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))))
-    end
-  end
-
-  let rec list_replaceo xs id value ys = ocanren {
-    (* xs == [] & ys == [] | (* NOTE: error *) *)
-    { fresh x, xs' in
-        xs == x :: xs' &
-        id == Nat.o &
-        ys == value :: xs' } |
-    { fresh x, xs', id', ys' in
-        xs == x :: xs' &
-        id == Nat.s id' &
-        ys == x :: ys' &
-        list_replaceo xs' id' value ys' }
-    }
-
-  (* let rec list_assoco a xs v' = *)
-    (* ocanren { *)
-    (* fresh a', b', xs' in *)
-      (* (Std.pair a' b') :: xs' == xs & *)
-      (* { a =/= a' & list_assoco a xs' v' | *)
-        (* a == a' & v' == b' } *)
-  (* } *)
-  (* TODO: difference from List.assoco ?? *)
-
-  let env_geto state id mem_id' =
-    let open St in
-    ocanren {
-    fresh env, mem, mem_len, assignments in
-      state == St (env, mem, mem_len, assignments) &
-      List.assoco id env mem_id'
-  }
-
-  let env_addo state id mem_id state' =
-    let open St in
-    ocanren {
-    fresh env, env', mem, mem_len, assignments in
-      state == St (env, mem, mem_len, assignments) &
-      state' == St (env', mem, mem_len, assignments) &
-      (Std.pair id mem_id) :: env == env'
-  }
-
-  let inv_ido mem_len id id' = ocanren {
-    fresh inv_id_inc in
-      Nat.addo inv_id_inc id mem_len &
-      Nat.addo id' 1 inv_id_inc
-  }
-
-  (* --- *)
-
-  let rec list_ntho xs id x' = ocanren {
-    (* xs == [] | (* NOTE: error *) *)
-    { fresh y', xs' in
-      id == Nat.o &
-      y' :: xs' == xs &
-      x' == y' } |
-    { fresh id', y', xs' in
-      Nat.s id' == id &
-      y' :: xs' == xs &
-      list_ntho xs' id' x' }
-  }
-
-  let mem_geto state id value' =
-    let open St in
-    ocanren {
-    fresh mem, mem_len, mem_id, mem_id_inv, _env, _assignments in
-    state == St (_env, mem, mem_len, _assignments) &
-    env_geto state id mem_id &
-    inv_ido mem_len mem_id mem_id_inv &
-    list_ntho mem mem_id_inv value'
-  }
-
-  let mem_seto state id value state'=
-    let open St in
-    ocanren {
-    fresh env, mem, mem_len, assignments, mem_id, inv_mem_id, mem', assignments' in
-      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' &
-      assignments' == id :: assignments &
-      state' == St (env, mem', mem_len, assignments')
-  }
-
-  let mem_addo state value state' =
-    let open St in
-    ocanren {
-    fresh env, mem, mem_len, mem_len', assignments, mem' in
-      state == St (env, mem, mem_len, assignments) &
-      mem' == value :: mem &
-      mem_len' == Nat.s mem_len &
-      state' == St (env, mem', mem_len', assignments)
-  }
-
-  let mem_checko state id state' =
-    let open Value in
-    ocanren {
-    mem_geto state id Unit & state' == state
-  }
-
-  (* --- *)
-
-  let rec list_foldlo f acc xs acc' = ocanren {
-    xs == [] & acc' == acc |
-    { fresh x', xs', acc_upd in
-      xs == x' :: xs' &
-      list_foldlo f acc xs' acc_upd &
-      f acc_upd x' acc' }
-  }
-
-  let rec list_foldro f acc xs acc' = ocanren {
-    xs == [] & acc' == acc |
-    { fresh x', xs', acc_upd in
-      xs == x' :: xs' &
-      f acc x' acc_upd &
-      list_foldro f acc_upd xs' acc' }
-    (* TODO: inf search on swap, investigate *)
-  }
-
-
-  let rec list_foldr2o f acc xs ys acc' = ocanren {
-    xs == [] & ys == [] & acc' == acc |
-    { fresh x', xs', y', ys', acc_upd in
-      xs == x' :: xs' &
-      ys == y' :: ys' &
-      f acc x' y' acc_upd &
-      list_foldr2o f acc_upd xs' ys' acc' }
-  }
-
-  let rec list_foldl2o f acc xs ys acc' = ocanren {
-    xs == [] & ys == [] & acc' == acc |
-    { fresh x', xs', y', ys', acc_upd in
-      xs == x' :: xs' &
-      ys == y' :: ys' &
-      list_foldl2o f acc xs' ys' acc_upd &
-      f acc_upd x' y' acc' }
-  }
-
-  let arg_to_valueo state arg value' =
-    let open Arg in
-    let open Value in
-    ocanren {
-    arg == RValue & value' == Unit |
-    { fresh id in
-      arg == LValue id &
-      mem_geto state id value' }
-  }
-
-  let arg_to_rvalueo _arg value' =
-    let open Arg in
-    ocanren { value' == RValue }
-
-  let st_mem_leno state mem_len' =
-    let open St in
-    ocanren {
-    fresh _env, _mem, _assignments in
-      state == St (_env, _mem, mem_len', _assignments)
-  }
-
-  let st_add_argo state state_before id arg_tag arg state'' =
-    (* let open Nat in *)
-    let open Arg in
-    let open Tag in
-    ocanren {
-    (* arg_tag == Tag.ref & arg == Arg.rvalue & state'' == state | *)
-      (* NOTE: error, TODO: allow later ?? *)
-    { fresh arg', value' in
-      arg_tag == Ref &
-      arg == LValue arg' &
-      env_geto state_before arg' value' &
-      env_addo state id value' state'' } |
-    { fresh value', state', mem_len_prev' in
-      arg_tag == Val &
-      arg_to_valueo state_before arg value' &
-      mem_addo state value' state' &
-      st_mem_leno state mem_len_prev' &
-      env_addo state' id mem_len_prev' state'' }
-  }
-
-  let st_spoil_foldero state id state' =
-    let open Value in
-    ocanren {
-    mem_seto state id Bot state'
-  }
-
-  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'
-  }
-
-  (* --- *)
-
-  let arg_to_lvalueo arg arg' =
-    let open Arg in
-    ocanren { arg' == LValue arg }
-
-  let rec list_dropo n xs xs' = ocanren {
-    xs == [] & xs' == [] |
-    n == Nat.o & xs == xs' & xs =/= [] |
-    { fresh n', _y, ys in
-        Nat.s n' == n &
-        xs == _y :: ys &
-        list_dropo n' ys xs' }
-  }
-
-  let rec eval_stmto state prog stmt state' =
-    let open Stmt in
-    let open Value in
-    ocanren {
-    { fresh f_id, args, f, args' in
-      stmt == Call (f_id, args) &
-      list_ntho prog f_id f &
-      List.mapo arg_to_lvalueo args args' &
-      eval_funo state prog f args' state' } |
-    { fresh id in stmt == Read id & mem_checko state id state' } |
-    { fresh id in stmt === Write id & mem_seto state id Unit state' }
-  }
-
-  and eval_body_foldero prog state stmt state' =
-    eval_stmto state prog stmt state'
-
-  and eval_bodyo state prog body state' =
-    list_foldro (eval_body_foldero prog) state body state' 
-
-  and add_arg_foldero state_before state_c arg_tag arg state_c' =
-    ocanren {
-    fresh state, id, state', id' in
-      state_c == Std.pair state id &
-      st_add_argo state state_before id arg_tag arg state' &
-      id' == Nat.s id &
-      state_c' == Std.pair state' id'
-  }
-
-  and eval_funo state prog decl args state' =
-    let open FunDecl in
-    let open St in
-    ocanren {
-    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 in
-      nil_env == [] &
-      nil_assignments == [] &
-      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_foldr2o (add_arg_foldero state) (Std.pair state Nat.o) arg_tags args (Std.pair state_with_vars _counter) & (* TODO: or foldr2o ?? *)
-      eval_bodyo state_with_vars prog body state_evaled &
-      st_spoil_assignmentso state_evaled state_spoiled &
-      state_spoiled == St (_env, mem_spoiled, len, _assignments) &
-      Nat.addo len_to_drop len_before len &
-      list_dropo len_to_drop mem_spoiled mem_updated &
-      state' == St (env_before, mem_updated, len_before, assignments_before)
-  }
-
-  and eval_fun_empty_argso state prog decl state' =
-    let open FunDecl in
-    ocanren {
-    fresh arg_tags, args, _body in
-      decl == FunDecl (arg_tags, _body) &
-      List.mapo arg_to_rvalueo arg_tags args &
-      eval_funo state prog decl args state'
-  }
-
-  (* --- *)
-
-  let empty_stateo state =
-    let open St in
-    ocanren {
-    fresh nil_env, nil_mem, nil_assignments in
-      nil_env == [] &
-      nil_assignments == [] &
-      nil_mem == [] &
-      state == St (nil_env, nil_mem, Nat.o, nil_assignments)
-  }
-
-  let eval_progo all_prog state' =
-    let open Prog in
-    ocanren {
-    fresh prog, main_decl, state in
-      all_prog == Prog (prog, main_decl) &
-      empty_stateo state &
-      eval_fun_empty_argso state prog main_decl state'
-  }
-end
diff --git a/simplest_model_with_mods/tests.ml b/simplest_model_with_mods/tests.ml
deleted file mode 100644
index 6e7452f..0000000
--- a/simplest_model_with_mods/tests.ml
+++ /dev/null
@@ -1,59 +0,0 @@
-open Tests_f
-open Synthesizer
-open Relational
-
-(* type tests *)
-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])] |}]
-
-(* function tests *)
-let%expect_test "inv_id test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}]
-let%expect_test "inv_id test 2" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}]
-let%expect_test "inv_id test 3" = print_endline (inv_id_t3 ()); [%expect {| [S (O)] |}]
-let%expect_test "list_drop test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}]
-let%expect_test "list_replace test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}]
-let%expect_test "arG_to_value test 1" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}]
-let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}]
-let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Unit], S (S (O)), [O])] |}]
-let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Bot], S (S (O)), [S (O)])] |}]
-let%expect_test "multiple writes eval 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 "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, O)], [Bot], S (O), [])] |}]
-let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Unit; Bot], S (S (O)), [])] |}]
-let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Unit], S (S (O)), [])] |}]
-let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Bot], S (S (O)), [])] |}]
-let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), S (O)); (O, O)], [Bot; Bot], S (S (O)), [])] |}]
-let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, O)], [Unit], S (O), [O])] |}]
-let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, O)], [Bot], S (O), [O])] |}]
-let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, S (O))], [Bot; Unit], S (S (O)), [O])] |}]
-let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}]
-let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, O)], [Unit], S (O), [])] |}]
-let%expect_test "rvalue test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}]
-let%expect_test "empty_state test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "function eval test 1" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "function eval test 2" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "function eval test 3" = print_endline (fun_eval_t3 ()); [%expect {| [] |}]
-let%expect_test "function eval test 4" = print_endline (fun_eval_t4 ()); [%expect {| [] |}]
-let%expect_test "function eval test 5" = print_endline (fun_eval_t5 ()); [%expect {| [] |}]
-let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "prog eval test 2" = print_endline (prog_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [])] |}]
-let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}]
-let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Val] |}]
-let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Ref; Val] |}]
-let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}]
-let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Val]] |}]
-let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Ref; Ref]; [Ref; Val]; [Val; Ref]; [Val; Val]] |}]
-let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Ref; Ref]; [Val; Ref]; [Ref; Val]; [Val; Val]] |}]
-let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Ref; Val]; [Val; Val]] |}]
-let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}]
-let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}]
-
-(* NOTE: inf test in current model (without additional functional interfaces and ) *)
-(* let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [])] |}] *)
-
diff --git a/simplest_model_with_mods/tests_f.ml b/simplest_model_with_mods/tests_f.ml
deleted file mode 100644
index 18ea63f..0000000
--- a/simplest_model_with_mods/tests_f.ml
+++ /dev/null
@@ -1,438 +0,0 @@
-open Synthesizer
-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_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 {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)])))
-
-(* annotation gen prog test *)
-let synt_t9 _ = 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; Read 1])], FunDecl ([Val; Val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, []))})
-  (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
-
-(* prog with recursive function call *)
-let rec_eval_t _ = 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; Call (0, [0])])], FunDecl ([Val], [Call (0, [0]); Write 0; Read 0]))) q})
-  (fun q -> q#reify (St.prj_exn))))
-