mirror of
https://github.com/ProgramSnail/pass_strategy_synthesis.git
synced 2026-04-27 08:43:11 +00:00
Compare commits
No commits in common. "0937d91f54fa72250652569a067df1db52ad9729" and "adeefc1c870a937f4820bcc7e0e27ad4457ab39a" have entirely different histories.
0937d91f54
...
adeefc1c87
1 changed files with 186 additions and 138 deletions
|
|
@ -24,6 +24,8 @@
|
|||
#let isPossibleWrite = `isPossibleWrite`
|
||||
#let isRef = `isRef`
|
||||
#let isCopy = `isCopy`
|
||||
#let isIn = `isIn`
|
||||
#let isOut = `isOut`
|
||||
|
||||
#let readTag = `read`
|
||||
#let writeTag = `write`
|
||||
|
|
@ -40,9 +42,6 @@
|
|||
#let In = `In`
|
||||
#let Out = `Out`
|
||||
|
||||
#let cl = $chevron.l$
|
||||
#let cr = $chevron.r$
|
||||
|
||||
#let expr = `expr`
|
||||
#let stmt = `stmt`
|
||||
#let decl = `decl`
|
||||
|
|
@ -57,9 +56,9 @@
|
|||
{ 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
|
||||
{ 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[$not$ Write][] } ), // 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] } ),
|
||||
|
|
@ -89,8 +88,8 @@
|
|||
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[$readTag writeTag ()$][simple type representing all primitive types] // `Unit`
|
||||
Or[$rf copyTag space 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 ?
|
||||
|
|
@ -153,7 +152,7 @@
|
|||
Or[$0$][valid value of simple type] // `Unit`
|
||||
Or[$\#$][valid or spoiled value of simple type] // `Unit`
|
||||
Or[$bot$][spoiled value of simple type] // `Unit`
|
||||
Or[$lambda$][function pointer value] // `Fun`
|
||||
Or[$lambda type+ stmt$][function pointer value] // `Fun`
|
||||
Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref`
|
||||
Or[$[deepValue+]$][tuple value] // `Prod`
|
||||
}
|
||||
|
|
@ -164,8 +163,9 @@
|
|||
Or[$0$][valid value of simple type] // `Unit`
|
||||
Or[$\#$][valid or spoiled value of simple type] // `Unit`
|
||||
Or[$bot$][spoiled value of simple type] // `Unit`
|
||||
Or[$lambda$][function pointer value] // `Fun`
|
||||
Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
|
||||
Or[$lambda type+ stmt$][function pointer value] // `Fun`
|
||||
// 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`
|
||||
}
|
||||
),
|
||||
|
|
@ -178,12 +178,15 @@
|
|||
$v in value$ - произвольное значение
|
||||
|
||||
Получение #deepValue по #value:
|
||||
- $rf l xarrowSquiggly(mu)_#[deep] rf mu[l]$
|
||||
- $rf c l xarrowSquiggly(mu)_#[deep] rf c mu[l]$
|
||||
- $* xarrowSquiggly(mu)_#[deep] *$
|
||||
где $*$ - произвольный конструктор значения, кроме $rf$
|
||||
|
||||
== Memory Model
|
||||
|
||||
#let cl = $chevron.l$
|
||||
#let cr = $chevron.r$
|
||||
|
||||
#let mem = `mem`
|
||||
|
||||
- $LL$ - множество меток памяти
|
||||
|
|
@ -216,12 +219,8 @@ $X$ - можество переменных
|
|||
#let pathenvmem = `pathenvmem`
|
||||
#let pathenvtype = `pathenvtype`
|
||||
|
||||
#let vals = $Sigma$
|
||||
#let types = $Gamma$
|
||||
#let envv = $#[env]_Sigma$
|
||||
#let envt = $#[env]_Gamma$
|
||||
$sigma : envv := X -> LL, space vals : envv$ - #[ метки памяти перменных контекста, частично определённая функция ]
|
||||
$sigma : envt := X -> type, space types : envt$ - #[ типы значений перменных контекста, частично определённая функция ]
|
||||
#let env = `env`
|
||||
$sigma : env := X -> LL times type, space sigma : env$ - #[ метки памяти и типы значений пеерменных контекста, частично определённая функция ]
|
||||
|
||||
// $DD : X -> decl$ - глобальные определения, частично определённая функция
|
||||
|
||||
|
|
@ -240,9 +239,8 @@ $s in stmt, f in X, x in X, a in X$
|
|||
#let eqmu = $attach(=, br: mu)$
|
||||
#let arrmu = $attach(->, br: mu)$
|
||||
|
||||
#let arrpath = $xarrowSquiggly(mu)_path$
|
||||
|
||||
#let ttype = $attach(tack.r, br: type)$
|
||||
#let tpath = $attach(tack.r, br: path)$
|
||||
#let tmode = $attach(tack.r, br: mode)$
|
||||
|
||||
#let val = `val`
|
||||
|
|
@ -250,22 +248,22 @@ $s in stmt, f in X, x in X, a in X$
|
|||
#let tval = $attach(tack.r, br: val)$
|
||||
#let tlabel = $attach(tack.r, br: label)$
|
||||
|
||||
// TODO: TMP, deprecated
|
||||
// #let tetype = $attach(tack.r.double, br: type)$
|
||||
// #let temode = $attach(tack.r.double, br: mode)$
|
||||
// #let telabel = $attach(tack.r.double, br: label)$
|
||||
#let tetype = $attach(tack.r.double, br: type)$
|
||||
#let temode = $attach(tack.r.double, br: mode)$
|
||||
|
||||
#let teval = $attach(tack.r.double, br: val)$
|
||||
#let telabel = $attach(tack.r.double, br: label)$
|
||||
|
||||
// TODO: env mem label ??, env mem value ??
|
||||
|
||||
// TODO: FIXME: backwards, deconstruction ??
|
||||
- #[ Конструирование путей по переменой
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ variable path],
|
||||
|
||||
$@x arrpath x$,
|
||||
$x tpath @x$,
|
||||
)
|
||||
))
|
||||
#align(center, prooftree(
|
||||
|
|
@ -273,8 +271,8 @@ $s in stmt, f in X, x in X, a in X$
|
|||
rule(
|
||||
name: [ reference path],
|
||||
|
||||
$p arrpath x$,
|
||||
$rf p arrpath x$,
|
||||
$x tpath p$,
|
||||
$x tpath rf p$,
|
||||
)
|
||||
))
|
||||
#align(center, prooftree(
|
||||
|
|
@ -282,9 +280,9 @@ $s in stmt, f in X, x in X, a in X$
|
|||
rule(
|
||||
name: [ tuple access path],
|
||||
|
||||
$p arrpath x$,
|
||||
$x tpath p$,
|
||||
|
||||
$p.i arrpath x$,
|
||||
$x tpath p.i$,
|
||||
)
|
||||
))
|
||||
]
|
||||
|
|
@ -295,8 +293,7 @@ $s in stmt, f in X, x in X, a in X$
|
|||
rule(
|
||||
name: [ variable type access],
|
||||
|
||||
$x : t_x in types$,
|
||||
$types ttype @x : t_x$,
|
||||
$x : t_x ttype @x : t_x$,
|
||||
)
|
||||
))
|
||||
#align(center, prooftree(
|
||||
|
|
@ -304,8 +301,9 @@ $s in stmt, f in X, x in X, a in X$
|
|||
rule(
|
||||
name: [ reference type access],
|
||||
|
||||
$types ttype p : rf mode t_p$,
|
||||
$types ttype *p : t_p$,
|
||||
$x tpath p$,
|
||||
$x : t_x ttype p : rf mode t_p$,
|
||||
$x : t_x ttype *p : t_p$,
|
||||
)
|
||||
))
|
||||
#align(center, prooftree(
|
||||
|
|
@ -313,24 +311,44 @@ $s in stmt, f in X, x in X, a in X$
|
|||
rule(
|
||||
name: [ tuple type access],
|
||||
|
||||
$types ttype p : [t_1, ... t_n]$,
|
||||
$types ttype p.i : t_i$,
|
||||
$x tpath p$,
|
||||
$x : t_x ttype p : [t_1, ... t_n]$,
|
||||
$x : t_x ttype p.i : t_i$,
|
||||
)
|
||||
))
|
||||
]
|
||||
|
||||
// TODO: not required (trivial) ??
|
||||
// - #[ Получение read-write тега поля
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ rw tag access],
|
||||
- #[ Получение read-write тега поля
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ variable rw tag access],
|
||||
|
||||
// $types ttype p : cl r, w cr$,
|
||||
// $types tmode p -> cl r, w cr$,
|
||||
// )
|
||||
// ))
|
||||
// ]
|
||||
$t_x = r w ()$,
|
||||
$x : t_x tmode @x -> cr r w cl$,
|
||||
)
|
||||
))
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ reference rw tag access],
|
||||
|
||||
$x tpath p$,
|
||||
$x : t_x tmode p -> cr r w cl$,
|
||||
$x : t_x tmode *p -> cr r w cl$,
|
||||
)
|
||||
))
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ tuple rw tag access],
|
||||
|
||||
$x tpath p$,
|
||||
$x : t_x tmode p -> cr r w cl$,
|
||||
$x : t_x tmode p.i -> cr r w cl$,
|
||||
)
|
||||
))
|
||||
]
|
||||
|
||||
- #[ Получение значения поля
|
||||
#align(center, prooftree(
|
||||
|
|
@ -338,9 +356,7 @@ $s in stmt, f in X, x in X, a in X$
|
|||
rule(
|
||||
name: [ variable value access],
|
||||
|
||||
$x -> l in vals$,
|
||||
$mu[l] = v$,
|
||||
$vals, mu tval x eqmu v$,
|
||||
$x eqmu v_x tval @x eqmu v_x$,
|
||||
)
|
||||
))
|
||||
#align(center, prooftree(
|
||||
|
|
@ -348,8 +364,9 @@ $s in stmt, f in X, x in X, a in X$
|
|||
rule(
|
||||
name: [ reference value access],
|
||||
|
||||
$vals, mu tval p eqmu rf l$,
|
||||
$vals, mu tval *p eqmu mu[l]$,
|
||||
$x tpath p$,
|
||||
$x eqmu v_x tval p eqmu rf l$,
|
||||
$x eqmu v_x tval *p eqmu mu[l]$,
|
||||
)
|
||||
))
|
||||
#align(center, prooftree(
|
||||
|
|
@ -357,37 +374,52 @@ $s in stmt, f in X, x in X, a in X$
|
|||
rule(
|
||||
name: [ tuple value access],
|
||||
|
||||
$vals, mu tval p eqmu [v_1, ... v_n]$,
|
||||
$vals, mu tval p.i eqmu v_i$,
|
||||
$x tpath p$,
|
||||
$x eqmu v_x tmode p eqmu [v_1, ... v_n]$,
|
||||
$x eqmu v_x tmode p.i eqmu v_i$,
|
||||
)
|
||||
))
|
||||
]
|
||||
|
||||
// TODO: FIXME: not required (trivial) ??
|
||||
// - #[ Получение метки поля
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ access],
|
||||
- #[ Получение метки поля
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ access],
|
||||
|
||||
// $vals, mu tval p eqmu rf l$,
|
||||
// $vals, mu tmode p arrmu l$,
|
||||
// )
|
||||
// ))
|
||||
// ]
|
||||
$v_x = rf l$,
|
||||
$x eqmu v_x tval p eqmu rf l$,
|
||||
|
||||
// TODO: not required (trivial) ??
|
||||
// - #[ Получение read-write тега поля по окружению
|
||||
// #align(center, prooftree(
|
||||
// vertical-spacing: 4pt,
|
||||
// rule(
|
||||
// name: [ access],
|
||||
$x eqmu v_x tmode p arrmu l$,
|
||||
)
|
||||
))
|
||||
]
|
||||
|
||||
// $x : types[x] tmode p -> cr r space w cl$,
|
||||
// $sigma temode p -> cr r space w cl$,
|
||||
// )
|
||||
// ))
|
||||
// ]
|
||||
- #[ Получение типа поля по окружению
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ access],
|
||||
|
||||
$x tpath p$,
|
||||
$x : sigma[x].2 ttype p : t$,
|
||||
$sigma tetype p : t$,
|
||||
)
|
||||
))
|
||||
]
|
||||
|
||||
- #[ Получение read-write тега поля по окружению
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ access],
|
||||
|
||||
$x tpath p$,
|
||||
$x : sigma[x].2 tmode p -> cr r space w cl$,
|
||||
$sigma temode p -> cr r space w cl$,
|
||||
)
|
||||
))
|
||||
]
|
||||
|
||||
- #[ Получение значения поля по окружению
|
||||
#align(center, prooftree(
|
||||
|
|
@ -395,12 +427,33 @@ $s in stmt, f in X, x in X, a in X$
|
|||
rule(
|
||||
name: [ access],
|
||||
|
||||
$x eqmu vals[x] tval p eqmu v$,
|
||||
$types, vals, mu teval p eqmu x$,
|
||||
$x tpath p$,
|
||||
$x eqmu sigma[x].1 tval p eqmu v$,
|
||||
$sigma, mu teval p eqmu x$,
|
||||
)
|
||||
))
|
||||
]
|
||||
|
||||
- #[ Получение метки поля по окружению
|
||||
#align(center, prooftree(
|
||||
vertical-spacing: 4pt,
|
||||
rule(
|
||||
name: [ access],
|
||||
|
||||
$x tpath p$,
|
||||
$x eqmu sigma[x].1 tlabel p arrmu l$,
|
||||
$sigma, mu telabel p arrmu l$,
|
||||
)
|
||||
))
|
||||
]
|
||||
|
||||
=== Mode Accessors
|
||||
|
||||
#let modevar = $(i space o)$
|
||||
|
||||
$ isIn modevar = i == In $
|
||||
$ isOut modevar = o == Out $
|
||||
|
||||
// FIXME: move to new mode model
|
||||
// === Mode Correctness
|
||||
|
||||
|
|
@ -457,40 +510,27 @@ $s in stmt, f in X, x in X, a in X$
|
|||
// TODO: FIXME: check for mode, is recursion required ??
|
||||
// TODO: FIXME: check mode & access corectness in os correct
|
||||
|
||||
$ vals in envv, types in envt, space mu in mem, space m in mode,
|
||||
$ 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)
|
||||
|
||||
// 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$,
|
||||
$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 (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
|
||||
$(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$,
|
||||
|
||||
$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)$,
|
||||
$sigma, mu, m, c tcorrect v : r' space w' () -> r space w ()$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -501,10 +541,10 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ ref assignment tags correctness],
|
||||
|
||||
$types, vals, mu, m, c_r tcorrect v : t -> t'$,
|
||||
$sigma, 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'$,
|
||||
$sigma, mu, m, c tcorrect rf c_r space v : rf c' space t -> rf c_r space t'$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -515,13 +555,24 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ tuple assignmenttags correctness],
|
||||
|
||||
$types, vals, mu, m, c tcorrect v_1 : t_1 -> t'_1$,
|
||||
$sigma, mu, m, c tcorrect v_1 : t_1 -> t'_1$,
|
||||
|
||||
$...$,
|
||||
|
||||
$types, vals, mu, m, c tcorrect v_n : t_n -> t'_n$,
|
||||
$sigma, 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]$,
|
||||
$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)$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -529,8 +580,6 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
|
||||
=== Value Construction
|
||||
|
||||
// TODO: FIXME:add ref / copy modes correctness check
|
||||
|
||||
#let new = `new`
|
||||
|
||||
#align(center, prooftree(
|
||||
|
|
@ -539,7 +588,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
name: [ new $0$ value],
|
||||
|
||||
// TODO: check that access is what required ??
|
||||
$cl 0, mu cr xarrowSquiggly(cl r\, w cr)_new cl 0, mu cr$,
|
||||
$cl 0, mu cr xarrowSquiggly(space)_new cl 0, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -549,7 +598,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
name: [ new $\#$ value],
|
||||
|
||||
// TODO: check that access is what required ??
|
||||
$cl \#, mu cr xarrowSquiggly(cl r\, w cr)_new cl \#, mu cr$,
|
||||
$cl \#, mu cr xarrowSquiggly(space)_new cl \#, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -558,7 +607,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ new $bot$ value],
|
||||
|
||||
$cl bot, mu cr xarrowSquiggly(cl r\, w cr)_new cl bot, mu cr$,
|
||||
$cl bot, mu cr xarrowSquiggly(space)_new cl bot, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -576,10 +625,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ new reference ref value],
|
||||
|
||||
// TODO: FIXME: recursive copy ?? (what heppens if ref field has copy substructure ??)
|
||||
// frbidden ??
|
||||
|
||||
$cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
|
||||
$cl rf Ref l, mu cr xarrowSquiggly(space)_new cl rf Ref l, mu cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -588,11 +634,11 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ new reference copy value],
|
||||
|
||||
$cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$,
|
||||
$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 l, mu cr xarrowSquiggly(rf Copy t)_new cl rf l', mu_a cr$,
|
||||
$cl rf Copy l, mu cr xarrowSquiggly(space)_new cl rf Copy l', mu_a cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -601,11 +647,11 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ new tuple value],
|
||||
|
||||
$cl v_1, mu_0 cr xarrowSquiggly(t_1)_new cl lambda v'_1, mu_1 cr$,
|
||||
$cl v_1, mu_0 cr xarrowSquiggly(space)_new cl lambda v'_1, mu_1 cr$,
|
||||
$...$,
|
||||
$cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_new cl lambda v'_n, mu_n cr$,
|
||||
$cl v_n, mu_(n - 1) cr xarrowSquiggly(space)_new cl lambda v'_n, mu_n cr$,
|
||||
|
||||
$cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_new cl [v'_1, ... v'_n], mu_n cr$,
|
||||
$cl [v_1, ... v_n], mu_0 cr xarrowSquiggly(space)_new cl [v'_1, ... v'_n], mu_n cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -639,7 +685,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
|
||||
$isPossibleWrite mode$, // NOTE: weak requirement: may write
|
||||
$not isCopy mode$,
|
||||
$mode = (\_, not Out)$,
|
||||
$not isOut mode$,
|
||||
|
||||
$isCorrect_(cl sigma, mu cr) (mode, x)$,
|
||||
|
||||
|
|
@ -658,7 +704,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
$mu stretch(=>)^args_sigma gamma$,
|
||||
|
||||
$isAlwaysWrite mode$, // NOTE: strong requirement: should write
|
||||
$mode = (\_, not Out)$,
|
||||
$isOut mode$,
|
||||
|
||||
$isCorrect_(cl sigma, mu cr) (mode, x)$,
|
||||
|
||||
|
|
@ -770,11 +816,11 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ READ $p$],
|
||||
|
||||
$mu, types, vals teval p eqmu 0$,
|
||||
$mu, sigma teval p eqmu 0$,
|
||||
|
||||
$cl types, vals, mu cr
|
||||
$cl sigma, mu, l cr
|
||||
xarrow("READ" p)
|
||||
cl types, vals, mu cr$,
|
||||
cl sigma, mu, l cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -785,14 +831,17 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ WRITE $x$],
|
||||
|
||||
$types ttype p : cl r, w cr$,
|
||||
$w = MaybeWrite or w = AlwaysWrite$,
|
||||
$p arrpath x$,
|
||||
$sigma temode p -> cr r space w cl$,
|
||||
|
||||
$w == MaybeWrite or w == AlwaysWrite$,
|
||||
|
||||
$x tpath p$,
|
||||
|
||||
$mu[x] xarrowSquiggly(p)_write v$,
|
||||
|
||||
$cl types, vals, mu cr
|
||||
$cl sigma, mu cr
|
||||
xarrow("WRITE" p)
|
||||
cl types, vals, mu[x <- v] cr$,
|
||||
cl sigma, mu[x <- v] cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -803,17 +852,17 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ $s \; t$],
|
||||
|
||||
$cl types, vals, mu cr
|
||||
$cl sigma, mu cr
|
||||
stretch(->)^s
|
||||
cl types_s, vals_s, mu_s cr$,
|
||||
cl sigma_s, mu_s cr$,
|
||||
|
||||
$cl types_s, vals_s, mu_s cr
|
||||
$cl sigma, mu cr
|
||||
stretch(->)^t
|
||||
cl types_t, vals_t, mu_t cr$,
|
||||
cl sigma_t, mu_t cr$,
|
||||
|
||||
$cl types, vals, mu, cr
|
||||
$cl sigma, mu, cr
|
||||
xarrow(s \; t)
|
||||
cl types_t, vals_t, mu_t cr$,
|
||||
cl sigma_t, mu_t cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
@ -827,22 +876,21 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
|
|||
rule(
|
||||
name: [ $s | t$],
|
||||
|
||||
$cl types, vals, mu cr
|
||||
$cl sigma, mu, l cr
|
||||
stretch(->)^s
|
||||
cl types_s, vals_s, mu_s cr$,
|
||||
cl sigma_s, mu_s, l_s cr$,
|
||||
|
||||
$cl types, vals, mu cr
|
||||
$cl sigma, mu, l cr
|
||||
stretch(->)^t
|
||||
cl types_t, vals_t, mu_t cr$,
|
||||
cl sigma_t, mu_t, l_t cr$,
|
||||
|
||||
$types_s = types_t$,
|
||||
$vals_s = vals_t$,
|
||||
$sigma_s = sigma_t$,
|
||||
$mu' = combine(mu_s, mu_t)$,
|
||||
|
||||
// TODO changes ?? two ways ??
|
||||
$cl types, vals, mu cr
|
||||
$cl sigma, mu cr
|
||||
xarrow(s | t)
|
||||
cl types_t, vals_t, mu' cr$,
|
||||
cl sigma_t, mu' cr$,
|
||||
)
|
||||
))
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue