| 1 | #include "cfa-pair.h" | 
|---|
| 2 | #include "fstream" | 
|---|
| 3 |  | 
|---|
| 4 | forall(otype R, otype S | 
|---|
| 5 | | { int ?==?(R, R); int ?<?(R, R); int ?<?(S, S); }) | 
|---|
| 6 | int ?<?(pair(R, S) p, pair(R, S) q) { | 
|---|
| 7 | return p.first < q.first || ( p.first == q.first && p.second < q.second ); | 
|---|
| 8 | } | 
|---|
| 9 |  | 
|---|
| 10 | forall(otype R, otype S | 
|---|
| 11 | | { int ?==?(R, R); int ?<?(R, R); int ?<=?(S, S); }) | 
|---|
| 12 | int ?<=?(pair(R, S) p, pair(R, S) q) { | 
|---|
| 13 | return p.first < q.first || ( p.first == q.first && p.second <= q.second ); | 
|---|
| 14 | } | 
|---|
| 15 |  | 
|---|
| 16 | forall(otype R, otype S | { int ?==?(R, R); int ?==?(S, S); }) | 
|---|
| 17 | int ?==?(pair(R, S) p, pair(R, S) q) { | 
|---|
| 18 | return p.first == q.first && p.second == q.second; | 
|---|
| 19 | } | 
|---|
| 20 |  | 
|---|
| 21 | forall(otype R, otype S | { int ?!=?(R, R); int ?!=?(S, S); }) | 
|---|
| 22 | int ?!=?(pair(R, S) p, pair(R, S) q) { | 
|---|
| 23 | return p.first != q.first || p.second != q.second; | 
|---|
| 24 | } | 
|---|
| 25 |  | 
|---|
| 26 | forall(otype R, otype S | 
|---|
| 27 | | { int ?==?(R, R); int ?>?(R, R); int ?>?(S, S); }) | 
|---|
| 28 | int ?>?(pair(R, S) p, pair(R, S) q) { | 
|---|
| 29 | return p.first > q.first || ( p.first == q.first && p.second > q.second ); | 
|---|
| 30 | } | 
|---|
| 31 |  | 
|---|
| 32 | forall(otype R, otype S | 
|---|
| 33 | | { int ?==?(R, R); int ?>?(R, R); int ?>=?(S, S); }) | 
|---|
| 34 | int ?>=?(pair(R, S) p, pair(R, S) q) { | 
|---|
| 35 | return p.first > q.first || ( p.first == q.first && p.second >= q.second ); | 
|---|
| 36 | } | 
|---|
| 37 |  | 
|---|
| 38 | // forall(otype R, otype S) | 
|---|
| 39 | // forall(dtype ostype | ostream( ostype ) | { ostype & ?|?( ostype &, R ); ostype & ?|?( ostype &, S );  }) | 
|---|
| 40 | // ostype & ?|?( ostype & os, pair(R, S) p ) { | 
|---|
| 41 | //      return os | '[' | p.first | ',' | p.second | ']'; | 
|---|
| 42 | // } // ?|? | 
|---|