share/lib/std/datatype/special.flx

  
  // Core types and type classes
  
  typedef any = any;
  

share/lib/std/datatype/typing.flx

  open class Typing
  {
  
    typefun dom(t:TYPE):TYPE =>
      typematch t with
      | ?a -> _ => a
      endmatch
    ;
  
    typefun cod(t:TYPE):TYPE =>
      typematch t with
      | _ -> ?b => b
      endmatch
    ;
  
    typefun prj1(t:TYPE):TYPE =>
      typematch t with
      | ?a * _ => a
      endmatch
    ;
  
    typefun prj2(t:TYPE):TYPE =>
      typematch t with
      | _ * ?b => b
      endmatch
    ;
  /*
    // THESE SHOULD PROBABLY BE FIXED OR DELETED
    typefun type_lnot(x:TYPE):TYPE=>
      typematch x with
      | 0 => 1
      | _ => 0
      endmatch
    ;
  
    typefun type_land(x:TYPE, y:TYPE):TYPE =>
      typematch (x,  y) with
      | 0, _ => 0
      | _,0 => 0
      | _,_ => 1
      endmatch
    ;
  
    typefun type_lor(x:TYPE, y:TYPE):TYPE=>
      typematch (x,  y) with
      | 0, 0 => 0
      | _,_ => 1
      endmatch
    ;
  
    typefun type_eq(x:TYPE, y:TYPE):TYPE=>
      typematch x with
      | y => typematch y with | x => 1 | _ => 0 endmatch
      | _ => 0
      endmatch
    ;
  
    typefun type_ne (x:TYPE, y:TYPE):TYPE=> type_lnot (type_eq (x , y));
  
    typefun type_le (x:TYPE, y:TYPE):TYPE=>
      typematch x with
      | y => 1 
      | _ => 0
      endmatch
    ;
  
    typefun type_ge (x:TYPE, y:TYPE):TYPE=>
      typematch y with
      | x => 1 
      | _ => 0
      endmatch
    ;
  
    typefun type_gt (x:TYPE, y:TYPE):TYPE=> type_le (y, x);
    typefun type_lt (x:TYPE, y:TYPE):TYPE=> type_ge (y, x);
  */
  
    // Polymorphic type comparisons, including subtyping AND subsumption
    typefun is_subtype (arg:TYPE, param:TYPE):BOOL =>
      subtypematch arg with
      | param => TRUE
      | _ => FALSE
      endmatch
    ;
  
    typefun is_supertype (param:TYPE, arg:TYPE):BOOL =>
      subtypematch arg with
      | param => TRUE
      | _ => FALSE
      endmatch
    ;
  
    typefun type_eq(a:TYPE, b:TYPE):BOOL =>
      typematch a with
      | b => TRUE
      | _ => FALSE
      endmatch
    ;
  
    const memcount[t] : size = "#memcount";
    const arrayindexcount[t] : size = "#arrayindexcount";
  
    // forward functor composition (1 argument)
    typefun \(\circ\) (f:TYPE->TYPE, g:TYPE->TYPE):TYPE->TYPE => 
      fun (T:TYPE):TYPE => f(g T)
    ;
  
    // reverse functor composition (1 argument)
    typefun \(\odot\) (f:TYPE->TYPE, g:TYPE->TYPE):TYPE->TYPE => 
      fun (T:TYPE):TYPE => g(f T)
    ;
  
  
  }
  

