(*
 * Bottom line at the top: We need type vars.
 *
 * I don't think this is going to work sweetly like type vars.  HOWEVER, we may
 * well not be able to have type vars, so let's deal with it the best we can.
 *
 * OK, there's hope after all.  One thing that might very well help things out
 * significantly is to require a type decl in a let, which really wouldn't be
 * all that bad anyway.  E.g., require
 *
 *     let var:type = ...
 *
 * This is clearly an aside here, given that there are no lets in this file.
 * But that's actually a good thing, in the sense that what we're after, here
 * and most likely in many other places, is a nice way to define liberry
 * functions.  The idea of not having var type inference is fully in keeping
 * with the general SE approach to SpecL.  Given that lets are not all that
 * pervasive in a lot of the specs we've written, and again having the
 * consistency of the SE context, I can pretty close to totally live with
 * requiring an explicit type decl in lets.
 *
 * So ..., the body of this file does not do much towards atempting to finish
 * the most-likely tortured and notationally-impoverished def of
 * AddWithRetentionAndNoJunk that does not use type vars.  Rather, we leave
 * this comment, and the one def of GenericList(T) as the beinnings of a
 * hopefully never-needed-to-by-completed task.  I.e., we'll have a restricted
 * form of parametric polymorphism, as inspried by Camarao et al., PPDP '04.
 *)

module StandardLibrary;

  export AddWithRetentionAndNoJunk;

  obj GenericList(T) = T*;    -- This really ain't going to cut the musturd.

  function AddWithRetentionAndNoJunk(
        valu:?T, in_list:?T*, out_list:?T*) -> boolean =

    (*
     * The basic condition is stated straightforwardly using the "in" operator.
     *)
    (valu in out_list)

        and

    (*
     * The retention condition is stated in logical terms as:
     *
     *     "For each element in the input list,
     *      that element is in the output list."
     *)
    (forall (value' in in_list) value' in out_list)

        and

    (*
     * The no junk condition is stated succinctly by saying that the number of
     * elements in the output list is one greater than the number of elements
     * in the input list.  Given the preceding two conditions, this precludes
     * any extra junk being in the output.
     *)
    (#out_list = #in_list + 1)

    description: (*
        The AddWithRetentionAndNoJunk function defines the logic of the
        "retention with no junk rule" for adding a value to a collection.  The
        rule is stated in functional terms, based on a value to be added, an
        input list to which the addition is to be made, and an output list to
        which the value has been successfully added.

        The retention-with-no-junk rule is stated with three conditions:

            (1) The basic condition:
                The value to be added is in the output list.
        
            (2) The retention condition:
                Everything in the input list is retained in the output list.

            (3) The no junk condition:
                Nothing else is in the output list.
    *);

  end AddWithRetentionAndNoJunk;

end StandardLibrary;