You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
73 lines
1.6 KiB
73 lines
1.6 KiB
module gcdt2[Operand]
|
|
|
|
-- Operations over the operands:
|
|
abstract sig Operation {
|
|
fn: Operand one->one (Operand one->one Operand)
|
|
}
|
|
|
|
sig Commutative, PseudoCommutative extends Operation {}
|
|
|
|
fact { Operation = Commutative + PseudoCommutative }
|
|
|
|
|
|
sig GCDT {
|
|
universe: set Operand,
|
|
operations: set Operation
|
|
}
|
|
|
|
|
|
sig Frame {
|
|
op: one Operation,
|
|
right: one Operand
|
|
}
|
|
|
|
|
|
sig Reducer {
|
|
base: Operand,
|
|
fold: Operand one->one Operand
|
|
}
|
|
|
|
fun baseReducer [val: Operand]: Reducer {
|
|
{ r: Reducer | r.base = val && r.fold = iden }
|
|
}
|
|
|
|
pred typeFrame[type: GCDT, frame: Frame] {
|
|
frame.op in type.operations
|
|
frame.right in type.universe
|
|
}
|
|
|
|
pred typeReducer[type: GCDT, reducer: Reducer] {
|
|
reducer.base in type.universe
|
|
}
|
|
|
|
pred applyFrame [type: GCDT, frame: Frame, reducer: Reducer, result: Operand] {
|
|
typeFrame[type, frame]
|
|
typeReducer[type, reducer]
|
|
result in type.universe
|
|
result = reducer.fold[frame.op.fn[reducer.base][frame.right]]
|
|
}
|
|
|
|
fun wrapFold [frame: Frame, fold: Operand one->one Operand]: Operand one->one Operand {
|
|
{lhs, rhs : Operand |
|
|
rhs = fold[frame.op.fn[lhs][frame.right]]
|
|
}
|
|
}
|
|
|
|
pred applyFold [type: GCDT, frame: Frame, reducer, result: Reducer] {
|
|
typeFrame[type, frame]
|
|
typeReducer[type, reducer]
|
|
typeReducer[type, result]
|
|
(frame.op in PseudoCommutative) => result.fold = wrapFold[frame, reducer.fold]
|
|
else (frame.op in Commutative) => result.fold = reducer.fold
|
|
}
|
|
|
|
fun reduceOnce[type: GCDT, frame: Frame, reducer: Reducer]: Reducer {
|
|
{ result: Reducer |
|
|
typeReducer[type, result]
|
|
&& applyFrame[type, frame, reducer, result.base]
|
|
&& applyFold[type, frame, reducer, result]
|
|
&& typeFrame[type, frame]
|
|
&& typeReducer[type, reducer]
|
|
}
|
|
}
|