st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-04-26 16:24:50 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

structures: combine + combine all

Browse source
This commit is contained in:
ProgramSnail 2026-04-25 15:07:16 +00:00
parent 18d19051c4
commit fd29f7d3da
1 changed files with 33 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

47
model_with_structures/model.typ
View file

@ -657,7 +657,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
rule(
name: [ combine trivial $0$ values],
$mu xarrowSquiggly(cl 0 \, 0 cr)_combine cl 0, mu cr$
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl 0 \, 0 cr)_combine cl 0, mu cr$
)
))
@ -668,7 +668,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
rule(
name: [ combine trivial $bot$ values],
$mu xarrowSquiggly(cl bot \, bot cr)_combine cl bot, mu cr$
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl bot \, bot cr)_combine cl bot, mu cr$
)
))
@ -682,7 +682,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
$v_1 in {0, \#, bot}$,
$v_2 in {0, \#, bot}$,
$v_1 != v_2$,
$mu xarrowSquiggly(cl v_1 \, v_2 cr)_combine cl \#, mu cr$
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl v_1 \, v_2 cr)_combine cl \#, mu cr$
)
))
@ -693,23 +693,25 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
rule(
name: [ combine lambda values],
$mu xarrowSquiggly(cl lambda \, lambda cr)_combine cl lambda, mu cr$
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl lambda \, lambda cr)_combine cl lambda, mu cr$
)
))
#h(10pt)
// NOTE: combine inplace, destroy values (actually only the first value)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ combine reference values (inplace)],
$mu xarrowSquiggly(cl mu[l_1] \, mu[l_2] cr)_combine cl v', mu' cr$,
// NOTE: not inplace variant // TODO FIXME: choose variant
// 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$,
// $mu xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l', mu'' cr$
$mu xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l_1, mu'[l_1 <- v'] cr$
// $cl mu_1, mu_2, mu cr xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l', mu'' cr$
// NOTE: version to use with "combine all"
$l_1 = l_2$,
$cl mu_1, mu_2, mu cr xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l_1, mu cr$
)
))
@ -720,10 +722,28 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
rule(
name: [ combine tuple values],
$mu_0 xarrowSquiggly(cl v^1_1 \, v^2_1 cr)_combine cl v'_1, mu_1 cr$,
$cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl v^1_1 \, v^2_1 cr)_combine cl v'_1, mu'_1 cr$,
$...$,
$mu_(n - 1) xarrowSquiggly(cl v^1_n \, v^2_n cr)_combine cl v'_n, mu_n cr$,
$mu_0 xarrowSquiggly(cl [v^1_1, ... v^1_n] \, [v^2_1 ... v^2_n] cr)_combine cl [v'_1, ... v'_n], mu_n cr$
$cl mu_1, mu_2, mu'_(n - 1) cr xarrowSquiggly(cl v^1_n \, v^2_n cr)_combine cl v'_n, mu'_n cr$,
$cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl [v^1_1, ... v^1_n] \, [v^2_1 ... v^2_n] cr)_combine cl [v'_1, ... v'_n], mu'_n cr$
)
))
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ combine tuple values],
$mu'_0 = nothing$,
// NOTE: same labels required
$mu_1 = {l_1 -> v^1_1, ... l_n -> v^1_n}$,
$mu_2 = {l_1 -> v^2_1, ... l_n -> v^2_n}$,
$cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl v^1_1 \, v^2_1 cr)_combine cl v'_1, mu'_1 cr$,
$...$,
$cl mu_1, mu_2, mu'_(n - 1) cr xarrowSquiggly(cl v^1_n \, v^2_n cr)_combine cl v'_n, mu'_n cr$,
$cl mu_1, mu_2 cr xarrowSquiggly(space)_#[combine all] mu'_n cr$
)
))
@ -933,7 +953,6 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
#h(10pt)
*TODO: combine replacement* // FIXME
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
@ -949,7 +968,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
$types_s = types_t$,
$vals_s = vals_t$,
$mu' = combine(mu_s, mu_t)$,
$cl mu_s, mu_t cr xarrowSquiggly(space)_#[combine all] mu'$,
// TODO changes ?? two ways ??
$cl types, vals, mu cr