<> <> DIRECTORY Rope, IO, MathExpr, AlgebraClasses, Bools, FormulaOperators, Points, Variables, DistribPolys, Polynomials; Formulas: CEDAR DEFINITIONS = BEGIN OPEN AC: AlgebraClasses, VARS: Variables, DP: DistribPolys, POL: Polynomials; <> <> <<>> Formula: TYPE = AC.Object; FormulaData: TYPE = REF FormulaDataRec; FormulaDataRec: TYPE = RECORD [ numFreeVars: CARDINAL, quantifiers: QuantifierSeq _ NIL, -- Assert length(quantifiers) = numTotalVars - numFreeVars = r - k. It is assumed that the lowest k variables are free, and the highest r - k are quantified. atomicMatrix: BOOL _ FALSE, mainOperator: FormulaOperators.Operator, -- (and, or, or not if not atomicMatrix; otherwise a Relation) operands: LIST OF Formula _ NIL, -- nonNIL iff not atomicMatrix; then each assumed to have r free variables, of which last (r - k) will be governed by the above quantifiers. polynomial: POL.Polynomial _ NIL -- nonNIL iff atomicMatrix ]; QuantifierSeq: TYPE = REF QuantifierSeqRec; QuantifierSeqRec: TYPE = RECORD [SEQUENCE lengthPlus1: [1..100] OF Quantifier]; Quantifier: TYPE = {Exists, ForAll}; <> formulaClass: AC.StructureClass; <> FormulaAlgebraData: TYPE = REF FormulaAlgebraDataRec; FormulaAlgebraDataRec: TYPE = RECORD [ polynomialRing: AC.Structure -- contains the polynomials occurring in matrices of formulas of this FormulaAlgebra. ]; <> FormulaAllVarEvalOp: TYPE = PROC [in: Formula, point: Points.Point] RETURNS [Bools.Bool]; <> <<>> FormulaOps: TYPE = REF FormulaOpsRec; -- prop key is $FormulaRing. FormulaOpsRec: TYPE = RECORD [ allVarEval: FormulaAllVarEvalOp ]; <> MakeFormulaAlgebra: PROC [polynomialRing: AC.Structure] RETURNS [formulaAlgebra: AC.Structure]; <> IsFormulaAlgebra: PROC [structure: AC.Structure] RETURNS [BOOL]; AllVarEval: PROC [formulaAlgebra: AC.Structure] RETURNS [FormulaAllVarEvalOp]; <> Quantify: PROC [quantifier: Quantifier, in: Formula] RETURNS [out: Formula]; <> <<>> ReadFormula: PROC [in: IO.STREAM, formulaAlgebra: AC.Structure] RETURNS [formula: Formula, termChar: CHAR]; ReadAtomicFormula: PROC [in: IO.STREAM, formulaAlgebra: AC.Structure] RETURNS [formula: Formula, termChar: CHAR]; FormulaFromRope: PROC [in: Rope.ROPE, formulaAlgebra: AC.Structure] RETURNS [out: Formula]; <<>> FormulaToRope: PROC [in: Formula, termRope: Rope.ROPE _ NIL] RETURNS [out: Rope.ROPE]; <> <<>> MakeFormulaExpr: PROC [in: Formula] RETURNS [out: MathExpr.EXPR]; WriteFormula: PROC [in: Formula, out: IO.STREAM]; <> Disjunct: PROC [in1, in2: Formula] RETURNS [out: Formula]; Conjunct: PROC [in1, in2: Formula] RETURNS [out: Formula]; Negate: PROC [in: Formula] RETURNS [out: Formula]; Difference: PROC [in1, in2: Formula] RETURNS [Formula]; AllVarEv: FormulaAllVarEvalOp; END.