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.
156 lines
4.5 KiB
156 lines
4.5 KiB
module gcdt[Operand]
|
|
|
|
-- Top-level GCDT signature:
|
|
sig GCDT {
|
|
-- A domain of operands
|
|
operand: Operand,
|
|
|
|
-- A universe of possible operations
|
|
ops: set Operation,
|
|
|
|
-- Sub-universe of commutative ops:
|
|
cOps: CommutativeOp & ops,
|
|
|
|
-- Sub-universe of pseudo-commutative ops:
|
|
pcOps: PseudoCommutativeOp & ops
|
|
} {
|
|
ops = cOps + pcOps
|
|
}
|
|
|
|
|
|
|
|
-- All operations over GCDT's are binary:
|
|
abstract sig Operation {
|
|
op: Operand one->one (Operand one->one Operand)
|
|
}
|
|
|
|
-- All operations should reflexively commute:
|
|
fact commutes {
|
|
all opr: Operation | all opd1, opd2: Operand |
|
|
opr.op[opd1][opd2] = opr.op[opd2][opd1]
|
|
}
|
|
|
|
|
|
|
|
-- Commutative operations:
|
|
sig CommutativeOp extends Operation {}
|
|
|
|
-- Commutative operations distribute trivially:
|
|
fact distributes {
|
|
all cop1, cop2: CommutativeOp | all op1, op2, op3: Operand |
|
|
cop1.op[cop2.op[op1][op2], op3] = cop1.op[op1, cop2.op[op2][op3]]
|
|
}
|
|
|
|
|
|
|
|
-- Pseudo-commutative operations:
|
|
sig PseudoCommutativeOp extends Operation {
|
|
right: Operand
|
|
}
|
|
|
|
-- Pseudo-commutative operations fold into subsequent operands:
|
|
fact pseudoCommutes {
|
|
all cop1, cop2: CommutativeOp | all pop: PseudoCommutativeOp |
|
|
all opd1, opd2, opd3, opd4: Operand |
|
|
pop.op[cop1.op[cop2.op[opd1, opd2], opd3], opd4] =
|
|
cop1.op[cop2.op[pop.op[opd1, opd4], pop.op[opd2, opd4]], pop.op[opd3, opd4]]
|
|
}
|
|
|
|
|
|
|
|
-- A single operation applied to a GCDT:
|
|
sig GCDTDiff {
|
|
op: one Operation,
|
|
right: one Operand
|
|
}
|
|
|
|
|
|
-- An order-agnostic set of operations applied to a GCDT:
|
|
sig GCDTBatch {
|
|
type: one GCDT,
|
|
base: one Operand,
|
|
ops: set GCDTDiff,
|
|
fold: Operand one->one Operand
|
|
} {
|
|
base in type.operand
|
|
ops = {diff: ops | diff.op in type.ops && diff.right in type.operand}
|
|
}
|
|
|
|
|
|
fun applyDiff [diff: GCDTDiff, opd: Operand]: Operand {
|
|
diff.op.op[opd][diff.right]
|
|
}
|
|
|
|
run applyDiff for 4
|
|
|
|
fun composeFold [opr: one Operation, right: one Operand, fold: Operand one->one Operand]: Operand one->one Operand {
|
|
{lhs, rhs: Operand | rhs = fold[opr.op[lhs][right]] }
|
|
}
|
|
|
|
pred batchStep [batch1, batch2: GCDTBatch, diff: one GCDTDiff] {
|
|
diff in batch1.ops
|
|
batch1.type = batch2.type
|
|
batch2.base = diff.op.op[batch1.fold[batch1.base]][batch1.fold[diff.right]]
|
|
(diff.op in batch1.type.pcOps) => batch2.fold = composeFold[diff.op, diff.right, batch1.fold]
|
|
else batch2.fold = batch1.fold
|
|
batch2.ops = batch1.ops - diff
|
|
}
|
|
|
|
run batchStep for 4
|
|
|
|
fun batchSteps [] : GCDTBatch one->one GCDTBatch {
|
|
{ batch1, batch2 : GCDTBatch | some diff: GCDTDiff | batchStep[batch1, batch2, diff] }
|
|
}
|
|
|
|
run batchSteps for 4
|
|
|
|
/*batchCommutes2: check {
|
|
some dt: GCDT | all cop1, cop2: CommutativeOp | all pop: PseudoCommutativeOp |
|
|
all diff1, diff2, diff3: GCDTDiff | all opBase: Operand |
|
|
all batch1, batch2, batch3, batch4, batch5, batch6, batch7: GCDTBatch |
|
|
all batch8, batch9, batch10, batch11, batch12, batch13, batch14: GCDTBatch |
|
|
(dt.cOps = cop1 + cop2 && dt.pcOps = pop) =>
|
|
(diff1.op = cop1 && diff2.op = cop2 && diff3.op = pop) =>
|
|
(batch1.type = dt && batch1.base = opBase && batch1.fold = iden) =>
|
|
(batch1.ops = diff1 + diff2 + diff3) =>
|
|
batchStep[batch1, batch2, diff1]
|
|
&& batchStep[batch2, batch3, diff2]
|
|
&& batchStep[batch3, batch4, diff3]
|
|
&& batchStep[batch1, batch5, diff1]
|
|
&& batchStep[batch5, batch6, diff3]
|
|
&& batchStep[batch6, batch4, diff2]
|
|
&& batchStep[batch1, batch7, diff2]
|
|
&& batchStep[batch7, batch8, diff1]
|
|
&& batchStep[batch8, batch4, diff3]
|
|
&& batchStep[batch1, batch9, diff2]
|
|
&& batchStep[batch9, batch10, diff3]
|
|
&& batchStep[batch10, batch4, diff1]
|
|
&& batchStep[batch1, batch11, diff3]
|
|
&& batchStep[batch11, batch12, diff1]
|
|
&& batchStep[batch12, batch4, diff2]
|
|
&& batchStep[batch1, batch13, diff3]
|
|
&& batchStep[batch13, batch14, diff2]
|
|
&& batchStep[batch14, batch2, diff1] -- FIXME: this is wrong. Should be batch4
|
|
} for exactly 1 GCDT, 2 CommutativeOp, 1 PseudoCommutativeOp, 3 GCDTDiff, 6 Operand, 14 GCDTBatch
|
|
|
|
/*pred batchOneStep[batch: one GCDTBatch, fold: Operand one->one Operand] {
|
|
result in batch.type.operand
|
|
batch = {diff: batch |
|
|
some val | val = diff.op.op[
|
|
}*/
|
|
|
|
-- This is wrong as it doesn't accumulate pseudo-commutative operations
|
|
/*pred recApplyDiff [type: GCDT, batch: set GCDTDiff, inOpd, outOpd: Operand] {
|
|
inOpd in type.operand
|
|
outOpd in type.operand
|
|
batch = {diff: batch |
|
|
diff.op in type.ops
|
|
&& diff.right in type.operand
|
|
&& recApplyDiff[type, (batch - diff), applyDiff[type, diff, inOpd], outOpd]
|
|
&& outOpd in type.operand}
|
|
}
|
|
|
|
pred evalBatch [batch: one GCDTBatch, result: Operand] {
|
|
recApplyDiff[batch.type, batch.ops, batch.base, result]
|
|
}*/
|