(****
 *
 * Module Schedule defines the objects and operations related to scheduling
 * appointments, meetings, events, and tasks in the Calendar system.
 *
 *)

module Schedule;

  import CalendarDB.CalendarDB, CalendarDB.UserWorkSpace,
         CalendarDB.UserCalendar, CalendarDB.UserOptions;
  export ScheduledItem, Title, StartTime, Duration, Category, Date, Hours,
        Minutes, DateNumber;

  object ScheduledItem
    components: title:Title and start:StartOrDueDate and EndDate and Category;
    description: (*
        A ScheduledItem is the generic definition for the types of items stored
        in a calendar.  The Title component is a brief description of what the
        item is for.  The StartOrDueDate and EndDate components indicate when
        the item is scheduled.  The Category component is used to organize
        items into related color-coded categories.

        There are four specializations of ScheduledItem.  They are Appointment,
        Meeting, Event, and Task, q.q.v.
    *);
  end ScheduledItem;

  object Appointment extends ScheduledItem
    components: StartTime and Duration and RecurringInfo and Location and
        Security and Priority and RemindInfo and Details;
    description: (*

        An Appointment adds a number of components to a generic ScheduledItem.
        The StartTime and Duration indicate when the appointment starts and how
        long it lasts.  The Location is where it is held.  The Security
        indicates who can see that the appointment is scheduled.  Priority is
        how important the appointment is.  RemindInfo indicates if and how the
        user is reminded of the appointment.  Details are free form text
        describing any specific appointment details.
    *);
  end Appointment;

  object Meeting extends Appointment
    components: Attendees;
    description: (*
        A Meeting adds an Attendees component to an Appointment.  This extra
        component reflects the fact that a meeting is scheduled for more than
        one person, whereas an appointment is for a single user.  Scheduling a
        meeting involves checking more than one user calendar and finding a
        common time among all attendees.  The description of the
        ScheduleMeeting operation has further details.
    *);
  end Meeting;

  object Task extends ScheduledItem
    components: DueTime and RecurringInfo and Security and TaskPriority and
        RemindInfo and Details and CompletedFlag and CompletionDate;
    description: (*
        Like an Appointment, a Task adds a number of components to a generic
        ScheduledItem.  A Task differs from an Appointment as follows: (1)
        Appointments have Duration and Location, Tasks do not.  (2) For
        Appointments, the priority is either 'Must' or 'Optional'; for Tasks,
        priority is a positive integer indicating the relative priority of a
        task compared to other tasks.  (3) Tasks have a CompletedFlag and
        CompletionDate components; Appointments do not.
    *);
  end Task;

  object Event extends ScheduledItem
    components: Location;
    description: (*
        An Event is the simplest type of ScheduledItem.  The only component it
        adds to is Location.
    *);
  end Event;

  object Priority
    components: Must or Optional;
    description: (*
        Priority indicates whether an appointment is a must or if it is
        optional.  This information is used to indicate the general importance
        of an appointment to the user.  The operational use of Priority is in
        the ScheduleMeeting operation, where the meeting scheduler can elect to
        consider optional appointments as allowable times for a meeting.
    *);
  end Priority;

  object Must
    description: (*
        Indicates a scheduled item is 'Must' priority.
    *);
  end;

  object Optional
    description: (*
        Indicates a scheduled item is 'Optional' priority.
    *);
  end;

  object TaskPriority = integer
    description: (*
        A TaskPriority is a positive integer that defines the priority of one
        task relative to others.
    *);
  end TaskPriority;

  axiom TaskPriorityNonNegative = forall (tp: TaskPriority) tp >= 0;

  object Title = string
    description: (*
        A Title is a free-form text string describing a scheduled item.
    *);
  end Title;

  object StartOrDueDate = Date
    description: (*
        StartOrDueDate is a multi-purpose component of ScheduledItem.  Its
        purpose depends on whether an item is a Task and whether it is
        recurring (Events cannot recur).  For non-recurring appointments and
        meetings, StartOrDueDate is used as the single date on which the item
        is scheduled.  If the item is recurring, StartOrDueDate is the first
        date on which it occurs.  For a non-recurring Task, StartOrDueDate is
        the single date the task is due.  If the task is recurring,
        StartOrDueDate is the first date it is due.
    *);
  end StartDate;

  object EndDate = Date
    description: (*
        In recurring appointments, meetings, and tasks, the end date defines
        the last date on which the item will recur.  In events, the end date
        defines the last date of a multi-day event.  When the value of end date
        is empty, the StartOrDueDate component is interpreted as the single
        date on which the item occurs.
    *);
  end EndDate;

  object Date = string
    description: (*
        For now, a Date is just a string.  This definition will expand soon.
    *);
  end Date;

  object StartTime = Time
    description: (*
        StartTime is the starting time of a scheduled appointment or meeting.
    *);
  end StartTime;

  object DueTime = Time
    description: (*
        DueTime is the time a task is due.
    *);
  end StartTime;

  object Duration
    components: Hours and Minutes;
    description: (*
        Duration is the time length of a scheduled item, in hours and minutes.
    *);
  end Duration;

  object Hours = integer
    description: (*
        Hours component of a scheduled item duration.
    *);
  end;

  object Minutes = integer
    description: (*
        Minutes component of a scheduled item duration.
    *);
  end;

  object Time = string
    description: (*
        As with Date, Time is for now just as string.  This definition will
        expand soon.
    *);
  end Time;

  object RecurringInfo
    components: IsRecurring and Interval and IntervalDetails;
    description: (*
        RecurringInfo has components to specify the nature of a recurring item.
        IsRecurring is an on/off flag that indicates whether an item recurs.
        Interval is one of Weekly, Biweekly, Monthly, or Yearly.  The
        IntervalDetails component defines the precise means to define
        recurrence for the different interval levels.
    *);
  end RecurringInfo;

  object IsRecurring = boolean;

  obj Interval
    components: Weekly or Biweekly or Monthly or Yearly;
    description: (*
        Interval specifies the granularity at which recurring items are
        defined.  The Weekly and Biweekly settings allow the user to specify
        recurrence on one or more days of the week.  The Monthly setting allows
        the user to specify recurrence on one or more days in one or more weeks
        of each month.  The Yearly setting allows the user to specify
        recurrence on one or more specific dates in the year.
    *);
  end Interval;

  object Weekly
    description: (* Indicates a scheduled item recurs weekly. *);
  end;

  object Biweekly
    description: (* Indicates a scheduled item recurs bi-weekly. *);
  end;

  object Monthly
    description: (* Indicates a scheduled item recurs monthly. *);
  end;

  object Yearly
    description: (* Indicates a scheduled item recurs yearly. *);
  end;

  object IntervalDetails
    components: WeeklyDetails or MonthlyDetails;
    description: (*
        IntervalDetails are either weekly or monthly.
    *);
  end IntervalDetails;

  object WeeklyDetails
    components: OnSun and OnMon and OnTue and OnWed and OnThu and OnFri and
        OnSat;
    description: (*
        WeeklyDetails has an on/off setting for each day of the week on which
        an item recurs.  These details are also used for the BiWeekly setting
        of the recurrance interval.
    *);
  end WeeklyDetails;

  object MonthlyDetails
    components: MonthlyDayDetails or MonthlyDateDetails;
    description: (*
        MonthlyDetails can be specificed on a day-of-the-week basis or on
        specifc date(s) basis.  The two components contain the specific details
        for these two types of settings.
    *);
  end MonthlyDetails;

  object MonthlyDayDetails
    components: FirstWeekDetails and SecondWeekDetails and ThirdWeekDetails and
        FourthWeekDetails and FifthWeekDetails and LastWeekDetails;
    description: (*
        MonthlyDayDetails contains a weekly details component for each possible
        week of a month.  The First- through ThirdWeekDetails are distinct for
        all possible months.  Depending on the configuration of a particular
        month in a particular year, there is potential conflict in specifying
        recurrance in the fourth, fifth, or last weeks.  The conflicts are
        resolved as follows:

        For months with 4 weeks only, the settings in FifthWeekDetails do not
        apply, and the settings in LastWeekDetails, if present, override any
        settings in FourthWeekDetails.  For months with 5 weeks only, the
        settings in LastWeekDetails, if present, override any settings in
        FifthWeekDetails.  (For months with 6 weeks, the LastWeekDetails
        component applies to the 6th week, and there are no conflicts.)
    *);
  end MonthlyDayDetails;

  object MonthlyDateDetails
    components: DateNumber*;
    description: (*
        MonthlyDateDetails is a list of zero or more specific dates in a month
        on which an item recurs.
    *);
  end MonthlyDateDetails;

  object DateNumber = integer
    description: (*
        The numeric value of the date in a month, between 1 and 31.
    *);
  end DateNumber;

  object OnSun = boolean
    description: (* Indicates that an item recurs on Sunday. *);
  end;

  object OnMon = boolean
    description: (* Indicates that an item recurs on Monday. *);
  end;

  object OnTue = boolean
    description: (* Indicates that an item recurs on Tuesday. *);
  end;

  object OnWed = boolean
    description: (* Indicates that an item recurs on Wednesday. *);
  end;

  object OnThu = boolean
    description: (* Indicates that an item recurs on Thursday. *);
  end;

  object OnFri = boolean
    description: (* Indicates that an item recurs on Friday. *);
  end;

  object OnSat = boolean
    description: (* Indicates that an item recurs on Saturday. *);
  end;


  object FirstWeekDetails = WeeklyDetails
    description: (*
        Scheulding details for the first week of a month.
    *);
  end;

  object SecondWeekDetails = WeeklyDetails
    description: (*
        Scheulding details for the second week of a month.
    *);
  end;

  object ThirdWeekDetails = WeeklyDetails
    description: (*
        Scheulding details for the third week of a month.
    *);
  end;

  object FourthWeekDetails = WeeklyDetails
    description: (*
        Scheulding details for the fourth week of a month.
    *);
  end;

  object FifthWeekDetails = WeeklyDetails
    description: (*
        Scheulding details for the fifth week of a month.
    *);
  end;

  object LastWeekDetails = WeeklyDetails
    description: (*
        Scheulding details for the last week of a month.
    *);
  end;

  object Category
    components: Name and StandardColor;
    description: (*
        A Category has a Name and StandardColor, which serve distinguish it
        from other categories.  Colored-coded categories serve visual cues to
        the user when viewing lists of scheduled items in some form.
        Categories can also be used in filtered viewing.
    *);
  end Category;

  object StandardColor
    components: Black or Brown or Red or Orange or Yellow or Green or Blue or
        Purple;
    description: (*
        A StandardColor is one of a fixed set of possibilities.
    *);
  end StandardColor;

  object Black
    description: (* One of the built-in category colors. *);
  end;

  object Brown
    description: (* One of the built-in category colors. *);
  end;

  object Red
    description: (* One of the built-in category colors. *);
  end;

  object Orange
    description: (* One of the built-in category colors. *);
  end;

  object Yellow
    description: (* One of the built-in category colors. *);
  end;

  object Green
    description: (* One of the built-in category colors. *);
  end;

  object Blue
    description: (* One of the built-in category colors. *);
  end;

  object Purple
    description: (* One of the built-in category colors. *);
  end;

  object Location = string
    description: (*
        Location is a free-form string indicating in what physical location an
        item is scheduled.
    *);
  end Location;

  object Security
    components: Public or PublicTitle or Confidential or Private;
    description: (*
        Security is one of four possible levels, from Public to Private.  The
        levels specify the degree of visibility a scheduled item has to other
        users.  For an appointment, task, or event, "other users" are defined
        as all users other than the user on whose calendar the scheduled item
        appears.  For a meeting, "other users" are all users not on the
        Attendees list of the meeting.
    *);
  end Security;

  object Public
    description: (*
        Public security means other users can see the scheduled item and all
        the information about the item.
    *);
  end Public;

  object PublicTitle
    description: (*
        PublicTitle security means other users can see the title of the
        scheduled item but none of the other information about the item.
    *);
  end Public;

  object Confidential
    description: (*
        Confidential security means other users can only see that a user is
        unavailable for the time period of a scheduled item; no other
        information about the scheduled item is visible.  Since confidential
        security applies to a specific time period, it is meaningful only for
        appointments and meetings, not for tasks or events; tasks and events do
        not have specific time components.
    *);
  end;

  object Private
    description: (*
        Private security means other users see no information at all about a
        scheduled item, not even that the item is scheduled.  Note that private
        security hides a scheduled item from the ScheduleMeeting operation,
        q.v., so that a meeting may be scheduled at the same time as a private
        appointment.  It is up to the user to handle this situation by
        accepting or refusing the scheduled meeting.  Given the nature of
        private security, it does not apply to meetings.  I.e., only
        appointments can have private security.
    *);
  end;

  object RemindInfo
    components: RemindWhen and RemindWhere;
  end RemindInfo;

  object RemindWhen
    components: integer and ReminderTimeUnits;
    description: (*
        RemindWhen defines how soon before a scheduled item the reminder is to
        be sent.  The time units are minutes, hours, or days.
    *);
  end RemindInfo;

  object ReminderTimeUnits
    components: MinutesBefore or HoursBefore or DaysBefore;
    description: (*
        Reminders can come minutes, hours, or days before an appointment.  Each
        of these units can be fractional, for maximum flexibility.
    *);
  end AppointmentReminderUnits;

  object MinutesBefore = real
    description: (*
        Number of minutes before a scheduled item to issue the reminder.
    *);
  end MinutesBefore;

  object HoursBefore = real
    description: (*
        Number of hours before a scheduled item to issue the reminder.
    *);
  end HoursBefore;

  object DaysBefore = real
    description: (*
        Number of days before a scheduled item to issue the reminder.
    *);
  end DaysBefore;

  object RemindWhere = OnScreen or BeepOnly or Email
    description: (*
        RemindInfo defines one of three ways that the user is alerted when a
        scheduled event is to occur.  OnScreen means the user is reminded with
        a pop-up alert on her computer screen.  BeepOnly means the user is
        reminded with a simple audible tone on the computer.  Email means the
        user is sent an electronic mail message reminder.
    *);
  end RemindInfo;

  object OnScreen
    description: (*
        Indicates that reminders are displayed in an on-screen pop-up window.
    *);
  end OnScreen;

  object BeepOnly
    description: (*
        Indicates that reminders are signaled with an audible beep only, with
        no pop-up window.
    *);
  end BeepOnly;

  object Email
    description: (*
        Indicates that reminders are send as email messages.
    *);
  end Email;  

  object Details = string
    description: (*
        Details is a plain text string describing any details about a scheduled
        item the user may care to add.
    *);
  end Details;

  object Attendees
    components: Name*;
    description: (*
        Attendees is a list of names of those who attend a meeting.
    *);
  end Attendees;

  object Name = string
    description: (*
        The name of a category or a meeting attendee.
    *);
  end;


  object CompletedFlag = boolean
    description: (*
        CompletedFlag is true if a Task has been completed, false if not.  The
        system does not enforce any specific constraints on the setting of a
        task's CompletedFlag.  That is, the user may set or clear it at will.
        Hence the meaning of the CompletedFlag is up to user interpretation,
        particularly for recurring tasks.
    *);
  end CompletionDate;

  object CompletionDate
    components: Date;
    description: (*
        CompletionDate is date on which as task is completed.  The system does
        not enforce any specific constraints on the setting of a task's
        CompletionDate (other than it being a legal Date value).  The meaning
        of the CompletionDate value is up to user interpretation, particularly
        for recurring tasks.
    *);
  end CompletionDate;

  operation ScheduleAppointment
    inputs: cdb:CalendarDB, a:Appointment;
    outputs: cdb':CalendarDB;

    precondition: 
        (*
         * No item of the same StartTime, Duration, and Title is in the
         * workspace of the current given CalendarDB.
         *)
        -- not (exists (item in cdb.workspace.calendars[cdb.workspace.current])
        --    (item.start ...)
	;

    postcondition: ;

    description: (*
        ScheduleAppointment adds the given Appointment to the current user's
        Calendar of the given CalendarDB, if an appointment of the same time,
        duration, and title is not already scheduled.  The RequiresSaving flag
        of the calendar is set to true.
    *);
  end ScheduleAppointment;

  operation ScheduleMeeting
    inputs: CalendarDB, MeetingRequest;
    outputs: PossibleMeetingTimes;
    precondition: (* User must be group leader *);
    postcondition: ;
    description: (*
        ScheduleMeeting uses the given MeetingRequest to determine possible
        times that the requested meeting might be held, within the existing set
        of scheduled items in the CalendarDB.  The PossibleMeetingTimes output
        is a list of zero or more possible times and dates that the meeting can
        be held.
    *);
  end ScheduleMeeting;

  object MeetingRequest extends Meeting
    where: StartDate = EarliestStartDate, EndDate=LatestEndDate,
        StartTime=EarliestStartTime;
    components: LatestStartDate and LatestEndDate and LatestStartTime;
    description: (*
        A meeting request has all the components of a meeting plus three
        additional components to specify the latest dates and time at which the
        meeting can be scheduled.  A meeting request is used to specify a range
        of possible meeting times, to allow scheduling alternatives to be
        considered.  The description of the ScheduleMeeting operation has
        further details on how meeting requests are handled.
    *);
  end MeetingRequest;

  object EarliestStartDate = Date
    description: (*
        In a meeting request, the earliest possible start date for the meeting
        to be scheduled.
    *);
  end;

  object LatestStartDate = Date
    description: (*
        In a meeting request, the latest possible start date for the meeting to
        be scheduled.
    *);
  end;

  object EarliestEndDate = Date
    description: (*
        In a meeting request, the earliest possible end date for a recurring
        meeting to be scheduled.
    *);
  end;

  object LatestEndDate = Date
    description: (*
        In a meeting request, the latest possible end date for a recurring
        meeting to be scheduled.
    *);
  end;

  object EarliestStartTime = Time
    description: (*
        In a meeting request, the earliest possible start time for the meeting
        to be scheduled.
    *);
  end;

  object LatestStartTime = Time
    description: (*
        In a meeting request, the latest possible start time for the meeting to
        be scheduled.
    *);
  end;

  object PossibleMeetingTimes = (StartTime and Date)*;

  operation ConfirmMeeting
    inputs: CalendarDB, MeetingRequest, PossibleMeetingTimes, SelectedTime;
    outputs: CalendarDB;
    precondition: ;
    postcondition: ;
    description: (*
        ConfirmMeeting takes a CalendarDB, MeetingRequest, list of
        PossibleMeetingTimes, and a Selected time from the list.  It outputs a
        new CalendarDB with the given request scheduled at the selected time.
        Further details of output constraints are forthcoming.
    *);
  end ConfirmMeeting;

  object SelectedTime = integer;

  operation ScheduleTask
    inputs: CalendarDB, Task;
    outputs: ;
    precondition: ;
    postcondition: ;
    description: (*
        ScheduleTask adds the given Task to the given CalendarDB, if a task of
        the same time, duration, and title is not already scheduled.
    *);
  end ScheduleTask;

  operation ScheduleEvent
    inputs: CalendarDB, Event;
    outputs: CalendarDB;
    precondition: ;
    postcondition: ;
    description: (*
        ScheduleEvent adds the given Event to the given CalendarDB, if an event
        of the same time, duration, and title is not already scheduled.
    *);
  end ScheduleEvent;

end Schedule;