mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-04-29 09:14:35 +00:00
Compare commits
No commits in common. "6a3368cbdf659c743ea467470821d20ee5c21f62" and "84d1ce7eb5ebdbd74a1b7f5fb04b8336807da4c2" have entirely different histories.
6a3368cbdf
...
84d1ce7eb5
1 changed files with 154 additions and 258 deletions
|
|
@ -11,7 +11,20 @@
|
||||||
|
|
||||||
// TODO: check correctnes for path, mem & type ??
|
// TODO: check correctnes for path, mem & type ??
|
||||||
|
|
||||||
== Syntax
|
Нужно будет добавить во write-flag модальности: `not write` | `may write` | `always write`
|
||||||
|
|
||||||
|
Добавление condition-исполнения - выбор из нескольких блоков. Варианты:
|
||||||
|
- & of | of & -вложенные блоки ?
|
||||||
|
- добавить несколько альтернативны тел функциям. Но тогда придётся при трансляции if-блоки выносить в функции
|
||||||
|
|
||||||
|
Лямбды - нужно тоже будет как-то находить лямбды и ля них тоже синтезировать атрибуты
|
||||||
|
вызов лямбд будет нужен в модели?
|
||||||
|
- lambda-аргумент - вложенные теги?, должна быть одна и та же сигнтура
|
||||||
|
можно ввести отдельные сигнатуры-определения?
|
||||||
|
|
||||||
|
проблема простой семантики: вызов лямбд: могут быть модифицируемые функции
|
||||||
|
|
||||||
|
== Синтаксис
|
||||||
|
|
||||||
#h(10pt)
|
#h(10pt)
|
||||||
|
|
||||||
|
|
@ -25,19 +38,18 @@
|
||||||
#let isIn = `isIn`
|
#let isIn = `isIn`
|
||||||
#let isOut = `isOut`
|
#let isOut = `isOut`
|
||||||
|
|
||||||
#let mode = `mode`
|
#let tag = `tag`
|
||||||
#let expr = `expr`
|
#let value = `value`
|
||||||
#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 argtype = `argtype`
|
||||||
|
#let argmem = `argmem`
|
||||||
#bnf(
|
#bnf(
|
||||||
Prod(`read`,
|
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[Read][read passed value]
|
||||||
Or[$not$ Read][] } ),
|
Or[Not Read][] } ),
|
||||||
Prod(`write`,
|
Prod(`write`,
|
||||||
{ Or[$square$ Write][in all cases there is a write to passed variable] // always write, requre at least one write in each flow variant
|
{ Or[$square$ Write][in all cases there is a write to passed variable] // always write, requre at least one write in each flow variant
|
||||||
Or[$diamond$ Write][in some cases there is a write to passed variable] // possible write, no requirements (?)
|
Or[$diamond$ Write][in some cases there is a write to passed variable] // possible write, no requirements (?)
|
||||||
|
|
@ -47,276 +59,117 @@
|
||||||
Or[Value][pass copy of the value] } ),
|
Or[Value][pass copy of the value] } ),
|
||||||
Prod(`in`,
|
Prod(`in`,
|
||||||
{ Or[In][parameter value used as input]
|
{ Or[In][parameter value used as input]
|
||||||
Or[$not$ In][] } ),
|
Or[Not In][] } ),
|
||||||
Prod(`out`,
|
Prod(`out`,
|
||||||
{ Or[Out][parameter value returned]
|
{ Or[Out][parametr value returned]
|
||||||
Or[$not$ Out][] } ),
|
Or[Not Out][] } ),
|
||||||
Prod(
|
Prod(
|
||||||
`mode`,
|
`tag`,
|
||||||
{
|
{
|
||||||
Or[`read` #h(3pt) `write` #h(3pt) `copy` #h(3pt) `in` #h(3pt) `out`][]
|
Or[`read` #h(3pt) `write` #h(3pt) `copy` #h(3pt) `in` #h(3pt) `out`][]
|
||||||
}
|
}
|
||||||
),
|
),
|
||||||
|
Prod(
|
||||||
|
`value`,
|
||||||
|
{
|
||||||
|
Or[$0$][cell with some value (always)]
|
||||||
|
Or[$X$][cell with possible value or $bot$]
|
||||||
|
Or[$bot$][spoiled cell (always)]
|
||||||
|
}
|
||||||
|
),
|
||||||
Prod(
|
Prod(
|
||||||
`path`,
|
`path`,
|
||||||
{
|
{
|
||||||
// NOTE: global vars & local vars names could be used with one constructor
|
Or[$@x$][fuction argument or variable itself]
|
||||||
// Or[$\#x$][funciton or global variable itself]
|
|
||||||
Or[$@ X$][function argument or variable itself]
|
|
||||||
Or[$* path$][reference insede path]
|
Or[$* path$][reference insede path]
|
||||||
Or[$path . n$][access $n$-th cell of the tuple]
|
Or[$path . n$][access $n$-th cell of the tuple]
|
||||||
// Or[$path : n$][access $n$-th cell of the union] // TODO: another notation ??
|
// Or[$path : n$][access $n$-th cell of the union] // TODO: another notation ??
|
||||||
}
|
}
|
||||||
),
|
),
|
||||||
Prod(
|
Prod(
|
||||||
`type`,
|
`argtype`,
|
||||||
{
|
{
|
||||||
Or[$()$][simple type representing all primitive types] // `Unit`
|
Or[$()$][simple type representing all primitive types] // `Unit`
|
||||||
Or[\& #h(3pt) `mode` #h(3pt) `type`][reference to structure, contains copy / ref choice] // `Ref`
|
Or[\& #h(3pt) `tag` #h(3pt) `argtype`][reference to structure, contains copy / ref choice] // `Ref`
|
||||||
Or[$[type+]$][tuple type] // `Prod`
|
Or[\[#overline(`argtype`)\]][pair type, allows to make tuples] // `Prod`
|
||||||
// Or[`type` $times$ `type`][pair type, allows to make tuples] // `Prod`
|
// Or[`argtype` $times$ `argtype`][pair type, allows to make tuples] // `Prod`
|
||||||
// Or[`type` $+$ `type`][union type (important in some way ???)] // `Sum` // TODO ?
|
// Or[`argtype` $+$ `argtype`][union type (important in some way ???)] // `Sum` // TODO ?
|
||||||
|
Or[$F_x$][type of lambda or function pointer, defined by function declaration id] // `Fun`
|
||||||
// NOTE: do not use names in type
|
|
||||||
// Or[$lambda_((x type)+)$][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`
|
|
||||||
}
|
}
|
||||||
),
|
),
|
||||||
// FIXME: replace with expr
|
|
||||||
Prod(
|
Prod(
|
||||||
`expr`,
|
`argmem`,
|
||||||
{
|
{
|
||||||
Or[$()$][value of simple type] // `Unit`
|
Or[$@m$][memory id for simple type variable] // `Unit`
|
||||||
Or[$path$][value from variable] // `Path`
|
Or[\& #h(3pt) `argmem`][reference to structure, contains copy / ref choice] // `Ref`
|
||||||
Or[$\& #h(3pt) expr$][reference expr] // `Ref`
|
// Or[\& #h(3pt) `tag` #h(3pt) `argmem`][reference to structure, contains copy / ref choice] // `Ref`
|
||||||
Or[$[expr+]$][tuple expr] // `Prod`
|
Or[\[#overline(`argmem`)\]][pair type, allows specify memory for tuples] // `Prod`
|
||||||
// NOTE: replaced with simple path value
|
// Or[`argmem` $times$ `argmem`][pair type, allows specify memory for tuples] // `Prod`
|
||||||
// Or[$lambda_path$][function value from variable] // `Fun`
|
// Or[`argmem` $+$ `argmem`][union type (important in some way ???)] // `Sum` // TODO ?
|
||||||
|
Or[$F$][memory for lambda or function pointer, defined by function declaration id] // `Fun` // why separated ??
|
||||||
|
// Or[$F_m$][memory for lambda or function pointer, defined by function declaration id] // `Fun` // why separated ??
|
||||||
}
|
}
|
||||||
),
|
),
|
||||||
|
// Prod(
|
||||||
|
// `arg`,
|
||||||
|
// {
|
||||||
|
// Or[$0$][new value, no associated variable]
|
||||||
|
// Or[$ amp d$][value from some variable]
|
||||||
|
// }
|
||||||
|
// ),
|
||||||
Prod(
|
Prod(
|
||||||
`stmt`,
|
`stmt`,
|
||||||
{
|
{
|
||||||
Or[`CALL` $f space expr+$][call function]
|
Or[`CALL` $f space overline(path)$][call function by id]
|
||||||
|
Or[`CALL_LAM` $path space overline(path)$][call lambda funciton (variable or funcitona argument field)]
|
||||||
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 ]
|
// TODO: or introduce block statement ?? // vars definiiton statment ??
|
||||||
Or[$stmt | stmt$][control flow operator, excution of one statements]
|
// (for example, for same named vars in nested spaces)
|
||||||
|
Or[`CHOICE` #overline(`stmt`) #overline(`stmt`)][control flow operator, xecution of one of the blocks]
|
||||||
|
// NOTE: var: replaced with arguments (use rvalue as init) (?)
|
||||||
|
// Or[`VAR`][variables inside functions] // NOTE: no modifiers required, because it is in the new memory ?? // TODO: not required ??
|
||||||
|
// NOTE: lambda: compile to call to the funciton with CHOICE between possible lambda bodies <- do this analysis inside synthesizer ?
|
||||||
}
|
}
|
||||||
),
|
),
|
||||||
Prod(
|
Prod(
|
||||||
`decl`,
|
`decl`,
|
||||||
{
|
{
|
||||||
// TODO: path not allowed ??
|
Or[$overline(stmt)$][function body]
|
||||||
Or[$"var" X : type = expr$][global variable declaration]
|
Or[$lambda a : argtype.$ `decl`][argument with argument pass strategy annotation]
|
||||||
Or[$"fun" X ((X : type)+) = stmt$][function declaration]
|
|
||||||
}
|
}
|
||||||
),
|
),
|
||||||
Prod(
|
Prod(
|
||||||
`prog`,
|
`prog`,
|
||||||
{
|
{
|
||||||
Or[$decl stmt$][declarations and executet statement]
|
Or[`decl`][main function]
|
||||||
|
Or[`decl` `prog`][with supplimentary funcitons]
|
||||||
}
|
}
|
||||||
),
|
),
|
||||||
)
|
)
|
||||||
|
== Семантика статического интерпретатора
|
||||||
|
|
||||||
== Value Model
|
#h(10pt)
|
||||||
|
|
||||||
// FIXME: check & add details
|
$V := value$ - значения памяти
|
||||||
#let value = `value`
|
|
||||||
#bnf(
|
|
||||||
Prod(
|
|
||||||
`value`,
|
|
||||||
{
|
|
||||||
Or[$()$][value of simple type] // `Unit`
|
|
||||||
Or[$lambda_X$][function pointer value] // `Fun`
|
|
||||||
Or[$\& #h(3pt) value$][reference value] // `Ref`
|
|
||||||
Or[$[value+]$][tuple value] // `Prod`
|
|
||||||
}
|
|
||||||
),
|
|
||||||
)
|
|
||||||
|
|
||||||
$value$ - значения, которые могут лежать в переменных и передаваться как аргументы функций (то, во что вычисляется $expr$)
|
$L := NN$ - позиции в памяти
|
||||||
|
|
||||||
== Memory Model
|
|
||||||
|
|
||||||
// FIXME: check & add details
|
|
||||||
#let memelem = `memelem`
|
|
||||||
#let valuemem = `valuemem`
|
|
||||||
#bnf(
|
|
||||||
Prod(
|
|
||||||
`memelem`,
|
|
||||||
{
|
|
||||||
Or[$0$][cell with some value (always)]
|
|
||||||
Or[$\#$][cell with possible value or $bot$]
|
|
||||||
Or[$bot$][spoiled cell (always)]
|
|
||||||
}
|
|
||||||
),
|
|
||||||
Prod(
|
|
||||||
`valuemem`,
|
|
||||||
{
|
|
||||||
Or[$()$][one unit of memory, for simple vars] // `Unit`
|
|
||||||
Or[$lambda$][memory for lambda or function pointer, is not important in the memory model, 0 units] // `Fun`
|
|
||||||
Or[$\& #h(3pt) LL valuemem$][reference to structure memory start] // `Ref`
|
|
||||||
Or[$[valuemem+]$][memory specification for each tuple member] // `Prod`
|
|
||||||
}
|
|
||||||
),
|
|
||||||
)
|
|
||||||
|
|
||||||
#let mem = `mem`
|
|
||||||
Память преставляется в виде стека из значений `memelem`:
|
|
||||||
- $LL = NN$ - множество меток памяти
|
|
||||||
- $mu : mem = LL -> V$ - память, частично определённая функция
|
|
||||||
- $l in LL$ - длина используемого фрагмента памяти
|
|
||||||
|
|
||||||
Каждому значению $value$ в соответствие ставится $valuemem$ - расположние этого значения в пaмяти
|
|
||||||
|
|
||||||
Соответствие:
|
|
||||||
- $() -> ()$
|
|
||||||
- $lambda_X -> lambda$
|
|
||||||
- $\& #h(3pt) value -> \& #h(3pt) LL valuemem$
|
|
||||||
- $[value+] -> [valuemem+]$
|
|
||||||
|
|
||||||
// TODO: move allocation semantics there ??
|
|
||||||
|
|
||||||
== Semantics
|
|
||||||
|
|
||||||
// $V := memelem$ - значения памяти
|
|
||||||
|
|
||||||
$X$ - можество переменных
|
$X$ - можество переменных
|
||||||
|
|
||||||
#let env = `env`
|
$sigma : X -> argmem times argtype$ - #[ позиции памяти, соответстующие переменным контекста,
|
||||||
$sigma : env = X -> valuemem times type$ - #[ позиции памяти, соответстующие переменным контекста, частично определённая функция ]
|
частично определённая функция ]
|
||||||
|
|
||||||
$DD : X -> decl$ - глобальные определения, частично определённая функция
|
$mu : NN -> V$ - память, частично определённая функция
|
||||||
|
|
||||||
$d in decl, s in stmt, f in X, x in X, a in X$
|
$l in NN$ - длина используемого фрагмента памяти
|
||||||
|
|
||||||
|
$DD : NN -> decl$ - определения функций, частично определённая функция
|
||||||
|
|
||||||
|
$d in decl, s in stmt, f in NN, x in X, a in NN$
|
||||||
|
|
||||||
$d space @ space overline(x)$ - запись применения функции (вида #decl) к аргументам
|
$d space @ space overline(x)$ - запись применения функции (вида #decl) к аргументам
|
||||||
|
|
||||||
=== Path Accessors
|
|
||||||
|
|
||||||
Набор частично определённых фунций для работы с путями.
|
|
||||||
Для удобства значение, получаемое из текущего применением пути, будем называть полем.
|
|
||||||
// Все эти функции используются с префиксом `path.`.
|
|
||||||
|
|
||||||
// FIXME: types & description for functios
|
|
||||||
#let pathtype = `path.type`
|
|
||||||
#let pathmem = `path.mem`
|
|
||||||
#let pathmode = `path.mode`
|
|
||||||
#let pathvar = `path.var`
|
|
||||||
|
|
||||||
#let pathsize = `path.memsize`
|
|
||||||
#let pathbasepos = `path.membasepos`
|
|
||||||
#let pathoffset = `path.memoffset`
|
|
||||||
#let pathpos = `path.mempos`
|
|
||||||
|
|
||||||
#let pathenvtype = `path.envtype`
|
|
||||||
#let pathenvmem = `path.envmem`
|
|
||||||
#let pathenvmode = `path.envmode`
|
|
||||||
|
|
||||||
#let pathenvpos = `path.envpos`
|
|
||||||
#let pathenvval = `path.envval`
|
|
||||||
|
|
||||||
- #[ Получение типа поля
|
|
||||||
$ pathtype : type -> path -> type $
|
|
||||||
$ pathtype(t, @x) = t $
|
|
||||||
$ pathtype(\& #h(3pt) mode #h(3pt) t, *p) = pathtype(t, p) $
|
|
||||||
$ pathtype([t_1, t_2, ..., t_n], p.i) = pathtype(t_i, p) $
|
|
||||||
]
|
|
||||||
- #[ Получение начала памяти поля (предусловие: $pathtype(t, p) = \& #h(3pt) ...$)
|
|
||||||
$ pathmem : valuemem -> path -> LL $
|
|
||||||
$ pathmem(\& #h(3pt) y m, @x) = y $ // NOTE: only memory for refsi in midel ?? // TODO: decide
|
|
||||||
$ pathmem(\& #h(3pt) y m, *p) = pathmem(m, p) $
|
|
||||||
$ pathmem([m_1, m_2, ..., m_n], p.i) = pathmem(m_i, p) $
|
|
||||||
]
|
|
||||||
- #[ Получения тега поля (предусловие: $pathtype(t, p) = \& #h(3pt) ...$)
|
|
||||||
$ pathmode : type -> path -> mode $
|
|
||||||
$ pathmode(\& #h(3pt) mode #h(3pt) t, @x) = mode $
|
|
||||||
$ pathmode(\& #h(3pt) mode #h(3pt) t, *p) = pathmode(t, p) $
|
|
||||||
$ pathmode([t_1, t_2, ..., t_n], p.i) = pathmode(t_i, p) $
|
|
||||||
]
|
|
||||||
- #[ Получение \"корневой\" переменной пути
|
|
||||||
$ pathvar : path -> X $
|
|
||||||
$ pathvar(@x) = x $
|
|
||||||
$ pathvar(* p) = pathvar(p) $
|
|
||||||
$ pathvar(p.i) = pathvar(p) $
|
|
||||||
]
|
|
||||||
- #[ Получение размера поля в памяти
|
|
||||||
$ pathsize : valuemem -> path -> LL $
|
|
||||||
$ pathsize((), @x) = 1 $
|
|
||||||
$ pathsize(lambda, @x) = 0 $
|
|
||||||
$ pathsize(\& #h(3pt) y m, @x) = 0 $ // TODO: FIXME ?? always disconnected location ??
|
|
||||||
$ pathsize([m_1, m_2, ..., m_n], @x) = pathsize(m_1, @x) + ... + pathsize(m_n, @x) $
|
|
||||||
$ pathsize(\& #h(3pt) y m, *p) = pathsize(m, p) $
|
|
||||||
$ pathsize([m_1, m_2, ..., m_n], p.i) = pathsize(m_i, p) $
|
|
||||||
]
|
|
||||||
// TODO: FIXME ??
|
|
||||||
- #[ Получение позиции последного ссылочного предка поля в пaмяти
|
|
||||||
$ pathbasepos : value -> path -> X $
|
|
||||||
// $ pathbasepos(m, @x) = bot $ // NOTE: trivial if not present ??
|
|
||||||
$ pathbasepos(\& #h(3pt) y m, *p) = pathbasepos(m, p) | y $
|
|
||||||
$ pathbasepos([m_1, m_2, ..., m_n], p.i) = pathbasepos(m_i, p) $
|
|
||||||
]
|
|
||||||
- #[ Получение смещения поля в последнем монолитном отрезке памяти
|
|
||||||
$ pathoffset : value -> path -> X $
|
|
||||||
$ pathoffset(m, @x) = 0 $
|
|
||||||
$ pathoffset(\& #h(3pt) y m, *p) = pathoffset(m, p) $
|
|
||||||
$ pathoffset([m_1, m_2, ..., m_n], p.i) = (i - 1) + pathoffset(m_i, p) $
|
|
||||||
]
|
|
||||||
- #[ Получение позиции поля в пaмяти
|
|
||||||
$ pathpos : value -> path -> X $
|
|
||||||
$ pathpos(m, p) = pathbasepos(m, p) + pathoffset(m, p)$
|
|
||||||
]
|
|
||||||
- #[ Получение типа поля по окружению
|
|
||||||
$ pathenvtype : env -> path -> type $
|
|
||||||
$ pathenvtype(sigma, p) = pathtype(sigma[pathvar(p)].2, p) $
|
|
||||||
]
|
|
||||||
- #[ Получение начала памяти поля по окружению (предусловие: $pathtype(t, p) = \& #h(3pt) ...$)
|
|
||||||
$ pathenvmem : env -> path -> LL $
|
|
||||||
$ pathenvmem(sigma, p) = pathmem(sigma[pathvar(p)].1, p) $
|
|
||||||
]
|
|
||||||
- #[ Получения тега поля по окружению (предусловие: $pathtype(t, p) = \& #h(3pt) ...$)
|
|
||||||
$ pathenvmode : env -> path -> mode $
|
|
||||||
$ pathenvmode(sigma, p) = pathmode(sigma[pathvar(p)].2, p) $
|
|
||||||
]
|
|
||||||
- #[ Получение позиции поля в пaмяти по окружению
|
|
||||||
$ pathenvpos : env -> path -> X $
|
|
||||||
$ pathenvpos(m, p) = pathpos(sigma[pathvar(p)].1, p)$
|
|
||||||
]
|
|
||||||
- #[ Получение поля в пaмяти
|
|
||||||
$ pathenvval : env -> mem -> path -> memelem $
|
|
||||||
$ pathenvval(sigma, mu, p) = mu[pathenvpos(sigma, p)]$
|
|
||||||
]
|
|
||||||
|
|
||||||
=== 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
|
|
||||||
|
|
||||||
// FIXME: make connected to syntax
|
|
||||||
*TODO*
|
|
||||||
|
|
||||||
#h(10pt)
|
|
||||||
|
|
||||||
#let args = `args`
|
#let args = `args`
|
||||||
|
|
||||||
#[
|
#[
|
||||||
|
|
@ -346,23 +199,66 @@ $ isRead mode -> isIn mode $
|
||||||
|
|
||||||
#h(10pt)
|
#h(10pt)
|
||||||
|
|
||||||
=== Correctness
|
=== Path
|
||||||
|
|
||||||
// TODO: FIXME: well formatness for mode, extract
|
#let pathtype = `pathtype`
|
||||||
// TODO: FIXME: check for mode, is recursion required ??
|
$ pathtype(t, @x) = t $
|
||||||
// TODO: FIXME: check mode & access corectness in os correct
|
$ pathtype(\& #h(3pt) tag #h(3pt) t, *p) = pathtype(t, p) $
|
||||||
|
$ pathtype([t_1, t_2, ..., t_n], p.i) = pathtype(t_i, p) $
|
||||||
|
|
||||||
|
#let pathmem = `pathmem`
|
||||||
|
$ pathmem(@m, @x) = m $
|
||||||
|
$ pathmem(\& #h(3pt) m, *p) = pathmem(m, p) $
|
||||||
|
$ pathmem([m_1, m_2, ..., m_n], p.i) = pathmem(m_i, p) $
|
||||||
|
|
||||||
|
// NOTE: is replaced with pathtype
|
||||||
|
// #let pathfun = `pathfun`
|
||||||
|
// $ pathfun(F_m, @x) = m $
|
||||||
|
// $ pathfun(\& #h(3pt) m, *p) = pathfun(m, p) $
|
||||||
|
// $ pathfun([m_1, m_2, ..., m_n], p.i) = pathfun(m_i, p) $
|
||||||
|
|
||||||
|
#let pathtag = `pathtag`
|
||||||
|
$ pathtag(\& #h(3pt) tag #h(3pt) t, @x) = tag $
|
||||||
|
$ pathtag(\& #h(3pt) tag #h(3pt) t, *p) = pathtag(t, p) $
|
||||||
|
$ pathtag([t_1, t_2, ..., t_n], p.i) = pathtag(t_i, p) $
|
||||||
|
|
||||||
|
#let pathvar = `pathvar`
|
||||||
|
$ pathvar(@x) = x $
|
||||||
|
$ pathvar(* p) = pathvar(p) $
|
||||||
|
$ pathvar(p.i) = pathvar(p) $
|
||||||
|
|
||||||
|
#h(10pt)
|
||||||
|
|
||||||
|
// $ pathtype({t_1, t_2, ..., t_n}, x -> i) = t_i$
|
||||||
|
|
||||||
|
#let typeof = `typeof`
|
||||||
|
$ typeof(sigma, p) = pathtype(sigma[pathvar(p)].2, p) $
|
||||||
|
|
||||||
|
// TODO: two versions: write with change & read ??
|
||||||
|
#let accessmem = `accessmem`
|
||||||
|
$ accessmem(sigma, p) = pathmem(sigma[pathvar(p)].1, p) $
|
||||||
|
|
||||||
|
#let argtag = `argtag`
|
||||||
|
$ argtag(sigma, p) = pathtag(sigma[pathvar(p)].2, p) $
|
||||||
|
|
||||||
|
#let access = `access`
|
||||||
|
$ access(sigma, mu, p) = mu[accessmem(sigma, p)] $
|
||||||
|
|
||||||
|
#h(10pt)
|
||||||
|
|
||||||
|
=== Correctness
|
||||||
|
|
||||||
// TODO: check all requirements
|
// TODO: check all requirements
|
||||||
#align(center, prooftree(
|
#align(center, prooftree(
|
||||||
vertical-spacing: 4pt,
|
vertical-spacing: 4pt,
|
||||||
rule(
|
rule(
|
||||||
name: [ is correct],
|
name: [ is correct],
|
||||||
$isOut mode -> isAlwaysWrite mode$, // NOTE; strong requirment should write
|
$isOut tag -> isAlwaysWrite tag$, // NOTE; strong requirment should write
|
||||||
$isRead mode -> isIn mode$,
|
$isRead tag -> isIn tag$,
|
||||||
$isPossibleWrite mode and (isOut mode or not isCopy mode) -> isAlwaysWrite pathenvmode(sigma, x)$, // NOTE: may mode => should sigma(x)
|
$isPossibleWrite tag and (isOut tag or not isCopy tag) -> isAlwaysWrite argtag(sigma, x)$, // NOTE: may tag => should sigma(x)
|
||||||
$isRead mode -> pathenvval(mu, sigma, x) != bot and pathenvval(mu, sigma, x) != X$,
|
$isRead tag -> access(mu, sigma, x) != bot and access(mu, sigma, x) != X$,
|
||||||
|
|
||||||
$isCorrect_(cl sigma, mu cr) (mode, x)$,
|
$isCorrect_(cl sigma, mu cr) (tag, x)$,
|
||||||
)
|
)
|
||||||
))
|
))
|
||||||
|
|
||||||
|
|
@ -370,10 +266,10 @@ $ isRead mode -> isIn mode $
|
||||||
|
|
||||||
=== Call Initialization
|
=== Call Initialization
|
||||||
|
|
||||||
Отсутствующий нижний индекс ($ref$, $copy$) означает произвольный индекс.
|
Отсутствующий ижний индекс ($ref$, $copy$) означает произвольный индекс.
|
||||||
Считается, что выбранный индекс одинаков в рамках одного правила.
|
Считается, что выбранный индекс одинаков в рамках одного правила.
|
||||||
|
|
||||||
// NOTE: no empty type
|
// NOTE: no empty argtype
|
||||||
// #align(center, prooftree(
|
// #align(center, prooftree(
|
||||||
// vertical-spacing: 4pt,
|
// vertical-spacing: 4pt,
|
||||||
// rule(
|
// rule(
|
||||||
|
|
@ -391,7 +287,7 @@ $ isRead mode -> isIn mode $
|
||||||
name: [ add paths field by copy],
|
name: [ add paths field by copy],
|
||||||
|
|
||||||
// TODO: check that access is what required ??
|
// TODO: check that access is what required ??
|
||||||
$cl sigma, mu, l cr xarrowSquiggly(p : ())_copy cl pathenvmem(sigma, p) <- l, mu [l <- 0], l + 1 cr$,
|
$cl sigma, mu, l cr xarrowSquiggly(p : ())_copy cl accessmem(sigma, p) <- l, mu [l <- 0], l + 1 cr$,
|
||||||
)
|
)
|
||||||
))
|
))
|
||||||
|
|
||||||
|
|
@ -414,9 +310,9 @@ $ isRead mode -> isIn mode $
|
||||||
rule(
|
rule(
|
||||||
name: [ add paths ref],
|
name: [ add paths ref],
|
||||||
$cl sigma, mu, l cr xarrowSquiggly(*p : t)_ref cl sigma', mu', l' cr$,
|
$cl sigma, mu, l cr xarrowSquiggly(*p : t)_ref cl sigma', mu', l' cr$,
|
||||||
$isRef mode$,
|
$isRef tag$,
|
||||||
|
|
||||||
$cl sigma, mu, l cr xarrowSquiggly(p : \& mode t) cl sigma', mu', l' cr$,
|
$cl sigma, mu, l cr xarrowSquiggly(p : \& tag t) cl sigma', mu', l' cr$,
|
||||||
)
|
)
|
||||||
))
|
))
|
||||||
|
|
||||||
|
|
@ -427,9 +323,9 @@ $ isRead mode -> isIn mode $
|
||||||
rule(
|
rule(
|
||||||
name: [ add paths ref],
|
name: [ add paths ref],
|
||||||
$cl sigma, mu, l cr xarrowSquiggly(*p : t)_copy cl sigma, mu, l cr$,
|
$cl sigma, mu, l cr xarrowSquiggly(*p : t)_copy cl sigma, mu, l cr$,
|
||||||
$isCopy mode$,
|
$isCopy tag$,
|
||||||
|
|
||||||
$cl sigma, mu, l cr xarrowSquiggly(p : \& mode t) cl sigma', mu', l' cr$,
|
$cl sigma, mu, l cr xarrowSquiggly(p : \& tag t) cl sigma', mu', l' cr$,
|
||||||
)
|
)
|
||||||
))
|
))
|
||||||
|
|
||||||
|
|
@ -479,14 +375,14 @@ $ isRead mode -> isIn mode $
|
||||||
|
|
||||||
$mu stretch(=>)^args_sigma gamma$,
|
$mu stretch(=>)^args_sigma gamma$,
|
||||||
|
|
||||||
$isPossibleWrite mode$, // NOTE: weak requirement: may write
|
$isPossibleWrite tag$, // NOTE: weak requirement: may write
|
||||||
$not isCopy mode$,
|
$not isCopy tag$,
|
||||||
$not isOut mode$,
|
$not isOut tag$,
|
||||||
|
|
||||||
$isCorrect_(cl sigma, mu cr) (mode, x)$,
|
$isCorrect_(cl sigma, mu cr) (tag, x)$,
|
||||||
|
|
||||||
// gamma - memory (as mu)
|
// gamma - memory (as mu)
|
||||||
$gamma stretch(=>)^((mode, x) : args)_sigma pathenvval(gamma, sigma, x) <- bot]$
|
$gamma stretch(=>)^((tag, x) : args)_sigma access(gamma, sigma, x) <- bot]$
|
||||||
)
|
)
|
||||||
))
|
))
|
||||||
|
|
||||||
|
|
@ -499,13 +395,13 @@ $ isRead mode -> isIn mode $
|
||||||
|
|
||||||
$mu stretch(=>)^args_sigma gamma$,
|
$mu stretch(=>)^args_sigma gamma$,
|
||||||
|
|
||||||
$isAlwaysWrite mode$, // NOTE: strong requirement: should write
|
$isAlwaysWrite tag$, // NOTE: strong requirement: should write
|
||||||
$isOut mode$,
|
$isOut tag$,
|
||||||
|
|
||||||
$isCorrect_(cl sigma, mu cr) (mode, x)$,
|
$isCorrect_(cl sigma, mu cr) (tag, x)$,
|
||||||
|
|
||||||
// gamma - memory (as mu)
|
// gamma - memory (as mu)
|
||||||
$gamma stretch(=>)^((mode, x) : args)_sigma pathenvval(gamma, sigma, x) <- 0]$
|
$gamma stretch(=>)^((tag, x) : args)_sigma access(gamma, sigma, x) <- 0]$
|
||||||
)
|
)
|
||||||
))
|
))
|
||||||
|
|
||||||
|
|
@ -521,10 +417,10 @@ $ isRead mode -> isIn mode $
|
||||||
$not "spoil step"$,
|
$not "spoil step"$,
|
||||||
$not "fix step"$,
|
$not "fix step"$,
|
||||||
|
|
||||||
$isCorrect_(cl sigma, mu cr) (mode, x)$,
|
$isCorrect_(cl sigma, mu cr) (tag, x)$,
|
||||||
|
|
||||||
// mu
|
// mu
|
||||||
$gamma stretch(=>)^((mode, x) : args)_sigma gamma$
|
$gamma stretch(=>)^((tag, x) : args)_sigma gamma$
|
||||||
)
|
)
|
||||||
))
|
))
|
||||||
|
|
||||||
|
|
@ -548,8 +444,8 @@ $ isRead mode -> isIn mode $
|
||||||
xarrowDashed(d space @ space overline(y))
|
xarrowDashed(d space @ space overline(y))
|
||||||
cl sigma'', mu'', l'' cr$,
|
cl sigma'', mu'', l'' cr$,
|
||||||
|
|
||||||
$isRead mode$,
|
$isRead tag$,
|
||||||
$not isCopy mode$,
|
$not isCopy tag$,
|
||||||
|
|
||||||
// NOTE: correctness checked in CALL f
|
// NOTE: correctness checked in CALL f
|
||||||
|
|
||||||
|
|
@ -609,7 +505,7 @@ $ isRead mode -> isIn mode $
|
||||||
rule(
|
rule(
|
||||||
name: [ CALL_LAM $y space overline(x)$],
|
name: [ CALL_LAM $y space overline(x)$],
|
||||||
|
|
||||||
$pathenvtype(sigma, y) = F_f$,
|
$typeof(sigma, y) = F_f$,
|
||||||
|
|
||||||
$cl sigma, mu, l cr
|
$cl sigma, mu, l cr
|
||||||
xarrow("CALL" f space overline(x))
|
xarrow("CALL" f space overline(x))
|
||||||
|
|
@ -628,8 +524,8 @@ $ isRead mode -> isIn mode $
|
||||||
rule(
|
rule(
|
||||||
name: [ READ $x$],
|
name: [ READ $x$],
|
||||||
|
|
||||||
$pathenvval(mu, sigma, x) != bot$,
|
$access(mu, sigma, x) != bot$,
|
||||||
$pathenvval(mu, sigma, x) != X$,
|
$access(mu, sigma, x) != X$,
|
||||||
|
|
||||||
$cl sigma, mu, l cr
|
$cl sigma, mu, l cr
|
||||||
xarrow("READ" x)
|
xarrow("READ" x)
|
||||||
|
|
@ -648,7 +544,7 @@ $ isRead mode -> isIn mode $
|
||||||
|
|
||||||
$cl sigma, mu, l cr
|
$cl sigma, mu, l cr
|
||||||
xarrow("WRITE" x)
|
xarrow("WRITE" x)
|
||||||
cl sigma, pathenvval(mu, sigma, x) <- 0, l cr$,
|
cl sigma, access(mu, sigma, x) <- 0, l cr$,
|
||||||
)
|
)
|
||||||
))
|
))
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue