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, xarrowDashed
+#import "@preview/xarrow:0.4.0": xarrow
 
 = Формальная модель используемого языка
 
@@ -11,81 +11,78 @@
 
 #h(10pt)
 
-#let tag = `tag`
-#let value = `value`
-#let stmt = `stmt`
-#let decl = `decl`
-#let prog = `prog`
 #bnf(
   Prod(
     `tag`,
     {
-      Or[$ast.basic$][pass by reference]
+      Or[`Ref`][pass by reference]
-      Or[$!$][copy]
+      Or[`Value`][copy]
     }
   ),
   Prod(
     `value`,
     {
-      Or[$0$][cell with some value]
+      Or[`Unit`][cell with some value]
-      Or[$bot$][spoiled cell]
+      Or[`Bot`][spoiled cell]
+    }
+  ),
+  Prod(
+    `arg`,
+    {
+      Or[`RValue`][new value, no associated variable]
+      Or[`LValue` $d$][value from some variable]
     }
   ),
-  // Prod(
-  //   `arg`,
-  //   {
-  //     Or[$0$][new value, no associated variable]
-  //     Or[$ amp d$][value from some variable]
-  //   }
-  // ),
   Prod(
     `stmt`,
     {
-      Or[`CALL` $f space overline(x)$][call function by id]
+      Or[$f($`args`$)$][call function by id]
-      Or[`WRITE` $x$][write to variable]
+      Or[`write` $d$][write to variable]
-      Or[`READ` $x$][read from variable]
+      Or[`read` $d$][read from variable]
     }
   ),
   Prod(
-    `decl`,
+    `body`,
     {
-      Or[ovreline(stmt)][function body]
+      Or[`body` `stmt`][with statement]
-      Or[$lambda #[`tag`] a.$ `decl`][with argument pass strategy annotation]
+      Or[$epsilon$][empty body]
+    }
+  ),
+  Prod(
+    `fun_decl`,
+    {
+      Or[`body`][function body]
+      Or[`tag` `fun_decl`][with argument pass strategy annotation]
     }
   ),
   Prod(
     `prog`,
     {
-      Or[`decl`][main function]
+      Or[`fun_decl`][main function]
-      Or[`decl` `prog`][with supplimentary funcitons]
+      Or[`fun_decl` `prog`][with supplimentary funcitons]
     }
   ),
 )
+#align(center, [$d, f in NN,$ `args` $in NN ast.basic$])
+
 == Семантика статического интерпретатора
 
 #h(10pt)
 
-$V := value$ - значения памяти
+$V := {0, bot}$ - значения памяти
 
 $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$
@@ -114,74 +111,19 @@ $d space @ space overline(x)$ - запись применения функции
 
 #h(10pt)
 
-#align(center, line())
-
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ $(lambda ast.basic a. d) x$],
+    name: [ $f(x), space f := lambda a. e$],
 
-    $cl sigma, mu, l, M cr
+    $cl [a -> sigma(x)], mu, l, nothing cr
-     xarrowDashed(d space @ space overline(y))
+     xarrow(e)
      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: [ $(lambda !a. d) x$],
-
-    $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("CALL" f space overline(x))
+     xarrow(f(*x))
      cl sigma, gamma|_[0, l), l, M cr$,
   )
 ))
@@ -211,3 +153,51 @@ $d space @ space overline(x)$ - запись применения функции
 ))
 
 ]
+
+== Пример аннтаций аргументов
+
+#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
+```
+