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

model_with_structures/analyzer.ml

@@ -200,8 +200,8 @@ struct
     | 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
@@ -570,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
@@ -987,6 +988,117 @@ struct
     Printf.printf "done!";
     [%expect {| done! |}]
 
+  (* - tests for presentation *)
+
+  let%expect_test "presentation test 1 (simple types), dsl" =
+    prog_eval_noret (
+      [
+        defgu uT_r_aw;
+        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)
+        )
+      ],
+      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 *)

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
 
@@ -581,28 +581,26 @@ $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 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$,
   )
 ))
 

model_with_structures/synthesizer.ml

@@ -569,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 --- *)
@@ -592,7 +592,7 @@ 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
@@ -613,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 } |
+        (* { c == Rf & mem_with_id' == Std.pair mem v } | *)
         { fresh v', mem_cp, v_cp, mem_add, id_add in
-            c == Cp &
+          (* 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) } } } |
+          mem_with_id' == (mem_add, RefV id_add) } } |
       { fresh vs, tps, mem', vs' in
         v == TupleV vs &
         tp == TupleT tps &
@@ -727,8 +727,8 @@ struct
     ocanren {
       { u == ZeroMV & v == ZeroMV & u' == ZeroMV } |
       { u == BotMV & v == BotMV & u' == BotMV } |
-      { u =/= ZeroMV & v =/= ZeroMV &
-        u =/= BotMV & v =/= BotMV & 
+      { { u =/= ZeroMV | { u == ZeroMV & v =/= ZeroMV } } &
+        { u =/= BotMV | { u == BotMV & v =/= BotMV } } & 
         u' == SmthMV }
   }
 
@@ -749,8 +749,8 @@ struct
     ocanren {
       { u == OneWV & v == OneWV & u' == OneWV } |
       { u == ZeroWV & v == ZeroWV & u' == ZeroWV } |
-      { u =/= ZeroWV & v =/= ZeroWV &
-        u =/= OneWV & v =/= OneWV & 
+      { { u =/= ZeroWV | { u == ZeroWV & v =/= ZeroWV } } &
+        { u =/= OneWV | { u == OneWV & v =/= OneWV } } & 
         u' == SmthWV }
   }
 
@@ -775,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 &

model_with_structures/tests_f.ml

@@ -28,16 +28,30 @@ open StEnv
 (* - shortcuts *)
 
 (* 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 *)
@@ -517,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))
@@ -527,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)
   }
@@ -965,4 +1380,4 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
               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))))