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

structures: remove in & out accessors

Browse source
This commit is contained in:
ProgramSnail 2026-04-25 13:45:24 +00:00
parent e786cc6135
commit 0937d91f54
1 changed files with 5 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

19
model_with_structures/model.typ
View file

@ -24,8 +24,6 @@
#let isPossibleWrite = `isPossibleWrite` #let isPossibleWrite = `isPossibleWrite`
#let isRef = `isRef` #let isRef = `isRef`
#let isCopy = `isCopy` #let isCopy = `isCopy`
#let isIn = `isIn`
#let isOut = `isOut`
#let readTag = `read` #let readTag = `read`
#let writeTag = `write` #let writeTag = `write`
@ -403,13 +401,6 @@ $s in stmt, f in X, x in X, a in X$
)) ))
] ]
=== Mode Accessors
#let modevar = $(i space o)$
$ isIn modevar = (i = In) $
$ isOut modevar = (o = Out) $
// FIXME: move to new mode model // FIXME: move to new mode model
// === Mode Correctness // === Mode Correctness
@ -479,10 +470,10 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
rule( rule(
name: [ unit assignment tags correctness], name: [ unit assignment tags correctness],
$r = Read => isIn m$, $r = Read => m = (In, \_)$,
$isOut m => w = AlwaysWrite$, $m = (\_, Out) => w = AlwaysWrite$,
// $sigma temode x -> cr r' space w' cl$, // NOTE: not required, value passed // $sigma temode x -> cr r' space w' cl$, // NOTE: not required, value passed
$(w = AlwaysWrite or w = MaybeWrite) and (isOut m or c = Ref) => w' = AlwaysWrite$, $(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
// $sigma, mu teval x eqmu v$, // NOTE: not required, value passed // $sigma, mu teval x eqmu v$, // NOTE: not required, value passed
$v in {0, \#, bot}$, $v in {0, \#, bot}$,
@ -648,7 +639,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
$isPossibleWrite mode$, // NOTE: weak requirement: may write $isPossibleWrite mode$, // NOTE: weak requirement: may write
$not isCopy mode$, $not isCopy mode$,
$not isOut mode$, $mode = (\_, not Out)$,
$isCorrect_(cl sigma, mu cr) (mode, x)$, $isCorrect_(cl sigma, mu cr) (mode, x)$,
@ -667,7 +658,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
$mu stretch(=>)^args_sigma gamma$, $mu stretch(=>)^args_sigma gamma$,
$isAlwaysWrite mode$, // NOTE: strong requirement: should write $isAlwaysWrite mode$, // NOTE: strong requirement: should write
$isOut mode$, $mode = (\_, not Out)$,
$isCorrect_(cl sigma, mu cr) (mode, x)$, $isCorrect_(cl sigma, mu cr) (mode, x)$,