struct: analyzer: remove old commented tests, etc.

model_with_structures/analyzer.ml

@@ -73,6 +73,8 @@ struct
              | RefV of memid
              | TupleV of value list
 
+  type revpath = VarRP | DerefRP of revpath | AccessRP of revpath * data
+
   (* TODO: any additional difference between rvalue and lvalue now ?? *)
 
   (* --- *)
@@ -154,13 +156,19 @@ struct
     | DerefP p -> pathvar p
     | AccessP (p, _) -> pathvar p
 
+  let rec pathrev (p : path) (acc : revpath) : revpath = match p with
+    | VarP x -> acc
+    | DerefP p -> pathrev p @@ DerefRP acc
+    | AccessP (p, i) -> pathrev p @@ AccessRP (acc, i)
+
   let rec pathtype (types : types) (p : path) : atype = match p with
     | VarP x -> types_assoc x types
     | DerefP p -> (match pathtype types p with
                     | RefT (_, t) -> t
                     | _ -> raise @@ Typing_error "pathtype: deref")
     | AccessP (p, id) -> match pathtype types p with
-                           | TupleT ts -> (List.nth ts id)
+                           | TupleT ts -> (* FIXME TMP Printf.printf "pathtype access sz=%i id=%i\n" (List.length ts) id; *)
+                                          (List.nth ts id)
                            | _ -> raise @@ Typing_error "pathtype: access"
 
   let rec pathval (mem :  mem) (vals : vals) (p : path) : value = match p with
@@ -174,7 +182,8 @@ struct
                     | RefV id -> mem_get mem id
                     | _ -> raise @@ Typing_error "pathval: deref")
     | AccessP (p, id) -> match pathval mem vals p with
-                           | TupleV vs -> (List.nth vs id)
+                           | TupleV vs -> (* FIXME TMP Printf.printf "pathval access sz=%i id=%i\n" (List.length vs) id; *)
+                                          (List.nth vs id)
                            | _ -> raise @@ Typing_error "pathval: access"
 
   (* --- eval rules --- *)
@@ -208,11 +217,13 @@ struct
 
   (* - value update *)
 
-  let rec valupd (mem : mem) (v : value) (p : path) (b : value) : mem * value = match p, v with
-    | VarP x, _ -> (mem, b)
-    | DerefP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in
+  let rec valupd (mem : mem) (v : value) (p : revpath) (b : value) : mem * value = match p, v with
+    | VarRP, _ -> (mem, b)
+    | DerefRP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in
                             (mem_set mem' id v', RefV id)
-    | AccessP (p, id), TupleV vs -> let (mem', v') = valupd mem (List.nth vs id) p b in
+    | AccessRP (p, id), TupleV vs -> let (mem', v') = (* FIXME TMP Printf.printf "vs size=%i id=%i\n" (List.length vs) id; *)
+                                                      valupd mem (List.nth vs id) p b in
+                                     (* FIXME TMP Printf.printf "before return\n"; *)
                                      (mem', TupleV (list_replace vs id v'))
     | _, _ -> raise @@ Typing_error "valupd"
 
@@ -316,7 +327,7 @@ struct
         let folder = fun (mem, vs') t u v ->
           let (mem', v') = valspoil mem v t u m c in (mem', v' :: vs') in
         let (mem', vs') = list_foldl3 folder (mem, []) ts us vs in
-        (mem', TupleV vs')
+        (mem', TupleV (List.rev vs'))
     | _, _, _ ->  raise @@ Typing_error "valspoil"
 
   (* full spoil *)
@@ -328,8 +339,9 @@ struct
     let b = pathval mem vals p in (* subvalue in var *)
     let t' = pathtype types p in (* type of subvalue *)
     let (mem', b') = valspoil mem b t t' m Cp in (* spoil subvalue *)
-    (* TODO: FIXME: why copy (Cp)? *)
-    let (mem'', v'') = valupd mem' (mem_get mem' id) p b' in (* set subvalue into var *)
+    (* TODO: FIXME: why copy (Cp)? maybe sometimes use top-level capability ? *)
+    let pi = pathrev p VarRP in
+    let (mem'', v'') = valupd mem' (mem_get mem' id) pi b' in (* set subvalue into var *)
     mem_set mem'' id v''
 
   let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
