From 9b9c6927cf19d7ad08389e1370f114cfc6b4cfa4 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 15 Mar 2026 16:05:22 +0000 Subject: [PATCH 1/2] part semantics changes to include conditions. problem: 'choice' makes undetermenistic changes to vars, need to deal with that => top level-only choice (other choices - syntactic sugar) or more possible values --- model_with_control_flow/model.typ | 50 ++++++++++++++++++++++++------- 1 file changed, 40 insertions(+), 10 deletions(-) diff --git a/model_with_control_flow/model.typ b/model_with_control_flow/model.typ index 3db4e2c..b105479 100644 --- a/model_with_control_flow/model.typ +++ b/model_with_control_flow/model.typ @@ -31,7 +31,8 @@ #let isCorrect = `isCorrect` #let isRead = `isRead` -#let isWrite = `isWrite` +#let isAlwaysWrite = `isAlwaysWrite` +#let isPossibleWrite = `isPossibleWrite` #let isRef = `isRef` #let isCopy = `isCopy` #let isIn = `isIn` @@ -47,11 +48,12 @@ { Or[Read][read passed value] Or[Not Read][] } ), Prod(`write`, - { Or[Write][write to passed variable] - Or[Not 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 Prod(`copy`, { Or[Ref][pass reference to the value] - Or[Value][pass copy of te value] } ), + Or[Value][pass copy of the value] } ), Prod(`in`, { Or[In][parameter value used as input] Or[Not In][] } ), @@ -84,13 +86,17 @@ 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`] a.$ `decl`][with argument pass strategy annotation] + Or[$lambda #[`tag` #h(3pt) `argtype`] a.$ `decl`][argument with argument pass strategy annotation] } ), Prod( @@ -159,9 +165,9 @@ $d space @ space overline(x)$ - запись применения функции vertical-spacing: 4pt, rule( name: [ is correct], - $isOut tag -> isWrite tag$, // NOTE; strong requirment should write + $isOut tag -> isAlwaysWrite tag$, // NOTE; strong requirment should write $isRead tag -> isIn tag$, - $isWrite tag and (isOut tag or not isCopy tag) -> isWrite sigma(x)$, // NOTE: may tag => should sigma(x) + $isPossibleWrite tag and (isOut tag or not isCopy tag) -> isAlwaysWrite sigma(x)$, // NOTE: may tag => should sigma(x) $isRead tag -> mu (sigma(x)) != bot$, // NOTE: may tag -> ... $isCorrect_(cl sigma, mu cr) (tag, x)$, @@ -187,7 +193,7 @@ $d space @ space overline(x)$ - запись применения функции $mu stretch(=>)^args_sigma gamma$, - $isWrite tag$, // NOTE: weak requirement: may write + $isPossibleWrite tag$, // NOTE: weak requirement: may write $not isCopy tag$, $not isOut tag$, @@ -207,7 +213,7 @@ $d space @ space overline(x)$ - запись применения функции $mu stretch(=>)^args_sigma gamma$, - $isWrite tag$, // NOTE: strong requirement: should write + $isAlwaysWrite tag$, // NOTE: strong requirement: should write $isOut tag$, $isCorrect_(cl sigma, mu cr) (tag, x)$, @@ -396,7 +402,7 @@ $d space @ space overline(x)$ - запись применения функции rule( name: [ WRITE $x$], - $isWrite sigma(x)$, + $isPossibleWrite sigma(x)$, // TODO: FIXME ?? always or possible ?? $cl sigma, mu, l cr xarrow("WRITE" x) @@ -404,4 +410,28 @@ $d space @ space overline(x)$ - запись применения функции ) )) +#h(10pt) + +// TODO: FIXME +// TODO: anyway choice is actually on the top level ?? +#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, gamma_s, l_s cr$, + + $cl sigma, mu, l cr + attach(stretch(->)^overline(t), tr: *) + cl sigma_t, gamma_t, l_t cr$, + + // TODO changes ?? two ways ?? + $cl sigma, mu, l cr + xarrow("CHOICE" overline(s) overline(t)) + cl sigma, mu, l cr$, + ) +)) + ] From 869bffb0df152e89d4ca79f414e291d815857d01 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sun, 15 Mar 2026 20:49:31 +0000 Subject: [PATCH 2/2] control flow semantics draft --- model_with_control_flow/model.typ | 34 ++++++++++++++++++++----------- 1 file changed, 22 insertions(+), 12 deletions(-) diff --git a/model_with_control_flow/model.typ b/model_with_control_flow/model.typ index b105479..d4a8119 100644 --- a/model_with_control_flow/model.typ +++ b/model_with_control_flow/model.typ @@ -7,9 +7,7 @@ = Формальная модель используемого языка -*TODO: добавить лямбды, control flow, локальные переменные в каком-то виде* - -*TODO: проблемы с добавлением if в будущем: как записать write and not write ?* +*TODO: проверить, что всё нужное добавлено* Нужно будет добавить во write-flag модальности: `not write` | `may write` | `always write` @@ -69,8 +67,9 @@ Prod( `value`, { - Or[$0$][cell with some value] - Or[$bot$][spoiled cell] + Or[$0$][cell with some value (always)] + Or[$X$][cell with possible value or $bot$] + Or[$bot$][spoiled cell (always)] } ), // Prod( @@ -387,7 +386,8 @@ $d space @ space overline(x)$ - запись применения функции rule( name: [ READ $x$], - $mu(sigma(x)) != bot$, + $mu[sigma(x)] != bot$, + $mu[sigma(x)] != X$, $cl sigma, mu, l cr xarrow("READ" x) @@ -412,8 +412,8 @@ $d space @ space overline(x)$ - запись применения функции #h(10pt) -// TODO: FIXME -// TODO: anyway choice is actually on the top level ?? +#let combine = `combine` + #align(center, prooftree( vertical-spacing: 4pt, rule( @@ -421,17 +421,27 @@ $d space @ space overline(x)$ - запись применения функции $cl sigma, mu, l cr attach(stretch(->)^overline(s), tr: *) - cl sigma_s, gamma_s, l_s cr$, + cl sigma_s, mu_s, l_s cr$, $cl sigma, mu, l cr attach(stretch(->)^overline(t), tr: *) - cl sigma_t, gamma_t, l_t cr$, + 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) overline(t)) - 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 $ + ]