FilingP10V5AuxImpl:
CEDAR
PROGRAM
IMPORTS Convert, Rope, AuthenticationP14V2Aux, FilingAttributesP10V5Aux
EXPORTS FilingP10V5Aux ~ {
OPEN FilingP10V5, FilingP10V5Aux;
ROPE: TYPE ~ Rope.ROPE;
ExposeSecondaryCredentials:
PUBLIC
PROC [arg: SecondaryCredentials, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← Rope.Cat["SecondaryCredentials(", ExposeStrength[arg.type, (level+1)], "): "];
WITH arg
SELECT
FROM
it:
REF SecondaryCredentialsObject.none => {
res ← Rope.Concat[res, ExposeEmptyRecord[it.none, (level+1)]] };
it:
REF SecondaryCredentialsObject.simple => {
res ← Rope.Concat[res, ExposeSecondary[it.simple, (level+1)]] };
it:
REF SecondaryCredentialsObject.strong => {
res ← Rope.Concat[res, ExposeEncryptedSecondary[it.strong, (level+1)]] };
ENDCASE => ERROR
};
ExposeEmptyRecord:
PUBLIC
PROC [arg: EmptyRecord, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[]";
};
ExposeTransferProblem:
PUBLIC
PROC [arg: TransferProblem, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
aborted => res ← "aborted";
checksumIncorrect => res ← "checksumIncorrect";
formatIncorrect => res ← "formatIncorrect";
noRendevous => res ← "noRendevous";
wrongDirection => res ← "wrongDirection";
ENDCASE => ERROR
};
ExposeByteRange:
PUBLIC
PROC [arg: ByteRange, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
res ← Rope.Cat[res, "firstByte~", Convert.RopeFromCard[arg.firstByte], ", "];
res ← Rope.Cat[res, "count~", Convert.RopeFromCard[arg.count], "]"];
};
ExposePatternFilter:
PUBLIC
PROC [arg: PatternFilter, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
res ← Rope.Cat[res, "attribute~", FilingAttributesP10V5Aux.ExposeAttribute[arg.attribute, (level+1)], "]"];
};
ExposeDirection:
PUBLIC
PROC [arg: Direction, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
forward => res ← "forward";
backward => res ← "backward";
ENDCASE => ERROR
};
ExposeConnectionProblem:
PUBLIC
PROC [arg: ConnectionProblem, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
noRoute => res ← "noRoute";
noResponse => res ← "noResponse";
transmissionHardware => res ← "transmissionHardware";
transportTimeout => res ← "transportTimeout";
tooManyLocalConnections => res ← "tooManyLocalConnections";
tooManyRemoteConnections => res ← "tooManyRemoteConnections";
missingCourier => res ← "missingCourier";
missingProgram => res ← "missingProgram";
missingProcedure => res ← "missingProcedure";
protocolMismatch => res ← "protocolMismatch";
parameterInconsistency => res ← "parameterInconsistency";
invalidMessage => res ← "invalidMessage";
returnTimedOut => res ← "returnTimedOut";
otherCallProblem => res ← "otherCallProblem";
ENDCASE => ERROR
};
ExposeFilterType:
PUBLIC
PROC [arg: FilterType, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
less => res ← "less";
lessOrEqual => res ← "lessOrEqual";
equal => res ← "equal";
notEqual => res ← "notEqual";
greaterOrEqual => res ← "greaterOrEqual";
greater => res ← "greater";
and => res ← "and";
or => res ← "or";
not => res ← "not";
none => res ← "none";
all => res ← "all";
matches => res ← "matches";
ENDCASE => ERROR
};
ExposeScopeSequence:
PUBLIC
PROC [arg: ScopeSequence, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
FOR i:
CARDINAL
IN [0..arg.length)
DO
res ← Rope.Cat[res, IF i>0 THEN ", " ELSE NIL, ExposeScope[arg.body[i], (level+1)]];
ENDLOOP;
res ← Rope.Concat[res, "]"];
};
ExposeControlType:
PUBLIC
PROC [arg: ControlType, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
lock => res ← "lock";
timeout => res ← "timeout";
access => res ← "access";
ENDCASE => ERROR
};
ExposeScope:
PUBLIC
PROC [arg: Scope, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← Rope.Cat["Scope(", ExposeScopeType[arg.type, (level+1)], "): "];
WITH arg
SELECT
FROM
it:
REF ScopeObject.count => {
res ← Rope.Concat[res, Convert.RopeFromCard[it.count]] };
it:
REF ScopeObject.depth => {
res ← Rope.Concat[res, Convert.RopeFromCard[it.depth]] };
it:
REF ScopeObject.direction => {
res ← Rope.Concat[res, ExposeDirection[it.direction, (level+1)]] };
it:
REF ScopeObject.filter => {
res ← Rope.Concat[res, ExposeFilter[it.filter, (level+1)]] };
ENDCASE => ERROR
};
ExposeHandle:
PUBLIC
PROC [arg: Handle, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
FOR i:
CARDINAL
IN [0..2)
DO
res ← Rope.Cat[res, IF i>0 THEN ", " ELSE NIL, Convert.RopeFromCard[arg[i]]];
ENDLOOP;
res ← Rope.Concat[res, "]"];
};
ExposeSecondary:
PUBLIC
PROC [arg: Secondary, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
FOR i:
CARDINAL
IN [0..arg.length)
DO
res ← Rope.Cat[res, IF i>0 THEN ", " ELSE NIL, ExposeSecondaryItem[arg.body[i], (level+1)]];
ENDLOOP;
res ← Rope.Concat[res, "]"];
};
ExposeSessionToken:
PUBLIC
PROC [arg: SessionToken, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
FOR i:
CARDINAL
IN [0..2)
DO
res ← Rope.Cat[res, IF i>0 THEN ", " ELSE NIL, Convert.RopeFromCard[arg[i]]];
ENDLOOP;
res ← Rope.Concat[res, "]"];
};
ExposeInsertionProblem:
PUBLIC
PROC [arg: InsertionProblem, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
positionUnavailable => res ← "positionUnavailable";
fileNotUnique => res ← "fileNotUnique";
loopInHierarchy => res ← "loopInHierarchy";
ENDCASE => ERROR
};
ExposeFilter:
PUBLIC
PROC [arg: Filter, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← Rope.Cat["Filter(", ExposeFilterType[arg.type, (level+1)], "): "];
WITH arg
SELECT
FROM
it:
REF FilterObject.less => {
res ← Rope.Concat[res, ExposeRelationFilter[it.less, (level+1)]] };
it:
REF FilterObject.lessOrEqual => {
res ← Rope.Concat[res, ExposeRelationFilter[it.lessOrEqual, (level+1)]] };
it:
REF FilterObject.equal => {
res ← Rope.Concat[res, ExposeRelationFilter[it.equal, (level+1)]] };
it:
REF FilterObject.notEqual => {
res ← Rope.Concat[res, ExposeRelationFilter[it.notEqual, (level+1)]] };
it:
REF FilterObject.greaterOrEqual => {
res ← Rope.Concat[res, ExposeRelationFilter[it.greaterOrEqual, (level+1)]] };
it:
REF FilterObject.greater => {
res ← Rope.Concat[res, ExposeRelationFilter[it.greater, (level+1)]] };
it:
REF FilterObject.and => {
res ← Rope.Concat[res, ExposeEmptyRecord[it.and, (level+1)]] };
it:
REF FilterObject.or => {
res ← Rope.Concat[res, ExposeEmptyRecord[it.or, (level+1)]] };
it:
REF FilterObject.not => {
res ← Rope.Concat[res, ExposeEmptyRecord[it.not, (level+1)]] };
it:
REF FilterObject.none => {
res ← Rope.Concat[res, ExposeEmptyRecord[it.none, (level+1)]] };
it:
REF FilterObject.all => {
res ← Rope.Concat[res, ExposeEmptyRecord[it.all, (level+1)]] };
it:
REF FilterObject.matches => {
res ← Rope.Concat[res, ExposePatternFilter[it.matches, (level+1)]] };
ENDCASE => ERROR
};
ExposeSecondaryItem:
PUBLIC
PROC [arg: SecondaryItem, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
res ← Rope.Cat[res, "type~", Convert.RopeFromCard[arg.type], ", "];
res ← Rope.Cat[res, "value~", ExposeSecondaryValueType[arg.value, (level+1)], "]"];
};
ExposeSession:
PUBLIC
PROC [arg: Session, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
res ← Rope.Cat[res, "token~", ExposeSessionToken[arg.token, (level+1)], ", "];
res ← Rope.Cat[res, "verifier~", AuthenticationP14V2Aux.ExposeSeqWords[arg.verifier, (level+1)], "]"];
};
ExposeAttributeTypeSequence:
PUBLIC
PROC [arg: AttributeTypeSequence, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
FOR i:
CARDINAL
IN [0..arg.length)
DO
res ← Rope.Cat[res, IF i>0 THEN ", " ELSE NIL, Convert.RopeFromCard[arg.body[i]]];
ENDLOOP;
res ← Rope.Concat[res, "]"];
};
ExposeRelationFilter:
PUBLIC
PROC [arg: RelationFilter, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
res ← Rope.Cat[res, "attribute~", FilingAttributesP10V5Aux.ExposeAttribute[arg.attribute, (level+1)], ", "];
res ← Rope.Cat[res, "interpretation~", FilingAttributesP10V5Aux.ExposeInterpretation[arg.interpretation, (level+1)], "]"];
};
ExposeEncryptedSecondary:
PUBLIC
PROC [arg: EncryptedSecondary, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
FOR i:
CARDINAL
IN [0..arg.length)
DO
res ← Rope.Cat[res, IF i>0 THEN ", " ELSE NIL, AuthenticationP14V2Aux.ExposeBlock[arg.body[i], (level+1)]];
ENDLOOP;
res ← Rope.Concat[res, "]"];
};
ExposeArgumentProblem:
PUBLIC
PROC [arg: ArgumentProblem, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
illegal => res ← "illegal";
disallowed => res ← "disallowed";
unreasonable => res ← "unreasonable";
unimplemented => res ← "unimplemented";
duplicated => res ← "duplicated";
missing => res ← "missing";
ENDCASE => ERROR
};
ExposeSecondaryValueType:
PUBLIC
PROC [arg: SecondaryValueType, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
FOR i:
CARDINAL
IN [0..arg.length)
DO
res ← Rope.Cat[res, IF i>0 THEN ", " ELSE NIL, Convert.RopeFromCard[arg.body[i]]];
ENDLOOP;
res ← Rope.Concat[res, "]"];
};
ExposeSpaceProblem:
PUBLIC
PROC [arg: SpaceProblem, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
allocationExceeded => res ← "allocationExceeded";
attributeAreaFull => res ← "attributeAreaFull";
mediumFull => res ← "mediumFull";
ENDCASE => ERROR
};
ExposeServiceProblem:
PUBLIC
PROC [arg: ServiceProblem, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
cannotAuthenticate => res ← "cannotAuthenticate";
serviceFull => res ← "serviceFull";
serviceUnavailable => res ← "serviceUnavailable";
sessionInUse => res ← "sessionInUse";
serviceUnknown => res ← "serviceUnknown";
ENDCASE => ERROR
};
ExposeAccessProblem:
PUBLIC
PROC [arg: AccessProblem, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
accessRightsInsufficient => res ← "accessRightsInsufficient";
accessRightsIndeterminate => res ← "accessRightsIndeterminate";
fileChanged => res ← "fileChanged";
fileDamaged => res ← "fileDamaged";
fileInUse => res ← "fileInUse";
fileNotFound => res ← "fileNotFound";
fileOpen => res ← "fileOpen";
ENDCASE => ERROR
};
ExposeScopeType:
PUBLIC
PROC [arg: ScopeType, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
count => res ← "count";
direction => res ← "direction";
filter => res ← "filter";
depth => res ← "depth";
ENDCASE => ERROR
};
ExposeStrength:
PUBLIC
PROC [arg: Strength, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
none => res ← "none";
simple => res ← "simple";
strong => res ← "strong";
ENDCASE => ERROR
};
ExposeHandleProblem:
PUBLIC
PROC [arg: HandleProblem, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
invalid => res ← "invalid";
nullDisallowed => res ← "nullDisallowed";
directoryRequired => res ← "directoryRequired";
ENDCASE => ERROR
};
ExposeSecondaryType:
PUBLIC
PROC [arg: SecondaryType, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
FOR i:
CARDINAL
IN [0..arg.length)
DO
res ← Rope.Cat[res, IF i>0 THEN ", " ELSE NIL, Convert.RopeFromCard[arg.body[i]]];
ENDLOOP;
res ← Rope.Concat[res, "]"];
};
ExposeControlTypeSequence:
PUBLIC
PROC [arg: ControlTypeSequence, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
FOR i:
CARDINAL
IN [0..arg.length)
DO
res ← Rope.Cat[res, IF i>0 THEN ", " ELSE NIL, ExposeControlType[arg.body[i], (level+1)]];
ENDLOOP;
res ← Rope.Concat[res, "]"];
};
ExposeSessionProblem:
PUBLIC
PROC [arg: SessionProblem, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
tokenInvalid => res ← "tokenInvalid";
serviceAlreadySet => res ← "serviceAlreadySet";
ENDCASE => ERROR
};
ExposeControlSequence:
PUBLIC
PROC [arg: ControlSequence, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
FOR i:
CARDINAL
IN [0..arg.length)
DO
res ← Rope.Cat[res, IF i>0 THEN ", " ELSE NIL, ExposeControl[arg.body[i], (level+1)]];
ENDLOOP;
res ← Rope.Concat[res, "]"];
};
ExposeLogicFilter:
PUBLIC
PROC [arg: LogicFilter, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← "[";
FOR i:
CARDINAL
IN [0..arg.length)
DO
res ← Rope.Cat[res, IF i>0 THEN ", " ELSE NIL, ExposeFilter[arg.body[i], (level+1)]];
ENDLOOP;
res ← Rope.Concat[res, "]"];
};
ExposeControl:
PUBLIC
PROC [arg: Control, level:
NAT]
RETURNS [res:
ROPE] ~ {
res ← Rope.Cat["Control(", ExposeControlType[arg.type, (level+1)], "): "];
WITH arg
SELECT
FROM
it:
REF ControlObject.lock => {
res ← Rope.Concat[res, ExposeLock[it.lock, (level+1)]] };
it:
REF ControlObject.timeout => {
res ← Rope.Concat[res, Convert.RopeFromCard[it.timeout]] };
it:
REF ControlObject.access => {
res ← Rope.Concat[res, FilingAttributesP10V5Aux.ExposeAccessSequence[it.access, (level+1)]] };
ENDCASE => ERROR
};
ExposeLock:
PUBLIC
PROC [arg: Lock, level:
NAT]
RETURNS [res:
ROPE] ~ {
SELECT arg
FROM
lockNone => res ← "lockNone";
share => res ← "share";
exclusive => res ← "exclusive";
ENDCASE => ERROR
};