#line 647 "/home/ubuntu/felix/src/packages/core_type_constructors.fdoc"
class Tuple[U] {
virtual fun tuple_str (x:U) => str x;
}
instance[U,V with Str[U], Tuple[V]] Tuple[U ** V] {
fun tuple_str (x: U ** V) =>
match x with
| a ,, b => str a +", " + tuple_str b
endmatch
;
}
instance[U,V with Str[U], Str[V]] Tuple[U * V] {
fun tuple_str (x: U * V) =>
match x with
| a , b => str a +", " + str b
endmatch
;
}
instance [U, V with Tuple[U ** V]] Str[U ** V] {
fun str (x: U ** V) => "(" + tuple_str x +")";
}
instance[T,U] Str[T*U] {
fun str (t:T, u:U) => "("+str t + ", " + str u+")";
}
instance[T] Str[T*T] {
fun str (t1:T, t2:T) => "("+str t1 + ", " + str t2+")";
}
open[U, V with Tuple[U **V]] Str [U**V];
open[U, V with Str[U], Str[V]] Str [U*V];
instance [T,U with Eq[T], Eq[U]] Eq[T ** U] {
fun == : (T ** U) * (T ** U) -> bool =
| (ah ,, at) , (bh ,, bt) => ah == bh and at == bt;
;
}
instance[t,u with Eq[t],Eq[u]] Eq[t*u] {
fun == : (t * u) * (t * u) -> bool =
| (x1,y1),(x2,y2) => x1==x2 and y1 == y2
;
}
instance[t with Eq[t]] Eq[t*t] {
fun == : (t * t) * (t * t) -> bool =
| (x1,y1),(x2,y2) => x1==x2 and y1 == y2
;
}
instance [T,U with Tord[T], Tord[U]] Tord[T ** U] {
fun < : (T ** U) * (T ** U) -> bool =
| (ah ,, at) , (bh ,, bt) => ah < bh or ah == bh and at < bt;
;
}
instance[t,u with Tord[t],Tord[u]] Tord[t*u] {
fun < : (t * u) * (t * u) -> bool =
| (x1,y1),(x2,y2) => x1 < x2 or x1 == x2 and y1 < y2
;
}
instance[t with Tord[t]] Tord[t*t] {
fun < : (t * t) * (t * t) -> bool =
| (x1,y1),(x2,y2) => x1 < x2 or x1 == x2 and y1 < y2
;
}
open [T,U with Tord[T], Tord[U]] Tord[T ** U];
open [T,U with Tord[T], Tord[U]] Tord[T * U];
open [T with Tord[T]] Tord[T * T];
open class parallel_tuple_comp
{
fun ravel[u1,u2,r1,r2] (f1:u1->r1,f2:u2->r2) : u1 * u2 -> r1 * r2 =>
fun (x1:u1,x2:u2) => f1 x1, f2 x2;
fun ravel[u1,u2,u3,r1,r2,r3] (
f1:u1->r1,
f2:u2->r2,
f3:u3->r3
) : u1 * u2 * u3 -> r1 * r2 * r3 =>
fun (x1:u1,x2:u2,x3:u3) => f1 x1, f2 x2, f3 x3;
fun ravel[u1,u2,u3,u4,r1,r2,r3,r4] (
f1:u1->r1,
f2:u2->r2,
f3:u3->r3,
f4:u4->r4
) : u1 * u2 * u3 * u4 -> r1 * r2 * r3 * r4=>
fun (x1:u1,x2:u2,x3:u3,x4:u4) => f1 x1, f2 x2, f3 x3, f4 x4;
fun ravel[u1,u2,u3,u4,u5,r1,r2,r3,r4,r5] (
f1:u1->r1,
f2:u2->r2,
f3:u3->r3,
f4:u4->r4,
f5:u5->r5
) : u1 * u2 * u3 * u4 * u5 -> r1 * r2 * r3 * r4 * r5 =>
fun (x1:u1,x2:u2,x3:u3,x4:u4,x5:u5) => f1 x1, f2 x2, f3 x3, f4 x4, f5 x5;
}