mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-04-26 16:24:50 +00:00
Compare commits
8 commits
0937d91f54
...
4eb3dea966
| Author | SHA1 | Date | |
|---|---|---|---|
|
4eb3dea966 | ||
|
|
22111a37ed | ||
|
|
5a33161117 | ||
|
|
eb90ba5449 | ||
|
|
9d21c99556 | ||
|
|
9d8dc1000c | ||
|
|
fd29f7d3da | ||
|
|
18d19051c4 |
1 changed files with 403 additions and 209 deletions
|
|
@ -9,7 +9,7 @@
|
|||
|
||||
#h(10pt)
|
||||
|
||||
// TODO: check correctnes for path, mem & type ??
|
||||
// TODO: check correctness for path, mem & type ??
|
||||
|
||||
== Syntax
|
||||
|
||||
|
|
@ -36,6 +36,7 @@
|
|||
#let Ref = `Ref`
|
||||
#let MaybeWrite = [$diamond$ `Write`]
|
||||
#let AlwaysWrite = [$square$ `Write`]
|
||||
#let NotWrite = [$not$ `Write`]
|
||||
#let Read = `Read`
|
||||
#let In = `In`
|
||||
#let Out = `Out`
|
||||
|
|
@ -111,14 +112,15 @@
|
|||
{
|
||||
Or[$()$][value of simple type] // `Unit`
|
||||
Or[$path$][value from variable] // `Path`
|
||||
Or[$rf expr$][reference expr] // `Ref`
|
||||
// TODO: FIXME: decide what is the result of ref expr eval
|
||||
// Or[$rf expr$][reference expr] // `Ref`
|
||||
Or[$[expr+]$][tuple expr] // `Prod`
|
||||
}
|
||||
),
|
||||
Prod(
|
||||
`stmt`,
|
||||
{
|
||||
Or[`CALL` $path space expr+$][call function]
|
||||
Or[`CALL` $path expr+$][call function]
|
||||
Or[`WRITE` $path$][write to variable]
|
||||
Or[`READ` $path$][read from variable]
|
||||
Or[$stmt ; stmt$][control flow operator, xecution ]
|
||||
|
|
@ -153,7 +155,7 @@
|
|||
Or[$0$][valid value of simple type] // `Unit`
|
||||
Or[$\#$][valid or spoiled value of simple type] // `Unit`
|
||||
Or[$bot$][spoiled value of simple type] // `Unit`
|
||||
Or[$lambda$][function pointer value] // `Fun`
|
||||
Or[$lambda overline(x) space stmt$][function pointer value] // `Fun`
|
||||
Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref`
|
||||
Or[$[deepValue+]$][tuple value] // `Prod`
|
||||
}
|
||||
|
|
@ -164,7 +166,7 @@
|
|||
Or[$0$][valid value of simple type] // `Unit`
|
||||
Or[$\#$][valid or spoiled value of simple type] // `Unit`
|
||||
Or[$bot$][spoiled value of simple type] // `Unit`
|
||||
Or[$lambda$][function pointer value] // `Fun`
|
||||
Or[$lambda overline(x) space stmt$][function pointer value] // `Fun`
|
||||
Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
|
||||
Or[$[value+]$][tuple value] // `Prod`
|
||||
}
|
||||
|
|
@ -204,17 +206,12 @@ $v in value$ - произвольное значение
|
|||
|
||||
== Semantics
|
||||
|
||||
// TODO: FIXME: add vars & funcs from global context in the beginnning
|
||||
|
||||
// $V := memelem$ - значения памяти
|
||||
|
||||
$X$ - можество переменных
|
||||
|
||||
// FIXME: TMP
|
||||
#let valuemem = `valuemem`
|
||||
#let memelem = `memelem`
|
||||
#let pathenvmode = `pathenvmode`
|
||||
#let pathenvval = `pathenvval`
|
||||
#let pathenvmem = `pathenvmem`
|
||||
#let pathenvtype = `pathenvtype`
|
||||
|
||||
#let vals = $Sigma$
|
||||
#let types = $Gamma$
|
||||
|
|
@ -246,18 +243,7 @@ $s in stmt, f in X, x in X, a in X$
|
|||
#let tmode = $attach(tack.r, br: mode)$
|
||||
|
||||
#let val = `val`
|
||||
#let label = `label`
|
||||
#let tval = $attach(tack.r, br: val)$
|
||||
#let tlabel = $attach(tack.r, br: label)$
|
||||
|
||||
// TODO: TMP, deprecated
|
||||
// #let tetype = $attach(tack.r.double, br: type)$
|
||||
// #let temode = $attach(tack.r.double, br: mode)$
|
||||
// #let telabel = $attach(tack.r.double, br: label)$
|
||||
|
||||
#let teval = $attach(tack.r.double, br: val)$
|
||||
|
||||
// TODO: env mem label ??, env mem value ??
|
||||
|
||||
- #[ Конструирование путей по переменой
|
||||
#align(center, prooftree(
|
||||
|
|
@ -363,70 +349,8 @@ $s in stmt, f in X, x in X, a in X$
|
|||
))
|
||||
]
|
||||
|
||||
// TODO: FIXME: not required (trivial) ??
|
||||
// - #[ Получение метки поля
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ access],
|
||||
|
||||
// $vals, mu tval p eqmu rf l$,
|
||||
// $vals, mu tmode p arrmu l$,
|
||||
// )
|
||||
// ))
|
||||
// ]
|
||||
|
||||
// TODO: not required (trivial) ??
|
||||
// - #[ Получение read-write тега поля по окружению
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ access],
|
||||
|
||||
// $x : types[x] tmode p -> cr r space w cl$,
|
||||
// $sigma temode p -> cr r space w cl$,
|
||||
// )
|
||||
// ))
|
||||
// ]
|
||||
|
||||
- #[ Получение значения поля по окружению
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ access],
|
||||
|
||||
$x eqmu vals[x] tval p eqmu v$,
|
||||
$types, vals, mu teval p eqmu x$,
|
||||
)
|
||||
))
|
||||
]
|
||||
|
||||
// FIXME: move to new mode model
|
||||
// === Mode Correctness
|
||||
|
||||
// Функции проверки тегов, имеют тип $mode -> #[bool]$:
|
||||
|
||||
// #let modevar = $(r space w space c space i space o)$
|
||||
|
||||
// $ 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 ??
|
||||
|
||||
=== Eval Rules
|
||||
|
||||
#let args = `args`
|
||||
|
||||
#[
|
||||
|
||||
#let ref = `ref`
|
||||
|
|
@ -451,6 +375,8 @@ $s in stmt, f in X, x in X, a in X$
|
|||
|
||||
=== Moded Type Correctness
|
||||
|
||||
*NOTE: скорее всего не нужна в таком виде, перенесено в spoil*
|
||||
|
||||
#let tcorrect = $attach(tack.r, br: #[correct])$
|
||||
|
||||
// TODO: FIXME: well formatness for mode, extract
|
||||
|
|
@ -529,36 +455,27 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
|
||||
=== Value Construction
|
||||
|
||||
// TODO: FIXME:add ref / copy modes correctness check
|
||||
// TODO: FIXME:add ref / copy modes correctness check ??
|
||||
|
||||
#let new = `new`
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ new $0$ value],
|
||||
name: [ new trivial read value],
|
||||
|
||||
// TODO: check that access is what required ??
|
||||
$cl 0, mu cr xarrowSquiggly(cl r\, w cr)_new cl 0, mu cr$,
|
||||
$v in {0, \#, bot}$,
|
||||
$cl v, mu cr xarrowSquiggly(cl Read \, w cr)_new cl v, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ new $\#$ value],
|
||||
name: [ new trivial $not$ read value],
|
||||
|
||||
// TODO: check that access is what required ??
|
||||
$cl \#, mu cr xarrowSquiggly(cl r\, w cr)_new cl \#, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ new $bot$ value],
|
||||
|
||||
$cl bot, mu cr xarrowSquiggly(cl r\, w cr)_new cl bot, mu cr$,
|
||||
$v in {0, \#, bot}$,
|
||||
$cl v, mu cr xarrowSquiggly(cl Read \, w cr)_new cl bot, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -611,40 +528,190 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
|
||||
=== Value Update
|
||||
|
||||
#let write = `write`
|
||||
#let modify = `modify`
|
||||
|
||||
*TODO: write to value*
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ modify trivial value],
|
||||
|
||||
=== Call Finalization
|
||||
|
||||
// FIXME: make connected to syntax
|
||||
*TODO*
|
||||
// $v in {0, \#, bot}$,
|
||||
// $cl v, mu cr xarrowSquiggly(cl \@ x \, b cr)_modify cl b, mu cr$,
|
||||
// )
|
||||
// ))
|
||||
|
||||
// TODO: add type check ??
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ spoil init],
|
||||
$mu stretch(=>)^nothing_(cl sigma, mu cr) mu$,
|
||||
name: [ modify end value],
|
||||
|
||||
// $v in {0, \#, bot}$,
|
||||
$cl v, mu cr xarrowSquiggly(cl \@ x \, b cr)_modify cl b, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ new reference copy value],
|
||||
|
||||
$cl mu[l], mu cr xarrowSquiggly(cl p \, b cr)_modify cl v', mu' cr$,
|
||||
$cl rf l, mu cr xarrowSquiggly(cl *p \, b cr)_modify cl rf l, mu'[l <- v'] cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ modify tuple value],
|
||||
|
||||
$cl v_i, mu cr xarrowSquiggly(cl p \, b cr)_modify cl v'_i, mu', cr$,
|
||||
$cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl p.i \, b cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
=== Value Combination
|
||||
|
||||
#let combine = `combine`
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ combine trivial $0$ values],
|
||||
|
||||
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl 0 \, 0 cr)_combine cl 0, mu cr$
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ combine trivial $bot$ values],
|
||||
|
||||
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl bot \, bot cr)_combine cl bot, mu cr$
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ combine other trivial values],
|
||||
|
||||
$v_1 in {0, \#, bot}$,
|
||||
$v_2 in {0, \#, bot}$,
|
||||
$v_1 != v_2$,
|
||||
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl v_1 \, v_2 cr)_combine cl \#, mu cr$
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ combine lambda values],
|
||||
|
||||
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl lambda \, lambda cr)_combine cl lambda, mu cr$
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ combine reference values (inplace)],
|
||||
|
||||
// NOTE: standalome version
|
||||
// $cl mu_1, mu_2, mu cr xarrowSquiggly(cl mu_1[l_1] \, mu_2[l_2] cr)_combine cl v', mu' cr$,
|
||||
// $mu' xarrowSquiggly(v')_#[add] cl rf l', mu'' cr$,
|
||||
// $cl mu_1, mu_2, mu cr xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l', mu'' cr$
|
||||
|
||||
// NOTE: version to use with "combine all"
|
||||
$l_1 = l_2$,
|
||||
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l_1, mu cr$
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ combine tuple values],
|
||||
|
||||
$cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl v^1_1 \, v^2_1 cr)_combine cl v'_1, mu'_1 cr$,
|
||||
$...$,
|
||||
$cl mu_1, mu_2, mu'_(n - 1) cr xarrowSquiggly(cl v^1_n \, v^2_n cr)_combine cl v'_n, mu'_n cr$,
|
||||
$cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl [v^1_1, ... v^1_n] \, [v^2_1 ... v^2_n] cr)_combine cl [v'_1, ... v'_n], mu'_n cr$
|
||||
)
|
||||
))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ combine tuple values],
|
||||
|
||||
$mu'_0 = []$,
|
||||
// NOTE: same labels required
|
||||
$mu_1 = {l_1 -> v^1_1, ... l_n -> v^1_n}$,
|
||||
$mu_2 = {l_1 -> v^2_1, ... l_n -> v^2_n}$,
|
||||
|
||||
$cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl v^1_1 \, v^2_1 cr)_combine cl v'_1, mu'_1 cr$,
|
||||
$...$,
|
||||
$cl mu_1, mu_2, mu'_(n - 1) cr xarrowSquiggly(cl v^1_n \, v^2_n cr)_combine cl v'_n, mu'_n cr$,
|
||||
|
||||
$cl mu_1, mu_2 cr xarrowSquiggly(space)_#[combine all] mu'_n cr$
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
=== Call Values Spoil
|
||||
|
||||
#let spoil = `spoil`
|
||||
|
||||
// TODO: FIXME: complete rule check
|
||||
#let tcorrectnew = $attach(tack.r.double, br: #[correct])$
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ correctness],
|
||||
|
||||
$r = Read => v = 0$,
|
||||
$r = Read => m = (In, \_)$,
|
||||
$m = (\_, Out) => w = AlwaysWrite$,
|
||||
$(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
|
||||
|
||||
$v in {0, \#, bot}$,
|
||||
|
||||
$ tcorrectnew cl v, r, w, r', w', m, c cr $,
|
||||
)
|
||||
))
|
||||
|
||||
// TODO: extract correctness
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ spoil step],
|
||||
|
||||
$mu stretch(=>)^args_sigma gamma$,
|
||||
$ tcorrectnew cl v, r, w, r', w', m, c cr $,
|
||||
|
||||
$isPossibleWrite mode$, // NOTE: weak requirement: may write
|
||||
$not isCopy mode$,
|
||||
$mode = (\_, not Out)$,
|
||||
|
||||
$isCorrect_(cl sigma, mu cr) (mode, x)$,
|
||||
|
||||
// gamma - memory (as mu)
|
||||
$gamma stretch(=>)^((mode, x) : args)_sigma pathenvval(gamma, sigma, x) <- bot]$
|
||||
$w = AlwaysWrite or w = MaybeWrite$,
|
||||
$v in {0, \#, bot}$,
|
||||
$cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, not Out) \, not Copy)_spoil cl bot, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -655,15 +722,11 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ fix step],
|
||||
|
||||
$mu stretch(=>)^args_sigma gamma$,
|
||||
$ tcorrectnew cl v, r, w, r', w', m, c cr $,
|
||||
|
||||
$isAlwaysWrite mode$, // NOTE: strong requirement: should write
|
||||
$mode = (\_, not Out)$,
|
||||
|
||||
$isCorrect_(cl sigma, mu cr) (mode, x)$,
|
||||
|
||||
// gamma - memory (as mu)
|
||||
$gamma stretch(=>)^((mode, x) : args)_sigma pathenvval(gamma, sigma, x) <- 0]$
|
||||
$w = AlwaysWrite$,
|
||||
$v in {0, \#, bot}$,
|
||||
$cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, Out) \, c)_spoil cl 0, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -674,49 +737,12 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ skip step],
|
||||
|
||||
$mu stretch(=>)^args_sigma gamma$,
|
||||
$ tcorrectnew cl v, r, w, r', w', m, c cr $,
|
||||
|
||||
$not "spoil step"$,
|
||||
$not "fix step"$,
|
||||
|
||||
$isCorrect_(cl sigma, mu cr) (mode, x)$,
|
||||
|
||||
// mu
|
||||
$gamma stretch(=>)^((mode, x) : args)_sigma gamma$
|
||||
)
|
||||
))
|
||||
|
||||
|
||||
#h(10pt)
|
||||
|
||||
=== Function Evaluation
|
||||
|
||||
// FIXME: make connected to syntax
|
||||
*TODO*
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ $(lambda a : t. d) m$],
|
||||
|
||||
// TODO: verify that type of m is t ??
|
||||
|
||||
$cl sigma [a <- (m, t)], mu, l cr
|
||||
xarrowSquiggly(t)
|
||||
cl sigma', mu', l' cr$,
|
||||
|
||||
$cl sigma', mu', l' cr
|
||||
xarrowDashed(d space @ space overline(y))
|
||||
cl sigma'', mu'', l'' cr$,
|
||||
|
||||
$isRead mode$,
|
||||
$not isCopy mode$,
|
||||
|
||||
// NOTE: correctness checked in CALL f
|
||||
|
||||
$cl sigma, mu, l cr
|
||||
xarrowDashed((lambda a. d) space @ space x space overline(y))
|
||||
cl sigma'', mu'', l'' cr$,
|
||||
$v in {0, \#, bot}$,
|
||||
$cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, not Out) \, c)_spoil cl v, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -725,17 +751,184 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [decl body],
|
||||
name: [ lambda step],
|
||||
|
||||
$cl sigma, mu, l cr
|
||||
attach(stretch(->)^overline(s), tr: *)
|
||||
cl sigma', mu', l' cr$,
|
||||
$cl lambda, mu cr xarrowSquiggly(lambda overline(t) \, lambda overline(t) \, m \, c)_spoil cl lambda, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
$d = overline(s)$,
|
||||
#h(10pt)
|
||||
|
||||
$cl sigma, mu, l cr
|
||||
xarrowDashed(d space @)
|
||||
cl sigma', mu', l' cr$,
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ reference step],
|
||||
|
||||
$cl mu[l], mu cr xarrowSquiggly(t \, t' m \, c')_spoil cl v', mu' cr$,
|
||||
// NOTE: copy mode of assigned type is not important (c'')
|
||||
$cl rf l, mu cr xarrowSquiggly(rf c' space t \, rf c'' space t' \, m \, c)_spoil cl rf l, mu'[l <- v'] cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ tuple step],
|
||||
|
||||
$cl v_1, mu cr xarrowSquiggly(t_1 \, t'_1 \, m \, c)_spoil cl v'_1, mu cr$,
|
||||
$...$,
|
||||
$cl v_n, mu cr xarrowSquiggly(t_n \, t'_n \, m \, c)_spoil cl v'_n, mu cr$,
|
||||
$cl [v_1, ... v_n], mu cr xarrowSquiggly([t_1, ... t_n] \, [t'_1, ... t'_n] \, m \, c)_spoil cl [v'_1, ... v'_n], mu' cr$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ full spoil],
|
||||
|
||||
$p arrpath x$,
|
||||
$l = vals[x]$,
|
||||
$vals, mu tval p eqmu b$,
|
||||
$types ttype p : t'$,
|
||||
// TODO: FIXME: Ref or Copy ?? in root <- Ref ??, because otherwise there could not b any Refs
|
||||
// FIXME depends on parent ??
|
||||
$cl b, mu cr xarrowSquiggly(t \, t' \, m \, Ref)_spoil cl b', mu' cr$,
|
||||
$cl mu[l], mu cr xarrowSquiggly(cl p \, b' cr)_modify cl v', mu' cr$,
|
||||
|
||||
$mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu'[l <- v']$,
|
||||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
=== Expression Evaluation
|
||||
|
||||
// TODO: check
|
||||
|
||||
#let eval = `eval`
|
||||
#let texpre = $attach(tack.r.double, br: eval)$
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ path type],
|
||||
|
||||
$vals, mu tval p eqmu v$,
|
||||
$vals, mu texpre p eqmu v$,
|
||||
)
|
||||
))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ unit value type],
|
||||
|
||||
$vals, mu texpre () eqmu 0$,
|
||||
)
|
||||
))
|
||||
|
||||
// NOTE: tmp removed
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ unit value type],
|
||||
|
||||
// $vals, mu texpre e : t$,
|
||||
|
||||
// [*TODO*],
|
||||
|
||||
// // TODO: reference to what ??
|
||||
// $vals, mu texpre rf e eqmu rf ??$,
|
||||
// )
|
||||
// ))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ unit value type],
|
||||
|
||||
$vals, mu texpre e_1 eqmu v_1$,
|
||||
$...$,
|
||||
$vals, mu texpre e_n eqmu v_n$,
|
||||
$vals, mu texpre [e_1, ... e_n] eqmu [v_1, ... v_n]$,
|
||||
)
|
||||
))
|
||||
|
||||
|
||||
=== Expresion Typing
|
||||
|
||||
// TODO: check
|
||||
|
||||
#let texprt = $attach(tack.r.double, br: type)$
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ path type],
|
||||
|
||||
$types ttype p : t$,
|
||||
$types texprt p : t$,
|
||||
)
|
||||
))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ unit value type],
|
||||
|
||||
$types texprt () : cl Read, NotWrite cr$,
|
||||
)
|
||||
))
|
||||
|
||||
// NOTE: tmp removed
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ unit value type],
|
||||
|
||||
// $types texprt e : t$,
|
||||
// // TODO: why Ref mode ?? <- due to immutability ??
|
||||
// $types texprt rf e : rf Ref t$,
|
||||
// )
|
||||
// ))
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ unit value type],
|
||||
|
||||
$types texprt e_1 : t_1$,
|
||||
$...$,
|
||||
$types texprt e_n : t_n$,
|
||||
$types texprt [e_1, ... e_n] : [t_1, ... t_n]$,
|
||||
)
|
||||
))
|
||||
|
||||
=== Function Argument Addition
|
||||
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ add argument],
|
||||
|
||||
|
||||
$vals, mu tval p eqmu v$,
|
||||
$types ttype p : t'$,
|
||||
// TODO: FIXME: check type compatibility for t and type for path p (?)
|
||||
[*TODO: check t ~ t' in sme way (?)*],
|
||||
$cl v', mu cr xarrowSquiggly(t)_new cl v, mu' cr$,
|
||||
|
||||
|
||||
// TODO save type mode somewhere ?? // <- not needed because is described by other params <- ??
|
||||
$cl types, vals, mu cr
|
||||
xarrowDashed(x space t space p)
|
||||
cl types[x <- t], vals[x <- v], mu' cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -743,23 +936,42 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
|
||||
=== Statement Evaluation
|
||||
|
||||
// FIXME: make connected to syntax
|
||||
*TODO: check type of lambda?, args from type?*
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ CALL $f space overline(p)$],
|
||||
name: [ CALL $f space [p_1, ... p_n]$],
|
||||
|
||||
$cl [], mu, l cr
|
||||
xarrowDashed(f space @ space overline(p))
|
||||
cl sigma', mu', l' cr$,
|
||||
$vals, mu texpre f eqmu lambda [x_1, ... x_n] space s$,
|
||||
$types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
|
||||
|
||||
// TODO: FIXME define args in some way
|
||||
$mu attach(stretch(=>)^args_sigma, tr: *) gamma$,
|
||||
// TODO: add args before statement eval
|
||||
|
||||
$cl sigma, mu, l cr
|
||||
xarrow("CALL" f space overline(p))
|
||||
cl sigma, gamma, l cr$,
|
||||
$types_0 = []$,
|
||||
$vals_0 = []$,
|
||||
$mu_0 = mu$,
|
||||
|
||||
// NOTE: dashed arrow to fill context
|
||||
$cl types_0, vals_0, mu_0, l cr
|
||||
xarrowDashed(x_1 space t_1 space p_1)
|
||||
cl types', vals_1, mu_1, l' cr$,
|
||||
$...$,
|
||||
$cl types_(n - 1), vals_(n - 1), mu_(n - 1), l cr
|
||||
xarrowDashed(x_n space t_n space p_n)
|
||||
cl types', vals_n, mu_n, l' cr$,
|
||||
|
||||
$cl types_n, vals_n, mu_n, l cr
|
||||
xarrow(s)
|
||||
cl types', vals', mu', l' cr$,
|
||||
|
||||
// NOTE: thick arrow to "spoil" context
|
||||
$gamma_0 = mu$,
|
||||
$gamma_0 stretch(=>)^(x_1 space m_1 space t_1 space p_1)_(cl vals, types cr) gamma_1$,
|
||||
$...$,
|
||||
$gamma_(n - 1) stretch(=>)^(m_n space t_n space p_n)_(cl vals, types cr) gamma_n$,
|
||||
|
||||
$cl vals, types, mu, l cr
|
||||
xarrow("CALL" f space [p_1, ... p_n])
|
||||
cl vals, types, gamma_n, l cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -770,7 +982,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ READ $p$],
|
||||
|
||||
$mu, types, vals teval p eqmu 0$,
|
||||
$mu, types, vals tval p eqmu 0$,
|
||||
|
||||
$cl types, vals, mu cr
|
||||
xarrow("READ" p)
|
||||
|
|
@ -783,16 +995,17 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ WRITE $x$],
|
||||
name: [ WRITE $p$],
|
||||
|
||||
$types ttype p : cl r, w cr$,
|
||||
$w = MaybeWrite or w = AlwaysWrite$,
|
||||
$p arrpath x$,
|
||||
$mu[x] xarrowSquiggly(p)_write v$,
|
||||
$l = vals(x)$,
|
||||
$mu[l] xarrowSquiggly(cl p \, 0 cr)_modify v'$,
|
||||
|
||||
$cl types, vals, mu cr
|
||||
xarrow("WRITE" p)
|
||||
cl types, vals, mu[x <- v] cr$,
|
||||
cl types, vals, mu[l <- v'] cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -819,9 +1032,6 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
|
||||
#h(10pt)
|
||||
|
||||
#let combine = `combine`
|
||||
|
||||
*TODO: combine replacement* // FIXME
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
|
|
@ -837,7 +1047,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
|
||||
$types_s = types_t$,
|
||||
$vals_s = vals_t$,
|
||||
$mu' = combine(mu_s, mu_t)$,
|
||||
$cl mu_s, mu_t cr xarrowSquiggly(space)_#[combine all] mu'$,
|
||||
|
||||
// TODO changes ?? two ways ??
|
||||
$cl types, vals, mu cr
|
||||
|
|
@ -846,20 +1056,4 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
)
|
||||
))
|
||||
|
||||
#h(10pt)
|
||||
|
||||
=== Combination
|
||||
|
||||
*TODO: rewrite as rules, fix* // FIXME
|
||||
|
||||
$ 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 (\_, \_) = \# $
|
||||
// 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 ??
|
||||
|
||||
]
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue