struct: fixes, test 2 from presentation (mostly, choice removed for now)

model_with_structures/analyzer.ml

@@ -59,22 +59,26 @@ struct
 
   (* value model & memory model *)
 
-  type deepvalue = ZeroDV
-                 | SmthDV
-                 | BotDV
-                 | FunDV of ((* data list * *) stmt) list
-                 | RefDV of deepvalue
-                 | TupleDV of deepvalue list
+  (* type deepvalue = ZeroDV *)
+                 (* | SmthDV *)
+                 (* | BotDV *)
+                 (* | FunDV of ((* data list * *) stmt) list *)
+                 (* | RefDV of deepvalue *)
+                 (* | TupleDV of deepvalue list *)
 
-  type value = ZeroV
-             | SmthV
-             | BotV
+  type memval = ZeroMV | SmthMV | BotMV (* | TopMV ?? *)
+  type readval = ZeroRV | OneRV | TopRV
+  type writeval = ZeroWV | SmthWV | OneWV
+
+  type value = UnitV of memval * readval * writeval
              | FunV of ((* data list * *) stmt) list
              | RefV of memid
              | TupleV of value list
 
   type revpath = VarRP | DerefRP of revpath | AccessRP of revpath * data
 
+  type action = ReadA | AlwaysWriteA | MayWriteA
+
   (* TODO: any additional difference between rvalue and lvalue now ?? *)
 
   (* --- *)
@@ -138,16 +142,17 @@ struct
   let mem_set (mem : mem) (id : memid) (v : value) : mem =
     (list_replace (fst mem) (snd mem - id - 1) v, snd mem)
 
-  let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with
-    | ZeroV -> ZeroDV
-    | SmthV -> SmthDV
-    | BotV -> BotDV
-    | FunV s -> FunDV s
-    | RefV id -> RefDV (v_to_deepv mem @@ mem_get mem id)
-    | TupleV vs -> TupleDV (List.map (v_to_deepv mem) vs)
+  (* let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with *)
+    (* | ZeroV -> ZeroDV *)
+    (* | SmthV -> SmthDV *)
+    (* | BotV -> BotDV *)
+    (* | FunV s -> FunDV s *)
+    (* | RefV id -> RefDV (v_to_deepv mem @@ mem_get mem id) *)
+    (* | TupleV vs -> TupleDV (List.map (v_to_deepv mem) vs) *)
 
-  let is_trivial_v (v : value) : bool = 
-    v == ZeroV || v == SmthV || v == BotV
+  let is_trivial_v (v : value) : bool =
+    match v with | UnitV (_, _, _) -> true
+                 | _ -> false
 
   (* --- path accessors --- *)
 
@@ -191,22 +196,12 @@ struct
   (* - value construction *)
 
   let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value =
-    if is_trivial_v v
-    then match t with
-    | UnitT (Rd, _) -> (mem, v)
-    | UnitT (NRd, _) -> (mem, BotV)
-    | _ -> raise @@ Typing_error "valcopy: trivial value, wrong type"
-    else match t, v with
-    (* NOTE: replaced with if | best choice ?? *)
-    (* | UnitT (Rd, w), ZeroV -> (mem, v) *)
-    (* | UnitT (Rd, w), SmthV -> (mem, v) *)
-    (* | UnitT (Rd, w), BotV -> (mem, v) *)
-    (* | UnitT (NRd, w), ZeroV -> (mem, BotV) *)
-    (* | UnitT (NRd, w), SmthV -> (mem, BotV) *)
-    (* | UnitT (NRd, w), BotV -> (mem, BotV) *)
+    match t, v with
+    | UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV))
+    | UnitT (NRd, _), UnitV _ -> (mem, UnitV (BotMV, ZeroRV, ZeroWV))
     | FunT _, FunV _ -> (mem, v)
-    | RefT (Rf, _), RefV _ -> (mem, v)
-    | RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
+    (* | RefT (Rf, _), RefV _ -> (mem, v) *)
+    | RefT (_, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
                                let (mem'', id'') = mem_add mem' v' in
                                (mem'', RefV id'') 
     | TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in
@@ -215,25 +210,76 @@ struct
                               (mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *)
     | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type"
 
+  (* - action rules *)
+
+  let memvmod (a : action) (v_m : memval) : memval =
+    match a, v_m with
+      | ReadA, ZeroMV -> ZeroMV
+      | ReadA, _ -> raise @@ Eval_error "memvmod: forbidden read"
+      | AlwaysWriteA, _ -> ZeroMV
+      | MayWriteA, ZeroMV -> ZeroMV
+      | MayWriteA, _ -> SmthMV
+
+  let readvmod (a : action) (v_r : readval) : readval =
+    match a, v_r with
+      | _, TopRV -> TopRV
+      | _, OneRV -> OneRV
+      | ReadA, ZeroRV -> OneRV
+      | AlwaysWriteA, ZeroRV -> TopRV
+      | MayWriteA, ZeroRV -> ZeroRV
+
+  let writevmod (a : action) (v_w : writeval) : writeval =
+    match a, v_w with
+      | ReadA, v -> v
+      | AlwaysWriteA, _ -> OneWV
+      | MayWriteA, OneWV -> OneWV
+      | MayWriteA, v -> v
+
   (* - value update *)
 
-  let rec valupd (mem : mem) (v : value) (p : revpath) (b : value) : mem * value = match p, v with
+  let rec valchange (mem : mem) (v : value) (p : revpath) (b : value) : mem * value = match p, v with
     | VarRP, _ -> (mem, b)
-    | DerefRP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in
+    | DerefRP p, RefV id -> let (mem', v') = valchange mem (mem_get mem id) p b in
                             (mem_set mem' id v', RefV id)
-    | AccessRP (p, id), TupleV vs -> let (mem', v') = (* FIXME TMP Printf.printf "vs size=%i id=%i\n" (List.length vs) id; *)
-                                                      valupd mem (List.nth vs id) p b in
-                                     (* FIXME TMP Printf.printf "before return\n"; *)
+    | AccessRP (p, id), TupleV vs -> let (mem', v') = valchange mem (List.nth vs id) p b in
+                                     (mem', TupleV (list_replace vs id v'))
+    | _, _ -> raise @@ Typing_error "valupd"
+
+  let rec valupd (mem : mem) (v : value) (p : revpath) (a : action) : mem * value = match p, v with
+    | VarRP, UnitV (v_m, v_r, v_w) -> (mem, UnitV (memvmod a v_m, readvmod a v_r, writevmod a v_w))
+    | DerefRP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p a in
+                            (mem_set mem' id v', RefV id)
+    | AccessRP (p, id), TupleV vs -> let (mem', v') = valupd mem (List.nth vs id) p a in
                                      (mem', TupleV (list_replace vs id v'))
     | _, _ -> raise @@ Typing_error "valupd"
 
   (* - value combination *)
 
+  let memvalcomb (u : memval) (v : memval) : memval =
+    match u, v with
+      | ZeroMV, ZeroMV -> ZeroMV
+      | BotMV, BotMV -> BotMV
+      | _, _ -> SmthMV
+
+  let readvalcomb (u : readval) (v : readval) : readval =
+    match u, v with
+      | TopRV, TopRV -> TopRV
+      | ZeroRV, ZeroRV -> ZeroRV
+      | TopRV, ZeroRV -> ZeroRV
+      | ZeroRV, TopRV -> ZeroRV
+      | _, _ -> OneRV
+
+  let writevalcomb (u : writeval) (v : writeval) : writeval =
+    match u, v with
+      | OneWV, OneWV -> OneWV
+      | ZeroWV, ZeroWV -> ZeroWV
+      | _, _ -> SmthWV
+
   let rec valcomb (u : value) (v : value) : value =
-    if is_trivial_v u && is_trivial_v v
-    then (if u == v then u else BotV)
-    else match u, v with
-      | FunV ustmts, FunV vstmts  -> FunV (ustmts @ vstmts)
+    match u, v with
+      | UnitV (u_m, u_r, u_w), UnitV (v_m, v_r, v_w) ->
+        UnitV (memvalcomb u_m v_m, readvalcomb u_r v_r, writevalcomb u_w v_w)
+      | FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts)
       | RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref"
       | TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs)
       | _, _ -> raise @@ Typing_error "valcomb"
@@ -246,7 +292,7 @@ struct
   (* - expression evaluation *)
 
   let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with
-    | UnitE -> ZeroV
+    | UnitE -> UnitV (ZeroMV, ZeroRV, ZeroWV)
     | PathE p -> pathval mem vals p
     | RefE x -> RefV (vals_assoc x vals)
     | TupleE es -> TupleV (List.map (exprval mem vals) es)
@@ -287,48 +333,64 @@ struct
 
   (* - call values spoil *)
 
