BooleImpl.mesa
Copyright Ó 1985, 1987 by Xerox Corporation. All rights reversed.
Created by Bertrand Serlet July 31, 1985 3:03:17 pm PDT
Bertrand Serlet May 19, 1987 0:13:51 am PDT
Louis Monier June 3, 1986 7:28:32 pm PDT
Barth, August 26, 1986 12:29:31 pm PDT
DIRECTORY Boole, IO, Rope;
BooleImpl: CEDAR PROGRAM
IMPORTS IO, Rope
EXPORTS Boole =
BEGIN
OPEN Boole;
Expression Types and Constants
Constants
Constant: TYPE = REF ConstantRec;
ConstantRec: TYPE = RECORD [value: BOOL];
true: PUBLIC Expression ← NEW [ConstantRec ← [TRUE]];
false: PUBLIC Expression ← NEW [ConstantRec ← [FALSE]];
Negation
Neg: TYPE = REF NegRec;
NegRec: TYPE = RECORD [expr: Expression];
Alps
Alps: TYPE = REF AlpsRec;
AlpsRec: TYPE = RECORD [var: Variable, thenExpr, elseExpr: Expression];
The invariant is that none of thenExpr and elseExpr contains variable var, and that NOT Equal[thenExpr, elseExpr]. The order of variables in thenExpr and elseExpr might be different
ROPE: TYPE = Rope.ROPE;
Binary Operators
Op2Proc: TYPE = PROC [expr1, expr2: Expression] RETURNS [result: Expression];
And2: Op2Proc = {
result ← SELECT TRUE FROM
expr1=false => false,
expr2=false => false,
expr1=true => expr2,
expr2=true => expr1,
ENDCASE => Op2[And2, expr1, expr2];
};
Or2: Op2Proc = {
result ← SELECT TRUE FROM
expr1=false => expr2,
expr2=false => expr1,
expr1=true => true,
expr2=true => true,
ENDCASE => Op2[Or2, expr1, expr2];
};
Xor2: Op2Proc = {
result ← SELECT TRUE FROM
expr1=false => expr2,
expr2=false => expr1,
expr1=true => Not[expr2],
expr2=true => Not[expr1],
ENDCASE => Op2[Xor2, expr1, expr2];
};
Op2: PROC [op: Op2Proc, expr1, expr2: Expression] RETURNS [result: Expression] = {
It is assumed that neither of expr1 and expr2 are constants
var: Variable ← FindVar[expr1];
expr1True, expr1False, expr2True, expr2False: Expression;
IF var=NIL THEN ERROR;
[expr1True, expr1False] ← Eval[var, expr1];
[expr2True, expr2False] ← Eval[var, expr2];
result ← CreateAlps[var, op[expr1True, expr2True], op[expr1False, expr2False]];
};
CreateAlps: PROC [var: Variable, thenExpr, elseExpr: Expression] RETURNS [result: Expression] = {
IF HasVar[thenExpr, var] OR HasVar[elseExpr, var] THEN ERROR; -- Incorrect Alps formation
IF Equal[thenExpr, elseExpr] THEN RETURN [thenExpr];
result ← NEW [AlpsRec ← [var: var, thenExpr: thenExpr, elseExpr: elseExpr]];
};
Operators returning Expressions
Not: PUBLIC PROC [expr: Expression] RETURNS [result: Expression] = {
WITH expr SELECT FROM
constant: Constant => RETURN [IF expr=true THEN false ELSE true];
neg: Neg  => RETURN [neg.expr];
alps: Alps  => RETURN [NEW [NegRec ← [expr: expr]]];
ENDCASE  => RETURN [CreateAlps[expr, false, true]];
};
And: PUBLIC PROC [expr1, expr2, expr3, expr4, expr5: Expression ← true] RETURNS [result: Expression] = {
result ← AndList[LIST [expr1, expr2, expr3, expr4, expr5]];
};
Or: PUBLIC PROC [expr1, expr2, expr3, expr4, expr5: Expression ← false] RETURNS [result: Expression] = {
result ← OrList[LIST [expr1, expr2, expr3, expr4, expr5]];
};
Xor: PUBLIC PROC [expr1, expr2, expr3, expr4, expr5: Expression ← false] RETURNS [result: Expression] = {
result ← XorList[LIST [expr1, expr2, expr3, expr4, expr5]];
};
Nand: PUBLIC PROC [expr1, expr2, expr3, expr4, expr5: Expression ← true] RETURNS [result: Expression] = {
result ← NandList[LIST [expr1, expr2, expr3, expr4, expr5]];
};
Nor: PUBLIC PROC [expr1, expr2, expr3, expr4, expr5: Expression ← false] RETURNS [result: Expression] = {
result ← NorList[LIST [expr1, expr2, expr3, expr4, expr5]];
};
AndList: PUBLIC PROC [exprs: LIST OF Expression] RETURNS [result: Expression] = {
result ← true;
WHILE exprs#NIL DO result ← And2[result, exprs.first]; exprs ← exprs.rest ENDLOOP;
};
OrList: PUBLIC PROC [exprs: LIST OF Expression] RETURNS [result: Expression] = {
result ← false;
WHILE exprs#NIL DO result ← Or2[result, exprs.first]; exprs ← exprs.rest ENDLOOP;
};
XorList: PUBLIC PROC [exprs: LIST OF Expression] RETURNS [result: Expression] = {
result ← false;
WHILE exprs#NIL DO result ← Xor2[result, exprs.first]; exprs ← exprs.rest ENDLOOP;
};
NandList: PUBLIC PROC [exprs: LIST OF Expression] RETURNS [result: Expression] = {
result ← Not[AndList[exprs]];
};
NorList: PUBLIC PROC [exprs: LIST OF Expression] RETURNS [result: Expression] = {
result ← Not[OrList[exprs]];
};
If: PUBLIC PROC [cond, then, else: Expression] RETURNS [result: Expression] = {
IF Equal[then, else] THEN RETURN [then];
result ← Or2[And2[cond, then], And2[Not[cond], else]];
};
Public operations
EqualVar: PUBLIC PROC [var1, var2: Variable] RETURNS [BOOL] = {
IF ISTYPE [var1, REF TEXT] THEN var1 ← Rope.FromRefText[NARROW [var1]];
IF ISTYPE [var2, REF TEXT] THEN var2 ← Rope.FromRefText[NARROW [var2]];
WITH var1 SELECT FROM
constant: Constant => ERROR;
neg: Neg  => ERROR;
alps: Alps  => ERROR;
refInt: REF INT => RETURN [
IF ISTYPE [var2, REF INT] THEN refInt^=NARROW [var2, REF INT]^ ELSE var1=var2
];
ENDCASE  => RETURN [
IF ISTYPE [var1, ROPE] AND ISTYPE [var2, ROPE]
THEN Rope.Equal[NARROW [var1], NARROW [var2]]
ELSE var1=var2
];
};
Equal: PUBLIC PROC [expr1, expr2: Expression] RETURNS [BOOL] = {
neg: BOOL ← TRUE;
IF expr1=expr2 THEN RETURN [TRUE];
IF ISTYPE [expr1, Neg] THEN {neg ← ~neg; expr1 ← Not[expr1]};
IF ISTYPE [expr2, Neg] THEN {neg ← ~neg; expr2 ← Not[expr2]};
IF ISTYPE [expr1, Constant] AND ISTYPE [expr2, Constant] THEN RETURN [(expr1=expr2)=neg];
IF ISTYPE [expr1, Constant] OR ISTYPE [expr2, Constant] THEN RETURN [FALSE];
IF NOT ISTYPE [expr1, Alps] THEN expr1 ← CreateAlps[expr1, true, false];
IF NOT ISTYPE [expr2, Alps] THEN expr2 ← CreateAlps[expr2, true, false];
IF ~HasVar[expr2, FindVar[expr1]] THEN RETURN [FALSE];
IF ~HasVar[expr1, FindVar[expr2]] THEN RETURN [FALSE];
BEGIN
var: Variable ← FindVar[expr1];
expr1True, expr1False, expr2True, expr2False: Expression;
IF var=NIL THEN ERROR; -- expr1 has no Wire
[expr1True, expr1False] ← Eval[var, expr1];
[expr2True, expr2False] ← Eval[var, expr2];
IF NOT neg THEN {expr2True ← Not[expr2True]; expr2False ← Not[expr2False]};
RETURN [Equal[expr1True, expr2True] AND Equal[expr1False, expr2False]]
END;
};
Eval: PUBLIC PROC [var: Variable, expr: Expression] RETURNS [whenTrue, whenFalse: Expression] = {
WITH expr SELECT FROM
constant: Constant => RETURN [expr, expr];
neg: Neg  => {
[whenTrue, whenFalse] ← Eval[var, neg.expr];
whenTrue ← Not[whenTrue]; whenFalse ← Not[whenFalse];
};
alps: Alps  => IF EqualVar[alps.var, var]
THEN RETURN [alps.thenExpr, alps.elseExpr]
ELSE {
thenExprTrue, thenExprFalse, elseExprTrue, elseExprFalse: Expression;
[thenExprTrue, thenExprFalse] ← Eval[var, alps.thenExpr];
[elseExprTrue, elseExprFalse] ← Eval[var, alps.elseExpr];
whenTrue ← CreateAlps[alps.var, thenExprTrue, elseExprTrue];
whenFalse ← CreateAlps[alps.var, thenExprFalse, elseExprFalse];
};
ENDCASE  => IF EqualVar[var, expr] THEN RETURN [true, false] ELSE RETURN [expr, expr];
};
FullEval: PUBLIC PROC [expr: Expression, evalVar: EvalVar] RETURNS [Expression] = {
WITH expr SELECT FROM
constant: Constant => RETURN [expr];
neg: Neg => SELECT FullEval[neg.expr, evalVar] FROM
true => RETURN [false];
false => RETURN [true];
ENDCASE => RETURN [NIL];
alps: Alps => SELECT FullEval[alps.var, evalVar] FROM
true => RETURN [FullEval[alps.thenExpr, evalVar]];
false => RETURN [FullEval[alps.elseExpr, evalVar]];
ENDCASE => RETURN [NIL];
ENDCASE => RETURN [evalVar[expr]];
};
FindVar: PUBLIC PROC [expr: Expression] RETURNS [var: Variable] = {
WITH expr SELECT FROM
constant: Constant => RETURN [NIL];
neg: Neg  => RETURN [FindVar[neg.expr]];
alps: Alps  => RETURN [alps.var];
ENDCASE  => RETURN [expr];
};
EnumerateVars: PUBLIC PROC [expr: Expression, enumVar: EnumVar] = {
WITH expr SELECT FROM
constant: Constant => NULL;
neg: Neg => EnumerateVars[neg.expr, enumVar];
alps: Alps => {
EnumerateVars[alps.var, enumVar];
EnumerateVars[alps.thenExpr, enumVar];
EnumerateVars[alps.elseExpr, enumVar];
};
ENDCASE => enumVar[expr];
};
HasVar: PUBLIC PROC [expr: Expression, var: Variable] RETURNS [found: BOOL ← FALSE] = {
WITH expr SELECT FROM
constant: Constant => RETURN [FALSE];
neg: Neg  => RETURN [HasVar[neg.expr, var]];
alps: Alps  => RETURN [IF EqualVar[var, alps.var] THEN TRUE ELSE HasVar[alps.thenExpr, var] OR HasVar[alps.elseExpr, var]];
ENDCASE  => RETURN [EqualVar[var, expr]];
};
PutExpr: PUBLIC PROC [out: IO.STREAM, expr: Expression, deep: INT ← LAST [INT], putRefAny: PROC [IO.STREAM, Variable] ← NIL] = {
PutNeg: PROC [expr: Expression] = {
out.PutRope["Not["];
PutExpr[out, expr, deep-1, putRefAny];
out.PutRope["]"];
};
Var: PROC [var: Variable] = {
WITH var SELECT FROM
constant: Constant => ERROR;
neg: Neg  => ERROR;
alps: Alps  => ERROR;
rope: ROPE  => out.PutRope[Rope.Cat["""", rope, """"]];
text: REF TEXT => out.PutRope[Rope.Cat["""", Rope.FromRefText[text], """"]];
refInt: REF INT => out.Put[IO.rope["Int["], IO.int[refInt^], IO.rope["]"]];
ENDCASE  => {
out.PutRope["Var["];
IF putRefAny=NIL THEN out.Put1[IO.refAny[var]] ELSE putRefAny[out, var];
out.PutRope["]"];
};
};
IF deep<0 THEN out.PutRope[" ... "];
WITH expr SELECT FROM
constant: Constant => out.PutRope[IF constant.value THEN "1" ELSE "0"];
neg: Neg  => PutNeg[neg.expr];
alps: Alps  => {
SELECT Case[alps.thenExpr, alps.elseExpr] FROM
$Case10 => Var[alps.var];
$Case01 => PutNeg[alps.var];
$Case1X => {
out.PutRope["Or["];
Var[alps.var];
out.PutRope[", "];
PutExpr[out, alps.elseExpr, deep-1, putRefAny];
out.PutRope["]"];
};
$Case0X => {
out.PutRope["And["];
PutNeg[alps.var];
out.PutRope[", "];
PutExpr[out, alps.elseExpr, deep-1, putRefAny];
out.PutRope["]"];
};
$CaseX1 => {
out.PutRope["Or["];
PutNeg[alps.var];
out.PutRope[", "];
PutExpr[out, alps.thenExpr, deep-1, putRefAny];
out.PutRope["]"];
};
$CaseX0 => {
out.PutRope["And["];
Var[alps.var];
out.PutRope[", "];
PutExpr[out, alps.thenExpr, deep-1, putRefAny];
out.PutRope["]"];
};
$CaseXY => {
out.PutRope["If["];
Var[alps.var];
out.PutRope[", "];
PutExpr[out, alps.thenExpr, deep-1, putRefAny];
out.PutRope[", "];
PutExpr[out, alps.elseExpr, deep-1, putRefAny];
out.PutRope["]"];
};
ENDCASE   => ERROR;
};
ENDCASE  => Var[expr];
};
GetExpr: PUBLIC PROC [in: IO.STREAM, getRefAny: PROC [IO.STREAM] RETURNS [Variable] ← NIL] RETURNS [expr: Expression] = {
tokenKind: IO.TokenKind; token: ROPE;
[tokenKind, token] ← IO.GetCedarTokenRope[in];
SELECT TRUE FROM
Rope.Equal[token, "0"]   => RETURN [false];
Rope.Equal[token, "1"]   => RETURN [true];
Rope.Equal[token, "Not"] => {
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, "["] THEN ERROR;
expr ← Not[GetExpr[in, getRefAny]];
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, "]"] THEN ERROR;
};
Rope.Equal[token, "Or"]  => {
expr1, expr2: Expression;
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, "["] THEN ERROR;
expr1 ← GetExpr[in, getRefAny];
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, ","] THEN ERROR;
expr2 ← GetExpr[in, getRefAny];
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, "]"] THEN ERROR;
expr ← Or[expr1, expr2];
};
Rope.Equal[token, "And"]  => {
expr1, expr2: Expression;
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, "["] THEN ERROR;
expr1 ← GetExpr[in, getRefAny];
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, ","] THEN ERROR;
expr2 ← GetExpr[in, getRefAny];
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, "]"] THEN ERROR;
expr ← And[expr1, expr2];
};
Rope.Equal[token, "If"]  => {
var, thenExpr, elseExpr: Expression;
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, "["] THEN ERROR;
var ← GetExpr[in, getRefAny];
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, ","] THEN ERROR;
thenExpr ← GetExpr[in, getRefAny];
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, ","] THEN ERROR;
elseExpr ← GetExpr[in, getRefAny];
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, "]"] THEN ERROR;
expr ← If[var, thenExpr, elseExpr];
};
Rope.Equal[token, "Int"] => {
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, "["] THEN ERROR;
expr ← NEW [INT ← IO.GetInt[in]];
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, "]"] THEN ERROR;
};
Rope.Equal[token, "Var"] => {
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, "["] THEN ERROR;
expr ← getRefAny[in];
IF NOT Rope.Equal[IO.GetCedarTokenRope[in].token, "]"] THEN ERROR;
};
tokenKind=tokenROPE  => expr ← Rope.Substr[token, 1, Rope.Length[token]-2];
ENDCASE      => ERROR;
};
ToRope: PUBLIC PROC [expr: Expression, deep: INT ← 5] RETURNS [ROPE] = {
out: IO.STREAM ← IO.ROS[];
PutExpr[out, expr, deep];
RETURN [IO.RopeFromROS[out]];
};
FromRope: PUBLIC PROC [rope: Rope.ROPE] RETURNS [Expression] = {
RETURN [GetExpr[IO.RIS[rope]]];
};
Private operations that depend on the representation
Case: PUBLIC PROC [whenTrue, whenFalse: Expression] RETURNS [case: ATOM] = {
case ← SELECT TRUE FROM
Equal[whenTrue, true] AND Equal[whenFalse, true]  => $Case11,
Equal[whenTrue, false] AND Equal[whenFalse, false]  => $Case00,
Equal[whenTrue, true] AND Equal[whenFalse, false]  => $Case10,
Equal[whenTrue, false] AND Equal[whenFalse, true]  => $Case01,
Equal[whenTrue, true]           => $Case1X,  
Equal[whenTrue, false]           => $Case0X,  
Equal[whenFalse, true]           => $CaseX1,  
Equal[whenFalse, false]           => $CaseX0,
Equal[whenTrue, whenFalse]         => $CaseXX,
ENDCASE               => $CaseXY;
};
END.