mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-06-10 19:28:16 +00:00
1736 lines
38 KiB
Typst
1736 lines
38 KiB
Typst
// #import "@preview/polylux:0.4.0": *
|
||
#import "@preview/simplebnf:0.1.1": *
|
||
// #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, xarrowSquiggly
|
||
|
||
= Формальная модель используемого языка
|
||
|
||
#h(10pt)
|
||
|
||
// TODO: check correctness for path, mem & type ??
|
||
|
||
== Syntax
|
||
|
||
// *TODO: top-level value copy mode ??* // TODO: FIXME
|
||
|
||
#h(10pt)
|
||
|
||
#let rf = $\& #h(3pt)$
|
||
|
||
#let isCorrect = `isCorrect`
|
||
|
||
#let isRead = `isRead`
|
||
#let isAlwaysWrite = `isAlwaysWrite`
|
||
#let isPossibleWrite = `isPossibleWrite`
|
||
#let isRef = `isRef`
|
||
#let isCopy = `isCopy`
|
||
|
||
#let readTag = `read`
|
||
#let writeTag = `write`
|
||
#let copyTag = `copy`
|
||
#let inTag = `in`
|
||
#let outTag = `out`
|
||
#let mode = `mode`
|
||
|
||
#let Copy = `Copy`
|
||
#let Ref = `Ref`
|
||
#let MaybeWrite = [$diamond$ `Write`]
|
||
#let AlwaysWrite = [$square$ `Write`]
|
||
#let NotWrite = [$not$ `Write`]
|
||
#let Read = `Read`
|
||
#let In = `In`
|
||
#let Out = `Out`
|
||
|
||
#let cl = $chevron.l$
|
||
#let cr = $chevron.r$
|
||
|
||
#let cdl = $chevron.l.double$
|
||
#let cdr = $chevron.r.double$
|
||
|
||
#let expr = `expr`
|
||
#let stmt = `stmt`
|
||
#let decl = `decl`
|
||
#let prog = `prog`
|
||
#let path = `path`
|
||
#let type = `type`
|
||
#let modedType = `modedtype`
|
||
#bnf(
|
||
Prod(`read`,
|
||
// NOTE: not three modalities for write, because read does not change value
|
||
// => it is not important to observe rsult, no differenc between always and maybe
|
||
{ Or[Read][read passed value]
|
||
Or[$not$ Read][] } ),
|
||
Prod(`write`,
|
||
{ Or[$square$ Write][in all cases there is a write to the variable] // always write, requre at least one write in each flow variant
|
||
Or[$diamond$ Write][in some cases there is a write to the variable] // possible write, no requirements (?)
|
||
Or[$not$ Write][in none cases there is a write to the variable ] } ), // no write, require n owrites in all flow variants
|
||
Prod(`copy`,
|
||
{ Or[Ref][pass reference to the value]
|
||
Or[Value][pass copy of the value] } ),
|
||
Prod(`in`,
|
||
{ Or[In][parameter value used as input]
|
||
Or[$not$ In][] } ),
|
||
Prod(`out`,
|
||
{ Or[Out][parameter value returned]
|
||
Or[$not$ Out][] } ),
|
||
Prod(
|
||
`mode`,
|
||
{
|
||
Or[$inTag outTag$][]
|
||
}
|
||
),
|
||
Prod(
|
||
`path`,
|
||
{
|
||
// NOTE: global vars & local vars names could be used with one constructor
|
||
// Or[$\#x$][funciton or global variable itself]
|
||
Or[$@ X$][function argument or variable itself]
|
||
Or[$* path$][reference insede path]
|
||
Or[$path . n$][access $n$-th cell of the tuple]
|
||
// Or[$path : n$][access $n$-th cell of the union] // TODO: another notation ??
|
||
}
|
||
),
|
||
Prod(
|
||
`type`,
|
||
{
|
||
Or[$cl readTag, writeTag cr$][simple type representing all primitive types] // `Unit`
|
||
Or[$rf copyTag type$][reference to structure, contains copy / ref choice] // `Ref`
|
||
Or[$[type+]$][tuple type] // `Prod`
|
||
// Or[`type` $times$ `type`][pair type, allows to make tuples] // `Prod`
|
||
// Or[`type` $+$ `type`][union type (important in some way ???)] // `Sum` // TODO ?
|
||
|
||
// NOTE: do not use names in type
|
||
// 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`
|
||
}
|
||
),
|
||
Prod(
|
||
`modedtype`,
|
||
{
|
||
Or[$mode type$][type woth in and out modifiers]
|
||
}
|
||
),
|
||
Prod(
|
||
`expr`,
|
||
{
|
||
Or[$()$][value of simple type] // `Unit`
|
||
Or[$path$][value from variable] // `Path`
|
||
// TODO FIXME: expand to support arbitrary paths (that do lead to lvalue)
|
||
// add relation to calc lvalue / rvalue for each element ?
|
||
Or[$rf X$][reference expr] // `Ref`
|
||
Or[$[expr+]$][tuple expr] // `Prod`
|
||
}
|
||
),
|
||
Prod(
|
||
`stmt`,
|
||
{
|
||
Or[`SKIP`][do nothing]
|
||
Or[`CALL` $path expr+$][call function]
|
||
Or[`WRITE` $path$][write to variable]
|
||
Or[`READ` $path$][read from variable]
|
||
Or[$stmt ; stmt$][sequence of two statements]
|
||
Or[$stmt | stmt$][choice between the statements]
|
||
}
|
||
),
|
||
Prod(
|
||
`decl`,
|
||
{
|
||
// TODO: path not allowed ??
|
||
// Or[$"var" X : type = expr$][global variable declaration]
|
||
Or[$"fun" X ((X : modedType)+) = stmt$][function declaration]
|
||
}
|
||
),
|
||
Prod(
|
||
`prog`,
|
||
{
|
||
Or[$decl+$][all program definitions]
|
||
}
|
||
),
|
||
)
|
||
|
||
== Value Model
|
||
|
||
// #let deepValue = `deepvalue`
|
||
#let value = `value`
|
||
#let vmem = $v_#[`mem`]$
|
||
#let vread = $v_#[`read`]$
|
||
#let vwrite = $v_#[`write`]$
|
||
#let revpath = $#[`path`]_#[`rev`]$
|
||
|
||
#bnf(
|
||
// Prod(
|
||
// $deepValue$,
|
||
// {
|
||
// 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 space (X+ stmt)+$][function pointer value, set of possible values] // `Fun`
|
||
// Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref`
|
||
// Or[$[deepValue+]$][tuple value] // `Prod`
|
||
// }
|
||
// ),
|
||
Prod(
|
||
$vmem$,
|
||
{
|
||
Or[$0$][valid value of simple type]
|
||
Or[$?$][valid or spoiled value of simple type]
|
||
Or[$bot$][spoiled value of simple type]
|
||
// NOTE: proably can't use correctly
|
||
// Or[$top$][value that is not spoiled because of the copy tag]
|
||
}
|
||
),
|
||
Prod(
|
||
$vread$,
|
||
{
|
||
Or[$0_r$][argument not read]
|
||
Or[$1_r$][argument read]
|
||
Or[$top_r$][argument already written from the function beginning]
|
||
}
|
||
),
|
||
Prod(
|
||
$vwrite$,
|
||
{
|
||
Or[$0_w$][no write]
|
||
Or[$?_w$][maybe write]
|
||
Or[$1_w$][always write]
|
||
}
|
||
),
|
||
Prod(
|
||
$value_mu$,
|
||
{
|
||
Or[$cdl vmem, vread, vwrite cdr$][value of the simple type, contains cells for analysis] // `Unit`
|
||
Or[$lambda$][function pointer value, carries no information] // `Fun`
|
||
Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
|
||
Or[$[value+]$][tuple value] // `Prod`
|
||
}
|
||
),
|
||
)
|
||
|
||
// #deepValue - полное значение,
|
||
#value - слой значения, привязан к конкретной памяти $mu$
|
||
|
||
Значения, могут лежать в переменных и передаваться как аргументы функций (то, во что вычисляется $expr$)
|
||
|
||
$v in value$ - произвольное значение
|
||
|
||
// Получение #deepValue по #value:
|
||
// - $rf l xarrowSquiggly(mu)_#[deep] rf mu[l]$
|
||
// - $* xarrowSquiggly(mu)_#[deep] *$
|
||
// где $*$ - произвольный конструктор значения, кроме $rf$
|
||
|
||
== Memory Model
|
||
|
||
#let mem = `mem`
|
||
|
||
- $LL$ - множество меток памяти
|
||
- $mem := LL -> value, space mu : mem$ - память, частично определённая функция
|
||
- $l in LL$ - новый тег памяти (ранее не использованный)
|
||
- `next` - получение следующей неиспользованной метки в памяти
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ add value to memory],
|
||
|
||
$l = #[next] (mu)$,
|
||
|
||
$mu xarrowSquiggly(v)_#[add] cl l, mu [l <- v] cr$,
|
||
)
|
||
))
|
||
|
||
== Semantics
|
||
|
||
#let action = `action`
|
||
#let readA = $#[`READ`]_a$
|
||
#let writeA = $#[`WRITE`]_a$
|
||
#let mbwriteA = $#[`MAYWRITE`]_a$
|
||
// #let spoilA = $#[`SPOIL`]_a$
|
||
// #let nospoilA = $#[`NOSPOIL`]_a$
|
||
|
||
#bnf(
|
||
Prod(
|
||
revpath,
|
||
{
|
||
Or[$\# .$][value by itself]
|
||
Or[$rf revpath$][reference to value]
|
||
Or[$n . revpath$][tuple with value as $n$-th element]
|
||
}
|
||
),
|
||
Prod(
|
||
$action$,
|
||
{
|
||
Or[$readA$][value read]
|
||
Or[$writeA$][value written]
|
||
Or[$mbwriteA$][value maybe written]
|
||
// NOTE: not required, spoils only first element ?
|
||
// Or[$spoilA$][value passed as funciton argument and spoiled]
|
||
// NOTE: probably acutally can't reliebly forbid Cp
|
||
// Or[$nospoilA$][value passed as funciton argument and not changed,
|
||
// but could be spoiled if mode will be $Copy$ instead of $Ref$]
|
||
// TODO: better wording ??
|
||
}
|
||
),
|
||
)
|
||
|
||
// $V := memelem$ - значения памяти
|
||
|
||
$X$ - можество переменных
|
||
|
||
#let vals = $Sigma$
|
||
#let types = $Gamma$
|
||
#let envv = $#[env]_Sigma$
|
||
#let envt = $#[env]_Gamma$
|
||
$envv := X -> LL, space vals : envv$ - #[ метки памяти перменных контекста, частично определённая функция ]
|
||
$envt := X -> type, space types : envt$ - #[ типы значений перменных контекста, частично определённая функция ]
|
||
|
||
$revpath$ - путь в обратную сторону, используется для обновления значений
|
||
|
||
$action$ - действия, совершаемые с примитивным значением,
|
||
модифицирующие содержащуюся таминформацию
|
||
|
||
- $r in readTag, w in writeTag$
|
||
- $c in copyTag$
|
||
- $i in inTag, o in outTag$
|
||
- $s in stmt$
|
||
- $f, x, a in X$
|
||
- $a in action$
|
||
- $p in path$
|
||
- $v in value$
|
||
- $v_m in vmem, v_r in vread, v_w in vwrite$
|
||
- $t, u in type$
|
||
- $pi in revpath$
|
||
|
||
=== Path Accessors
|
||
|
||
Набор частично определённых фунций для работы с путями.
|
||
Для удобства значение, получаемое из текущего применением пути, будем называть полем.
|
||
// Все эти функции используются с префиксом `path.`.
|
||
|
||
#let eqmu = $attach(=, br: mu)$
|
||
#let arrmu = $attach(->, br: mu)$
|
||
|
||
#let arrpath = $xarrowSquiggly(space)_path$
|
||
#let arrrevpath = $xarrowSquiggly(space)_#[rev path]$
|
||
|
||
#let ttype = $attach(tack.r, br: type)$
|
||
#let tmode = $attach(tack.r, br: mode)$
|
||
|
||
#let val = `val`
|
||
#let tval = $attach(tack.r, br: val)$
|
||
|
||
- #[ Соответствующая пути переменная
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ variable path],
|
||
|
||
$@x arrpath x$,
|
||
)
|
||
))
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ reference path],
|
||
|
||
$p arrpath x$,
|
||
$* p arrpath x$,
|
||
)
|
||
))
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ tuple access path],
|
||
|
||
$p arrpath x$,
|
||
|
||
$p.i arrpath x$,
|
||
)
|
||
))
|
||
]
|
||
|
||
- #[ Обращение пути
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ variable path],
|
||
|
||
$@x arrrevpath^pi pi$,
|
||
)
|
||
))
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ reference path],
|
||
|
||
$p arrrevpath^(rf pi) pi'$,
|
||
$*p arrrevpath^pi pi'$,
|
||
)
|
||
))
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ tuple access path],
|
||
|
||
$p arrrevpath^(i.pi) pi'$,
|
||
|
||
$p.i arrrevpath^pi pi'$,
|
||
)
|
||
))
|
||
]
|
||
|
||
- #[ Получение типа поля
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ variable type access],
|
||
|
||
$x : t_x in types$,
|
||
$types ttype @x : t_x$,
|
||
)
|
||
))
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ reference type access],
|
||
|
||
$types ttype p : rf mode t_p$,
|
||
$types ttype *p : t_p$,
|
||
)
|
||
))
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ tuple type access],
|
||
|
||
$types ttype p : [t_1, ... t_n]$,
|
||
$types ttype p.i : t_i$,
|
||
)
|
||
))
|
||
]
|
||
|
||
// TODO: not required (trivial) ??
|
||
// - #[ Получение read-write тега поля
|
||
// #align(center, prooftree(
|
||
// vertical-spacing: 4pt,
|
||
// rule(
|
||
// name: [ rw tag access],
|
||
|
||
// $types ttype p : cl r, w cr$,
|
||
// $types tmode p -> cl r, w cr$,
|
||
// )
|
||
// ))
|
||
// ]
|
||
|
||
- #[ Получение значения поля
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ variable value access],
|
||
|
||
$x -> l in vals$,
|
||
$mu[l] = v$,
|
||
$vals, mu tval x eqmu v$,
|
||
)
|
||
))
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ reference value access],
|
||
|
||
$vals, mu tval p eqmu rf l$,
|
||
$vals, mu tval *p eqmu mu[l]$,
|
||
)
|
||
))
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ tuple value access],
|
||
|
||
$vals, mu tval p eqmu [v_1, ... v_n]$,
|
||
$vals, mu tval p.i eqmu v_i$,
|
||
)
|
||
))
|
||
]
|
||
|
||
=== Eval Rules
|
||
|
||
#[
|
||
|
||
#let ref = `ref`
|
||
#let copy = `copy`
|
||
#let read = `read`
|
||
|
||
// #align(center, grid(
|
||
// columns: 3,
|
||
// gutter: 5%,
|
||
// align(bottom, prooftree(
|
||
// ...
|
||
// )),
|
||
// align(bottom, prooftree(
|
||
// ...
|
||
// )),
|
||
// align(bottom, prooftree(
|
||
// ...
|
||
// )),
|
||
// ))
|
||
|
||
// TODO: introduce spep env argument ??
|
||
|
||
// --- >>> ---
|
||
// === Moded Type Correctness
|
||
// *NOTE: скорее всего не нужна в таком виде, перенесено в spoil*
|
||
// #let tcorrect = $attach(tack.r, br: #[correct])$
|
||
// $ vals in envv, types in envt, space mu in mem, space m in mode,
|
||
// 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)
|
||
// // TODO: FIXME: complete rule check
|
||
// // + add part about ref -> not copy later
|
||
// #align(center, prooftree(
|
||
// vertical-spacing: 4pt,
|
||
// rule(
|
||
// name: [ unit assignment tags correctness],
|
||
// $r = Read => m = (In, \_)$,
|
||
// $m = (\_, Out) => w = AlwaysWrite$,
|
||
// // $sigma temode x -> cr r' space w' cl$, // NOTE: not required, value passed
|
||
// $(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
|
||
// // $sigma, mu teval x eqmu v$, // NOTE: not required, value passed
|
||
// $v in {0, ?, bot}$,
|
||
// $r = Read => v = 0$,
|
||
// $types, vals, mu, m, c tcorrect v : cl r', w' cr -> cl r, w cr$,
|
||
// )
|
||
// ))
|
||
// #h(10pt)
|
||
// #align(center, prooftree(
|
||
// vertical-spacing: 4pt,
|
||
// rule(
|
||
// name: [ function pointer tags correctness],
|
||
// $types, vals, mu, m, c tcorrect lambda : lambda space overline(t) -> lambda space overline(t)$,
|
||
// )
|
||
// ))
|
||
// #h(10pt)
|
||
// #align(center, prooftree(
|
||
// vertical-spacing: 4pt,
|
||
// rule(
|
||
// name: [ ref assignment tags correctness],
|
||
// $types, vals, mu, m, c_r tcorrect v : t -> t'$,
|
||
// // TODO: FIXME: which tag translations are correct ?? <- only assignee?
|
||
// $types, vals, mu, m, c tcorrect rf space v : rf c' space t -> rf c_r space t'$,
|
||
// )
|
||
// ))
|
||
// #h(10pt)
|
||
// #align(center, prooftree(
|
||
// vertical-spacing: 4pt,
|
||
// rule(
|
||
// name: [ tuple assignmenttags correctness],
|
||
// $types, vals, mu, m, c tcorrect v_1 : t_1 -> t'_1$,
|
||
// $...$,
|
||
// $types, vals, mu, m, c tcorrect v_n : t_n -> t'_n$,
|
||
// $types, vals, mu, m, c tcorrect [v_1, ... v_n] : [t_1, ..., t_n] -> [t'_1, ... t'_n]$,
|
||
// )
|
||
// ))
|
||
// #h(10pt)
|
||
// --- <<< ---
|
||
|
||
=== Value Construction
|
||
|
||
#let build = `build`
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ build trivial read value],
|
||
|
||
$mu xarrowSquiggly(cl Read \, w cr)_build
|
||
cl cdl 0_m, 0_r, 0_w cdr, mu cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ build trivial $not$ read value],
|
||
|
||
$mu xarrowSquiggly(cl not Read \, w cr)_build
|
||
cl cdl bot, 0_r, 0_w cdr, mu cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
// TODO: function pointer type ??
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ build funciton pointer value],
|
||
|
||
$cl mu cr xarrowSquiggly(lambda space c space overline(t))_build cl lambda, mu cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ build reference value],
|
||
|
||
$mu xarrowSquiggly(t)_build cl v, mu_v cr$,
|
||
|
||
$mu_v xarrowSquiggly(v)_#[add] cl l, mu_a cr$,
|
||
|
||
$mu xarrowSquiggly(rf c t)_build cl rf l, mu_a cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ build tuple value],
|
||
|
||
$mu_0 xarrowSquiggly(t_1)_build cl v_1, mu_1 cr$,
|
||
$...$,
|
||
$mu_(n - 1) xarrowSquiggly(t_n)_build cl v_n, mu_n cr$,
|
||
|
||
$mu_0 xarrowSquiggly([t_1, ... t_n])_build cl [v_1, ... v_n], mu_n cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
// ---
|
||
|
||
// TODO: FIXME:add ref / copy modes correctness check ??
|
||
|
||
// #let copy = `copy`
|
||
|
||
// #align(center, prooftree(
|
||
// vertical-spacing: 4pt,
|
||
// rule(
|
||
// name: [ new trivial read value],
|
||
|
||
// // NOTE: should not be important to copy v_m, because spoil & tags
|
||
// // should care for this instead
|
||
// $v_m in {0, ?, bot}$,
|
||
// $cl cdl v_m, v_r, v_w cdr, mu cr
|
||
// xarrowSquiggly(cl Read \, w cr)_copy
|
||
// cl cdl v_m, 0_r, 0_w cdr, mu cr$,
|
||
// )
|
||
// ))
|
||
|
||
// #h(10pt)
|
||
|
||
// #align(center, prooftree(
|
||
// vertical-spacing: 4pt,
|
||
// rule(
|
||
// name: [ new trivial $not$ read value],
|
||
|
||
// $v_m in {0, ?, bot/*, top */}$,
|
||
// $cl cdl v_m, v_r, v_w cdr, mu cr
|
||
// xarrowSquiggly(cl not Read \, w cr)_copy
|
||
// cl cdl bot, 0_r, 0_w cdr, mu cr$,
|
||
// )
|
||
// ))
|
||
|
||
// #h(10pt)
|
||
|
||
// #align(center, prooftree(
|
||
// vertical-spacing: 4pt,
|
||
// rule(
|
||
// name: [ new funciton pointer value],
|
||
|
||
// $cl lambda, mu cr xarrowSquiggly(lambda space c space overline(t))_copy cl lambda, mu cr$,
|
||
// )
|
||
// ))
|
||
|
||
// #h(10pt)
|
||
|
||
// NOTE: due to new memory cells types (with rw subcells) valnue should always be copied
|
||
// #align(center, prooftree(
|
||
// vertical-spacing: 4pt,
|
||
// rule(
|
||
// name: [ new reference /* copy */ value],
|
||
|
||
// $cl mu[l], mu cr xarrowSquiggly(t)_copy cl v, mu_v cr$,
|
||
|
||
// $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
|
||
|
||
// $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_copy cl rf l', mu_a cr$,
|
||
// )
|
||
// ))
|
||
|
||
// #h(10pt)
|
||
|
||
// #align(center, prooftree(
|
||
// vertical-spacing: 4pt,
|
||
// rule(
|
||
// name: [ new tuple value],
|
||
|
||
// $cl v_1, mu_0 cr xarrowSquiggly(t_1)_copy cl v'_1, mu_1 cr$,
|
||
// $...$,
|
||
// $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_copy cl v'_n, mu_n cr$,
|
||
|
||
// $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_copy cl [v'_1, ... v'_n], mu_n cr$,
|
||
// )
|
||
// ))
|
||
|
||
=== Action Rules
|
||
|
||
#let modM = $attach(<-, br: m)$
|
||
#let modR = $attach(<-, br: r)$
|
||
#let modW = $attach(<-, br: w)$
|
||
|
||
#align(center, grid(
|
||
columns: 3,
|
||
gutter: 10%,
|
||
align: center,
|
||
table(
|
||
columns: 3,
|
||
table.header(
|
||
[*a*], [*x*], $modM$
|
||
),
|
||
$readA$, $0$, $0$,
|
||
// $readA$, $top$, $0$,
|
||
$readA$, $?$, $-$, // err
|
||
$readA$, $bot$, $-$, // err
|
||
$writeA$, $0$, $0$,
|
||
// $writeA$, $top$, $-$,
|
||
$writeA$, $?$, $0$,
|
||
$writeA$, $bot$, $0$,
|
||
$mbwriteA$, $0$, $0$,
|
||
// $mbwriteA$, $top$, $top$,
|
||
$mbwriteA$, $?$, $?$,
|
||
$mbwriteA$, $bot$, $?$,
|
||
// $spoilA$, $0$, $bot$,
|
||
// // $spoilA$, $top$, $bot$,
|
||
// $spoilA$, $?$, $bot$,
|
||
// $spoilA$, $bot$, $bot$,
|
||
// $nospoilA$, $0$, $top$,
|
||
// $nospoilA$, $top$, $top$,
|
||
// $nospoilA$, $?$, $-$, // ??
|
||
// $nospoilA$, $bot$, $-$,
|
||
),
|
||
|
||
table(
|
||
columns: 3,
|
||
table.header(
|
||
[*a*], [*x*], $modR$
|
||
),
|
||
$readA$, $1$, $1$,
|
||
$readA$, $0$, $1$,
|
||
$readA$, $top$, $top$,
|
||
$writeA$, $1$, $1$,
|
||
$writeA$, $0$, $top$,
|
||
$writeA$, $top$, $top$,
|
||
$mbwriteA$, $1$, $1$,
|
||
$mbwriteA$, $0$, $0$,
|
||
$mbwriteA$, $top$, $top$,
|
||
|
||
// $spoilA$, $1$, $1$,
|
||
// $spoilA$, $0$, $0$,
|
||
// $spoilA$, $top$, $top$,
|
||
// $nospoilA$, $1$, $1$,
|
||
// $nospoilA$, $0$, $0$,
|
||
// $nospoilA$, $top$, $top$,
|
||
),
|
||
|
||
table(
|
||
columns: 3,
|
||
table.header(
|
||
[*a*], [*x*], $modW$
|
||
),
|
||
$readA$, $1$, $1$,
|
||
$readA$, $?$, $?$,
|
||
$readA$, $0$, $0$,
|
||
$writeA$, $1$, $1$,
|
||
$writeA$, $?$, $1$,
|
||
$writeA$, $0$, $1$,
|
||
$mbwriteA$, $1$, $1$,
|
||
$mbwriteA$, $?$, $?$,
|
||
$mbwriteA$, $0$, $?$,
|
||
|
||
// $spoilA$, $1$, $1$,
|
||
// $spoilA$, $?$, $?$,
|
||
// $spoilA$, $0$, $0$,
|
||
// $nospoilA$, $1$, $1$,
|
||
// $nospoilA$, $?$, $?$,
|
||
// $nospoilA$, $0$, $0$,
|
||
)
|
||
))
|
||
|
||
Прочерк \"$-$\" означает, что данная операция не определена.
|
||
|
||
=== Value Update
|
||
|
||
==== Change
|
||
|
||
Замена подзначения в значении по $revpath$, $b in value$.
|
||
|
||
#let change = `change`
|
||
|
||
// TODO: add type check ??
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ change final value],
|
||
|
||
// $v in {0, ?, bot}$,
|
||
$cl v, mu cr xarrowSquiggly(cl \# . \, b cr)_change cl b, mu cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ change reference value],
|
||
|
||
$cl mu[l], mu cr xarrowSquiggly(cl pi \, b cr)_change cl v', mu' cr$,
|
||
$cl rf l, mu cr xarrowSquiggly(cl rf pi \, b cr)_change cl rf l, mu'[l <- v'] cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ change tuple value],
|
||
|
||
$cl v_i, mu cr xarrowSquiggly(cl p \, b cr)_change cl v'_i, mu', cr$,
|
||
$cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl i.pi \, b cr)_change cl [v_1, ... v'_i, ... v_n], mu' cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
==== Modify
|
||
|
||
Совершение операции над тривиальным подзначением в значении по $revpath$, $a in action$
|
||
|
||
#let modify = `modify`
|
||
|
||
// TODO: add type check ??
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ modify final value: unit],
|
||
|
||
$cl cdl v_m, v_r, v_w cdr, mu cr
|
||
xarrowSquiggly(cl \# . \, a cr)_modify
|
||
cl cdl v_m modM a, v_r modR a, v_w modW a cdr, mu cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ modify final value: ref],
|
||
|
||
$cl mu[l], mu cr xarrowSquiggly(cl \# . \, a cr)_modify cl v', mu' cr$,
|
||
$cl rf l, mu cr xarrowSquiggly(cl \# . \, a cr)_modify cl rf l, mu'[l <- v'] cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ modify final value: tuple],
|
||
|
||
$cl v_1, mu_0 cr xarrowSquiggly(cl \# . \, a cr)_modify cl v'_1, mu_1, cr$,
|
||
$...$,
|
||
$cl v_n, mu_(n - 1) cr xarrowSquiggly(cl \# . \, a cr)_modify cl v'_n, mu_n, cr$,
|
||
$cl [v_1, ... v_n], mu cr xarrowSquiggly(cl \# . \, a cr)_modify cl [v'_1, ... v'_n], mu_n cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ modify reference value],
|
||
|
||
$cl mu[l], mu cr xarrowSquiggly(cl pi \, a cr)_modify cl v', mu' cr$,
|
||
$cl rf l, mu cr xarrowSquiggly(cl rf pi \, a 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 pi \, a cr)_modify cl v'_i, mu', cr$,
|
||
$cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl i.pi \, a cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
=== Value Combination
|
||
|
||
#align(center, grid(
|
||
columns: 3,
|
||
gutter: 20%,
|
||
align: center,
|
||
table(
|
||
columns: 3,
|
||
table.header(
|
||
[*x*], [*y*], $plus.o_m$
|
||
),
|
||
$0$, $0$, $0$,
|
||
// $0$, $top$, $0$,
|
||
$0$, $?$, $?$,
|
||
$0$, $bot$, $?$,
|
||
$?$, $0$, $?$,
|
||
$?$, $?$, $?$,
|
||
$?$, $bot$, $?$,
|
||
// $?$, $top$, $?$,
|
||
$bot$, $0$, $?$,
|
||
$bot$, $?$, $?$,
|
||
// $bot$, $top$, $?$,
|
||
// $top$, $0$, $?$,
|
||
// $top$, $?$, $?$,
|
||
// $top$, $bot$, $?$,
|
||
$bot$, $bot$, $bot$,
|
||
// $top$, $top$, $top$,
|
||
),
|
||
|
||
table(
|
||
columns: 3,
|
||
table.header(
|
||
[*x*], [*y*], $plus.o_r$
|
||
),
|
||
$1$, $1$, $1$,
|
||
$1$, $0$, $1$,
|
||
$1$, $top$, $1$,
|
||
$0$, $1$, $1$,
|
||
$top$, $1$, $1$,
|
||
$0$, $0$, $0$,
|
||
$0$, $top$, $0$,
|
||
$top$, $0$, $0$,
|
||
$top$, $top$, $top$,
|
||
),
|
||
|
||
table(
|
||
columns: 3,
|
||
table.header(
|
||
[*x*], [*y*], $plus.o_w$
|
||
),
|
||
$1$, $1$, $1$,
|
||
$1$, $?$, $?$,
|
||
$1$, $0$, $?$,
|
||
$?$, $1$, $?$,
|
||
$?$, $?$, $?$,
|
||
$?$, $0$, $?$,
|
||
$0$, $1$, $?$,
|
||
$0$, $?$, $?$,
|
||
$0$, $0$, $0$,
|
||
)
|
||
))
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ combine trivial values],
|
||
|
||
$v_1 = cdl v_1_m, v_1_r, v_1_w cdr$,
|
||
$v_2 = cdl v_2_m, v_2_r, v_2_w cdr$,
|
||
$v_1 plus.o v_2 = cdl v_1_m plus.o_m v_2_m, v_1_r plus.o_r v_2_r, v_1_w plus.o_w v_2_w cdr$
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ combine lambda values],
|
||
|
||
$lambda plus.o lambda = lambda$
|
||
)
|
||
))
|
||
|
||
#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$,
|
||
$rf l_1 plus.o rf l_2 = rf l_1$
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ combine tuple values],
|
||
|
||
$v^1_1 plus.o v^2_1 = v'_1$,
|
||
$...$,
|
||
$v^1_n plus.o v^2_n = v'_n$,
|
||
$[v^1_1, ... v^1_n] plus.o [v^2_1 ... v^2_n] = [v'_1, ... v'_n]$
|
||
)
|
||
))
|
||
|
||
#let dom = `dom`
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ combine memory],
|
||
|
||
$dom mu_1 = dom mu_2$,
|
||
|
||
$mu_1 plus.o mu_2 = l -> mu_1[l] plus.o mu_2[l]$
|
||
)
|
||
))
|
||
|
||
#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: [ unit expr value],
|
||
|
||
$vals, mu texpre () eqmu cdl 0_m, 0_r, 0_w cdr$,
|
||
)
|
||
))
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ path expr value],
|
||
|
||
$vals, mu tval p eqmu v$,
|
||
$vals, mu texpre p eqmu v$,
|
||
)
|
||
))
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ ref expr value],
|
||
|
||
$vals, mu texpre rf x eqmu rf vals[x]$,
|
||
)
|
||
))
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ tuple expr value],
|
||
|
||
$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: [ unit value expr type],
|
||
|
||
$types texprt () : cl Read, NotWrite cr$,
|
||
)
|
||
))
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ path expr type],
|
||
|
||
$types ttype p : t$,
|
||
$types texprt p : t$,
|
||
)
|
||
))
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ ref expr type],
|
||
|
||
$types texprt rf x : rf Ref types[x]$,
|
||
)
|
||
))
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ tuple expr type],
|
||
|
||
$types texprt e_1 : t_1$,
|
||
$...$,
|
||
$types texprt e_n : t_n$,
|
||
$types texprt [e_1, ... e_n] : [t_1, ... t_n]$,
|
||
)
|
||
))
|
||
|
||
=== Context Initialization
|
||
|
||
#let init = `init`
|
||
|
||
// #align(center, prooftree(
|
||
// vertical-spacing: 4pt,
|
||
// rule(
|
||
// name: [ add variable declaration],
|
||
|
||
// // NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers)
|
||
// // expect well typed program
|
||
|
||
// $vals, mu texpre e eqmu v$,
|
||
// $cl v, mu cr xarrowSquiggly(t)_copy cl v', mu' cr$, // TODO: FIXME check (required?)
|
||
// $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$,
|
||
|
||
// $cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu'' cr$
|
||
// )
|
||
// ))
|
||
|
||
// #h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ add function declaration],
|
||
|
||
$mu xarrowSquiggly(lambda)_#[add] cl l, mu' cr$,
|
||
|
||
$cl types, vals, mu cr
|
||
xarrowSquiggly("fun" f (x_1 space : space m_1 t_1, ... space x_n space : space m_n t_n) space = space s)_init
|
||
cl types[f <- lambda space [t_1, ... t_n]], vals[f <- l], mu' cr$
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
=== Call Values Spoil
|
||
|
||
#let spoil = `spoil`
|
||
#let tryread = `try read`
|
||
#let tryspoil = `try spoil`
|
||
|
||
#let tcorrectnew = $attach(tack.r.double, br: #[correct])$
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ correctness],
|
||
|
||
$m = (\_, Out) => c = Ref$,
|
||
$m = (\_, Out) => w = AlwaysWrite$,
|
||
$r = Read => m = (In, \_)$,
|
||
|
||
$ tcorrectnew cl r, w, m, c cr $,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ argument read],
|
||
|
||
$cl v_m, v_r, v_w cr,
|
||
xarrowSquiggly(Read)_tryread
|
||
cl v_m modW readA, v_r modR readA, v_w modW readA cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ argument not read],
|
||
|
||
$cl v_m, v_r, v_w cr,
|
||
xarrowSquiggly(not Read)_tryread
|
||
cl v_m, v_r, v_w cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ value maybe spoiled],
|
||
|
||
$v_m,
|
||
xarrowSquiggly(not Out \, MaybeWrite)_tryspoil
|
||
?$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ value always spoiled],
|
||
|
||
$v_m,
|
||
xarrowSquiggly(not Out \, AlwaysWrite)_tryspoil
|
||
bot$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ value not spoiled],
|
||
|
||
$v_m,
|
||
xarrowSquiggly(Out \, w)_tryspoil
|
||
v_m$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ write spoil step],
|
||
|
||
$ tcorrectnew cl r, w, m, c cr $,
|
||
$cl v_m, v_r, v_w cr,
|
||
xarrowSquiggly(r)_tryread
|
||
cl v_m', v_r', v_w' cr$,
|
||
|
||
$v_m' modW writeA xarrowSquiggly(o \, AlwaysWrite)_tryspoil v_m''$,
|
||
|
||
$cl cdl v_m, v_r, v_w cdr, mu cr
|
||
xarrowSquiggly(cl r \, AlwaysWrite cr \, (\_, o) \, Ref)_spoil
|
||
cl cdl v_m'', v_r' modR writeA, v_w' modW writeA cdr, cdr, mu cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ maybe write step],
|
||
|
||
$ tcorrectnew cl r, w, m, c cr $,
|
||
$cl v_m, v_r, v_w cr,
|
||
xarrowSquiggly(r)_tryread
|
||
cl v_m', v_r', v_w' cr$,
|
||
|
||
$v_m' modW mbwriteA xarrowSquiggly(o \, MaybeWrite)_tryspoil v_m''$,
|
||
|
||
$cl cdl v_m, v_r, v_w cdr, mu cr
|
||
xarrowSquiggly(cl r \, MaybeWrite cr \, (\_, o) \, Ref)_spoil
|
||
cl cdl v_m'', v_r' modR mbwriteA, v_w' modW mbwriteA cdr, mu cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ skip step],
|
||
|
||
$ tcorrectnew cl r, w, m, c cr $,
|
||
$cl v_m, v_r, v_w cr,
|
||
xarrowSquiggly(r)_tryread
|
||
cl v_m', v_r', v_w' cr$,
|
||
|
||
$c = Copy or w = NotWrite$,
|
||
|
||
$cl cdl v_m, v_r, v_w cdr, mu cr
|
||
xarrowSquiggly(cl r \, w cr cr \, (\_, \_) \, c)_spoil
|
||
cl cdl v_m', v_r', v_w' cdr mu cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ lambda step],
|
||
|
||
$overline(t) = overline(t')$,
|
||
$cl lambda, mu cr xarrowSquiggly(lambda overline(t) \, lambda overline(t') \, m \, c)_spoil cl lambda, mu cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#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$,
|
||
)
|
||
))
|
||
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ tuple step],
|
||
|
||
$cl v_1, mu_0 cr xarrowSquiggly(t_1 \, t'_1 \, m \, c)_spoil cl v'_1, mu_1 cr$,
|
||
$...$,
|
||
$cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n \, t'_n \, m \, c)_spoil cl v'_n, mu_n cr$,
|
||
$cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n] \, [t'_1, ... t'_n] \, m \, c)_spoil cl [v'_1, ... v'_n], mu_n cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ full spoil for unit expr],
|
||
|
||
$mu stretch(=>)^(m space cl r, w cr space ())_(cl vals, types cr) mu$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ full spoil for path expr],
|
||
|
||
$p : path$,
|
||
$p arrpath x$,
|
||
$l = vals[x]$,
|
||
$vals, mu texpre p eqmu b$,
|
||
$types ttype p : t'$,
|
||
// TODO: FIXME: Ref or Copy ?? in root <- Copy ??,
|
||
// <- otherwise all subsequent copy capabilities will be ref (in current impl)
|
||
// FIXME depends on parent ??
|
||
$cl b, mu cr xarrowSquiggly(t \, t' \, m \, Copy)_spoil cl b', mu' cr$,
|
||
$p arrrevpath^(\#.) pi$,
|
||
$cl mu'[l], mu' cr xarrowSquiggly(cl pi \, b' cr)_change cl v'', mu'' cr$,
|
||
|
||
$mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu''[l <- v'']$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ full spoil for ref expr],
|
||
|
||
// NOTE: x as path
|
||
$mu stretch(=>)^(m space t space x)_(cl vals, types cr) mu'$,
|
||
|
||
// TODO:: is c important ?
|
||
$mu stretch(=>)^(m space rf c space t space rf x)_(cl vals, types cr) mu'$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ full spoil for tuple expr],
|
||
|
||
$mu_0 stretch(=>)^(m space t_1 space e_1)_(cl vals, types cr) mu_1$,
|
||
$...$,
|
||
$mu_(n - 1) stretch(=>)^(m space t_n space e_n)_(cl vals, types cr) mu_n$,
|
||
|
||
$mu_0 stretch(=>)^(m space [t_1, ... t_n] space [e_1, ... e_n])_(cl vals, types cr) mu_n$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
=== Function Argument Addition
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ add argument],
|
||
|
||
// programs considired to be well-typed
|
||
$cl v, mu cr xarrowSquiggly(t)_build cl v, mu' cr$,
|
||
$mu' xarrowSquiggly(v)_#[add] cl l, mu'' cr$,
|
||
|
||
// TODO save type mode somewhere ?? // <- not needed because is described by other params <- ??
|
||
$cl types, vals, mu cr
|
||
xarrowDashed(x space t)
|
||
cl types[x <- t], vals[x <- l], mu'' cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
=== Function Evaluation
|
||
|
||
#align(center, grid(
|
||
columns: 2,
|
||
gutter: 20%,
|
||
align: center,
|
||
|
||
[
|
||
$ x ~_r t$
|
||
|
||
#table(
|
||
columns: 2,
|
||
table.header(
|
||
[*x*], [*t*]
|
||
),
|
||
$1$, $Read$,
|
||
$0$, $not Read$,
|
||
$top$, $not Read$,
|
||
)
|
||
],
|
||
|
||
[
|
||
$x ~_w t$
|
||
#table(
|
||
columns: 2,
|
||
table.header(
|
||
[*x*], [*t*]
|
||
),
|
||
$0$, $NotWrite$,
|
||
$?$, $MaybeWrite$,
|
||
$1$, $AlwaysWrite$,
|
||
)
|
||
]
|
||
))
|
||
|
||
#let ttags = $attach(tack.r, br: #[`tags`])$
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ trivial type check],
|
||
|
||
$v_r ~_r r$,
|
||
$v_w ~_w w$,
|
||
$mu ttags cdl v_m, v_r, v_w cdr : cl r, w cr$,
|
||
)
|
||
))
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ lambda check],
|
||
|
||
$mu ttags lambda : lambda overline(t)$,
|
||
)
|
||
))
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ reference check],
|
||
|
||
$mu ttags mu[l] : t$,
|
||
$mu ttags rf l : rf t$,
|
||
)
|
||
))
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ tuple check],
|
||
|
||
$mu ttags v_1 : t_1$,
|
||
$...$,
|
||
$mu ttags v_n : t_n$,
|
||
$mu ttags [v_1, ... v_n] : [t_1, ... t_n]$,
|
||
)
|
||
))
|
||
|
||
#let tfunceval = $attach(tack.r.double, br: #[func eval])$
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ function evaluation],
|
||
|
||
// NOTE: dashed arrow to fill context
|
||
$cl types_0, vals_0, mu_0 cr
|
||
xarrowDashed(x_1 space t_1)
|
||
cl types', vals_1, mu_1 cr$,
|
||
$...$,
|
||
$cl types_(n - 1), vals_(n - 1), mu_(n - 1) cr
|
||
xarrowDashed(x_n space t_n)
|
||
cl types_n, vals_n, mu_n cr$,
|
||
|
||
// NOTE: eval function body
|
||
$cl types_n, vals_n, mu_n cr
|
||
xarrow(s)
|
||
cl types', vals', mu' cr$,
|
||
|
||
// NOTE: check that read and write tags are used properly
|
||
$mu' ttags mu'[vals'[x_1]] : t_1$,
|
||
$...$,
|
||
$mu' ttags mu'[vals'[x_n]] : t_n$,
|
||
|
||
$types_0, vals_0, mu_0 tfunceval cl "fun" f [(x_1 m_1 t_1), .. (x_n m_n x_n)] = s$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
=== Writability Check
|
||
|
||
#let twrite = $attach(tack.r, br: #[`write`])$
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ writable unit type: AlwaysWrite],
|
||
|
||
$twrite cl r, AlwaysWrite cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ writable unit type: MaybeWrite],
|
||
|
||
$twrite cl r, MaybeWrite cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ writable ref type],
|
||
|
||
$twrite t$,
|
||
$twrite rf c space t$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ writable lambda type],
|
||
|
||
$twrite lambda space overline(t)$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ writable tuple type],
|
||
|
||
$twrite t_1$,
|
||
$...$,
|
||
$twrite t_n$,
|
||
$twrite [t_1, ... t_n]$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
=== Statement Evaluation
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ SKIP],
|
||
|
||
$cl types, vals, mu cr
|
||
xarrow("SKIP")
|
||
cl types, vals, mu cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ CALL $f space [e_1, ... e_n]$],
|
||
|
||
// $vals, mu_0 tval f eqmu lambda [overline(x)_1 space s_1, ... overline(x)_n space s_n]$,
|
||
$types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
|
||
|
||
// NOTE: should be done on decl eval now
|
||
// NOTE: check that all the possible bodies are possible to eval
|
||
// $vals, mu_0 tfunceval cl s_1, overline(x)_1, [t_1, ... t_n], [e_1, ... e_n] cr$,
|
||
// $...$,
|
||
// $vals, mu_0 tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] cr$,
|
||
|
||
// NOTE: "spoil" context for each argument usage
|
||
$mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$,
|
||
$...$,
|
||
$mu_(n - 1) stretch(=>)^(m_n space t_n space e_n)_(cl vals, types cr) mu_n$,
|
||
|
||
$cl types, vals, mu_0 cr
|
||
xarrow("CALL" f space [e_1, ... e_n])
|
||
cl types, vals, mu_n cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ WRITE $p$],
|
||
|
||
$types ttype p : t$,
|
||
$twrite t$,
|
||
$p arrpath x$,
|
||
$l = vals[x]$,
|
||
$p arrrevpath^(\#.) pi$,
|
||
$mu[l] xarrowSquiggly(cl pi \, writeA cr)_modify v'$,
|
||
|
||
$cl types, vals, mu cr
|
||
xarrow("WRITE" p)
|
||
cl types, vals, mu[l <- v'] cr$,
|
||
)
|
||
))
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ READ $p$],
|
||
|
||
// TODO: already handled in modify ?
|
||
// $vals, mu tval p eqmu cdr v_m, \_, \_ cdl$,
|
||
// $v_m in { 0, top }$,
|
||
|
||
$p arrpath x$,
|
||
$l = vals[x]$,
|
||
$p arrrevpath^(\#.) pi$,
|
||
$mu[l] xarrowSquiggly(cl pi \, readA cr)_modify v'$,
|
||
|
||
$cl types, vals, mu cr
|
||
xarrow("READ" p)
|
||
cl types, vals, mu[l <- v'] cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ $s \; t$],
|
||
|
||
$cl types, vals, mu cr
|
||
stretch(->)^s
|
||
cl types_s, vals_s, mu_s cr$,
|
||
|
||
$cl types_s, vals_s, mu_s cr
|
||
stretch(->)^t
|
||
cl types_t, vals_t, mu_t cr$,
|
||
|
||
$cl types, vals, mu cr
|
||
xarrow(s \; t)
|
||
cl types_t, vals_t, mu_t cr$,
|
||
)
|
||
))
|
||
|
||
#h(10pt)
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ $s | t$],
|
||
|
||
$cl types, vals, mu cr
|
||
stretch(->)^s
|
||
cl types_s, vals_s, mu_s cr$,
|
||
|
||
$cl types, vals, mu cr
|
||
stretch(->)^t
|
||
cl types_t, vals_t, mu_t cr$,
|
||
|
||
$types_s = types_t$,
|
||
$vals_s = vals_t$,
|
||
$mu_s plus.o mu_t = mu'$,
|
||
|
||
// TODO changes ?? two ways ??
|
||
$cl types, vals, mu cr
|
||
xarrow(s | t)
|
||
cl types_t, vals_t, mu' cr$,
|
||
)
|
||
))
|
||
|
||
=== Program Evaluation
|
||
|
||
#let progeval = `prog eval`
|
||
|
||
#align(center, prooftree(
|
||
vertical-spacing: 4pt,
|
||
rule(
|
||
name: [ program evaluation],
|
||
|
||
// NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers)
|
||
// expect well typed program
|
||
|
||
$cl types_0, vals_0, mu_0 cr xarrowSquiggly(d_1)_init cl types_1, vals_1, mu_1 cr$,
|
||
$...$,
|
||
$cl types_(n - 1), vals_(n - 1), mu_(n - 1) cr xarrowSquiggly(d_n)_init cl types_n, vals_n, mu_n cr$,
|
||
|
||
$cl types_n, vals_n, mu_n tfunceval d_1$,
|
||
$...$,
|
||
$cl types_n, vals_n, mu_n tfunceval d_n$,
|
||
|
||
$cl types_0, vals_0, mu_0 cr xarrowSquiggly(d_1 ... d_n)_prog_eval cl types_n, vals_n, mu_n cr$
|
||
)
|
||
))
|
||
|
||
]
|