-  (* TODO: check all cases *)
-  let is_correct_tags (v : value) (r : read_cap) (w : write_cap)
-                      (r' : read_cap) (w' : write_cap) (m : mode)
-                      (c : copy_cap) : bool =
-    (* FIXME TMP *)
-    (* Printf.printf "%b %b %b %b %b\n" *)
-      (* (r != Rd || v == ZeroV) *)
-      (* (r != Rd || fst m == In) *)
-      (* (snd m != Out || w == AlwaysWr) *)
-      (* (* TODO: FIXME: why always write ?? *) *)
-      (* (((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr)) *)
-      (* (is_trivial_v v); *)
-    (r != Rd || v == ZeroV) &&
-    (r != Rd || fst m == In) &&
+  (* TODO: check assignment type matches types separately later ?? *)
+  let is_correct_tags (r : read_cap) (w : write_cap)
+                      (m : mode) (c : copy_cap) : bool =
+    (snd m != Out || c == Rf) &&
     (snd m != Out || w == AlwaysWr) &&
-    (* TODO: FIXME: check *)
-    ((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr) &&
-    is_trivial_v v
+    (r != Rd || fst m == In)
+
+  let tryread (r : read_cap) (v_m : memval)
+              (v_r : readval) (v_w : writeval) : value =
+    match r with
+      | Rd -> UnitV (memvmod ReadA v_m,
+                     readvmod ReadA v_r,
+                     writevmod ReadA v_w)
+      | NRd -> UnitV (v_m, v_r, v_w) 
+  
+  let tryspoil (m : mode) (w : write_cap) (v_m : memval) : memval =
+    match m, w with
+      | (_, Out), AlwaysWr -> v_m
+      | (_, Out), MayWr -> v_m
+      | (_, NOut), AlwaysWr -> BotMV
+      | (_, NOut), MayWr -> SmthMV
+      | _ -> raise @@ Typing_error "tryspoil: unexpected pair mode + write cap"
 
   let rec valspoil (mem : mem) (v : value) (t : atype)
-                   (u : atype) (m : mode) (c : copy_cap)
-                   : mem * value = match t, u, v with
-    | UnitT (r, w), UnitT (r', w'), _ ->
-      if not @@ is_trivial_v v
-        then raise @@ Typing_error "valspoil: unit, not trivial"
-      else if not @@ is_correct_tags v r w r' w' m c
-        then raise @@ Typing_error "valspoil: unit, not correct"
-      else if snd m == NOut && c == Rf && (w == AlwaysWr || w == MayWr)
-        then (mem, BotV)
-      else if snd m == Out && w == AlwaysWr
-        then (mem, ZeroV)
-      else (mem, v)
-    | FunT ts, FunT us, FunV _ -> if ts == us then (mem, v) else raise @@ Typing_error "valspoil: fun"
-    | RefT (ct, t), RefT (cu, u), RefV id ->
-      let (mem', v') = valspoil mem (mem_get mem id) t u m ct in
+                   (m : mode) (c : copy_cap)
+                   : mem * value = match t, v with
+    | UnitT (r, w), UnitV (v_m, v_r, v_w) ->
+      if not @@ is_correct_tags r w m c
+        then raise @@ Typing_error "valspoil: trivial type tags combination is not correct"
+      else
+        let v' = tryread r v_m v_r v_w in
+        if c == Cp || w == NeverWr
+          then (mem, v')
+        else (match v' with
+          | UnitV (v_m', v_r', v_w') ->
+            let (v_m'', v_r'', v_w'') =
+              (if w == AlwaysWr
+                then (memvmod AlwaysWriteA v_m',
+                      readvmod AlwaysWriteA v_r',
+                      writevmod AlwaysWriteA v_w')
+                else (* MayWr *)
+                     (memvmod MayWriteA v_m',
+                      readvmod MayWriteA v_r',
+                      writevmod MayWriteA v_w'))
+            in
+            let v_m''' = tryspoil m w v_m'' in
+            (mem, UnitV (v_m''', v_r'', v_w''))
+          | _ -> raise @@ Typing_error "valspoil: value after tryread is not unit")
+    | FunT ts, FunV _ -> (mem, v)
+    | RefT (ct, t), RefV id ->
+      let (mem', v') = valspoil mem (mem_get mem id) t m ct in
       (mem_set mem id v', RefV id)
-    | TupleT ts, TupleT us, TupleV vs ->
-        let folder = fun (mem, vs') t u v ->
-          let (mem', v') = valspoil mem v t u m c in (mem', v' :: vs') in
-        let (mem', vs') = list_foldl3 folder (mem, []) ts us vs in
+    | TupleT ts, TupleV vs ->
+        let folder = fun (mem, vs') t v ->
+          let (mem', v') = valspoil mem v t m c in (mem', v' :: vs') in
+        let (mem', vs') = List.fold_left2 folder (mem, []) ts vs in
         (mem', TupleV (List.rev vs'))
-    | _, _, _ ->  raise @@ Typing_error "valspoil"
+    | _, _ ->  raise @@ Typing_error "valspoil"
 
   (* full spoil *)
 
@@ -337,11 +399,11 @@ struct
     let x = pathvar p in
     let id = vals_assoc x vals in (* base var address *)
     let b = pathval mem vals p in (* subvalue in var *)
-    let t' = pathtype types p in (* type of subvalue *)
-    let (mem', b') = valspoil mem b t t' m Cp in (* spoil subvalue *)
+    (* let t' = pathtype types p in (* type of subvalue *) *)
+    let (mem', b') = valspoil mem b t m Cp in (* spoil subvalue *)
     (* TODO: FIXME: why copy (Cp)? maybe sometimes use top-level capability ? *)
     let pi = pathrev p VarRP in
-    let (mem'', v'') = valupd mem' (mem_get mem' id) pi b' in (* set subvalue into var *)
+    let (mem'', v'') = valchange mem' (mem_get mem' id) pi b' in (* set subvalue into var *)
     mem_set mem'' id v''
 
   let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
@@ -369,15 +431,34 @@ struct
   (* NOTE: not needed due to performed optimization in stmt_eval *)
   (* let func_eval (mem : mem) (vals : vals) (s : stmt) (ts : mtype list) (es : expr list) = *)
 
+  let writeval_to_cap (v_w : writeval) : write_cap =
+    match v_w with
+      | ZeroWV -> NeverWr
+      | SmthWV -> MayWr
+      | OneWV -> AlwaysWr
+
+  let rec tags_check (mem : mem) (v : value) (t : atype) : unit =
+    match v, t with
+      | UnitV (v_m, v_r, v_w), UnitT (r, w) ->
+        if (r == Rd) && (v_r != OneRV)
+          then raise @@ Eval_error "tags_check: wrong read tag"
+        else if (r == NRd) && (v_r == OneRV)
+          then raise @@ Eval_error "tags_check: wrong not read tag"
+        else if writeval_to_cap v_w != w
+          then raise @@ Eval_error "tags_check: wrong write tag"
+        else ()
+      | FunV _, FunT _ -> ()
+      | RefV id, RefT (_, t) -> tags_check mem (mem_get mem id) t
+      | TupleV vs, TupleT ts -> ignore @@ List.map2 (tags_check mem) vs ts
+      | _, _ -> raise @@ Typing_error "tags_check"
+
   (* - statement evaluation *)
 
   let rec stmt_eval (state : state) (s : stmt) : state =
     match state with (mem, types, vals, visited) -> match s with
     | SkipS -> state
-    | CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *)
-                               pathval mem vals f in
-                       let t = (* FIXME TMP Printf.printf "call, before t\n"; *)
-                               pathtype types f in
+    | CallS (f, es) -> let v = pathval mem vals f in
+                       let t = pathtype types f in
                        let types' : types = (fst types, fst types) in
                        let vals' : vals = (fst vals, fst vals) in
                        (match v, t with
@@ -394,7 +475,14 @@ struct
                                                     if List.mem stmt visited_old
                                                     then stmt :: visited_old
                                                     else match stmt_eval (mem_swa, types_swa, vals_swa, stmt :: visited_old) stmt with
-                                                      (_, _, _, visited_after_stmt) -> visited_after_stmt)
+                                                      (mem_after_stmt, _, vals_after_stmt, visited_after_stmt) ->
+                                                        ignore @@ List.fold_left
+                                                          (fun x (_, t) ->
+                                                             let id = vals_assoc x vals_after_stmt in
+                                                             let v = mem_get mem_after_stmt id in
+                                                             tags_check mem_after_stmt v t; x + 1)
+                                                          0 ts;
+                                                        visited_after_stmt)
                                                  visited_swa
                                                  fstmts in
                              let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *)
@@ -412,16 +500,28 @@ struct
                        else let x = pathvar p in
                             let id = vals_assoc x vals in
                             let pi = pathrev p VarRP in
-                            let (mem', v') = valupd mem (mem_get mem id) pi ZeroV in
+                            let (mem', v') = valupd mem (mem_get mem id) pi AlwaysWriteA in
                             (mem_set mem' id v', types, vals, visited)
                      | RefT _ -> raise @@ Eval_error "write: ref type"
                      | TupleT _ -> raise @@ Eval_error "write: tuple type"
                      | _ -> raise @@ Eval_error "write: type")
-    | ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV 
-                 then raise @@ Eval_error "read: spoiled value"
-                 else if pathval mem vals p != ZeroV 
-                 then raise @@ Eval_error "read: nontrivial value"
-                 else state
+    | ReadS p -> (match pathtype types p with
+                    | UnitT (_, _) ->
+                      (* NOTE: not required *)
+                      (* if r == NRd *)
+                      (* then raise @@ Eval_error "read: not read tag" *)
+                      (* else *)
+                      let x = pathvar p in
+                      let id = vals_assoc x vals in
+                      let pi = pathrev p VarRP in
+                      let (mem', v') = valupd mem (mem_get mem id) pi ReadA in
+                      (mem_set mem' id v', types, vals, visited)
+                    | RefT _ -> raise @@ Eval_error "read: ref type"
+                    | TupleT _ -> raise @@ Eval_error "read: tuple type"
+                    | _ -> raise @@ Eval_error "read: type")
+                 (* NOTE: handled inside through undefined in memvmod *)
+                 (* if pathval mem vals p == SmthV || pathval mem vals p == BotV *) 
+                 (* then raise @@ Eval_error "read: spoiled value" *)
     | SeqS (sl, sr) -> let statel = stmt_eval state sl in
                        stmt_eval statel sr
     | ChoiceS (sl, sr) -> let statel = stmt_eval state sl in
@@ -470,6 +570,7 @@ struct
   let vg8 = VarP (globals_min_id + 8)
   let vg9 = VarP (globals_min_id + 9)
   let vg10 = VarP (globals_min_id + 10)
+  let vg11 = VarP (globals_min_id + 11)
 
   let rf0E = RefE 0
   let rf1E = RefE 1
@@ -518,23 +619,30 @@ struct
   let rdS p = ReadS p 
   let callS f args = CallS (f, args)
 
+  let uV m = UnitV (m, ZeroRV, ZeroWV)
+
   (* - utils tests *)
 
+  let v_memval_is v m =
+    match v with
+     | UnitV (v_m, _, _) -> v_m == m
+     | _ -> false
+
   let%expect_test "mem add / get / set" =
     let mem = empty_mem in
-    let (mem, id1) = mem_add mem ZeroV in 
-    let (mem, id2) = mem_add mem SmthV in 
-    let (mem, id3) = mem_add mem BotV in 
+    let (mem, id1) = mem_add mem @@ uV ZeroMV in 
+    let (mem, id2) = mem_add mem @@ uV SmthMV in 
+    let (mem, id3) = mem_add mem @@ uV BotMV in 
     Printf.printf "%i %i %i " id1 id2 id3;
-    Printf.printf "%b %b %b " (mem_get mem id1 == ZeroV)
-                              (mem_get mem id2 == SmthV)
-                              (mem_get mem id3 == BotV);
-    let mem = mem_set mem id1 BotV in 
-    let mem = mem_set mem id2 ZeroV in 
-    let mem = mem_set mem id3 SmthV in 
-    Printf.printf "%b %b %b" (mem_get mem id1 == BotV)
-                              (mem_get mem id2 == ZeroV)
-                              (mem_get mem id3 == SmthV);
+    Printf.printf "%b %b %b " (v_memval_is (mem_get mem id1) ZeroMV)
+                              (v_memval_is (mem_get mem id2) SmthMV)
+                              (v_memval_is (mem_get mem id3) BotMV);
+    let mem = mem_set mem id1 @@ uV BotMV in 
+    let mem = mem_set mem id2 @@ uV ZeroMV in 
+    let mem = mem_set mem id3 @@ uV SmthMV in 
+    Printf.printf "%b %b %b" (v_memval_is (mem_get mem id1) BotMV)
+                             (v_memval_is (mem_get mem id2) ZeroMV)
+                             (v_memval_is (mem_get mem id3) SmthMV);
     [%expect {| 0 1 2 true true true true true true |}]
 
   (* - basic var tests *)
@@ -555,7 +663,7 @@ struct
                          ReadS (VarP globals_min_id));
          [%expect.unreachable]);
     with Eval_error msg -> Printf.printf "%s" msg;
-    [%expect {| read: spoiled value |}]
+    [%expect {| memvmod: forbidden read |}]
 
   let%expect_test "simple vars, no read & read" =
     prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE);
@@ -621,10 +729,10 @@ struct
   let%expect_test "simple call with write, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_mw;
-        defg (rfT uT_r_mw) rfg0E;
+        defgu uT_aw;
+        defg (rfT uT_aw) rfg0E;
         FunD (
-          [moded @@ cpT @@ uT_r_mw],
+          [moded @@ cpT @@ uT_aw],
           wrS @@ drf @@ v0
         )
       ],
@@ -636,10 +744,10 @@ struct
   let%expect_test "simple call with read after write, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_mw;
-        defg (rfT uT_r_mw) rfg0E;
+        defgu uT_aw;
+        defg (rfT uT_aw) rfg0E;
         FunD (
-          [moded @@ cpT @@ uT_mw],
+          [moded @@ cpT @@ uT_aw],
           (wrS @@ drf @@ v0) #.
           (rdS @@ drf @@ v0)
         )
@@ -696,7 +804,7 @@ struct
     );
     [%expect.unreachable]);
     with Eval_error msg -> Printf.printf "%s" msg;
