st/pass_strategy_synthesis
1
0
Fork 0
mirror of https://github.com/ProgramSnail/pass_strategy_synthesis.git synced 2026-04-30 17:52:41 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

structures: context initialization semantics

Browse source
This commit is contained in:
ProgramSnail 2026-04-29 12:25:56 +00:00
parent 35de5946f0
commit 1d28d01c17
1 changed files with 35 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

35
model_with_structures/model.typ
View file

@ -743,6 +743,41 @@ $s in stmt, f in X, x in X, a in X$
) )
)) ))
=== Context Initialization
#let init = `init`
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ add variable declaration],
// NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers)
// expect well typed program
$vals, mu texpre e eqmu v$,
$types texprt e : t'$,
$mu xarrowSquiggly(v)_#[add] cl l, mu' cr$,
$cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu' cr$
)
))
#h(10pt)
#align(center, prooftree(
vertical-spacing: 4pt,
rule(
name: [ add function declaration],
$cl types, vals, mu cr
xarrowSquiggly("fun" f (x_1 space : space m_1 t_1, ... space x_n space : space m_n t_n) space = space s)_init
cl types[f <- lambda space [t_1, ... t_n]], vals[f <- lambda space [[x_1, ... x_n] s], mu cr$
)
))
#h(10pt)
=== Call Values Spoil === Call Values Spoil
#let spoil = `spoil` #let spoil = `spoil`