struct: synthesiszer fix, tests fix

model_with_structures/analyzer.ml

@@ -38,7 +38,7 @@ struct
             | SeqS of stmt * stmt
             | ChoiceS of stmt * stmt
 
-  type decl = VarD of (* data * *) atype * expr
+  type decl = VarD of (* data * *) atype (* * expr *)
             | FunD of (* data * *) (* (data * *) mtype (* )  *) list * stmt
 
   type prog = decl list * stmt
@@ -71,7 +71,7 @@ struct
   type writeval = ZeroWV | SmthWV | OneWV
 
   type value = UnitV of memval * readval * writeval
-             | FunV of ((* data list * *) stmt) list
+             | FunV (* of ((* data list * *) stmt) list *)
              | RefV of memid
              | TupleV of value list
 
@@ -84,10 +84,9 @@ struct
   (* --- *)
 
   type mem = value list * memid (* NOTE: memory and first free elem *)
-  type types = (data * atype) list (* glob *) * (data * atype) list (* glob + loc *)
+  type types = (data * atype) list
-  type vals = (data * memid) list (* glob *) * (data * memid) list (* glob + loc *)
+  type vals = (data * memid) list
-  type visited = stmt list (* TODO: FIXME: optimize, use ids *)
+  type state = mem * types * vals
-  type state = mem * types * vals * visited
 
   (* --- *)
 
@@ -96,23 +95,17 @@ struct
   let types_assoc (x : data) (types : types) : atype =
     (* try ( List.assoc x (fst types) ) *)
     (* with Not_found -> *)
-    List.assoc x (snd types)
+    List.assoc x types
   let vals_assoc (x : data) (vals : vals) : memid =
     (* try ( List.assoc x (fst vals) ) *)
     (* with Not_found -> *)
-    List.assoc x (snd vals)
+    List.assoc x vals
-
-  let types_glob_add (types : types) (x : data) (t : atype) =
-    ((x, t) :: fst types, (x, t) :: snd types)
 
   let types_add (types : types) (x : data) (t : atype) =
-    (fst types, (x, t) :: snd types)
+    (x, t) :: types
-
-  let vals_glob_add (vals : vals) (x : data) (id : memid) =
-    ((x, id) :: fst vals, (x, id) :: snd vals)
 
   let vals_add (vals : vals) (x : data) (id : memid) =
-    (fst vals, (x, id) :: snd vals)
+    (x, id) :: vals
 
   (* - utils *)
 
@@ -195,20 +188,34 @@ struct
 
   (* - value construction *)
 
-  let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value =
+  let rec valbuild (mem : mem) (t : atype) : mem * value =
-    match t, v with
+    match t with
-    | UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV))
+    | UnitT (Rd, _) -> (mem, UnitV (ZeroMV, ZeroRV, ZeroWV))
-    | UnitT (NRd, _), UnitV _ -> (mem, UnitV (BotMV, ZeroRV, ZeroWV))
+    | UnitT (NRd, _) -> (mem, UnitV (BotMV, ZeroRV, ZeroWV))
-    | FunT _, FunV _ -> (mem, v)
+    | 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
+                     (mem'', RefV id'') 
+    | TupleT ts -> let folder = fun t (mem, vs') -> let (mem', v') = valbuild mem t in
+                                                        (mem', v' :: vs') in 
+                   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
+    (* | RefT (_, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in *)
-                               let (mem'', id'') = mem_add mem' v' in
+                               (* let (mem'', id'') = mem_add mem' v' in *)
-                               (mem'', RefV id'') 
+                               (* (mem'', RefV id'') *) 
-    | TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in
+    (* | TupleT ts, TupleV vs -> let folder = fun v t (mem, vs') -> let (mem', v') = valcopy mem v t in *)
-                                                                 (mem', v' :: vs') in 
+                                                                 (* (mem', v' :: vs') in *) 
-                              let mem', vs' = List.fold_left2 folder (mem, []) vs ts in
+                              (* let mem', vs' = List.fold_right2 folder vs ts (mem, []) in *)
-                              (mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *)
+                              (* (mem', TupleV vs') *)
-    | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type"
+    (* | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type" *)
 
   (* - action rules *)
 
@@ -286,7 +293,7 @@ struct
     match u, v with
       | UnitV (u_m, u_r, u_w), UnitV (v_m, v_r, v_w) ->
         UnitV (memvalcomb u_m v_m, readvalcomb u_r v_r, writevalcomb u_w v_w)
-      | FunV ustmts, FunV vstmts -> FunV (ustmts @ vstmts)
+      | FunV, FunV -> FunV
       | RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref"
       | TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs)
       | _, _ -> raise @@ Typing_error "valcomb"
@@ -318,16 +325,15 @@ struct
   
   (* TODO: check new in vars *)
   let add_decl (state : state) (x : data) (d : decl) : state =
-    match state with (mem, types, vals, visited) -> match d with
+    match state with (mem, types, vals) -> match d with
-    | VarD (t, e) -> let v = exprval mem vals e in
+    | VarD t -> let (mem', v) = valbuild mem t in
-                     let (mem', v') = valcopy mem v t in
+                let (mem'', id) = mem_add mem' v in
-                     let (mem'', id) = mem_add mem' v' in
+                (mem'', types_add types x t, vals_add vals x id)
-                     (mem'', types_glob_add types x t, vals_glob_add vals x id, visited)
+    | FunD (ts, s)  -> let (mem', id) = mem_add mem FunV in
-    | FunD (ts, s)  -> let (mem', id) = mem_add mem (FunV [s]) in
+                       (mem', types_add types x (FunT ts), vals_add vals x id)
-                       (mem', types_glob_add types x (FunT ts), vals_glob_add vals x id, visited)
 
   let empty_mem : mem = ([], 0)
-  let empty_state : state = (empty_mem, ([], []), ([], []), [])
+  let empty_state : state = (empty_mem, [], [])
 
   (* TODO: better way ??? *)
   let globals_min_id : data = 1000
@@ -388,7 +394,7 @@ struct
             let v_m''' = tryspoil m w v_m'' in
             (mem, UnitV (v_m''', v_r'', v_w''))
           | _ -> raise @@ Typing_error "valspoil: value after tryread is not unit")
-    | FunT ts, FunV _ -> (mem, v)
+    | FunT ts, FunV -> (mem, v)
     | RefT (ct, t), RefV id ->
       let (mem', v') = valspoil mem (mem_get mem id) t m ct in
       (mem_set mem id v', RefV id)
@@ -402,7 +408,7 @@ struct
   (* full spoil *)
 
   let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
-    match state with (mem, types, vals, visited) ->
+    match state with (mem, types, vals) ->
     let x = pathvar p in
     let id = vals_assoc x vals in (* base var address *)
     let b = pathval mem vals p in (* subvalue in var *)
@@ -414,29 +420,25 @@ struct
     mem_set mem'' id v''
 
   let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
-    match state with (mem, types, vals, visited) -> match e, t with
+    match state with (mem, types, vals) -> match e, t with
       | UnitE, UnitT _ -> mem
       | PathE p, t -> argsspoilp state m t p
       | RefE x, t -> argsspoilp state m t (VarP x)
       (* TODO: FIXME: check RefE case ? *)
       | TupleE es, TupleT ts -> List.fold_left2
-                                  (fun mem' t' e' -> argsspoile (mem', types, vals, visited) m t' e')
+                                  (fun mem' t' e' -> argsspoile (mem', types, vals) m t' e')
                                   mem ts es
       | _, _ ->  raise @@ Typing_error "valspoile"
 
   (* - funciton argument addition *)
 
-  let addarg (state : state) (oldvals : vals) (x : data) (t : atype) (e : expr) : state =
+  let addarg (state : state) (x : data) (t : atype) : state =
-    match state with (mem, types, vals, visited) ->
+    match state with (mem, types, vals) ->
-    let v = exprval mem oldvals e in
+    let (mem', v) = valbuild mem t in
-    (* let t' = pathtype types p in *)
+    let (mem'', id) = mem_add mem' v in
-    let (mem', v') = valcopy mem v t in
+    (mem'', types_add types x t, vals_add vals x id)
-    let (mem'', id) = mem_add mem' v' in
-    (mem'', types_add types x t, vals_add vals x id, visited)
 
-  (* - function evaluation *)
+  (* --- *)
-  (* NOTE: not needed due to performed optimization in stmt_eval *)
-  (* let func_eval (mem : mem) (vals : vals) (s : stmt) (ts : mtype list) (es : expr list) = *)
 
   let writeval_to_cap (v_w : writeval) : write_cap =
     match v_w with
@@ -454,7 +456,7 @@ struct
         else if writeval_to_cap v_w != w
           then raise @@ Eval_error "tags_check: wrong write tag"
         else ()
-      | FunV _, FunT _ -> ()
+      | FunV, FunT _ -> ()
       | RefV id, RefT (_, t) -> tags_check mem (mem_get mem id) t
       | TupleV vs, TupleT ts -> ignore @@ List.map2 (tags_check mem) vs ts
       | _, _ -> raise @@ Typing_error "tags_check"
@@ -471,42 +473,17 @@ struct
   (* - statement evaluation *)
 
   let rec stmt_eval (state : state) (s : stmt) : state =
-    match state with (mem, types, vals, visited) -> match s with
+    match state with (mem, types, vals) -> match s with
     | SkipS -> state
     | CallS (f, es) -> let v = pathval mem vals f in
                        let t = pathtype types f in
-                       let types' : types = (fst types, fst types) in
-                       let vals' : vals = (fst vals, fst vals) in
                        (match v, t with
-                          | FunV (* xs, *) fstmts (* ) *), FunT ts ->
+                          | FunV, FunT ts ->
-                            let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *)
+                             let mem_spoiled = List.fold_left2
-                                                       List.fold_left2 (* TODO: FIXME: check x's order *)
+                               (fun mem (m, t) e -> argsspoile (mem, types, vals) m t e)
-                              (fun (st, x) (m, t) e -> (addarg st vals x t e, x + 1))
-                              ((mem, types', vals', visited), 0) ts es in
-                            (* NOTE: same x's, so can use same args for all the statements *)
-                            (match state_with_args with (mem_swa, types_swa, vals_swa, visited_swa) ->
-                             let visited_new = (* FIXME TMP Printf.printf "call, before eval\n"; *)
-                                               List.fold_left
-                                                 (fun visited_old stmt ->
-                                                    if List.mem stmt visited_old
-                                                    then stmt :: visited_old
-                                                    else match stmt_eval (mem_swa, types_swa, vals_swa, stmt :: visited_old) stmt with
-                                                      (mem_after_stmt, _, vals_after_stmt, visited_after_stmt) ->
-                                                        ignore @@ List.fold_left
-                                                          (fun x (_, t) ->
-                                                             let id = vals_assoc x vals_after_stmt in
-                                                             let v = mem_get mem_after_stmt id in
-                                                             tags_check mem_after_stmt v t; x + 1)
-                                                          0 ts;
-                                                        visited_after_stmt)
-                                                 visited_swa
-                                                 fstmts in
-                             let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *)
-                                               List.fold_left2
-                               (fun mem (m, t) e -> argsspoile (mem, types, vals, (* NOTE: not important *) visited_new) m t e)
                                mem ts es in
-                             (mem_spoiled, types, vals, visited_new))
+                             (mem_spoiled, types, vals)
-                          | FunV _, _ -> raise @@ Eval_error "call: function type"
+                          | FunV, _ -> raise @@ Eval_error "call: function type"
                           | _, FunT _ -> raise @@ Eval_error "call: function val"
                           | _, _ -> raise @@ Eval_error "call: function type & val")
     | WriteS p -> if not @@ is_all_type_writable @@ pathtype types p
@@ -515,12 +492,12 @@ struct
                        let id = vals_assoc x vals in
                        let pi = pathrev p VarRP in
                        let (mem', v') = valupd mem (mem_get mem id) pi AlwaysWriteA in
-                       (mem_set mem' id v', types, vals, visited)
+                       (mem_set mem' id v', types, vals)
     | ReadS p -> let x = pathvar p in
                  let id = vals_assoc x vals in
                  let pi = pathrev p VarRP in
                  let (mem', v') = valupd mem (mem_get mem id) pi ReadA in
-                 (mem_set mem' id v', types, vals, visited)
+                 (mem_set mem' id v', types, vals)
                  (* NOTE: handled inside through undefined in memvmod *)
                  (* if pathval mem vals p == SmthV || pathval mem vals p == BotV *) 
                  (* then raise @@ Eval_error "read: spoiled value" *)
@@ -528,18 +505,36 @@ struct
                        stmt_eval statel sr
     | ChoiceS (sl, sr) -> let statel = stmt_eval state sl in
                           let stater = stmt_eval state sr in
-                          match statel with (meml, typesl, valsl, visitedl) ->
+                          match statel with (meml, typesl, valsl) ->
-                          match stater with (memr, typesr, valsr, visitedr) ->
+                          match stater with (memr, typesr, valsr) ->
                           if typesl != typesr || valsl != valsr
                           then raise @@ Eval_error "choice"
                           (* TODO: FIXME: better list union ??  *)
-                          else (memcomb meml memr, typesl, valsl, visitedl @ visitedr)
+                          else (memcomb meml memr, typesl, valsl)
+
+  (* - function evaluation *)
+
+  let rec func_eval (state : state) (d : decl) : unit =
+    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
+         (fun x (_, t) ->
+            let id = vals_assoc x vals_after_stmt in
+            let v = mem_get mem_after_stmt id in
+            tags_check mem_after_stmt v t; x + 1)
+         0 ts)
+    | VarD _ -> ()
 
   (* --- program execution --- *)
 
   let prog_eval (prog : prog) : state =
     match prog with (decls, s) ->
     let init_state = prog_init prog in
+    ignore @@ List.map (func_eval init_state) decls;
     stmt_eval init_state s
 
   let prog_eval_noret (prog : prog) : unit =
@@ -614,8 +609,7 @@ struct
 
   let moded t = ((In, NOut), t)
 
-  let defgu t = VarD (t, UnitE)
+  let defg t = VarD t
-  let defg t e = VarD (t, e)
 
   let wrS p = WriteS p 
   let rdS p = ReadS p 
@@ -655,40 +649,40 @@ struct
     [%expect {| done! |}]
 
   let%expect_test "simple var" =
-    prog_eval_noret ([VarD (UnitT (Rd, MayWr), UnitE)],
+    prog_eval_noret ([VarD (UnitT (Rd, MayWr))],
                       ReadS (VarP globals_min_id));
     Printf.printf "done!";
     [%expect {| done! |}]
 
   let%expect_test "simple var, forbidden read" =
-    try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)],
+    try(prog_eval_noret ([VarD (UnitT (NRd, MayWr))],
                          ReadS (VarP globals_min_id));
          [%expect.unreachable]);
     with Eval_error msg -> Printf.printf "%s" msg;
     [%expect {| memvmod: forbidden read |}]
 
   let%expect_test "simple vars, no read & read" =
-    prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE);
+    prog_eval_noret ([VarD (UnitT (NRd, MayWr));
-                      VarD (UnitT (Rd, MayWr), UnitE)],
+                      VarD (UnitT (Rd, MayWr))],
                      ReadS (VarP (globals_min_id + 1)));
     Printf.printf "done!";
     [%expect {| done! |}]
 
   let%expect_test "simple var, write" =
-    prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)],
+    prog_eval_noret ([VarD (UnitT (NRd, MayWr))],
                      WriteS (VarP globals_min_id));
     Printf.printf "done!";
     [%expect {| done! |}]
 
   let%expect_test "simple var, forbidden write" =
-    try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr), UnitE)],
+    try(prog_eval_noret ([VarD (UnitT (NRd, NeverWr))],
                          WriteS (VarP globals_min_id));
          [%expect.unreachable]);
     with Eval_error msg -> Printf.printf "%s" msg;
     [%expect {| write: write tag |}]
 
   let%expect_test "simple var, write & read" =
-    prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)],
+    prog_eval_noret ([VarD (UnitT (NRd, MayWr))],
                      SeqS (WriteS (VarP globals_min_id),
                            ReadS (VarP globals_min_id)));
     Printf.printf "done!";
