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.
44 lines
816 B
44 lines
816 B
open gcdt2[Int]
|
|
|
|
fun plusFn []: Int one->one (Int one->one Int) {
|
|
{opl, opr, res: Int |
|
|
res = opl + opr
|
|
}
|
|
}
|
|
|
|
fun plusOp []: Commutative {
|
|
{c: Commutative |
|
|
c.fn = plusFn[]
|
|
}
|
|
}
|
|
|
|
fun mulFn []: Int one->one (Int one->one Int) {
|
|
{opl, opr, res: Int |
|
|
res = mul[opl, opr]
|
|
}
|
|
}
|
|
|
|
fun mulOp []: PseudoCommutative {
|
|
{pc: PseudoCommutative |
|
|
pc.fn = mulFn[]
|
|
}
|
|
}
|
|
|
|
fun intType []: GCDT {
|
|
{dt: GCDT |
|
|
dt.universe = Int &&
|
|
dt.operations = {plusOp[] + mulOp[]}
|
|
}
|
|
}
|
|
|
|
run intType for 5
|
|
|
|
basicReduction: check {
|
|
all dt: GCDT | all r0: Reducer | all f1, f2, f3: Frame |
|
|
(dt = intType[] && r0 = baseReducer[0]) =>
|
|
(f1.op = plusOp[] && f1.right = 1) =>
|
|
(f2.op = mulOp[] && f2.right = 2) =>
|
|
(f3.op = plusOp[] && f3.right = 2) =>
|
|
reduceOnce[dt, f3, reduceOnce[dt, f2, reduceOnce[dt, f1, r0]]].base = 6
|
|
} for 20
|