FormulasImpl.mesa
Last Edited by: Arnon, June 10, 1985 4:19:22 pm PDT
DIRECTORY
Rope,
Basics,
IO,
Atom,
AlgebraClasses,
Bools,
MathExpr,
MathConstructors,
Variables,
DistribPolys,
Polynomials,
FormulaOperators,
Formulas;
FormulasImpl: CEDAR PROGRAM
IMPORTS Rope, IO, Atom, AlgebraClasses, Bools, DistribPolys, Polynomials, MathConstructors, FormulaOperators
EXPORTS Formulas =
BEGIN OPEN AC: AlgebraClasses, VARS: Variables, DP: DistribPolys, POL: Polynomials, Formulas;
TypeError: PUBLIC ERROR [message: ATOM ← $Unspecified] = CODE;
Class for a Boolean Algebra of Formulas
ClassPrintName: AC.PrintNameProc = {
data: FormulaAlgebraData ← NARROW[structure.instanceData];
RETURN[Rope.Concat[
"Formulas in ",
data.polynomialRing.class.printName[data.polynomialRing]
] ];
};
ClassShortPrintName: AC.PrintNameProc = {
data: FormulaAlgebraData ← NARROW[structure.instanceData];
RETURN[Rope.Cat[
"F(",
data.polynomialRing.class.shortPrintName[data.polynomialRing],
")"
] ];
};
ClassIsElementOf: AC.ElementOfProc = {
Assumes that if item is a formula, then it really belongs to the domain pointed to by its structure field.
formula: Formula;
IF NOT ISTYPE[item, Formula] THEN RETURN[FALSE];
formula ← NARROW[item];
IF NOT structure.class.structureEqual[structure, formula.structure] THEN RETURN[FALSE];
RETURN[ TRUE ]
};
ClassLegalFirstChar: AC.LegalFirstCharOp = {
data: FormulaAlgebraData ← NARROW[structure.instanceData];
IF data.polynomialRing.class.legalFirstChar[char, data.polynomialRing] THEN RETURN[TRUE];
RETURN[char = '( OR char = '~ OR char = '[ ];
Legal first char of formula is either legal first char of polynomial, or ( or [ or ~
};
ClassRead: AC.ReadOp = {
termChar: CHAR;
formula: Formula;
[formula, termChar] ← ReadFormula[in, structure];
RETURN[formula ];
};
formulaOps: FormulaOps ← NEW[FormulaOpsRec ← [
allVarEval: AllVarEv
] ];
formulaProp: Atom.DottedPair ← NEW[Atom.DottedPairNode← [$FormulaAlgebra, formulaOps]];
formulaClass: PUBLIC AC.StructureClass ← NEW[AC.StructureClassRec ← [
category: lattice,
printName: ClassPrintName,
shortPrintName: ClassShortPrintName,
structureEqual: AC.defaultStructureEqualityTest,
isElementOf: ClassIsElementOf,
legalFirstChar: ClassLegalFirstChar,
read: ClassRead,
fromRope: FromRope,
toRope: ToRope,
write: Write,
toExpr: ToExpr,
add: Disjunct,
negate: Negate, -- hack
multiply: Conjunct,
divide: Difference,
booleanAlgebra: TRUE,
complement: Negate,
propList: LIST[formulaProp]
] ];
Constructor for a Boolean Algebra of Formulas
MakeFormulaAlgebra: PUBLIC PROC [polynomialRing: AC.Structure] RETURNS [formulaAlgebra: AC.Structure] ~ {
formulaAlgebraData: FormulaAlgebraData ← NEW[FormulaAlgebraDataRec ← [
polynomialRing: polynomialRing
] ];
formulaAlgebra ← NEW[AC.StructureRec ← [
class: formulaClass,
instanceData: formulaAlgebraData
] ];
};
Extract Formula Operations from Class Property Lists
IsFormulaAlgebra: PUBLIC PROC [structure: AC.Structure] RETURNS [BOOL] ~ {
IF Atom.GetPropFromList[structure.class.propList, $FormulaAlgebra] # NIL THEN RETURN[TRUE] ELSE RETURN[FALSE];
};
AllVarEval: PUBLIC PROC [formulaAlgebra: AC.Structure] RETURNS [AC.BinaryOp] ~ {
formulaOps: FormulaOps ← NARROW[ Atom.GetPropFromList[formulaAlgebra.class.propList, $FormulaAlgebra] ];
IF formulaOps = NIL THEN ERROR;
RETURN[formulaOps.allVarEval];
};
Conversion and I/O
ReadFormula: PUBLIC PROC [in: IO.STREAM, formulaAlgebra: AC.Structure] RETURNS [formula: Formula, termChar: CHAR] ~ {
Assumes that formula is quantifier-free, and is either an atomic formula, a formula enclosed in parentheses, the negation of a formula enclosed in parenthesis, a disjunction of formulas, or a conjunction of formulas. Termination is either by end of stream, or $, or an extra ) (for recursive calls). If by end of stream, then termChar = NUL. If by $, then the $ is removed from in. If by ), the ) is not removed from in.
char: CHAR;
junct: Formula;
list, listTail: LIST OF Formula ← NIL;
formulaAlgebraData: FormulaAlgebraData ← NARROW[formulaAlgebra.instanceData];
polynomialRing: AC.Structure ← formulaAlgebraData.polynomialRing;
polyRingData: POL.PolynomialRingData ← NARROW[polynomialRing.instanceData];
ReadJunct: PROC ~ {
Skips preceding white space and read a junct. At exit, char is "terminating char", i.e. first nonblank char beyond junct (NUL if end of stream). char has been removed if = $, otherwise not.
[]← in.SkipWhitespace[];
char ← in.PeekChar[];
IF polynomialRing.class.legalFirstChar[char, polynomialRing] THEN -- unparenthesized atomic formula
[junct, char] ← ReadAtomicFormula[in, formulaAlgebra]
ELSE IF char='~ THEN {
char ← in.GetChar[]; -- remove tilde
[]← in.SkipWhitespace[];
char ← in.PeekChar[];
IF char='( THEN {
[] ← in.GetChar[]; -- remove left paren
[junct, char] ← ReadFormula[in, formulaAlgebra];
IF char#') THEN ERROR;
junct ← NEW[AC.ObjectRec ← [
structure: formulaAlgebra,
data: NEW[FormulaDataRec ← [
numFreeVars: polyRingData.allVariables.lengthPlus1 - 1,
atomicMatrix: FALSE,
mainOperator: FormulaOperators.FromRope["not", FormulaOperators.Operators],
operands: LIST[junct]
]]
]];
[] ← in.GetChar[]; -- remove right paren
[]← in.SkipWhitespace[];
IF in.EndOf[] THEN {char ← 000C; RETURN};
char ← in.PeekChar[];
IF char = '$ THEN [] ← in.GetChar[]; -- remove $
RETURN;
}
ELSE ERROR;
}
ELSE IF char='( THEN {
[] ← in.GetChar[]; -- move past left paren
[junct, char] ← ReadFormula[in, formulaAlgebra];
IF char#') THEN ERROR;
[] ← in.GetChar[]; -- remove right paren
[]← in.SkipWhitespace[];
IF in.EndOf[] THEN {char ← 000C; RETURN};
char ← in.PeekChar[];
IF char = '$ THEN [] ← in.GetChar[]; -- remove $
RETURN;
}
ELSE ERROR;
};
ReadJunct[]; formula ← junct;
IF in.EndOf[] THEN RETURN[formula, char];
IF char='| THEN {
list ← listTail ← LIST[junct];
WHILE char='| DO
[] ← in.GetChar[]; -- remove |
ReadJunct[];
listTail ← listTail.rest ← LIST[junct];
ENDLOOP;
formula ← NEW[AC.ObjectRec ← [
structure: formulaAlgebra,
data: NEW[FormulaDataRec ← [
numFreeVars: polyRingData.allVariables.lengthPlus1 - 1,
atomicMatrix: FALSE,
mainOperator: FormulaOperators.FromRope["or", FormulaOperators.Operators],
operands: list
]]
]];
};
IF char='& THEN {
list ← listTail ← LIST[junct];
WHILE char='& DO
[] ← in.GetChar[]; -- remove |
ReadJunct[];
listTail ← listTail.rest ← LIST[junct];
ENDLOOP;
formula ← NEW[AC.ObjectRec ← [
structure: formulaAlgebra,
data: NEW[FormulaDataRec ← [
numFreeVars: polyRingData.allVariables.lengthPlus1 - 1,
atomicMatrix: FALSE,
mainOperator: FormulaOperators.FromRope["and", FormulaOperators.Operators],
operands: list
]]
]];
};
RETURN[formula, char];
};
ReadAtomicFormula: PUBLIC PROC [in: IO.STREAM, formulaAlgebra: AC.Structure] RETURNS [formula: Formula, termChar: CHAR] ~ {
May be terminated by end of stream, or by &, |, ), or $. If by end of stream, then termChar ← NUL. If by $, then $ has been removed from in. If by any of the other chars, then not removed from in.
leftPoly, rightPoly, formulaPoly: POL.Polynomial;
leftDPoly, rightDPoly: DP.DPolynomial;
firstRelationChar: CHAR;
relation: Rope.ROPE;
polySign: Basics.Comparison;
formulaAlgebraData: FormulaAlgebraData ← NARROW[formulaAlgebra.instanceData];
polynomialRing: AC.Structure ← formulaAlgebraData.polynomialRing;
polyRingData: POL.PolynomialRingData ← NARROW[polynomialRing.instanceData];
V: VARS.VariableSeq ← polyRingData.allVariables;
RelationProc: DP.TermCharProc = {
SELECT char FROM
'<, '>, '=, '#,'~ => RETURN[TRUE];
ENDCASE => RETURN[FALSE];
};
EndAtomicFormulaProc: DP.TermCharProc = {
SELECT char FROM
'&, '|, '), '$ => RETURN[TRUE];
ENDCASE => RETURN[FALSE];
};
[leftDPoly, firstRelationChar] ← DP.ReadDPoly[in, V, polyRingData.baseCoeffRing, RelationProc];
IF in.EndOf[] OR firstRelationChar = '$ THEN ERROR; -- check that we saw a relation char
[] ← in.GetChar[]; -- remove firstRelationChar
leftPoly ← NARROW[POL.PolyFromDPoly[leftDPoly, polynomialRing]];
SELECT firstRelationChar FROM
'< => IF in.PeekChar[] = '= THEN {relation ← "le"; [] ← in.GetChar[] } ELSE relation ← "lt";
'> => IF in.PeekChar[] = '= THEN {relation ← "ge"; [] ← in.GetChar[] } ELSE relation ← "gt";
'~ => IF in.PeekChar[] = '= THEN {relation ← "ne"; [] ← in.GetChar[] } ELSE ERROR; -- no other valid meaning for ~ here
'= => relation ← "eq";
'# => relation ← "ne";
ENDCASE => ERROR; -- only cases possible
[rightDPoly, termChar] ← DP.ReadDPoly[in, V, polyRingData.baseCoeffRing, EndAtomicFormulaProc];
rightPoly ← NARROW[POL.PolyFromDPoly[rightDPoly, polynomialRing]];
formulaPoly ← NARROW[ polynomialRing.class.subtract[leftPoly, rightPoly] ];
IF polynomialRing.class.ordered THEN
polySign ← polynomialRing.class.sign[formulaPoly]
ELSE
polySign ← greater;
IF polySign = less THEN {
formulaPoly ← NARROW[ polynomialRing.class.negate[formulaPoly] ]; -- polynomial in atomic formula must be nonnegative
SELECT relation FROM
"lt" => relation ← "gt";
"le" => relation ← "ge";
"gt" => relation ← "lt";
"ge" => relation ← "le";
ENDCASE;
};
formula ← NEW[AC.ObjectRec ← [
structure: formulaAlgebra,
data: NEW[FormulaDataRec ← [
numFreeVars: polyRingData.allVariables.lengthPlus1 - 1,
atomicMatrix: TRUE,
mainOperator: FormulaOperators.FromRope[relation, FormulaOperators.Operators],
polynomial: formulaPoly
]]
]];
RETURN[formula, termChar];
};
FromRope: PUBLIC AC.FromRopeOp ~ {
stream: IO.STREAM ← IO.RIS[in];
termChar: CHAR;
[out, termChar ] ← ReadFormula[stream, structure];
};
ToRope: PUBLIC AC.ToRopeOp ~ {
formulaAlgebraData: FormulaAlgebraData ← NARROW[in.structure.instanceData];
polynomialRing: AC.Structure ← formulaAlgebraData.polynomialRing;
polyRingData: POL.PolynomialRingData ← NARROW[polynomialRing.instanceData];
V: VARS.VariableSeq ← polyRingData.allVariables;
coeffRing: AC.Structure ← polyRingData.baseCoeffRing;
inData: FormulaData ← NARROW[in.data];
IF inData.atomicMatrix THEN {
mainOperatorData: FormulaOperators.OperatorData ← NARROW[inData.mainOperator.data];
out ← Rope.Concat[ "( ", POL.PolyToRope[inData.polynomial, ""]];
SELECT mainOperatorData^ FROM
lt => out ← Rope.Concat[out, " < 0 )"];
le => out ← Rope.Concat[out, " <= 0 )"];
gt => out ← Rope.Concat[out, " > 0 )"];
ge => out ← Rope.Concat[out, " >= 0 )"];
eq => out ← Rope.Concat[out, " = 0 )"];
ne => out ← Rope.Concat[out, " # 0 )"];
ENDCASE;
RETURN[ Rope.Concat[out] ];
}
ELSE {
terms: LIST OF Formula ← inData.operands;
mainOperatorData: FormulaOperators.OperatorData ← NARROW[inData.mainOperator.data];
IF mainOperatorData^ # not THEN out ← "( " ELSE out ← "~ ( ";
WHILE terms#NIL DO
out ← Rope.Concat[out, ToRope[terms.first] ];
terms ← terms.rest;
IF terms#NIL THEN SELECT mainOperatorData^ FROM
and => out ← Rope.Concat[out, " & "];
or => out ← Rope.Concat[out, " | "];
ENDCASE => ERROR; -- shouldn't be in here when mainOperator = not
ENDLOOP;
out ← Rope.Cat[out, " )"];
};
};
Write: PUBLIC AC.WriteOp ~ {
formulaRope: Rope.ROPE ← ToRope[in];
stream.PutF["\n %g \n", IO.rope[formulaRope] ];
};
ToExpr: PUBLIC AC.ToExprOp ~ {
formulaAlgebraData: FormulaAlgebraData ← NARROW[in.structure.instanceData];
polynomialRing: AC.Structure ← formulaAlgebraData.polynomialRing;
polyRingData: POL.PolynomialRingData ← NARROW[polynomialRing.instanceData];
V: VARS.VariableSeq ← polyRingData.allVariables;
coeffRing: AC.Structure ← polyRingData.baseCoeffRing;
inData: FormulaData ← NARROW[in.data];
IF inData.atomicMatrix THEN {
polynomial: POL.Polynomial ← inData.polynomial;
mainOperatorData: FormulaOperators.OperatorData ← NARROW[inData.mainOperator.data];
SELECT mainOperatorData^ FROM
lt => RETURN[MathConstructors.MakeLtFormula[
POL.MakePolyExpr[polynomial], MathConstructors.MakeInt["0"] ] ];
le => RETURN[MathConstructors.MakeLeFormula[
POL.MakePolyExpr[polynomial], MathConstructors.MakeInt["0"] ] ];
gt => RETURN[MathConstructors.MakeGtFormula[
POL.MakePolyExpr[polynomial], MathConstructors.MakeInt["0"] ] ];
ge => RETURN[MathConstructors.MakeGeFormula[
POL.MakePolyExpr[polynomial], MathConstructors.MakeInt["0"] ] ];
eq => RETURN[MathConstructors.MakeEqFormula[
POL.MakePolyExpr[polynomial], MathConstructors.MakeInt["0"] ] ];
ne => RETURN[MathConstructors.MakeNotEqFormula[
POL.MakePolyExpr[polynomial], MathConstructors.MakeInt["0"] ] ];
ENDCASE;
}
ELSE {
terms: LIST OF Formula ← inData.operands;
firstTermExpr: MathExpr.EXPR ← ToExpr[terms.first];
mainOperatorData: FormulaOperators.OperatorData ← NARROW[inData.mainOperator.data];
IF mainOperatorData^ = not THEN
RETURN[MathConstructors.MakeNot[MathConstructors.MakeParen[firstTermExpr] ] ];
out ← MathConstructors.MakeParen[firstTermExpr];
terms ← terms.rest;
WHILE terms#NIL DO
SELECT mainOperatorData^ FROM
and => out ← MathConstructors.MakeAnd[out, MathConstructors.MakeParen[ToExpr[terms.first] ] ];
or => out ← MathConstructors.MakeOr[out, MathConstructors.MakeParen[ToExpr[terms.first] ] ];
ENDCASE => ERROR; -- shouldn't be in here when mainOperator = not
terms ← terms.rest;
ENDLOOP;
};
};
Arithmetic
Disjunct: PUBLIC AC.BinaryOp = {
data1: FormulaData ← NARROW[firstArg.data];
data2: FormulaData ← NARROW[secondArg.data];
RETURN[NEW[AC.ObjectRec ← [
structure: firstArg.structure,
data: NEW[FormulaDataRec ← [
numFreeVars: MAX[data1.numFreeVars, data2.numFreeVars],
atomicMatrix: FALSE,
mainOperator: FormulaOperators.FromRope["or", FormulaOperators.Operators],
operands: LIST[firstArg, secondArg]
]]
]]
];
};
Conjunct: PUBLIC AC.BinaryOp = {
data1: FormulaData ← NARROW[firstArg.data];
data2: FormulaData ← NARROW[secondArg.data];
RETURN[NEW[AC.ObjectRec ← [
structure: firstArg.structure,
data: NEW[FormulaDataRec ← [
numFreeVars: MAX[data1.numFreeVars, data2.numFreeVars],
atomicMatrix: FALSE,
mainOperator: FormulaOperators.FromRope["and", FormulaOperators.Operators],
operands: LIST[firstArg, secondArg]
]]
]]
];
};
Negate: PUBLIC AC.UnaryOp = {
data: FormulaData ← NARROW[arg.data];
RETURN[NEW[AC.ObjectRec ← [
structure: arg.structure,
data: NEW[FormulaDataRec ← [
numFreeVars: data.numFreeVars,
atomicMatrix: FALSE,
mainOperator: FormulaOperators.FromRope["not", FormulaOperators.Operators],
operands: LIST[arg]
]]
]]
];
};
Difference: PUBLIC AC.BinaryOp = {
RETURN[ Conjunct[firstArg, Negate[secondArg] ] ];
};
AllVarEv: PUBLIC AC.BinaryOp ~ {
data: FormulaAlgebraData ← NARROW[firstArg.structure.instanceData];
polynomialRing: AC.Structure ← data.polynomialRing;
polyRingData: POL.PolynomialRingData ← NARROW[polynomialRing.instanceData];
baseCoeffRing: AC.Structure ← polyRingData.baseCoeffRing;
inData: FormulaData ← NARROW[firstArg.data];
IF NOT baseCoeffRing.class.ordered THEN TypeError[$OrderedStructureNeeded];
IF inData.atomicMatrix THEN {
sign: Basics.Comparison ← baseCoeffRing.class.sign[POL.AllVarEv[inData.polynomial, secondArg] ];
mainOperatorData: FormulaOperators.OperatorData ← NARROW[inData.mainOperator.data];
SELECT mainOperatorData^ FROM
lt => RETURN[IF sign = less THEN Bools.FromBOOL[TRUE] ELSE Bools.FromBOOL[FALSE]];
le => RETURN[IF sign = less OR sign = equal THEN Bools.FromBOOL[TRUE] ELSE Bools.FromBOOL[FALSE] ];
gt => RETURN[IF sign = greater THEN Bools.FromBOOL[TRUE] ELSE Bools.FromBOOL[FALSE]];
ge => RETURN[IF sign = greater OR sign = equal THEN Bools.FromBOOL[TRUE] ELSE Bools.FromBOOL[FALSE] ];
eq => RETURN[IF sign = equal THEN Bools.FromBOOL[TRUE] ELSE Bools.FromBOOL[FALSE] ];
ne => RETURN[IF sign = less OR sign = greater THEN Bools.FromBOOL[TRUE] ELSE Bools.FromBOOL[FALSE] ];
ENDCASE;
}
ELSE {
terms: LIST OF Formula ← inData.operands;
bool: Bools.Bool ← AllVarEv[terms.first, secondArg];
mainOperatorData: FormulaOperators.OperatorData ← NARROW[inData.mainOperator.data];
IF mainOperatorData^ = not THEN
RETURN[Bools.Negate[bool] ];
terms ← terms.rest;
WHILE terms#NIL DO
SELECT mainOperatorData^ FROM
and => {
IF NOT NARROW[bool.data, Bools.BoolData]^ THEN RETURN[Bools.FromBOOL[FALSE]];
bool ← Bools.Conjunct[bool, AllVarEv[terms.first, secondArg] ];
};
or => {
IF NARROW[bool.data, Bools.BoolData]^ THEN RETURN[Bools.FromBOOL[TRUE]];
bool ← Bools.Disjunct[bool, AllVarEv[terms.first, secondArg] ];
};
ENDCASE => ERROR; -- shouldn't be in here when mainOperator = not
terms ← terms.rest;
ENDLOOP;
RETURN[bool];
};
RETURN[Bools.FromBOOL[TRUE]]; -- satisfy compiler
};
END.