DIRECTORY  Boole, IO, Rope;

BooleImpl: CEDAR PROGRAM
IMPORTS IO, Rope
EXPORTS Boole = 
BEGIN 
OPEN Boole;
Constant: TYPE = REF ConstantRec;
ConstantRec: TYPE = RECORD [value: BOOL];

true: PUBLIC Expression _ NEW [ConstantRec _ [TRUE]];
false: PUBLIC Expression _ NEW [ConstantRec _ [FALSE]];
Neg: TYPE = REF NegRec;
NegRec: TYPE = RECORD [expr: Expression];
Alps: TYPE = REF AlpsRec;
AlpsRec: TYPE = RECORD [var: Variable, thenExpr, elseExpr: Expression];
ROPE: TYPE = Rope.ROPE;
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] = {
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]];
};
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]];
};
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, $Case0X, $CaseX1, $CaseX0, $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, "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]]];
};
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.
 
΄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 April 2, 1987 9:37:46 pm PST
Louis Monier June 3, 1986 7:28:32 pm PDT
Barth, August 26, 1986 12:29:31 pm PDT

Expression Types and Constants
Constants

Negation

Alps
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

Binary Operators 
It is assumed that neither of expr1 and expr2 are constants
Operators returning Expressions
Public operations
Private operations that depend on the representation
Κ€–

