AssertingImpl:
CEDAR
MONITOR
IMPORTS IO, IOClasses, List, Rope, SS: StructuredStreams
EXPORTS Asserting, AssertingIO =
{OPEN Asserting, AssertingIO;
Error: PUBLIC ERROR [a: Assertion] = CODE;
Warning: PUBLIC SIGNAL [a: Assertion] = CODE;
readers, writers:
PUBLIC Assertions ←
NIL;
Functions from reln to read or write proc.
ROPE: TYPE = Rope.ROPE;
Bool: TYPE = REF BOOL;
Int: TYPE = REF INT;
Reel: TYPE = REF REAL;
Proc: TYPE = REF PROC ANY RETURNS ANY;
LORA: TYPE = LIST OF REF ANY;
Cons:
PUBLIC
PROC [reln: Term, terms: Terms]
RETURNS [a: Assertion] =
{a ← List.DotCons[reln, terms]};
RelnOf:
PUBLIC
PROC [a: Assertion]
RETURNS [reln: Term] = {
reln ← a.key};
TermsOf:
PUBLIC
PROC [a: Assertion]
RETURNS [terms: Terms] = {
terms ← NARROW[a.val]};
ToAssertion:
PUBLIC
PROC [terms: Terms]
RETURNS [a: Assertion] =
{a ← Cons[terms.first, terms.rest]};
ToAssertions:
PUBLIC
PROC [terms: Terms]
RETURNS [as: Assertions] = {
tail: Assertions ← as ← NIL;
FOR terms ← terms, terms.rest
WHILE terms #
NIL
DO
lora: LORA ← NARROW[terms.first];
this: Assertions ← LIST[Cons[lora.first, lora.rest]];
IF as = NIL THEN as ← this ELSE tail.rest ← this;
tail ← this;
ENDLOOP;
};
Assert:
PUBLIC
PROC [reln: Term, terms: Terms, inAdditionTo: Assertions]
RETURNS [allTogetherNow: Assertions] =
{allTogetherNow ← CONS[Cons[reln, terms], inAdditionTo]};
Test:
PUBLIC
PROC [reln: Term, terms: Terms, in: Assertions]
RETURNS [
BOOL] = {
FOR in ← in, in.rest
WHILE in #
NIL
DO
IF Equal[RelnOf[in.first], reln] AND Equal[TermsOf[in.first], terms] THEN RETURN [TRUE];
ENDLOOP;
RETURN [FALSE];
};
AssertionsNotAbout:
PUBLIC
PROC [reln: Term, from: Assertions]
RETURNS [filtered: Assertions] = {
filtered ← NIL;
FOR from ← from, from.rest
WHILE from #
NIL
DO
IF NOT Equal[RelnOf[from.first], reln] THEN filtered ← CONS[from.first, filtered];
ENDLOOP;
filtered ← filtered --so we can break at exit--};
AssertionsAbout:
PUBLIC
PROC [reln: Term, from: Assertions]
RETURNS [filtered: Assertions] = {
filtered ← NIL;
FOR from ← from, from.rest
WHILE from #
NIL
DO
IF Equal[RelnOf[from.first], reln] THEN filtered ← CONS[from.first, filtered];
ENDLOOP;
filtered ← filtered --so we can break at exit--};
EnumerateAssertionsAbout:
PUBLIC
PROC [reln: Term, from: Assertions, to: AssertionConsumer] = {
FOR from ← from, from.rest
WHILE from #
NIL
DO
IF Equal[RelnOf[from.first], reln] THEN to[from.first];
ENDLOOP;
};
AssertFn:
PUBLIC
PROC [fn: Term, terms: Terms, inAdditionTo: Assertions, numArgs:
INT ← 0]
RETURNS [allTogetherNow: Assertions] = {
prefix, prefixTail: Assertions ← NIL;
IF NOT numArgs IN [0 .. List.Length[terms]] THEN ERROR;
FOR al: Assertions ← inAdditionTo, al.rest
WHILE al #
NIL
DO
l2: Terms ← CONS[fn, terms];
l1: Terms ← CONS[RelnOf[al.first], TermsOf[al.first]];
FOR i:
INT
IN [0 .. numArgs]
DO
IF NOT Equal[l1.first, l2.first] THEN GOTO NotThisOne;
l1 ← l1.rest;
l2 ← l2.rest;
ENDLOOP;
IF prefixTail #
NIL
THEN {
prefixTail.rest ← CONS[Cons[fn, terms], al.rest];
RETURN [prefix]}
ELSE RETURN[CONS[Cons[fn, terms], al.rest]];
REPEAT
NotThisOne => {
prefix ← CONS[al.first, prefix];
IF prefixTail = NIL THEN prefixTail ← prefix;
};
ENDLOOP;
allTogetherNow ← CONS[Cons[fn, terms], inAdditionTo]};
AssertFn1:
PUBLIC
PROC [fn, val: Term, inAdditionTo: Assertions, args: Terms ←
NIL]
RETURNS [allTogetherNow: Assertions] =
{allTogetherNow ← AssertFn[fn: fn, terms: List.Append[args, LIST[val]], inAdditionTo: inAdditionTo, numArgs: List.Length[args]]};
FnVals:
PUBLIC
PROC [fn: Term, from: Assertions, args: Terms ←
NIL]
RETURNS [vals: Terms] = {
l2: Terms ← CONS[fn, args];
numArgs: INT ← List.Length[args];
FOR al: Assertions ← from, al.rest
WHILE al #
NIL
DO
l1: Terms ← CONS[RelnOf[al.first], TermsOf[al.first]];
FOR i:
INT
IN [0 .. numArgs]
DO
IF NOT Equal[l1.first, l2.first] THEN EXIT;
l1 ← l1.rest;
l2 ← l2.rest;
IF l1 = NIL THEN ERROR;
REPEAT
FINISHED => RETURN [l1];
ENDLOOP;
ENDLOOP;
vals ← NIL};
FnVal:
PUBLIC
PROC [fn: Term, from: Assertions, args: Terms ←
NIL]
RETURNS [val: Term] = {
vals: Terms ← FnVals[fn: fn, from: from, args: args];
IF vals = NIL THEN RETURN [NIL];
IF vals.rest # NIL THEN ERROR Error[Cons[$NotSingleValued, vals]];
val ← vals.first;
};
CheckFn:
PUBLIC
PROC [fn: Term, in: Assertions, args: Terms ←
NIL] = {
found: INT ← 0;
l2: Terms ← CONS[fn, args];
numArgs: INT ← List.Length[args];
FOR al: Assertions ← in, al.rest
WHILE al #
NIL
DO
l1: Terms ← CONS[RelnOf[al.first], TermsOf[al.first]];
FOR i:
INT
IN [0 .. numArgs]
DO
IF NOT Equal[l1.first, l2.first] THEN EXIT;
l1 ← l1.rest;
l2 ← l2.rest;
IF l1 = NIL THEN ERROR;
REPEAT
FINISHED => found ← found + 1;
ENDLOOP;
ENDLOOP;
IF found # 1 THEN ERROR Error[Cons[$NotFunctional, LIST[fn, in, NEW [INT ← found]]]]};
Union:
PUBLIC
PROC [a, b: Assertions]
RETURNS [c: Assertions] = {
c ← b;
WHILE a #
NIL
DO
c ← CONS[a.first, c];
a ← a.rest;
ENDLOOP;
c ← c};
Equal:
PUBLIC
PROC [a, b: Term]
RETURNS [
BOOL] = {
IF (a = NIL) # (b = NIL) THEN RETURN [FALSE];
IF a = NIL THEN RETURN [TRUE];
WITH a
SELECT
FROM
aa: ATOM => RETURN [a = b];
ra: ROPE => RETURN [ISTYPE[b, ROPE] AND ra.Equal[NARROW[b]]];
ba: Bool => RETURN [ISTYPE[b, Bool] AND ba^ = NARROW[b, Bool]^];
ia: Int => RETURN [ISTYPE[b, Int] AND ia^ = NARROW[b, Int]^];
ra: Reel => RETURN [ISTYPE[b, Reel] AND ra^ = NARROW[b, Reel]^];
pa: Proc => RETURN [ISTYPE[b, Proc] AND pa^ = NARROW[b, Proc]^];
ca: Terms =>
IF
ISTYPE[b, Terms]
THEN {
cb: Terms ← NARROW[b];
WHILE (ca #
NIL)
AND (cb #
NIL)
DO
IF NOT Equal[ca.first, cb.first] THEN RETURN [FALSE];
ca ← ca.rest;
cb ← cb.rest;
ENDLOOP;
RETURN [(ca = NIL) = (cb = NIL)];
} ELSE RETURN [FALSE];
ENDCASE => RETURN [a = b];
};
GeneralWrite:
PUBLIC
PROC [to:
IO.
STREAM, assertion: Assertion] = {
to.PutChar['(];
SS.Begin[to];
{ENABLE UNWIND => SS.End[to];
SS.Bp[to, FALSE, 2];
to.Put[IO.refAny[RelnOf[assertion]]];
FOR terms: Terms ← TermsOf[assertion], terms.rest
WHILE terms #
NIL
DO
to.PutChar[' ];
SS.Bp[to, FALSE, 2];
to.Put[IO.refAny[terms.first]];
ENDLOOP;
SS.Bp[to, FALSE, 0];
};
SS.End[to];
to.PutChar[')];
};
l: LORA ← CONS[RelnOf[assertion], TermsOf[assertion]];
to.Put[IO.refAny[l]]};
DontWrite: PUBLIC PROC [to: IO.STREAM, assertion: Assertion] = {};
GeneralRead:
PUBLIC
PROC [from:
IO.
STREAM, reln: Term]
RETURNS [assertion: Assertion] = {
in: IO.STREAM ← IOClasses.CreateCatInputStream[IO.RIS["("], from];
rest: Terms ← NARROW[in.GetRefAny[]];
assertion ← Cons[reln, rest]};
SetReader:
PUBLIC
ENTRY
PROC [reln: Term, rp: ReadProc] = {
ENABLE UNWIND => {};
readers ← AssertFn1[reln, NEW [ReadProc ← rp], readers]};
SetWriter:
PUBLIC
ENTRY
PROC [reln: Term, wp: WriteProc] = {
ENABLE UNWIND => {};
writers ← AssertFn1[reln, NEW [WriteProc ← wp], writers]};
GetReader:
PUBLIC
PROC [reln: Term]
RETURNS [rp: ReadProc] = {
rr: REF ReadProc ← NARROW[FnVal[reln, readers]];
rp ← IF rr = NIL THEN GeneralRead ELSE rr^};
GetWriter:
PUBLIC
PROC [reln: Term]
RETURNS [wp: WriteProc] = {
wr: REF WriteProc ← NARROW[FnVal[reln, writers]];
wp ← IF wr = NIL THEN GeneralWrite ELSE wr^};
WriteAssn:
PUBLIC
PROC [to:
IO.
STREAM, assertion: Assertion] = {
wp: WriteProc ← GetWriter[RelnOf[assertion]];
wp[to: to, assertion: assertion]};
ReadAssn:
PUBLIC
PROC [from:
IO.
STREAM]
RETURNS [assertion: Assertion] = {
reln: Term;
rp: ReadProc;
char: CHAR ← from.GetChar[];
IF char # '( THEN ERROR;
reln ← from.GetRefAny[];
rp ← GetReader[reln];
assertion ← rp[from: from, reln: reln]};
Read:
PUBLIC
PROC [from:
IO.
STREAM]
RETURNS [assertions: Assertions] = {
char: CHAR;
[] ← from.SkipWhitespace[];
IF from.EndOf[] THEN ERROR Error[Cons[$EndOfFile, LIST[from]]];
char ← from.GetChar[];
IF char # '( THEN ERROR Error[Cons[$NotAssertions, LIST[from]]];
DO
ass: Assertion;
[] ← from.SkipWhitespace[];
IF from.EndOf[] THEN ERROR Error[Cons[$EndOfFile, LIST[from]]];
char ← from.GetChar[];
IF char = '^
THEN {
IF from.EndOf[] THEN ERROR Error[Cons[$EndOfFile, LIST[from]]];
char ← from.GetChar[]};
SELECT char
FROM
') => RETURN;
'( => NULL;
ENDCASE => ERROR Error[Cons[$SyntaxError, LIST[from]]];
from.Backup['(];
ass ← ReadAssn[from: from];
assertions ← CONS[ass, assertions];
ENDLOOP;
};
Write:
PUBLIC
PROC [to:
IO.
STREAM, assertions: Assertions] = {
to.PutRope["("];
SS.Begin[to];
{ENABLE UNWIND => SS.End[to];
FOR assertions ← assertions, assertions.rest
WHILE assertions #
NIL
DO
SS.Bp[to, TRUE, 2];
WriteAssn[to, assertions.first];
IF assertions.rest # NIL THEN to.PutChar[' ];
ENDLOOP;
SS.Bp[to, TRUE, 0];
};
SS.End[to];
to.PutRope[")"];
};
WriteTail:
PUBLIC
PROC [to:
IO.
STREAM, assertions: Assertions] = {
FOR assertions ← assertions, assertions.rest
WHILE assertions #
NIL
DO
to.PutChar[' ];
SS.Bp[to, TRUE, 2];
WriteAssn[to, assertions.first];
ENDLOOP;
};
}.