
    <<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.