@@ -697,7 +691,7 @@ struct
   (* - basic call tests *)
 
   (* let%expect_test "simple call with read" = *)
-    (* prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE); *)
+    (* prog_eval_noret ([VarD (UnitT (Rd, NeverWr)); *)
                       (* FunD ([((In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0)))], *)
                      (* CallS (VarP (globals_min_id + 1), *)
                             (* [PathE (VarP globals_min_id)])); *)
@@ -705,7 +699,7 @@ struct
     (* [%expect {| done! |}] *)
 
   (* let%expect_test "simple call with write" = *)
-    (* prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE); *)
+    (* prog_eval_noret ([VarD ((UnitT (Rd, MayWr))); *)
                       (* VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE globals_min_id); *)
                       (* FunD ([((In, NOut), RefT (Cp, UnitT (Rd, MayWr)))], WriteS (DerefP (VarP 0)))], *)
                      (* CallS (VarP (globals_min_id + 2), *)
@@ -716,8 +710,8 @@ struct
   let%expect_test "simple call with read, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_mw;
+        defg uT_r_mw;
-        defg (rfT uT_r_mw) rfg0E;
+        defg (rfT uT_r_mw);
         FunD (
           [moded @@ cpT @@ uT_r],
           rdS @@ drf @@ v0
@@ -731,8 +725,8 @@ struct
   let%expect_test "simple call with write, dsl" =
     prog_eval_noret (
       [
-        defgu uT_aw;
+        defg uT_aw;
-        defg (rfT uT_aw) rfg0E;
+        defg (rfT uT_aw);
         FunD (
           [moded @@ cpT @@ uT_aw],
           wrS @@ drf @@ v0
@@ -746,8 +740,8 @@ struct
   let%expect_test "simple call with read after write, dsl" =
     prog_eval_noret (
       [
-        defgu uT_aw;
+        defg uT_aw;
-        defg (rfT uT_aw) rfg0E;
+        defg (rfT uT_aw);
         FunD (
           [moded @@ cpT @@ uT_aw],
           (wrS @@ drf @@ v0) #.
@@ -762,8 +756,8 @@ struct
   let%expect_test "simple call with forbidden write, dsl" =
     try (prog_eval_noret (
       [
-        defgu uT_r_mw;
+        defg uT_r_mw;
-        defg (rfT uT_r_mw) rfg0E;
+        defg (rfT uT_r_mw);
         FunD (
           [moded @@ cpT @@ uT_r],
           wrS @@ drf @@ v0
@@ -779,8 +773,8 @@ struct
   let%expect_test "simple call with write to ref, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg (rfT uT_r_aw);
         FunD (
           [moded @@ rfT @@ uT_aw],
           wrS @@ drf @@ v0
@@ -794,8 +788,8 @@ struct
   let%expect_test "simple call with forbidden write to ref, dsl" =
     try (prog_eval_noret (
       [
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg (rfT uT_r_aw);
         FunD (
           [moded @@ rfT @@ uT_aw],
           wrS @@ drf @@ v0
@@ -811,8 +805,8 @@ struct
   let%expect_test "simple call with write to ref with fix, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg (rfT uT_r_aw);
         FunD (
           [moded @@ rfT @@ uT_aw],
           wrS @@ drf @@ v0
@@ -828,8 +822,8 @@ struct
   let%expect_test "call inside call, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg (rfT uT_r_aw);
         FunD (
           [moded @@ rfT @@ uT_aw],
           wrS @@ drf @@ v0
@@ -850,8 +844,8 @@ struct
   let%expect_test "call inside call, recursive, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg (rfT uT_r_aw);
         FunD (
           [moded @@ cpT @@ uT_aw],
           (callS vg2 [pE v0]) #.
@@ -867,8 +861,8 @@ struct
   let%expect_test "call to fix after call, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg (rfT uT_r_aw);
         FunD (
           [moded @@ rfT @@ uT_aw],
           wrS @@ drf @@ v0
@@ -888,8 +882,8 @@ struct
   let%expect_test "simple call with global variable usage, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r) rfg0E;
+        defg (rfT uT_r);
         FunD (
           [moded @@ cpT @@ uT],
           (wrS @@ vg0) #.
@@ -905,10 +899,10 @@ struct
   let%expect_test "simple call with read & write (2 args), dsl" =
     prog_eval_noret (
       [
-        defgu uT_r;
+        defg uT_r;
-        defg (rfT uT_r) rfg0E;
+        defg (rfT uT_r);
-        defgu uT_aw;
+        defg uT_aw;
-        defg (rfT uT_aw) rfg2E;
+        defg (rfT uT_aw);
         FunD (
           [
             moded @@ rfT @@ uT_r;
@@ -926,14 +920,14 @@ struct
   let%expect_test "simple call with different arguments modifiers, copy, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
+        defg (rfT uT_r_aw);
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg2E;
+        defg (rfT uT_r_aw);
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg4E;
+        defg (rfT uT_r_aw);
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg6E;
+        defg (rfT uT_r_aw);
         FunD (
           [
             ((NIn, NOut), cpT @@ uT);
@@ -960,14 +954,14 @@ struct
   let%expect_test "simple call with different arguments modifiers, ref, dsl" =
     prog_eval_noret (
       [
-        defgu uT_r;
+        defg uT_r;
-        defg (rfT uT_r) rfg0E;
+        defg (rfT uT_r);
-        defgu uT_r;
+        defg uT_r;
-        defg (rfT uT_r) rfg2E;
+        defg (rfT uT_r);
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg4E;
+        defg (rfT uT_r_aw);
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg6E;
+        defg (rfT uT_r_aw);
         FunD (
           [
             ((NIn, NOut), rfT @@ uT);
@@ -995,14 +989,14 @@ struct
   let%expect_test "presentation test 1 (simple types), dsl" =
     prog_eval_noret (
       [
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E; (* x *)
+        defg (rfT uT_r_aw); (* x *)
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg2E; (* y *)
+        defg (rfT uT_r_aw); (* y *)
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg4E; (* z *)
+        defg (rfT uT_r_aw); (* z *)
-        defgu uT_r_aw;
+        defg uT_r_aw;
-        defg (rfT uT_r_aw) rfg6E; (* k *)
+        defg (rfT uT_r_aw); (* k *)
         FunD ( (* f *)
           [
             (moded @@ rfT @@ uT_r_aw);
@@ -1073,7 +1067,7 @@ struct
       (* [ *)
         (* defg userT userE; *)
         (* defg dataT dataE; *)
-        (* defgu uT_r_aw; (* time *) *)
+        (* defg uT_r_aw; (* time *) *)
         (* defg requestT requestE; *)
         (* FunD ( (* send *) *)
           (* [ *)
@@ -1168,7 +1162,7 @@ struct
         (* defg userT userE; *)
         (* defg versionT versionE; *)
         (* defg utilsT utilsE; *)
-        (* defgu uT_r_aw; *)
+        (* defg uT_r_aw; *)
         (* defg requestT requestE; *)
         (* get_version_idF; *)
         (* updated_versionF; *)

model_with_structures/model.typ

@@ -15,8 +15,6 @@
 
 // *TODO: top-level value copy mode ??* // TODO: FIXME
 
-*TODO: add formal global env to all types and vals (as in code) ??* // TODO: FIXME
-
 #h(10pt)
 
 #let rf = $\& #h(3pt)$
@@ -140,14 +138,14 @@
     `decl`,
     {
       // TODO: path not allowed ??
-      Or[$"var" X : type = expr$][global variable declaration]
+      Or[$"var" X : type$][global variable declaration]
       Or[$"fun" X ((X : modedType)+) = stmt$][function declaration]
     }
   ),
   Prod(
     `prog`,
     {
-      Or[$decl+ space stmt$][declarations and executed statement]
+      Or[$decl+ stmt$][all program definitions and executed statement]
     }
   ),
 )
@@ -203,7 +201,7 @@
     $value_mu$,
     {
       Or[$cdl vmem, vread, vwrite cdr$][value of the simple type, contains cells for analysis] // `Unit`
-      Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun`
+      Or[$lambda$][function pointer value, carries no information] // `Fun`
       Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
       Or[$[value+]$][tuple value] // `Prod`
     }
@@ -276,8 +274,6 @@ $v in value$ - произвольное значение
   ),
 )
 
-// TODO: FIXME: add vars & funcs from global context in the beginnning
-
 // $V := memelem$ - значения памяти
 
 $X$ - можество переменных
@@ -286,18 +282,25 @@ $X$ - можество переменных
 #let types = $Gamma$
 #let envv = $#[env]_Sigma$
 #let envt = $#[env]_Gamma$
-$sigma : envv := X -> LL, space vals : envv$ - #[ метки памяти перменных контекста, частично определённая функция ]
+$envv := X -> LL, space vals : envv$ - #[ метки памяти перменных контекста, частично определённая функция ]
-$sigma : envt := X -> type, space types : envt$ - #[ типы значений перменных контекста, частично определённая функция ]
+$envt := X -> type, space types : envt$ - #[ типы значений перменных контекста, частично определённая функция ]
 
 $revpath$ - путь в обратную сторону, используется для обновления значений
 
 $action$ - действия, совершаемые с примитивным значением,
            модифицирующие содержащуюся таминформацию
 
-// $DD : X -> decl$ - глобальные определения, частично определённая функция
+- $r in readTag, w in writeTag$
-
+- $c in copyTag$
-// $d in decl, $
+- $i in inTag, o in outTag$
-$s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
+- $s in stmt$
+- $f, x, a in X$
+- $a in action$
+- $p in path$
+- $v in value$
+- $v_m in vmem, v_r in vread, v_w in vwrite$
+- $t, u in type$
+- $pi in revpath$
 
 === Path Accessors
 
@@ -533,89 +536,150 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 
 === Value Construction
 
+#let build = `build`
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ build trivial read value],
+
+    $mu xarrowSquiggly(cl Read \, w cr)_build
+     cl cdl 0_m, 0_r, 0_w cdr, mu cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ build trivial $not$ read value],
+
+    $mu xarrowSquiggly(cl not Read \, w cr)_build
+     cl cdl bot, 0_r, 0_w cdr, mu cr$,
+  )
+))
+
+#h(10pt)
+
+// TODO: function pointer type ??
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ build funciton pointer value],
+
+    $cl mu cr xarrowSquiggly(lambda space c space overline(t))_build cl lambda, mu cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ build reference value],
+
+    $mu xarrowSquiggly(t)_build cl v, mu_v cr$,
+
+    $mu_v xarrowSquiggly(v)_#[add] cl l, mu_a cr$,
+
+    $mu xarrowSquiggly(rf c t)_build cl rf l, mu_a cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ build tuple value],
+
+    $mu_0 xarrowSquiggly(t_1)_build cl v_1, mu_1 cr$,
+    $...$,
+    $mu_(n - 1) xarrowSquiggly(t_n)_build cl v_n, mu_n cr$,
+
+    $mu_0 xarrowSquiggly([t_1, ... t_n])_build cl [v_1, ... v_n], mu_n cr$,
+  )
+))
+
+#h(10pt)
+
+// ---
+
 // TODO: FIXME:add ref / copy modes correctness check ??
 
-#let new = `new`
+// #let copy = `copy`
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ new trivial read value],
-
-    $v_m in {0, ?, bot}$,
-    $cl cdl v_m, v_r, v_w cdr, mu cr
-     xarrowSquiggly(cl Read \, w cr)_new
-     cl cdl v_m, 0, 0 cdr, mu cr$,
-  )
-))
 
 // #align(center, prooftree(
 //   vertical-spacing: 4pt,
 //   rule(
-//     name: [ new trivial read $top$ value],
+//     name: [ new trivial read value],
 
-//     $cl cdl top, v_r, v_w cdr, mu cr
+//     // NOTE: should not be important to copy v_m, because spoil & tags
-//      xarrowSquiggly(cl Read \, w cr)_new
+//     // should care for this instead
-//      cl cdl 0, 0, 0 cdr, mu cr$,
+//     $v_m in {0, ?, bot}$,
+//     $cl cdl v_m, v_r, v_w cdr, mu cr
+//      xarrowSquiggly(cl Read \, w cr)_copy
+//      cl cdl v_m, 0_r, 0_w cdr, mu cr$,
 //   )
 // ))
 
-#align(center, prooftree(
+// #h(10pt)
-  vertical-spacing: 4pt,
-  rule(
-    name: [ new trivial $not$ read value],
-
-    $v_m in {0, ?, bot/*, top */}$,
-    $cl cdl v_m, v_r, v_w cdr, mu cr
-     xarrowSquiggly(cl not Read \, w cr)_new
-     cl cdl bot, 0, 0 cdr, mu cr$,
-  )
-))
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ new funciton pointer value],
-
-    $cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_new cl lambda overline(s), mu cr$,
-  )
-))
 
 // #align(center, prooftree(
 //   vertical-spacing: 4pt,
 //   rule(
-//     name: [ new reference ref value],
+//     name: [ new trivial $not$ read value],
 
-//     $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
+//     $v_m in {0, ?, bot/*, top */}$,
+//     $cl cdl v_m, v_r, v_w cdr, mu cr
+//      xarrowSquiggly(cl not Read \, w cr)_copy
+//      cl cdl bot, 0_r, 0_w cdr, mu cr$,
 //   )
 // ))
 
+// #h(10pt)
+
+// #align(center, prooftree(
+//   vertical-spacing: 4pt,
+//   rule(
+//     name: [ new funciton pointer value],
+
+//     $cl lambda, mu cr xarrowSquiggly(lambda space c space overline(t))_copy cl lambda, mu cr$,
+//   )
+// ))
+
+// #h(10pt)
+
 // NOTE: due to new memory cells types (with rw subcells) valnue should always be copied
-#align(center, prooftree(
+// #align(center, prooftree(
-  vertical-spacing: 4pt,
+//   vertical-spacing: 4pt,
-  rule(
+//   rule(
-    name: [ new reference /* copy */ value],
+//     name: [ new reference /* copy */ value],
 
-    $cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$,
+//     $cl mu[l], mu cr xarrowSquiggly(t)_copy cl v, mu_v cr$,
 
-    $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
+//     $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
 
-    $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_new cl rf l', mu_a cr$,
+//     $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_copy cl rf l', mu_a cr$,
-  )
+//   )
-))
+// ))
 
-#align(center, prooftree(
+// #h(10pt)
-  vertical-spacing: 4pt,
-  rule(
-    name: [ new tuple value],
 
-    $cl v_1, mu_0 cr xarrowSquiggly(t_1)_new cl lambda v'_1, mu_1 cr$,
+// #align(center, prooftree(
-    $...$,
+//   vertical-spacing: 4pt,
-    $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_new cl lambda v'_n, mu_n cr$,
+//   rule(
+//     name: [ new tuple value],
 
-    $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_new cl [v'_1, ... v'_n], mu_n cr$,
+//     $cl v_1, mu_0 cr xarrowSquiggly(t_1)_copy cl v'_1, mu_1 cr$,
-  )
+//     $...$,
-))
+//     $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_copy cl v'_n, mu_n cr$,
+
+//     $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_copy cl [v'_1, ... v'_n], mu_n cr$,
+//   )
+// ))
 
 === Action Rules
 
@@ -898,12 +962,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ combine lambda values],
 
-    $overline(x_1) = overline(x_2)$,
+    $lambda plus.o lambda = lambda$
-    $s_1 = s_2$,
-    $lambda space [overline(x^1_1) space s^1_1, ... overline(x^n_1) space s^n_1]
-     plus.o lambda space [overline(x^1_2) space s^1_2, ... overline(x^m_2) space s^m_2]
-     = lambda space [overline(x^1_1) space s^1_1, ... overline(x^n_1) space s^n_1,
-                     overline(x^1_2) space s^1_2, ... overline(x^m_2) space s^m_2]$
   )
 ))
 
@@ -1059,11 +1118,10 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
     // NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers)
     // expect well typed program
 
-    $vals, mu texpre e eqmu v$,
+    $cl mu cr xarrowSquiggly(t)_build cl v, mu' cr$,
-    $cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$, // TODO: FIXME check (required?)
+    $mu' xarrowSquiggly(v)_#[add] cl l, mu'' cr$,
-    $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$,
 
-    $cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu'' cr$
+    $cl types, vals, mu cr xarrowSquiggly("var" x : t)_init cl types[x <- t], vals[x <- l], mu'' cr$
   )
 ))
 
@@ -1074,7 +1132,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ add function declaration],
 
-    $mu xarrowSquiggly(lambda space [[x_1, ... x_n] s])_#[add] cl l, mu' cr$,
+    $mu xarrowSquiggly(lambda)_#[add] cl l, mu' cr$,
 
     $cl types, vals, mu cr
      xarrowSquiggly("fun" f (x_1 space : space m_1 t_1, ... space x_n space : space m_n t_n) space = space s)_init
@@ -1254,8 +1312,6 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   )
 ))
 
-#h(10pt)
-
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
@@ -1342,17 +1398,13 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ add argument],
 
-    $vals_#[ctx], mu texpre e eqmu v$,
+    // programs considired to be well-typed
-    // $types ttype p : t'$, // TODO: not required if there is no check
+    $cl v, mu cr xarrowSquiggly(t)_build cl v, mu' cr$,
-    // TODO: check type compatibility for t and type for path p (?)
+    $mu' xarrowSquiggly(v)_#[add] cl l, mu'' cr$,
-    // [*TODO: check t ~ t' in sme way (?)*],
-    // <- programs considired to be well-typed
-    $cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$,
-    $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$,
 
     // TODO save type mode somewhere ?? // <- not needed because is described by other params <- ??
     $cl types, vals, mu cr
-     xarrowDashed(x space t space e)_(vals_#[ctx])
+     xarrowDashed(x space t)
      cl types[x <- t], vals[x <- l], mu'' cr$,
   )
 ))
@@ -1411,7 +1463,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ lambda check],
 
-    $mu ttags lambda space overline(s) : lambda overline(t)$,
+    $mu ttags lambda : lambda overline(t)$,
   )
 ))
 #align(center, prooftree(
@@ -1439,20 +1491,15 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ new reference copy value],
+    name: [ function declaration evaluation],
-
-    // TODO: FIXME: introduce global types and vals
-    $types_0 = types_#[glob]$,
-    $vals_0 = vals_#[glob]$,
-    $mu_0 = mu$,
 
     // NOTE: dashed arrow to fill context
     $cl types_0, vals_0,  mu_0 cr
-     xarrowDashed(x_1 space t_1 space e_1)_vals
+     xarrowDashed(x_1 space t_1)
      cl types', vals_1, mu_1 cr$,
     $...$,
     $cl types_(n - 1), vals_(n - 1),  mu_(n - 1) cr
-     xarrowDashed(x_n space t_n space e_n)_vals
+     xarrowDashed(x_n space t_n)
      cl types_n, vals_n, mu_n cr$,
 
     // NOTE: eval function body
@@ -1465,7 +1512,18 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
     $...$,
     $mu' ttags mu'[vals'[x_n]] : t_n$,
 
-    $vals, mu_0 tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$,
+    $types_0, vals_0, mu_0 tfunceval "fun" f [(x_1 m_1 t_1), .. (x_n m_n x_n)] = s$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ var declaration evaluation (skip)],
+
+    $types, vals, mu tfunceval "var" x : t$,
   )
 ))
 
@@ -1554,14 +1612,8 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
   rule(
     name: [ CALL $f space [e_1, ... e_n]$],
 
-    $vals, mu_0 tval f eqmu lambda [overline(x)_1 space s_1, ... overline(x)_n space s_n]$,
     $types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
 
-    // NOTE: check that all the possible bodies are possible to eval
-    $vals, mu_0 tfunceval cl s_1, overline(x)_1, [t_1, ... t_n], [e_1, ... e_n] cr$,
-    $...$,
-    $vals, mu_0 tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] cr$,
-
     // NOTE: "spoil" context for each argument usage
     $mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$,
     $...$,
@@ -1676,14 +1728,11 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
     $...$,
     $cl types_(n - 1), vals_(n - 1), mu_(n - 1) cr xarrowSquiggly(d_n)_init cl types_n, vals_n, mu_n cr$,
 
-    // TODO: FIXME: some easy way to pass to eval ??
+    $cl types_n, vals_n, mu_n tfunceval d_1$,
-    $types_#[glob] = types_n$,
+    $...$,
-    $vals_#[glob] = vals_n$,
+    $cl types_n, vals_n, mu_n tfunceval d_n$,
-    $mu_#[glob] = mu_n$,
 
-    $cl types_n, vals_n, mu_n cr xarrow(s) cl types', vals', mu' cr$,
+    $cl types_0, vals_0, mu_0 cr xarrowSquiggly(d_1 ... d_n)_prog_eval  cl types_n, vals_n, mu_n cr$
-
-    $cl types_0, vals_0, mu_0 cr xarrowSquiggly(d_1 ... d_n s)_prog_eval  cl types', vals', mu' cr$
   )
 ))
 

model_with_structures/send_example.md

@@ -49,19 +49,19 @@ struct Request {
   Version* version;
   Utils* utils;
   Data* data;
-  DateTime operaiton_date;
+  DateTime time;
 };
 
 // example itself
 
-int get_version_id(Request /*[?]*/  r) {
+int get_version_id(Request /*[?]*/ r) {
   if (r.utils.has_version) {
     return r.version.id;
   }
   return old_version_placeholder().id;
 }
 
-Version updated_version(Request /*[?]*/  r) {
+Version updated_version(Request /*[?]*/ r) {
   if (not r.utils.has_version) {
     return old_version_placeholder();
   }
@@ -114,12 +114,12 @@ Request := [& User; # user
             & Version; # version
             & Utils; # utils
             & (); # data
-            ()] # operation_date
+            ()] # time
 # or Request := [& [& [(); ()], & [(); (); ()]]; # user
 #                & [(); (); ()]; # version
 #                & [(); ()]; # utils
 #                & (); # data
-#                ()] # operation_date
+#                ()] # time
 
 # example itself
 

model_with_structures/synthesizer.ml

@@ -147,7 +147,7 @@ struct
   module Decl = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ((* 'd, *) 't, 'e, (* 'dl, *) 'mtl, 's) t = VarD of (* 'd * *) 't * 'e | FunD of (* 'd * 'dl * *) 'mtl * 's
+      type nonrec ((* 'd, *) 't, 'e, (* 'dl, *) 'mtl, 's) t = VarD of (* 'd * *) 't | FunD of (* 'd * 'dl * *) 'mtl * 's
       [@@deriving gt ~options:{ show; gmap }]
       type ground = ((* Nat.ground, *) Type.ground, Expr.ground, (* Nat.ground List.ground, *) (Mode.ground * Type.ground) List.ground, Stmt.ground) t
     ]
@@ -194,13 +194,12 @@ struct
   module Value = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ('vm, 'vr, 'vw, 'sl, 'd, 'vl) t = UnitV of 'vm * 'vr * 'vw
+      type nonrec ('vm, 'vr, 'vw, 'd, 'vl) t = UnitV of 'vm * 'vr * 'vw
-                                                  | FunV of 'sl
+                                             | FunV
-                                                  | RefV of 'd
+                                             | RefV of 'd
-                                                  | TupleV of 'vl
+                                             | TupleV of 'vl
       [@@deriving gt ~options:{ show; gmap }]
       type ground = (MemVal.ground, ReadVal.ground, WriteVal.ground,
-                     ((* Nat.ground List.ground * *) Stmt.ground) List.ground,
                      Nat.ground, ground List.ground) t
     ]
   end
@@ -237,7 +236,7 @@ struct
   module TypesEnv = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec 'dtl t = TypesEnv of 'dtl (* glob *) * 'dtl (* glob + loc *)
+      type nonrec 'dtl t = TypesEnv of 'dtl
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = ((Nat.ground * Type.ground) List.ground) t
     ]
@@ -246,27 +245,18 @@ struct
   module ValsEnv = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec 'ddl t = ValsEnv of 'ddl (* glob *) * 'ddl (* glob + loc *)
+      type nonrec 'ddl t = ValsEnv of 'ddl
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t
     ]
   end
 
-  module VisitedEnv = struct
-    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
-    [%%ocanren_inject
-      type nonrec 'sl t = VisitedEnv of 'sl
-      [@@deriving gt ~options:{ show; gmap }]
-      type nonrec ground = (Stmt.ground List.ground) t
-    ]
-  end
-
   module StEnv = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ('mem, 'types, 'vals, 'visited) t = StEnv of 'mem * 'types * 'vals * 'visited
+      type nonrec ('mem, 'types, 'vals) t = StEnv of 'mem * 'types * 'vals
       [@@deriving gt ~options:{ show; gmap }]
-      type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground, VisitedEnv.ground) t
+      type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground) t
     ]
   end
 
@@ -405,87 +395,35 @@ struct
   let types_assoco id types tp =
     let open TypesEnv in
     ocanren {
-      fresh _glob_tps, tps in
+      fresh tps in
-      types == TypesEnv (_glob_tps, tps) &
+      types == TypesEnv tps &
       List.assoco id tps tp
     }
 
   let vals_assoco id vals v =
     let open ValsEnv in
     ocanren {
-      fresh _glob_vs, vs in
+      fresh vs in
-      vals == ValsEnv (_glob_vs, vs) &
+      vals == ValsEnv vs &
       List.assoco id vs v
     }
 
-  let types_glob_addo types x tp types' = 
-    let open TypesEnv in
-    ocanren {
-      fresh glob_tps, tps in
-      types == TypesEnv (glob_tps, tps) &
-      types' == TypesEnv ((Std.pair x tp) :: glob_tps,
-                          (Std.pair x tp) :: tps)
-  }
-
   let types_addo types x tp types' = 
     let open TypesEnv in
     ocanren {
-      fresh glob_tps, tps in
+      fresh tps in
-      types == TypesEnv (glob_tps, tps) &
+      types == TypesEnv tps &
-      types' == TypesEnv (glob_tps, (Std.pair x tp) :: tps)
+      types' == TypesEnv ((Std.pair x tp) :: tps)
-  }
-
-  let vals_glob_addo vals x v vals' = 
-    let open ValsEnv in
-    ocanren {
-      fresh glob_vs, vs in
-      vals == ValsEnv (glob_vs, vs) &
-      vals' == ValsEnv ((Std.pair x v) :: glob_vs,
-                        (Std.pair x v) :: vs)
   }
 
   let vals_addo vals x v vals' = 
     let open ValsEnv in
     ocanren {
-      fresh glob_vs, vs in
+      fresh vs in
-      vals == ValsEnv (glob_vs, vs) &
+      vals == ValsEnv vs &
-      vals' == ValsEnv (glob_vs, (Std.pair x v) :: vs)
+      vals' == ValsEnv ((Std.pair x v) :: vs)
   }
 
-  let visited_appendo visitedl visitedr visited' = 
-    let open VisitedEnv in
-    ocanren {
-      fresh vsl, vsr, vs' in
-      visitedl == VisitedEnv vsl &
-      visitedr == VisitedEnv vsr &
-      List.appendo vsl vsr vs' &
-      visited' == VisitedEnv vs'
-  }
-
-  let visited_checko visited stmt =
-    let open VisitedEnv in
-    ocanren {
-      fresh vs in
-      visited == VisitedEnv vs &
-      List.membero vs stmt
-    }
-
-  let not_visited_checko visited stmt =
-    let open VisitedEnv in
-    ocanren {
-      fresh vs in
-      visited == VisitedEnv vs &
-      list_not_membero vs stmt
-    }
-
-  let visited_addo visited stmt visited' =
-    let open VisitedEnv in
-    ocanren {
-      fresh vs in
-      visited == VisitedEnv vs &
-      visited' == VisitedEnv (stmt :: vs)
-    }
-
   (* --- *)
 
   let mem_geto mem id v =
@@ -588,15 +526,15 @@ struct
 
   (* - value construction *)
 
-  let rec valcopy_foldero mem_with_vs v tp mem_with_vs' =
+  let rec valbuild_foldero mem_with_vs tp mem_with_vs' =
     ocanren {
       fresh mem, vs, mem', v', vs' in
       Std.pair mem vs == mem_with_vs &
-      valcopyo mem v tp (Std.pair mem' v') &
+      valbuildo mem tp (Std.pair mem' v') &
       vs' == v' :: vs &
       mem_with_vs' == Std.pair mem' vs'
   }
-  and valcopyo mem v tp mem_with_id' = 
+  and valbuildo mem tp mem_with_id' = 
     let open Type in
     let open Value in
     let open ReadCap in
@@ -606,35 +544,72 @@ struct
     let open WriteVal in
     ocanren {
       { fresh r, w in
-        is_trivial_vo v &
         tp == UnitT (r, w) &
-        { { fresh v_m, _v_r, _v_w in
+        { { r == Rd &
-            r == Rd &
+            mem_with_id' == Std.pair mem (UnitV (ZeroMV, ZeroRV, ZeroWV)) } |
-            v == UnitV (v_m, _v_r, _v_w) &
-            mem_with_id' == Std.pair mem (UnitV (v_m, ZeroRV, ZeroWV)) } |
           { r == NRd &
             mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } |
-      { fresh stmts, ts in
+      (* { fresh ts in *)
-        v == FunV stmts &
+        (* tp == FunT ts & *)
-        tp == FunT ts &
+        (* ??? } | *)
-        mem_with_id' == Std.pair mem v } |
+      { fresh c, tp' in
-      { fresh c, tp', id in
-        v == RefV id &
         tp == RefT (c, tp') &
-        (* { c == Rf & mem_with_id' == Std.pair mem v } | *)
+        { fresh mem_cp, v_cp, mem_add, id_add in
-        { fresh v', mem_cp, v_cp, mem_add, id_add in
+          valbuildo mem tp' (Std.pair mem_cp v_cp) &
-          (* c == Cp & *)
-          mem_geto mem id v' &
-          valcopyo mem v' tp' (Std.pair mem_cp v_cp) &
           mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
           mem_with_id' == (mem_add, RefV id_add) } } |
-      { fresh vs, tps, mem', vs' in
+      { fresh tps, mem', vs' in
-        v == TupleV vs &
         tp == TupleT tps &
-        list_foldr2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') &
+        list_foldro valbuild_foldero (Std.pair mem []) tps (Std.pair mem' vs') &
         mem_with_id' == Std.pair mem' (TupleV vs') }
   }
 
+  (* let rec valcopy_foldero mem_with_vs v tp mem_with_vs' = *)
+    (* ocanren { *)
+      (* fresh mem, vs, mem', v', vs' in *)
+      (* Std.pair mem vs == mem_with_vs & *)
+      (* valcopyo mem v tp (Std.pair mem' v') & *)
+      (* vs' == v' :: vs & *)
+      (* mem_with_vs' == Std.pair mem' vs' *)
+  (* } *)
+  (* and valcopyo mem v tp mem_with_id' = *) 
+    (* let open Type in *)
+    (* let open Value in *)
+    (* let open ReadCap in *)
+    (* let open CopyCap in *)
+    (* let open MemVal in *)
+    (* let open ReadVal in *)
+    (* let open WriteVal in *)
+    (* ocanren { *)
+      (* { fresh r, w in *)
+        (* tp == UnitT (r, w) & *)
+        (* { { fresh v_m, _v_r, _v_w in *)
+            (* r == Rd & *)
+            (* v == UnitV (v_m, _v_r, _v_w) & *)
+            (* mem_with_id' == Std.pair mem (UnitV (v_m, ZeroRV, ZeroWV)) } | *)
+          (* { r == NRd & *)
+            (* mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } | *)
+      (* { fresh stmts, ts in *)
+        (* v == FunV stmts & *)
+        (* tp == FunT ts & *)
+        (* mem_with_id' == Std.pair mem v } | *)
+      (* { fresh c, tp', id in *)
+        (* v == RefV id & *)
+        (* tp == RefT (c, tp') & *)
+        (* { c == Rf & mem_with_id' == Std.pair mem v } | *)
+        (* { fresh v', mem_cp, v_cp, mem_add, id_add in *)
+          (* c == Cp & *)
+          (* mem_geto mem id v' & *)
+          (* valcopyo mem v' tp' (Std.pair mem_cp v_cp) & *)
+          (* mem_addo mem_cp v_cp (Std.pair mem_add id_add) & *)
+          (* mem_with_id' == (mem_add, RefV id_add) } } | *)
+      (* { fresh vs, tps, mem', vs' in *)
+        (* v == TupleV vs & *)
+        (* tp == TupleT tps & *)
+        (* list_foldr2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') & *)
+        (* mem_with_id' == Std.pair mem' (TupleV vs') } *)
+  (* } *)
+
   (* - action rules *)
 
   let memvmodo a v_m v_m' =
@@ -757,8 +732,7 @@ struct
       { u == ZeroRV & v == ZeroRV & u' == ZeroRV } |
       { u == TopRV & v == ZeroRV & u' == ZeroRV } |
       { u == ZeroRV & v == TopRV & u' == ZeroRV } |
-      { u =/= TopRV & v =/= TopRV &
+      { { u == OneRV | { u =/= OneRV & v == OneRV } } &
-        u =/= ZeroRV & v =/= ZeroRV & 
         u' == OneRV }
   }
 
@@ -784,12 +758,9 @@ struct
       readvalcombo u_r v_r u_r' &
       writevalcombo u_w v_w u_w' &
       u' == UnitV (u_m', u_r', u_w') } |
-    { fresh ustmts, vstmts, ustmts' in
+    { u == FunV &
-      u == FunV ustmts &
+      v == FunV &
-      v == FunV vstmts &
+      u' == FunV } |
-      (* TODO: swap stmts order o efficiency ? *)
-      List.appendo ustmts vstmts ustmts' &
-      u' == FunV ustmts' } |
     { fresh a, b in
       u == RefV a &
       v == RefV b &
@@ -874,32 +845,26 @@ struct
     let open Value in
     let open Type in
     ocanren {
-      fresh mem, types, vals, visited in
+      fresh mem, types, vals in
-      st == StEnv (mem, types, vals, visited) &
+      st == StEnv (mem, types, vals) &
       {
-        { fresh tp, e, v,
+        { fresh tp, mem_bd, v_bd,
-                mem_cp, v_cp,
                 mem_add, id_add,
                 types', vals' in
-          d == VarD (tp, e) &
+          d == VarD tp &
-          exprvalo mem vals e v &
+          valbuildo mem tp (Pair.pair mem_bd v_bd) &
-          valcopyo mem v tp (Pair.pair mem_cp v_cp) &
+          mem_addo mem_bd v_bd (Pair.pair mem_add id_add) &
-          (* mem_cp == mem & v_cp == v & *)
+          types_addo types x tp types' &
-          mem_addo mem_cp v_cp (Pair.pair mem_add id_add) &
+          vals_addo vals x id_add vals' &
-          (* mem_add == mem_cp & *)
+          st' == StEnv (mem_add, types', vals') } |
-          types_glob_addo types x tp types' &
-          (* types == types' & *)
-          (* vals == vals' & *)
-          vals_glob_addo vals x id_add vals' &
-          st' == StEnv (mem_add, types', vals', visited) } |
         { fresh tps, s,
                 mem_add, id_add,
                 types', vals' in
           d == FunD (tps, s) &
-          mem_addo mem (FunV [s]) (Pair.pair mem_add id_add) &
+          mem_addo mem FunV (Pair.pair mem_add id_add) &
-          types_glob_addo types x (FunT tps) types' &
+          types_addo types x (FunT tps) types' &
-          vals_glob_addo vals x id_add vals' &
+          vals_addo vals x id_add vals' &
-          st' == StEnv (mem_add, types', vals', visited)
+          st' == StEnv (mem_add, types', vals')
          }
       }
   }
@@ -912,11 +877,10 @@ struct
     let open StEnv in
     let open TypesEnv in
     let open ValsEnv in
-    let open VisitedEnv in
     ocanren {
       fresh m in
       empty_memo m &
-      st == StEnv (m, TypesEnv ([], []), ValsEnv ([], []), VisitedEnv [])
+      st == StEnv (m, TypesEnv [], ValsEnv [])
   }
 
   (* TODO: better way ??? *)
@@ -1022,9 +986,9 @@ struct
             v'' == UnitV (v_m''', v_r'', v_w'') &
             mem_with_v' == Std.pair mem v'' }
         } } |
-      { fresh ts, _stmts in
+      { fresh ts in
         tp == FunT ts &
-        v == FunV _stmts &
+        v == FunV &
         mem_with_v' == Std.pair mem v } |
       { fresh ctp', tp', id', v', mem_sp, v_sp, mem_set in
         tp == RefT (ctp', tp') &
@@ -1050,10 +1014,10 @@ struct
     let open CopyCap in
     let open RevPath in
     ocanren {
-      fresh mem, types, vals, visited,
+      fresh mem, types, vals,
             x, id, b(* , tp' *), rp,
             mem_sp, b_sp, v_sp, mem_upd, v_upd in
-      st == StEnv (mem, types, vals, visited) &
+      st == StEnv (mem, types, vals) &
       pathvaro p x &
       vals_assoco x vals id &
       pathvalo mem vals p b &
@@ -1065,11 +1029,11 @@ struct
       mem_seto mem_upd id v_upd mem'
   }
 
-  let rec argsspoile_foldero types vals visited m mem tp e mem' =
+  let rec argsspoile_foldero types vals m mem tp e mem' =
     let open StEnv in
     ocanren {
       fresh st in
-      st == StEnv (mem, types, vals, visited) &
+      st == StEnv (mem, types, vals) &
       argsspoileo st m tp e mem'
   }
   and argsspoileo st m tp e mem' =
@@ -1078,8 +1042,8 @@ struct
     let open Type in
     let open Path in
     ocanren {
-      fresh _r, _w, mem, types, vals, visited in
+      fresh _r, _w, mem, types, vals in
-      st == StEnv (mem, types, vals, visited) &
+      st == StEnv (mem, types, vals) &
       {
         { e == UnitE &
           tp == UnitT (_r, _w) &
@@ -1093,30 +1057,28 @@ struct
         { fresh es, tps in
           e == TupleE es &
           tp == TupleT tps &
-          list_foldl2o (argsspoile_foldero types vals visited m) mem tps es mem'}
+          list_foldl2o (argsspoile_foldero types vals m) mem tps es mem'}
       }
   }
 
   (* - funciton argument addition *)
 
-  let addargo st oldvals x tp e st' =
+  let addargo st x tp st' =
     let open StEnv in
     ocanren {
-      fresh mem, types, vals, visited, v,
+      fresh mem, types, vals,
-            mem_cp, v_cp,
+            mem_bd, v_bd,
             mem_add, id_add,
             types', vals' in
-      st == StEnv (mem, types, vals, visited) &
+      st == StEnv (mem, types, vals) &
-      exprvalo mem oldvals e v &
+      valbuildo mem tp (Std.pair mem_bd v_bd) &
-      valcopyo mem v tp (Std.pair mem_cp v_cp) &
+      mem_addo mem_bd v_bd (Std.pair mem_add id_add) &
-      mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
       types_addo types x tp types' &
       vals_addo vals x id_add vals' &
-      st' == StEnv (mem_add, types', vals', visited)
+      st' == StEnv (mem_add, types', vals')
   }
 
-  (* - function evaluation *)
+  (* --- *)
-  (* NOTE: not needed due to performed optimization in stmt_eval ? *)
 
   let writeval_to_capo v_w w' =
     let open WriteVal in
@@ -1144,8 +1106,8 @@ struct
         } &
         writeval_to_capo v_w w
          } |
-      { fresh _stmts, _ts in
+      { fresh _ts in
-        v == FunV _stmts &
+        v == FunV &
         tp == FunT _ts } |
       { fresh id, _c, tp', v' in
         v == RefV id &
@@ -1179,90 +1141,34 @@ struct
 
   (* - statement evaluation *)
 
-  let rec stmt_addarg_foldero vals st_with_id mtp e st_with_id' = ocanren {
+  let rec stmt_eval_spoil_foldero types vals mem mtp e mem' =
-    fresh st, x, m, tp, st' in
-    Std.pair st x == st_with_id &
-    Std.pair m tp == mtp &
-    addargo st vals x tp e st' &
-    st_with_id' == Std.pair st' (Nat.s x)
-  }
-  and f_tags_check_foldero mem vals x mtp x' = ocanren {
-    fresh m, tp, id', v' in
-    mtp == Std.pair m tp &
-    vals_assoco x vals id' &
-    mem_geto mem id' v' &
-    tags_checko mem v' tp &
-    x' == Nat.s x
-  }
-  and stmt_eval_func_foldero mem types vals tps visited stmt visited' =
-    let open StEnv in
-    ocanren {
-      { fresh visited_add, st,
-              st', mem', types', vals',
-              _x', visited'' in
-        not_visited_checko visited stmt &
-        visited_addo visited stmt visited_add &
-        st == StEnv (mem, types, vals, visited_add) &
-        stmt_evalo st stmt st' &
-        st' == StEnv (mem', types', vals', visited'') &
-        list_foldlo (f_tags_check_foldero mem' vals') 0 tps _x' &
-        visited' == visited''
-         } |
-      { visited_checko visited stmt &
-        visited == visited' }
-  }
-  and stmt_eval_spoil_foldero types vals visited mem mtp e mem' =
     let open StEnv in
     ocanren {
       fresh m, tp, st in
       Std.pair m tp == mtp &
-      st == StEnv (mem, types, vals, visited) &
+      st == StEnv (mem, types, vals) &
       argsspoileo st m tp e mem'
   }
   and stmt_evalo st s st' =
     let open StEnv in
     let open Stmt in
-    let open Value in
     let open Type in
-    (* let open WriteCap in *)
-    let open TypesEnv in
-    let open ValsEnv in
     let open RevPath in
     let open Action in
     ocanren {
-      fresh mem, types, vals, visited in
+      fresh mem, types, vals in
-      st == StEnv (mem, types, vals, visited) &
+      st == StEnv (mem, types, vals) &
       {
         { s == SkipS & st == st' } |
-        { fresh f, es, v, tp,
+        { fresh f, es, tp,
-                glob_tps, _tps,
+                _tps, _vs, tps,
-                glob_vs, _vs,
+                mem_spoiled in
-                types_call, vals_call,
-                fstmts, tps, st_call,
-                state_with_args,
-                mem_swa, types_swa,
-                vals_swa, visited_swa,
-                _arg_id, mem_spoiled,
-                visited' in
           s == CallS (f, es) &
-          pathvalo mem vals f v &
           pathtypeo types f tp &
-          types == TypesEnv (glob_tps, _tps) &
-          vals == ValsEnv (glob_vs, _vs) &
-          types_call == TypesEnv (glob_tps, glob_tps) &
-          vals_call == ValsEnv (glob_vs, glob_vs) &
-          v == FunV fstmts &
           tp == FunT tps &
-          st_call == StEnv (mem, types_call, vals_call, visited) &
+          list_foldl2o (stmt_eval_spoil_foldero types vals)
-          list_foldl2o (stmt_addarg_foldero vals)
-                       (Std.pair st_call 0) tps es
-                       (Std.pair state_with_args _arg_id) &
-          state_with_args == StEnv (mem_swa, types_swa, vals_swa, visited_swa) &
-          list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa tps) visited_swa fstmts visited' &
-          (* TODO: FIXME check left or right order *)
-          list_foldl2o (stmt_eval_spoil_foldero types vals (* NOTE: not important*) visited')
                        mem tps es mem_spoiled &
-          st' == StEnv (mem_spoiled, types, vals, visited')
+          st' == StEnv (mem_spoiled, types, vals)
         } |
         { fresh p, tp, x, id, v, rp,
                 mem_upd, v_upd, mem_set in
@@ -1275,7 +1181,7 @@ struct
           pathrevo p VarRP rp &
           valupdo mem v rp AlwaysWriteA (Std.pair mem_upd v_upd) &
           mem_seto mem_upd id v_upd mem_set &
-          st' == StEnv (mem_set, types, vals, visited) } |
+          st' == StEnv (mem_set, types, vals) } |
         { fresh p, _tp, _r, _w, x, id, v, rp,
                 mem_upd, v_upd, mem_set in
           s == ReadS p &
@@ -1285,7 +1191,7 @@ struct
           pathrevo p VarRP rp &
           valupdo mem v rp ReadA (Std.pair mem_upd v_upd) &
           mem_seto mem_upd id v_upd mem_set &
-          st' == StEnv (mem_set, types, vals, visited) } |
+          st' == StEnv (mem_set, types, vals) } |
         (* { fresh p in *)
           (* s == ReadS p & *)
           (* pathvalo mem vals p ZeroV & *)
@@ -1295,22 +1201,58 @@ struct
           stmt_evalo st sl stl &
           stmt_evalo stl sr st' } |
         { fresh sl, sr, stl, str,
-                meml, typesl, valsl, visitedl,
+                meml, typesl, valsl,
-                memr, typesr, valsr, visitedr,
+                memr, typesr, valsr,
-                visited', mem' in
+                mem' in
           s == ChoiceS (sl, sr) &
           stmt_evalo st sl stl &
           stmt_evalo st sr str &
-          stl == StEnv (meml, typesl, valsl, visitedl) &
+          stl == StEnv (meml, typesl, valsl) &
-          str == StEnv (memr, typesr, valsr, visitedr) &
+          str == StEnv (memr, typesr, valsr) &
           typesl == typesr &
           valsl == valsr &
           memcombo meml memr mem' &
-          visited_appendo visitedr visitedl visited' &
+          st' == StEnv (mem', typesl, valsl) }
-          st' == StEnv (mem', typesl, valsl, visited') }
       }
   }
 
+  (* - function evaluation *)
+
+  let rec f_addarg_foldero st_with_id mtp st_with_id' = ocanren {
+    fresh st, x, m, tp, st' in
+    Std.pair st x == st_with_id &
+    Std.pair m tp == mtp &
+    addargo st x tp st' &
+    st_with_id' == Std.pair st' (Nat.s x)
+  }
+  and f_tags_check_foldero mem vals x mtp x' = ocanren {
+    fresh m, tp, id', v' in
+    mtp == Std.pair m tp &
+    vals_assoco x vals id' &
+    mem_geto mem id' v' &
+    tags_checko mem v' tp &
+    x' == Nat.s x
+  }
+
+  (* list_foldlo (stmt_eval_func_foldero mem_swa types_swa vals_swa tps) visited_swa fstmts visited' & *)
+  and func_evalo st d =
+    let open StEnv in
+    let open Decl in
+    ocanren {
+      { fresh tps, stmt,
+              state_with_args, _arg_id, st_after_stmt,
+              mem_after_stmt, _types_after_stmt, vals_after_stmt, _x' in
+        d == FunD (tps, stmt) &
+        list_foldlo f_addarg_foldero
+                    (Std.pair st 0) tps
+                    (Std.pair state_with_args _arg_id) &
+        stmt_evalo state_with_args stmt st_after_stmt &
+        st_after_stmt == StEnv (mem_after_stmt, _types_after_stmt, vals_after_stmt) &
+        list_foldlo (f_tags_check_foldero mem_after_stmt vals_after_stmt) 0 tps _x'
+         } |
+      { fresh _tp in
+        d == VarD _tp }
+  }
   (* --- program execution --- *)
 
   let prog_evalo prog st' =
@@ -1319,6 +1261,7 @@ struct
       fresh decls, s, init_st in
       prog == Prg (decls, s) &
       prog_inito prog init_st &
+      list_checko (func_evalo init_st) decls &
       stmt_evalo init_st s st'
   }
 end

model_with_structures/tests_f.ml

@@ -67,7 +67,7 @@ let prog_eval_t_simple_var _ = show(answer) (Stream.take (run q
   (fun q -> ocanren {
               fresh prog, xg in
               globals_min_ido xg &
-              prog == Prg ([VarD (UnitT (Rd, MayWr), UnitE)],
+              prog == Prg ([VarD (UnitT (Rd, MayWr))],
                            ReadS (VarP xg)) &
               prog_evalo prog q })
   (fun q -> q#reify (StEnv.prj_exn))))
@@ -87,7 +87,7 @@ let prog_eval_t_simple_var_fbd_rd _ = show(answer) (Stream.take (run q
   (fun q -> ocanren {
               fresh prog, xg in
               globals_min_ido xg &
-              prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)],
+              prog == Prg ([VarD (UnitT (NRd, MayWr))],
                            ReadS (VarP xg)) &
               prog_evalo prog q })
   (fun q -> q#reify (StEnv.prj_exn))))
@@ -97,8 +97,8 @@ let prog_eval_t_simple_vars_fbd_rd_rd _ = show(answer) (Stream.take (run q
               fresh prog, xg, yg in
               globals_min_ido xg &
               yg == Nat.s xg &
-              prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE);
+              prog == Prg ([VarD (UnitT (NRd, MayWr));
-                            VarD (UnitT (Rd, MayWr), UnitE)],
+                            VarD (UnitT (Rd, MayWr))],
                            ReadS (VarP yg)) &
               prog_evalo prog q })
   (fun q -> q#reify (StEnv.prj_exn))))
@@ -107,7 +107,7 @@ let prog_eval_t_simple_var_wr _ = show(answer) (Stream.take (run q
   (fun q -> ocanren {
               fresh prog, xg in
               globals_min_ido xg &
-              prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)],
+              prog == Prg ([VarD (UnitT (NRd, MayWr))],
                            WriteS (VarP xg)) &
               prog_evalo prog q })
   (fun q -> q#reify (StEnv.prj_exn))))
@@ -116,7 +116,7 @@ let prog_eval_t_simple_var_fbd_wr _ = show(answer) (Stream.take (run q
   (fun q -> ocanren {
               fresh prog, xg in
               globals_min_ido xg &
-              prog == Prg ([VarD (UnitT (NRd, NeverWr), UnitE)],
+              prog == Prg ([VarD (UnitT (NRd, NeverWr))],
                            WriteS (VarP xg)) &
               prog_evalo prog q })
   (fun q -> q#reify (StEnv.prj_exn))))
@@ -125,7 +125,7 @@ let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q
   (fun q -> ocanren {
               fresh prog, xg in
               globals_min_ido xg &
-              prog == Prg ([VarD (UnitT (NRd, MayWr), UnitE)],
+              prog == Prg ([VarD (UnitT (NRd, MayWr))],
                            SeqS (WriteS (VarP xg),
                                  ReadS (VarP xg))) &
               prog_evalo prog q })
@@ -139,7 +139,7 @@ let prog_eval_t_simple_var_wr_rd _ = show(answer) (Stream.take (run q
               (* fresh prog, xg, fg, xd, fd in *)
               (* globals_min_ido xg & *)
               (* fg == Nat.s xg & *)
-              (* xd == VarD (UnitT (Rd, NeverWr), UnitE) & *)
+              (* xd == VarD (UnitT (Rd, NeverWr)) & *)
               (* fd == FunD ([], SkipS) & *)
               (* prog == Prg ([xd; fd], CallS (VarP fg, [])) & *)
               (* prog_evalo prog q }) *)
@@ -150,7 +150,7 @@ let prog_eval_t_simple_call_rd _ = show(answer) (Stream.take (run q
               fresh prog, xg, fg, xd, fd in
               globals_min_ido xg &
               fg == Nat.s xg &
-              xd == VarD (UnitT (Rd, NeverWr), UnitE) &
+              xd == VarD (UnitT (Rd, NeverWr)) &
               fd == FunD ([(Mode (In, NOut), UnitT (Rd, NeverWr))], ReadS (VarP 0)) &
               prog == Prg ([xd; fd], CallS (VarP fg, [PathE (VarP xg)])) &
               prog_evalo prog q })
@@ -162,8 +162,8 @@ let prog_eval_t_simple_call_rd_ref _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, NeverWr), UnitE) &
+              xd == VarD (UnitT (Rd, NeverWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, NeverWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, NeverWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
                           ReadS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@@ -176,8 +176,8 @@ let prog_eval_t_simple_call_wr _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (NRd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@@ -190,8 +190,8 @@ let prog_eval_t_simple_call_wr_rd _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (NRd, MayWr), UnitE) &
+              xd == VarD (UnitT (NRd, MayWr)) &
-              yd == VarD (RefT (Rf, UnitT (NRd, MayWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (NRd, MayWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
                           SeqS (WriteS (DerefP (VarP 0)),
                                 ReadS (DerefP (VarP 0)))) &
@@ -205,8 +205,8 @@ let prog_eval_t_simple_call_fbd_wr _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, MayWr), UnitE) &
+              xd == VarD (UnitT (Rd, MayWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, MayWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, MayWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@@ -219,8 +219,8 @@ let prog_eval_t_simple_call_ref_wr _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (NRd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@@ -233,8 +233,8 @@ let prog_eval_t_simple_call_ref_fbd_wr _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@@ -248,8 +248,8 @@ let prog_eval_t_simple_call_ref_wr_with_fix _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (NRd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (NRd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (NRd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@@ -265,8 +265,8 @@ let prog_eval_t_call_in_call _ = show(answer) (Stream.take (run q
               yg == Nat.s xg &
               fg == Nat.s yg &
               f2g == Nat.s fg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               f2d == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
@@ -283,8 +283,8 @@ let prog_eval_t_call_in_call_rec _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (NRd, AlwaysWr)))],
                           SeqS (CallS (VarP fg, [PathE (VarP 0)]),
                                 WriteS (DerefP (VarP 0)))) &
@@ -300,8 +300,8 @@ let prog_eval_t_fix_call_after_call _ = show(answer) (Stream.take (run q
               yg == Nat.s xg &
               fg == Nat.s yg &
               f2g == Nat.s fg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               f2d == FunD ([(Mode (In, Out), RefT (Rf, UnitT (NRd, AlwaysWr)))],
@@ -318,8 +318,8 @@ let prog_eval_t_call_with_glob_usage _ = show(answer) (Stream.take (run q
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Cp, UnitT (Rd, NeverWr)))],
                           SeqS (WriteS (VarP xg),
                                 ReadS (DerefP (VarP 0)))) &
@@ -337,10 +337,10 @@ let prog_eval_t_call_with_rd_wr_2_args _ = show(answer) (Stream.take (run q
               x2g == Nat.s yg &
               y2g == Nat.s x2g &
               fg == Nat.s y2g &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
-              x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              x2d == VarD (UnitT (Rd, AlwaysWr)) &
-              y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) &
+              y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (Rf, UnitT (Rd, NeverWr)));
                            (Mode (In, NOut), RefT (Rf, UnitT (NRd, AlwaysWr)))],
                           SeqS (ReadS (DerefP (VarP 0)),
@@ -375,14 +375,14 @@ let prog_eval_t_call_with_dif_mods_cp _ = show(answer) (Stream.take (run q
               x4g == Nat.s y3g &
               y4g == Nat.s x4g &
               fg == Nat.s y4g &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
-              x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              x2d == VarD (UnitT (Rd, AlwaysWr)) &
-              y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) &
+              y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
-              x3d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              x3d == VarD (UnitT (Rd, AlwaysWr)) &
-              y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x3g) &
+              y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
-              x4d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              x4d == VarD (UnitT (Rd, AlwaysWr)) &
-              y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x4g) &
+              y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               seqo [ReadS (DerefP (VarP 1));
                     ReadS (DerefP (VarP 3));
                     WriteS (DerefP (VarP 1));
@@ -434,14 +434,14 @@ let prog_eval_t_call_with_dif_mods_rf _ = show(answer) (Stream.take (run q
               x4g == Nat.s y3g &
               y4g == Nat.s x4g &
               fg == Nat.s y4g &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
-              x2d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              x2d == VarD (UnitT (Rd, AlwaysWr)) &
-              y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x2g) &
+              y2d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
-              x3d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              x3d == VarD (UnitT (Rd, AlwaysWr)) &
-              y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x3g) &
+              y3d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
-              x4d == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              x4d == VarD (UnitT (Rd, AlwaysWr)) &
-              y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE x4g) &
+              y4d == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               seqo [ReadS (DerefP (VarP 1));
                     ReadS (DerefP (VarP 3));
                     WriteS (DerefP (VarP 2));
@@ -477,8 +477,8 @@ let prog_cp_cap_synt_t_simple_call_ref_wr _ = show(answerCpCap) (Stream.take (ru
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@@ -492,8 +492,8 @@ let prog_cp_cap_synt_t_simple_call_ref_wr' _ = show(answerCpCap) (Stream.take (r
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (rd_cap, wr_cap)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], CallS (VarP fg, [PathE (VarP yg)])) &
@@ -506,8 +506,8 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr _ = show(answerCpCap) (Stream.take
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (NRd, AlwaysWr)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@@ -522,8 +522,8 @@ let prog_cp_cap_synt_t_simple_call_ref_fbd_wr' _ = show(answerCpCap) (Stream.tak
               globals_min_ido xg &
               yg == Nat.s xg &
               fg == Nat.s yg &
-              xd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xd == VarD (UnitT (Rd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               fd == FunD ([(Mode (In, NOut), RefT (q, UnitT (rd_cap, wr_cap)))],
                           WriteS (DerefP (VarP 0))) &
               prog == Prg ([xd; yd; fd], SeqS (CallS (VarP fg, [PathE (VarP yg)]),
@@ -561,14 +561,14 @@ let prog_eval_t_presentation_simple_tp _ = show(answer) (Stream.take (run q
               wg == Nat.s fg &
               gg == Nat.s wg &
               rg == Nat.s gg &
-              xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xbd == VarD (UnitT (Rd, AlwaysWr)) &
-              xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) &
+              xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
-              ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              ybd == VarD (UnitT (Rd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
-              zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              zbd == VarD (UnitT (Rd, AlwaysWr)) &
-              zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) &
+              zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
-              kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              kbd == VarD (UnitT (Rd, AlwaysWr)) &
-              kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) &
+              kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               seqo [ReadS (DerefP (VarP 0));
                     WriteS (DerefP (VarP 0));
                     ReadS (DerefP (VarP 1))] fstmts &
@@ -635,14 +635,14 @@ let prog_synt_t_presentation_simple_tp _ = show(answerCpCapList) (Stream.take (r
               wg == Nat.s fg &
               gg == Nat.s wg &
               rg == Nat.s gg &
-              xbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              xbd == VarD (UnitT (Rd, AlwaysWr)) &
-              xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE xbg) &
+              xd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
-              ybd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              ybd == VarD (UnitT (Rd, AlwaysWr)) &
-              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE ybg) &
+              yd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
-              zbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              zbd == VarD (UnitT (Rd, AlwaysWr)) &
-              zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE zbg) &
+              zd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
-              kbd == VarD (UnitT (Rd, AlwaysWr), UnitE) &
+              kbd == VarD (UnitT (Rd, AlwaysWr)) &
-              kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr)), RefE kbg) &
+              kd == VarD (RefT (Rf, UnitT (Rd, AlwaysWr))) &
               seqo [ReadS (DerefP (VarP 0));
                     WriteS (DerefP (VarP 0));
                     ReadS (DerefP (VarP 1))] fstmts &
@@ -792,32 +792,27 @@ let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q
               timeE == UnitE &
               requestE == TupleE [RefE userVID; RefE dataVID; RefE timeVID] &
 
-              fresh data_p0, data_p1, time_p,
+              fresh data_p, time_p,
-                    user_id_p, user_name_p, user_surname_p in
+                    user_id_p, user_name_p in
-              access_deref_accesso 0 1 0 data_p0 &
+              deref_accesso 1 0 data_p &
-              access_deref_accesso 1 1 0 data_p1 &
               deref_accesso 2 0 time_p &
               access_deref_accesso 0 0 0 user_id_p &
               access_deref_accesso 1 0 0 user_name_p &
-              access_deref_accesso 2 0 0 user_surname_p &
+              seqo [ReadS data_p;
-              seqo [ReadS data_p0;
+                    WriteS data_p;
-                    ReadS data_p1;
-                    WriteS data_p0;
-                    WriteS data_p1;
-
                     ReadS user_name_p;
                     WriteS user_name_p] sendBranchStmts &
-              seqo [sendBranchStmts; (* TMP *)
+              seqo [ChoiceS (sendBranchStmts, SkipS);
-                    (* TODO: FIXME *)
-                    (* ChoiceS (sendBranchStmts, SkipS); *)
                     WriteS time_p;
 
-                    ReadS data_p0;
+                    ReadS (VarP 0)
-                    ReadS data_p1;
+                    (* ReadS data_p0; *)
-                    ReadS time_p;
+                    (* ReadS data_p1; *)
-                    ReadS user_id_p;
+                    (* ReadS time_p; *)
-                    ReadS user_name_p;
+                    (* ReadS user_id_p; *)
-                    ReadS user_surname_p] sendStmts &
+                    (* ReadS user_name_p; *)
+                    (* ReadS user_surname_p *)
+              ] sendStmts &
               (* sendStmts == SkipS & *)
               sendD == FunD ([(Mode (In, NOut), requestArgsT)], sendStmts) &
 
@@ -828,18 +823,15 @@ let prog_eval_t_presentation_complex_tp _ = show(answer) (Stream.take (run q
               seqo [
                     CallS (VarP sendFID, [PathE (VarP requestVID)]);
                     WriteS time_gp;
-                    (* TODO: FIXME *)
+                    ChoiceS (ReadS user_name_gp,
-                    (* ChoiceS (ReadS user_name_gp, *)
+                             ReadS user_surname_gp);
-                             (* ReadS user_surname_gp); *)
-                    ReadS user_name_gp; (* TMP *)
-                    ReadS user_surname_gp; (* TMP *)
                     ReadS time_gp
                   ] stmts &
               prog == Prg ([
-                            VarD (userT, userE);
+                            VarD userT;
-                            VarD (dataT, dataE);
+                            VarD dataT;
-                            VarD (timeT, timeE);
+                            VarD timeT;
-                            VarD (requestT, requestE);
+                            VarD requestT;
                             sendD
                             ],
                            stmts
@@ -884,12 +876,9 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take (
               access_deref_accesso 2 0 0 user_surname_p &
               seqo [ReadS data_p;
                     WriteS data_p;
-
                     ReadS user_name_p;
                     WriteS user_name_p] sendBranchStmts &
-              seqo [sendBranchStmts; (* TMP *)
+              seqo [ChoiceS (sendBranchStmts, SkipS);
-                    (* TODO: FIXME *)
-                    (* ChoiceS (sendBranchStmts, SkipS); *)
                     WriteS time_p;
                     ReadS (VarP 0)
               ] sendStmts &
@@ -903,18 +892,16 @@ let prog_synt_t_presentation_complex_tp _ = show(answerCpCapList) (Stream.take (
               seqo [
                     CallS (VarP sendFID, [PathE (VarP requestVID)]);
                     WriteS time_gp;
-                    (* TODO: FIXME *)
+                    ChoiceS (ReadS user_name_gp,
-                    (* ChoiceS (ReadS user_name_gp, *)
+                             ReadS user_surname_gp);
-                             (* ReadS user_surname_gp); *)
-                    ReadS user_name_gp; (* TMP *)
                     ReadS user_surname_gp; (* TMP *)
                     ReadS time_gp
                   ] stmts &
               prog == Prg ([
-                            VarD (userT, userE);
+                            VarD userT;
-                            VarD (dataT, dataE);
+                            VarD dataT;
-                            VarD (timeT, timeE);
+                            VarD timeT;
-                            VarD (requestT, requestE);
+                            VarD requestT;
                             sendD
                             ],
                            stmts
@@ -1031,9 +1018,8 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
                     ReadS sb_access3]
                    sendFBranch &
               seqo [ChoiceS (sendFBranch, SkipS);
-                    WriteS (AccessP (VarP 0, 4));
+                    WriteS (VarP 0);
-                    (* TODO: read all the substructure ?? *)
+                    ReadS (VarP 0)]
-                    ReadS (AccessP (VarP 0, 4)) (*rdS v0*)] (* FIXME: TMP, parial read, should be full *)
                    sendF &
 
               fresh sa_access0, sa_access1, sa_access2, sa_access3 in
@@ -1041,7 +1027,7 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
               access_deref_accesso 1 1 0 sa_access1 &
               access_deref_access_deref_accesso 0 0 0 0 sa_access2 &
               access_deref_accesso 0 1 0 sa_access3 &
-              seqo [WriteS (AccessP (VarP 0, 4)) (*wrS v0*); (* FIXME: TMP, parial write, should be full *)
+              seqo [WriteS (VarP 0);
                     CallS (VarP sendID, [PathE (VarP 0)]);
                     CallS (VarP get_version_idID, [PathE (VarP 0)]);
                     CallS (VarP updated_versionID, [PathE (VarP 0)]);
@@ -1055,13 +1041,13 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
                    send_allF &
 
               prog == Prg ([
-                VarD (user_utilsT, user_utilsE);
+                VarD user_utilsT;
-                VarD (user_infoT, user_infoE);
+                VarD user_infoT;
-                VarD (userT, userE);
+                VarD userT;
-                VarD (versionT, versionE);
+                VarD versionT;
-                VarD (utilsT, utilsE);
+                VarD utilsT;
-                VarD (uT_r_aw, UnitE); (* data *)
+                VarD uT_r_aw; (* data *)
-                VarD (requestT, requestE);
+                VarD requestT;
                 FunD ([moded_requestT], get_version_idF);
                 FunD ([moded_requestT], updated_versionF);
                 FunD ([moded_requestT], sendF);
@@ -1317,8 +1303,7 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
                    sendFBranch &
               seqo [ChoiceS (sendFBranch, SkipS);
                     WriteS (AccessP (VarP 0, 4));
-                    (* TODO: read all the substructure ?? *)
+                    ReadS (VarP 0)]
-                    ReadS (AccessP (VarP 0, 4)) (*rdS v0*)] (* FIXME: TMP, parial read, should be full *)
                    sendF &
 
               fresh sa_access0, sa_access1, sa_access2, sa_access3 in
@@ -1326,11 +1311,10 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
               access_deref_accesso 1 1 0 sa_access1 &
               access_deref_access_deref_accesso 0 0 0 0 sa_access2 &
               access_deref_accesso 0 1 0 sa_access3 &
-              seqo [WriteS (AccessP (VarP 0, 4)) (*wrS v0*); (* FIXME: TMP, parial write, should be full *)
+              seqo [WriteS (AccessP (VarP 0, 4));
                     CallS (VarP sendID, [PathE (VarP 0)]);
                     CallS (VarP get_version_idID, [PathE (VarP 0)]);
                     CallS (VarP updated_versionID, [PathE (VarP 0)]);
-                    (* TODO: read all the substructure ?? *)
                     WriteS sa_access0;
                     WriteS sa_access1;
                     ChoiceS (
@@ -1352,13 +1336,13 @@ let prog_synt_compl_test_send _ = show(answerCpCapList) (Stream.take (run q
               (* [gvi_c0; gvi_c1; gvi_c2; gvi_c3; gvi_c4; gvi_c5] & *)
 
               prog == Prg ([
-                VarD (user_utilsT, user_utilsE);
+                VarD user_utilsT;
-                VarD (user_infoT, user_infoE);
+                VarD user_infoT;
-                VarD (userT, userE);
+                VarD userT;
-                VarD (versionT, versionE);
+                VarD versionT;
-                VarD (utilsT, utilsE);
+                VarD utilsT;
-                VarD (uT_r_aw, UnitE); (* data *)
+                VarD uT_r_aw; (* data *)
-                VarD (requestT, requestE);
+                VarD requestT;
                 (* FunD ([mrT'], get_version_idF); *)
                 (* FunD ([mrT'], updated_versionF); *)
                 (* FunD ([mrT'], sendF); *)