struct: make mode constructor named in analyzers (to unify code view with synt)

model_with_structures/analyzer.ml

@@ -14,7 +14,7 @@ struct
   type in_cap = In | NIn
   type out_cap = Out | NOut
 
-  type mode = in_cap * out_cap
+  type mode = Mode of in_cap * out_cap
 
   type path = VarP of data | DerefP of path | AccessP of path * data
 
@@ -103,10 +103,12 @@ struct
 
   let types_add (types : types) (x : data) (t : atype) =
     (x, t) :: types
-
   let vals_add (vals : vals) (x : data) (id : memid) =
     (x, id) :: vals
 
+  let mode_in (m : mode) : in_cap = match m with Mode (i, _) -> i
+  let mode_out (m : mode) : out_cap = match m with Mode (_, o) -> o
+
   (* - utils *)
 
   let rec list_replace (xs : 'a list) (id : int) (y : 'a) : 'a list = match xs, id with
@@ -349,9 +351,9 @@ struct
   (* 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) &&
+    (mode_out m != Out || c == Rf) &&
-    (snd m != Out || w == AlwaysWr) &&
+    (mode_out m != Out || w == AlwaysWr) &&
-    (r != Rd || fst m == In)
+    (r != Rd || mode_in m == In)
 
   let tryread (r : read_cap) (v_m : memval)
               (v_r : readval) (v_w : writeval) : value =
@@ -363,10 +365,10 @@ struct
   
   let tryspoil (m : mode) (w : write_cap) (v_m : memval) : memval =
     match m, w with
-      | (_, Out), AlwaysWr -> v_m
+      | Mode (_, Out), AlwaysWr -> v_m
-      | (_, Out), MayWr -> v_m
+      | Mode (_, Out), MayWr -> v_m
-      | (_, NOut), AlwaysWr -> BotMV
+      | Mode (_, NOut), AlwaysWr -> BotMV
-      | (_, NOut), MayWr -> SmthMV
+      | Mode (_, NOut), MayWr -> SmthMV
       | _ -> raise @@ Typing_error "tryspoil: unexpected pair mode + write cap"
 
   let rec valspoil (mem : mem) (v : value) (t : atype)
@@ -607,7 +609,7 @@ struct
   let rfT t = RefT (Rf, t)
   let cpT t = RefT (Cp, t)
 
-  let moded t = ((In, NOut), t)
+  let moded t = (Mode (In, NOut), t)
 
   let defg t = VarD t
 
@@ -868,7 +870,7 @@ struct
           wrS @@ drf @@ v0
         );
         FunD (
-          [((In, Out), rfT @@ uT_aw)],
+          [(Mode (In, Out), rfT @@ uT_aw)],
           wrS @@ drf @@ v0
         )
       ],
@@ -930,10 +932,10 @@ struct
         defg (rfT uT_r_aw);
         FunD (
           [
-            ((NIn, NOut), cpT @@ uT);
+            (Mode (NIn, NOut), cpT @@ uT);
-            ((In, NOut), cpT @@ uT_r_aw);
+            (Mode (In, NOut), cpT @@ uT_r_aw);
-            ((NIn, Out), rfT @@ uT_aw);
+            (Mode (NIn, Out), rfT @@ uT_aw);
-            ((In, Out), rfT @@ uT_r_aw);
+            (Mode (In, Out), rfT @@ uT_r_aw);
           ],
           (rdS @@ drf @@ v1) #.
           (rdS @@ drf @@ v3) #.
@@ -964,10 +966,10 @@ struct
         defg (rfT uT_r_aw);
         FunD (
           [
-            ((NIn, NOut), rfT @@ uT);
+            (Mode (NIn, NOut), rfT @@ uT);
-            ((In, NOut), rfT @@ uT_r);
+            (Mode (In, NOut), rfT @@ uT_r);
-            ((NIn, Out), rfT @@ uT_aw);
+            (Mode (NIn, Out), rfT @@ uT_aw);
-            ((In, Out), rfT @@ uT_r_aw);
+            (Mode (In, Out), rfT @@ uT_r_aw);
           ],
           (rdS @@ drf @@ v1) #.
           (rdS @@ drf @@ v3) #.
@@ -1049,130 +1051,4 @@ struct
     );
     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; *)
