(*
 * Bottom line at the top: This attempt has failed, yet again.  The problem is
 * that type vars used in function signatures provide a context that cannot be
 * duplicated with with generic type defs alone.

 * In the example below, we define GenericList as a parameterized type and then
 * define a function with a parameter defined using that type uninstantiated.
 * This means that the function can be called with lists of any type.  The
 * problem, however, is what to do about the other function parameter which we
 * want to restrict to be of the basetype of the list.  The function signature
 * has only the generic type name, with no reference to its basetype.  That
 * means we have no static way to refer to that basetype elsewhere in the
 * signature.
 *
 * If we try add a basetype to the signature via instantiation of the generic
 * type, we're just going around in circles.  This is because we have no type
 * variable to do this with, and if we instantite with non-variable type, then
 * we've got a function that we could have declared with no generics at all.
 * I.e., we don't have a generic function.

 * See the comments in ./retention-and-no-junk-with-generics.fmsl.  This file
 * was yet another attempt to see if we can do (or satisfactoricly do) with
 * generic type defs what we can do function type vars.  The tack here is to
 * allow a function to be declared with an uninstantiated generic type, thereby
 * giving it what amounts to a type-var parameter.
 *)

module StandardLibrary;

  export AddWithRetentionAndNoJunk;

  obj T;
  obj GenericList(T) = T*;
  obj GenericListElement(T) = T;

  function AddWithRetentionAndNoJunk(
        valu:?T, in_list:GenericList, out_list:GenericList) -> boolean =
--           ^^
--           ^^ but what how do we define this without function type vars?

    (*
     * 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;