share/lib/std/datatype/option.flx

  
  // Note: some felix internals expect this to be defined here, not in a class, and
  // in this order.  Don't mess with it!
  publish "option type"
  variant opt[T] =
    | None
    | Some of T
  ;
  
  open class Option {
   
    instance[T with Show[T]] Str[opt[T]] {
      fun str (x:opt[T]) =>
        match x with
        | Some x => "Some " + (str x)
        | #None => "None"
        endmatch
      ;
    }
   
    instance[T with Eq[T]] Eq[opt[T]] {
      fun == : opt[T] * opt[T] -> bool =
      | None, None => true
      | Some x, Some y => x == y
      | _ => false
      ;
    }
    inherit[T] Eq[T];
   
    // Return the value of the option if it has any, otherwise
    // returns the default value provided
    fun or_else[T] (x:opt[T]) (d:T) : T =>
       match x with
       | Some v => v
       | #None => d
       endmatch
       ;
    
    // Returns the first option if it has the value, otherwise
    // the second option
    fun or_else[T] (x:opt[T]) (alt:opt[T]) : opt[T] =>
       match x with
       | Some _ => x
       | #None => alt
       endmatch
       ;
    
    // If the option has a value, call the given procedure on it
    proc iter[T] (_f:T->void) (x:opt[T]) =>
      match x with
      | #None => {}
      | Some v => { _f v; }
      endmatch
      ;
    
    // Convert an option to a list with either zero or one elements
    ctor[T] list[T] (x:opt[T]) => 
      match x with 
      | #None => list[T]()
      | Some v => list[T](v) 
      endmatch
    ;
    
    // True if this option has no value
    pure fun is_empty[T] : opt[T] -> 2 =
      | #None => true
      | _ => false
    ;
    
    // True if this option has a value
    pure fun is_defined[T] : opt[T] -> 2 =
      | #None => false
      | _ => true
    ;
    
    // Get the optional value; aborts if no value is available
    fun get[T] : opt[T] -> T =
      | Some v => v
    ;
    
    // If the option has a value, apply the function to it and return a new Some value.
    // If the option has no value, returns None
    fun map[T,U] (_f:T->U) (x:opt[T]): opt[U] => 
      match x with
      | #None => None[U]
      | Some v => Some(_f v) 
      endmatch
    ;
    
    // Mimics the filter operation on a list.
    // If there is a value and the predicate returns false for that value, return
    // None.  Otherwise return the same option object.
    fun filter[T] (P:T -> bool) (x:opt[T]) : opt[T] =>
      match x with
      | Some v => if P(v) then x else None[T] endif
      | #None => x
      endmatch
    ;
    
    // Make option types iterable.  Iteration will loop once
    // if there is a value.  It's a handy shortcut for using
    // the value if you don't care about the None case.
    gen iterator[T] (var x:opt[T]) () = {
      yield x;
      return None[T];
    }
  }
  
  class DefaultValue[T] {
    virtual fun default[T]: 1->T;
  
    fun or_default[T]  (x:opt[T]) () =>
                 x.or_else #default[T]
         ;
    
  }
  