-        (* defg 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; *)
-        (* defg 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/analyzer_rw.ml

@@ -1,35 +1,48 @@
-module Functional =
+module FunctionalRW =
 struct
+  open GT
 
   type data = int
+  [@@deriving gt ~options:{ show }]
   type memid = int
+  [@@deriving gt ~options:{ show }]
 
   (* --- syntax --- *)
 
-  type read_cap = Rd | NRd (* | UndefRd ? *)
+  type read_cap = Rd | NRd | UndefRd
+  [@@deriving gt ~options:{ show }]
 
-  type write_cap = AlwaysWr | MayWr | NeverWr (* | UndefWr ? *)
+  type write_cap = AlwaysWr | MayWr | NeverWr | UndefWr
-  type copy_cap = Cp | Rf
+  [@@deriving gt ~options:{ show }]
+  type copy_cap = Rf | Cp
+  [@@deriving gt ~options:{ show }]
 
   type in_cap = In | NIn
+  [@@deriving gt ~options:{ show }]
   type out_cap = Out | NOut
+  [@@deriving gt ~options:{ show }]
 
-  type mode = in_cap * out_cap
+  type mode = Mode of in_cap * out_cap
+  [@@deriving gt ~options:{ show }]
 
   type path = VarP of data | DerefP of path | AccessP of path * data
+  [@@deriving gt ~options:{ show }]
 
   type atype = UnitT of read_cap * write_cap
              | RefT of copy_cap * atype
              | TupleT of atype list
              | FunT of (mode * atype) list (* TODO: declaration id for ease of impl / performance instead (?) *)
+  [@@deriving gt ~options:{ show }]
 
   type mtype = mode * atype
+  [@@deriving gt ~options:{ show }]
 
   type expr = UnitE
             | PathE of path
             (* TODO: extend to include arbitrary path *)
             | RefE of data
             | TupleE of expr list
+  [@@deriving gt ~options:{ show }]
 
   type stmt = SkipS
             | CallS of path * expr list
@@ -37,11 +50,14 @@ struct
             | ReadS of path
             | SeqS of stmt * stmt
             | ChoiceS of stmt * stmt
+  [@@deriving gt ~options:{ show }]
 
   type decl = VarD of (* data * *) atype (* * expr *)
             | FunD of (* data * *) (* (data * *) mtype (* )  *) list * stmt
+  [@@deriving gt ~options:{ show }]
 
   type prog = decl list * stmt
+  [@@deriving gt ~options:{ show }]
 
   (* --- exceptions --- *)
 
@@ -56,6 +72,7 @@ struct
   exception Typing_error of string
   exception Eval_error of string
   exception Cant_fold3_error
+  exception Cant_deduce_rw_error of string
 
   (* value model & memory model *)
 
@@ -67,26 +84,36 @@ struct
                  (* | TupleDV of deepvalue list *)
 
   type memval = ZeroMV | SmthMV | BotMV (* | TopMV ?? *)
+  [@@deriving gt ~options:{ show }]
   type readval = ZeroRV | OneRV | TopRV
+  [@@deriving gt ~options:{ show }]
   type writeval = ZeroWV | SmthWV | OneWV
+  [@@deriving gt ~options:{ show }]
 
   type value = UnitV of memval * readval * writeval
              | FunV (* of ((* data list * *) stmt) list *)
              | RefV of memid
              | TupleV of value list
+  [@@deriving gt ~options:{ show }]
 
   type revpath = VarRP | DerefRP of revpath | AccessRP of revpath * data
+  [@@deriving gt ~options:{ show }]
 
   type action = ReadA | AlwaysWriteA | MayWriteA
+  [@@deriving gt ~options:{ show }]
 
   (* TODO: any additional difference between rvalue and lvalue now ?? *)
 
   (* --- *)
 
   type mem = value list * memid (* NOTE: memory and first free elem *)
+  [@@deriving gt ~options:{ show }]
   type types = (data * atype) list
+  [@@deriving gt ~options:{ show }]
   type vals = (data * memid) list
+  [@@deriving gt ~options:{ show }]
   type state = mem * types * vals
+  [@@deriving gt ~options:{ show }]
 
   (* --- *)
 
@@ -103,10 +130,12 @@ struct
 
   let types_add (types : types) (x : data) (t : atype) =
     (x, t) :: types
-
   let vals_add (vals : vals) (x : data) (id : memid) =
     (x, id) :: vals
 
+  let mode_in (m : mode) : in_cap = match m with Mode (i, _) -> i
+  let mode_out (m : mode) : out_cap = match m with Mode (_, o) -> o
+
   (* - utils *)
 
   let rec list_replace (xs : 'a list) (id : int) (y : 'a) : 'a list = match xs, id with
@@ -192,6 +221,8 @@ struct
     match t with
     | UnitT (Rd, _) -> (mem, UnitV (ZeroMV, ZeroRV, ZeroWV))
     | UnitT (NRd, _) -> (mem, UnitV (BotMV, ZeroRV, ZeroWV))
+    (* NOTE: ignore pre-tag in rw-analysis *)
+    | UnitT (UndefRd, _) -> (mem, UnitV (ZeroMV, ZeroRV, ZeroWV))
     | FunT _ -> raise @@ Typing_error "valbuild: funciton value is not supported"
     | RefT (_, t) -> let (mem', v') = valbuild mem t in
                      let (mem'', id'') = mem_add mem' v' in
@@ -201,22 +232,6 @@ struct
                    let mem', vs' = List.fold_right folder ts (mem, []) in
                    (mem', TupleV vs')
 
-  (* NOTE: not needed now *)
-  (* let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = *)
-    (* 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 (_, 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 v t (mem, vs') -> let (mem', v') = valcopy mem v t in *)
-                                                                 (* (mem', v' :: vs') in *) 
-                              (* let mem', vs' = List.fold_right2 folder vs ts (mem, []) in *)
-                              (* (mem', TupleV vs') *)
-    (* | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type" *)
-
   (* - action rules *)
 
   let memvmod (a : action) (v_m : memval) : memval =
@@ -338,20 +353,14 @@ struct
   (* TODO: better way ??? *)
   let globals_min_id : data = 1000
 
-  let prog_init (prog : prog) : state =
-    match prog with (decls, _) -> fst @@ List.fold_left (* TODO: FIXME: check x's order *)
-                                    (fun (st, x) d -> (add_decl st x d, x + 1))
-                                    (empty_state, globals_min_id)
-                                    decls
-
   (* - call values spoil *)
 
   (* 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) &&
+    (mode_out m != Out || c == Rf) &&
-    (snd m != Out || w == AlwaysWr) &&
+    (mode_out m != Out || w == AlwaysWr || w == UndefWr) &&
-    (r != Rd || fst m == In)
+    (r != Rd || mode_in m == In)
 
   let tryread (r : read_cap) (v_m : memval)
               (v_r : readval) (v_w : writeval) : value =
@@ -359,14 +368,16 @@ struct
       | Rd -> UnitV (memvmod ReadA v_m,
                      readvmod ReadA v_r,
                      writevmod ReadA v_w)
-      | NRd -> UnitV (v_m, v_r, v_w) 
+      | NRd -> UnitV (v_m, v_r, v_w)
+      | UndefRd -> raise @@ Cant_deduce_rw_error "tryread"
   
   let tryspoil (m : mode) (w : write_cap) (v_m : memval) : memval =
     match m, w with
-      | (_, Out), AlwaysWr -> v_m
+      | Mode (_, Out), AlwaysWr -> v_m
-      | (_, Out), MayWr -> v_m
+      | Mode (_, Out), MayWr -> v_m
-      | (_, NOut), AlwaysWr -> BotMV
+      | Mode (_, NOut), AlwaysWr -> BotMV
-      | (_, NOut), MayWr -> SmthMV
+      | Mode (_, NOut), MayWr -> SmthMV
+      | _, UndefWr -> raise @@ Cant_deduce_rw_error "tryspoil"
       | _ -> raise @@ Typing_error "tryspoil: unexpected pair mode + write cap"
 
   let rec valspoil (mem : mem) (v : value) (t : atype)
@@ -386,10 +397,12 @@ struct
                 then (memvmod AlwaysWriteA v_m',
                       readvmod AlwaysWriteA v_r',
                       writevmod AlwaysWriteA v_w')
-                else (* MayWr *)
+              else if w == UndefWr
-                     (memvmod MayWriteA v_m',
+                then raise @@ Cant_deduce_rw_error "valspoil"
-                      readvmod MayWriteA v_r',
+              else (* MayWr *)
-                      writevmod MayWriteA v_w'))
+                   (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''))
@@ -440,32 +453,42 @@ struct
 
   (* --- *)
 
+  let readval_to_cap (v_w : readval) : read_cap =
+    match v_w with
+      | ZeroRV -> NRd
+      | OneRV -> Rd
+      | TopRV -> NRd
+
   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 =
+  (* NOTE: in analyzer rw tags check replaces tags with calculated ones *)
+  let rec tags_check (mem : mem) (v : value) (t : atype) : atype =
     match v, t with
       | UnitV (v_m, v_r, v_w), UnitT (r, w) ->
-        if (r == Rd) && (v_r != OneRV)
+        let r' = readval_to_cap v_r in
-          then raise @@ Eval_error "tags_check: wrong read tag"
+        let w' = writeval_to_cap v_w in
-        else if (r == NRd) && (v_r == OneRV)
+        if r != UndefRd && r != r'
-          then raise @@ Eval_error "tags_check: wrong not read tag"
+          then raise @@ Eval_error "tags_check: not undef read tag & not correct"
-        else if writeval_to_cap v_w != w
+        else if w != UndefWr && w != w'
-          then raise @@ Eval_error "tags_check: wrong write tag"
+          then raise @@ Eval_error "tags_check: not undef write tag & not correct"
-        else ()
+        else UnitT (r', w')
-      | FunV, FunT _ -> ()
+      | FunV, FunT _ -> t
-      | RefV id, RefT (_, t) -> tags_check mem (mem_get mem id) t
+      | RefV id, RefT (c, t) -> RefT (c, tags_check mem (mem_get mem id) t)
-      | TupleV vs, TupleT ts -> ignore @@ List.map2 (tags_check mem) vs ts
+      | TupleV vs, TupleT ts -> TupleT (List.map2 (tags_check mem) vs ts)
       | _, _ -> raise @@ Typing_error "tags_check"
 
   (* - writability check *)
 
   let rec is_all_type_writable (t : atype) : bool =
     match t with
-      | UnitT (_, w) -> w == MayWr || w == AlwaysWr
+      | UnitT (_, MayWr) -> true
+      | UnitT (_, AlwaysWr) -> true
+      | UnitT (_, NeverWr) -> false
+      | UnitT (_, UndefWr) -> true (* NOTE: tag is not deduced yet, consider writable *)
       | FunT _ -> true
       | RefT (_, t) -> is_all_type_writable t
       | TupleT ts -> List.for_all is_all_type_writable ts
@@ -514,28 +537,51 @@ struct
 
   (* - function evaluation *)
 
-  let rec func_eval (state : state) (d : decl) : unit =
+  let rec replace_rw_undef_with_r_aw (t : atype) : atype = match t with
+    | UnitT (r, w) -> let r' = if r == UndefRd then Rd else r in
+                      let w' = if w == UndefWr then AlwaysWr else w in
+                      UnitT (r', w')
+    | RefT (c, t) -> RefT (c, replace_rw_undef_with_r_aw t)
+    | TupleT ts -> TupleT (List.map replace_rw_undef_with_r_aw ts)
+    | FunT ts -> FunT ts (* NOTE: can't properly deduce *)
+
+  (* NOTE: in analyzer rw replaces read & write tags with calculated ones *)
+  let rec func_eval (state : state) (d : decl) : decl =
     match d with
     | FunD (ts, stmt) ->
       (let (state_with_args, _) = List.fold_left
          (fun (st, x) (m, t) -> (addarg st x t, x + 1))
          (state, 0) ts in
        match stmt_eval state_with_args stmt with (mem_after_stmt, _, vals_after_stmt) ->
-       ignore @@ List.fold_left
+       let (_, ts') = List.fold_left
-         (fun x (_, t) ->
+         (fun (x, ts_acc) (m, 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)
+            let t' = tags_check mem_after_stmt v t in
-         0 ts)
+            (x + 1, (m, t') :: ts_acc))
-    | VarD _ -> ()
+         (0, []) ts in
+       (* TODO: FIXME: isure that need reverse ? *)
+       FunD (List.rev ts', stmt))
+    (* NOTE: tags for globals not checked and not important in current implementation *)
+    | VarD t -> VarD (replace_rw_undef_with_r_aw t)
 
   (* --- program execution --- *)
 
-  let prog_eval (prog : prog) : state =
+  (* NOTE: decls returned in the reversed order (?) *)
+  let prog_init (prog : prog) : (state * decl list) =
+    match prog with (decls, _) -> let (st', decls', _) = List.fold_left (* TODO: FIXME: check x's order *)
+                                    (fun (st, decls', x) d ->
+                                      let d' = func_eval st d in 
+                                      (add_decl st x d', d' :: decls', x + 1))
+                                    (empty_state, [], globals_min_id)
+                                    decls in
+                                  (st', List.rev decls')
+
+  let prog_eval (prog : prog) : prog =
     match prog with (decls, s) ->
-    let init_state = prog_init prog in
+    let (init_state, decls') = prog_init prog in
-    ignore @@ List.map (func_eval init_state) decls;
+    ignore @@ stmt_eval init_state s;
-    stmt_eval init_state s
+    (decls', s)
 
   let prog_eval_noret (prog : prog) : unit =
     ignore @@ prog_eval prog
@@ -603,11 +649,12 @@ struct
   let uT_mw = UnitT (NRd, MayWr)
   let uT_r = UnitT (Rd, NeverWr)
   let uT = UnitT (NRd, NeverWr)
+  let uT_undef = UnitT (UndefRd, UndefWr)
 
   let rfT t = RefT (Rf, t)
   let cpT t = RefT (Cp, t)
 
-  let moded t = ((In, NOut), t)
+  let moded t = (Mode (In, NOut), t)
 
   let defg t = VarD t
 
@@ -641,6 +688,86 @@ struct
                              (v_memval_is (mem_get mem id3) SmthMV);
     [%expect {| 0 1 2 true true true true true true |}]
 
+  (* - simple rw tags gen tests *)
+
+  let%expect_test "simple call with read, dsl, rw gen" =
+    let prog' = prog_eval (
+      [
+        defg (rfT uT_r_mw);
+        FunD (
+          [moded @@ cpT @@ uT_undef],
+          rdS @@ drf @@ v0
+        )
+      ],
+      callS vg1 [pE vg0]
+    ) in
+    prog_eval_noret prog';
+    print_endline @@ show(prog) prog';
+    [%expect {| ([VarD (RefT (Rf, UnitT (Rd, MayWr))); FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))], ReadS (DerefP (VarP (0))))], CallS (VarP (1001), [PathE (VarP (1000))])) |}]
+
+  let%expect_test "presentation test 1 (simple types), dsl, rw gen" =
+    let prog' = prog_eval (
+      [
+        defg (rfT uT_r_aw); (* x *)
+        defg (rfT uT_r_aw); (* y *)
+        defg (rfT uT_r_aw); (* z *)
+        defg (rfT uT_r_aw); (* k *)
+        FunD ( (* f *)
+          [
+            (moded @@ rfT @@ uT_undef);
+            (moded @@ rfT @@ uT_undef);
+          ],
+          (rdS @@ drf @@ v0) #.
+          (wrS @@ drf @@ v0) #.
+          (rdS @@ drf @@ v1)
+        );
+        FunD ( (* w *)
+          [
+            (moded @@ cpT @@ uT_undef);
+          ],
+          (wrS @@ drf @@ v0) |. skp
+        );
+        FunD ( (* g *)
+          [
+            (moded @@ rfT @@ uT_undef);
+            (moded @@ cpT @@ uT_undef);
+          ],
+          (wrS @@ drf @@ v0) #.
+          ((wrS @@ drf @@ v1) |. (wrS @@ drf @@ v0)) #.
+          (rdS @@ drf @@ v0) #.
+          (rdS @@ drf @@ v1)
+        );
+        FunD ( (* r *)
+          [
+            (moded @@ rfT @@ uT_undef);
+          ],
+          (rdS @@ drf @@ v0)
+        )
+      ],
+      let xV = vg0 in
+      let yV = vg1 in
+      let zV = vg2 in
+      let kV = vg3 in
+      let fF = vg4 in
+      let wF = vg5 in
+      let gF = vg6 in
+      let rF = vg7 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])
+    ) in
+    prog_eval_noret prog';
+    print_endline @@ show(prog) prog';
+    [%expect {| ([VarD (RefT (Rf, UnitT (Rd, AlwaysWr))); VarD (RefT (Rf, UnitT (Rd, AlwaysWr))); VarD (RefT (Rf, UnitT (Rd, AlwaysWr))); VarD (RefT (Rf, UnitT (Rd, AlwaysWr))); FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr))); (Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))], SeqS (SeqS (ReadS (DerefP (VarP (0))), WriteS (DerefP (VarP (0)))), ReadS (DerefP (VarP (1))))); FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, MayWr)))], ChoiceS (WriteS (DerefP (VarP (0))), SkipS)); FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr))); (Mode (In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], SeqS (SeqS (SeqS (WriteS (DerefP (VarP (0))), ChoiceS (WriteS (DerefP (VarP (1))), WriteS (DerefP (VarP (0))))), ReadS (DerefP (VarP (0)))), ReadS (DerefP (VarP (1))))); FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)))], ReadS (DerefP (VarP (0))))], SeqS (SeqS (SeqS (SeqS (SeqS (SeqS (SeqS (SeqS (CallS (VarP (1005), [PathE (VarP (1000))]), CallS (VarP (1007), [PathE (VarP (1000))])), CallS (VarP (1004), [PathE (VarP (1000)); PathE (VarP (1001))])), CallS (VarP (1007), [PathE (VarP (1001))])), CallS (VarP (1006), [PathE (VarP (1002)); PathE (VarP (1003))])), WriteS (DerefP (VarP (1002)))), CallS (VarP (1005), [PathE (VarP (1002))])), CallS (VarP (1004), [PathE (VarP (1001)); PathE (VarP (1002))])), CallS (VarP (1007), [PathE (VarP (1003))]))) |}]
+
+  (* TODO *)
+
   (* - basic var tests *)
 
   let%expect_test "empty" =
