<> <> <<>> <> <<>> DIRECTORY Rope, IO, AlgebraClasses, ASAtomicFormulaOps, Variables, Polynomials; ASFormulaStructure: CEDAR DEFINITIONS = BEGIN <> Formula: TYPE = AlgebraClasses.Object; <<>> Quantifier: TYPE = {exists, forAll}; PropositionalConnective: TYPE = {and, or, xOr, difference, implies, equivalent}; <<>> FormulaData: TYPE = REF FormulaDataRec; FormulaDataRec: TYPE ~ RECORD [ SELECT type:* FROM atomic => [ rel: ASAtomicFormulaOps.Operator, -- relation polynomial: Polynomials.Polynomial -- standard form assumed, i.e. polynomial rel 0. ], negation => [ arg: Formula ], compound => [ op: PropositionalConnective, args: LIST OF Formula -- two or more, obviously; assumed to all have same free variables ], quantified => [ quantifiers: LIST OF Quantifier, -- a sequence of m >= 1 Quantifiers matrix: Formula -- it is assumed that matrix has at least m free variables, and that the quantifiers bind the "upper" ("rightmost") m of them. ] ENDCASE ]; <> <> FormulaAlgebraData: TYPE = REF FormulaAlgebraDataRec; FormulaAlgebraDataRec: TYPE = RECORD [ polynomialRing: AlgebraClasses.Object -- the Structure for the polynomials occurring in the atomic formulas of this FormulaStructure. ]; <> MakeFormulaAlgebra: PROC [polynomialRing: AlgebraClasses.Object] RETURNS [formulaAlgebra: AlgebraClasses.Object]; <> <> <> PrintName: AlgebraClasses.ToRopeOp; ShortPrintName: AlgebraClasses.ToRopeOp; IsFormulaAlgebra: AlgebraClasses.UnaryPredicate; PolynomialRing: AlgebraClasses.UnaryOp; <> <<>> <> Quantify: PROC [quantifiers: LIST OF Quantifier, in: Formula] RETURNS [out: Formula]; <> <<>> QuantifyChecked: PROC [quantifiers: LIST OF Quantifier, variables: LIST OF Variables.Variable, in: Formula] RETURNS [out: Formula]; <> <> Recast: AlgebraClasses.BinaryOp; CanRecast: AlgebraClasses.BinaryPredicate; ToExpr: AlgebraClasses.ToExprOp; LegalFirstChar: AlgebraClasses.LegalFirstCharOp; Read: AlgebraClasses.ReadOp; FromRope: AlgebraClasses.FromRopeOp; <<>> ToRope: AlgebraClasses.ToRopeOp; Write: AlgebraClasses.WriteOp; <> FreeVariables: AlgebraClasses.UnaryToListOp; <> Negate: AlgebraClasses.UnaryOp; And: AlgebraClasses.NaryOp; <> Or: AlgebraClasses.NaryOp; XOr: AlgebraClasses.BinaryOp; Difference: AlgebraClasses.BinaryOp; Implies: AlgebraClasses.BinaryOp; Equiv: AlgebraClasses.BinaryOp; AllVarEval: AlgebraClasses.BinaryOp; <> <> <> <> <> <> <> <> <B AND B=>A].>> <> Eval: AlgebraClasses.BinaryOp; <> <> <> <> END.