share/lib/std/datatype/slice.flx

  
  open class Slice {
  variant slice[T] =
    | Slice_all
    | Slice_from of T
    | Slice_from_counted of T * int /* second arg is count */
    | Slice_to_incl of T
    | Slice_to_excl of T
    | Slice_range_incl of T * T
    | Slice_range_excl of T * T
    | Slice_one of T
    | Slice_none
  ;
  
  fun min[T with BoundRandomSequence[T]] (x:slice[T]) => match x with
    | ( Slice_all 
      | Slice_to_incl _ 
      | Slice_to_excl
      ) => #minval[T]
    | (Slice_from i 
      | Slice_from_counted (i,_) 
      | Slice_range_incl (i,_) 
      | Slice_range_excl (i,_) 
      | Slice_one i 
      ) => i
    | Slice_none => #maxval[T]
  ;
  fun max[T with BoundRandomSequence[T]] (x:slice[T]) => match x with
    | ( Slice_all 
      | Slice_from _
      ) => #maxval[T]
    | Slice_from_counted (i,n) => pred (advance (n, i))
    | Slice_to_incl i => i
    | Slice_to_excl i => pred i
    | Slice_range_incl (_,i) => i
    | Slice_range_excl (_,i) => pred i
    | Slice_one i => i
    | Slice_none => #minval  
  ;
  
  fun normalise_to_inclusive_range[T with BoundRandomSequence[T]] (x:slice[T]) =>
    let l = x.min in
    let u = x.max in
    if l <= u then Slice_range_incl (l,u) 
    else Slice_none[T]
  ;
  
  fun \(\cap\)[T with BoundRandomSequence[T]] (x:slice[T], y:slice[T]) =>
    let l = max (min x, min y) in
    let u = min (max x, max y) in
    if  l <= u then Slice_range_incl (l,u) 
    else Slice_none[T]
  ;
  
  fun \(\in\)[T with BoundRandomSequence[T]] (x:T, s:slice[T]) => 
    match s with
    | #Slice_all => true
    | Slice_from i => x >= i
    | Slice_from_counted (i,n) => x >= i and x < advance (n, i)
    | Slice_to_incl j => x <= j
    | Slice_to_excl j => x < j
    | Slice_range_incl (i,j) => x >= i and x <= j
    | Slice_range_excl (i,j) => x >= i and x < j 
    | Slice_one i => i == x
    | Slice_none => false
  ;
  
  
  gen iterator[T with BoundRandomSequence[T]] (s:slice[T]) =>
    match s with
    | Slice_one x => { yield Some x; return None[T]; }
    | Slice_range_incl (first, last) => slice_range_incl first last
    | Slice_range_excl (first, last) => slice_range_excl first last
    | Slice_to_incl (last) => slice_range_incl #minval[T] last
    | Slice_to_excl (last) => slice_range_excl #minval[T] last
    | Slice_from (first) => slice_range_incl first #maxval[T]
    | Slice_from_counted (first, count) => slice_from_counted first count
    | #Slice_all => slice_range_incl #minval #maxval
    | #Slice_none => { return None[T]; } 
    endmatch
  ;
  
  // Note: guarrantees no overflow
  // handles all cases for all integers correctly
  // produces nothing if first > last
  gen slice_range_incl[T with BoundRandomSequence[T]] (first:T) (last:T) () = {
    var i = first;
    while i < last do 
      yield Some i; 
      i = succ i;
    done 
    if i == last perform yield Some i;
    return None[T]; 
  }
  
  gen slice_range_excl[T with BoundRandomSequence[T]] (first:T) (limit:T) () = {
    var i = first;
    while i < limit do 
      yield Some i; 
      i = succ i;
    done 
    return None[T]; 
  }
  
  
  gen slice_from_counted[T with BoundRandomSequence[T]] (first:T) (count:int) () = {
    var k = count; 
    while k > 0 do 
      yield Some (advance (count - k, first)); 
      k = k - 1;
    done 
    return None[T]; 
  }
  
  // hack so for in f do .. done will work too
  gen iterator[t] (f:1->opt[t]) => f;
  
  // slice index calculator
  
  // Given length n, begin b and end e indicies
  // normalise so either 0 <= b <= e <= n or m = 0
  // 
  // if m = 0 ignore b,e and use empty slice
  // otherwise return a slice starting at b inclusive
  // and ending at e exclusive, length m > 0
  
  // Normalised form allows negative indices.
  // However out of range indices are trimmed back:
  // the calculation is NOT modular.
  
  
  fun cal_slice (n:int, var b:int, var e:int) = {
    if b<0 do b = b + n; done
    if b<0 do b = 0; done
    if b>=n do b = n; done
    // assert 0 <= b <= n (valid index or one past end)
    if e<0 do  e = e + n; done
    if e<0 do  e = 0; done
    if e>=n do e = n; done 
    // assert 0 <= e <= n (valid index or one pas end)
    var m = e - b; 
    if m<0 do m = 0; done
    // assert 0 <= m <= n (if m > 0 then b < e else m = 0)
    return b,e,m;
    // assert m = 0 or  0 <= b <= e <= n and 0 < m < n
  }
  
  variant gslice[T] =
    | GSlice of slice[T]
    | GSSList of list[gslice[T]]
    | GSIList of list[T]
    | GSIter of 1 -> opt[T]
    | GSMap of (T -> T) * gslice[T]
  ;
  
  gen gslist_iterator[T with Integer[T]] (ls: list[gslice[T]]) () : opt[T] =
  {
    var current = ls;
  next:>
    match current with
    | #Empty => return None[T];
    | Cons (gs, tail) =>
      for v in gs do yield Some v; done
      current = tail;
      goto next;
    endmatch;
  }
  
  gen gsmap_iterator[T] (f:T->T) (var gs:gslice[T]) () : opt[T] =
  {
    for v in gs do yield v.f.Some; done
    return None[T];
  }
  
  gen iterator[T with Integer[T]] (gs:gslice[T]) =>
    match gs with
    | GSlice s => iterator s
    | GSSList ls => gslist_iterator ls
    | GSIList ls => iterator ls
    | GSIter it => it
    | GSMap (f,gs) => gsmap_iterator f gs
  ;
  
  fun +[T with Integer[T]] (x:gslice[T], y:gslice[T]) =>
    GSSList (list (x,y))
  ;
  
  fun +[T with Integer[T]] (x:gslice[T], y:slice[T]) =>
   x + GSlice y
  ;
  
  fun +[T with Integer[T]] (x:slice[T], y:gslice[T]) =>
   GSlice x + y
  ;
  
  fun +[T with Integer[T]] (x:slice[T], y:slice[T]) =>
   GSlice x + GSlice y
  ;
  
  fun map[T with Integer[T]] (f:T->T) (gs:gslice[T]) =>
    GSMap (f,gs)
  ;
  }
  

