[Indigo]<AlgebraStructures>MathExprClassesLogical.mesa!4

MathExprClassesLogical.mesa

Carl Waldspurger, August 30, 1986 7:12:37 pm PDT

Bier, November 20, 1986 2:02:38 pm PST

Arnon, March 24, 1987 4:15:37 pm PST

Mcisaac, July 9, 1987 7:02:32 pm PDT

DIRECTORY

MathExpr,

MathRules,

MathDB,

MathTypes,

MathBox,

Imager,

Rope,

Vector,

MathConstructors;

MathExprClassesLogical: CEDAR PROGRAM

IMPORTS MathBox, MathRules, MathExpr,

MathDB, MathConstructors

BEGIN

Type Abbreviations from Imported Interfaces

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;

Procedure Abbreviations from Imported Interfaces

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;

Constants

smallGap: REAL = 0.05;

medGap: REAL = 0.10;

bigGap: REAL = 0.25;

Box Procs for Compound Expr Classes

FixedSizeBoxRule: CompoundBoxProc ~ {

effects: Returns unaltered boxes (i.e. no resizing takes place)

RETURN[boxes];

};

Composition Procs for Compound Expr Classes

UnaryOpCompRule: CompositionProc ~ {

effects: Composes layout for expr of form ($aliasUnaryOp $aliasA).

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 ~ {

effects: Composes layout for expr of form ($aliasBinOp $aliasA $aliasB) with

symbols $aliasLeftSpace & $aliasRightSpace.

tempBox: BOX;

tempBoxes: LIST OF BOX;

leftVertOffsetA, leftVertOffsetOp, rightVertOffsetB, rightVertOffsetOp: Offset;

alignments: LIST OF Alignment2D;

set vertical offset depending on format classes of A & B arguments

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 ~ {

effects: Composes layout for expr of form ($aliasRelation $aliasLHS $aliasRHS) with

symbols $aliasLeftSpace & $aliasRightSpace.

tempBox: BOX;

tempBoxes: LIST OF BOX;

leftVertOffsetLHS, leftVertOffsetRel, rightVertOffsetRHS, rightVertOffsetRel: Offset;

alignments: LIST OF Alignment2D;

set vertical offset depending on format classes of lhs & rhs arguments

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];

};

Class Constructors

MakeUnaryOpClass: PUBLIC PROC[class, op, arg: ATOM, operation: EXPR, description: ROPE, cvtAS, cvtReduce, cvtSMP, cvtOther: ROPE ← NIL] RETURNS[CompoundClass] ~ {

effects: Creates and returns standard unary operation compound class named "class".

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] ~ {

effects: Creates and returns standard binary operation compound class named "class".

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] ~ {

effects: Creates and returns standard relation compound class named "class".

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]];

};

Signals & Errors

wrongBoxType: PUBLIC ERROR = CODE;

Define & Install Expression Classes

InstallLogicalClassesA: PROC [] ~ {

local declarations

differenceClass: CompoundClass;

binary operations

differenceClass ← MakeBinOpClass[$difference, $minus, $subtrahend, $minuend, MathConstructors.MakePlainSym['-], "a - b", "$subtrahend - $minuend"];

Register compound classes in user-friendly order

MathDB.InstallCompoundClass[differenceClass];

MathDB.AddOperator[differenceClass, $Logical]; -- difference op goes in three classes

};

InstallLogicalClassesAA: PROC [] ~ {

local declarations

orClass, notClass, andClass, existsClass, forAllClass: CompoundClass;

define compound classes

binary operations

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"];

unary operations

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 [] ~ {

local declarations

eqFormulaClass, notEqFormulaClass, ltFormulaClass, leFormulaClass, geFormulaClass, gtFormulaClass, approachesClass, impliesClass, equivClass: CompoundClass;

relations

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.MakeOverlaySym["=/"], "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.MakeBigMathSym['\024], "a <= b", "$lhs <= $rhs"];

geFormulaClass ← MakeRelationClass[$geFormula, $ge, $lhs, $rhs, MathConstructors.MakeSmallMathSym['\025], "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];

};

Install Classes Defined in this Module

InstallLogicalClassesA[];

InstallLogicalClassesAA[];

InstallLogicalClassesB[];

END.