(*
 * Old idea version -- that '*' by itself is a legal type spec.  This is the
 * built-in generic list idea.
 *
function IsSorted( l:* ) =
    forall (i,j: integer |
        (i in [1..#l]) and (j in [1..#l]) and (i<j))
            l[i].id < l[j].id;
 *
 *)

(* 
 * Another old idea version, that uses the would-be built-in type any.
 *
function IsSorted( l:any* ) =
    forall (i,j: integer |
        (i in [1..#l]) and (j in [1..#l]) and (i<j))
            l[i].id < l[j].id;
 *
 *)

obj SortableElem;

function IsSorted( l:SortableElem* ) =
    forall (i,j: integer |
        (i in [1..#l]) and (j in [1..#l]) and (i<j))
            l[i] < l[j];

obj ListElem < SortableElem;
op f(l:ListElem*)->boolean =
    IsSorted(l);

obj SortableListElem;
obj SortableList = SortableListElem*;

function IsSorted( l:SortableList ) =
    forall (i,j: integer |
        (i in [1..#l]) and (j in [1..#l]) and (i<j))
            l[i] < l[j];

obj MyList < SortableList (* = elems:integer* *)
    where: SortableListElem = integer;
end MyList;

obj KeyedTuple = key:string and valu:integer;
obj ListOfKeyedTuple < SortableList
    where: SortableListElem = KeyedTuple;
end ListOfKeyedTuple;

op LessThan(kt1:KeyedTuple, kt2:KeyedTuple)->boolean =
    kt1.key < kt2.key;


op f(l:MyList)->boolean = (
    (*
     * The following call to IsSorted(l) has got a lot going on in terms of
     * what's underneath typecheckingwise.  Here's a summary:
     *
     *     1. By generic instantiation, l is a list of ints, and is passed as
     *        such to IsSorted.
     *     2. Inside IsSort, the expression l[i] < l[j] type checked
     *        generically OK since '<' is fully overloaded on all types,
     *        including opaque types, which is what type l[i] and l[j] have at
     *        the time IsSorted is generically type checked.
     *     3. Via dynamic binding at runtime, l[i] and l[j] will have int
     *        values, not opaque ones, and we'll use the overload of ',' for
     *        ints.  We'll know this at runtime by the (normal) use of tagged
     *        values.
     *     4. At runtime, the KeyedTuple overload of '<' gets run from within
     *        IsSorted, via the normal rules of dynamic binding.
     *
     *     4a. SpecL Update: Since there is no more op overloading in SpecL,
     *         the original def of "<" has been renamed "LessThan".  However,
     *         putting a call to LessThan in the IsSorted functions does not
     *         typecheck, so the "<" operator is left there.  This does not
     *         really matter at this point, given the further remarks that
     *         follow.
     *
     *         The actual implementation of built-in operator overlading has
     *         never been anything but a pipe dream, even for the type checker,
     *         since there is no special handling of operator overloads.  E.g.,
     *         chkRelOp does no checking for operator overloads, and in fact is
     *         bogus as of 17jun09, given that the isOrdered macro is
     *         vacuuously true.  (See the 17jun09 LOG entry for more info.)
     *
     *         Furthermore, given the current implementation of the
     *         interpreter, I think that items 2-4 are pretty much bogus.  We
     *         can try to work things out here if we want at some point, but it
     *         ain't happening right now.
     *)
    IsSorted(l);

    l[1] = nil
    (* l.elems[1] = nil; *)
);