"cedar" style˜
codeš
œ™Jš
œB™BJ™7J™,K™(K™&K™—KšΟk	œ	œ˜J˜•StartOfExpansion[]šΟn	œœ
˜Kšœ
œ˜Kšœ	˜Kšœ
˜Kšœ˜—
head™™	Kšœ
œœ
˜!Kšœ
œœ	œ˜)J˜Jšœœœœ˜5Jšœœœœ˜7K™—™Kšœœœ˜Kšœœœ˜)K™—™Kšœœœ	˜šœ	œœ1˜GKšœTœ_™Ά
K™——Kšœœœ
˜—š
œ™K–I -- [design: Core.Design, me: Core.CellType] RETURNS [new: Core.CellType]šœ	œœœ˜MK˜šžœ
˜šœ	œ
œ
˜Kš
œ˜Kš
œ˜Kš
œ˜Kš
œ˜Kšœ˜#—K˜—K–I -- [design: Core.Design, me: Core.CellType] RETURNS [new: Core.CellType]˜–I -- [design: Core.Design, me: Core.CellType] RETURNS [new: Core.CellType]šžœ
˜šœ	œ
œ
˜Kš
œ˜Kš
œ˜Kš
œ˜Kš
œ˜Kšœ˜"—K˜—K˜–I -- [design: Core.Design, me: Core.CellType] RETURNS [new: Core.CellType]šžœ
˜šœ	œ
œ
˜Kš
œ˜Kš
œ˜Kš
œ˜Kš
œ˜Kšœ˜#—K˜—K˜šžœœ)œ˜RKš
œ;™;Kš
œ˜Jš
œ9˜9Jšœœ
œ
œ
˜Jš
œ+˜+Jš
œ+˜+Jš
œO˜OK˜—K˜šž
œœ1œ˜aKš	œœœ
œΟc˜YKšœœ
œ˜4Kšœ	œ@˜LK˜——š
œ™šžœœ
œœ˜Dšœœ
˜Kš	œœœœœ˜AKšœ
œ˜Kšœœœ˜4Kšœœ!˜3—K˜—K˜šžœœ
œ8œ˜hKšœœ&˜;Kš
œ˜—šžœœ
œ9œ˜hKšœœ&˜:Kš
œ˜—šžœœ
œ9œ˜iKšœœ&˜;Kš
œ˜—šžœœ
œ8œ˜iKšœœ&˜<Kš
œ˜—šžœœ
œ9œ˜iKšœœ&˜;Kš
œ˜—K˜šžœœ
œ	œ
œ
œ˜QKš
œ˜Kšœœ
œ8œ
˜RK˜—šžœœ
œ	œ
œ
œ˜PKš
œ˜Kšœœ
œ7œ
˜QK˜—šžœœ
œ	œ
œ
œ˜QKš
œ˜Kšœœ
œ8œ
˜RK˜—šžœœ
œ	œ
œ
œ˜RKš
œ˜K˜—šžœœ
œ	œ
œ
œ˜QKš
œ˜K˜—K˜šžœœ
œ œ˜OKšœœ
œ˜(Kš
œ6˜6K˜——™š
žœœ
œœœ˜?Kšœ
œœ
œœœ	˜GKšœ
œœ
œœœ	˜Gšœœ
˜Kšœœ
˜Kšœ
œ
˜Kšœœ
˜šœœ
œœ˜Kšœ
œœ
œœ	œœ
œœ
˜MK˜—šœœ˜šœ
œœœ
œœ˜/Kšœœ	œ˜-Kšœ
˜—K˜—K˜—K˜—š
žœœ
œœœ˜@Kšœœœ
˜Kšœ
œ
œœ˜"Kšœ
œœ"˜=Kšœ
œœ"˜=Kšœ
œœ
œœ
œ˜YKšœ
œœ
œœ
œœ˜LKšœ
œ
œœ(˜HKšœ
œ
œœ(˜HKšœ œ
œœ˜6Kšœ œ
œœ˜6š
˜Kš
œ˜Kš
œ9˜9Kš	œœ
œ
œŸ˜+Kš
œ+˜+Kš
œ+˜+Kšœ
œœ<˜KKšœœ˜FKšœ
˜—K˜K˜—šžœœ
œ#œ&˜ašœœ
˜Kšœœ˜*š
œ˜Jš
œ,˜,Kš
œ5˜5K˜—šœœ˜*Kšœ
œ ˜+šœ˜Kš
œE˜EKš
œ9˜9Kš
œ9˜9Kš
œ<˜<Kš
œ?˜?K˜——Kšœœœ
œœ
œ˜V—K˜K˜—šžœœ
œ&œ˜Sšœœ
˜Kšœœ˜$šœœ˜3Kšœœ	˜Kšœ	œ˜Kšœœœ˜—šœœ˜5Kšœœ$˜2Kšœ	œ$˜3Kšœœœ˜—Kšœœ˜"—K˜K˜—šžœœ
œœ˜Cšœœ
˜Kšœœœ˜#Kšœ
œ˜(Kšœœ˜!Kšœœ˜—J˜J˜—šž
œœ
œ)˜Cšœœ
˜Kšœœ
˜Kš
œ-˜-š
œ˜Kš
œ!˜!Kš
œ&˜&Kš
œ&˜&K˜—Kšœ˜—K˜K˜—šžœœ
œ#œ	œœ˜Wšœœ
˜Kšœœœ˜%Kšœ
œ˜,Kš
œœœœ
œ
œœ˜{Kšœœ˜)—K˜K˜—šžœœ
œœ
œœœœœœ
œœ˜€
šžœœ˜#Kš
œ˜Kš
œ&˜&Kš
œ˜K˜—šžœœ˜šœœ
˜Kšœœ
˜Kšœ
œ
˜Kšœœ
˜Kšœœ-˜7Kšœœ
œ>˜LKšœœ
œœœœ˜Kšœ˜
Kš
œ˜Kš
œœ
œ
œœ˜HKš
œ˜K˜——K˜—Kšœœ˜$šœœ
˜Kšœ"œœœ˜GKš
œ˜š
œ˜šœ$˜.Kš
œ˜Kš
œ˜š
œ0˜0Kš
œ˜Kš
œ˜Kš
œ˜Kš
œ/˜/Kš
œ˜Kš
œ/˜/Kš
œ˜K˜—Kšœœ
˜—K˜—Kšœ˜—J˜J˜—šžœœ
œœ
œ
œœ
œœœœ˜yJšœœœ
˜%Jšœœ˜.šœ
œ
˜Jšœœ	˜+Jšœœ˜*š
œ˜Jš
œ
œœ#œ
œ
˜BJš
œ#˜#Jš
œ
œœ#œ
œ
˜BJ˜—š
œ˜Jš
œ$˜$Jš
œ
œœ#œ
œ
˜BJš
œ˜Jš
œ
œœ#œ
œ
˜BJš
œ"˜"Jš
œ
œœ#œ
œ
˜BJš
œ"˜"Jš
œ
œœ#œ
œ
˜BJš
œ#˜#J˜—š
œ˜Jš
œ
œœ#œ
œ
˜BJšœœœœ
˜!Jš
œ
œœ#œ
œ
˜BJ˜—š
œ˜Jš
œ
œœ#œ
œ
˜BJš
œ˜Jš
œ
œœ#œ
œ
˜BJ˜—Jš
œK˜KJšœ	œ
˜—J˜J˜—šžœœ
œœœœ˜HJš	œœ
œœ
œ˜Jš
œ˜Jšœœ˜J˜J˜—š
žœœ
œ
œœ˜@Jšœ
œ
œ	˜J˜——™4š
žœœ
œ#œœ˜Lšœœ
œ
˜Jšœœ$˜=Jšœœ%˜?Jšœœ%˜>Jšœœ$˜>Jš
œ-˜-Jš
œ.˜.Jš
œ.˜.Jš
œ-˜-Jš
œ.˜.Jšœ˜!—J˜——Kšœ
˜K˜
—…—,,?`