(****
 *
 * Module File defines the objects and operations related to file processing
 * in the calendar system.
 *
 *)

module File;

  import CalendarDB.CalendarDB, CalendarDB.UserCalendar,
         CalendarDB.UserWorkSpace, CalendarDB.RequiresSaving,
         CalendarDB.Settings, CalendarDB.CalendarSpecificSettings,
         CalendarDB.Today;
  import Schedule.Date;
  import Admin.UserId;
  import Options.Options;
  export FileSpace, File, FileSize;

  object FileSpace = File*
    description: (*
        A FileSpace is an abstract model of a file space in the operating
        environment in which the CalendarTool is run.  The FileSpace is simply
        a collection of zero or more Files, with no other properties modeled
        here.
     *);
  end;

  object File
    components: name:FileName and permissions:FilePermissions and
        file_type:FileType and size:FileSize and data:FileData;
    description: (*
        A File is an abstraction of a file stored in the file space.  It has a
        name, permissions, type, and data.  These are the components sufficient
        to specify the behavior of Calendar Tool file operations.
    *);
  end File;

  object FileName = string
    description: (*
        The name of a file.  The string representation here is an abstraction
        of file names used in specific operating environments.  Implementations
        may obey any syntactic or semantic constraints imposed by a particular
        environment.
    *);
  end;

  object FilePermissions = is_readable:IsReadable and is_writable:IsWritable
    description: (*
        FilePermissions indicate whether a file is readable and/or writable.
    *);
  end;

  object IsReadable = boolean
    description: (*
        Flag indicating whether a file is readable, which is required to be
        true by the FileOpen operation.
    *);
  end;

  object IsWritable = boolean
    description: (*
        Flag indicating whether a file is writable, which is required to be
        true by the FileSave operation.
    *);
  end;

  object FileType = calendar_type:CalendarType or other_type:OtherType
    description: (*
        The type of file data is either CalendarType data (which we care
        about), SettingsType data (which we also care about), or any other
        type of data (which we don't care about).
    *);
  end FileType;

  object CalendarType
    description: (*
        File data typing tag indicating that a file contains calendar data
        created by the Calendar Tool.
    *);
  end CalendarType;

  object OtherType
    description: (*
        File data typing tag indicating that a file contains data other than
        calendar data created by the Calendar Tool.
    *);
  end OtherType;

  object FileSize = integer
    description: (*
       The size in megabytes of a file.
    *);
  end FileSize;

  object FileData = UserCalendar
    description: (*
        The abstract representation of calendar-type FileData is a UserCalendar
        object.  Calendar Tool implementors may use any concrete file data
        representation that accurately holds all UserCalendar components.
    *);
  end FileData;

  operation FileNew 
    inputs: uws:UserWorkSpace;
    outputs: uws':UserWorkSpace;

    description: (*
        Add a new empty calendar to the workspace and make it current.
    *);

    precondition: ;

    postcondition:
        (*
         * The output workspace has a new empty calendar and that calendar is
         * current.  The settings and user id of the new calendar are those of
         * the workspace.  The file is empty.  The name is unique, per the
         * logic defined in IsUniqueName, which requires a unique numeric
         * suffix if necessary for disambiguation.  The selected calendar date
         * is today and the calendar does not require saving.  The calendars in
         * positions 1-last in the the input workspace are in positions
         * 2-last+1 in the output workspace.  All other calendars in the input
         * workspace are in the output workspace.
         *)
        (exists (uc:UserCalendar)
            (uc.items = nil) and
            (uc = uws'.calendars[1]) and
            (uc.settings = uws.settings.cal) and
            (uc.uid = uws.uid) and
            (uc.file = nil) and
            IsUniqueName(uws, uws', uc) and
            (uc.selected_date) = Today() and
            (not uc.requires_saving) and
            (forall (i:integer | (i >= 1) and (i <= #(uws.calendars)))
                uws'.calendars[i+1] = uws.calendars[i]
            ) and
            forall (uc':UserCalendar)
                uc' in uws'.calendars iff uc = uc or uc' in uws.calendars;
        );

  end FileNew;

  operation FileOpen 
    inputs: fs:FileSpace, fn:FileName, uws:UserWorkSpace;
    outputs: uws':UserWorkSpace;

    description: (*
        Open an existing calendar file of the given name and put the data from
        that file in the workspace.
    *);

    precondition:
        (*
         * A file of the given name exists in the given file space, the file
         * is readable, and the file's data are of type calendar.
         *)
        exists (file in fs)
            (file.name = fn) and
            file.permissions.is_readable and
            file.file_type?.calendar_type;

    postcondition:
        (*
         * The output workspace has a new calendar containing the file data of
         * the input file, and that calendar is current.  The user id of the
         * new calendar is that of the workspace, the options are the given
         * global options input, and the calendar does not require saving.  The
         * calendars in positions 1-last in the the input workspace are in
         * positions 2-last+1 in the output workspace.
         *)
        (exists (uc:UserCalendar)
            (uc = uws'.calendars[1]) and
            (exists (file in fs)
                (file.name = fn) and
                (uc = file.data)
            ) and
            (uc.uid = uws.uid) and
            IsUniqueName(uws, uws', uc) and
            (uc.selected_date) = Today() and
            (not uc.requires_saving) and
            (#(uws'.calendars) = #(uws.calendars) +1) and
            (forall (i:integer | (i >= 2) and (i <= #(uws.calendars)))
                uws'.calendars[i+1] = uws.calendars[i+1]
            )
        );

  end FileOpen;

  operation FileClose 
    inputs: fs:FileSpace, uws:UserWorkSpace;
    outputs: uws':UserWorkSpace;

    description: (*
        Close the current calendar if it does not require saving.
    *);

    precondition: 
        (*
         * The calendar does not require saving.
         *)
        not (uws.calendars[1].requires_saving);

    postcondition:
        (*
         * The current calendar is deleted from the workspace.  The remaining
         * calendars, if any, are shifted in position in the list one position
         * earlier.
         *)
        (not (uws.calendars[1] in uws'.calendars)) and
        (#(uws'.calendars) = #(uws.calendars) - 1) and
        (forall (i:integer | (i >= 1) and (i < #(uws.calendars)))
            uws'.calendars[i] = uws.calendars[i+1];
        );

  end FileClose;

operation FileSave 
    inputs: fs:FileSpace, uws:UserWorkSpace;
    outputs: fs':FileSpace, uws':UserWorkSpace;

    description: (*
        If the calendar in the given workspace requires saving, save it in the
        given file space.
    *);

    precondition:
        (*
         * The given workspace requires saving.  Also, there is a writable
         * file of the current workspace filename in the given FileSpace.  Note
         * that the only way the current file could be unwritable is through an
         * external change to the file space since the file was opened by the
         * Calendar Tool.  Note further that this precondition disallows the
         * case where the current calendar file has been externally deleted
         * since it was opened by the calendar tool.  That is, the file must
         * both exist and be writable at the time the save is attempted.
         *)
        (uws.calendars[1].requires_saving)

            and

        (exists (file in fs)
            (file.name = uws.calendars[1].file.name) and
            (file.permissions.is_writable));

    postcondition:
        (*
         * There is a calendar-type file in the resulting FileSpace containing
         * the current workspace calendar as its file data.  In the resulting
         * workspace, the requires saving indicator is false.
         *)
        (exists (file in fs')
            (file.name = uws'.calendars[1].file.name) and
            (file.data = uws'.calendars[1]) and
            (file.permissions.is_writable) and
            (file.file_type?.calendar_type) and
            (not uws'.calendars[1].requires_saving)
        );
  end FileSave;

  function IsUniqueName
    inputs: uws:UserWorkSpace, uws':UserWorkSpace, uc:UserCalendar;
    outputs: boolean;
    description: (*
        If the name of the given user calendar is not unique in the given
        workspace uws, then suffix it with a unique integer.  The integer is
        one greater than the suffix of same-name calendar with the largest
        suffix in uws.  If name of the given calendar is unique in uws, then
        its name suffix is nil.
    *);
  end IsUniqueName;

end File;