model fixes, model for correct declarations & multiarg functions

simplest_model/model.typ

@@ -3,7 +3,7 @@
 // #import "@preview/zebraw:0.5.0": *
 // #show: zebraw
 #import "@preview/curryst:0.6.0": rule, prooftree, rule-set
-#import "@preview/xarrow:0.4.0": xarrow
+#import "@preview/xarrow:0.4.0": xarrow, xarrowDashed
 
 = Формальная модель используемого языка
 
@@ -11,78 +11,81 @@
 
 #h(10pt)
 
+#let tag = `tag`
+#let value = `value`
+#let stmt = `stmt`
+#let decl = `decl`
+#let prog = `prog`
 #bnf(
   Prod(
     `tag`,
     {
-      Or[`Ref`][pass by reference]
-      Or[`Value`][copy]
+      Or[$ast.basic$][pass by reference]
+      Or[$!$][copy]
     }
   ),
   Prod(
     `value`,
     {
-      Or[`Unit`][cell with some value]
-      Or[`Bot`][spoiled cell]
-    }
-  ),
-  Prod(
-    `arg`,
-    {
-      Or[`RValue`][new value, no associated variable]
-      Or[`LValue` $d$][value from some variable]
+      Or[$0$][cell with some value]
+      Or[$bot$][spoiled cell]
     }
   ),
+  // Prod(
+  //   `arg`,
+  //   {
+  //     Or[$0$][new value, no associated variable]
+  //     Or[$ amp d$][value from some variable]
+  //   }
+  // ),
   Prod(
     `stmt`,
     {
-      Or[$f($`args`$)$][call function by id]
-      Or[`write` $d$][write to variable]
-      Or[`read` $d$][read from variable]
+      Or[`CALL` $f space overline(x)$][call function by id]
+      Or[`WRITE` $x$][write to variable]
+      Or[`READ` $x$][read from variable]
     }
   ),
   Prod(
-    `body`,
+    `decl`,
     {
-      Or[`body` `stmt`][with statement]
-      Or[$epsilon$][empty body]
-    }
-  ),
-  Prod(
-    `fun_decl`,
-    {
-      Or[`body`][function body]
-      Or[`tag` `fun_decl`][with argument pass strategy annotation]
+      Or[ovreline(stmt)][function body]
+      Or[$lambda #[`tag`] a.$ `decl`][with argument pass strategy annotation]
     }
   ),
   Prod(
     `prog`,
     {
-      Or[`fun_decl`][main function]
-      Or[`fun_decl` `prog`][with supplimentary funcitons]
+      Or[`decl`][main function]
+      Or[`decl` `prog`][with supplimentary funcitons]
     }
   ),
 )
-#align(center, [$d, f in NN,$ `args` $in NN ast.basic$])
-
 == Семантика статического интерпретатора
 
 #h(10pt)
 
-$V := {0, bot}$ - значения памяти
+$V := value$ - значения памяти
 
 $L := NN$ - позиции в памяти
 
 $X$ - можество переменных
 
-$sigma : X -> L$ - позиции памяти, соответстующие переменным контекста
+$sigma : X -> L$ - #[ позиции памяти, соответстующие переменным контекста,
+                            частично определённая функция ]
 
-$mu : NN -> V$ - память
+$mu : NN -> V$ - память, частично определённая функция
 
 $l in NN$ - длина используемого фрагмента памяти
 
 $M subset NN$ - множество испорченных ячеек памяти
 
+$DD : NN -> decl$ - определения функций, частично определённая функция
+
+$d in decl, s in stmt, f in NN, x in X, a in NN$
+
+$d space @ space overline(x)$ - запись применения функции (вида #decl) к аргументам
+
 #[
 
 #let cl = $chevron.l$
@@ -111,36 +114,74 @@ $M subset NN$ - множество испорченных ячеек памят
 
 #h(10pt)
 
+#align(center, line())
+
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ $f(x), space f(ast.basic a) = e$],
-
-    $cl [a -> sigma(x)], mu, l, nothing cr
-     xarrow(e)
-     cl sigma, mu', l', M' cr$,
-
-    $mu' =>^M' gamma$,
+    name: [ $(lambda ast.basic a. d) x$],
 
     $cl sigma, mu, l, M cr
-     xarrow(f(ast.basic x))
-     cl sigma, gamma|_[0, l), l, M cr$,
+     xarrowDashed(d space @ space overline(y))
+     cl sigma, mu', l', M' cr$,
+
+    $cl sigma, mu, l, M cr
+     xarrowDashed((lambda ast.basic a. d) space @ space  x space overline(y))
+     cl sigma, mu', l', M' cr$,
   )
 ))
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ $f(x), space f(a) = e$],
+    name: [ $(lambda !a. d) x$],
 
-    $cl [a -> l], mu, l + 1, nothing cr
-     xarrow(e)
-     cl sigma, mu', l', M' cr$,
+    $cl sigma [a <- l], mu, l + 1, M cr
+     xarrowDashed(d space @ space overline(y))
+     cl sigma', mu', l', M' cr$,
+
+    $cl sigma, mu, l, M cr
+     xarrowDashed((lambda !a. d) space @ space x space overline(y))
+     cl sigma', mu', l', M' cr$,
+  )
+))
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [decl body],
+
+    $cl sigma, mu, l, M cr
+     attach(stretch(->)^overline(s), tr: *)
+     cl sigma', mu', l', M' cr$,
+
+    $d = overline(s)$,
+
+    $cl sigma, mu, l, M cr
+     xarrowDashed(d space @)
+     cl sigma', mu', l', M' cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, line())
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ CALL $f space overline(x)$],
+
+    $cl [], mu, l, nothing cr
+     xarrowDashed(d space @ space overline(x))
+     cl sigma', mu', l', M' cr$,
 
     $mu' =>^M' gamma$,
 
+    $DD(f) := d$,
+
     $cl sigma, mu, l, M cr
-     xarrow(f(x))
+     xarrow("CALL" f space overline(x))
      cl sigma, gamma|_[0, l), l, M cr$,
   )
 ))
@@ -170,51 +211,3 @@ $M subset NN$ - множество испорченных ячеек памят
 ))
 
 ]
-
-== Пример аннтаций аргументов
-
-#h(10pt)
-
-#align(center, grid(
-columns: 3,
-gutter: 5%,
-  ```
-  def f(?fx x, ?fy y) {
-    read(x);
-    write(x);
-    read(y);
-  }
-  def w(?wx x) {
-    write(x);
-  } 
-  ```,
-  ```
-  def g(?gx x, ?gy y) {
-    write(x);
-    write(y);
-    read(x);
-    read(y);
-  }
-  def r(?rx x) {
-    read(x);
-  } 
-  ```,
-  ```
-  def main(x, y, z, k) {
-    w(x);
-    r(x); // -> ?wx != ref
-    f(x, y);
-    r(y);
-    g(z, k);
-    w(z);
-    f(y, z);
-    r(k); // -> ?gy != ref
-  }
-  ```
-))
-```
--> ?fx = ref, ?fy = ref, ?wx = copy, ?gx = ref, ?gy = copy, ?rx = ref
-...
--> ?fx = copy, ?fy = copy, ?wx = copy, ?gx = copy, ?gy = copy, ?rx = copy
-```
-