@@ -840,23 +967,23 @@ struct
     Printf.printf "done!";
     [%expect {| done! |}]
 
-  (* NOTE: memoization used *)
+  (* NOTE: does not work for annalyzer rw to the sequenced declaration addition to calculate tags  *)
-  let%expect_test "call inside call, recursive, dsl" =
+  (* let%expect_test "call inside call, recursive, dsl" = *)
-    prog_eval_noret (
+    (* prog_eval_noret ( *)
-      [
+      (* [ *)
-        defg uT_r_aw;
+        (* defg uT_r_aw; *)
-        defg (rfT uT_r_aw);
+        (* defg (rfT uT_r_aw); *)
-        FunD (
+        (* FunD ( *)
-          [moded @@ cpT @@ uT_aw],
+          (* [moded @@ cpT @@ uT_aw], *)
-          (callS vg2 [pE v0]) #.
+          (* (callS vg2 [pE v0]) #. *)
-          (wrS @@ drf @@ v0)
+          (* (wrS @@ drf @@ v0) *)
-        )
+        (* ) *)
-      ],
+      (* ], *)
-      (callS vg2 [pE vg1]) #.
+      (* (callS vg2 [pE vg1]) #. *)
-      (rdS @@ drf @@ vg1)
+      (* (rdS @@ drf @@ vg1) *)
-    );
+    (* ); *)
-    Printf.printf "done!";
+    (* Printf.printf "done!"; *)
-    [%expect {| done! |}]
+    (* [%expect {| done! |}] *)
 
   let%expect_test "call to fix after call, dsl" =
     prog_eval_noret (
@@ -868,7 +995,7 @@ struct
           wrS @@ drf @@ v0
         );
         FunD (
-          [((In, Out), rfT @@ uT_aw)],
+          [(Mode (In, Out), rfT @@ uT_aw)],
           wrS @@ drf @@ v0
         )
       ],
@@ -930,10 +1057,10 @@ struct
         defg (rfT uT_r_aw);
         FunD (
           [
-            ((NIn, NOut), cpT @@ uT);
+            (Mode (NIn, NOut), cpT @@ uT);
-            ((In, NOut), cpT @@ uT_r_aw);
+            (Mode (In, NOut), cpT @@ uT_r_aw);
-            ((NIn, Out), rfT @@ uT_aw);
+            (Mode (NIn, Out), rfT @@ uT_aw);
-            ((In, Out), rfT @@ uT_r_aw);
+            (Mode (In, Out), rfT @@ uT_r_aw);
           ],
           (rdS @@ drf @@ v1) #.
           (rdS @@ drf @@ v3) #.
@@ -964,10 +1091,10 @@ struct
         defg (rfT uT_r_aw);
         FunD (
           [
-            ((NIn, NOut), rfT @@ uT);
+            (Mode (NIn, NOut), rfT @@ uT);
-            ((In, NOut), rfT @@ uT_r);
+            (Mode (In, NOut), rfT @@ uT_r);
-            ((NIn, Out), rfT @@ uT_aw);
+            (Mode (NIn, Out), rfT @@ uT_aw);
-            ((In, Out), rfT @@ uT_r_aw);
+            (Mode (In, Out), rfT @@ uT_r_aw);
           ],
           (rdS @@ drf @@ v1) #.
           (rdS @@ drf @@ v3) #.
@@ -1050,129 +1177,98 @@ struct
     Printf.printf "done!";
     [%expect {| done! |}]
 
-  (* TODO tags, access *)
+  let%expect_test "presentation test 2 (complex types), dsl, rw gen" =
-  (* let%expect_test "presentation test 2 (complex types), dsl" = *)
+    let prog' = prog_eval (
-    (* prog_eval_noret ( *)
+      let userT = TupleT [uT_undef; uT_undef; uT_undef] in
-      (* let userT = TupleT [uT_r_aw; uT_r_aw; uT_r_aw] in *)
+      let dataT =  TupleT [uT_undef; uT_undef] in
-      (* let dataT =  TupleT [uT_r_aw; uT_r_aw] in *)
+      let requestT = TupleT [cpT userT;
-      (* let requestT = TupleT [cpT userT; *)
+                             cpT dataT;
-                             (* cpT dataT; *)
+                             cpT uT_undef] in
-                             (* cpT dataT] in *)
+      let requestArgsT = TupleT [cpT userT;
-      (* let requestArgsT = TupleT [cpT userT; (* TODO: tags *) *)
+                                 rfT dataT;
-                                 (* cpT dataT; *)
+                                 rfT uT_undef] in
-                                 (* cpT dataT] in *)
+      [
-      (* let userE = TupleE [UnitE; UnitE; UnitE] in *)
+        defg requestT;
-      (* let dataE =  TupleE [UnitE; UnitE] in *)
+        FunD ( (* send *)
-      (* let requestE = TupleE [rfg0E; rfg1E; rfg2E] in *)
+          [
-      (* [ *)
+            (moded @@ requestArgsT)
-        (* defg userT userE; *)
+          ],
-        (* defg dataT dataE; *)
+          ((
-        (* defg uT_r_aw; (* time *) *)
+            (rdS @@ drf @@ access 1 @@ v0) #.
-        (* defg requestT requestE; *)
+            (wrS @@ drf @@ access 1 @@ v0) #.
-        (* FunD ( (* send *) *)
+            (rdS v0) #.
-          (* [ *)
+            (wrS @@ access 1 @@ drf @@ access 0 @@ v0)
-            (* (moded @@ requestArgsT) *)
+          ) |.
-          (* ], *)
+          skp) #.
-          (* ( *)
+          (wrS @@ drf @@ access 2 @@ v0) #.
-          (* ( (* TODO access *) *)
+          (rdS v0)
-            (* (rdS @@ drf @@ v0) #. *)
+        );
-            (* (wrS @@ drf @@ v0) #. *)
+      ],
-            (* (rdS @@ drf @@ v0) #. *)
+      (callS vg1 [pE vg0]) #.
-            (* (wrS @@ drf @@ v0) *)
+      (wrS @@ drf @@ access 2 @@ vg0) #.
-          (* ) |. *)
+      ((rdS @@ access 1 @@ drf @@ access 0 @@ vg0) |.
-          (* skp) #. *)
+       (rdS @@ access 2 @@ drf @@ access 0 @@ vg0)) #.
-          (* TODO access *)
+      (rdS @@ drf @@ access 2 @@ vg0)
-          (* (wrS @@ drf @@ v0) #. *)
+    ) in
-          (* (rdS @@ drf @@ v1) *)
+    prog_eval_noret prog';
-        (* ); *)
+    print_endline @@ show(prog) prog';
-      (* ], *)
+    [%expect {| ([VarD (TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr))])); FunD ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, MayWr); UnitT (Rd, NeverWr)])); RefT (Rf, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, MayWr)])); RefT (Rf, UnitT (Rd, AlwaysWr))]))], SeqS (SeqS (ChoiceS (SeqS (SeqS (SeqS (ReadS (DerefP (AccessP (VarP (0), 1))), WriteS (DerefP (AccessP (VarP (0), 1)))), ReadS (VarP (0))), WriteS (AccessP (DerefP (AccessP (VarP (0), 0)), 1))), SkipS), WriteS (DerefP (AccessP (VarP (0), 2)))), ReadS (VarP (0))))], SeqS (SeqS (SeqS (CallS (VarP (1001), [PathE (VarP (1000))]), WriteS (DerefP (AccessP (VarP (1000), 2)))), ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (1000), 0)), 1)), ReadS (AccessP (DerefP (AccessP (VarP (1000), 0)), 2)))), ReadS (DerefP (AccessP (VarP (1000), 2))))) |}]
-      (* (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 *)
+  let%expect_test "complex test: send, dsl" =
-  (* NOTE: path access isreversed to intuitive function application
+    let prog' = prog_eval (
-           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_utilsT = TupleT [uT_undef (* 0 id *); uT_undef] in
-      (* let user_infoT =  TupleT [uT_r_aw (* 0 name *); uT_r_aw; uT_r_aw] in *)
+      let user_infoT =  TupleT [uT_undef (* 0 name *); uT_undef; uT_undef] in
-      (* let userT = TupleT [cpT user_utilsT (* 0 utils *); cpT user_infoT (* 1 info *)] 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 versionT = TupleT [uT_undef (* 0 id *); uT_undef; uT_undef] in
-      (* let utilsT = TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 1 id *)] in *)
+      let utilsT = TupleT [uT_undef (* 0 has_version *); uT_undef (* 1 id *)] in
-      (* let requestT = TupleT [cpT userT (* 0 user *); *)
+      let requestT = TupleT [cpT userT (* 0 user *);
-                             (* cpT versionT (* 1 version *); *)
+                             cpT versionT (* 1 version *);
-                             (* cpT utilsT (* 2 utils *); *)
+                             cpT utilsT (* 2 utils *);
-                             (* cpT uT_r_aw (* 3 data *); *)
+                             cpT uT_undef (* 3 data *);
-                             (* uT_r_aw (* 4 operation_date *)] in *)
+                             uT_undef (* 4 operation_date *)] in
-      (* let user_utilsE = TupleE [UnitE (* 0 id *); UnitE] in *)
+      let get_version_idID = vg1 in
-      (* let user_infoE =  TupleE [UnitE (* 0 name *); UnitE; UnitE] in *)
+      let updated_versionID = vg2 in
-      (* let userE = TupleE [rfg0E (* 0 utils *); rfg1E (* 1 info *)] in *)
+      let sendID = vg3 in
-      (* let versionE = TupleE [UnitE (* 0 id *); UnitE; UnitE] in *)
+      let send_allID = vg4 in
-      (* let utilsE = TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] in *)
+      let get_version_idF = FunD ([moded requestT],
-      (* let requestE = TupleE [rfg2E (* 0 user *); *)
+        (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in
-                             (* rfg3E (* 1 version *); *)
+      let updated_versionF = FunD ([moded requestT],
-                             (* rfg4E (* 2 utils *); *)
+        (rdS @@ access 0 @@ drf @@ access 2 v0) #.
-                             (* 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 0 @@ drf @@ access 1 v0) #.
-        (* (rdS @@ access 1 @@ drf @@ access 1 v0)) in *)
+        (rdS @@ access 1 @@ drf @@ access 1 v0)) in
-      (* let sendF = FunD ([moded requestT], *)
+      let sendF = FunD ([moded requestT],
-        (* (( *)
+        ((
-           (* (wrS @@ access 0 @@ drf @@ access 2 v0) #. *)
+           (wrS @@ access 0 @@ drf @@ access 2 v0) #.
-           (* (rdS @@ drf @@ access 3 v0) #. *)
+           (rdS @@ drf @@ access 3 v0) #.
-           (* (wrS @@ drf @@ access 3 v0) #. *)
+           (wrS @@ drf @@ access 3 v0) #.
-           (* (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0) *)
+           (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0)
-         (* ) |. skp) #. *)
+         ) |. skp) #.
-         (* (wrS @@ access 4 v0) #. *)
+         (wrS @@ access 4 v0) #.
-         (* TODO: read all the substructure ?? *)
+         (rdS v0)) in
-         (* (rdS @@ access 4 v0) (*rdS v0*)) in (* FIXME: TMP, parial read, should be full *) *)
+      let send_allF = FunD ([moded requestT],
-      (* let send_allF = FunD ([moded requestT], *)
+        (wrS v0) #.
-        (* (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *) *)
+        (callS sendID [pE v0]) #.
-        (* (callS sendID [pE v0]) #. *)
+        (callS get_version_idID [pE v0]) #.
-        (* (callS get_version_idID [pE v0]) #. *)
+        (callS updated_versionID [pE v0]) #.
-        (* (callS updated_versionID [pE v0]) #. *)
+        (wrS @@ drf @@ access 1 v0) #. (* TODO: check, all required substruct ? *)
-        (* 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 0 @@ drf @@ access 0 v0) |.
-         (* (rdS @@ access 0 @@ drf @@ access 1 v0))) in *)
+         (rdS @@ access 0 @@ drf @@ access 1 v0))) in
-      (* let varID = vg6 in *)
+      let varID = vg0 in
-      (* [ *)
+      [
-        (* defg user_utilsT user_utilsE; *)
+        defg requestT;
-        (* defg user_infoT user_infoE; *)
+        get_version_idF;
-        (* defg userT userE; *)
+        updated_versionF;
-        (* defg versionT versionE; *)
+        sendF;
-        (* defg utilsT utilsE; *)
+        send_allF
-        (* defg uT_r_aw; *)
+      ],
-        (* defg requestT requestE; *)
+      callS send_allID [pE varID]
-        (* get_version_idF; *)
+    ) in
-        (* updated_versionF; *)
+    prog_eval_noret prog';
-        (* sendF; *)
+    print_endline @@ show(prog) prog';
-        (* send_allF *)
+    [%expect {| ([VarD (TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr)); UnitT (Rd, AlwaysWr)])); FunD ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (Cp, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (Cp, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (Cp, UnitT (NRd, NeverWr)); UnitT (NRd, NeverWr)]))], ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 0)), SkipS)); FunD ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (Cp, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr); UnitT (NRd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (NRd, NeverWr)])); RefT (Cp, UnitT (NRd, NeverWr)); UnitT (NRd, NeverWr)]))], SeqS (SeqS (ReadS (AccessP (DerefP (AccessP (VarP (0), 2)), 0)), ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 0))), ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 1)))); FunD ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr); UnitT (Rd, NeverWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr); UnitT (Rd, NeverWr)])); RefT (Cp, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, NeverWr)])); RefT (Cp, UnitT (Rd, MayWr)); UnitT (NRd, AlwaysWr)]))], SeqS (SeqS (ChoiceS (SeqS (SeqS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (0), 2)), 0)), ReadS (DerefP (AccessP (VarP (0), 3)))), WriteS (DerefP (AccessP (VarP (0), 3)))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (0), 0)), 1)), 0))), SkipS), WriteS (AccessP (VarP (0), 4))), ReadS (VarP (0)))); FunD ([(Mode (In, NOut), TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)])); RefT (Cp, UnitT (NRd, AlwaysWr)); UnitT (NRd, AlwaysWr)]))], SeqS (SeqS (SeqS (SeqS (SeqS (WriteS (VarP (0)), CallS (VarP (1003), [PathE (VarP (0))])), CallS (VarP (1001), [PathE (VarP (0))])), CallS (VarP (1002), [PathE (VarP (0))])), WriteS (DerefP (AccessP (VarP (0), 1)))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (0), 0)), 0)), 0)), ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 0)))))], CallS (VarP (1004), [PathE (VarP (1000))])) |}]
-      (* ], *)
-      (* callS send_allID [pE varID] *)
-    (* ); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* TODO: version with more optimal modifiers *)
 end

