st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-06-11 03:38:15 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

struct: model: add substructure read / write

Browse source
This commit is contained in:
ProgramSnail 2026-05-16 16:20:46 +00:00
parent d684b8eeb9
commit 0c83218109
1 changed files with 28 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

30
model_with_structures/model.typ
View file

@ -758,7 +758,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ modify final value], name: [ modify final value: unit],
$cl cdl v_m, v_r, v_w cdr, mu cr $cl cdl v_m, v_r, v_w cdr, mu cr
xarrowSquiggly(cl \# . \, a cr)_modify xarrowSquiggly(cl \# . \, a cr)_modify
@ -768,6 +768,32 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
#h(10pt) #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( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
@ -785,7 +811,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
rule( rule(
name: [ modify tuple value], name: [ modify tuple value],
$cl v_i, mu cr xarrowSquiggly(cl p \, a cr)_modify cl v'_i, mu', cr$, $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$, $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$,
) )
)) ))