model_with_structures/analyzer.ml

@@ -14,7 +14,7 @@ struct
   type in_cap = In | NIn
   type out_cap = Out | NOut
 
-  type mode = Mode of in_cap * out_cap
+  type mode = in_cap * out_cap
 
   type path = VarP of data | DerefP of path | AccessP of path * data
 
@@ -103,12 +103,10 @@ 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
@@ -351,9 +349,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 =
-    (mode_out m != Out || c == Rf) &&
+    (snd m != Out || c == Rf) &&
-    (mode_out m != Out || w == AlwaysWr) &&
+    (snd m != Out || w == AlwaysWr) &&
-    (r != Rd || mode_in m == In)
+    (r != Rd || fst m == In)
 
   let tryread (r : read_cap) (v_m : memval)
               (v_r : readval) (v_w : writeval) : value =
@@ -365,10 +363,10 @@ struct
   
   let tryspoil (m : mode) (w : write_cap) (v_m : memval) : memval =
     match m, w with
-      | Mode (_, Out), AlwaysWr -> v_m
+      | (_, Out), AlwaysWr -> v_m
-      | Mode (_, Out), MayWr -> v_m
+      | (_, Out), MayWr -> v_m
-      | Mode (_, NOut), AlwaysWr -> BotMV
+      | (_, NOut), AlwaysWr -> BotMV
-      | Mode (_, NOut), MayWr -> SmthMV
+      | (_, NOut), MayWr -> SmthMV
       | _ -> raise @@ Typing_error "tryspoil: unexpected pair mode + write cap"
 
   let rec valspoil (mem : mem) (v : value) (t : atype)
@@ -609,7 +607,7 @@ struct
   let rfT t = RefT (Rf, t)
   let cpT t = RefT (Cp, t)
 
-  let moded t = (Mode (In, NOut), t)
+  let moded t = ((In, NOut), t)
 
   let defg t = VarD t
 
@@ -870,7 +868,7 @@ struct
           wrS @@ drf @@ v0
         );
         FunD (
-          [(Mode (In, Out), rfT @@ uT_aw)],
+          [((In, Out), rfT @@ uT_aw)],
           wrS @@ drf @@ v0
         )
       ],
@@ -932,10 +930,10 @@ struct
         defg (rfT uT_r_aw);
         FunD (
           [
-            (Mode (NIn, NOut), cpT @@ uT);
+            ((NIn, NOut), cpT @@ uT);
-            (Mode (In, NOut), cpT @@ uT_r_aw);
+            ((In, NOut), cpT @@ uT_r_aw);
-            (Mode (NIn, Out), rfT @@ uT_aw);
+            ((NIn, Out), rfT @@ uT_aw);
-            (Mode (In, Out), rfT @@ uT_r_aw);
+            ((In, Out), rfT @@ uT_r_aw);
           ],
           (rdS @@ drf @@ v1) #.
           (rdS @@ drf @@ v3) #.
@@ -966,10 +964,10 @@ struct
         defg (rfT uT_r_aw);
         FunD (
           [
-            (Mode (NIn, NOut), rfT @@ uT);
+            ((NIn, NOut), rfT @@ uT);
-            (Mode (In, NOut), rfT @@ uT_r);
+            ((In, NOut), rfT @@ uT_r);
-            (Mode (NIn, Out), rfT @@ uT_aw);
+            ((NIn, Out), rfT @@ uT_aw);
-            (Mode (In, Out), rfT @@ uT_r_aw);
+            ((In, Out), rfT @@ uT_r_aw);
           ],
           (rdS @@ drf @@ v1) #.
           (rdS @@ drf @@ v3) #.
@@ -1051,4 +1049,130 @@ 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,48 +1,35 @@
-module FunctionalRW =
+module Functional =
 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 ? *)
-  [@@deriving gt ~options:{ show }]
+  type copy_cap = Cp | Rf
-  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 = Mode of in_cap * out_cap
+  type mode = 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
@@ -50,14 +37,11 @@ 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 --- *)
 
@@ -72,7 +56,6 @@ 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 *)
 
@@ -84,36 +67,26 @@ 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 }]
 
   (* --- *)
 
@@ -130,12 +103,10 @@ 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
@@ -221,8 +192,6 @@ 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
@@ -232,6 +201,22 @@ 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 =
@@ -353,14 +338,20 @@ 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 =
-    (mode_out m != Out || c == Rf) &&
+    (snd m != Out || c == Rf) &&
-    (mode_out m != Out || w == AlwaysWr || w == UndefWr) &&
+    (snd m != Out || w == AlwaysWr) &&
-    (r != Rd || mode_in m == In)
+    (r != Rd || fst m == In)
 
   let tryread (r : read_cap) (v_m : memval)
               (v_r : readval) (v_w : writeval) : value =
