st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-06-10 19:28:16 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Compare commits

base: st:8fc0ffa805bc383c47b9c0bad35171ee24835421
Branches Tags
st:main
st:lambdas_no_value
st:memory_ext
...
compare: st:0c83218109f52de3fbcdd9ef6790b0b2a358f626
Branches Tags
st:main
st:lambdas_no_value
st:memory_ext

3 commits
8fc0ffa805 ... 0c83218109

Author SHA1 Message Date
ProgramSnail
0c83218109 struct: model: add substructure read / write 2026-05-16 16:20:46 +00:00
ProgramSnail
d684b8eeb9 struct: progam eval rule in modal, fix func eval rule 2026-05-16 12:49:05 +00:00
ProgramSnail
506ea25b10 struct: lambda tags check fix in model 2026-05-16 12:28:31 +00:00
1 changed files with 57 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

60
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(
vertical-spacing: 4pt,
rule(
name: [ modify final value],
name: [ modify final value: unit],
$cl cdl v_m, v_r, v_w cdr, mu cr
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)
#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(
vertical-spacing: 4pt,
rule(
@ -785,7 +811,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
rule(
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$,
)
))
@ -1385,7 +1411,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
rule(
name: [ lambda check],
$mu ttags lambda space overline(s) :$,
$mu ttags lambda space overline(s) : lambda overline(t)$,
)
))
#align(center, prooftree(
@ -1418,6 +1444,7 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
// TODO: FIXME: introduce global types and vals
$types_0 = types_#[glob]$,
$vals_0 = vals_#[glob]$,
$mu_0 = mu$,
// NOTE: dashed arrow to fill context
$cl types_0, vals_0, mu_0 cr
@ -1572,4 +1599,31 @@ $s in stmt, f in X, x in X, a in X, p in path, pi in revpath$
)
))
=== Program Evaluation
#let progeval = `prog eval`
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ program evaluation],
// NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers)
// expect well typed program
$cl types_0, vals_0, mu_0 cr xarrowSquiggly(d_1)_init cl types_1, vals_1, mu_1 cr$,
$...$,
$cl types_(n - 1), vals_(n - 1), mu_(n - 1) cr xarrowSquiggly(d_n)_init cl types_n, vals_n, mu_n cr$,
// TODO: FIXME: some easy way to pass to eval ??
$types_#[glob] = types_n$,
$vals_#[glob] = vals_n$,
$mu_#[glob] = mu_n$,
$cl types_n, vals_n, mu_n cr xarrow(s) cl types', vals', mu' cr$,
$cl types_0, vals_0, mu_0 cr xarrowSquiggly(d_1 ... d_n s)_prog_eval cl types', vals', mu' cr$
)
))
]