-    [%expect {| read: spoiled value |}]
+    [%expect {| memvmod: forbidden read |}]
 
   let%expect_test "simple call with write to ref with fix, dsl" =
     prog_eval_noret (
@@ -779,9 +887,9 @@ struct
     prog_eval_noret (
       [
         defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg (rfT uT_r) rfg0E;
         FunD (
-          [moded @@ cpT @@ uT_aw],
+          [moded @@ cpT @@ uT],
           (wrS @@ vg0) #.
           (rdS @@ drf @@ vg1)
         )
@@ -795,10 +903,10 @@ struct
   let%expect_test "simple call with read & write (2 args), dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg2E;
+        defgu uT_r;
+        defg (rfT uT_r) rfg0E;
+        defgu uT_aw;
+        defg (rfT uT_aw) rfg2E;
         FunD (
           [
             moded @@ rfT @@ uT_r;
@@ -826,10 +934,10 @@ struct
         defg (rfT uT_r_aw) rfg6E;
         FunD (
           [
-            ((NIn, NOut), cpT @@ uT_aw);
+            ((NIn, NOut), cpT @@ uT);
             ((In, NOut), cpT @@ uT_r_aw);
-            ((NIn, Out), cpT @@ uT_aw);
-            ((In, Out), cpT @@ uT_r_aw);
+            ((NIn, Out), rfT @@ uT_aw);
+            ((In, Out), rfT @@ uT_r_aw);
           ],
           (rdS @@ drf @@ v1) #.
           (rdS @@ drf @@ v3) #.
@@ -850,10 +958,10 @@ struct
   let%expect_test "simple call with different arguments modifiers, ref, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg2E;
+        defgu uT_r;
+        defg (rfT uT_r) rfg0E;
+        defgu uT_r;
+        defg (rfT uT_r) rfg2E;
         defgu uT_r_aw;
         defg (rfT uT_r_aw) rfg4E;
         defgu uT_r_aw;
@@ -880,83 +988,195 @@ struct
     Printf.printf "done!";
     [%expect {| done! |}]
 
-  (* - complex tests *)
+  (* - tests for presentation *)
 
-  (* NOTE: path access isreversed to intuitive function application
-           by definition *)
-  let%expect_test "complex test: send, dsl" =
+  let%expect_test "presentation test 1 (simple types), dsl" =
     prog_eval_noret (
-      (* TODO: set optimal ref mods later *)
-      let user_utilsT = TupleT [uT_r_aw (* 0 id *); uT_r_aw] in
-      let user_infoT =  TupleT [uT_r_aw (* 0 name *); uT_r_aw; uT_r_aw] in
-      let userT = TupleT [cpT user_utilsT (* 0 utils *); cpT user_infoT (* 1 info *)] in
-      let versionT = TupleT [uT_r_aw (* 0 id *); uT_r_aw; uT_r_aw] in
-      let utilsT = TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] in
-      let requestT = TupleT [cpT userT (* 0 user *);
-                             cpT versionT (* 1 version *);
-                             cpT utilsT (* 2 utils *);
-                             cpT uT_r_aw (* 3 data *);
-                             uT_r_aw (* 4 operation_date *)] in
-      let user_utilsE = TupleE [UnitE (* 0 id *); UnitE] in
-      let user_infoE =  TupleE [UnitE (* 0 name *); UnitE; UnitE] in
-      let userE = TupleE [rfg0E (* 0 utils *); rfg1E (* 1 info *)] in
-      let versionE = TupleE [UnitE (* 0 id *); UnitE; UnitE] in
-      let utilsE = TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] in
-      let requestE = TupleE [rfg2E (* 0 user *);
-                             rfg3E (* 1 version *);
-                             rfg4E (* 2 utils *);
-                             rfg5E (* 3 data *);
-                             UnitE (* 4 operation_date *)] in
-      let get_version_idID = vg7 in
-      let updated_versionID = vg8 in
-      let sendID = vg9 in
-      let send_allID = vg10 in
-      let get_version_idF = FunD ([moded requestT],
-        (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in
-      let updated_versionF = FunD ([moded requestT],
-        (rdS @@ access 0 @@ drf @@ access 2 v0) #.
-        (* TODO: read all the substructure ?? *)
-        (rdS @@ access 0 @@ drf @@ access 1 v0) #.
-        (rdS @@ access 1 @@ drf @@ access 1 v0)) in
-      let sendF = FunD ([moded requestT],
-        ((
-           (wrS @@ access 0 @@ drf @@ access 2 v0) #.
-           (rdS @@ drf @@ access 3 v0) #.
-           (wrS @@ drf @@ access 3 v0) #.
-           (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0)
-         ) |. skp) #.
-         (wrS @@ access 4 v0) #.
-         (* TODO: read all the substructure ?? *)
-         (rdS @@ access 4 v0) (*rdS v0*)) in (* FIXME: TMP, parial read, should be full *)
-      let send_allF = FunD ([moded requestT],
-        (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *)
-        (callS sendID [pE v0]) #.
-        (callS get_version_idID [pE v0]) #.
-        (callS updated_versionID [pE v0]) #.
-        (* TODO: read all the substructure ?? *)
-        (wrS @@ access 0 @@ drf @@ access 1 v0) #.
-        (wrS @@ access 1 @@ drf @@ access 1 v0) #.
-        (* --- *)
-        ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |.
-         (rdS @@ access 0 @@ drf @@ access 1 v0))) in
-      let varID = vg6 in
       [
-        defg user_utilsT user_utilsE;
-        defg user_infoT user_infoE;
-        defg userT userE;
-        defg versionT versionE;
-        defg utilsT utilsE;
         defgu uT_r_aw;
-        defg requestT requestE;
-        get_version_idF;
-        updated_versionF;
-        sendF;
-        send_allF
+        defg (rfT uT_r_aw) rfg0E; (* x *)
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg2E; (* y *)
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg4E; (* z *)
+        defgu uT_r_aw;
+        defg (rfT uT_r_aw) rfg6E; (* k *)
+        FunD ( (* f *)
+          [
+            (moded @@ rfT @@ uT_r_aw);
+            (moded @@ rfT @@ uT_r);
+          ],
+          (rdS @@ drf @@ v0) #.
+          (wrS @@ drf @@ v0) #.
+          (rdS @@ drf @@ v1)
+        );
+        FunD ( (* w *)
+          [
+            (moded @@ cpT @@ uT_mw);
+          ],
+          (wrS @@ drf @@ v0) |. skp
+        );
+        FunD ( (* g *)
+          [
+            (moded @@ rfT @@ uT_aw);
+            (moded @@ cpT @@ uT_r_mw);
+          ],
+          (wrS @@ drf @@ v0) #.
+          ((wrS @@ drf @@ v1) |. (wrS @@ drf @@ v0)) #.
+          (rdS @@ drf @@ v0) #.
+          (rdS @@ drf @@ v1)
+        );
+        FunD ( (* r *)
+          [
+            (moded @@ rfT @@ uT_r);
+          ],
+          (rdS @@ drf @@ v0)
+        )
       ],
-      callS send_allID [pE varID]
+      let xV = vg1 in
+      let yV = vg3 in
+      let zV = vg5 in
+      let kV = vg7 in
+      let fF = vg8 in
+      let wF = vg9 in
+      let gF = vg10 in
+      let rF = vg11 in
+      (callS wF [pE xV]) #.
+      (callS rF [pE xV]) #.
+      (callS fF [pE xV; pE yV]) #.
+      (callS rF [pE yV]) #.
+      (callS gF [pE zV; pE kV]) #.
+      (wrS @@ drf @@ zV) #.
+      (callS wF [pE zV]) #.
+      (callS fF [pE yV; pE zV]) #.
+      (callS rF [pE kV])
     );
     Printf.printf "done!";
     [%expect {| done! |}]
 
+  (* TODO tags, access *)
+  (* let%expect_test "presentation test 2 (complex types), dsl" = *)
+    (* prog_eval_noret ( *)
+      (* let userT = TupleT [uT_r_aw; uT_r_aw; uT_r_aw] in *)
+      (* let dataT =  TupleT [uT_r_aw; uT_r_aw] in *)
+      (* let requestT = TupleT [cpT userT; *)
+                             (* cpT dataT; *)
+                             (* cpT dataT] in *)
+      (* let requestArgsT = TupleT [cpT userT; (* TODO: tags *) *)
+                                 (* cpT dataT; *)
+                                 (* cpT dataT] in *)
+      (* let userE = TupleE [UnitE; UnitE; UnitE] in *)
+      (* let dataE =  TupleE [UnitE; UnitE] in *)
+      (* let requestE = TupleE [rfg0E; rfg1E; rfg2E] in *)
+      (* [ *)
+        (* defg userT userE; *)
+        (* defg dataT dataE; *)
+        (* defgu uT_r_aw; (* time *) *)
+        (* defg requestT requestE; *)
+        (* FunD ( (* send *) *)
+          (* [ *)
+            (* (moded @@ requestArgsT) *)
+          (* ], *)
+          (* ( *)
+          (* ( (* TODO access *) *)
+            (* (rdS @@ drf @@ v0) #. *)
+            (* (wrS @@ drf @@ v0) #. *)
+            (* (rdS @@ drf @@ v0) #. *)
+            (* (wrS @@ drf @@ v0) *)
+          (* ) |. *)
+          (* skp) #. *)
+          (* TODO access *)
+          (* (wrS @@ drf @@ v0) #. *)
+          (* (rdS @@ drf @@ v1) *)
+        (* ); *)
+      (* ], *)
+      (* (callS vg4 [pE vg3]) #. *)
+      (* TODO access *)
+      (* (wrS @@ drf @@ vg3) #. *)
+      (* ((rdS @@ drf @@ vg3) |. (rdS @@ drf @@ vg3)) #. *)
+      (* (rdS @@ drf @@ vg3) *)
+    (* ); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* - complex tests *)
+
+  (* TODO: FIXME: rw tags *)
+  (* NOTE: path access isreversed to intuitive function application
+           by definition *)
+  (* let%expect_test "complex test: send, dsl" = *)
+    (* prog_eval_noret ( *)
+      (* TODO: set optimal ref mods later *)
+      (* let user_utilsT = TupleT [uT_r_aw (* 0 id *); uT_r_aw] in *)
+      (* let user_infoT =  TupleT [uT_r_aw (* 0 name *); uT_r_aw; uT_r_aw] in *)
+      (* let userT = TupleT [cpT user_utilsT (* 0 utils *); cpT user_infoT (* 1 info *)] in *)
+      (* let versionT = TupleT [uT_r_aw (* 0 id *); uT_r_aw; uT_r_aw] in *)
+      (* let utilsT = TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] in *)
+      (* let requestT = TupleT [cpT userT (* 0 user *); *)
+                             (* cpT versionT (* 1 version *); *)
+                             (* cpT utilsT (* 2 utils *); *)
+                             (* cpT uT_r_aw (* 3 data *); *)
+                             (* uT_r_aw (* 4 operation_date *)] in *)
+      (* let user_utilsE = TupleE [UnitE (* 0 id *); UnitE] in *)
+      (* let user_infoE =  TupleE [UnitE (* 0 name *); UnitE; UnitE] in *)
+      (* let userE = TupleE [rfg0E (* 0 utils *); rfg1E (* 1 info *)] in *)
+      (* let versionE = TupleE [UnitE (* 0 id *); UnitE; UnitE] in *)
+      (* let utilsE = TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] in *)
+      (* let requestE = TupleE [rfg2E (* 0 user *); *)
+                             (* rfg3E (* 1 version *); *)
+                             (* rfg4E (* 2 utils *); *)
+                             (* rfg5E (* 3 data *); *)
+                             (* UnitE (* 4 operation_date *)] in *)
+      (* let get_version_idID = vg7 in *)
+      (* let updated_versionID = vg8 in *)
+      (* let sendID = vg9 in *)
+      (* let send_allID = vg10 in *)
+      (* let get_version_idF = FunD ([moded requestT], *)
+        (* (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in *)
+      (* let updated_versionF = FunD ([moded requestT], *)
+        (* (rdS @@ access 0 @@ drf @@ access 2 v0) #. *)
+        (* TODO: read all the substructure ?? *)
+        (* (rdS @@ access 0 @@ drf @@ access 1 v0) #. *)
+        (* (rdS @@ access 1 @@ drf @@ access 1 v0)) in *)
+      (* let sendF = FunD ([moded requestT], *)
+        (* (( *)
+           (* (wrS @@ access 0 @@ drf @@ access 2 v0) #. *)
+           (* (rdS @@ drf @@ access 3 v0) #. *)
+           (* (wrS @@ drf @@ access 3 v0) #. *)
+           (* (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0) *)
+         (* ) |. skp) #. *)
+         (* (wrS @@ access 4 v0) #. *)
+         (* TODO: read all the substructure ?? *)
+         (* (rdS @@ access 4 v0) (*rdS v0*)) in (* FIXME: TMP, parial read, should be full *) *)
+      (* let send_allF = FunD ([moded requestT], *)
+        (* (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *) *)
+        (* (callS sendID [pE v0]) #. *)
+        (* (callS get_version_idID [pE v0]) #. *)
+        (* (callS updated_versionID [pE v0]) #. *)
+        (* TODO: read all the substructure ?? *)
+        (* (wrS @@ access 0 @@ drf @@ access 1 v0) #. *)
+        (* (wrS @@ access 1 @@ drf @@ access 1 v0) #. *)
+        (* --- *)
+        (* ((rdS @@ access 0 @@ drf @@ access 0 @@ drf @@ access 0 v0) |. *)
+         (* (rdS @@ access 0 @@ drf @@ access 1 v0))) in *)
+      (* let varID = vg6 in *)
+      (* [ *)
+        (* defg user_utilsT user_utilsE; *)
+        (* defg user_infoT user_infoE; *)
+        (* defg userT userE; *)
+        (* defg versionT versionE; *)
+        (* defg utilsT utilsE; *)
+        (* defgu uT_r_aw; *)
+        (* defg requestT requestE; *)
+        (* get_version_idF; *)
+        (* updated_versionF; *)
+        (* sendF; *)
+        (* send_allF *)
+      (* ], *)
+      (* callS send_allID [pE varID] *)
+    (* ); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
   (* TODO: version with more optimal modifiers *)
 end

model_with_structures/model.typ

@@ -13,7 +13,7 @@
 
 == Syntax
 
-*TODO: top-level value copy mode ??* // TODO: FIXME
+// *TODO: top-level value copy mode ??* // TODO: FIXME
 
 *TODO: add formal global env to all types and vals (as in code) ??* // TODO: FIXME
 
@@ -48,6 +48,9 @@
 #let cl = $chevron.l$
 #let cr = $chevron.r$
 
+#let cdl = $chevron.l.double$
+#let cdr = $chevron.r.double$
+
 #let expr = `expr`
 #let stmt = `stmt`
 #let decl = `decl`
@@ -151,55 +154,73 @@
 
 == Value Model
 
-#let deepValue = `deepvalue`
+// #let deepValue = `deepvalue`
 #let value = `value`
+#let vmem = $v_#[`mem`]$
+#let vread = $v_#[`read`]$
+#let vwrite = $v_#[`write`]$
 #let revpath = $#[`path`]_#[`rev`]$
 
 #bnf(
+  // Prod(
+  //   $deepValue$,
+  //   {
+  //     Or[$0$][valid value of simple type] // `Unit`
+  //     Or[$\#$][valid or spoiled value of simple type] // `Unit`
+  //     Or[$bot$][spoiled value of simple type] // `Unit`
+  //     Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun`
+  //     Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref`
+  //     Or[$[deepValue+]$][tuple value] // `Prod`
+  //   }
+  // ),
   Prod(
-    $deepValue$,
+    $vmem$,
     {
-      Or[$0$][valid value of simple type] // `Unit`
-      Or[$\#$][valid or spoiled value of simple type] // `Unit`
-      Or[$bot$][spoiled value of simple type] // `Unit`
-      Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun`
-      Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref`
-      Or[$[deepValue+]$][tuple value] // `Prod`
+      Or[$0$][valid value of simple type]
+      Or[$?$][valid or spoiled value of simple type]
+      Or[$bot$][spoiled value of simple type]
+      // NOTE: proably can't use correctly
+      // Or[$top$][value that is not spoiled because of the copy tag]
+    }
+  ),
+  Prod(
+    $vread$,
+    {
+      Or[$0_r$][argument not read]
+      Or[$1_r$][argument read]
+      Or[$top_r$][argument already written from the function beginning]
+    }
+  ),
+  Prod(
+    $vwrite$,
+    {
+      Or[$0_w$][no write]
+      Or[$?_w$][maybe write]
+      Or[$1_w$][always write]
     }
   ),
   Prod(
     $value_mu$,
     {
-      Or[$0$][valid value of simple type] // `Unit`
-      Or[$\#$][valid or spoiled value of simple type] // `Unit`
-      Or[$bot$][spoiled value of simple type] // `Unit`
+      Or[$cdl vmem, vread, vwrite cdr$][value of the simple type, contains cells for analysis] // `Unit`
       Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun`
       Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
       Or[$[value+]$][tuple value] // `Prod`
     }
   ),
-  Prod(
-    revpath,
-    {
-      Or[$\# .$][value by itself]
-      Or[$rf revpath$][reference to value]
-      Or[$n . revpath$][tuple with value as $n$-th element]
-    }
-  ),
 )
 
-#deepValue - полное значение, #value - слой значения, привязан к конкретной памяти $mu$
+// #deepValue - полное значение,
+#value - слой значения, привязан к конкретной памяти $mu$
 
 Значения, могут лежать в переменных и передаваться как аргументы функций (то, во что вычисляется $expr$)
 
-$revpath$ - путь в обратную сторону, используется для обновления значений
-
 $v in value$ - произвольное значение
 
-Получение #deepValue по #value:
-- $rf l xarrowSquiggly(mu)_#[deep] rf mu[l]$
-- $* xarrowSquiggly(mu)_#[deep] *$
-где $*$ - произвольный конструктор значения, кроме $rf$
+// Получение #deepValue по #value:
+// - $rf l xarrowSquiggly(mu)_#[deep] rf mu[l]$
+// - $* xarrowSquiggly(mu)_#[deep] *$
+// где $*$ - произвольный конструктор значения, кроме $rf$
 
 == Memory Model
 
@@ -223,13 +244,44 @@ $v in value$ - произвольное значение
 
 == Semantics
 
+#let action = `action`
+#let readA = $#[`READ`]_a$
+#let writeA = $#[`WRITE`]_a$
+#let mbwriteA = $#[`MAYWRITE`]_a$
+// #let spoilA = $#[`SPOIL`]_a$
+// #let nospoilA = $#[`NOSPOIL`]_a$
+
+#bnf(
+  Prod(
+    revpath,
+    {
+      Or[$\# .$][value by itself]
+      Or[$rf revpath$][reference to value]
+      Or[$n . revpath$][tuple with value as $n$-th element]
+    }
+  ),
+  Prod(
+    $action$,
+    {
+      Or[$readA$][value read]
+      Or[$writeA$][value written]
+      Or[$mbwriteA$][value maybe written]
+      // NOTE: not required, spoils only first element ?
+      // Or[$spoilA$][value passed as funciton argument and spoiled]
+      // NOTE: probably acutally can't reliebly forbid Cp
+      // Or[$nospoilA$][value passed as funciton argument and not changed,
+      //                but could be spoiled if mode will be $Copy$ instead of $Ref$]
+      // TODO: better wording ??
+    }
+  ),
+)
+
 // TODO: FIXME: add vars & funcs from global context in the beginnning
 
 // $V := memelem$ - значения памяти
 
 $X$ - можество переменных
 
-
 #let vals = $Sigma$
 #let types = $Gamma$
 #let envv = $#[env]_Sigma$
@@ -237,6 +289,11 @@ $X$ - можество переменных
 $sigma : envv := X -> LL, space vals : envv$ - #[ метки памяти перменных контекста, частично определённая функция ]
 $sigma : envt := X -> type, space types : envt$ - #[ типы значений перменных контекста, частично определённая функция ]
 
+$revpath$ - путь в обратную сторону, используется для обновления значений
+
+$action$ - действия, совершаемые с примитивным значением,
+           модифицирующие содержащуюся таминформацию
+
 // $DD : X -> decl$ - глобальные определения, частично определённая функция
 
 // $d in decl, $
@@ -437,7 +494,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 //     // $sigma temode x -> cr r' space w' cl$, // NOTE: not required, value passed
 //     $(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
 //     // $sigma, mu teval x eqmu v$, // NOTE: not required, value passed
-//     $v in {0, \#, bot}$,
+//     $v in {0, ?, bot}$,
 //     $r = Read => v = 0$,
 //     $types, vals, mu, m, c tcorrect v : cl r', w' cr -> cl r, w cr$,
 //   )
@@ -485,18 +542,33 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ new trivial read value],
 
-    $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl Read \, w cr)_new cl v, mu cr$,
+    $v_m in {0, ?, bot}$,
+    $cl cdl v_m, v_r, v_w cdr, mu cr
+     xarrowSquiggly(cl Read \, w cr)_new
+     cl cdl v_m, 0, 0 cdr, mu cr$,
   )
 ))
 
+// #align(center, prooftree(
+//   vertical-spacing: 4pt,
+//   rule(
+//     name: [ new trivial read $top$ value],
+
+//     $cl cdl top, v_r, v_w cdr, mu cr
+//      xarrowSquiggly(cl Read \, w cr)_new
+//      cl cdl 0, 0, 0 cdr, mu cr$,
+//   )
+// ))
+
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ new trivial $not$ read value],
 
-    $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl not Read \, w cr)_new cl bot, mu cr$,
+    $v_m in {0, ?, bot/*, top */}$,
+    $cl cdl v_m, v_r, v_w cdr, mu cr
+     xarrowSquiggly(cl not Read \, w cr)_new
+     cl cdl bot, 0, 0 cdr, mu cr$,
   )
 ))
 
@@ -505,32 +577,30 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ new funciton pointer value],
 
-    $cl lambda overline(t) s, mu cr xarrowSquiggly(lambda space c space overline(t))_new cl lambda overline(t) s, mu cr$,
+    $cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_new cl lambda overline(s), mu cr$,
   )
 ))
 
+// #align(center, prooftree(
+//   vertical-spacing: 4pt,
+//   rule(
+//     name: [ new reference ref value],
+
+//     $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
+//   )
+// ))
+
+// NOTE: due to new memory cells types (with rw subcells) valnue should always be copied
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ new reference ref value],
-
-    // TODO: FIXME: recursive copy ?? (what heppens if ref field has copy substructure ??)
-    // <- forbidden ??
-
-    $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
-  )
-))
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ new reference copy value],
+    name: [ new reference /* copy */ value],
 
     $cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$,
 
     $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
 
-    $cl rf l, mu cr xarrowSquiggly(rf Copy t)_new cl rf l', mu_a cr$,
+    $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_new cl rf l', mu_a cr$,
   )
 ))
 
@@ -547,18 +617,108 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   )
 ))
 
+=== Action Rules
+
+#let modM = $attach(<-, br: m)$
+#let modR = $attach(<-, br: r)$
+#let modW = $attach(<-, br: w)$
+
+#align(center, grid(
+  columns: 3,
+  gutter: 10%,
+  align: center,
+  table(
+    columns: 3,
+    table.header(
+      [*a*], [*x*], $modM$
+    ),
+    $readA$, $0$, $0$,
+    // $readA$, $top$, $0$,
+    $readA$, $?$, $-$, // err
+    $readA$, $bot$, $-$, // err
+    $writeA$, $0$, $0$,
+    // $writeA$, $top$, $-$,
+    $writeA$, $?$, $0$,
+    $writeA$, $bot$, $0$,
+    $mbwriteA$, $0$, $0$,
+    // $mbwriteA$, $top$, $top$,
+    $mbwriteA$, $?$, $?$,
+    $mbwriteA$, $bot$, $?$,
+    // $spoilA$, $0$, $bot$,
+    // // $spoilA$, $top$, $bot$,
+    // $spoilA$, $?$, $bot$,
+    // $spoilA$, $bot$, $bot$,
+    // $nospoilA$, $0$, $top$,
+    // $nospoilA$, $top$, $top$,
+    // $nospoilA$, $?$, $-$, // ??
+    // $nospoilA$, $bot$, $-$,
+  ),
+
+  table(
+    columns: 3,
+    table.header(
+      [*a*], [*x*], $modR$
+    ),
+    $readA$, $1$, $1$,
+    $readA$, $0$, $1$,
+    $readA$, $top$, $top$,
+    $writeA$, $1$, $1$,
+    $writeA$, $0$, $top$,
+    $writeA$, $top$, $top$,
+    $mbwriteA$, $1$, $1$,
+    $mbwriteA$, $0$, $0$,
+    $mbwriteA$, $top$, $top$,
+
+    // $spoilA$, $1$, $1$,
+    // $spoilA$, $0$, $0$,
+    // $spoilA$, $top$, $top$,
+    // $nospoilA$, $1$, $1$,
+    // $nospoilA$, $0$, $0$,
+    // $nospoilA$, $top$, $top$,
+  ),
+
+  table(
+    columns: 3,
+    table.header(
+      [*a*], [*x*], $modW$
+    ),
+    $readA$, $1$, $1$,
+    $readA$, $?$, $?$,
+    $readA$, $0$, $0$,
+    $writeA$, $1$, $1$,
+    $writeA$, $?$, $1$,
+    $writeA$, $0$, $1$,
+    $mbwriteA$, $1$, $1$,
+    $mbwriteA$, $?$, $?$,
+    $mbwriteA$, $0$, $?$,
+
+    // $spoilA$, $1$, $1$,
+    // $spoilA$, $?$, $?$,
+    // $spoilA$, $0$, $0$,
+    // $nospoilA$, $1$, $1$,
+    // $nospoilA$, $?$, $?$,
+    // $nospoilA$, $0$, $0$,
+  )
+))
+
+Прочерк \"$-$\" означает, что данная операция не определена.
+
 === Value Update
 
-#let modify = `modify`
+==== Change
+
+Замена подзначения в значении по $revpath$, $b in value$.
+
+#let change = `change`
 
 // TODO: add type check ??
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ modify end value],
+    name: [ change final value],
 
-    // $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl \# . \, b cr)_modify cl b, mu cr$,
+    // $v in {0, ?, bot}$,
+    $cl v, mu cr xarrowSquiggly(cl \# . \, b cr)_change cl b, mu cr$,
   )
 ))
 
@@ -567,10 +727,54 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ new reference copy value],
+    name: [ change reference value],
 
-    $cl mu[l], mu cr xarrowSquiggly(cl pi \, b cr)_modify cl v', mu' cr$,
-    $cl rf l, mu cr xarrowSquiggly(cl rf pi \, b cr)_modify cl rf l, mu'[l <- v'] cr$,
+    $cl mu[l], mu cr xarrowSquiggly(cl pi \, b cr)_change cl v', mu' cr$,
+    $cl rf l, mu cr xarrowSquiggly(cl rf pi \, b cr)_change cl rf l, mu'[l <- v'] cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ change tuple value],
+
+    $cl v_i, mu cr xarrowSquiggly(cl p \, b cr)_change cl v'_i, mu', cr$,
+    $cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl i.pi \, b cr)_change cl [v_1, ... v'_i, ... v_n], mu' cr$,
+  )
+))
+
+#h(10pt)
+
+==== Modify
+
+Совершение операции над тривиальным подзначением в значении по $revpath$, $a in action$
+
+#let modify = `modify`
+
+// TODO: add type check ??
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ modify final value],
+
+    $cl cdl v_m, v_r, v_w cdr, mu cr
+     xarrowSquiggly(cl \# . \, a cr)_modify
+     cl cdl v_m modM a, v_r modR a, v_w modW a cdr, mu cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ modify reference value],
+
+    $cl mu[l], mu cr xarrowSquiggly(cl pi \, a cr)_modify cl v', mu' cr$,
+    $cl rf l, mu cr xarrowSquiggly(cl rf pi \, a cr)_modify cl rf l, mu'[l <- v'] cr$,
   )
 ))
 
@@ -581,8 +785,8 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ modify tuple value],
 
-    $cl v_i, mu cr xarrowSquiggly(cl p \, b cr)_modify cl v'_i, mu', cr$,
-    $cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl i.pi \, b cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$,
+    $cl v_i, mu cr xarrowSquiggly(cl p \, a cr)_modify cl v'_i, mu', cr$,
+    $cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl i.pi \, a cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$,
   )
 ))
 
@@ -590,29 +794,74 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 
 === Value Combination
 
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ combine same trivial values],
+#align(center, grid(
+  columns: 3,
+  gutter: 20%,
+  align: center,
+  table(
+    columns: 3,
+    table.header(
+      [*x*], [*y*], $plus.o_m$
+    ),
+    $0$, $0$, $0$,
+    // $0$, $top$, $0$,
+    $0$, $?$, $?$,
+    $0$, $bot$, $?$,
+    $?$, $0$, $?$,
+    $?$, $?$, $?$,
+    $?$, $bot$, $?$,
+    // $?$, $top$, $?$,
+    $bot$, $0$, $?$,
+    $bot$, $?$, $?$,
+    // $bot$, $top$, $?$,
+    // $top$, $0$, $?$,
+    // $top$, $?$, $?$,
+    // $top$, $bot$, $?$,
+    $bot$, $bot$, $bot$,
+    // $top$, $top$, $top$,
+  ),
 
-    $v_1 in {0, \#, bot}$,
-    $v_2 in {0, \#, bot}$,
-    $v_1 = v_2$,
-    $v_1 plus.o v_2 = v_1$
+  table(
+    columns: 3,
+    table.header(
+      [*x*], [*y*], $plus.o_r$
+    ),
+    $1$, $1$, $1$,
+    $1$, $0$, $1$,
+    $1$, $top$, $1$,
+    $0$, $1$, $1$,
+    $top$, $1$, $1$,
+    $0$, $0$, $0$,
+    $0$, $top$, $0$,
+    $top$, $0$, $0$,
+    $top$, $top$, $top$,
+  ),
+
+  table(
+    columns: 3,
+    table.header(
+      [*x*], [*y*], $plus.o_w$
+    ),
+    $1$, $1$, $1$,
+    $1$, $?$, $?$,
+    $1$, $0$, $?$,
+    $?$, $1$, $?$,
+    $?$, $?$, $?$,
+    $?$, $0$, $?$,
+    $0$, $1$, $?$,
+    $0$, $?$, $?$,
+    $0$, $0$, $0$,
   )
 ))
 
-#h(10pt)
-
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ combine different trivial values],
+    name: [ combine trivial values],
 
-    $v_1 in {0, \#, bot}$,
-    $v_2 in {0, \#, bot}$,
-    $v_1 != v_2$,
-    $v_1 plus.o v_2 = \#$
+    $v_1 = cdl v_1_m, v_1_r, v_1_w cdr$,
+    $v_2 = cdl v_2_m, v_2_r, v_2_w cdr$,
+    $v_1 plus.o v_2 = cdl v_1_m plus.o_m v_2_m, v_1_r plus.o_r v_2_r, v_1_w plus.o_w v_2_w cdr$
   )
 ))
 
@@ -691,7 +940,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ unit expr value],
 
-    $vals, mu texpre () eqmu 0$,
+    $vals, mu texpre () eqmu cdl 0_m, 0_r, 0_w cdr$,
   )
 ))
 
@@ -812,37 +1061,20 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 === Call Values Spoil
 
 #let spoil = `spoil`
+#let tryread = `try read`
+#let tryspoil = `try spoil`
 
-// TODO: FIXME: complete rule check
 #let tcorrectnew = $attach(tack.r.double, br: #[correct])$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ correctness],
 
-    $r = Read => v = 0$,
-    $r = Read => m = (In, \_)$, 
+    $m = (\_, Out) => c = Ref$, 
     $m = (\_, Out) => w = AlwaysWrite$,
-    $(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
+    $r = Read => m = (In, \_)$, 
 
-    $v in {0, \#, bot}$,
-
-    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
-  )
-))
-
-// TODO: extract correctness
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ spoil step],
-
-    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
-
-    $w = AlwaysWrite or w = MaybeWrite$,
-    $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, not Out) \, not Copy)_spoil cl bot, mu cr$,
+    $ tcorrectnew cl r, w, m, c cr $,
   )
 ))
 
@@ -851,13 +1083,103 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ fix step],
+    name: [ argument read],
 
-    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
+    $cl v_m, v_r, v_w cr,
+     xarrowSquiggly(Read)_tryread
+     cl v_m modW readA, v_r modR readA, v_w modW readA cr$,
+  )
+))
 
-    $w = AlwaysWrite$,
-    $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \,  (\_, Out) \, c)_spoil cl 0, mu cr$,
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ argument not read],
+
+    $cl v_m, v_r, v_w cr,
+     xarrowSquiggly(not Read)_tryread
+     cl v_m, v_r, v_w cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ value maybe spoiled],
+
+    $v_m,
+     xarrowSquiggly(not Out \, MaybeWrite)_tryspoil
+     ?$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ value always spoiled],
+
+    $v_m,
+     xarrowSquiggly(not Out \, AlwaysWrite)_tryspoil
+     bot$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ value not spoiled],
+
+    $v_m,
+     xarrowSquiggly(Out \, w)_tryspoil
+     v_m$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ write spoil step],
+
+    $ tcorrectnew cl r, w, m, c cr $,
+    $cl v_m, v_r, v_w cr,
+     xarrowSquiggly(r)_tryread
+     cl v_m', v_r', v_w' cr$,
+
+    $v_m' modW writeA xarrowSquiggly(o \, AlwaysWrite)_tryspoil v_m''$,
+
+    $cl cdl v_m, v_r, v_w cdr, mu cr
+     xarrowSquiggly(cl r \, AlwaysWrite cr \, (\_, o) \, Ref)_spoil
+     cl cdl v_m'', v_r' modR writeA, v_w' modW writeA cdr, cdr, mu cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ maybe write step],
+
+    $ tcorrectnew cl r, w, m, c cr $,
+    $cl v_m, v_r, v_w cr,
+     xarrowSquiggly(r)_tryread
+     cl v_m', v_r', v_w' cr$,
+
+    $v_m' modW mbwriteA xarrowSquiggly(o \, MaybeWrite)_tryspoil v_m''$,
+
+    $cl cdl v_m, v_r, v_w cdr, mu cr
+     xarrowSquiggly(cl r \, MaybeWrite cr \, (\_, o) \, Ref)_spoil
+     cl cdl v_m'', v_r' modR mbwriteA, v_w' modW mbwriteA cdr, mu cr$,
   )
 ))
 
@@ -868,12 +1190,16 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ skip step],
 
-    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
+    $ tcorrectnew cl r, w, m, c cr $,
+    $cl v_m, v_r, v_w cr,
+     xarrowSquiggly(r)_tryread
+     cl v_m', v_r', v_w' cr$,
 
-    $not "spoil step"$,
-    $not "fix step"$,
-    $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, not Out) \, c)_spoil cl v, mu cr$,
+    $c = Copy or w = NotWrite$,
+
+    $cl cdl v_m, v_r, v_w cdr, mu cr
+     xarrowSquiggly(cl r \, w cr cr \, (\_, \_) \, c)_spoil
+     cl cdl v_m', v_r', v_w' cdr mu cr$,
   )
 ))
 
@@ -945,7 +1271,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
     // FIXME depends on parent ??
     $cl b, mu cr xarrowSquiggly(t \, t' \, m \, Copy)_spoil cl b', mu' cr$,
     $p arrrevpath^(\#.) pi$,
-    $cl mu'[l], mu' cr xarrowSquiggly(cl pi \, b' cr)_modify cl v'', mu'' cr$,
+    $cl mu'[l], mu' cr xarrowSquiggly(cl pi \, b' cr)_change cl v'', mu'' cr$,
 
     $mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu''[l <- v'']$,
   )
@@ -1009,6 +1335,80 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 
 === Function Evaluation
 
+#align(center, grid(
+  columns: 2,
+  gutter: 20%,
+  align: center,
+
+  [
+    $ x ~_r t$
+
+    #table(
+      columns: 2,
+      table.header(
+        [*x*], [*t*]
+      ),
+      $1$, $Read$,
+      $0$, $not Read$,
+      $top$, $not Read$,
+    )
+  ],
+
+  [
+    $x ~_w t$
+    #table(
+      columns: 2,
+      table.header(
+        [*x*], [*t*]
+      ),
+      $0$, $NotWrite$,
+      $?$, $MaybeWrite$,
+      $1$, $AlwaysWrite$,
+    )
+  ]
+))
+
+#let ttags = $attach(tack.r, br: #[`tags`])$
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ trivial type check],
+
+    $v_r ~_r r$,
+    $v_w ~_w w$,
+    $mu ttags cdl v_m, v_r, v_w cdr : cl r, w cr$,
+  )
+))
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ lambda check],
+
+    $mu ttags lambda space overline(s) :$,
+  )
+))
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ reference check],
+
+    $mu ttags mu[l] : t$,
+    $mu ttags rf l : rf t$,
+  )
+))
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ tuple check],
+
+    $mu ttags v_1 : t_1$,
+    $...$,
+    $mu ttags v_n : t_n$,
+    $mu ttags [v_1, ... v_n] : [t_1, ... t_n]$,
+  )
+))
+
 #let tfunceval = $attach(tack.r.double, br: #[func eval])$
 #align(center, prooftree(
   vertical-spacing: 4pt,
@@ -1028,10 +1428,16 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
      xarrowDashed(x_n space t_n space e_n)_vals
      cl types_n, vals_n, mu_n cr$,
 
+    // NOTE: eval function body
     $cl types_n, vals_n,  mu_n cr
      xarrow(s)
      cl types', vals', mu' cr$,
 
+    // NOTE: check that read and write tags are used properly
+    $mu' ttags mu'[vals'[x_1]] : t_1$,
+    $...$,
+    $mu' ttags mu'[vals'[x_n]] : t_n$,
+
     $vals, mu_0 tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$,
   )
 ))
@@ -1066,7 +1472,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
     $...$,
     $vals, mu_0 tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] cr$,
 
-    // NOTE: thick arrow to "spoil" context
+    // NOTE: "spoil" context for each argument usage
     $mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$,
     $...$,
     $mu_(n - 1) stretch(=>)^(m_n space t_n space e_n)_(cl vals, types cr) mu_n$,
@@ -1089,7 +1495,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
     $p arrpath x$,
     $l = vals[x]$,
     $p arrrevpath^(\#.) pi$,
-    $mu[l] xarrowSquiggly(cl pi \, 0 cr)_modify v'$,
+    $mu[l] xarrowSquiggly(cl pi \, writeA cr)_modify v'$,
 
     $cl types, vals, mu cr
      xarrow("WRITE" p)
@@ -1102,18 +1508,25 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ READ $p$],
 
-    $vals, mu tval p eqmu 0$,
+    // TODO: already handled in modify ?
+    // $vals, mu tval p eqmu cdr v_m, \_, \_ cdl$,
+    // $v_m in { 0, top }$,
+
+    $types ttype p : cl r, w cr$,
+    $r = Read$,
+    $p arrpath x$,
+    $l = vals[x]$,
+    $p arrrevpath^(\#.) pi$,
+    $mu[l] xarrowSquiggly(cl pi \, readA cr)_modify v'$,
 
     $cl types, vals, mu cr
      xarrow("READ" p)
-     cl types, vals, mu cr$,
+     cl types, vals, mu[l <- v'] cr$,
   )
 ))
 
 #h(10pt)
 
-#h(10pt)
-
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(

model_with_structures/synthesizer.ml

@@ -164,12 +164,44 @@ struct
 
   (* NOTE: deepvalue - not used (?) *)
 
+  module MemVal = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec t = ZeroMV | SmthMV | BotMV
+      [@@deriving gt ~options:{ show; gmap }]
+      type ground = t
+    ]
+  end
+
+  module ReadVal = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec t = ZeroRV | OneRV | TopRV
+      [@@deriving gt ~options:{ show; gmap }]
+      type ground = t
+    ]
+  end
+
+  module WriteVal = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec t = ZeroWV | SmthWV | OneWV
+      [@@deriving gt ~options:{ show; gmap }]
+      type ground = t
+    ]
+  end
+
   module Value = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ('sl, 'd, 'vl) t = ZeroV | SmthV | BotV | FunV of 'sl | RefV of 'd | TupleV of 'vl
+      type nonrec ('vm, 'vr, 'vw, 'sl, 'd, 'vl) t = UnitV of 'vm * 'vr * 'vw
+                                                  | FunV of 'sl
+                                                  | RefV of 'd
+                                                  | TupleV of 'vl
       [@@deriving gt ~options:{ show; gmap }]
-      type ground = (((* Nat.ground List.ground * *) Stmt.ground) List.ground, Nat.ground, ground List.ground) t
+      type ground = (MemVal.ground, ReadVal.ground, WriteVal.ground,
+                     ((* Nat.ground List.ground * *) Stmt.ground) List.ground,
+                     Nat.ground, ground List.ground) t
     ]
   end
 
@@ -182,6 +214,15 @@ struct
     ]
   end
 
+  module Action = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec t = ReadA | AlwaysWriteA | MayWriteA
+      [@@deriving gt ~options:{ show; gmap }]
+      type ground = t
+    ]
+  end
+
   (* --- *)
 
   module MemEnv = struct
@@ -340,6 +381,17 @@ struct
     { xs == [] & ys == [] & zs == [] }
   }
 
+  (* NOTE: unrequired ? *)
+  (* let list_map2o f xs ys zs = ocanren { *)
+    (* { xs == [] & ys == [] } | *)
+    (* { fresh x', xs', y', ys', z', zs' in *)
+      (* xs == x' :: xs' & *)
+      (* ys == y' :: ys' & *)
+      (* f x' y' z' *)
+      (* mapo f xs' ys' zs' & *)
+      (* zs == z' :: zs' } *)
+  (* } *)
+
   (* - state utils *)
 
   let types_assoco id types tp =
@@ -459,7 +511,8 @@ struct
   let is_trivial_vo v =
     let open Value in
     ocanren {
-    v == ZeroV | v == SmthV | v == BotV
+    fresh v_m, v_r, v_w in
+    v == UnitV (v_m, v_r, v_w)
   }
 
   let rec pathvaro p x =
@@ -516,11 +569,11 @@ struct
         pathvalo mem vals p' v' &
         v' == RefV id &
         mem_geto mem id v } |
-      { fresh p', id, v', vs in
-        p == AccessP (p', id) &
+      { fresh p', id', v', vs in
+        p == AccessP (p', id') &
         pathvalo mem vals p' v' &
         v' == TupleV vs &
-        list_ntho vs id v }
+        list_ntho vs id' v }
   }
 
   (* --- eval rules --- *)
@@ -539,13 +592,20 @@ struct
     let open Type in
     let open Value in
     let open ReadCap in
-    let open CopyCap in
+    (* let open CopyCap in *)
+    let open MemVal in
+    let open ReadVal in
+    let open WriteVal in
     ocanren {
       { fresh r, w in
         is_trivial_vo v &
         tp == UnitT (r, w) &
-        { { r == Rd & mem_with_id' == Std.pair mem v } |
-          { r == NRd & mem_with_id' == Std.pair mem BotV } } } |
+        { { fresh v_m, _v_r, _v_w in
+            r == Rd &
+            v == UnitV (v_m, _v_r, _v_w) &
+            mem_with_id' == Std.pair mem (UnitV (v_m, ZeroRV, ZeroWV)) } |
+          { r == NRd &
+            mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } |
       { fresh stmts, ts in
         v == FunV stmts &
         tp == FunT ts &
@@ -553,13 +613,13 @@ struct
       { fresh c, tp', id in
         v == RefV id &
         tp == RefT (c, tp') &
-        { { c == Rf & mem_with_id' == Std.pair mem v } |
-          { fresh v', mem_cp, v_cp, mem_add, id_add in
-            c == Cp &
-            mem_geto mem id v' &
-            valcopyo mem v' tp' (Std.pair mem_cp v_cp) &
-            mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
-            mem_with_id' == (mem_add, RefV id_add) } } } |
+        (* { c == Rf & mem_with_id' == Std.pair mem v } | *)
+        { fresh v', mem_cp, v_cp, mem_add, id_add in
+          (* c == Cp & *)
+          mem_geto mem id v' &
+          valcopyo mem v' tp' (Std.pair mem_cp v_cp) &
+          mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
+          mem_with_id' == (mem_add, RefV id_add) } } |
       { fresh vs, tps, mem', vs' in
         v == TupleV vs &
         tp == TupleT tps &
@@ -567,10 +627,43 @@ struct
         mem_with_id' == Std.pair mem' (TupleV vs') }
   }
 
+  (* - action rules *)
+
+  let memvmodo a v_m v_m' =
+    let open MemVal in
+    let open Action in
+    ocanren {
+      { a == ReadA & v_m == ZeroMV & v_m' == ZeroMV } |
+      { a == AlwaysWriteA & v_m' == ZeroMV } |
+      { a == MayWriteA & v_m == ZeroMV & v_m' == ZeroMV } |
+      { a == MayWriteA & v_m =/= ZeroMV & v_m' == SmthMV }
+  }
+
+  let readvmodo a v_r v_r' =
+    let open ReadVal in
+    let open Action in
+    ocanren {
+      { v_r == TopRV & v_r' == TopRV } |
+      { v_r == OneRV & v_r' == OneRV } |
+      { a == ReadA & v_r == ZeroRV & v_r' == OneRV } |
+      { a == AlwaysWriteA & v_r == ZeroRV & v_r' == TopRV } |
+      { a == MayWriteA & v_r == ZeroRV & v_r' == ZeroRV }
+  }
+
+  let writevmodo a v_w v_w' =
+    let open WriteVal in
+    let open Action in
+    ocanren {
+      { a == ReadA & v_w' == v_w } |
+      { a == AlwaysWriteA & v_w' == OneWV } |
+      { a == MayWriteA & v_w == OneWV & v_w' == OneWV } |
+      { a == MayWriteA & v_w =/= OneWV & v_w' == v_w }
+  }
+
   (* - value update *)
 
   (* NOTE: reversed path used *)
-  let rec valupdo mem v rp b mem_with_v' =
+  let rec valchangeo mem v rp b mem_with_v' =
     let open RevPath in
     let open Value in
     ocanren {
@@ -580,7 +673,7 @@ struct
         rp == DerefRP rp' &
         v == RefV id &
         mem_geto mem id v' &
-        valupdo mem v' rp' b mem_with_v_upd &
+        valchangeo mem v' rp' b mem_with_v_upd &
         Std.pair mem_upd v_upd == mem_with_v_upd &
         mem_seto mem_upd id v_upd mem_st &
         mem_with_v' == Std.pair mem_st (RefV id) } |
@@ -588,7 +681,40 @@ struct
         rp == AccessRP (rp', id) &
         v == TupleV vs' &
         list_ntho vs' id v' &
-        valupdo mem v' rp' b mem_with_v_upd &
+        valchangeo mem v' rp' b mem_with_v_upd &
+        Std.pair mem_upd v_upd == mem_with_v_upd &
+        list_replaceo vs' id v_upd vs_upd &
+        mem_with_v' == Std.pair mem_upd (TupleV vs_upd) }
+  }
+
+  (* NOTE: reversed path used *)
+  let rec valupdo mem v rp a mem_with_v' =
+    let open RevPath in
+    let open Value in
+    ocanren {
+      { fresh v_m, v_r, v_w,
+              v_m', v_r', v_w',
+              v' in
+        rp == VarRP &
+        v == UnitV (v_m, v_r, v_w) &
+        memvmodo a v_m v_m' &
+        readvmodo a v_r v_r' &
+        writevmodo a v_w v_w' &
+        v' == UnitV (v_m', v_r', v_w') &
+        mem_with_v' == Std.pair mem v' } |
+      { fresh rp', id, v', mem_upd, v_upd, mem_with_v_upd, mem_st in
+        rp == DerefRP rp' &
+        v == RefV id &
+        mem_geto mem id v' &
+        valupdo mem v' rp' a mem_with_v_upd &
+        Std.pair mem_upd v_upd == mem_with_v_upd &
+        mem_seto mem_upd id v_upd mem_st &
+        mem_with_v' == Std.pair mem_st (RefV id) } |
+      { fresh rp', id, vs', v', mem_upd, v_upd, mem_with_v_upd, vs_upd in
+        rp == AccessRP (rp', id) &
+        v == TupleV vs' &
+        list_ntho vs' id v' &
+        valupdo mem v' rp' a mem_with_v_upd &
         Std.pair mem_upd v_upd == mem_with_v_upd &
         list_replaceo vs' id v_upd vs_upd &
         mem_with_v' == Std.pair mem_upd (TupleV vs_upd) }
@@ -596,13 +722,50 @@ struct
 
   (* - value combination *)
 
+  let memvalcombo u v u' =
+    let open MemVal in
+    ocanren {
+      { u == ZeroMV & v == ZeroMV & u' == ZeroMV } |
+      { u == BotMV & v == BotMV & u' == BotMV } |
+      { { u =/= ZeroMV | { u == ZeroMV & v =/= ZeroMV } } &
+        { u =/= BotMV | { u == BotMV & v =/= BotMV } } & 
+        u' == SmthMV }
+  }
+
+  let readvalcombo u v u' =
+    let open ReadVal in
+    ocanren {
+      { u == TopRV & v == TopRV & u' == TopRV } |
+      { u == ZeroRV & v == ZeroRV & u' == ZeroRV } |
+      { u == TopRV & v == ZeroRV & u' == ZeroRV } |
+      { u == ZeroRV & v == TopRV & u' == ZeroRV } |
+      { u =/= TopRV & v =/= TopRV &
+        u =/= ZeroRV & v =/= ZeroRV & 
+        u' == OneRV }
+  }
+
+  let writevalcombo u v u' =
+    let open WriteVal in
+    ocanren {
+      { u == OneWV & v == OneWV & u' == OneWV } |
+      { u == ZeroWV & v == ZeroWV & u' == ZeroWV } |
+      { { u =/= ZeroWV | { u == ZeroWV & v =/= ZeroWV } } &
+        { u =/= OneWV | { u == OneWV & v =/= OneWV } } & 
+        u' == SmthWV }
+  }
+
   let rec valcombo u v u' =
     let open Value in
     ocanren {
-    { is_trivial_vo u &
-      is_trivial_vo v &
-      (* TODO: do not use disequality constraint ? *)
-      { { u == v & u' == u } | { u =/= v & u' == BotV } } } |
+    { fresh u_m, u_r, u_w,
+            v_m, v_r, v_w,
+            u_m', u_r', u_w' in
+      u == UnitV (u_m, u_r, u_w) &
+      v == UnitV (v_m, v_r, v_w) &
+      memvalcombo u_m v_m u_m' &
+      readvalcombo u_r v_r u_r' &
+      writevalcombo u_w v_w u_w' &
+      u' == UnitV (u_m', u_r', u_w') } |
     { fresh ustmts, vstmts, ustmts' in
       u == FunV ustmts &
       v == FunV vstmts &
@@ -612,7 +775,8 @@ struct
     { fresh a, b in
       u == RefV a &
       v == RefV b &
-      a == b } |
+      a == b &
+      u' == RefV a } |
     { fresh us, vs, us' in
       u == TupleV us &
       v == TupleV vs &
@@ -642,8 +806,11 @@ struct
   exprvalo mem vals e v' = 
     let open Expr in
     let open Value in
+    let open MemVal in
+    let open ReadVal in
+    let open WriteVal in
     ocanren {
-      { e == UnitE & v' == ZeroV } |
+      { e == UnitE & v' == UnitV (ZeroMV, ZeroRV, ZeroWV) } |
       { fresh p in
         e == PathE p &
         pathvalo mem vals p v' } |
@@ -698,7 +865,6 @@ struct
                 types', vals' in
           d == VarD (tp, e) &
           exprvalo mem vals e v &
-          (* v == TupleV [ZeroV; ZeroV] & (* FIXME TMP *) *)
           valcopyo mem v tp (Pair.pair mem_cp v_cp) &
           (* mem_cp == mem & v_cp == v & *)
           mem_addo mem_cp v_cp (Pair.pair mem_add id_add) &
@@ -760,76 +926,100 @@ struct
   (* - call values spoil *)
 
   (* TODO: check that negation is interpreted correctly *)
-  let is_correct_tagso v r w _r' w' m c =
-    let open Value in
+  let is_correct_tagso r w m c =
     let open ReadCap in
     let open WriteCap in
     let open Mode in
     let open CopyCap in
     ocanren {
-      { r == NRd | r == Rd & v == ZeroV } &
       { r == NRd | r == Rd & is_ino m } &
-      { is_not_outo m | is_outo m & w == AlwaysWr } &
-      { w == NeverWr |
-        w =/= NeverWr & w' =/= AlwaysWr & is_not_outo m & c == Cp |
-        w =/= NeverWr & w' == AlwaysWr } &
-      is_trivial_vo v
+      { is_not_outo m | is_outo m & w == AlwaysWr & c == Rf }
   }
 
-  let rec valspoil_foldero m c mem_with_vs tp u v mem_with_vs' = ocanren {
-    fresh mem, vs, mem', v' in
-    Std.pair mem vs == mem_with_vs &
-    valspoilo mem v tp u m c (Std.pair mem' v') &
-    mem_with_vs' == Std.pair mem' (v' :: vs)
-  }
-  and valspoilo mem v tp u m c mem_with_v' =
-    let open Type in
+  let tryreado r v_m v_r v_w v' =
+    let open Action in
     let open Value in
+    let open ReadCap in
+    ocanren {
+      { fresh v_m', v_r', v_w' in
+        r == Rd &
+        memvmodo ReadA v_m v_m' &
+        readvmodo ReadA v_r v_r' &
+        writevmodo ReadA v_w v_w' &
+        v' == UnitV (v_m', v_r', v_w') } |
+      { r == NRd &
+        v' == UnitV (v_m, v_r, v_w)}
+  }
+
+  let tryspoilo m w v_m v_m' =
     let open Mode in
     let open WriteCap in
-    let open CopyCap in
+    let open MemVal in
     ocanren {
-      { fresh r, w, r', w' in
+      { is_outo m & { w == AlwaysWr | w == MayWr } & v_m' == v_m } |
+      { is_not_outo m & w == AlwaysWr & v_m' == BotMV } |
+      { is_not_outo m & w == MayWr & v_m' == SmthMV }
+  }
+
+  let rec valspoil_foldero m c mem_with_vs tp v mem_with_vs' = ocanren {
+    fresh mem, vs, mem', v' in
+    Std.pair mem vs == mem_with_vs &
+    valspoilo mem v tp m c (Std.pair mem' v') &
+    mem_with_vs' == Std.pair mem' (v' :: vs)
+  }
+  and valspoilo mem v tp m c mem_with_v' =
+    let open Type in
+    let open Value in
+    let open WriteCap in
+    let open CopyCap in
+    let open Action in
+    ocanren {
+      { fresh r, w,
+              v_m, v_r, v_w,
+              v', v'' in
         tp == UnitT (r, w) &
-        u == UnitT (r', w') &
-        is_trivial_vo v &
-        is_correct_tagso v r w r' w' m c &
+        v == UnitV (v_m, v_r, v_w) &
+        is_correct_tagso r w m c &
+        tryreado r v_m v_r v_w v' &
         {
-          { is_not_outo m &
+          { { c == Cp | { c == Rf & w == NeverWr } } &
+            mem_with_v' == Std.pair mem v' } |
+          { fresh v_m', v_r', v_w',
+                  v_m'', v_r'', v_w'',
+                  v_m''' in
             c == Rf &
             { w == AlwaysWr | w == MayWr } &
-            mem_with_v' == Std.pair mem BotV } |
-          { is_outo m &
-            w == AlwaysWr &
-            mem_with_v' == Std.pair mem ZeroV } |
-          { { is_outo m |
-              is_not_outo m & c == Cp |
-              is_not_outo m & c == Rf & w == NeverWr } &
-            { is_not_outo m |
-              is_outo m & w == MayWr |
-              is_outo m & w == NeverWr } &
-            mem_with_v' == Std.pair mem v }
+            v' == UnitV (v_m', v_r', v_w') &
+            {
+              { w == AlwaysWr &
+                memvmodo AlwaysWriteA v_m' v_m'' &
+                readvmodo AlwaysWriteA v_r' v_r'' &
+                writevmodo AlwaysWriteA v_w' v_w'' } |
+              { w == MayWr &
+                memvmodo MayWriteA v_m' v_m'' &
+                readvmodo MayWriteA v_r' v_r'' &
+                writevmodo MayWriteA v_w' v_w'' }
+            } &
+            tryspoilo m w v_m'' v_m''' &
+            v'' == UnitV (v_m''', v_r'', v_w'') &
+            mem_with_v' == Std.pair mem v'' }
         } } |
-      { fresh ts, us, _stmts in
+      { fresh ts, _stmts in
         tp == FunT ts &
-        u == FunT us &
         v == FunV _stmts &
-        ts == us &
         mem_with_v' == Std.pair mem v } |
-      { fresh ctp', tp', cu', u', id', v', mem_sp, v_sp, mem_set in
+      { fresh ctp', tp', id', v', mem_sp, v_sp, mem_set in
         tp == RefT (ctp', tp') &
-        u == RefT (cu', u') &
         v == RefV id' &
         mem_geto mem id' v' &
-        valspoilo mem v' tp' u' m ctp' (Std.pair mem_sp v_sp) &
+        valspoilo mem v' tp' m ctp' (Std.pair mem_sp v_sp) &
         mem_seto mem_sp id' v_sp mem_set &
         mem_with_v' == Std.pair mem_set (RefV id') } |
-      { fresh tps, us, vs, mem_sp, vs_sp in
+      { fresh tps, vs, mem_sp, vs_sp in
         tp == TupleT tps &
-        u == TupleT us &
         v == TupleV vs &
-        list_foldr3o (valspoil_foldero m c)
-                     (Std.pair mem []) tps us vs
+        list_foldr2o (valspoil_foldero m c)
+                     (Std.pair mem []) tps vs
                      (Std.pair mem_sp vs_sp) &
         mem_with_v' == Std.pair mem_sp (TupleV vs_sp)
       }
@@ -837,34 +1027,34 @@ struct
 
   (* full spoil *)
 
-  let argspoilpo st m tp p mem' =
+  let argsspoilpo st m tp p mem' =
     let open StEnv in
     let open CopyCap in
     let open RevPath in
     ocanren {
       fresh mem, types, vals, visited,
-            x, id, b, tp', rp,
+            x, id, b(* , tp' *), rp,
             mem_sp, b_sp, v_sp, mem_upd, v_upd in
       st == StEnv (mem, types, vals, visited) &
       pathvaro p x &
       vals_assoco x vals id &
       pathvalo mem vals p b &
-      pathtypeo types p tp' &
-      valspoilo mem b tp tp' m Cp (Std.pair mem_sp b_sp) &
-      mem_geto mem_sp id v_sp &
+      (* pathtypeo types p tp' & *)
+      valspoilo mem b tp m Cp (Std.pair mem_sp b_sp) &
       pathrevo p VarRP rp &
-      valupdo mem_sp v_sp rp b_sp (Std.pair mem_upd v_upd) &
+      mem_geto mem_sp id v_sp &
+      valchangeo mem_sp v_sp rp b_sp (Std.pair mem_upd v_upd) &
       mem_seto mem_upd id v_upd mem'
   }
 
-  let rec argspoile_foldero types vals visited m mem tp e mem' =
+  let rec argsspoile_foldero types vals visited m mem tp e mem' =
     let open StEnv in
     ocanren {
       fresh st in
       st == StEnv (mem, types, vals, visited) &
-      argspoileo st m tp e mem'
+      argsspoileo st m tp e mem'
   }
-  and argspoileo st m tp e mem' =
+  and argsspoileo st m tp e mem' =
     let open StEnv in
     let open Expr in
     let open Type in
@@ -878,14 +1068,14 @@ struct
           mem' == mem } |
         { fresh p in
           e == PathE p &
-          argspoilpo st m tp p mem' } |
+          argsspoilpo st m tp p mem' } |
         { fresh x in
           e == RefE x &
-          argspoilpo st m tp (VarP x) mem' } |
+          argsspoilpo st m tp (VarP x) mem' } |
         { fresh es, tps in
           e == TupleE es &
           tp == TupleT tps &
-          list_foldl2o (argspoile_foldero types vals visited m) mem tps es mem'}
+          list_foldl2o (argsspoile_foldero types vals visited m) mem tps es mem'}
       }
   }
 
@@ -910,8 +1100,47 @@ struct
   (* - function evaluation *)
   (* NOTE: not needed due to performed optimization in stmt_eval ? *)
 
+  let writeval_to_capo v_w w' =
+    let open WriteVal in
+    let open WriteCap in
+    ocanren {
+      { v_w == ZeroWV & w' == NeverWr } |
+      { v_w == SmthWV & w' == MayWr } |
+      { v_w == OneWV & w' == AlwaysWr }
+  }
+
+  let rec tags_checko mem v tp =
+    let open ReadVal in
+    let open ReadCap in
+    let open Type in
+    let open Value in
+    ocanren {
+      { fresh v_m, v_r, v_w,
+              r, w in
+        v == UnitV (v_m, v_r, v_w) &
+        tp == UnitT (r, w) &
+        {
+          { r == Rd & v_r == OneRV } |
+          { r == NRd & v_r == ZeroRV } |
+          { r == NRd & v_r == TopRV }
+        } &
+        writeval_to_capo v_w w
+         } |
+      { fresh _stmts, _ts in
+        v == FunV _stmts &
+        tp == FunT _ts } |
+      { fresh id, _c, tp', v' in
+        v == RefV id &
+        tp == RefT (_c, tp') &
+        mem_geto mem id v' &
+        tags_checko mem v' tp' } |
+      { fresh vs, tps in
+        v == TupleV vs &
+        tp == TupleT tps &
+        List.mapo (tags_checko mem) vs tps }
+  }
+
   (* - statement evaluation *)
-  (* TODO *)
 
   let rec stmt_addarg_foldero vals st_with_id mtp e st_with_id' = ocanren {
     fresh st, x, m, tp, st' in
@@ -920,16 +1149,28 @@ struct
     addargo st vals x tp e st' &
     st_with_id' == Std.pair st' (Nat.s x)
   }
-  and stmt_eval_func_foldero mem types vals visited stmt visited' =
+  and f_tags_check_foldero mem vals x mtp x' = ocanren {
+    fresh m, tp, id', v' in
+    mtp == Std.pair m tp &
+    vals_assoco x vals id' &
+    mem_geto mem id' v' &
+    tags_checko mem v' tp &
+    x' == Nat.s x
+  }
+  and stmt_eval_func_foldero mem types vals tps visited stmt visited' =
     let open StEnv in
     ocanren {
       { fresh visited_add, st,
-              st', mem', types', vals' in
+              st', mem', types', vals',
+              _x', visited'' in
         not_visited_checko visited stmt &
         visited_addo visited stmt visited_add &
         st == StEnv (mem, types, vals, visited_add) &
         stmt_evalo st stmt st' &
-        st' == StEnv (mem', types', vals', visited') } |
+        st' == StEnv (mem', types', vals', visited'') &
+        list_foldlo (f_tags_check_foldero mem' vals') 0 tps _x' &
+        visited' == visited''
+         } |
       { visited_checko visited stmt &
         visited == visited' }
   }
@@ -939,7 +1180,7 @@ struct
       fresh m, tp, st in
       Std.pair m tp == mtp &
       st == StEnv (mem, types, vals, visited) &
-      argspoileo st m tp e mem'
+      argsspoileo st m tp e mem'
   }
   and stmt_evalo st s st' =
     let open StEnv in
@@ -950,6 +1191,7 @@ struct
     let open TypesEnv in
     let open ValsEnv in
     let open RevPath in
+    let open Action in
     ocanren {
       fresh mem, types, vals, visited in
       st == StEnv (mem, types, vals, visited) &
@@ -979,7 +1221,7 @@ struct
                        (Std.pair st_call 0) tps es
                        (Std.pair state_with_args _arg_id) &
           state_with_args == StEnv (mem_swa, types_swa, vals_swa, visited_swa) &
-          list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa) visited_swa fstmts visited' &
+          list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa tps) visited_swa fstmts visited' &
           (* TODO: FIXME check left or right order *)
           list_foldl2o (stmt_eval_spoil_foldero types vals (* NOTE: not important*) visited')
                        mem tps es mem_spoiled &
@@ -995,13 +1237,25 @@ struct
           vals_assoco x vals id &
           mem_geto mem id v &
           pathrevo p VarRP rp &
-          valupdo mem v rp ZeroV (Std.pair mem_upd v_upd) &
+          valupdo mem v rp AlwaysWriteA (Std.pair mem_upd v_upd) &
           mem_seto mem_upd id v_upd mem_set &
           st' == StEnv (mem_set, types, vals, visited) } |
-        { fresh p in
+        { fresh p, tp, _r, _w, x, id, v, rp,
+                mem_upd, v_upd, mem_set in
           s == ReadS p &
-          pathvalo mem vals p ZeroV &
-          st == st' } |
+          pathtypeo types p tp &
+          tp == UnitT (_r, _w) &
+          pathvaro p x &
+          vals_assoco x vals id &
+          mem_geto mem id v &
+          pathrevo p VarRP rp &
+          valupdo mem v rp ReadA (Std.pair mem_upd v_upd) &
+          mem_seto mem_upd id v_upd mem_set &
+          st' == StEnv (mem_set, types, vals, visited) } |
+        (* { fresh p in *)
+          (* s == ReadS p & *)
+          (* pathvalo mem vals p ZeroV & *)
+          (* st == st' } | *)
         { fresh sl, sr, stl in
           s == SeqS (sl, sr) &
           stmt_evalo st sl stl &

model_with_structures/tests_f.ml

@@ -16,6 +16,7 @@ open WriteCap
 open InCap
 open OutCap
 open Mode
+open StEnv
 
 @type answer =
   StEnv.ground GT.list with show
@@ -26,19 +27,31 @@ open Mode
 
 (* - shortcuts *)
 
-(* TODO *)
-
 (* NOTE: redo with fold ?? *)
-let rec seqo stmts stmt' = ocanren {
-    { stmts == [] & stmt' == SkipS } |
-    { fresh s in
-      stmts == [s] &
-      stmt' == s } |
-    { fresh s, s', ss, stmt_rest' in
-      stmts == s :: s' :: ss &
-      seqo (s' :: ss) stmt_rest' &
-      stmt' == SeqS(s, stmt_rest')
-    }
+let seq_foldero stmt_acc stmt stmt_acc' = ocanren {
+    stmt_acc' == SeqS(stmt, stmt_acc)
+  }
+let seqo stmts stmt' = ocanren {
+    list_foldro seq_foldero SkipS stmts stmt'
+  }
+(* ocanren { *)
+    (* { stmts == [] & stmt' == SkipS } | *)
+    (* { fresh s in *)
+      (* stmts == [s] & *)
+      (* stmt' == s } | *)
+    (* { fresh s, s', ss, stmt_rest' in *)
+      (* stmts == s :: s' :: ss & *)
+      (* seqo (s' :: ss) stmt_rest' & *)
+      (* stmt' == SeqS(s, stmt_rest') *)
+    (* } *)
+  (* } *)
+
+let deref_accesso id v p' = ocanren {
+    p' == DerefP (AccessP (VarP v, id))
+  }
+
+let access_deref_accesso id_ext id_int v p' = ocanren {
+    p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext)
   }
 
   (* - basic var tests *)
@@ -120,6 +133,18 @@ let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q
 
   (* - basic call tests *)
 
+(* NOTE: should add ? *)
+(* let prog_eval_t_simple_call_noarg _ = show(answer) (Stream.take (run q *)
+  (* (fun q -> ocanren { *)
+              (* fresh prog, xg, fg, xd, fd in *)
+              (* globals_min_ido xg & *)
+              (* fg == Nat.s xg & *)
+              (* xd == VarD (UnitT (Rd, NeverWr), UnitE) & *)
+              (* fd == FunD ([], SkipS) & *)
+              (* prog == Prg ([xd; fd], CallS (VarP fg, [])) & *)
+              (* prog_evalo prog q }) *)
+  (* (fun q -> q#reify (StEnv.prj_exn)))) *)
+
 let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q
   (fun q -> ocanren {
               fresh prog, xg, fg, xd, fd in
@@ -137,9 +162,9 @@ let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, MayWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE xg) &
-              fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))],
+              xd == VarD (UnitT (Rd, NeverWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (Rd, NeverWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
                           ReadS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
               prog_evalo prog q })
@@ -151,9 +176,9 @@ let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, MayWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE xg) &
-              fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))],
+              xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
               prog_evalo prog q })
@@ -194,9 +219,9 @@ let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
-              fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
+              xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
               prog_evalo prog q })
@@ -223,9 +248,9 @@ let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
-              fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
+              xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
+              fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
                                          SeqS (WriteS (DerefP (VarP yg)),
@@ -242,9 +267,9 @@ let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q
               f2g == Nat.s fg &
               xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
               yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
-              fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
+              fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
-              f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))],
+              f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
                            SeqS (CallS (VarP fg, [PathE (VarP 0)]),
                                  WriteS (DerefP (VarP 0)))) &
               prog == Prg ([xd; yd; fd; f2d], SeqS (CallS (VarP f2g, [PathE (VarP yg)]),
@@ -260,7 +285,7 @@ let prog_eval_t_call_in_call_rec _ = show(answer) (Stream.take (run q
               fg == Nat.s yg &
               xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
               yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
-              fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))],
+              fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
                           SeqS (CallS (VarP fg, [PathE (VarP 0)]),
                                 WriteS (DerefP (VarP 0)))) &
               prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@@ -295,7 +320,7 @@ let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q
               fg == Nat.s yg &
               xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
               yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
-              fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)))],
+              fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
                           SeqS (WriteS (VarP xg),
                                 ReadS (DerefP (VarP 0)))) &
               prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@@ -363,10 +388,10 @@ let prog_eval_t_call_with_dif_mods_cp _ = show(answer) (Stream.take (run q
                     WriteS (DerefP (VarP 1));
                     WriteS (DerefP (VarP 2));
                     WriteS (DerefP (VarP 3))] fstmts &
-              fd == FunD ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)));
+              fd == FunD ([(Mode (NIn, NOut), RefT (Cp, UnitT (NRd, NeverWr)));
                            (Mode (In, NOut), RefT (Cp, UnitT (Rd, AlwaysWr)));
-                           (Mode (NIn, Out), RefT (Cp, UnitT (NRd, AlwaysWr)));
-                           (Mode (In, Out), RefT (Cp, UnitT (Rd, AlwaysWr)))],
+                           (Mode (NIn, Out), RefT (Rf, UnitT (NRd, AlwaysWr)));
+                           (Mode (In, Out), RefT (Rf, UnitT (Rd, AlwaysWr)))],
                           fstmts) &
               seqo [CallS (VarP fg, [PathE (VarP yg);
                                      PathE (VarP y2g);
@@ -454,7 +479,7 @@ let prog_cp_cap_synt_t_simple_call_ref_wr _ = show(answerCpCap) (Stream.take (ru
               fg == Nat.s yg &
               xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
               yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
-              fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (Rd, AlwaysWr)))],
+              fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
               prog_evalo prog st })
@@ -483,7 +508,7 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr _ = show(answerCpCap) (Stream.take
               fg == Nat.s yg &
               xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
               yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
-              fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (Rd, AlwaysWr)))],
+              fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
                                                ReadS (DerefP (VarP yg)))) &
@@ -506,7 +531,158 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak
               prog_evalo prog st })
   (fun q -> q#reify (CopyCap.prj_exn))))
 
-(* - complex tests *)
+(* - presentation tests *)
+
+(* simple types *)
+
+let prog_eval_t_presentation_simple_tp _ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog, xbg, xg,
+                          ybg, yg,
+                          zbg, zg,
+                          kbg, kg,
+                          fg, wg, gg, rg,
+                          xbd, xd,
+                          ybd, yd,
+                          zbd, zd,
+                          kbd, kd,
+                          fd, wd, gd, rd,
+                          fstmts, gstmts,
+                          stmts in
+              globals_min_ido xbg &
+              xg == Nat.s xbg &
+              ybg == Nat.s xg &
+              yg == Nat.s ybg &
+              zbg == Nat.s yg &
+              zg == Nat.s zbg &
+              kbg == Nat.s zg &
+              kg == Nat.s kbg &
+              fg == Nat.s kg &
+              wg == Nat.s fg &
+              gg == Nat.s wg &
+              rg == Nat.s gg &
+              xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) &
+              ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) &
+              zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) &
+              kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) &
+              seqo [ReadS (DerefP (VarP 0));
+                    WriteS (DerefP (VarP 0));
+                    ReadS (DerefP (VarP 1))] fstmts &
+              fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)));
+                           (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))],
+                          fstmts) &
+              wd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, MayWr)))],
+                          ChoiceS (WriteS (DerefP (VarP 0)), SkipS)) &
+              seqo [WriteS (DerefP (VarP 0));
+                    ChoiceS (WriteS (DerefP (VarP 1)), WriteS (DerefP (VarP 0)));
+                    ReadS (DerefP (VarP 0));
+                    ReadS (DerefP (VarP 1))] gstmts &
+              gd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)));
+                           (Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))],
+                          gstmts) &
+              rd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))],
+                          ReadS (DerefP (VarP 0))) &
+              seqo [
+                    CallS (VarP wg, [PathE (VarP xg)]);
+                    CallS (VarP rg, [PathE (VarP xg)]);
+                    CallS (VarP fg, [PathE (VarP xg); PathE (VarP yg)]);
+                    CallS (VarP rg, [PathE (VarP yg)]);
+                    CallS (VarP gg, [PathE (VarP zg); PathE (VarP kg)]);
+                    CallS (VarP wg, [PathE (VarP zg)]);
+                    WriteS (DerefP (VarP zg));
+                    CallS (VarP fg, [PathE (VarP yg); PathE (VarP zg)]);
+                    CallS (VarP rg, [PathE (VarP kg)])
+                  ] stmts &
+              prog == Prg ([xbd; xd;
+                            ybd; yd;
+                            zbd; zd;
+                            kbd; kd;
+                            fd; wd; gd; rd],
+                           stmts) &
+              prog_evalo prog q
+              })
+  (fun q -> q#reify (StEnv.prj_exn))))
+
+let prog_synt_t_presentation_simple_tp _ = show(answerCpCapList) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog, xbg, xg,
+                          ybg, yg,
+                          zbg, zg,
+                          kbg, kg,
+                          fg, wg, gg, rg,
+                          xbd, xd,
+                          ybd, yd,
+                          zbd, zd,
+                          kbd, kd,
+                          fd, wd, gd, rd,
+                          fstmts, gstmts,
+                          stmts,
+                          c_fx, c_fy, c_wx, c_gx, c_gy, c_rx,
+                          st in
+              globals_min_ido xbg &
+              xg == Nat.s xbg &
+              ybg == Nat.s xg &
+              yg == Nat.s ybg &
+              zbg == Nat.s yg &
+              zg == Nat.s zbg &
+              kbg == Nat.s zg &
+              kg == Nat.s kbg &
+              fg == Nat.s kg &
+              wg == Nat.s fg &
+              gg == Nat.s wg &
+              rg == Nat.s gg &
+              xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) &
+              ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) &
+              zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) &
+              kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) &
+              seqo [ReadS (DerefP (VarP 0));
+                    WriteS (DerefP (VarP 0));
+                    ReadS (DerefP (VarP 1))] fstmts &
+              fd == FunD ([(Mode (In, NOut), RefT (c_fx, UnitT (Rd, AlwaysWr)));
+                           (Mode (In, NOut), RefT (c_fy, UnitT (Rd, NeverWr)))],
+                          fstmts) &
+              wd == FunD ([(Mode (In, NOut), RefT (c_wx, UnitT (NRd, MayWr)))],
+                          ChoiceS (WriteS (DerefP (VarP 0)), SkipS)) &
+              seqo [WriteS (DerefP (VarP 0));
+                    ChoiceS (WriteS (DerefP (VarP 1)), WriteS (DerefP (VarP 0)));
+                    ReadS (DerefP (VarP 0));
+                    ReadS (DerefP (VarP 1))] gstmts &
+              gd == FunD ([(Mode (In, NOut), RefT (c_gx, UnitT (NRd, AlwaysWr)));
+                           (Mode (In, NOut), RefT (c_gy, UnitT (Rd, MayWr)))],
+                          gstmts) &
+              rd == FunD ([(Mode (In, NOut), RefT (c_rx, UnitT (Rd, NeverWr)))],
+                          ReadS (DerefP (VarP 0))) &
+              seqo [
+                    CallS (VarP wg, [PathE (VarP xg)]);
+                    CallS (VarP rg, [PathE (VarP xg)]);
+                    CallS (VarP fg, [PathE (VarP xg); PathE (VarP yg)]);
+                    CallS (VarP rg, [PathE (VarP yg)]);
+                    CallS (VarP gg, [PathE (VarP zg); PathE (VarP kg)]);
+                    CallS (VarP wg, [PathE (VarP zg)]);
+                    WriteS (DerefP (VarP zg));
+                    CallS (VarP fg, [PathE (VarP yg); PathE (VarP zg)]);
+                    CallS (VarP rg, [PathE (VarP kg)])
+                  ] stmts &
+              prog == Prg ([xbd; xd;
+                            ybd; yd;
+                            zbd; zd;
+                            kbd; kd;
+                            fd; wd; gd; rd],
+                           stmts) &
+              prog_evalo prog st &
+              q ==  [c_fx; c_fy; c_wx; c_gx; c_gy; c_rx]
+              })
+  (fun q -> q#reify (List.prj_exn CopyCap.prj_exn))))
+
+(* complex type *)
 
 let deref_accesso id v p' = ocanren {
     p' == DerefP (AccessP (VarP v, id))
@@ -516,6 +692,256 @@ let access_deref_accesso id_ext id_int v p' = ocanren {
     p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext)
   }
 
+(* --- *)
+
+let p_rw_unitTo tp = ocanren {
+    (* fresh r, w in *)
+    tp == UnitT (Rd, AlwaysWr)
+  }
+
+let p_rw_userTo tp = ocanren {
+    fresh x, y, z in
+    p_rw_unitTo x &
+    p_rw_unitTo y &
+    p_rw_unitTo z &
+    tp == TupleT [x; y; z]
+  }
+
+let p_rw_dataTo tp = ocanren {
+    fresh x, y in
+    p_rw_unitTo x &
+    p_rw_unitTo y &
+    tp == TupleT [x; y]
+  }
+
+let p_rw_timeTo tp = ocanren {
+    p_rw_unitTo tp
+  }
+
+let p_rw_requestTo cu cd ct tp = ocanren {
+    fresh userT, dataT, timeT in
+    p_rw_userTo userT &
+    p_rw_dataTo dataT &
+    p_rw_timeTo timeT &
+    tp == TupleT [RefT (cu, userT);
+                  RefT (cd, dataT);
+                  RefT (ct, timeT)]
+  }
+
+(* --- *)
+
+let p_any_unitTo tp = ocanren {
+    fresh r, w in
+    tp == UnitT (r, w)
+  }
+
+let p_any_userTo tp = ocanren {
+    fresh x, y, z in
+    p_any_unitTo x &
+    p_any_unitTo y &
+    p_any_unitTo z &
+    tp == TupleT [x; y; z]
+  }
+
+let p_any_dataTo tp = ocanren {
+    fresh x, y in
+    p_any_unitTo x &
+    p_any_unitTo y &
+    tp == TupleT [x; y]
+  }
+
+let p_any_timeTo tp = ocanren {
+    p_any_unitTo tp
+  }
+
+let p_any_requestTo cu cd ct tp = ocanren {
+    fresh userT, dataT, timeT in
+    p_any_userTo userT &
+    p_any_dataTo dataT &
+    p_any_timeTo timeT &
+    tp == TupleT [RefT (cu, userT);
+                  RefT (cd, dataT);
+                  RefT (ct, timeT)]
+  }
+
+(* --- *)
+
+let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog,
+                    userT, dataT, timeT, requestT,
+                    requestArgsT,
+                    userE, dataE, timeE, requestE,
+                    userVID, dataVID, timeVID, requestVID,
+                    sendFID, sendD, sendBranchStmts, sendStmts,
+                    stmts in
+              globals_min_ido userVID &
+              dataVID == Nat.s userVID &
+              timeVID == Nat.s dataVID &
+              requestVID == Nat.s timeVID &
+              sendFID == Nat.s requestVID &
+
+              p_rw_userTo userT &
+              p_rw_dataTo dataT &
+              p_rw_timeTo timeT &
+              p_rw_requestTo Cp Cp Cp requestT &
+              p_any_requestTo Cp Cp Cp requestArgsT & (* NOTE: for now *)
+
+              userE == TupleE [UnitE; UnitE; UnitE] &
+              dataE == TupleE [UnitE; UnitE] &
+              timeE == UnitE &
+              requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] &
+
+              fresh data_p0, data_p1, time_p,
+                    user_id_p, user_name_p, user_surname_p in
+              access_deref_accesso 0 1 0 data_p0 &
+              access_deref_accesso 1 1 0 data_p1 &
+              deref_accesso 2 0 time_p &
+              access_deref_accesso 0 0 0 user_id_p &
+              access_deref_accesso 1 0 0 user_name_p &
+              access_deref_accesso 2 0 0 user_surname_p &
+              seqo [ReadS data_p0;
+                    ReadS data_p1;
+                    WriteS data_p0;
+                    WriteS data_p1;
+
+                    ReadS user_name_p;
+                    WriteS user_name_p] sendBranchStmts &
+              seqo [sendBranchStmts; (* TMP *)
+                    (* TODO: FIXME *)
+                    (* ChoiceS (sendBranchStmts, SkipS); *)
+                    WriteS time_p;
+
+                    ReadS data_p0;
+                    ReadS data_p1;
+                    ReadS time_p;
+                    ReadS user_id_p;
+                    ReadS user_name_p;
+                    ReadS user_surname_p] sendStmts &
+              (* sendStmts == SkipS & *)
+              sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) &
+
+              fresh time_gp, user_name_gp, user_surname_gp in
+              deref_accesso 2 requestVID time_gp &
+              access_deref_accesso 1 0 requestVID user_name_gp &
+              access_deref_accesso 2 0 requestVID user_surname_gp &
+              seqo [
+                    CallS (VarP sendFID, [PathE (VarP requestVID)]);
+                    WriteS time_gp;
+                    (* TODO: FIXME *)
+                    (* ChoiceS (ReadS user_name_gp, *)
+                             (* ReadS user_surname_gp); *)
+                    ReadS user_name_gp; (* TMP *)
+                    ReadS user_surname_gp; (* TMP *)
+                    ReadS time_gp
+                  ] stmts &
+              prog == Prg ([
+                            VarD (userT, userE);
+                            VarD (dataT, dataE);
+                            VarD (timeT, timeE);
+                            VarD (requestT, requestE);
+                            sendD
+                            ],
+                           stmts
+                           ) &
+              prog_evalo prog q
+              })
+  (fun q -> q#reify (StEnv.prj_exn))))
+
+let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog,
+                    userT, dataT, timeT, requestT,
+                    requestArgsT,
+                    userE, dataE, timeE, requestE,
+                    userVID, dataVID, timeVID, requestVID,
+                    sendFID, sendD, sendBranchStmts, sendStmts,
+                    stmts,
+                    st, c_u, c_d, c_t in
+              globals_min_ido userVID &
+              dataVID == Nat.s userVID &
+              timeVID == Nat.s dataVID &
+              requestVID == Nat.s timeVID &
+              sendFID == Nat.s requestVID &
+
+              p_rw_userTo userT &
+              p_rw_dataTo dataT &
+              p_rw_timeTo timeT &
+              p_rw_requestTo Cp Cp Cp requestT &
+              p_any_requestTo c_u c_d c_t requestArgsT & (* NOTE: for now *)
+
+              userE == TupleE [UnitE; UnitE; UnitE] &
+              dataE == TupleE [UnitE; UnitE] &
+              timeE == UnitE &
+              requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] &
+
+              fresh data_p0, data_p1, time_p,
+                    user_id_p, user_name_p, user_surname_p in
+              access_deref_accesso 0 1 0 data_p0 &
+              access_deref_accesso 1 1 0 data_p1 &
+              deref_accesso 2 0 time_p &
+              access_deref_accesso 0 0 0 user_id_p &
+              access_deref_accesso 1 0 0 user_name_p &
+              access_deref_accesso 2 0 0 user_surname_p &
+              seqo [ReadS data_p0;
+                    ReadS data_p1;
+                    WriteS data_p0;
+                    WriteS data_p1;
+
+                    ReadS user_name_p;
+                    WriteS user_name_p] sendBranchStmts &
+              seqo [sendBranchStmts; (* TMP *)
+                    (* TODO: FIXME *)
+                    (* ChoiceS (sendBranchStmts, SkipS); *)
+                    WriteS time_p;
+
+                    ReadS data_p0;
+                    ReadS data_p1;
+                    ReadS time_p;
+                    ReadS user_id_p;
+                    ReadS user_name_p;
+                    ReadS user_surname_p] sendStmts &
+              (* sendStmts == SkipS & *)
+              sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) &
+
+              fresh time_gp, user_name_gp, user_surname_gp in
+              deref_accesso 2 requestVID time_gp &
+              access_deref_accesso 1 0 requestVID user_name_gp &
+              access_deref_accesso 2 0 requestVID user_surname_gp &
+              seqo [
+                    CallS (VarP sendFID, [PathE (VarP requestVID)]);
+                    WriteS time_gp;
+                    (* TODO: FIXME *)
+                    (* ChoiceS (ReadS user_name_gp, *)
+                             (* ReadS user_surname_gp); *)
+                    ReadS user_name_gp; (* TMP *)
+                    ReadS user_surname_gp; (* TMP *)
+                    ReadS time_gp
+                  ] stmts &
+              prog == Prg ([
+                            VarD (userT, userE);
+                            VarD (dataT, dataE);
+                            VarD (timeT, timeE);
+                            VarD (requestT, requestE);
+                            sendD
+                            ],
+                           stmts
+                           ) &
+              prog_evalo prog st &
+              q == [c_u; c_d; c_t]
+              })
+  (fun q -> q#reify (List.prj_exn CopyCap.prj_exn))))
+
+(* - complex tests *)
+
+(* let deref_accesso id v p' = ocanren { *)
+    (* p' == DerefP (AccessP (VarP v, id)) *)
+  (* } *)
+
+(* let access_deref_accesso id_ext id_int v p' = ocanren { *)
+    (* p' == AccessP (DerefP (AccessP (VarP v, id_int)), id_ext) *)
+  (* } *)
+
 let access_deref_access_deref_accesso id_ext id_mid id_int v p' = ocanren {
     p' == AccessP (DerefP (AccessP (DerefP (AccessP (VarP v, id_int)), id_mid)), id_ext)
   }
@@ -655,11 +1081,84 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
               prog_evalo prog q })
   (fun q -> q#reify (StEnv.prj_exn))))
 
+(* rw versions *)
+
 let rw_unitTo tp = ocanren {
     (* fresh r, w in *)
     tp == UnitT (Rd, AlwaysWr)
   }
 
+let rw_user_utilsTo tp = ocanren {
+    fresh x, y in
+    rw_unitTo x &
+    rw_unitTo y &
+    tp == TupleT [x; y]
+  }
+
+let rw_user_infoTo tp = ocanren {
+    fresh x, y, z in
+    rw_unitTo x &
+    rw_unitTo y &
+    rw_unitTo z &
+    tp == TupleT [x; y; z]
+  }
+
+let rw_versionTo tp = ocanren {
+    fresh x, y, z in
+    rw_unitTo x &
+    rw_unitTo y &
+    rw_unitTo z &
+    tp == TupleT [x; y; z]
+  }
+
+let rw_utilsTo tp = ocanren {
+    fresh x, y in
+    rw_unitTo x &
+    rw_unitTo y &
+    tp == TupleT [x; y]
+  }
+
+let rw_dataTo tp = ocanren {
+    rw_unitTo tp
+  }
+
+let rw_op_dateTo tp = ocanren {
+    rw_unitTo tp
+  }
+
+let rw_userTo cu ci tp = ocanren {
+    fresh utilsT, infoT in
+    rw_user_infoTo infoT &
+    rw_user_utilsTo utilsT &
+    tp == TupleT [RefT (cu, utilsT) (* 0 utils *);
+                  RefT (ci, infoT) (* 1 info *)]
+  }
+
+let rw_requestTo cus cv cut cd cus_u cus_i tp = ocanren {
+    fresh userT, versionT, utilsT, dataT, op_dateT in
+    rw_userTo cus_u cus_i userT &
+    rw_versionTo versionT &
+    rw_utilsTo utilsT &
+    rw_dataTo dataT &
+    rw_op_dateTo op_dateT &
+    tp == TupleT [RefT (cus, userT) (* 0 user *);
+                  RefT (cv, versionT) (* 1 version *);
+                  RefT (cut, utilsT) (* 2 utils *);
+                  RefT (cd, dataT) (* 3 data *);
+                  op_dateT (* 4 operation_date *)]
+  }
+let rw_moded_requestTo cus cv cut cd cus_u cus_i tp = ocanren {
+    fresh requestT in
+    rw_requestTo cus cv cut cd cus_u cus_i requestT &
+    tp == (Mode (In, NOut), requestT)
+  }
+let rw_boxed_moded_requestTo tp = ocanren {
+    fresh cus, cv, cut, cd, cus_u, cus_i in
+    rw_moded_requestTo cus cv cut cd cus_u cus_i tp
+  }
+
+(* any versions *)
+
 let any_unitTo tp = ocanren {
     fresh r, w in
     tp == UnitT (r, w)
@@ -667,40 +1166,40 @@ let any_unitTo tp = ocanren {
 
 let any_user_utilsTo tp = ocanren {
     fresh x, y in
-    rw_unitTo x &
-    rw_unitTo y &
+    any_unitTo x &
+    any_unitTo y &
     tp == TupleT [x; y]
   }
 
 let any_user_infoTo tp = ocanren {
     fresh x, y, z in
-    rw_unitTo x &
-    rw_unitTo y &
-    rw_unitTo z &
+    any_unitTo x &
+    any_unitTo y &
+    any_unitTo z &
     tp == TupleT [x; y; z]
   }
 
 let any_versionTo tp = ocanren {
     fresh x, y, z in
-    rw_unitTo x &
-    rw_unitTo y &
-    rw_unitTo z &
+    any_unitTo x &
+    any_unitTo y &
+    any_unitTo z &
     tp == TupleT [x; y; z]
   }
 
 let any_utilsTo tp = ocanren {
     fresh x, y in
-    rw_unitTo x &
-    rw_unitTo y &
+    any_unitTo x &
+    any_unitTo y &
     tp == TupleT [x; y]
   }
 
 let any_dataTo tp = ocanren {
-    rw_unitTo tp
+    any_unitTo tp
   }
 
 let any_op_dateTo tp = ocanren {
-    rw_unitTo tp
+    any_unitTo tp
   }
 
 let any_userTo cu ci tp = ocanren {
@@ -767,13 +1266,13 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
                     (* synt *)
                     st in
               (* types *)
-              any_unitTo uT_r_aw &
-              any_user_utilsTo user_utilsT &
-              any_user_infoTo user_infoT &
-              any_userTo Cp Cp userT &
-              any_versionTo versionT &
-              any_utilsTo utilsT &
-              any_requestTo Cp Cp Cp Cp Cp Cp requestT &
+              rw_unitTo uT_r_aw &
+              rw_user_utilsTo user_utilsT &
+              rw_user_infoTo user_infoT &
+              rw_userTo Cp Cp userT &
+              rw_versionTo versionT &
+              rw_utilsTo utilsT &
+              rw_requestTo Cp Cp Cp Cp Cp Cp requestT &
               (* moded_requestTo moded_requestT & *)
               (* global vars init exprs *)
               user_utilsE == TupleE [UnitE (* 0 id *); UnitE] &
@@ -849,15 +1348,16 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
                    send_allF &
 
               fresh mrT_gvi, mrT_uv, mrT_s, mrT_sa in
-              fresh gvi_c0, gvi_c1, gvi_c2, gvi_c3, gvi_c4, gvi_c5, mrT' in
-              any_moded_requestTo gvi_c0 gvi_c1 gvi_c2 gvi_c3 gvi_c4 gvi_c5 mrT' &
+              (* fresh gvi_c0, gvi_c1, gvi_c2, gvi_c3, gvi_c4, gvi_c5, mrT' in *)
+              (* any_moded_requestTo gvi_c0 gvi_c1 gvi_c2 gvi_c3 gvi_c4 gvi_c5 mrT' & *)
               (* TODO *)
-              (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_gvi & *)
-              (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_uv & *)
-              (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_s & *)
-              (* any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_sa & *)
+              any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_gvi &
+              any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_uv &
+              any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_s &
+              any_moded_requestTo Cp Cp Cp Cp Cp Cp mrT_sa &
 
-              q == [gvi_c0; gvi_c1; gvi_c2; gvi_c3; gvi_c4; gvi_c5] &
+              q == [Cp] &
+              (* [gvi_c0; gvi_c1; gvi_c2; gvi_c3; gvi_c4; gvi_c5] & *)
 
               prog == Prg ([
                 VarD (user_utilsT, user_utilsE);
@@ -867,17 +1367,17 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
                 VarD (utilsT, utilsE);
                 VarD (uT_r_aw, UnitE); (* data *)
                 VarD (requestT, requestE);
-                FunD ([mrT'], get_version_idF);
-                FunD ([mrT'], updated_versionF);
-                FunD ([mrT'], sendF);
-                FunD ([mrT'], send_allF)
-                (* FunD ([mrT_gvi], get_version_idF); *)
-                (* FunD ([mrT_uv], updated_versionF); *)
-                (* FunD ([mrT_s], sendF); *)
-                (* FunD ([mrT_sa], send_allF) *)
+                (* FunD ([mrT'], get_version_idF); *)
+                (* FunD ([mrT'], updated_versionF); *)
+                (* FunD ([mrT'], sendF); *)
+                (* FunD ([mrT'], send_allF) *)
+                FunD ([mrT_gvi], get_version_idF);
+                FunD ([mrT_uv], updated_versionF);
+                FunD ([mrT_s], sendF);
+                FunD ([mrT_sa], send_allF)
               ],
               (* SkipS *)
               CallS (VarP send_allID, [PathE (VarP requestID)])
               ) &
               prog_evalo prog st })
-  (fun q -> q#reify (List.prj_exn CopyCap.prj_exn)))) (* TODO: list *)
+  (fun q -> q#reify (List.prj_exn CopyCap.prj_exn))))