From 0937d91f54fa72250652569a067df1db52ad9729 Mon Sep 17 00:00:00 2001 From: ProgramSnail Date: Sat, 25 Apr 2026 13:45:24 +0000 Subject: [PATCH] structures: remove in & out accessors --- model_with_structures/model.typ | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ index 7016dff..0968b8b 100644 --- a/model_with_structures/model.typ +++ b/model_with_structures/model.typ @@ -24,8 +24,6 @@ #let isPossibleWrite = `isPossibleWrite` #let isRef = `isRef` #let isCopy = `isCopy` -#let isIn = `isIn` -#let isOut = `isOut` #let readTag = `read` #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 // === Mode Correctness @@ -479,10 +470,10 @@ $ vals in envv, types in envt, space mu in mem, space m in mode, rule( name: [ unit assignment tags correctness], - $r = Read => isIn m$, - $isOut m => w = AlwaysWrite$, + $r = Read => m = (In, \_)$, + $m = (\_, Out) => w = AlwaysWrite$, // $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 $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 $not isCopy mode$, - $not isOut mode$, + $mode = (\_, not Out)$, $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$, $isAlwaysWrite mode$, // NOTE: strong requirement: should write - $isOut mode$, + $mode = (\_, not Out)$, $isCorrect_(cl sigma, mu cr) (mode, x)$,