@@ -369,15 +360,13 @@ struct
                      readvmod ReadA v_r,
                      writevmod ReadA 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
-      | Mode (_, Out), AlwaysWr -> v_m
+      | (_, Out), AlwaysWr -> v_m
-      | Mode (_, Out), MayWr -> v_m
+      | (_, Out), MayWr -> v_m
-      | Mode (_, NOut), AlwaysWr -> BotMV
+      | (_, NOut), AlwaysWr -> BotMV
-      | Mode (_, NOut), MayWr -> SmthMV
+      | (_, 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)
@@ -397,8 +386,6 @@ struct
                 then (memvmod AlwaysWriteA v_m',
                       readvmod AlwaysWriteA v_r',
                       writevmod AlwaysWriteA v_w')
-              else if w == UndefWr
-                then raise @@ Cant_deduce_rw_error "valspoil"
                 else (* MayWr *)
                      (memvmod MayWriteA v_m',
                       readvmod MayWriteA v_r',
@@ -453,42 +440,32 @@ 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
 
-  (* NOTE: in analyzer rw tags check replaces tags with calculated ones *)
+  let rec tags_check (mem : mem) (v : value) (t : atype) : unit =
-  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) ->
-        let r' = readval_to_cap v_r in
+        if (r == Rd) && (v_r != OneRV)
-        let w' = writeval_to_cap v_w in
+          then raise @@ Eval_error "tags_check: wrong read tag"
-        if r != UndefRd && r != r'
+        else if (r == NRd) && (v_r == OneRV)
-          then raise @@ Eval_error "tags_check: not undef read tag & not correct"
+          then raise @@ Eval_error "tags_check: wrong not read tag"
-        else if w != UndefWr && w != w'
+        else if writeval_to_cap v_w != w
-          then raise @@ Eval_error "tags_check: not undef write tag & not correct"
+          then raise @@ Eval_error "tags_check: wrong write tag"
-        else UnitT (r', w')
+        else ()
-      | FunV, FunT _ -> t
+      | FunV, FunT _ -> ()
-      | RefV id, RefT (c, t) -> RefT (c, tags_check mem (mem_get mem id) t)
+      | RefV id, RefT (_, t) -> tags_check mem (mem_get mem id) t
-      | TupleV vs, TupleT ts -> TupleT (List.map2 (tags_check mem) vs ts)
+      | TupleV vs, TupleT ts -> ignore @@ 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 (_, MayWr) -> true
+      | UnitT (_, w) -> w == MayWr || w == AlwaysWr
-      | 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
@@ -537,51 +514,28 @@ struct
 
   (* - function evaluation *)
 
-  let rec replace_rw_undef_with_r_aw (t : atype) : atype = match t with
+  let rec func_eval (state : state) (d : decl) : unit =
-    | 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) ->
-       let (_, ts') = List.fold_left
+       ignore @@ List.fold_left
-         (fun (x, ts_acc) (m, t) ->
+         (fun x (_, t) ->
             let id = vals_assoc x vals_after_stmt in
             let v = mem_get mem_after_stmt id in
-            let t' = tags_check mem_after_stmt v t in
+            tags_check mem_after_stmt v t; x + 1)
-            (x + 1, (m, t') :: ts_acc))
+         0 ts)
-         (0, []) ts in
+    | VarD _ -> ()
-       (* 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 --- *)
 
-  (* NOTE: decls returned in the reversed order (?) *)
+  let prog_eval (prog : prog) : state =
-  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, decls') = prog_init prog in
+    let init_state = prog_init prog in
-    ignore @@ stmt_eval init_state s;
+    ignore @@ List.map (func_eval init_state) decls;
-    (decls', s)
+    stmt_eval init_state s
 
   let prog_eval_noret (prog : prog) : unit =
     ignore @@ prog_eval prog
@@ -649,12 +603,11 @@ 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 = (Mode (In, NOut), t)
+  let moded t = ((In, NOut), t)
 
   let defg t = VarD t
 
@@ -688,86 +641,6 @@ 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" =
@@ -967,23 +840,23 @@ struct
     Printf.printf "done!";
     [%expect {| done! |}]
 
-  (* NOTE: does not work for annalyzer rw to the sequenced declaration addition to calculate tags  *)
+  (* NOTE: memoization used *)
-  (* 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 (
@@ -995,7 +868,7 @@ struct
           wrS @@ drf @@ v0
         );
         FunD (
-          [(Mode (In, Out), rfT @@ uT_aw)],
+          [((In, Out), rfT @@ uT_aw)],
           wrS @@ drf @@ v0
         )
       ],
@@ -1057,10 +930,10 @@ struct
         defg (rfT uT_r_aw);
         FunD (
           [
-            (Mode (NIn, NOut), cpT @@ uT);
+            ((NIn, NOut), cpT @@ uT);
-            (Mode (In, NOut), cpT @@ uT_r_aw);
+            ((In, NOut), cpT @@ uT_r_aw);
-            (Mode (NIn, Out), rfT @@ uT_aw);
+            ((NIn, Out), rfT @@ uT_aw);
-            (Mode (In, Out), rfT @@ uT_r_aw);
+            ((In, Out), rfT @@ uT_r_aw);
           ],
           (rdS @@ drf @@ v1) #.
           (rdS @@ drf @@ v3) #.
@@ -1091,10 +964,10 @@ struct
         defg (rfT uT_r_aw);
         FunD (
           [
-            (Mode (NIn, NOut), rfT @@ uT);
+            ((NIn, NOut), rfT @@ uT);
-            (Mode (In, NOut), rfT @@ uT_r);
+            ((In, NOut), rfT @@ uT_r);
-            (Mode (NIn, Out), rfT @@ uT_aw);
+            ((NIn, Out), rfT @@ uT_aw);
-            (Mode (In, Out), rfT @@ uT_r_aw);
+            ((In, Out), rfT @@ uT_r_aw);
           ],
           (rdS @@ drf @@ v1) #.
           (rdS @@ drf @@ v3) #.
@@ -1177,98 +1050,129 @@ struct
     Printf.printf "done!";
     [%expect {| done! |}]
 
-  let%expect_test "presentation test 2 (complex types), dsl, rw gen" =
+  (* TODO tags, access *)
-    let prog' = prog_eval (
+  (* let%expect_test "presentation test 2 (complex types), dsl" = *)
-      let userT = TupleT [uT_undef; uT_undef; uT_undef] in
+    (* prog_eval_noret ( *)
-      let dataT =  TupleT [uT_undef; uT_undef] in
+      (* let userT = TupleT [uT_r_aw; uT_r_aw; uT_r_aw] in *)
-      let requestT = TupleT [cpT userT;
+      (* let dataT =  TupleT [uT_r_aw; uT_r_aw] in *)
-                             cpT dataT;
+      (* let requestT = TupleT [cpT userT; *)
-                             cpT uT_undef] in
+                             (* cpT dataT; *)
-      let requestArgsT = TupleT [cpT userT;
+                             (* cpT dataT] in *)
-                                 rfT dataT;
+      (* let requestArgsT = TupleT [cpT userT; (* TODO: tags *) *)
-                                 rfT uT_undef] in
+                                 (* cpT dataT; *)
-      [
+                                 (* cpT dataT] in *)
-        defg requestT;
+      (* let userE = TupleE [UnitE; UnitE; UnitE] in *)
-        FunD ( (* send *)
+      (* let dataE =  TupleE [UnitE; UnitE] in *)
-          [
+      (* let requestE = TupleE [rfg0E; rfg1E; rfg2E] in *)
-            (moded @@ requestArgsT)
+      (* [ *)
-          ],
+        (* defg userT userE; *)
-          ((
+        (* defg dataT dataE; *)
-            (rdS @@ drf @@ access 1 @@ v0) #.
+        (* defg uT_r_aw; (* time *) *)
-            (wrS @@ drf @@ access 1 @@ v0) #.
+        (* defg requestT requestE; *)
-            (rdS v0) #.
+        (* FunD ( (* send *) *)
-            (wrS @@ access 1 @@ drf @@ access 0 @@ v0)
+          (* [ *)
-          ) |.
+            (* (moded @@ requestArgsT) *)
-          skp) #.
+          (* ], *)
-          (wrS @@ drf @@ access 2 @@ v0) #.
+          (* ( *)
-          (rdS v0)
+          (* ( (* TODO access *) *)
-        );
+            (* (rdS @@ drf @@ v0) #. *)
-      ],
+            (* (wrS @@ drf @@ v0) #. *)
-      (callS vg1 [pE vg0]) #.
+            (* (rdS @@ drf @@ v0) #. *)
-      (wrS @@ drf @@ access 2 @@ vg0) #.
+            (* (wrS @@ drf @@ v0) *)
-      ((rdS @@ access 1 @@ drf @@ access 0 @@ vg0) |.
+          (* ) |. *)
-       (rdS @@ access 2 @@ drf @@ access 0 @@ vg0)) #.
+          (* skp) #. *)
-      (rdS @@ drf @@ access 2 @@ vg0)
+          (* TODO access *)
-    ) in
+          (* (wrS @@ drf @@ v0) #. *)
-    prog_eval_noret prog';
+          (* (rdS @@ drf @@ v1) *)
-    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 *)
 
-  let%expect_test "complex test: send, dsl" =
+  (* TODO: FIXME: rw tags *)
-    let prog' = prog_eval (
+  (* 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_undef (* 0 id *); uT_undef] in
+      (* let user_utilsT = TupleT [uT_r_aw (* 0 id *); uT_r_aw] in *)
-      let user_infoT =  TupleT [uT_undef (* 0 name *); uT_undef; uT_undef] 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 userT = TupleT [cpT user_utilsT (* 0 utils *); cpT user_infoT (* 1 info *)] in *)
-      let versionT = TupleT [uT_undef (* 0 id *); uT_undef; uT_undef] in
+      (* let versionT = TupleT [uT_r_aw (* 0 id *); uT_r_aw; uT_r_aw] in *)
-      let utilsT = TupleT [uT_undef (* 0 has_version *); uT_undef (* 1 id *)] in
+      (* let utilsT = TupleT [uT_r_aw (* 0 has_version *); uT_r_aw (* 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_undef (* 3 data *);
+                             (* cpT uT_r_aw (* 3 data *); *)
-                             uT_undef (* 4 operation_date *)] in
+                             (* uT_r_aw (* 4 operation_date *)] in *)
-      let get_version_idID = vg1 in
+      (* let user_utilsE = TupleE [UnitE (* 0 id *); UnitE] in *)
-      let updated_versionID = vg2 in
+      (* let user_infoE =  TupleE [UnitE (* 0 name *); UnitE; UnitE] in *)
-      let sendID = vg3 in
+      (* let userE = TupleE [rfg0E (* 0 utils *); rfg1E (* 1 info *)] in *)
-      let send_allID = vg4 in
+      (* let versionE = TupleE [UnitE (* 0 id *); UnitE; UnitE] in *)
-      let get_version_idF = FunD ([moded requestT],
+      (* let utilsE = TupleE [UnitE (* 0 has_version *); UnitE (* 1 id *)] in *)
-        (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in
+      (* let requestE = TupleE [rfg2E (* 0 user *); *)
-      let updated_versionF = FunD ([moded requestT],
+                             (* rfg3E (* 1 version *); *)
-        (rdS @@ access 0 @@ drf @@ access 2 v0) #.
+                             (* 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 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) #. *)
-         (rdS v0)) in
+         (* TODO: read all the substructure ?? *)
-      let send_allF = FunD ([moded requestT],
+         (* (rdS @@ access 4 v0) (*rdS v0*)) in (* FIXME: TMP, parial read, should be full *) *)
-        (wrS v0) #.
+      (* let send_allF = FunD ([moded requestT], *)
-        (callS sendID [pE v0]) #.
+        (* (wrS @@ access 4 v0) (*wrS v0*) #. (* FIXME: TMP, parial write, should be full *) *)
-        (callS get_version_idID [pE v0]) #.
+        (* (callS sendID [pE v0]) #. *)
-        (callS updated_versionID [pE v0]) #.
+        (* (callS get_version_idID [pE v0]) #. *)
-        (wrS @@ drf @@ access 1 v0) #. (* TODO: check, all required substruct ? *)
+        (* (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 0 @@ drf @@ access 0 v0) |. *)
-         (rdS @@ access 0 @@ drf @@ access 1 v0))) in
+         (* (rdS @@ access 0 @@ drf @@ access 1 v0))) in *)
-      let varID = vg0 in
+      (* let varID = vg6 in *)
-      [
+      (* [ *)
-        defg requestT;
+        (* defg user_utilsT user_utilsE; *)
-        get_version_idF;
+        (* defg user_infoT user_infoE; *)
-        updated_versionF;
+        (* defg userT userE; *)
-        sendF;
+        (* defg versionT versionE; *)
-        send_allF
+        (* defg utilsT utilsE; *)
-      ],
+        (* defg uT_r_aw; *)
-      callS send_allID [pE varID]
+        (* defg requestT requestE; *)
-    ) in
+        (* get_version_idF; *)
-    prog_eval_noret prog';
+        (* updated_versionF; *)
-    print_endline @@ show(prog) prog';
+        (* sendF; *)
-    [%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))])) |}]
+        (* send_allF *)
+      (* ], *)
+      (* callS send_allID [pE varID] *)
+    (* ); *)
+    (* Printf.printf "done!"; *)
+    (* [%expect {| done! |}] *)
+
+  (* TODO: version with more optimal modifiers *)
 end

model_with_structures/tests.ml

@@ -107,6 +107,3 @@ 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,62 +1357,3 @@ 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))))