Treated as finite cyclic groups.

share/lib/std/datatype/unitsum.flx

  
  // -----------------------------------------------------------------------------
  typedef void = 0;
  typedef unit = 1;
  
  instance Str[void] {
    fun str (x:void) => "void";
  }
  open Show[void];
  
  
  instance Str[unit] {
    fun str (x:unit) => "()";
  }
  open Show[unit];
  
  instance[T:COMPACTLINEAR] Eq[T] {
    fun == (x:T,y:T) => caseno x ==caseno y;
  }
  instance[T:COMPACTLINEAR] Tord[T] {
    fun < (x:T,y:T) => caseno x < caseno y;
  }
  instance[T:COMPACTLINEAR] ForwardSequence[T] {
    fun succ (x:T) => (caseno x + 1) :>> T;
  }
  instance[T:COMPACTLINEAR] BidirectionalSequence[T] {
    fun pred (x:T) => (caseno x - 1) :>> T;
  }
  instance[T:COMPACTLINEAR] UpperBoundTotalOrder[T] {
    fun maxval () => (memcount[T].int - 1) :>> T;
  }
  
  instance[T:COMPACTLINEAR] LowerBoundTotalOrder[T] {
    fun minval () => 0 :>> T;
  }
  
  instance[T:COMPACTLINEAR] RandomSequence[T] {
    fun advance (amt: int,  pos:T) => (caseno pos + amt) :>> T;
  }
  open[T:COMPACTLINEAR] BoundRandomSequence[T];
  
  
  typefun n"`+" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_add",(x,y),UNITSUM);
  typefun n"`-" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_diff",(x,y),UNITSUM);
  typefun n"`*" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_mul",(x,y),UNITSUM);
  typefun n"`/" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_div",(x,y),UNITSUM);
  typefun n"`%" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_mod",(x,y),UNITSUM);
  
  typefun n"_unitsum_min" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_min",(x,y),UNITSUM);
  typefun n"_unitsum_max" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_max",(x,y),UNITSUM);
  typefun n"_unitsum_gcd" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_gcd",(x,y),UNITSUM);
  typefun n"_unitsum_lcm" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_lcm",(x,y),UNITSUM);
  
  typefun n"`<" (x:UNITSUM,y:UNITSUM):BOOL=> _typeop ("_unitsum_lt",(x,y),BOOL);
  typefun n"`>" (x:UNITSUM,y:UNITSUM):BOOL=> _typeop ("_unitsum_lt",(y,x),BOOL);
  typefun n"`==" (x:UNITSUM,y:UNITSUM):BOOL=> x `< y and y `< x;

// -----------------------------------------------------------------------------

