BEGIN OPEN ClientStateInfo
;
PrivateState: TYPE = REF InclusionRelation;
InclusionRelation: TYPE = { inside }; -- our model is that retained areas have state "inside", and unretained areas have state NIL
defaultState: PUBLIC State ← NEW[InclusionRelation ← inside ];
BooleanFunction: TYPE = { Union, Difference };
stateCombiner:
PUBLIC StateCombiner = {
RETURN[ NIL ]; -- Difference function (default)
};
StateEqual:
PUBLIC PROC [state1, state2: State]
RETURNS [
BOOL] ~ {
s1: PrivateState ← NARROW[state1];
s2: PrivateState ← NARROW[state2];
IF state1=NIL OR state2=NIL THEN RETURN[state1=NIL AND state2 = NIL];
RETURN[s1^ = s2^];
};
RopeFromState:
PUBLIC
PROC [state: State]
RETURNS [Rope.
ROPE] ~ {
s: PrivateState ← NARROW[state];
IF state=NIL THEN RETURN["NIL"];
IF s^ = inside THEN RETURN["inside"] ELSE ERROR;
};
StateFromRope:
PUBLIC
PROC [in: Rope.
ROPE]
RETURNS [s: State] ~ {
IF Rope.Equal[in, "NIL"] THEN RETURN[NIL] ELSE IF Rope.Equal[in, "inside"] THEN RETURN[NEW[InclusionRelation ← inside]] ELSE ERROR;
};
END.