<> <> <> <> <> DIRECTORY MathExpr, MathRules, MathDB, MathTypes, MathBox, Imager, Rope, Vector, MathConstructors; MathExprClassesLogical: CEDAR PROGRAM IMPORTS MathBox, MathRules, MathExpr, MathDB, MathConstructors ~ BEGIN <> EXPR: TYPE ~ MathExpr.EXPR; BOX: TYPE ~ MathBox.BOX; ROPE: TYPE ~ Rope.ROPE; VEC: TYPE ~ Vector.VEC; CompoundBoxProc: TYPE ~ MathRules.CompoundBoxProc; CompositionProc: TYPE ~ MathRules.CompositionProc; Alignment2D: TYPE ~ MathRules.Alignment2D; Offset: TYPE ~ MathRules.Offset; Size: TYPE ~ MathRules.Size; Argument: TYPE ~ MathExpr.Argument; Symbol: TYPE ~ MathExpr.Symbol; CompoundClass: TYPE ~ MathExpr.CompoundClass; FormatClass: TYPE ~ MathTypes.FormatClass; Style: TYPE ~ MathTypes.Style; <> MakeArgument: PROC[name: ATOM, aliases: LIST OF ATOM, size: Size] RETURNS[Argument] ~ MathExpr.MakeArgument; MakeSymbol: PROC[name: ATOM, aliases: LIST OF ATOM, size: Size, value: EXPR] RETURNS[Symbol] ~ MathExpr.MakeSymbol; MakeCompoundClass: PROC[name: ATOM, formatClass: FormatClass, description: ROPE, args: LIST OF Argument, syms: LIST OF Symbol, boxRule: CompoundBoxProc, compBox: CompositionProc, cvtAS, cvtReduce, cvtSMP, cvtOther: ROPE _ NIL] RETURNS[CompoundClass] ~ MathExpr.MakeCompoundClass; <> smallGap: REAL = 0.05; medGap: REAL = 0.10; bigGap: REAL = 0.25; <> FixedSizeBoxRule: CompoundBoxProc ~ { <> RETURN[boxes]; }; <> UnaryOpCompRule: CompositionProc ~ { <> tempBox: BOX; tempBoxes: LIST OF BOX; alignments: LIST OF Alignment2D _ LIST[ [$aliasSpace, [$aliasUnaryOp, [left], [right]], [$aliasUnaryOp, [origin], [origin]]], [$aliasA, [$aliasSpace, [left], [right]], [$aliasSpace, [origin], [origin]]]]; [tempBox, tempBoxes] _ MathRules.Compose[boxes, alignments, [$aliasUnaryOp, [origin]], [$aliasUnaryOp, [origin]]]; RETURN[tempBox, tempBoxes]; }; BinaryOpCompRule: CompositionProc ~ { <> << symbols $aliasLeftSpace & $aliasRightSpace.>> <<>> tempBox: BOX; tempBoxes: LIST OF BOX; leftVertOffsetA, leftVertOffsetOp, rightVertOffsetB, rightVertOffsetOp: Offset; alignments: LIST OF Alignment2D; <> SELECT MathBox.GetBox[$aliasA, boxes].FormatClass[] FROM over => { leftVertOffsetA _ [origin]; leftVertOffsetOp _ [center]; }; matrix => { leftVertOffsetA _ [center]; leftVertOffsetOp _ [center]; }; ENDCASE => { leftVertOffsetA _ [origin]; leftVertOffsetOp _ [origin]; }; SELECT MathBox.GetBox[$aliasB, boxes].FormatClass[] FROM over => { rightVertOffsetB _ [origin]; rightVertOffsetOp _ [center]; }; matrix => { rightVertOffsetB _ [center]; rightVertOffsetOp _ [center]; }; ENDCASE => { rightVertOffsetB _ [origin]; rightVertOffsetOp _ [origin]; }; alignments _ LIST[ [$aliasLeftSpace, [$aliasBinOp, [right], [left]], [$aliasBinOp, [origin], [origin]]], [$aliasA, [$aliasLeftSpace, [right], [left]], [$aliasBinOp, leftVertOffsetA, leftVertOffsetOp]], [$aliasRightSpace, [$aliasBinOp, [left], [right]], [$aliasBinOp, [origin], [origin]]], [$aliasB, [$aliasRightSpace, [left], [right]], [$aliasBinOp, rightVertOffsetB, rightVertOffsetOp]]]; [tempBox, tempBoxes] _ MathRules.Compose[boxes, alignments, [$aliasA, [origin]], [$aliasBinOp, [origin]]]; RETURN[tempBox, tempBoxes]; }; RelationCompRule: CompositionProc ~ { <> << symbols $aliasLeftSpace & $aliasRightSpace.>> <<>> tempBox: BOX; tempBoxes: LIST OF BOX; leftVertOffsetLHS, leftVertOffsetRel, rightVertOffsetRHS, rightVertOffsetRel: Offset; alignments: LIST OF Alignment2D; <> SELECT MathBox.GetBox[$aliasLHS, boxes].FormatClass[] FROM over => { leftVertOffsetLHS _ [origin]; leftVertOffsetRel _ [center]; }; matrix => { leftVertOffsetLHS _ [center]; leftVertOffsetRel _ [center]; }; ENDCASE => { leftVertOffsetLHS _ [origin]; leftVertOffsetRel _ [origin]; }; SELECT MathBox.GetBox[$aliasRHS, boxes].FormatClass[] FROM over => { rightVertOffsetRHS _ [origin]; rightVertOffsetRel _ [center]; }; matrix => { rightVertOffsetRHS _ [center]; rightVertOffsetRel _ [center]; }; ENDCASE => { rightVertOffsetRHS _ [origin]; rightVertOffsetRel _ [origin]; }; alignments _ LIST[ [$aliasLeftSpace, [$aliasRelation, [right], [left]], [$aliasRelation, [origin], [origin]]], [$aliasLHS, [$aliasLeftSpace, [right], [left]], [$aliasRelation, leftVertOffsetLHS, leftVertOffsetRel]], [$aliasRightSpace, [$aliasRelation, [left], [right]], [$aliasRelation, [origin], [origin]]], [$aliasRHS, [$aliasRightSpace, [left], [right]], [$aliasRelation, rightVertOffsetRHS, rightVertOffsetRel]]]; [tempBox, tempBoxes] _ MathRules.Compose[boxes, alignments, [$aliasLHS, [origin]], [$aliasRelation, [origin]]]; RETURN[tempBox, tempBoxes]; }; <> MakeUnaryOpClass: PUBLIC PROC[class, op, arg: ATOM, operation: EXPR, description: ROPE, cvtAS, cvtReduce, cvtSMP, cvtOther: ROPE _ NIL] RETURNS[CompoundClass] ~ { <> << The alignment is "operation arg"; alignment is thru baselines. >> << Both op, arg are of fixed size "normal".>> <<>> argArg: Argument _ MakeArgument[arg, LIST[$aliasA, $aliasHot], normal]; spaceSym: Symbol _ MakeSymbol[$Space, LIST[$aliasSpace], normal, MathConstructors.MakeSpace[$medium]]; unaryOpSym: Symbol _ MakeSymbol[op, LIST[$aliasUnaryOp], normal, operation]; RETURN[MakeCompoundClass[class, unaryOp, description, LIST[argArg], LIST[unaryOpSym, spaceSym], FixedSizeBoxRule, UnaryOpCompRule, cvtAS, cvtReduce, cvtSMP, cvtOther]]; }; MakeBinOpClass: PUBLIC PROC[class, op, a, b: ATOM, operation: EXPR, description: ROPE, cvtAS, cvtReduce, cvtSMP, cvtOther: ROPE _ NIL] RETURNS[CompoundClass] ~ { <> << The alignment is "a operation b"; alignment is thru baselines. >> << All of a, b, op are of fixed size "normal".>> aArg: Argument _ MakeArgument[a, LIST[$aliasA, $aliasHot], normal]; bArg: Argument _ MakeArgument[b, LIST[$aliasB], normal]; opSym: Symbol _ MakeSymbol[op, LIST[$aliasBinOp], normal, operation]; leftSpace: Symbol _ MakeSymbol[$leftThinSpace, LIST[$aliasLeftSpace], normal, MathConstructors.MakeSpace[$thin]]; rightSpace: Symbol _ MakeSymbol[$rightThinSpace, LIST[$aliasRightSpace], normal, MathConstructors.MakeSpace[$thin]]; RETURN[MakeCompoundClass[class, binaryOp, description, LIST[aArg, bArg], LIST[opSym, leftSpace, rightSpace], FixedSizeBoxRule, BinaryOpCompRule, cvtAS, cvtReduce, cvtSMP, cvtOther]]; }; MakeRelationClass: PUBLIC PROC[class, rel, lhs, rhs: ATOM, relation: EXPR, description: ROPE, cvtAS, cvtReduce, cvtSMP, cvtOther: ROPE _ NIL] RETURNS[CompoundClass] ~ { <> << The alignment is "lhs relation rhs"; alignment is thru baselines. >> << All of lhs, rhs, rel are of fixed size "normal".>> lhsArg: Argument _ MakeArgument[lhs, LIST[$aliasLHS, $aliasHot], normal]; rhsArg: Argument _ MakeArgument[rhs, LIST[$aliasRHS], normal]; relSym: Symbol _ MakeSymbol[rel, LIST[$aliasRelation], normal, relation]; leftSpace: Symbol _ MakeSymbol[$leftSpace, LIST[$aliasLeftSpace], normal, MathConstructors.MakeSpace[$thick]]; rightSpace: Symbol _ MakeSymbol[$rightSpace, LIST[$aliasRightSpace], normal, MathConstructors.MakeSpace[$thick]]; RETURN[MakeCompoundClass[class, relation, description, LIST[lhsArg, rhsArg], LIST[relSym, leftSpace, rightSpace], FixedSizeBoxRule, RelationCompRule, cvtAS, cvtReduce, cvtSMP, cvtOther]]; }; <> wrongBoxType: PUBLIC ERROR = CODE; <> InstallLogicalClassesA: PROC [] ~ { <> differenceClass: CompoundClass; <> differenceClass _ MakeBinOpClass[$difference, $minus, $subtrahend, $minuend, MathConstructors.MakePlainSym['-], "a - b", "$subtrahend - $minuend"]; <> <<>> MathDB.InstallCompoundClass[differenceClass]; MathDB.AddOperator[differenceClass, $Logical]; -- difference op goes in three classes }; InstallLogicalClassesAA: PROC [] ~ { <> orClass, notClass, andClass, existsClass, forAllClass: CompoundClass; <> <<>> <> andClass _ MakeBinOpClass[$and, $andOp, $a, $b, MathConstructors.MakeBigMathSym['\266], "a AND b", "$a & $b"]; orClass _ MakeBinOpClass[$or, $orOp, $a, $b, MathConstructors.MakeBigMathSym['\267], "a OR b", "$a | $b"]; <> notClass _ MakeUnaryOpClass[$not, $notOp, $a, MathConstructors.MakeBigMathSym['\152], "~a", "~ $a"]; existsClass _ MakeUnaryOpClass[$exists, $existsOp, $a, MathConstructors.MakeBigMathSym['\264], "exists a", "E $a"]; forAllClass _ MakeUnaryOpClass[$forAll, $forAllOp, $a, MathConstructors.MakeBigMathSym['\265], "forAll a", "A $a"]; MathDB.InstallCompoundClass[existsClass]; MathDB.AddOperator[existsClass, $Logical]; MathDB.InstallCompoundClass[forAllClass]; MathDB.AddOperator[forAllClass, $Logical]; MathDB.InstallCompoundClass[andClass]; MathDB.AddOperator[andClass, $Logical]; MathDB.InstallCompoundClass[orClass]; MathDB.AddOperator[orClass, $Logical]; MathDB.InstallCompoundClass[notClass]; MathDB.AddOperator[notClass, $Logical]; }; InstallLogicalClassesB: PROC [] ~ { <> eqFormulaClass, notEqFormulaClass, ltFormulaClass, leFormulaClass, geFormulaClass, gtFormulaClass, approachesClass, impliesClass, equivClass: CompoundClass; <> eqFormulaClass _ MakeRelationClass[$eqFormula, $equals, $lhs, $rhs, MathConstructors.MakePlainSym['=], "a = b", "$lhs = $rhs", "equal($lhs, $rhs)", "Eq[$lhs, $rhs]"]; notEqFormulaClass _ MakeRelationClass[$notEqFormula, $equals, $lhs, $rhs, MathConstructors.MakeXCSym['\140,'\041], "a # b", "$lhs # $rhs"]; ltFormulaClass _ MakeRelationClass[$ltFormula, $lt, $lhs, $rhs, MathConstructors.MakePlainSym['<], "a < b", "$lhs < $rhs"]; gtFormulaClass _ MakeRelationClass[$gtFormula, $gt, $lhs, $rhs, MathConstructors.MakePlainSym['>], "a > b", "$lhs > $rhs"]; leFormulaClass _ MakeRelationClass[$leFormula, $le, $lhs, $rhs, MathConstructors.MakeXCSym['\145,'\041], "a <= b", "$lhs <= $rhs"]; geFormulaClass _ MakeRelationClass[$geFormula, $ge, $lhs, $rhs, MathConstructors.MakeXCSym['\146,'\041], "a >= b", "$lhs >= $rhs"]; approachesClass _ MakeRelationClass[$approachesFormula, $approaches, $lhs, $rhs, MathConstructors.MakePlainSym['\256], "a -> b", "$lhs -> $rhs", "Rep($lhs, $rhs)", "Rep[$lhs, $rhs]"]; impliesClass _ MakeRelationClass[$impliesFormula, $implies, $lhs, $rhs, MathConstructors.MakeBigMathSym['\117], "a => b", "$lhs => $rhs"]; equivClass _ MakeRelationClass[$equivFormula, $equiv, $lhs, $rhs, MathConstructors.MakeBigMathSym['\116], "a equiv b", "$lhs equiv $rhs"]; <<>> MathDB.InstallCompoundClass[eqFormulaClass]; MathDB.AddOperator[eqFormulaClass, $Logical]; MathDB.InstallCompoundClass[notEqFormulaClass]; MathDB.AddOperator[notEqFormulaClass, $Logical]; MathDB.InstallCompoundClass[ltFormulaClass]; MathDB.AddOperator[ltFormulaClass, $Logical]; MathDB.InstallCompoundClass[leFormulaClass]; MathDB.AddOperator[leFormulaClass, $Logical]; MathDB.InstallCompoundClass[gtFormulaClass]; MathDB.AddOperator[gtFormulaClass, $Logical]; MathDB.InstallCompoundClass[geFormulaClass]; MathDB.AddOperator[geFormulaClass, $Logical]; MathDB.InstallCompoundClass[approachesClass]; MathDB.AddOperator[approachesClass, $Logical]; MathDB.InstallCompoundClass[impliesClass]; MathDB.AddOperator[impliesClass, $Logical]; MathDB.InstallCompoundClass[equivClass]; MathDB.AddOperator[equivClass, $Logical]; }; <> InstallLogicalClassesA[]; InstallLogicalClassesAA[]; InstallLogicalClassesB[]; END.