share/lib/std/datatype/functional.flx

  
  Categorical Operators
  open class Functional
  {
    // note: in Felix, products are uniquely decomposable, but arrows
    // are not. So we cannot overload based on arrow factorisation.
    // for example, the curry functions can be overloaded but
    // the uncurry functions cannot be
  
    // Note: Felix is not powerful enough to generalise these
    // operation in user code, i.e. polyadic programming
  
    change star into arrow (2 components)
    fun curry[u,v,r] (f:u*v->r) : u -> v -> r => fun (x:u) (y:v) => f (x,y);
  
    change star into arrow (3 components)
    fun curry[u,v,w,r] (f:u*v*w->r) : u -> v -> w -> r => fun (x:u) (y:v) (z:w) => f (x,y,z);
  
    change arrow into star (arity 2)
    fun uncurry2[u,v,r] (f:u->v->r) : u * v -> r => fun (x:u,y:v) => f x y;
  
    change arrow into star (arity 3)
    fun uncurry3[u,v,w,r] (f:u->v->w->r) : u * v * w -> r => fun (x:u,y:v,z:w) => f x y z;
  
    argument order permutation (2 components)
    fun twist[u,v,r] (f:u*v->r) : v * u -> r => fun (x:v,y:u) => f (y,x);
  
    projection 1 (2 components)
    fun proj1[u1,u2,r1,r2] (f:u1*u2->r1*r2) : u1 * u2 -> r1 => 
      fun (x:u1*u2) => match f x with | a,_ => a endmatch;
  
    projection 2 (2 components)
    fun proj2[u1,u2,r1,r2] (f:u1*u2->r1*r2) : u1 * u2 -> r2 => 
      fun (x:u1*u2) => match f x with | _,b => b endmatch;
  
    // aka \delta or diagonal function 
    fun dup[T] (x:T) => x,x;
  
    unique product (of above projections)
    // if f: C-> A and g: C -> B there is a unique function
    // <f,g>: C -> A * B such that f = <f,g> \odot \pi0 and
    // g = <f,g> \odot pi1
    // WHAT IS THE FUNCTION CALLED?
  
    fun prdx[u1,r1,r2] (f1:u1->r1,f2:u1->r2) : u1 -> r1 * r2 => 
      fun (x1:u1) => f1 x1, f2 x1;
  
    series composition (2 functions)
    fun compose[u,v,w] (f:v->w, g:u->v) : u -> w => 
      fun (x:u) => f (g x)
    ;
  
    series composition (2 functions)
    fun compose[u,v,w] (f:v->.w, g:u->.v) : u ->. w => 
      fun (x:u) =>. f (g x)
    ;
  
    fun \(\circ\) [u,v,w] (f:v->w, g:u->v) : u -> w => 
      fun (x:u) => f (g x)
    ;
  
    fun \(\circ\) [u,v,w] (f:v->.w, g:u->.v) : u ->. w => 
      fun (x:u) =>. f (g x)
    ;
  
    series reverse composition (2 functions)
    fun rev_compose[u,v,w] (f:u->v, g:v->w) : u -> w => 
      fun (x:u) => g (f x)
    ;
  
    series reverse composition (2 functions)
    fun rev_compose[u,v,w] (f:u->.v, g:v->.w) : u ->. w => 
      fun (x:u) =>. g (f x)
    ;
  
    series reverse composition (2 functions)
    fun \(\odot\)[u,v,w] (f:u->v, g:v->w) : u -> w => 
      fun (x:u) => g (f x)
    ;
  
    series reverse composition (2 functions)
    fun \(\odot\)[u,v,w] (f:u->.v, g:v->.w) : u ->. w => 
      fun (x:u) =>. g (f x)
    ;
  
    series reverse composition (2 functions)
    fun \(\cdot\)[u,v,w] (f:u->v, g:v->w) : u -> w => 
      fun (x:u) => g (f x)
    ;
  
    series reverse composition (2 functions)
    fun \(\cdot\)[u,v,w] (f:u->.v, g:v->.w) : u -> w => 
      fun (x:u) =>. g (f x)
    ;
  
    // these are in the wrong place but they have to go somewhere!
    // these are bindings to C function types and also, conditionally,
    // clang block function types.
    // 
    // They're provided so C parameter types as for the T, P1, P2 
    // in C notation T (*f) (P1 p1, P2 p2)
    // are syntactically atomic since Felix doesn't know how to ravel
    // the name in complicated types...
    // 
    // the c variants are for C functions
    // the b variants are for clang block functions
    // the integer indicates the number of type variables required
  
    type cproc1[R] = "typename _type1<?1>::cproc";
    type cfun1[R] = "typename _type1<?1>::cfun";
    type bproc1[R] = "typename _type1<?1>::bproc";
    type bfun1[R] = "typename _type1<?1>::bfun";
  
    type cproc2[R,P1] = "typename _type2<?1,?2>::cproc";
    type cfun2[R,P1] = "typename _type2<?1,?2>::cfun";
    type bproc2[R,P1] = "typename _type2<?1,?2>::bproc";
    type bfun2[R,P1] = "typename _type2<?1,?2>::bfun";
  
    type cproc3[R,P1,P2] = "typename _type3<?1,?2,?3>::cproc";
    type cfun3[R,P1,P2] = "typename _type3<?1,?2,?3>::cfun";
    type bproc3[R,P1,P2] = "typename _type3<?1,?2,?3>::bproc";
    type bfun3[R,P1,P2] = "typename _type3<?1,?2,?3>::bfun";
  
    type cproc4[R,P1,P2,P3] = "typename _type4<?1,?2,?3,?4>::cproc";
    type cfun4[R,P1,P2,P3] = "typename _type4<?1,?2,?3,?4>::cfun";
    type bproc4[R,P1,P2,P3] = "typename _type4<?1,?2,?3,?4>::bproc";
    type bfun4[R,P1,P2,P3] = "typename _type4<?1,?2,?3,?4>::bfun";
  
    type cproc5[R,P1,P2,P3,P4] = "typename _type5<?1,?2,?3,?4,?5>::cproc";
    type cfun5[R,P1,P2,P3,P4] = "typename _type5<?1,?2,?3,?4,?5>::cfun";
    type bproc5[R,P1,P2,P3,P4] = "typename _type5<?1,?2,?3,?4,?5>::bproc";
    type bfun5[R,P1,P2,P3,P4] = "typename _type5<?1,?2,?3,?4,?5>::bfun";
  
  }
  

