model with structures: init from control flow model, model formal difinition draft part

model_with_structures/.gitignore

@@ -0,0 +1 @@
+*.pdf

model_with_structures/analyzer.ml

@@ -0,0 +1,539 @@
+module Functional =
+struct
+
+  (* --- types --- *)
+
+  type data = int
+
+  type read_cap = Rd | NRd
+  type write_cap = AlwaysWr | MayWr | NeverWr
+  type copy_cap = Cp | NCp
+
+  type in_cap = In | NIn
+  type out_cap = Out | NOut
+
+  type tag = read_cap * write_cap * copy_cap * in_cap * out_cap
+
+  type stmt = Call of data * data list | Read of data | Write of data | Choice of stmt list * stmt list
+
+  type body = stmt list
+
+
+  type fun_decl = 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
+  exception Invalid_argument_tag of int
+  exception Incompatible_states
+
+  (* --- static interpreter (no rec) --- *)
+
+  (* TODO: allow data (rvalue) in calls ?? *)
+  type arg = RValue | LValue of data
+  type value = UnitV | UndefV | BotV (* NOTE: RefV of data - not needed for now *)
+
+  type env = (int * (tag * data)) list
+
+  (* env * memory * last unused memory * visited functions *) 
+  type state = env * value list * int * int list
+
+  (* --- *)
+
+  let rec list_zip_with f xs ys = match xs, ys with (* TODO: alternative from stdlib *)
+    | x :: xs, y :: ys -> f x y :: list_zip_with f xs ys 
+    | _, _ -> []
+
+  (* --- *)
+
+  let value_combine (left : value) (right : value) : value = match left, right with
+    | UnitV, UnitV -> UnitV
+    | BotV, BotV -> BotV
+    | _, _ -> UndefV (* NOTE: should be expanded in relational interpreter to not use ineq (?) *)
+
+  let memory_combine (left : value list) (right : value list) : value list =
+    list_zip_with value_combine left right
+
+  let state_combine (left : state) (right : state) : state = match left, right with
+    (lenv, lmem, lmem_len, lvisited), (renv, rmem, rmem_len, rvisited) ->
+    if lenv != renv || lmem_len != rmem_len then raise Incompatible_states
+    else (lenv, memory_combine lmem rmem, lmem_len, List.append lvisited rvisited)
+    (* TODO: union visited lists instead ? *)
+
+  (* --- *)
+
+  let is_read (tag : tag) : bool = match tag with
+    | (Rd, _, _, _, _) -> true
+    | _ -> false
+
+  let is_always_write (tag : tag) : bool = match tag with
+    | (_, AlwaysWr, _, _, _) -> true
+    | _ -> false
+
+  let is_may_write (tag : tag) : bool = match tag with
+    | (_, AlwaysWr, _, _, _) -> true
+    | (_, MayWr, _, _, _) -> true
+    | _ -> false
+
+  let is_never_write (tag : tag) : bool = match tag with
+    | (_, NeverWr, _, _, _) -> true
+    | _ -> false
+
+  let is_copy (tag : tag) : bool = match tag with
+    | (_, _, Cp, _, _) -> true
+    | _ -> false
+
+  let is_in (tag : tag) : bool = match tag with
+    | (_, _, _, In, _) -> true
+    | _ -> false
+
+  let is_out (tag : tag) : bool = match tag with
+    | (_, _, _, _, Out) -> true
+    | _ -> false
+
+  (* --- *)
+
+  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 visited_add (state : state) (id : data) : state =
+    match state with (env, mem, mem_len, visited) -> (env, mem, mem_len, id :: visited)
+
+  let visited_check (state : state) (id : data) : bool =
+    match state with (_, _, _, visited) -> List.exists (fun i -> i == id) visited
+
+  let env_get (state : state) (id : data) : (tag * data) =
+    match state with (env, _mem, _mem_len, _visited) -> List.assoc id env
+
+  let env_add (state : state) (id : data) (mode : tag) (mem_id : data) : state = match state with
+    (env, mem, mem_len, visited) -> let env = (id, (mode, mem_id)) :: env in
+                           (env, mem, mem_len, visited)
+
+  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, _visited) -> 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, visited) -> 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, visited)
+
+  let mem_add (state : state) (value : value) : state = match state with
+    (env, mem, mem_len, visited) -> let mem = value :: mem in (env, mem, mem_len + 1, visited)
+
+  let mem_check (state : state) (id : data) : unit =
+    if mem_get state id == BotV then raise @@ Incorrect_memory_access id else ()
+
+
+  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 check_tag_correct (tag : tag) (id : data) : unit =
+    if (* (is_in tag && not (is_read tag)) || *) (* TODO: required ?? *)
+       is_out tag > is_always_write tag ||
+       is_read tag > is_in tag
+       (* || is_copy tag && is_out tag *) (* ?? *)
+    then raise @@ Invalid_argument_tag id
+    else ()
+
+  let st_add_arg (state : state) (state_before : state)
+      (id : data) (arg_tag : tag) (arg : arg) : state =
+    check_tag_correct arg_tag id;
+    if is_copy arg_tag
+    then let state = mem_add state (arg_to_value state_before arg) in
+         env_add state id arg_tag (st_mem_len state - 1)
+    else match arg with
+      | RValue -> raise @@ Ref_rvalue_argument id (* TODO: allow later ?? *)
+      | LValue arg -> let (parent_tag, mem_id) = env_get state_before arg in
+                      if is_may_write arg_tag > is_always_write parent_tag (* TODO: FIXME: not updated semantics ?? *)
+                      then raise @@ Incorrect_const_cast id
+                      else if is_read arg_tag
+                      then env_add state id arg_tag mem_id
+                      (* TODO: parent state is spoiled, check that this is correct *)
+                      else let state_ext = env_add state id arg_tag mem_id in
+                           mem_set state_ext id BotV
+
+  (* TODO: FIXME: not enough tests on incorrect const cast (passed without ref or out check) *)
+  (* TODO; FIXME: forbid duplicates,  collect lists of all spoils & checks ? *)
+  let st_spoil_by_args (state : state) (arg_tags : tag list) (args : data list) : state =
+    match state with (env, mem, mem_len, _visited) ->
+    let state_before = state in
+    let spoil_folder (state : state) (tag : tag) (id : data) : state =
+      let parent_tag = fst (env_get state id) in
+      (* NOTE: replaced with later condition *)
+      (* if is_write tag > is_write parent_tag && (not (is_copy tag) || is_out tag) then raise @@ Incorrect_const_cast idi else *)
+      let state = if is_read tag then (mem_check state_before id; state) else state (* NOTE: state override *)
+      in if is_never_write tag then state (* TODO: FIXME: check *)
+      else match is_out tag with
+        | true -> if not @@ is_always_write parent_tag then raise @@ Incorrect_const_cast id
+                  else mem_set state id UnitV
+        | false -> if is_copy tag then state
+                   else if not @@ is_may_write parent_tag then raise @@ Incorrect_const_cast id (* TODO: check that may modifier correct *)
+                   else mem_set state id BotV
+    in List.fold_left2 spoil_folder 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
+                             let state_with_visited = if visited_check state f_id
+                                          then state
+                                          else let new_state_with_visited = visited_add state f_id in
+                                               let state_fun = eval_fun new_state_with_visited prog f_decl (List.map (fun arg -> LValue arg) args) in
+                                               (* NOTE: now memory in function is not spoiled  *)
+                                               state_fun
+                             in st_spoil_by_args state_with_visited arg_tags args
+      | Read id -> mem_check state id; state
+      | Write id -> if is_may_write @@ fst @@ env_get state id
+                    then mem_set state id UnitV
+                    else raise @@ Incorrect_const_cast id
+      | Choice (xs, ys) -> let state_x = eval_body state prog xs in
+                           let state_y = eval_body state prog ys in
+                           state_combine state_x state_y
+                           (* TODO: FIXME: additional may write / always write checks ?? *)
+
+  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, visited_before) as state_before ->
+    let state : state = ([], mem_before, len_before, visited_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, visited) ->
+    (env_before, mem_before, len_before, visited)
+    (* (env_before, list_drop (len - len_before) mem, len_before, visited) (* 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 *)
+
+  let rwi_value : tag = (Rd, AlwaysWr, Cp, In, NOut)
+  let rmwi_value : tag = (Rd, MayWr, Cp, In, NOut)
+  let ri_value : tag = (Rd, NeverWr, Cp, In, NOut)
+  let wi_value : tag = (NRd, AlwaysWr, Cp, In, NOut)
+  let mwi_value : tag = (NRd, MayWr, Cp, In, NOut)
+  let i_value : tag = (NRd, NeverWr, Cp, In, NOut)
+  let rwi_ref : tag = (Rd, AlwaysWr, NCp, In, NOut)
+  let rmwi_ref : tag = (Rd, MayWr, NCp, In, NOut)
+  let ri_ref : tag = (Rd, NeverWr, NCp, In, NOut)
+  let wi_ref : tag = (NRd, AlwaysWr, NCp, In, NOut)
+  let mwi_ref : tag = (NRd, MayWr, NCp, In, NOut)
+  let i_ref : tag = (NRd, NeverWr, NCp, In, NOut)
+
+  (* >> 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 ([], ([i_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 ([], ([wi_value], [Write 0]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple read" = (* NOTE: should not work with read-before-write check*)
+    eval_prog ([], ([ri_value], [Read 0]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "multiple read & write" =
+    eval_prog ([], ([rwi_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 ([], ([wi_value; wi_value; wi_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 ([], ([wi_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 ([], ([wi_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 ([([wi_value], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple function call with ref arg" =
+    eval_prog ([([wi_ref], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "function with value arg & read" =
+    eval_prog ([([wi_value], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Read 0 ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* --- *)
+
+  let%expect_test "function with ref arg & read" =
+    try (eval_prog ([([rwi_ref], [Read 0; Write 0])], ([wi_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 ([([rwi_ref], [Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Call (0, [0]) ]));
+         [%expect.unreachable])
+    with Incorrect_memory_access id -> Printf.printf "%i" id;
+    [%expect {| 0 |}]
+
+  (* NOTE: behaviour is fixed with new capabilities *)
+  let%expect_test "function with ref arg, write first & call twice" =
+    eval_prog ([([wi_ref], [Write 0; Read 0; Write 0])], ([wi_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 ([([rwi_ref], [Read 0; Write 0])], ([wi_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 ([([rwi_ref], [Read 0; Write 0])], ([wi_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 ([([ri_ref], [Read 0; Read 0])], ([wi_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 ([([ri_ref], [Read 0; Read 1])], ([wi_value; i_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 ([([ri_ref], [Read 0; Read 1])], ([wi_value; i_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 ([([rwi_value], [Read 0; Write 1])], ([wi_value; i_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 ([([ri_value], [Read 0])], ([wi_value; i_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 (
+      [([ri_ref; ri_value], [Read 0; Read 1])],
+      ([wi_value; wi_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 (
+      [([ri_ref; rwi_value], [Read 0; Read 1; Write 1; Read 1])],
+      ([wi_value; wi_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 (
+      [([rwi_ref; rwi_value],[Read 0; Read 1; Write 0; Write 1; Read 1])],
+      ([wi_value; wi_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 (
+      [([ri_ref; ri_ref],[Read 0; Read 1; Read 1])],
+      ([wi_value], [Write 0; Call (0, [0; 0]); Read 0 ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* NOTE: changed semantics by comporasion with prev analyzer, new test *)
+  let%expect_test "function with ref two same ref args, read both & nothing" =
+    eval_prog (
+      [([ri_ref; ri_ref],[Read 0; Read 1; Read 1])],
+      ([wi_value], [Write 0; Call (0, [0; 0]); ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* NOTE: changed semantics by comporasion with prev analyzer, new test *)
+  let%expect_test "function with ref & copy of the same arg, read & write both & nothing" =
+    eval_prog (
+      [([rwi_ref; rwi_value],[Read 0; Read 1; Write 0; Write 1; Read 1])],
+      ([wi_value], [Write 0; Call (0, [0; 0]); ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* NOTE: changed semantics by comporasion with prev analyzer, new test *)
+  let%expect_test "function with copy & ref of the same arg, read & write both & nothing" =
+    eval_prog (
+      [([rwi_value; rwi_ref],[Read 0; Read 1; Write 0; Write 1; Read 1])],
+      ([wi_value], [Write 0; Call (0, [0; 0]); ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* TODO: FIXME: now correct (use state before for mem check), is this good ?, proper way to fix ? *)
+  (* NOTE: maybe important case in the future *)
+  let%expect_test "function with ref two same ref args, read & write both, error" =
+    (* try ( *)
+      eval_prog (
+      [([rwi_ref; rwi_ref],[Read 0; Read 1; Write 0; Write 1; Read 1])],
+      ([wi_value], [Write 0; Call (0, [0; 0]); ]));
+         (* [%expect.unreachable]) *)
+    (* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
+    (* [%expect {| 0 |}] *)
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* >> tests with several functions *)
+
+  let%expect_test "two functions with ref arg, read func -> write func" =
+    eval_prog (
+      [([ri_ref], [Read 0]); ([wi_ref], [Write 0])],
+      ([wi_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 (
+      [([ri_ref], [Read 0]); ([wi_ref], [Write 0])],
+      ([wi_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 (
+      [([rwi_ref], [Read 0; Write 0]); ([rwi_value], [Read 0; Write 0])],
+      ([wi_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 (
+      [([rwi_ref], [Read 0; Write 0]); ([rwi_value], [Read 0; Write 0])],
+      ([wi_value], [Write 0; Call (0, [0]); Call (1, [0]) ]));
+         [%expect.unreachable])
+    with Incorrect_memory_access id -> Printf.printf "%i" id;
+    [%expect {| 0 |}]
+
+  (* --- *)
+
+  let%expect_test "simple function call with value arg, const cast error" =
+    try (eval_prog ([([ri_value], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ]));
+         [%expect.unreachable])
+    with Incorrect_const_cast id -> Printf.printf "%i" id;
+    [%expect {| 0 |}]
+
+  let%expect_test "simple function call with ref arg, const cast error" =
+    try (eval_prog ([([ri_ref], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ]));
+         [%expect.unreachable])
+    with Incorrect_const_cast id -> Printf.printf "%i" id;
+    [%expect {| 0 |}]
+
+  let%expect_test "simple function call with value arg, const cast ok" =
+    eval_prog ([([ri_value], [Read 0])], ([wi_value], [Write 0; Call (0, [0]) ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple function call with ref arg, const cast ok" =
+    eval_prog ([([ri_ref], [Read 0])], ([wi_value], [Write 0; Call (0, [0]) ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* --- *)
+
+  let%expect_test "simple function call with arg, recursive calls" =
+    eval_prog ([([rwi_value], [Write 0; Read 0; Write 0; Call (0, [0])])], ([wi_value], [Write 0; Call (0, [0]) ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  (* --- *)
+
+  (* TODO: out arguments test, etc. *)
+
+  (* --- *)
+
+  (* TODO: more Combine statement tests *)
+
+  let%expect_test "simple function call with value arg and choice, rw" =
+    eval_prog ([([wi_value], [Choice ([Write 0; Read 0], [Write 0]); Read 0])], ([wi_value], [Write 0; Call (0, [0]) ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+  let%expect_test "simple function call with ref arg and choice, rw" =
+    try (eval_prog ([([ri_ref], [Choice ([Read 0], [Write 0])])], ([wi_value], [Write 0; Call (0, [0]) ]));
+         [%expect.unreachable])
+    with Incorrect_const_cast id -> Printf.printf "%i" id;
+    [%expect {| 0 |}]
+
+  let%expect_test "simple function call with ref arg and choice, rr" =
+    eval_prog ([([ri_ref], [Choice ([Read 0], [Read 0; Read 0])])], ([wi_value], [Write 0; Call (0, [0]) ]));
+    Printf.printf "done!";
+    [%expect {| done! |}]
+
+end

model_with_structures/dune

@@ -0,0 +1,64 @@
+; (env
+;  (_
+;   (flags
+;    (:standard -warn-error +5))))
+
+(library
+ (name analyzer_cf)
+ (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_cf)
+ (modules tests)
+ (flags (-rectypes))
+ (libraries synthesizer_cf tests_f_cf)
+ (inline_tests)
+ (wrapped false)
+ (preprocess
+  (pps ppx_expect ppx_inline_test)))
+
+(library
+ (name tests_f_cf)
+ (modules tests_f)
+ (flags (-rectypes))
+ (libraries OCanren OCanren.tester synthesizer_cf)
+ (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_cf)
+ (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)))

model_with_structures/model.typ

@@ -0,0 +1,457 @@
+// #import "@preview/polylux:0.4.0": *
+#import "@preview/simplebnf:0.1.1": *
+// #import "@preview/zebraw:0.5.0": *
+// #show: zebraw
+#import "@preview/curryst:0.6.0": rule, prooftree, rule-set
+#import "@preview/xarrow:0.4.0": xarrow, xarrowDashed
+
+= Формальная модель используемого языка
+
+*TODO: проверить, что всё нужное добавлено*
+*TODO: добавить сложные структуры (типы) и работу с ними*
+*TODO: добавить тип лямбд (тип с id сигнатуры)*
+*TODO: добавить тип вызова поля структуры*
+*TODO: добавить правльную работу со вложенными тегами, path-доступ к полям переменных, корректность пути*
+
+Нужно будет добавить во write-flag модальности: `not write` | `may write` | `always write`
+
+Добавление condition-исполнения - выбор из нескольких блоков. Варианты:
+- & of | of & -вложенные блоки ?
+- добавить несколько альтернативны тел функциям. Но тогда придётся при трансляции if-блоки выносить в функции
+
+Лямбды - нужно тоже будет как-то находить лямбды и ля них тоже синтезировать атрибуты
+вызов лямбд будет нужен в модели?
+- lambda-аргумент - вложенные теги?, должна быть одна и та же сигнтура
+можно ввести отдельные сигнатуры-определения?
+
+проблема простой семантики: вызов лямбд: могут быть модифицируемые функции
+
+== Синтаксис
+
+#h(10pt)
+
+#let isCorrect = `isCorrect`
+
+#let isRead = `isRead`
+#let isAlwaysWrite = `isAlwaysWrite`
+#let isPossibleWrite = `isPossibleWrite`
+#let isRef = `isRef`
+#let isCopy = `isCopy`
+#let isIn = `isIn`
+#let isOut = `isOut`
+
+#let tag = `tag`
+#let value = `value`
+#let stmt = `stmt`
+#let decl = `decl`
+#let prog = `prog`
+#let path = `path`
+#let argtype = `argtype`
+#let argmem = `argmem`
+#bnf(
+  Prod(`read`,
+    { Or[Read][read passed value]
+      Or[Not Read][] } ),
+  Prod(`write`,
+    { Or[$square$ Write][in all cases there is a write to passed variable] // always write, requre at least one write in each flow variant
+      Or[$diamond$ Write][in some cases there is a write to passed variable] // possible write, no requirements (?)
+      Or[$not$ Write][] } ), // no write, require n owrites in all flow variants
+  Prod(`copy`,
+    { Or[Ref][pass reference to the value]
+      Or[Value][pass copy of the value] } ),
+  Prod(`in`,
+    { Or[In][parameter value used as input]
+      Or[Not In][] } ),
+  Prod(`out`,
+    { Or[Out][parametr value returned]
+      Or[Not Out][] } ),
+  Prod(
+    `tag`,
+    {
+      Or[`read` #h(3pt) `write` #h(3pt) `copy` #h(3pt) `in` #h(3pt) `out`][]
+    }
+  ),
+  Prod(
+    `value`,
+    {
+      Or[$0$][cell with some value (always)]
+      Or[$X$][cell with possible value or $bot$]
+      Or[$bot$][spoiled cell (always)]
+    }
+  ),
+  Prod(
+    `path`,
+    {
+      Or[$x$][fuction argument or variable itself]
+      Or[$path . n$][access $n$-th cell of the tuple]
+      Or[$path : n$][access $n$-th cell of the union] // TODO: another notation ??
+    }
+  ),
+  Prod(
+    `argtype`,
+    {
+      Or[$()$][simple type representing all primitive types] // `Unit`
+      Or[\& #h(3pt) `tag` #h(3pt) `argtype`][reference to structure, contains copy / ref choice] // `Ref`
+      Or[`argtype` $times$ `argtype`][pair type, allows to make tuples] // `Prod`
+      // Or[`argtype` $+$ `argtype`][union type (important in some way ???)] // `Sum` // TODO ?
+      Or[$F_x$][type of lambda or function pointer, defined by function declaration id] // `Fun`
+    }
+  ),
+  Prod(
+    `argmem`,
+    {
+      Or[$[m]$][memory id for simple type variable] // `Unit`
+      Or[\& #h(3pt) `tag` #h(3pt) `argmem`][reference to structure, contains copy / ref choice] // `Ref`
+      Or[`argmem` $times$ `argmem`][pair type, allows specify memory for tuples] // `Prod`
+      // Or[`argmem` $+$ `argmem`][union type (important in some way ???)] // `Sum` // TODO ?
+      Or[$F_m$][memory for lambda or function pointer, defined by function declaration id] // `Fun` // why separated ??
+    }
+  ),
+  // Prod(
+  //   `arg`,
+  //   {
+  //     Or[$0$][new value, no associated variable]
+  //     Or[$ amp d$][value from some variable]
+  //   }
+  // ),
+  Prod(
+    `stmt`,
+    {
+      Or[`CALL` $f space overline(path)$][call function by id]
+      Or[`CALL_LAM` $path space overline(path)$][call lambda funciton (variable or funcitona argument field)]
+      Or[`WRITE` $path$][write to variable]
+      Or[`READ` $path$][read from variable]
+      // TODO: or introduce block statement ?? // vars definiiton statment ??
+      // (for example, for same named vars in nested spaces)
+      Or[`CHOICE` #overline(`stmt`) #overline(`stmt`)][control flow operator, xecution of one of the blocks]
+      // NOTE: var: replaced with arguments (use rvalue as init) (?)
+      // Or[`VAR`][variables inside functions] // NOTE: no modifiers required, because it is in the new memory ?? // TODO: not required ??
+      // NOTE: lambda: compile to call to the funciton with CHOICE between possible lambda bodies <- do this analysis inside synthesizer ?
+    }
+  ),
+  Prod(
+    `decl`,
+    {
+      Or[$overline(stmt)$][function body]
+      Or[$lambda #[`argtype`] a.$ `decl`][argument with argument pass strategy annotation]
+    }
+  ),
+  Prod(
+    `prog`,
+    {
+      Or[`decl`][main function]
+      Or[`decl` `prog`][with supplimentary funcitons]
+    }
+  ),
+)
+== Семантика статического интерпретатора
+
+#h(10pt)
+
+$V := value$ - значения памяти
+
+$L := NN$ - позиции в памяти
+
+$X$ - можество переменных
+
+*TODO: специфицировать доступ*
+
+*TODO: формально описать accessor-ы tag*
+
+$sigma : X -> argmem$ - #[ позиции памяти, соответстующие переменным контекста,
+                           частично определённая функция ]
+
+$mu : NN -> V$ - память, частично определённая функция
+
+$l in NN$ - длина используемого фрагмента памяти
+
+$DD : NN -> decl$ - определения функций, частично определённая функция
+
+$d in decl, s in stmt, f in NN, x in X, a in NN$
+
+$d space @ space overline(x)$ - запись применения функции (вида #decl) к аргументам
+
+#let args = `args`
+
+#[
+
+#let ref = `ref`
+#let copy = `copy`
+#let read = `read`
+
+#let cl = $chevron.l$
+#let cr = $chevron.r$
+
+// #align(center, grid(
+//   columns: 3,
+//   gutter: 5%,
+//   align(bottom, prooftree(
+//   ...
+//   )),
+//   align(bottom, prooftree(
+//   ...
+//   )),
+//   align(bottom, prooftree(
+//   ...
+//   )),
+// ))
+
+// TODO: introduce spep env argument ??
+
+// TODO: FIXME: define typeof operation
+#let typeof = `typeof`
+
+// TODO: FIXME: define access operation
+// TODO: two versions: write with change & read
+#let access = `access`
+
+// TODO: FIXME: define argtag operation
+#let argtag = `argtag`
+
+// TODO: FIXME: define addpaths operation: ~>
+
+// FIXME
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ is correct],
+    $isOut tag -> isAlwaysWrite tag$, // NOTE; strong requirment should write
+    $isRead tag -> isIn tag$,
+    $isPossibleWrite tag and (isOut tag or not isCopy tag) -> isAlwaysWrite argtag(sigma, x)$, // NOTE: may tag => should sigma(x)
+    $isRead tag -> access(mu, sigma, x) != bot and access(mu, sigma, x) != X$,
+
+    $isCorrect_(cl sigma, mu cr) (tag, x)$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ spoil init],
+    $mu stretch(=>)^nothing_(cl sigma, mu cr) mu$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ spoil step],
+
+    $mu stretch(=>)^args_sigma gamma$,
+
+    $isPossibleWrite tag$, // NOTE: weak requirement: may write
+    $not isCopy tag$,
+    $not isOut tag$,
+
+    $isCorrect_(cl sigma, mu cr) (tag, x)$,
+
+    // gamma - memory (as mu)
+    $gamma stretch(=>)^((tag, x) : args)_sigma access(gamma, sigma, x) <- bot]$
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ fix step],
+
+    $mu stretch(=>)^args_sigma gamma$,
+
+    $isAlwaysWrite tag$, // NOTE: strong requirement: should write
+    $isOut tag$,
+
+    $isCorrect_(cl sigma, mu cr) (tag, x)$,
+
+    // gamma - memory (as mu)
+    $gamma stretch(=>)^((tag, x) : args)_sigma access(gamma, sigma, x) <- 0]$
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ skip step],
+
+    $mu stretch(=>)^args_sigma gamma$,
+
+    $not "spoil step"$,
+    $not "fix step"$,
+
+    $isCorrect_(cl sigma, mu cr) (tag, x)$,
+
+    // mu
+    $gamma stretch(=>)^((tag, x) : args)_sigma gamma$
+  )
+))
+
+
+#h(10pt)
+
+#align(center, line())
+
+#h(10pt)
+
+// TODO: special operation to add all paths one by one ??
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ $(lambda a. d) x$],
+
+    $cl sigma, mu, l cr
+     stretch(~>)^a
+     cl sigma, mu', l' cr$,
+
+    $cl sigma', mu', l' cr
+     xarrowDashed(d space @ space overline(y))
+     cl sigma'', mu'', l'' cr$,
+
+    $isRead tag$,
+    $not isCopy tag$,
+
+    // NOTE: correctness checked in CALL f
+
+    $cl sigma, mu, l cr
+     xarrowDashed((lambda a. d) space @ space x space overline(y))
+     cl sigma'', mu'', l'' cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [decl body],
+
+    $cl sigma, mu, l cr
+     attach(stretch(->)^overline(s), tr: *)
+     cl sigma', mu', l' cr$,
+
+    $d = overline(s)$,
+
+    $cl sigma, mu, l cr
+     xarrowDashed(d space @)
+     cl sigma', mu', l' cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, line())
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ CALL $f space overline(x)$],
+
+    $cl [], mu, l cr
+     xarrowDashed(d space @ space overline(x))
+     cl sigma', mu', l' cr$,
+
+    // TODO: FIXME define args in some way
+    $mu attach(stretch(=>)^args_sigma, tr: *) gamma$,
+
+    $DD(f) := d$,
+
+    $cl sigma, mu, l cr
+     xarrow("CALL" f space overline(x))
+     cl sigma, gamma, l cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ CALL_LAM $y space overline(x)$],
+
+    $typeof(y) = F_f$,
+
+    $cl sigma, mu, l cr
+     xarrow("CALL" f space overline(x))
+     cl sigma, gamma, l cr$,
+
+    $cl sigma, mu, l cr
+     xarrow("CALL_LAM" y space overline(x))
+     cl sigma, gamma, l cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ READ $x$],
+
+    $access(mu, sigma, x) != bot$,
+    $access(mu, sigma, x) != X$,
+
+    $cl sigma, mu, l cr
+     xarrow("READ" x)
+     cl sigma, mu, l cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ WRITE $x$],
+
+    $isPossibleWrite sigma(x)$, // TODO: FIXME ?? always or possible ??
+
+    $cl sigma, mu, l cr
+     xarrow("WRITE" x)
+     cl sigma, access(mu, sigma, x) <- 0, l cr$,
+  )
+))
+
+#h(10pt)
+
+#let combine = `combine`
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ CHOICE $overline(s)$ $overline(t)$],
+
+    $cl sigma, mu, l cr
+     attach(stretch(->)^overline(s), tr: *)
+     cl sigma_s, mu_s, l_s cr$,
+
+    $cl sigma, mu, l cr
+     attach(stretch(->)^overline(t), tr: *)
+     cl sigma_t, mu_t, l_t cr$,
+
+    $l_t = l_s$,
+    $sigma_s = sigma_t$,
+
+    // TODO changes ?? two ways ??
+    $cl sigma, mu, l cr
+     xarrow("CHOICE" overline(s) space overline(t))
+     cl sigma, combine(mu_s, mu_t), l cr$,
+  )
+))
+
+#h(10pt)
+
+$ combine(mu_1, mu_2)[i] = combine_e (mu_1[i], mu_2[i]) $
+$ combine_e (bot, bot) = bot $
+$ combine_e (0, 0) = 0 $
+$ combine_e (\_, \_) = X $
+
+]

model_with_structures/synthesizer.ml

@@ -0,0 +1,704 @@
+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 ReadCap = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec t = Rd | NRd
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = t
+    ]
+  end
+
+  module WriteCap = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec t = AlwaysWr | MayWr | NeverWr
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = t
+    ]
+  end
+
+  (* NOTE: rename names ?? *)
+  module CopyCap = 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
+    ]
+
+  end
+
+  module InCap = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec t = In | NIn
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = t
+    ]
+  end
+
+  module OutCap = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec t = Out | NOut
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = t
+    ]
+  end
+
+  module Tag = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec ('r, 'w, 'c, 'i, 'o) t = Tag of 'r * 'w * 'c * 'i * 'o
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = (ReadCap.ground, WriteCap.ground, CopyCap.ground, InCap.ground, OutCap.ground) t
+    ]
+
+    (* TODO: less repeats *)
+    (* common constructors *)
+    let rwi_val = let open ReadCap in
+                  let open WriteCap in
+                  let open CopyCap in
+                  let open InCap in
+                  let open OutCap in
+                  ocanren { Tag (Rd, AlwaysWr, Val, In, NOut) }
+    let ri_val = let open ReadCap in
+                 let open WriteCap in
+                 let open CopyCap in
+                 let open InCap in
+                 let open OutCap in
+                 ocanren { Tag (Rd, NeverWr, Val, In, NOut) }
+    let wi_val = let open ReadCap in
+                 let open WriteCap in
+                 let open CopyCap in
+                 let open InCap in
+                 let open OutCap in
+                 ocanren { Tag (NRd, AlwaysWr, Val, In, NOut) }
+    let i_val = let open ReadCap in
+                let open WriteCap in
+                let open CopyCap in
+                let open InCap in
+                let open OutCap in
+                ocanren { Tag (NRd, NeverWr, Val, In, NOut) }
+    let rwi_ref = let open ReadCap in
+                  let open WriteCap in
+                  let open CopyCap in
+                  let open InCap in
+                  let open OutCap in
+                  ocanren { Tag (Rd, AlwaysWr, Ref, In, NOut) }
+    let ri_ref = let open ReadCap in
+                 let open WriteCap in
+                 let open CopyCap in
+                 let open InCap in
+                 let open OutCap in
+                 ocanren { Tag (Rd, NeverWr, Ref, In, NOut) }
+    let wi_ref = let open ReadCap in
+                 let open WriteCap in
+                 let open CopyCap in
+                 let open InCap in
+                 let open OutCap in
+                 ocanren { Tag (NRd, AlwaysWr, Ref, In, NOut) }
+    let i_ref = let open ReadCap in
+                let open WriteCap in
+                let open CopyCap in
+                let open InCap in
+                let open OutCap in
+                ocanren { Tag (NRd, NeverWr, Ref, In, NOut) }
+
+    (* constraints *)
+    let x_any tag = let open InCap in
+                    let open OutCap in
+                    ocanren { fresh r, w, c in
+                              tag == Tag (r, w, c, NIn, NOut) }
+    let i_any tag = let open InCap in
+                    let open OutCap in
+                    ocanren { fresh r, w, c in
+                              tag == Tag (r, w, c, In, NOut) }
+    let o_any tag = let open InCap in
+                    let open OutCap in
+                    ocanren { fresh r, w, c in
+                              tag == Tag (r, w, c, NIn, Out) }
+    let io_any tag = let open InCap in
+                     let open OutCap in
+                     ocanren { fresh r, w, c in
+                               tag == Tag (r, w, c, In, Out) }
+
+    (* accessors *)
+    let is_reado tag = let open ReadCap in ocanren {
+                         fresh w_, c_, i_, o_ in
+                         tag == Tag (Rd, w_, c_, i_, o_) }
+    let is_not_reado tag = let open ReadCap in ocanren {
+                             fresh w_, c_, i_, o_ in
+                             tag == Tag (NRd, w_, c_, i_, o_) }
+    let is_always_writeo tag = let open WriteCap in ocanren {
+                                 fresh r_, c_, i_, o_ in
+                                 tag == Tag (r_, AlwaysWr, c_, i_, o_) }
+    let is_may_writeo tag = let open WriteCap in ocanren {
+                              fresh r_, c_, i_, o_ in
+                              { tag == Tag (r_, AlwaysWr, c_, i_, o_) |
+                                tag == Tag (r_, MayWr, c_, i_, o_) } }
+    let is_never_writeo tag = let open WriteCap in ocanren {
+                                fresh r_, c_, i_, o_ in
+                                tag == Tag (r_, NeverWr, c_, i_, o_) }
+    let is_refo tag = let open CopyCap in ocanren {
+                        fresh r_, w_, i_, o_ in
+                        tag == Tag (r_, w_, Ref, i_, o_) }
+    let is_valueo tag = let open CopyCap in ocanren {
+                          fresh r_, w_, i_, o_ in
+                          tag == Tag (r_, w_, Val, i_, o_) }
+    let is_ino tag = let open InCap in ocanren {
+                       fresh r_, w_, c_, o_ in
+                       tag == Tag (r_, w_, c_, In, o_) }
+    let is_not_ino tag = let open InCap in ocanren {
+                           fresh r_, w_, c_, o_ in
+                           tag == Tag (r_, w_, c_, NIn, o_) }
+    let is_outo tag = let open OutCap in ocanren {
+                        fresh r_, w_, c_, i_ in
+                        tag == Tag (r_, w_, c_, i_, Out) }
+    let is_not_outo tag = let open OutCap in ocanren {
+                            fresh r_, w_, c_, i_ in
+                            tag == Tag (r_, w_, c_, i_, NOut) }
+
+    let eq_copyo tag cp = let open CopyCap in ocanren {
+                           fresh r_, w_, i_, o_ in
+                           tag == Tag (r_, w_, cp, i_, o_) }
+
+    module Test = struct
+      @type answer = logic GT.list with show
+
+      let test _ = show(answer) (Stream.take (run q (fun q -> let open ReadCap in
+                                                              let open WriteCap in
+                                                              let open CopyCap in
+                                                              let open InCap in
+                                                              let open OutCap in
+                                                              ocanren {q == Tag (Rd, NeverWr, Ref, In, NOut)})
+                                                    (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, 'sl) t = Call of 'd * 'dl | Read of 'd | Write of 'd | Choice of 'sl * 'sl
+      [@@deriving gt ~options:{ show; gmap }]
+      type ground = (Nat.ground, Nat.ground List.ground, 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 ([rwi_ref; rwi_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 ([ri_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 | Undef | 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, 'visited) t = St of 'env * 'mem * 'last_mem * 'visited
+      [@@deriving gt ~options:{ show; gmap }]
+      type nonrec ground = (((Nat.ground, ((Tag.ground, Nat.ground) Pair.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
+                                                              let open Tag in
+                                                              ocanren {St ([Std.pair 0 (Std.pair rwi_val 0)], [Bot], 1, [0]) == q})
+                                                    (fun q -> q#reify (prj_exn))))
+    end
+  end
+
+  (* --- *)
+
+  let rec list_zip_witho f xs ys zs = ocanren {
+    { fresh x, xs', y, ys', z, zs' in
+      xs == x :: xs' &
+      ys == y :: ys' &
+      zs == z :: zs' &
+      f x y z &
+      list_zip_witho f xs' ys' zs' } |
+    { fresh x, xs' in
+      xs == x :: xs' &
+      ys == [] &
+      zs == [] } |
+    { fresh y, ys' in
+      xs == [] &
+      ys == y :: ys' &
+      zs == [] } |
+    { xs == [] & ys == [] & zs == [] }
+  }
+
+  (* --- *)
+
+  let value_combineo left right res = let open Value in ocanren {
+    { left == Unit & right == Unit & res == Unit } |
+    { left == Bot & right == Bot & res == Bot } |
+    { left == Unit & right == Bot & res == Undef } |
+    { left == Bot & right == Unit & res == Undef }
+  }
+
+  let memory_combineo left right res = ocanren {
+    list_zip_witho value_combineo left right res
+  }
+
+  let state_combineo left right res = let open St in ocanren {
+    fresh lenv, lmem, lmem_len, lvisited, renv, rmem, rmem_len, rvisited, res_mem in
+    left == St (lenv, lmem, lmem_len, lvisited) &
+    right == St (renv, rmem, rmem_len, rvisited) &
+    lenv == renv & lmem_len == rmem_len &
+    memory_combineo lmem rmem res_mem  &
+    res == St (lenv, rmem, lmem_len, List.appendo lvisited rvisited)
+    (* TODO: union visited lists instead ? *)
+  }
+
+  (* --- *)
+
+  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 env_geto state id tag' mem_id' =
+    let open St in
+    ocanren {
+    fresh env, _mem, _mem_len, _visited, elem in
+      state == St (env, _mem, _mem_len, _visited) &
+      List.assoco id env elem &
+      Std.pair tag' mem_id' == elem
+  }
+
+  let env_addo state id tg mem_id state' =
+    let open St in
+    ocanren {
+    fresh env, env', mem, mem_len, visited, elem in
+      state == St (env, mem, mem_len, visited) &
+      Std.pair tg mem_id == elem & 
+      (Std.pair id elem) :: env == env' &
+      state' == St (env', mem, mem_len, visited)
+  }
+
+  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, _visited, _tag in
+    state == St (_env, mem, mem_len, _visited) &
+    env_geto state id _tag 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, visited, mem_id, inv_mem_id, mem', _tag in
+      state == St (env, mem, mem_len, visited) &
+      env_geto state id _tag mem_id &
+      inv_ido mem_len mem_id inv_mem_id &
+      list_replaceo mem inv_mem_id value mem' &
+      state' == St (env, mem', mem_len, visited)
+  }
+
+  let mem_addo state value state' =
+    let open St in
+    ocanren {
+      fresh env, mem, mem_len, mem_len', visited, mem' in
+      state == St (env, mem, mem_len, visited) &
+      mem' == value :: mem &
+      mem_len' == Nat.s mem_len &
+      state' == St (env, mem', mem_len', visited)
+  }
+
+  let mem_checko state id =
+    let open Value in
+    ocanren {
+      mem_geto state id Unit
+    }
+
+  (* --- *)
+
+  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
+    let open Tag in
+    ocanren { is_valueo arg & value' == RValue }
+
+  let st_mem_leno state mem_len' =
+    let open St in
+    ocanren {
+    fresh _env, _mem, _visited in
+      state == St (_env, _mem, mem_len', _visited)
+  }
+
+  let tag_correcto tg =
+    let open Tag in
+    ocanren {
+      {is_not_outo tg | { is_outo tg & is_always_writeo tg } } &
+      {is_not_reado tg | { is_reado tg & is_ino tg } }
+    }
+
+  let st_add_argo state state_before id arg_tag arg state'' =
+    (* let open Nat in *)
+    let open Value in
+    let open Arg in
+    let open Tag in
+    ocanren {
+        tag_correcto arg_tag & {
+        { fresh value', state', mem_len_prev' in
+          is_valueo arg_tag &
+          arg_to_valueo state_before arg value' &
+          mem_addo state value' state' &
+          st_mem_leno state mem_len_prev' &
+          env_addo state' id arg_tag mem_len_prev' state'' } |
+        { fresh arg', parent_tag, mem_id, state' in
+          is_refo arg_tag &
+            (* { arg == RValue } *) (* NOTE: not allowed for now *)
+          arg == LValue arg' &
+          env_geto state_before id parent_tag mem_id &
+          env_addo state id arg_tag mem_id state' &
+          { is_never_writeo arg_tag | { is_may_writeo arg_tag & is_may_writeo parent_tag } } &
+          {
+            { is_reado arg_tag & state' == state'' } |
+            { is_not_reado arg_tag & mem_seto state' id Bot state'' }
+          }
+        }
+      }
+    }
+
+  let st_spoil_foldero state_before state tg id state' =
+    let open Value in
+    let open Tag in
+    let open St in
+    ocanren {
+      fresh env, mem, mem_len, _visited, parent_tg, _mem_id in
+      state == St (env, mem, mem_len, _visited) &
+      env_geto state id parent_tg _mem_id &
+      { is_not_reado tg | { is_reado tg & mem_checko state_before id } } &
+      { { is_never_writeo tg & state == state'} |
+        { is_always_writeo tg & 
+          is_outo tg & is_may_writeo parent_tg & mem_seto state id Unit state' } |
+        { is_may_writeo tg & {
+          { is_not_outo tg & is_valueo tg & state == state' } |
+          { is_not_outo tg & is_refo tg & is_may_writeo parent_tg & mem_seto state id Bot state' }
+        } }
+      }
+    }
+
+  let st_spoil_by_argso state arg_tags args state' =
+    ocanren {
+      fresh state_before in
+      state == state_before & (* TODO: required ? *)
+      list_foldl2o (st_spoil_foldero state_before) state arg_tags args state'
+    }
+
+  (* let st_spoil_assignmentso state state' = *)
+    (* let open St in *)
+    (* ocanren { *)
+    (* fresh _env, _mem, _mem_len, visited in *)
+      (* state == St (_env, _mem, _mem_len, visited) & *)
+      (* list_foldlo st_spoil_foldero state visited 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 list_not_membero xs x = ocanren {
+    xs == [] |
+    { fresh x', xs' in
+        xs == x' :: xs' &
+        x' =/= x &
+        list_not_membero xs' x }
+  }
+
+  let visited_checko state f_id =
+    let open St in
+    ocanren {
+      fresh _env, _mem, _mem_len, visited in
+      state == St (_env, _mem, _mem_len, visited) &
+      List.membero visited f_id
+    }
+
+  let not_visited_checko state f_id =
+    let open St in
+    ocanren {
+      fresh _env, _mem, _mem_len, visited in
+      state == St (_env, _mem, _mem_len, visited) &
+      list_not_membero visited f_id
+    }
+
+  let visited_addo state f_id state' =
+    let open St in
+    ocanren {
+      fresh env, mem, mem_len, visited, visited' in
+      state == St (env, mem, mem_len, visited) &
+      visited' == f_id :: visited &
+      state' == St (env,mem, mem_len, visited')
+    }
+
+  let rec eval_stmto state prog stmt state' =
+    let open Stmt in
+    let open Value in
+    let open FunDecl in
+    let open Tag in
+    ocanren {
+    { fresh f_id, args, f, args', state_after_call, arg_tags, _body in
+      stmt == Call (f_id, args) &
+      list_ntho prog f_id f &
+      FunDecl (arg_tags, _body) == f &
+      List.mapo arg_to_lvalueo args args' &
+      (* TODO: FIXME: memoisation, do not do calls on check successfull *)
+      
+      (* NOTE: tmp simplification for less branching (TODO?) *)
+      { { fresh state_with_visited in
+          not_visited_checko state f_id &
+          visited_addo state f_id state_with_visited &
+          eval_funo state_with_visited prog f args' state_after_call } |
+        { visited_checko state f_id &
+          state_after_call == state } } &
+      st_spoil_by_argso state_after_call arg_tags args state' } |
+    { fresh id in stmt == Read id & mem_checko state id & state == state' } |
+    { fresh id, tag, _mem_id in
+      stmt == Write id &
+      env_geto state id tag _mem_id &
+      is_may_writeo tag &
+      mem_seto state id Unit state' } |
+    { fresh xs, ys in
+      stmt == Choice (xs, ys) }
+    (* TODO: FIXME: choice actions *)
+  }
+
+  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, visited_before,
+          state_clean,
+          state_with_vars, _counter,
+          state_evaled,
+          _env, _mem, _len, visited,
+          nil_env, nil_visited in
+      nil_env == [] &
+      nil_visited == [] &
+      decl == FunDecl (arg_tags, body) &
+      state == St (env_before, mem_before, len_before, visited_before) &
+      state_clean == St (nil_env, mem_before, len_before, nil_visited) &
+      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 &
+      state_evaled == St (_env,_mem, _len, visited) &
+      state' == St (env_before, mem_before, len_before, visited)
+  }
+
+  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_visited in
+      nil_env == [] &
+      nil_visited == [] &
+      nil_mem == [] &
+      state == St (nil_env, nil_mem, Nat.o, nil_visited)
+  }
+
+  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

model_with_structures/tests.ml

@@ -0,0 +1,61 @@
+open Tests_f
+open Synthesizer
+open Relational
+
+(* type tests *)
+let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}]
+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 ([Tag (Rd, AlwaysWr, Ref, In, NOut); Tag (Rd, AlwaysWr, Val, In, NOut)], [Call (S (O), [O]); Write (S (O))])] |}]
+let%expect_test "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Tag (Rd, NeverWr, Val, In, NOut)], [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, (Tag (Rd, AlwaysWr, Val, In, NOut), 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, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
+let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [])] |}]
+let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [])] |}]
+let%expect_test "multiple writes eval test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Unit], S (S (O)), [])] |}]
+let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [O])] |}]
+let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [O])] |}]
+let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [O])] |}]
+let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}]
+let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}]
+let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit], S (O), [])] |}]
+let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [])] |}]
+let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O)))], [Bot; Unit], S (S (O)), [])] |}]
+let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
+let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), 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 "function eval test 6" = print_endline (fun_eval_t6 ()); [%expect {| [St ([], [], O, [O])] |}]
+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, [O])] |}]
+let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [O])] |}]
+let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}]
+let%expect_test "prog eval test 5" = print_endline (prog_eval_t5 ()); [%expect {| [St ([], [], O, [O])] |}]
+let%expect_test "prog eval test 6" = print_endline (prog_eval_t6 ()); [%expect {| [] |}]
+let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Tag (Rd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)] |}]
+let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Ref, In, NOut)] |}]
+let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]; [Tag (NRd, AlwaysWr, Ref, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]] |}]
+let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut)]] |}]
+let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Val]; [Ref; Ref]] |}]
+let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Ref]; [Ref; Val]] |}]
+let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Val; Val]; [Ref; Val]] |}]
+let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Val]; [Val; Ref]] |}]
+let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}]
+
+let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [O])] |}]
+