model_with_structures/tests.ml

@@ -107,3 +107,6 @@ let%expect_test "presentation test 2 (complex types), synt" = print_endline(prog
 (* let%expect_test "complex test: send" = print_endline(prog_synt_compl_test_send ()); *)
   (* [%expect {| [[Rf; Cp; Cp; Cp; Cp; Cp]; [Cp; Cp; Cp; Cp; Cp; Cp]] |}] (* TODO: FIXME *) *)
 (* TODO *)
+
+let%expect_test "complex test: send, gen rw" = print_endline(prog_synt_compl_test_send_gen_rw ());
+  [%expect {| [[Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Rf; Cp; Rf; Rf; Rf; Rf; Rf; Rf; Rf]] |}]

model_with_structures/tests_f.ml

@@ -1357,3 +1357,62 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
               ) &
               prog_evalo prog st })
   (fun q -> q#reify (List.prj_exn CopyCap.prj_exn))))
+
+(* complex test with already generated rw tags *)
+
+let prog_synt_compl_test_send_gen_rw _ = show(answerCpCapList) (Stream.take (run q
+  (fun q -> ocanren {
+              fresh prog, st,
+                    c00, c01, c02, c03, c04, c05,
+                    c10, c11, c12, c13, c14, c15,
+                    c20, c21, c22, c23, c24, c25,
+                    c30, c31, c32, c33, c34, c35
+              in
+
+              q == [
+                c00; c01; c02; c03; c04; c05;
+                c10; c11; c12; c13; c14; c15;
+                c20; c21; c22; c23; c24; c25;
+                c30; c31; c32; c33; c34; c35
+              ] &
+
+              c00 == Rf &
+              c01 == Rf &
+              c02 == Rf &
+              c03 == Rf &
+              c04 == Rf &
+              c05 == Rf &
+              c10 == Rf &
+              c11 == Rf &
+              c12 == Rf &
+              c13 == Rf &
+              c14 == Rf &
+              c15 == Rf &
+              c20 == Rf &
+              c21 == Rf &
+              c22 == Rf &
+              c23 == Rf &
+              c24 == Cp &
+              c25 == Rf &
+              c30 == Rf &
+              c31 == Rf &
+              c32 == Rf &
+              c33 == Rf &
+              c34 == Rf &
+              c35 == Rf &
+
+              prog == Prg ([
+                VarD (TupleT ([RefT (Cp, TupleT ([RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)]))])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, TupleT ([UnitT (Rd, AlwaysWr); UnitT (Rd, AlwaysWr)])); RefT (Cp, UnitT (Rd, AlwaysWr)); UnitT (Rd, AlwaysWr)]));
+                FunD ([(Mode (In, NOut), TupleT ([RefT (c00, TupleT ([RefT (c01, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (c02, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)]))])); RefT (c03, TupleT ([UnitT (Rd, NeverWr); UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (c04, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (c05, UnitT (NRd, NeverWr)); UnitT (NRd, NeverWr)]))],
+                      ChoiceS (ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 0)), SkipS));
+                FunD ([(Mode (In, NOut), TupleT ([RefT (c10, TupleT ([RefT (c11, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)])); RefT (c12, TupleT ([UnitT (NRd, NeverWr); UnitT (NRd, NeverWr); UnitT (NRd, NeverWr)]))])); RefT (c13, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr); UnitT (NRd, NeverWr)])); RefT (c14, TupleT ([UnitT (Rd, NeverWr); UnitT (NRd, NeverWr)])); RefT (c15, UnitT (NRd, NeverWr)); UnitT (NRd, NeverWr)]))],
+                      SeqS (SeqS (ReadS (AccessP (DerefP (AccessP (VarP (0), 2)), 0)), ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 0))), ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 1))));
+                FunD ([(Mode (In, NOut), TupleT ([RefT (c20, TupleT ([RefT (c21, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr)])); RefT (c22, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr); UnitT (Rd, NeverWr)]))])); RefT (c23, TupleT ([UnitT (Rd, NeverWr); UnitT (Rd, NeverWr); UnitT (Rd, NeverWr)])); RefT (c24, TupleT ([UnitT (Rd, MayWr); UnitT (Rd, NeverWr)])); RefT (c25, UnitT (Rd, MayWr)); UnitT (NRd, AlwaysWr)]))],
+                      SeqS (SeqS (ChoiceS (SeqS (SeqS (SeqS (WriteS (AccessP (DerefP (AccessP (VarP (0), 2)), 0)), ReadS (DerefP (AccessP (VarP (0), 3)))), WriteS (DerefP (AccessP (VarP (0), 3)))), ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (0), 0)), 1)), 0))), SkipS), WriteS (AccessP (VarP (0), 4))), ReadS (VarP (0))));
+                FunD ([(Mode (In, NOut), TupleT ([RefT (c30, TupleT ([RefT (c31, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)])); RefT (c32, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)]))])); RefT (c33, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)])); RefT (c34, TupleT ([UnitT (NRd, AlwaysWr); UnitT (NRd, AlwaysWr)])); RefT (c35, UnitT (NRd, AlwaysWr)); UnitT (NRd, AlwaysWr)]))],
+                      SeqS (SeqS (SeqS (SeqS (SeqS (WriteS (VarP (0)), CallS (VarP (13), [PathE (VarP (0))])), CallS (VarP (11), [PathE (VarP (0))])), CallS (VarP (12), [PathE (VarP (0))])), WriteS (DerefP (AccessP (VarP (0), 1)))), ChoiceS (ReadS (AccessP (DerefP (AccessP (DerefP (AccessP (VarP (0), 0)), 0)), 0)), ReadS (AccessP (DerefP (AccessP (VarP (0), 1)), 0)))))
+              ],
+              CallS (VarP (14), [PathE (VarP (10))])
+              ) &
+              prog_evalo prog st })
+  (fun q -> q#reify (List.prj_exn CopyCap.prj_exn))))