| | 70 | |
| | 71 | theorems[\R, L1, L2\]() = |
| | 72 | <|[\((ActualReduction[\ R, L1 \], ActualReduction[\ R, L2 \], E -> R)->Boolean, (ActualReduction[\ R, L1 \], ActualReduction[\ R, L2 \], E -> R)->R)\] |
| | 73 | (fn (r, q, f) => conditionAbiding[\ R, L1, L2 \](r, q, f), fn (r, q, f) => efficientImplAbiding[\ R, L1, L2 \](r, q, f)) |
| | 74 | |> |
| | 75 | |
| | 76 | (*--- conditions ---*) |
| | 77 | conditionAbiding[\ R, L1, L2 \](q : ActualReduction[\ R, L1 \], r : ActualReduction[\ R, L2 \], f : E -> R) : Boolean = abiding(q, r) |
| | 78 | |
| | 79 | (*--- implementation using the abide-tree reduction *) |
| | 80 | efficientImplAbiding[\ R, L1, L2 \](q : ActualReduction[\ R, L1 \], r : ActualReduction[\ R, L2 \], f : E -> R) = do |
| | 81 | |
| | 82 | (* println("Abide!") *) |
| | 83 | |
| | 84 | (* we assume that two operators have the same lifting, i.e., L1 = L2 *) |
| | 85 | r.unlift(GeneratorATWrapper(seed()).generateAT[\L1\](q, r, fn a => r.lift(f(a)))) |
| | 86 | end |
| | 87 | |
| | 113 | |
| | 114 | theorems[\R, L1, L2\]() = |
| | 115 | <|[\((ActualReduction[\ R, L1 \], ActualReduction[\ R, L2 \], E -> R)->Boolean, (ActualReduction[\ R, L1 \], ActualReduction[\ R, L2 \], E -> R)->R)\] |
| | 116 | (fn (r, q, f) => conditionAbiding[\ R, L1, L2 \](r, q, f), fn (r, q, f) => efficientImplAbiding[\ R, L1, L2 \](r, q, f)) |
| | 117 | |> |
| | 118 | |
| | 119 | (*--- conditions ---*) |
| | 120 | conditionAbiding[\ R, L1, L2 \](q : ActualReduction[\ R, L1 \], r : ActualReduction[\ R, L2 \], f : E -> R) : Boolean = abiding(q, r) |
| | 121 | |
| | 122 | (*--- implementation using the abide-tree reduction *) |
| | 123 | efficientImplAbiding[\ R, L1, L2 \](q : ActualReduction[\ R, L1 \], r : ActualReduction[\ R, L2 \], f : E -> R) = do |
| | 124 | |
| | 125 | (* println("Abide!") *) |
| | 126 | |
| | 127 | (* we assume that two operators have the same lifting, i.e., L1 = L2 *) |
| | 128 | r.unlift(GeneratorATWrapper(seed()).generateAT[\L1\](r, q, fn a => r.lift(f(a)))) |
| | 129 | end |
| | 130 | |