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