(****
 *
 * Module RolodexGUI defines objects and operations that are specific to the
 * GUI for the abstract Rolodex defined in the Rolodex module, q.v.
 *
 * IMPORTANT NOTE: As soon as the translator is fixed we need to change the
 * names InvokeChange and InvokeDelete to plan Change and Delete.
 *
 *)

module RolodexGUI;

  import Rolodex.Rolodex, Rolodex.Card, Rolodex.Name, Rolodex.Id, Rolodex.Add,
    Rolodex.Find, Rolodex.Change, Rolodex.Delete;
  import Screen.Screen;

  operation InvokeAdd
    inputs: r:Rolodex, ac:AddConfirmation, s:Screen;
    outputs: r':Rolodex, s':Screen;

    description: (*
        Invoke the model Add operation from the GUI.  Get the card to be added
        from the user and invoke the model add to perform the computation.
    *);

    postcondition: (
        let card_to_add, input_screen = GetUserCardInput();
        if (ac?.ok) then
            (r' = Add(r, card_to_add)) and
            (s = input_screen)
        else if (ac?.cancel) then
            (r' = r) and
            (s = EmptyScreen());
        else  (* ac?.clear)
            (r' = r) and
            (s = EmptyCardScreen());
    );
  end;

  operation InvokeFind
    inputs: r:Rolodex;
    outputs: s:Screen;

    description: (*
        Invoke the model Add operation from the GUI.  Get the card to be added
        from the user and invoke the model Find to perform the computation.
        Display the found results to the user.
    *);

    postcondition: (
        let card_name = GetUserNameInput();
        let cards = Find(r, card_name);
        s = DisplayCards(cards);
    );        
  end;

  operation InvokeChange
    inputs: r:Rolodex, n:Name;
    outputs: r':Rolodex;

    description: (*
        Invoke the model Delete operation from the GUI.  InvokeChange uses
        auxiliary operations to obtain Card inputs from the user.  These inputs
        are then passed to the model version of Change to perform the actual
        change computation.  First, FindCardsToChange is used to get a list of
        zero or more cards to select from.  Then SelectedCardToChange is used
        on the found list to get a single card to change.  Finally, the model
        Change operation is invoked with the selected card, new card data from
        the user, and the given Rolodex input.
    *);

    postcondition: (
	let found_list = FindCardsToChange(r, n);
	let selected_card = SelectCardToChange(found_list, GetUserIntInput());
	r' = Change(r, selected_card, GetUserCardInput());
    );

  end;

  operation FindCardsToChange
    inputs: r:Rolodex, n:Name;
    outputs: cl:Card*;

    description: (*
        In preparation for changing a card, find all of the cards of the given
        name in the given rolodex.
    *);

    postcondition:

        (*
         * Cards in the output list consist of those in the input rolodex with 
         * the given name.
         *)
        forall (c:Card)
            (c in cl) iff ((c in r) and (c.name = n))

            and

        (*
         * A multi-card output list is sorted in ascending order by card id.
         *)
        forall (i:integer | (i >= 1) and (i < #cl))
            cl[i].id < cl[i+1].id;

  end FindCardsToChange;

  operation SelectCardToChange
    inputs: cl:Card*, i:integer;
    outputs: c:Card;

    description: (*
        Select one card from a list of cards found to change.
    *);

    precondition:
        (*
         * The given position i is within the bounds of the given card list.
         *)
        (1 >= i) and (i <= #cl);

    postcondition:
        (*
         * The output card is the one at the ith position in the list.
         *)
        c = cl[i];

  end SelectCardToChange;

  operation InvokeDelete
    inputs: r:Rolodex, n:Name;
    outputs: r':Rolodex;

    description: (*
        This version of Delete is invoked from the GUI interface.  It uses
        auxiliary operations to obtain Card inputs from the user.  These inputs
        are then passed to the model version of Delete to perform the actual
        change computation.  First, FindCardsToDelete is used to get a list of
        zero or more cards to select from.  Then SelectedCardToDelete is used
        on the found list to get a single card to change.  Finally, the model
        Delete operation is invoked with the selected card, new card data from
        the user, and the given Rolodex input.
    *);

    postcondition: (
	let found_list = FindCardsToDelete(r, n);
	let selected_card = SelectCardToDelete(found_list, GetUserIntInput());
	r' = Delete(r, selected_card);
    );

  end;

  operation FindCardsToDelete
    inputs: r:Rolodex, n:Name;
    outputs: cl:Card*;

    description: (*
        In preparation for deleteing a card, find all of the cards of the given
        name in the given rolodex.
    *);

    postcondition:

        (*
         * Cards in the output list consist of those in the input rolodex with 
         * the given name.
         *)
        forall (c:Card)
            (c in cl) iff ((c in r) and (c.name = n))

            and

        (*
         * A multi-card output list is sorted in ascending order by card id.
         *)
	forall (i:integer | (i >= 1) and (i < #cl))
	    cl[i].id < cl[i+1].id;

  end FindCardsToDelete;

  operation SelectCardToDelete
    inputs: cl:Card*, i:integer;
    outputs: c:Card;

    description: (*
        Select one card from a list of cards found to delete.
    *);

    precondition:
        (*
         * The given position i is within the bounds of the given card list.
         *)
        (1 >= i) and (i <= #cl);

    postcondition:
        (*
         * The output card is the one at the ith position in the list.
         *)
        c = cl[i];

  end SelectCardToDelete;

  function GetUserCardInput() -> (Card, Screen);
  function GetUserIntInput() -> integer;
  function GetUserNameInput() -> Name;

  function DisplayCards(cl:Card*)->Screen;

end RolodexGUI;