struct: model update to use reverse paths in valupd (fix)

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)