st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-04-29 09:14:35 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Compare commits

base: st:adeefc1c870a937f4820bcc7e0e27ad4457ab39a
Branches Tags
st:main
..
compare: st:57bb3a72ecf64d7564c6e2d69d032056c95fbeb5
Branches Tags
st:main

No commits in common. "adeefc1c870a937f4820bcc7e0e27ad4457ab39a" and "57bb3a72ecf64d7564c6e2d69d032056c95fbeb5" have entirely different histories.
adeefc1c87 ... 57bb3a72ec

1 changed files with 174 additions and 259 deletions
Download patch file Download diff file Expand all files Collapse all files

433
model_with_structures/model.typ
View file

@ -15,8 +15,6 @@
#h(10pt) #h(10pt)
#let rf = $\& #h(3pt)$
#let isCorrect = `isCorrect` #let isCorrect = `isCorrect`
#let isRead = `isRead` #let isRead = `isRead`
@ -27,28 +25,13 @@
#let isIn = `isIn` #let isIn = `isIn`
#let isOut = `isOut` #let isOut = `isOut`
#let readTag = `read`
#let writeTag = `write`
#let copyTag = `copy`
#let inTag = `in`
#let outTag = `out`
#let mode = `mode` #let mode = `mode`
#let Copy = `Copy`
#let Ref = `Ref`
#let MaybeWrite = [$diamond$ `Write`]
#let AlwaysWrite = [$square$ `Write`]
#let Read = `Read`
#let In = `In`
#let Out = `Out`
#let expr = `expr` #let expr = `expr`
#let stmt = `stmt` #let stmt = `stmt`
#let decl = `decl` #let decl = `decl`
#let prog = `prog` #let prog = `prog`
#let path = `path` #let path = `path`
#let type = `type` #let type = `type`
#let modedType = `modedtype`
#bnf( #bnf(
Prod(`read`, Prod(`read`,
// NOTE: not three modalities for write, because read does not change value // NOTE: not three modalities for write, because read does not change value
@ -71,7 +54,7 @@
Prod( Prod(
`mode`, `mode`,
{ {
Or[$inTag space outTag$][] Or[`read` #h(3pt) `write` #h(3pt) `copy` #h(3pt) `in` #h(3pt) `out`][]
} }
), ),
Prod( Prod(
@ -88,36 +71,33 @@
Prod( Prod(
`type`, `type`,
{ {
Or[$readTag writeTag ()$][simple type representing all primitive types] // `Unit` Or[$()$][simple type representing all primitive types] // `Unit`
Or[$rf copyTag space type$][reference to structure, contains copy / ref choice] // `Ref` Or[\& #h(3pt) `mode` #h(3pt) `type`][reference to structure, contains copy / ref choice] // `Ref`
Or[$[type+]$][tuple type] // `Prod` Or[$[type+]$][tuple type] // `Prod`
// Or[`type` $times$ `type`][pair type, allows to make tuples] // `Prod` // Or[`type` $times$ `type`][pair type, allows to make tuples] // `Prod`
// Or[`type` $+$ `type`][union type (important in some way ???)] // `Sum` // TODO ? // Or[`type` $+$ `type`][union type (important in some way ???)] // `Sum` // TODO ?
// NOTE: do not use names in type // NOTE: do not use names in type
// Or[$lambda_((x type)+)$][type of lambda or function pointer, defined by function declaration] // `Fun` // Or[$lambda_((x type)+)$][type of lambda or function pointer, defined by function declaration] // `Fun`
Or[$lambda (modedType)+$][type of lambda or function pointer, defined by function declaration] // `Fun` Or[$lambda type+$][type of lambda or function pointer, defined by function declaration] // `Fun`
}
),
Prod(
`modedtype`,
{
Or[$mode type$][type woth in and out modifiers]
} }
), ),
// FIXME: replace with expr
Prod( Prod(
`expr`, `expr`,
{ {
Or[$()$][value of simple type] // `Unit` Or[$()$][value of simple type] // `Unit`
Or[$path$][value from variable] // `Path` Or[$path$][value from variable] // `Path`
Or[$rf expr$][reference expr] // `Ref` Or[$\& #h(3pt) expr$][reference expr] // `Ref`
Or[$[expr+]$][tuple expr] // `Prod` Or[$[expr+]$][tuple expr] // `Prod`
// NOTE: replaced with simple path value
// Or[$lambda_path$][function value from variable] // `Fun`
} }
), ),
Prod( Prod(
`stmt`, `stmt`,
{ {
Or[`CALL` $path space expr+$][call function] Or[`CALL` $f space expr+$][call function]
Or[`WRITE` $path$][write to variable] Or[`WRITE` $path$][write to variable]
Or[`READ` $path$][read from variable] Or[`READ` $path$][read from variable]
Or[$stmt ; stmt$][control flow operator, xecution ] Or[$stmt ; stmt$][control flow operator, xecution ]
@ -129,7 +109,7 @@
{ {
// TODO: path not allowed ?? // TODO: path not allowed ??
Or[$"var" X : type = expr$][global variable declaration] Or[$"var" X : type = expr$][global variable declaration]
Or[$"fun" X ((X : modedType)+) = stmt$][function declaration] Or[$"fun" X ((X : type)+) = stmt$][function declaration]
} }
), ),
Prod( Prod(
@ -142,19 +122,21 @@
== Value Model == Value Model
#let deepValue = `deepvalue` #let rf = $\& #h(3pt)$
#let value = `value`
// FIXME: check & add details
#let deepvalue = `deepvalue`
#let value = `value`
#bnf( #bnf(
Prod( Prod(
$deepValue$, $deepvalue$,
{ {
Or[$0$][valid value of simple type] // `Unit` Or[$0$][valid value of simple type] // `Unit`
Or[$\#$][valid or spoiled value of simple type] // `Unit` Or[$\#$][valid or spoiled value of simple type] // `Unit`
Or[$bot$][spoiled value of simple type] // `Unit` Or[$bot$][spoiled value of simple type] // `Unit`
Or[$lambda type+ stmt$][function pointer value] // `Fun` Or[$lambda type+ stmt$][function pointer value] // `Fun`
Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref` Or[$rf deepvalue$][reference value, contains label of the value in the memory] // `Ref`
Or[$[deepValue+]$][tuple value] // `Prod` Or[$[deepvalue+]$][tuple value] // `Prod`
} }
), ),
Prod( Prod(
@ -164,23 +146,22 @@
Or[$\#$][valid or spoiled value of simple type] // `Unit` Or[$\#$][valid or spoiled value of simple type] // `Unit`
Or[$bot$][spoiled value of simple type] // `Unit` Or[$bot$][spoiled value of simple type] // `Unit`
Or[$lambda type+ stmt$][function pointer value] // `Fun` Or[$lambda type+ stmt$][function pointer value] // `Fun`
// FIXME: embed mode into value for simplification ?? Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
Or[$rf copyTag LL$][reference value, contains label of the value in the memory] // `Ref`
Or[$[value+]$][tuple value] // `Prod` Or[$[value+]$][tuple value] // `Prod`
} }
), ),
) )
#deepValue - полное значение, #value - слой значения, привязан к конкретной памяти $mu$ #deepvalue - полное значение, #value - слой значения, привязан к конкретной памяти $mu$
Значения, могут лежать в переменных и передаваться как аргументы функций (то, во что вычисляется $expr$) Значения, могут лежать в переменных и передаваться как аргументы функций (то, во что вычисляется $expr$)
$v in value$ - произвольное значение $v in value$ - произвольное значение
Получение #deepValue по #value: Получение #value по #deepvalue:
- $rf c l xarrowSquiggly(mu)_#[deep] rf c mu[l]$ - $rf LL xarrowSquiggly(mu)_#[deep] rf mu[LL]$
- $* xarrowSquiggly(mu)_#[deep] *$ - $* xarrowSquiggly(mu)_#[deep] *$
где $*$ - произвольный конструктор значения, кроме $rf$ где $*$ - произвольный конструктор значения кроме $rf$
== Memory Model == Memory Model
@ -192,16 +173,17 @@ $v in value$ - произвольное значение
- $LL$ - множество меток памяти - $LL$ - множество меток памяти
- $mem := LL -> value, space mu : mem$ - память, частично определённая функция - $mem := LL -> value, space mu : mem$ - память, частично определённая функция
- $l in LL$ - новый тег памяти (ранее не использованный) - $l in LL$ - новый тег памяти (ранее не использованный)
- `next` - получение следующей неиспользованной метки в памяти - `next` - получение следующей неиспользованной метки
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ add value to memory], name: [ add value to memory],
$l = #[next] (mu)$, $l' = #[next] (l)$,
$cl mu cr xarrowSquiggly(v)_#[add] cl l, mu [l <- v] cr$, // TODO: check that access is what required ??
$cl mu, l cr xarrowSquiggly(v)_#[add] cl mu [l <- v], l' cr$,
) )
)) ))
@ -278,7 +260,7 @@ $s in stmt, f in X, x in X, a in X$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ tuple access path], name: [ access path],
$x tpath p$, $x tpath p$,
@ -291,7 +273,7 @@ $s in stmt, f in X, x in X, a in X$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ variable type access], name: [ variable typing],
$x : t_x ttype @x : t_x$, $x : t_x ttype @x : t_x$,
) )
@ -299,7 +281,7 @@ $s in stmt, f in X, x in X, a in X$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ reference type access], name: [ reference typing],
$x tpath p$, $x tpath p$,
$x : t_x ttype p : rf mode t_p$, $x : t_x ttype p : rf mode t_p$,
@ -309,7 +291,7 @@ $s in stmt, f in X, x in X, a in X$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ tuple type access], name: [ access typing],
$x tpath p$, $x tpath p$,
$x : t_x ttype p : [t_1, ... t_n]$, $x : t_x ttype p : [t_1, ... t_n]$,
@ -318,34 +300,34 @@ $s in stmt, f in X, x in X, a in X$
)) ))
] ]
- #[ Получение read-write тега поля - #[ Получение тега поля
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ variable rw tag access], name: [ variable typing],
$t_x = r w ()$, $t_x = rf mode t$,
$x : t_x tmode @x -> cr r w cl$, $x : t_x tmode @x -> mode$,
) )
)) ))
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ reference rw tag access], name: [ reference typing],
$x tpath p$, $x tpath p$,
$x : t_x tmode p -> cr r w cl$, $x : t_x tmode p : rf mode t_p$,
$x : t_x tmode *p -> cr r w cl$, $x : t_x tmode *p : t_p$,
) )
)) ))
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ tuple rw tag access], name: [ access typing],
$x tpath p$, $x tpath p$,
$x : t_x tmode p -> cr r w cl$, $x : t_x tmode p : [t_1, ... t_n]$,
$x : t_x tmode p.i -> cr r w cl$, $x : t_x tmode p.i : t_i$,
) )
)) ))
] ]
@ -354,7 +336,7 @@ $s in stmt, f in X, x in X, a in X$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ variable value access], name: [ variable typing],
$x eqmu v_x tval @x eqmu v_x$, $x eqmu v_x tval @x eqmu v_x$,
) )
@ -362,7 +344,7 @@ $s in stmt, f in X, x in X, a in X$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ reference value access], name: [ reference typing],
$x tpath p$, $x tpath p$,
$x eqmu v_x tval p eqmu rf l$, $x eqmu v_x tval p eqmu rf l$,
@ -372,7 +354,7 @@ $s in stmt, f in X, x in X, a in X$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ tuple value access], name: [ access typing],
$x tpath p$, $x tpath p$,
$x eqmu v_x tmode p eqmu [v_1, ... v_n]$, $x eqmu v_x tmode p eqmu [v_1, ... v_n]$,
@ -385,11 +367,11 @@ $s in stmt, f in X, x in X, a in X$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ access], name: [ variable typing],
$v_x = rf l$, $v_x = rf l$,
$x eqmu v_x tval p eqmu rf l$,
$x eqmu v_x tval p eqmu rf l$,
$x eqmu v_x tmode p arrmu l$, $x eqmu v_x tmode p arrmu l$,
) )
)) ))
@ -399,7 +381,7 @@ $s in stmt, f in X, x in X, a in X$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ access], name: [ access typing],
$x tpath p$, $x tpath p$,
$x : sigma[x].2 ttype p : t$, $x : sigma[x].2 ttype p : t$,
@ -408,15 +390,15 @@ $s in stmt, f in X, x in X, a in X$
)) ))
] ]
- #[ Получение read-write тега поля по окружению - #[ Получение тега поля по окружению
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ access], name: [ access typing],
$x tpath p$, $x tpath p$,
$x : sigma[x].2 tmode p -> cr r space w cl$, $x : sigma[x].2 tmode p -> mode$,
$sigma temode p -> cr r space w cl$, $sigma temode p -> mode$,
) )
)) ))
] ]
@ -425,7 +407,7 @@ $s in stmt, f in X, x in X, a in X$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ access], name: [ access typing],
$x tpath p$, $x tpath p$,
$x eqmu sigma[x].1 tval p eqmu v$, $x eqmu sigma[x].1 tval p eqmu v$,
@ -438,7 +420,7 @@ $s in stmt, f in X, x in X, a in X$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ access], name: [ access typing],
$x tpath p$, $x tpath p$,
$x eqmu sigma[x].1 tlabel p arrmu l$, $x eqmu sigma[x].1 tlabel p arrmu l$,
@ -447,37 +429,34 @@ $s in stmt, f in X, x in X, a in X$
)) ))
] ]
=== Mode Accessors === Mode Correctness
#let modevar = $(i space o)$ Функции проверки тегов, имеют тип $mode -> #[bool]$:
$ isIn modevar = i == In $ #let modevar = $(r space w space c space i space o)$
$ isOut modevar = o == Out $
// FIXME: move to new mode model $ isRead modevar = r == "Read" $
// === Mode Correctness $ isAlwaysWrite modevar = w == square "Write" $
$ isPossibleWrite modevar = w == diamond "Write" || w == square "Write" $
$ isRef modevar = c == "Ref" $
$ isCopy modevar = c == "Copy" $
$ isIn modevar = i == "In" $
$ isOut modevar = o == "Out" $
// Функции проверки тегов, имеют тип $mode -> #[bool]$: Требования к тегам:
// #let modevar = $(r space w space c space i space o)$ $ isOut mode -> isAlwaysWrite mode $
$ isRead mode -> isIn mode $
// $ isRead modevar = r == "Read" $
// $ isAlwaysWrite modevar = w == square "Write" $
// $ isPossibleWrite modevar = w == diamond "Write" || w == square "Write" $
// $ isRef modevar = c == "Ref" $
// $ isCopy modevar = c == "Copy" $
// $ isIn modevar = i == "In" $
// $ isOut modevar = o == "Out" $
// Требования к тегам:
// $ isOut mode -> isAlwaysWrite mode $
// $ isRead mode -> isIn mode $
// TODO: rest conditions ?? // TODO: rest conditions ??
=== Eval Rules === Eval Rules
// FIXME: make connected to syntax
*TODO*
#h(10pt)
#let args = `args` #let args = `args`
#[ #[
@ -502,170 +481,124 @@ $ isOut modevar = o == Out $
// TODO: introduce spep env argument ?? // TODO: introduce spep env argument ??
=== Moded Type Correctness #h(10pt)
#let tcorrect = $attach(tack.r, br: #[correct])$ === Correctness
// TODO: FIXME: well formatness for mode, extract // TODO: FIXME: well formatness for mode, extract
// TODO: FIXME: check for mode, is recursion required ?? // TODO: FIXME: check for mode, is recursion required ??
// TODO: FIXME: check mode & access corectness in os correct // TODO: FIXME: check mode & access corectness in os correct
$ sigma in env, space mu in mem, space m in mode, // TODO: check all requirements
space c in copyTag, space r, r' in readTag, space w, w' in writeTag,
space v in value, space t, t' in type $
#h(10pt)
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ unit assignment tags correctness], name: [ is correct],
$isOut mode -> isAlwaysWrite mode$, // NOTE; strong requirment should write
$isRead mode -> isIn mode$,
$isPossibleWrite mode and (isOut mode or not isCopy mode) -> isAlwaysWrite pathenvmode(sigma, x)$, // NOTE: may mode => should sigma(x)
$isRead mode -> pathenvval(mu, sigma, x) != bot and pathenvval(mu, sigma, x) != X$,
$r = Read => isIn m$, $isCorrect_(cl sigma, mu cr) (mode, x)$,
$isOut m => w = AlwaysWrite$,
// $sigma temode x -> cr r' space w' cl$, // NOTE: not required, value passed
$(w = AlwaysWrite or w = MaybeWrite) and (isOut m or c = Ref) => w' = AlwaysWrite$,
// $sigma, mu teval x eqmu v$, // NOTE: not required, value passed
$v in {0, \#, bot}$,
$r = Read => v = 0$,
$sigma, mu, m, c tcorrect v : r' space w' () -> r space w ()$,
) )
)) ))
#h(10pt) #h(10pt)
#align(center, prooftree( === Call Initialization
vertical-spacing: 4pt,
rule(
name: [ ref assignment tags correctness],
$sigma, mu, m, c_r tcorrect v : t -> t'$, Отсутствующий нижний индекс ($ref$, $copy$) означает произвольный индекс.
Считается, что выбранный индекс одинаков в рамках одного правила.
// TODO: FIXME: which tag translations are correct ?? <- only assignee? // NOTE: no empty type
$sigma, mu, m, c tcorrect rf c_r space v : rf c' space t -> rf c_r space t'$, // #align(center, prooftree(
) // vertical-spacing: 4pt,
)) // rule(
// name: [ add paths init],
#h(10pt) // $cl sigma, mu, l cr stretch(~>)^nothing cl sigma, mu, l cr$,
// )
// ))
// #h(10pt)
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ tuple assignmenttags correctness], name: [ add paths field by copy],
$sigma, mu, m, c tcorrect v_1 : t_1 -> t'_1$,
$...$,
$sigma, mu, m, c tcorrect v_n : t_n -> t'_n$,
$sigma, mu, m, c tcorrect [v_1, ... v_n] : [t_1, ..., t_n] -> [t'_1, t'_n]$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ function pointer tags correctness],
$sigma, mu, m, c tcorrect lambda space overline(t) space s : lambda space overline(t) -> lambda space overline(t)$,
)
))
#h(10pt)
=== Value Construction
#let new = `new`
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ new $0$ value],
// TODO: check that access is what required ?? // TODO: check that access is what required ??
$cl 0, mu cr xarrowSquiggly(space)_new cl 0, mu cr$, $cl sigma, mu, l cr xarrowSquiggly(p : ())_copy cl pathenvmem(sigma, p) <- l, mu [l <- 0], l + 1 cr$,
) )
)) ))
#h(10pt)
// NOTE: do nothing, ref init by default
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ add paths field by reference],
$cl sigma, mu, l cr xarrowSquiggly(p : ())_ref cl sigma, mu, l cr$,
)
))
#h(10pt)
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ new $\#$ value], name: [ add paths ref],
$cl sigma, mu, l cr xarrowSquiggly(*p : t)_ref cl sigma', mu', l' cr$,
$isRef mode$,
// TODO: check that access is what required ?? $cl sigma, mu, l cr xarrowSquiggly(p : \& mode t) cl sigma', mu', l' cr$,
$cl \#, mu cr xarrowSquiggly(space)_new cl \#, mu cr$,
) )
)) ))
#h(10pt)
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ new $bot$ value], name: [ add paths ref],
$cl sigma, mu, l cr xarrowSquiggly(*p : t)_copy cl sigma, mu, l cr$,
$isCopy mode$,
$cl bot, mu cr xarrowSquiggly(space)_new cl bot, mu cr$, $cl sigma, mu, l cr xarrowSquiggly(p : \& mode t) cl sigma', mu', l' cr$,
) )
)) ))
#h(10pt)
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ new funciton pointer value], name: [ add paths tuple],
$cl sigma, mu, l cr xarrowSquiggly(p.1 : t_1) cl sigma_1, mu_1, l_1 cr$,
$cl lambda overline(t) s, mu cr xarrowSquiggly(space)_new cl lambda overline(t) s, mu cr$,
)
))
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ new reference ref value],
$cl rf Ref l, mu cr xarrowSquiggly(space)_new cl rf Ref l, mu cr$,
)
))
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ new reference copy value],
$cl mu[l], mu cr xarrowSquiggly(space)_new cl v, mu_v cr$,
$cl mu_v cr xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
$cl rf Copy l, mu cr xarrowSquiggly(space)_new cl rf Copy l', mu_a cr$,
)
))
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ new tuple value],
$cl v_1, mu_0 cr xarrowSquiggly(space)_new cl lambda v'_1, mu_1 cr$,
$...$, $...$,
$cl v_n, mu_(n - 1) cr xarrowSquiggly(space)_new cl lambda v'_n, mu_n cr$, $cl sigma_(n - 1), mu_(n - 1), l_(n - 1) cr xarrowSquiggly(p.n : t_n) cl sigma_n, mu_n, l_n cr$,
$cl [v_1, ... v_n], mu_0 cr xarrowSquiggly(space)_new cl [v'_1, ... v'_n], mu_n cr$, $cl sigma, mu, l cr xarrowSquiggly(p : [t_1, ... t_n]) cl sigma_n, mu_n, l_n cr$,
) )
)) ))
=== Value Update #h(10pt)
#let write = `write` #align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ add paths funciton pointer],
*TODO: write to value* $cl sigma, mu, l cr xarrowSquiggly(F_x) cl sigma, mu, l cr$,
)
))
#h(10pt)
=== Call Finalization === Call Finalization
// FIXME: make connected to syntax
*TODO*
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
@ -737,9 +670,6 @@ $ sigma in env, space mu in mem, space m in mode,
=== Function Evaluation === Function Evaluation
// FIXME: make connected to syntax
*TODO*
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
@ -789,22 +719,22 @@ $ sigma in env, space mu in mem, space m in mode,
=== Statement Evaluation === Statement Evaluation
// FIXME: make connected to syntax
*TODO: check type of lambda?, args from type?*
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ CALL $f space overline(p)$], name: [ CALL $f space overline(x)$],
$cl [], mu, l cr $cl [], mu, l cr
xarrowDashed(f space @ space overline(p)) xarrowDashed(d space @ space overline(x))
cl sigma', mu', l' cr$, cl sigma', mu', l' cr$,
// TODO: FIXME define args in some way // TODO: FIXME define args in some way
$mu attach(stretch(=>)^args_sigma, tr: *) gamma$, $mu attach(stretch(=>)^args_sigma, tr: *) gamma$,
$DD(f) := d$,
$cl sigma, mu, l cr $cl sigma, mu, l cr
xarrow("CALL" f space overline(p)) xarrow("CALL" f space overline(x))
cl sigma, gamma, l cr$, cl sigma, gamma, l cr$,
) )
)) ))
@ -814,12 +744,32 @@ $ sigma in env, space mu in mem, space m in mode,
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ READ $p$], name: [ CALL_LAM $y space overline(x)$],
$mu, sigma teval p eqmu 0$, $pathenvtype(sigma, y) = F_f$,
$cl sigma, mu, l cr $cl sigma, mu, l cr
xarrow("READ" p) xarrow("CALL" f space overline(x))
cl sigma, gamma, l cr$,
$cl sigma, mu, l cr
xarrow("CALL_LAM" y space overline(x))
cl sigma, gamma, l cr$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ READ $x$],
$pathenvval(mu, sigma, x) != bot$,
$pathenvval(mu, sigma, x) != X$,
$cl sigma, mu, l cr
xarrow("READ" x)
cl sigma, mu, l cr$, cl sigma, mu, l cr$,
) )
)) ))
@ -831,38 +781,11 @@ $ sigma in env, space mu in mem, space m in mode,
rule( rule(
name: [ WRITE $x$], name: [ WRITE $x$],
$sigma temode p -> cr r space w cl$, $isPossibleWrite sigma(x)$,
$w == MaybeWrite or w == AlwaysWrite$, $cl sigma, mu, l cr
xarrow("WRITE" x)
$x tpath p$, cl sigma, pathenvval(mu, sigma, x) <- 0, l cr$,
$mu[x] xarrowSquiggly(p)_write v$,
$cl sigma, mu cr
xarrow("WRITE" p)
cl sigma, mu[x <- v] cr$,
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ $s \; t$],
$cl sigma, mu cr
stretch(->)^s
cl sigma_s, mu_s cr$,
$cl sigma, mu cr
stretch(->)^t
cl sigma_t, mu_t cr$,
$cl sigma, mu, cr
xarrow(s \; t)
cl sigma_t, mu_t cr$,
) )
)) ))
@ -870,27 +793,26 @@ $ sigma in env, space mu in mem, space m in mode,
#let combine = `combine` #let combine = `combine`
*TODO: combine replacement* // FIXME
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ $s | t$], name: [ CHOICE $overline(s)$ $overline(t)$],
$cl sigma, mu, l cr $cl sigma, mu, l cr
stretch(->)^s attach(stretch(->)^overline(s), tr: *)
cl sigma_s, mu_s, l_s cr$, cl sigma_s, mu_s, l_s cr$,
$cl sigma, mu, l cr $cl sigma, mu, l cr
stretch(->)^t attach(stretch(->)^overline(t), tr: *)
cl sigma_t, mu_t, l_t cr$, cl sigma_t, mu_t, l_t cr$,
$l_t = l_s$,
$sigma_s = sigma_t$, $sigma_s = sigma_t$,
$mu' = combine(mu_s, mu_t)$,
// TODO changes ?? two ways ?? // TODO changes ?? two ways ??
$cl sigma, mu cr $cl sigma, mu, l cr
xarrow(s | t) xarrow("CHOICE" overline(s) space overline(t))
cl sigma_t, mu' cr$, cl sigma, combine(mu_s, mu_t), l cr$,
) )
)) ))
@ -898,16 +820,9 @@ $ sigma in env, space mu in mem, space m in mode,
=== Combination === Combination
*TODO: rewrite as rules, fix* // FIXME
$ combine(mu_1, mu_2)[i] = combine_e (mu_1[i], mu_2[i]) $ $ combine(mu_1, mu_2)[i] = combine_e (mu_1[i], mu_2[i]) $
$ combine_e (bot, bot) = bot $ $ combine_e (bot, bot) = bot $
$ combine_e (0, 0) = 0 $ $ combine_e (0, 0) = 0 $
$ combine_e (\_, \_) = \# $ $ combine_e (\_, \_) = X $
// FIXME: ref to combined memory
$ combine_e (rf c l_1, rf c' l_2) | c == c' = rf c combine_e(mu_1[l_1], mu_2[l_2])$
$ combine_e (v^1_1, ... v^1_n, v^2_1 ... v^2_n) = [combine_e(v^1_1, v^2_1), ..., combine_e(v^1_n, v^2_n)]$
$ combine_e (lambda space overline(t_1) space s_1, lambda space overline(t_2) space s_2) | overline(t_1) == overline(t_2) = lambda space overline(t_1) space s_1 $
// TODO: FIXME: statemient in lambda is not important ??
] ]