@@ -399,8 +411,11 @@ struct
                        then raise @@ Eval_error "write: write tag"
                        else let x = pathvar p in
                             let id = vals_assoc x vals in
-                            let (mem', v') = valupd mem (mem_get mem id) p ZeroV in
+                            let pi = pathrev p VarRP in
+                            let (mem', v') = valupd mem (mem_get mem id) pi ZeroV in
                             (mem_set mem' id v', types, vals, visited)
+                     | RefT _ -> raise @@ Eval_error "write: ref type"
+                     | TupleT _ -> raise @@ Eval_error "write: tuple type"
                      | _ -> raise @@ Eval_error "write: type")
     | ReadS p -> if pathval mem vals p == SmthV || pathval mem vals p == BotV 
                  then raise @@ Eval_error "read: spoiled value"
@@ -867,6 +882,8 @@ struct
 
   (* - complex tests *)
 
+  (* 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 *)
@@ -895,38 +912,33 @@ struct
       let sendID = vg9 in
       let send_allID = vg10 in
       let get_version_idF = FunD ([moded requestT],
-        (* (rdS @@ access 1 @@ drf @@ access 0 v0) |. skp) in *)
-         skp) in
-      (* TODO: real op paths *)
+        (rdS @@ access 0 @@ drf @@ access 1 v0) |. skp) in
       let updated_versionF = FunD ([moded requestT],
-        (* (rdS @@ access 2 @@ drf @@ access 0 v0) #. *)
+        (rdS @@ access 0 @@ drf @@ access 2 v0) #.
         (* TODO: read all the substructure ?? *)
-        (* (rdS @@ access 1 @@ drf @@ access 0 v0) #. *)
-        (* (rdS @@ access 1 @@ drf @@ access 1 v0)) in *)
-         skp) in
+        (rdS @@ access 0 @@ drf @@ access 1 v0) #.
+        (rdS @@ access 1 @@ drf @@ access 1 v0)) in
       let sendF = FunD ([moded requestT],
-        (* (( *)
-           (* (wrS @@ access 2 @@ drf @@ access 0 v0) #. *)
-           (* (rdS @@ access 3 @@ drf v0) #. *)
-           (* (wrS @@ access 3 @@ drf v0) #. *)
-           (* (rdS @@ access 0 @@ drf @@ access 1 @@ drf @@ access 0 v0) *)
-         (* ) |. skp) #. *)
-         (* (wrS @@ access 4 v0) #. *)
+        ((
+           (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 *) *)
-         skp) in
+         (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]) #. *)
+        (callS sendID [pE v0]) #.
+        (callS get_version_idID [pE v0]) #.
+        (callS updated_versionID [pE v0]) #.
         (* TODO: read all the substructure ?? *)
-        (wrS @@ access 1 @@ drf @@ access 0 v0) #.
-        (* (wrS @@ access 1 @@ drf @@ access 1 v0) #. *)
+        (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 2 @@ drf @@ access 0 v0))) in *)
-         skp) in
+        ((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;
@@ -940,315 +952,11 @@ struct
         updated_versionF;
         sendF;
         send_allF
-        (* TODO: var def *)
       ],
       callS send_allID [pE varID]
     );
     Printf.printf "done!";
     [%expect {| done! |}]
 
-  (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
-
-  (* --- tests --- *)
-
-  (* let rwi_value : tag = (Rd, AlwaysWr, Cp, In, NOut) *)
-  (* let rmwi_value : tag = (Rd, MayWr, Cp, In, NOut) *)
-  (* let ri_value : tag = (Rd, NeverWr, Cp, In, NOut) *)
-  (* let wi_value : tag = (NRd, AlwaysWr, Cp, In, NOut) *)
-  (* let mwi_value : tag = (NRd, MayWr, Cp, In, NOut) *)
-  (* let i_value : tag = (NRd, NeverWr, Cp, In, NOut) *)
-  (* let rwi_ref : tag = (Rd, AlwaysWr, Rf, In, NOut) *)
-  (* let rmwi_ref : tag = (Rd, MayWr, Rf, In, NOut) *)
-  (* let ri_ref : tag = (Rd, NeverWr, Rf, In, NOut) *)
-  (* let wi_ref : tag = (NRd, AlwaysWr, Rf, In, NOut) *)
-  (* let mwi_ref : tag = (NRd, MayWr, Rf, In, NOut) *)
-  (* let i_ref : tag = (NRd, NeverWr, Rf, In, NOut) *)
-
-  (* >> tests without functions *)
-
-  (* let%expect_test "empty" = *)
-    (* eval_prog ([], ([], [])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "ref param in main failure" = *)
-    (* try (eval_prog ([], ([i_ref], [])); *)
-         (* [%expect.unreachable]) *)
-    (* with Ref_rvalue_argument id -> Printf.printf "%i" id; *)
-    (* [%expect {| 0 |}] *)
-
-  (* let%expect_test "read empty args" = *)
-    (* try (eval_prog ([], ([], [Read 0])); *)
-         (* [%expect.unreachable]) *)
-    (* with Not_found -> Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "write empty args" = *)
-    (* try (eval_prog ([], ([], [Write 0])); *)
-         (* [%expect.unreachable]) *)
-    (* with Not_found -> Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "simple write" = *)
-    (* eval_prog ([], ([wi_value], [Write 0])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "simple read" = (* NOTE: should not work with read-before-write check*) *)
-    (* eval_prog ([], ([ri_value], [Read 0])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "multiple read & write" = *)
-    (* eval_prog ([], ([rwi_value], [Write 0; Read 0; Write 0; Write 0; Read 0; Read 0])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "multiple read & write, multiple args" = *)
-    (* eval_prog ([], ([wi_value; wi_value; wi_value], [Write 0; Read 0; Write 1; Write 0; Write 2; Read 1; Write 2; Read 0; Read 2])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "main, access out of range" = *)
-    (* try(eval_prog ([], ([wi_value], [Write 0; Read 5 ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Not_found -> Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "main, access out of range" = *)
-    (* try(eval_prog ([], ([wi_value], [Write 0; Write 5 ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Not_found -> Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* >> tests with one function *)
-
-  (* let%expect_test "simple function call with value arg" = *)
-    (* eval_prog ([([wi_value], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "simple function call with ref arg" = *)
-    (* eval_prog ([([wi_ref], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "function with value arg & read" = *)
-    (* eval_prog ([([wi_value], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Read 0 ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* --- *)
-
-  (* let%expect_test "function with ref arg & read" = *)
-    (* try (eval_prog ([([rwi_ref], [Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Read 0 ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
-    (* [%expect {| 0 |}] *)
-
-  (* let%expect_test "function with ref arg & call twice" = *)
-    (* try (eval_prog ([([rwi_ref], [Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Call (0, [0]) ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
-    (* [%expect {| 0 |}] *)
-
-  (* NOTE: behaviour is fixed with new capabilities *)
-  (* let%expect_test "function with ref arg, write first & call twice" = *)
-    (* eval_prog ([([wi_ref], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Call (0, [0]) ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-
-  (* let%expect_test "function with ref arg & read, write" = *)
-    (* try (eval_prog ([([rwi_ref], [Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Read 0; Write 0 ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
-    (* [%expect {| 0 |}] *)
-
-  (* let%expect_test "function with ref arg & write, read" = *)
-    (* eval_prog ([([rwi_ref], [Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]); Write 0; Read 0 ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "function with ref arg, no write inside & read" = *)
-    (* eval_prog ([([ri_ref], [Read 0; Read 0])], ([wi_value], [Write 0; Call (0, [0]); Read 0 ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* --- *)
-
-  (* let%expect_test "function with value arg, read out of range" = *)
-    (* try(eval_prog ([([ri_ref], [Read 0; Read 1])], ([wi_value; i_value], [Write 0; Call (0, [0]); Read 0 ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Not_found -> Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "function with ref arg, read out of range" = *)
-    (* try(eval_prog ([([ri_ref], [Read 0; Read 1])], ([wi_value; i_value], [Write 0; Call (0, [0]); Read 0 ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Not_found -> Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "function with value arg, write out of range" = *)
-    (* try(eval_prog ([([rwi_value], [Read 0; Write 1])], ([wi_value; i_value], [Write 0; Call (0, [0]); Read 0 ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Not_found -> Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "function with value arg, call out of range" = *)
-    (* try(eval_prog ([([ri_value], [Read 0])], ([wi_value; i_value], [Write 0; Call (0, [2]); Read 0 ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Not_found -> Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* --- *)
-
-  (* let%expect_test "function with ref & value args, no write inside & read" = *)
-    (* eval_prog ( *)
-      (* [([ri_ref; ri_value], [Read 0; Read 1])], *)
-      (* ([wi_value; wi_value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "function with ref & value args, write value inside & read" = *)
-    (* eval_prog ( *)
-      (* [([ri_ref; rwi_value], [Read 0; Read 1; Write 1; Read 1])], *)
-      (* ([wi_value; wi_value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "function with ref & value args, write both inside & read" = *)
-    (* try (eval_prog ( *)
-      (* [([rwi_ref; rwi_value],[Read 0; Read 1; Write 0; Write 1; Read 1])], *)
-      (* ([wi_value; wi_value], [Write 0; Write 1; Call (0, [0; 1]); Read 0; Read 1 ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
-    (* [%expect {| 0 |}] *)
-
-  (* --- *)
-
-  (* let%expect_test "function with ref two same ref args, read both & read" = *)
-    (* eval_prog ( *)
-      (* [([ri_ref; ri_ref],[Read 0; Read 1; Read 1])], *)
-      (* ([wi_value], [Write 0; Call (0, [0; 0]); Read 0 ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "function with ref two same ref args, read both & nothing" = *)
-    (* eval_prog ( *)
-      (* [([ri_ref; ri_ref],[Read 0; Read 1; Read 1])], *)
-      (* ([wi_value], [Write 0; Call (0, [0; 0]); ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "function with ref & copy of the same arg, read & write both & nothing" = *)
-    (* eval_prog ( *)
-      (* [([rwi_ref; rwi_value],[Read 0; Read 1; Write 0; Write 1; Read 1])], *)
-      (* ([wi_value], [Write 0; Call (0, [0; 0]); ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "function with copy & ref of the same arg, read & write both & nothing" = *)
-    (* eval_prog ( *)
-      (* [([rwi_value; rwi_ref],[Read 0; Read 1; Write 0; Write 1; Read 1])], *)
-      (* ([wi_value], [Write 0; Call (0, [0; 0]); ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* TODO: FIXME: now correct (use state before for mem check), is this good ?, proper way to fix ? *)
-  (* let%expect_test "function with ref two same ref args, read & write both, error" = *)
-    (* try ( *)
-      (* eval_prog ( *)
-      (* [([rwi_ref; rwi_ref],[Read 0; Read 1; Write 0; Write 1; Read 1])], *)
-      (* ([wi_value], [Write 0; Call (0, [0; 0]); ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* >> tests with several functions *)
-
-  (* let%expect_test "two functions with ref arg, read func -> write func" = *)
-    (* eval_prog ( *)
-      (* [([ri_ref], [Read 0]); ([wi_ref], [Write 0])], *)
-      (* ([wi_value], [Write 0; Call (0, [0]); Read 0; Call (1, [0]) ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "two functions with ref arg, write func -> read func" = *)
-    (* try (eval_prog ( *)
-      (* [([ri_ref], [Read 0]); ([wi_ref], [Write 0])], *)
-      (* ([wi_value], [Write 0; Call (1, [0]); Call (0, [0]) ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
-    (* [%expect {| 0 |}] *)
-
-  (* let%expect_test "two functions: ref arg after value arg" = *)
-    (* eval_prog ( *)
-      (* [([rwi_ref], [Read 0; Write 0]); ([rwi_value], [Read 0; Write 0])], *)
-      (* ([wi_value], [Write 0; Call (1, [0]); Read 0; Call (0, [0]) ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "two functions: value arg after spoiled ref arg" = *)
-    (* try (eval_prog ( *)
-      (* [([rwi_ref], [Read 0; Write 0]); ([rwi_value], [Read 0; Write 0])], *)
-      (* ([wi_value], [Write 0; Call (0, [0]); Call (1, [0]) ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Incorrect_memory_access id -> Printf.printf "%i" id; *)
-    (* [%expect {| 0 |}] *)
-
-  (* --- *)
-
-  (* let%expect_test "simple function call with value arg, const cast error" = *)
-    (* try (eval_prog ([([ri_value], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Incorrect_const_cast id -> Printf.printf "%i" id; *)
-    (* [%expect {| 0 |}] *)
-
-  (* let%expect_test "simple function call with ref arg, const cast error" = *)
-    (* try (eval_prog ([([ri_ref], [Write 0; Read 0; Write 0])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Incorrect_const_cast id -> Printf.printf "%i" id; *)
-    (* [%expect {| 0 |}] *)
-
-  (* let%expect_test "simple function call with value arg, const cast ok" = *)
-    (* eval_prog ([([ri_value], [Read 0])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "simple function call with ref arg, const cast ok" = *)
-    (* eval_prog ([([ri_ref], [Read 0])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* --- *)
-
-  (* let%expect_test "simple function call with arg, recursive calls" = *)
-    (* eval_prog ([([rwi_value], [Write 0; Read 0; Write 0; Call (0, [0])])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* --- *)
-
-  (* TODO: out arguments test, etc. *)
-
-  (* --- *)
-
-  (* TODO: more Combine statement tests *)
-
-  (* let%expect_test "simple function call with value arg and choice, rw" = *)
-    (* eval_prog ([([wi_value], [Choice ([Write 0; Read 0], [Write 0]); Read 0])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "simple function call with ref arg and choice, rw" = *)
-    (* try (eval_prog ([([ri_ref], [Choice ([Read 0], [Write 0])])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
-         (* [%expect.unreachable]) *)
-    (* with Incorrect_const_cast id -> Printf.printf "%i" id; *)
-    (* [%expect {| 0 |}] *)
-
-  (* let%expect_test "simple function call with ref arg and choice, rr" = *)
-    (* eval_prog ([([ri_ref], [Choice ([Read 0], [Read 0; Read 0])])], ([wi_value], [Write 0; Call (0, [0]) ])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
+  (* TODO: version with more optimal modifiers *)
 end

model_with_structures/model.typ

@@ -153,6 +153,7 @@
 
 #let deepValue = `deepvalue`
 #let value = `value`
+#let revpath = $#[`path`]_#[`rev`]$
 
 #bnf(
   Prod(
@@ -177,12 +178,22 @@
       Or[$[value+]$][tuple value] // `Prod`
     }
   ),
+  Prod(
+    revpath,
+    {
+      Or[$\# .$][value by itself]
+      Or[$rf revpath$][reference to value]
+      Or[$n . revpath$][tuple with value as $n$-th element]
+    }
+  ),
 )
 
 #deepValue - полное значение, #value - слой значения, привязан к конкретной памяти $mu$
 
 Значения, могут лежать в переменных и передаваться как аргументы функций (то, во что вычисляется $expr$)
 
+$revpath$ - путь в обратную сторону, используется для обновления значений
+
 $v in value$ - произвольное значение
 
 Получение #deepValue по #value:
@@ -229,7 +240,7 @@ $sigma : envt := X -> type, space types : envt$ - #[ типы значений
 // $DD : X -> decl$ - глобальные определения, частично определённая функция
 
 // $d in decl, $
-$s in stmt, f in X, x in X, a in X$
+$s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
 
 === Path Accessors
 
@@ -241,6 +252,7 @@ $s in stmt, f in X, x in X, a in X$
 #let arrmu = $attach(->, br: mu)$
 
 #let arrpath = $xarrowSquiggly(space)_path$
+#let arrrevpath = $xarrowSquiggly(space)_#[rev path]$
 
 #let ttype = $attach(tack.r, br: type)$
 #let tmode = $attach(tack.r, br: mode)$
@@ -248,7 +260,7 @@ $s in stmt, f in X, x in X, a in X$
 #let val = `val`
 #let tval = $attach(tack.r, br: val)$
 
-- #[ Конструирование путей по переменой
+- #[ Соответствующая пути переменная
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
@@ -263,7 +275,7 @@ $s in stmt, f in X, x in X, a in X$
     name: [ reference path],
 
     $p arrpath x$,
-    $rf p arrpath x$,
+    $* p arrpath x$,
   )
 ))
 #align(center, prooftree(
@@ -278,6 +290,36 @@ $s in stmt, f in X, x in X, a in X$
 ))
 ]
 
+- #[ Обращение пути
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ variable path],
+
+    $@x arrrevpath^pi pi$,
+  )
+))
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ reference path],
+
+    $p arrrevpath^(rf pi) pi'$,
+    $*p arrrevpath^pi pi'$,
+  )
+))
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ tuple access path],
+
+    $p arrrevpath^(i.pi) pi'$,
+
+    $p.i arrrevpath^pi pi'$,
+  )
+))
+]
+
 - #[ Получение типа поля
 #align(center, prooftree(
   vertical-spacing: 4pt,
@@ -509,16 +551,6 @@ $s in stmt, f in X, x in X, a in X$
 
 #let modify = `modify`
 
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ modify trivial value],
-
-//     $v in {0, \#, bot}$,
-//     $cl v, mu cr xarrowSquiggly(cl \@ x \, b cr)_modify cl b, mu cr$,
-//   )
-// ))
-
 // TODO: add type check ??
 #align(center, prooftree(
   vertical-spacing: 4pt,
@@ -526,7 +558,7 @@ $s in stmt, f in X, x in X, a in X$
     name: [ modify end value],
 
     // $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl \@ x \, b cr)_modify cl b, mu cr$,
+    $cl v, mu cr xarrowSquiggly(cl \# . \, b cr)_modify cl b, mu cr$,
   )
 ))
 
@@ -537,8 +569,8 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ new reference copy value],
 
-    $cl mu[l], mu cr xarrowSquiggly(cl p \, b cr)_modify cl v', mu' cr$,
-    $cl rf l, mu cr xarrowSquiggly(cl *p \, b cr)_modify cl rf l, mu'[l <- v'] cr$,
+    $cl mu[l], mu cr xarrowSquiggly(cl pi \, b cr)_modify cl v', mu' cr$,
+    $cl rf l, mu cr xarrowSquiggly(cl rf pi \, b cr)_modify cl rf l, mu'[l <- v'] cr$,
   )
 ))
 
@@ -550,7 +582,7 @@ $s in stmt, f in X, x in X, a in X$
     name: [ modify tuple value],
 
     $cl v_i, mu cr xarrowSquiggly(cl p \, b cr)_modify cl v'_i, mu', cr$,
-    $cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl p.i \, b cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$,
+    $cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl i.pi \, b cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$,
   )
 ))
 
@@ -912,7 +944,8 @@ $s in stmt, f in X, x in X, a in X$
     // <- otherwise all subsequent copy capabilities will be ref (in current impl)
     // FIXME depends on parent ??
     $cl b, mu cr xarrowSquiggly(t \, t' \, m \, Copy)_spoil cl b', mu' cr$,
-    $cl mu'[l], mu' cr xarrowSquiggly(cl p \, b' cr)_modify cl v'', mu'' cr$,
+    $p arrrevpath^(\#.) pi$,
+    $cl mu'[l], mu' cr xarrowSquiggly(cl pi \, b' cr)_modify cl v'', mu'' cr$,
 
     $mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu''[l <- v'']$,
   )
@@ -1055,7 +1088,8 @@ $s in stmt, f in X, x in X, a in X$
     $w = MaybeWrite or w = AlwaysWrite$,
     $p arrpath x$,
     $l = vals[x]$,
-    $mu[l] xarrowSquiggly(cl p \, 0 cr)_modify v'$,
+    $p arrrevpath^(\#.) pi$,
+    $mu[l] xarrowSquiggly(cl pi \, 0 cr)_modify v'$,
 
     $cl types, vals, mu cr
      xarrow("WRITE" p)

model_with_structures/synthesizer.ml

@@ -105,7 +105,6 @@ struct
     (* end *)
   end
 
-  (* TODO: access: data or int ? *)
   module Path = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
@@ -174,6 +173,15 @@ struct
     ]
   end
 
+  module RevPath = struct
+    [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
+    [%%ocanren_inject
+      type nonrec ('d, 'p) t = VarRP | DerefRP of 'p | AccessRP of 'p * 'd
+      [@@deriving gt ~options:{ show; gmap }]
+      type ground = (Nat.ground, ground) t
+    ]
+  end
+
   (* --- *)
 
   module MemEnv = struct
@@ -462,6 +470,21 @@ struct
       { fresh p', _id in p == AccessP (p', _id) & pathvaro p' x }
   }
 
+  let rec pathrevo p rp rp' =
+    let open Path in
+    let open RevPath in
+    ocanren {
+      { fresh _x in
+        p == VarP _x &
+        rp == rp' } |
+      { fresh p' in
+        p == DerefP p' &
+        pathrevo p' (DerefRP rp) rp' } |
+      { fresh p', id in
+        p == AccessP (p', id) &
+        pathrevo p' (AccessRP (rp, id)) rp' }
+  }
+
   let rec pathtypeo types p tp =
     let open Path in
     let open Type in
@@ -542,33 +565,32 @@ struct
         v == TupleV vs &
         tp == TupleT tps &
         list_foldl2o valcopy_foldero (Std.pair mem []) vs tps (Std.pair mem' vs') &
-         == mem_with_vs' &
-        List.reverso vs' vs''
+        List.reverso vs' vs'' &
         mem_with_id' == Std.pair mem' (TupleV vs'') }
   }
 
   (* - value update *)
 
-  let rec valupdo mem v p b mem_with_v' =
-    let open Path in
+  (* NOTE: reversed path used *)
+  let rec valupdo mem v rp b mem_with_v' =
+    let open RevPath in
     let open Value in
     ocanren {
-      { fresh x in
-        p == VarP x &
+      { rp == VarRP &
         mem_with_v' == Std.pair mem b } |
-      { fresh p', id, v', mem_upd, v_upd, mem_with_v_upd, mem_st in
-        p == DerefP p' &
+      { fresh rp', id, v', mem_upd, v_upd, mem_with_v_upd, mem_st in
+        rp == DerefRP rp' &
         v == RefV id &
         mem_geto mem id v' &
-        valupdo mem v' p' b mem_with_v_upd &
+        valupdo mem v' rp' b mem_with_v_upd &
         Std.pair mem_upd v_upd == mem_with_v_upd &
         mem_seto mem_upd id v_upd mem_st &
         mem_with_v' == Std.pair mem_st (RefV id) } |
-      { fresh p', id, vs', v', mem_upd, v_upd, mem_with_v_upd, vs_upd in
-        p == AccessP (p', id) &
+      { fresh rp', id, vs', v', mem_upd, v_upd, mem_with_v_upd, vs_upd in
+        rp == AccessRP (rp', id) &
         v == TupleV vs' &
         list_ntho vs' id v' &
-        valupdo mem v' p' b mem_with_v_upd &
+        valupdo mem v' rp' b mem_with_v_upd &
         Std.pair mem_upd v_upd == mem_with_v_upd &
         list_replaceo vs' id v_upd vs_upd &
         mem_with_v' == Std.pair mem_upd (TupleV vs_upd) }
@@ -791,14 +813,15 @@ struct
         valspoilo mem v' tp' u' m ctp' (Std.pair mem_sp v_sp) &
         mem_seto mem_sp id' v_sp mem_set &
         mem_with_v' == Std.pair mem_set (RefV id') } |
-      { fresh tps, us, vs, mem_sp,vs_sp in
+      { fresh tps, us, vs, mem_sp, vs_sp, vs_sp' in
         tp == TupleT tps &
         u == TupleT us &
         v == TupleV vs &
         list_foldl3o (valspoil_foldero m c)
                      (Std.pair mem []) tps us vs
                      (Std.pair mem_sp vs_sp) &
-        mem_with_v' == Std.pair mem_sp (TupleV vs_sp)
+        List.reverso vs_sp vs_sp' &
+        mem_with_v' == Std.pair mem_sp (TupleV vs_sp')
       }
   }
 
@@ -807,9 +830,10 @@ struct
   let argspoilpo st m tp p mem' =
     let open StEnv in
     let open CopyCap in
+    let open RevPath in
     ocanren {
       fresh mem, types, vals, visited,
-            x, id, b, tp',
+            x, id, b, tp', rp,
             mem_sp, b_sp, v_sp, mem_upd, v_upd in
       st == StEnv (mem, types, vals, visited) &
       pathvaro p x &
@@ -818,7 +842,8 @@ struct
       pathtypeo types p tp' &
       valspoilo mem b tp tp' m Cp (Std.pair mem_sp b_sp) &
       mem_geto mem_sp id v_sp &
-      valupdo mem_sp v_sp p b_sp (Std.pair mem_upd v_upd) &
+      pathrevo p VarRP rp &
+      valupdo mem_sp v_sp rp b_sp (Std.pair mem_upd v_upd) &
       mem_seto mem_upd id v_upd mem'
   }
 
@@ -914,6 +939,7 @@ struct
     let open WriteCap in
     let open TypesEnv in
     let open ValsEnv in
+    let open RevPath in
     ocanren {
       fresh mem, types, vals, visited in
       st == StEnv (mem, types, vals, visited) &
@@ -949,7 +975,7 @@ struct
                        mem tps es mem_spoiled &
           st' == StEnv (mem_spoiled, types, vals, visited')
         } |
-        { fresh p, tp, _r, w, x, id, v,
+        { fresh p, tp, _r, w, x, id, v, rp,
                 mem_upd, v_upd, mem_set in
           s == WriteS p &
           pathtypeo types p tp &
@@ -958,7 +984,8 @@ struct
           pathvaro p x &
           vals_assoco x vals id &
           mem_geto mem id v &
-          valupdo mem v p ZeroV (Std.pair mem_upd v_upd) &
+          pathrevo p VarRP rp &
+          valupdo mem v rp ZeroV (Std.pair mem_upd v_upd) &
           mem_seto mem_upd id v_upd mem_set &
           st' == StEnv (mem_set, types, vals, visited) } |
         { fresh p in