share/lib/std/datatype/tuple.flx

  
  //------------------------------------------------------------------------------
  // Class Str: convert to string
  
  // Tuple class for inner tuple listing
  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
    ;
  }
  
  // actual Str class impl.
  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];
  
  
  //------------------------------------------------------------------------------
  // Class Eq: Equality
  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
    ;
  }
  
  //------------------------------------------------------------------------------
  // Class Tord: Total Order
  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];
  
  /* type equality now requires type_eq!
  //------------------------------------------------------------------------------
  // Generic Field access
  fun field[n,t,u where n==0] (a:t,b:u)=>a;
  fun field[n,t,u where n==1] (a:t,b:u)=>b;
  
  fun field[n,t,u,v where n==0] (a:t,b:u,c:v)=>a;
  fun field[n,t,u,v where n==1] (a:t,b:u,c:v)=>b;
  fun field[n,t,u,v where n==2] (a:t,b:u,c:v)=>c;
  
  fun field[n,t,u,v,w where n==0] (a:t,b:u,c:v,d:w)=>a;
  fun field[n,t,u,v,w where n==1] (a:t,b:u,c:v,d:w)=>b;
  fun field[n,t,u,v,w where n==2] (a:t,b:u,c:v,d:w)=>c;
  fun field[n,t,u,v,w where n==3] (a:t,b:u,c:v,d:w)=>d;
  
  fun field[n,t,u,v,w,x where n==0] (a:t,b:u,c:v,d:w,e:x)=>a;
  fun field[n,t,u,v,w,x where n==1] (a:t,b:u,c:v,d:w,e:x)=>b;
  fun field[n,t,u,v,w,x where n==2] (a:t,b:u,c:v,d:w,e:x)=>c;
  fun field[n,t,u,v,w,x where n==3] (a:t,b:u,c:v,d:w,e:x)=>d;
  fun field[n,t,u,v,w,x where n==4] (a:t,b:u,c:v,d:w,e:x)=>e;
  */
  
  //------------------------------------------------------------------------------
  open class parallel_tuple_comp
  {
    parallel composition
    // notation: f \times g
    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;
  
  }