model_with_control_flow/model.typ

@@ -7,7 +7,9 @@
 
 = Формальная модель используемого языка
 
-*TODO: проверить, что всё нужное добавлено*
+*TODO: добавить лямбды, control flow, локальные переменные в каком-то виде*
+
+*TODO: проблемы с добавлением if в будущем: как записать write and not write ?*
 
 Нужно будет добавить во write-flag модальности: `not write` | `may write` | `always write`
 
@@ -29,8 +31,7 @@
 #let isCorrect = `isCorrect`
 
 #let isRead = `isRead`
-#let isAlwaysWrite = `isAlwaysWrite`
-#let isPossibleWrite = `isPossibleWrite`
+#let isWrite = `isWrite`
 #let isRef = `isRef`
 #let isCopy = `isCopy`
 #let isIn = `isIn`
@@ -46,12 +47,11 @@
     { Or[Read][read passed value]
       Or[Not Read][] } ),
   Prod(`write`,
-    { Or[$square$ Write][in all cases there is a write to passed variable] // always write, requre at least one write in each flow variant
-      Or[$diamond$ Write][in some cases there is a write to passed variable] // possible write, no requirements (?)
-      Or[$not$ Write][] } ), // no write, require n owrites in all flow variants
+    { Or[Write][write to passed variable]
+      Or[Not Write][] } ),
   Prod(`copy`,
     { Or[Ref][pass reference to the value]
-      Or[Value][pass copy of the value] } ),
+      Or[Value][pass copy of te value] } ),
   Prod(`in`,
     { Or[In][parameter value used as input]
       Or[Not In][] } ),
@@ -67,9 +67,8 @@
   Prod(
     `value`,
     {
-      Or[$0$][cell with some value (always)]
-      Or[$X$][cell with possible value or $bot$]
-      Or[$bot$][spoiled cell (always)]
+      Or[$0$][cell with some value]
+      Or[$bot$][spoiled cell]
     }
   ),
   // Prod(
@@ -85,17 +84,13 @@
       Or[`CALL` $f space overline(x)$][call function by id]
       Or[`WRITE` $x$][write to variable]
       Or[`READ` $x$][read from variable]
-      Or[`CHOICE` #overline(`stmt`) #overline(`stmt`)][control flow operator, xecution of one of the blocks]
-      // NOTE: var: replaced with arguments (use rvalue as init) (?)
-      // Or[`VAR`][variables inside functions] // NOTE: no modifiers required, because it is in the new memory ?? // TODO: not required ??
-      // NOTE: lambda: compile to call to the funciton with CHOICE between possible lambda bodies <- do this analysis inside synthesizer ?
     }
   ),
   Prod(
     `decl`,
     {
       Or[ovreline(stmt)][function body]
-      Or[$lambda #[`tag` #h(3pt) `argtype`] a.$ `decl`][argument with argument pass strategy annotation]
+      Or[$lambda #[`tag`] a.$ `decl`][with argument pass strategy annotation]
     }
   ),
   Prod(
@@ -164,9 +159,9 @@ $d space @ space overline(x)$ - запись применения функции
   vertical-spacing: 4pt,
   rule(
     name: [ is correct],
-    $isOut tag -> isAlwaysWrite tag$, // NOTE; strong requirment should write
+    $isOut tag -> isWrite tag$, // NOTE; strong requirment should write
     $isRead tag -> isIn tag$,
-    $isPossibleWrite tag and (isOut tag or not isCopy tag) -> isAlwaysWrite sigma(x)$, // NOTE: may tag => should sigma(x)
+    $isWrite tag and (isOut tag or not isCopy tag) -> isWrite sigma(x)$, // NOTE: may tag => should sigma(x)
     $isRead tag -> mu (sigma(x)) != bot$, // NOTE: may tag -> ... 
 
     $isCorrect_(cl sigma, mu cr) (tag, x)$,
@@ -192,7 +187,7 @@ $d space @ space overline(x)$ - запись применения функции
 
     $mu stretch(=>)^args_sigma gamma$,
 
-    $isPossibleWrite tag$, // NOTE: weak requirement: may write
+    $isWrite tag$, // NOTE: weak requirement: may write
     $not isCopy tag$,
     $not isOut tag$,
 
@@ -212,7 +207,7 @@ $d space @ space overline(x)$ - запись применения функции
 
     $mu stretch(=>)^args_sigma gamma$,
 
-    $isAlwaysWrite tag$, // NOTE: strong requirement: should write
+    $isWrite tag$, // NOTE: strong requirement: should write
     $isOut tag$,
 
     $isCorrect_(cl sigma, mu cr) (tag, x)$,
@@ -386,8 +381,7 @@ $d space @ space overline(x)$ - запись применения функции
   rule(
     name: [ READ $x$],
 
-    $mu[sigma(x)] != bot$,
-    $mu[sigma(x)] != X$,
+    $mu(sigma(x)) != bot$,
 
     $cl sigma, mu, l cr
      xarrow("READ" x)
@@ -402,7 +396,7 @@ $d space @ space overline(x)$ - запись применения функции
   rule(
     name: [ WRITE $x$],
 
-    $isPossibleWrite sigma(x)$, // TODO: FIXME ?? always or possible ??
+    $isWrite sigma(x)$,
 
     $cl sigma, mu, l cr
      xarrow("WRITE" x)
@@ -410,38 +404,4 @@ $d space @ space overline(x)$ - запись применения функции
   )
 ))
 
-#h(10pt)
-
-#let combine = `combine`
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ CHOICE $overline(s)$ $overline(t)$],
-
-    $cl sigma, mu, l cr
-     attach(stretch(->)^overline(s), tr: *)
-     cl sigma_s, mu_s, l_s cr$,
-
-    $cl sigma, mu, l cr
-     attach(stretch(->)^overline(t), tr: *)
-     cl sigma_t, mu_t, l_t cr$,
-
-    $l_t = l_s$,
-    $sigma_s = sigma_t$,
-
-    // TODO changes ?? two ways ??
-    $cl sigma, mu, l cr
-     xarrow("CHOICE" overline(s) space overline(t))
-     cl sigma, combine(mu_s, mu_t), l cr$,
-  )
-))
-
-#h(10pt)
-
-$ combine(mu_1, mu_2)[i] = combine_e (mu_1[i], mu_2[i]) $
-$ combine_e (bot, bot) = bot $
-$ combine_e (0, 0) = 0 $
-$ combine_e (\_, \_) = X $
-
 ]