model_with_structures/tests_f.ml

@@ -0,0 +1,509 @@
+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
+@type answerCopyCap = CopyCap.ground GT.list with show
+@type answerCopyCaps = (CopyCap.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 rwi_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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
+      p == [FunDecl ([wi_ref; wi_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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
+      p == [FunDecl ([wi_ref; wi_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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
+      p == [FunDecl ([wi_ref; wi_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 (Std.pair wi_ref 0)], [Unit], 1, []) &
+      p == [FunDecl ([wi_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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
+      p == [FunDecl ([wi_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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
+      p == [FunDecl ([wi_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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
+      p == [FunDecl ([wi_ref; wi_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 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
+      p == [FunDecl ([wi_ref; wi_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 (Std.pair wi_ref 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 (Std.pair wi_ref 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 (Std.pair wi_ref 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) rwi_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 == [rwi_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 ([wi_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 ([wi_ref], [Write 0])] &
+                        d == FunDecl ([wi_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 ([wi_ref], [Write 0])] &
+                        d == FunDecl ([wi_val; wi_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 ([wi_ref; wi_ref], [Write 0; Write 1])] &
+                        d == FunDecl ([wi_val; wi_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))))
+
+(* fun eval test *)
+let fun_eval_t6 _ = 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 ([wi_val], [Write 0])] &
+                        d == FunDecl ([wi_val], [Call (0, [0])]) &
+                        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 ([wi_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 ([wi_val], [Write 0; Read 0])],
+                                       FunDecl ([wi_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 ([wi_ref], [Write 0; Read 0])],
+                                       FunDecl ([wi_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 ([wi_ref], [Write 0])],
+                                       FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
+  (fun q -> q#reify (St.prj_exn))))
+
+(* prog with func eval test *)
+let prog_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 {eval_progo (Prog ([FunDecl ([wi_val], [Write 0])],
+                                       FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
+  (fun q -> q#reify (St.prj_exn))))
+
+(* prog with func eval test *)
+let prog_eval_t6 _ = 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 ([ri_val], [Write 0])],
+                                       FunDecl ([wi_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 {i_any q &
+                     eval_progo (Prog ([FunDecl ([q], [Write 0])],
+                                       FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, [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 {i_any q & is_not_reado q &
+                     eval_progo (Prog ([FunDecl ([q], [Write 0])],
+                                       FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [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 {i_any q & is_not_reado q & i_any r & is_not_reado r &
+                     eval_progo (Prog ([FunDecl ([q], [Write 0])],
+                                       FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [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 {i_any q & is_not_reado q &
+                     eval_progo (Prog ([FunDecl ([q], [Write 0])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, [0]))})
+  (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *)
+
+(* annotation gen prog test *)
+let synt_t5 _ = show(answerCopyCaps) (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 {fresh q', r' in
+                     i_any q' & is_not_reado q' &
+                     i_any r' & is_not_reado r' & is_never_writeo r' &
+                     eq_copyo q' q & eq_copyo r' r &
+                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
+  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *)
+
+(* annotation gen prog test *)
+let synt_t6 _ = show(answerCopyCaps) (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 {fresh q', r' in
+                     i_any q' & is_not_reado q' &
+                     i_any r' & is_not_reado r' & is_never_writeo r' &
+                     eq_copyo q' q & eq_copyo r' r &
+                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
+  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *)
+
+(* annotation gen prog test *)
+let synt_t7 _ = show(answerCopyCaps) (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 {fresh q', r' in
+                     i_any q' & is_not_reado q' & i_any r' & is_not_reado r' &
+                     eq_copyo q' q & eq_copyo r' r &
+                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))})
+  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
+
+(* annotation gen prog test *)
+let synt_t8 _ = show(answerCopyCaps) (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 {fresh q', r' in
+                     i_any q' & is_not_reado q' & i_any r' & is_not_reado r' &
+                     eq_copyo q' q & eq_copyo r' r &
+                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))})
+  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
+
+(* annotation gen prog test *)
+let synt_t9 _ = show(answerCopyCaps) (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 {fresh q', r' in
+                     i_any q' & is_not_reado q' &
+                     i_any r' & is_reado r' & is_never_writeo r' &
+                     eq_copyo q' q & eq_copyo r' r &
+                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Read 1])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, [0]))})
+  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
+
+(* TODO: FIXME: implement memoization cuts *)
+(* 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 ([wi_ref], [Write 0; Call (0, [0])])],
+                                       FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) q})
+  (fun q -> q#reify (St.prj_exn))))
+