st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-04-29 09:14:35 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

structures: statement eval fix (?)

Browse source
This commit is contained in:
ProgramSnail 2026-04-25 16:15:23 +00:00
parent 9d21c99556
commit eb90ba5449
1 changed files with 10 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

28
model_with_structures/model.typ
View file

@ -351,8 +351,6 @@ $s in stmt, f in X, x in X, a in X$
=== Eval Rules === Eval Rules
#let args = `args`
#[ #[
#let ref = `ref` #let ref = `ref`
@ -685,7 +683,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
rule( rule(
name: [ spoil step], name: [ spoil step],
$mu stretch(=>)^args_sigma gamma$, $mu stretch(=>)^"args"_sigma gamma$,
$isPossibleWrite mode$, // NOTE: weak requirement: may write $isPossibleWrite mode$, // NOTE: weak requirement: may write
$not isCopy mode$, $not isCopy mode$,
@ -694,7 +692,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
$isCorrect_(cl sigma, mu cr) (mode, x)$, $isCorrect_(cl sigma, mu cr) (mode, x)$,
// gamma - memory (as mu) // gamma - memory (as mu)
$gamma stretch(=>)^((mode, x) : args)_sigma "pathenvval"(gamma, sigma, x) <- bot]$ $gamma stretch(=>)^((mode, x) : "args")_sigma "pathenvval"(gamma, sigma, x) <- bot]$
) )
)) ))
@ -705,7 +703,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
rule( rule(
name: [ fix step], name: [ fix step],
$mu stretch(=>)^args_sigma gamma$, $mu stretch(=>)^"args"_sigma gamma$,
$isAlwaysWrite mode$, // NOTE: strong requirement: should write $isAlwaysWrite mode$, // NOTE: strong requirement: should write
$mode = (\_, not Out)$, $mode = (\_, not Out)$,
@ -715,7 +713,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
$isCorrect_(cl sigma, mu cr) (mode, x)$, $isCorrect_(cl sigma, mu cr) (mode, x)$,
// gamma - memory (as mu) // gamma - memory (as mu)
$gamma stretch(=>)^((mode, x) : args)_sigma "pathenvval"(gamma, sigma, x) <- 0]$ $gamma stretch(=>)^((mode, x) : "args")_sigma "pathenvval"(gamma, sigma, x) <- 0]$
) )
)) ))
@ -726,7 +724,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
rule( rule(
name: [ skip step], name: [ skip step],
$mu stretch(=>)^args_sigma gamma$, $mu stretch(=>)^"args"_sigma gamma$,
$not "spoil step"$, $not "spoil step"$,
$not "fix step"$, $not "fix step"$,
@ -734,7 +732,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
$isCorrect_(cl sigma, mu cr) (mode, x)$, $isCorrect_(cl sigma, mu cr) (mode, x)$,
// mu // mu
$gamma stretch(=>)^((mode, x) : args)_sigma gamma$ $gamma stretch(=>)^((mode, x) : "args")_sigma gamma$
) )
)) ))
@ -896,16 +894,10 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
#align(center, prooftree( #align(center, prooftree(
vertical-spacing: 4pt, vertical-spacing: 4pt,
rule( rule(
name: [ CALL $f space overline(p)$], name: [ CALL $f space [p_1, ... p_n]$],
// TODO: FIXME: take corresponding statement & var names $vals, mu texpre f eqmu lambda [x_1, ... x_n] space s$,
// use eval ?? $types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
[*TODO: statement (from value?) + x'es \<\- expr eval ? *],
$types ttype f : lambda args $,
$args = [m_1 t_1, ... m_n t_n]$,
$overline(p) = [p_1, ... p_n]$,
$overline(x) = [x_1, ... x_n]$,
// TODO: add args before statement eval // TODO: add args before statement eval
@ -933,7 +925,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
$gamma_(n - 1) stretch(=>)^(x_n space m_n space t_n)_(cl vals, types cr) gamma_n$, $gamma_(n - 1) stretch(=>)^(x_n space m_n space t_n)_(cl vals, types cr) gamma_n$,
$cl vals, types, mu, l cr $cl vals, types, mu, l cr
xarrow("CALL" f space overline(p)) xarrow("CALL" f space [p_1, ... p_n])
cl vals, types, gamma_n, l cr$, cl vals, types, gamma_n, l cr$,
) )
)) ))