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

module File;

  from CalendarDB import CalendarDB, UserCalendar, UserWorkSpace,
    RequiresSaving;
  from Admin import UserId, AdminPassword, AdminEmailAddress;
  from Options import RegularUserOptions, AdministrativeOptions;
  export FileSpace, File, FileSize;

  object FileSpace is 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 is
    components: name:FileName and permissions:FilePermissions and
        file_type:FileType and data:FileData and size:FileSize;
    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 is 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 is_readable:IsReadable and is_writable:IsWritable
    description: (*
        FilePermissions indicate whether a file is readable and/or writable.
    *);
  end;

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

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

  object FileType is 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 FileData is 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;

  object FileSize is integer
    description: (*
       Size in bytes of the file.
    *);
  end FileSize;


  operation FileNew is
    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 user id of the new calendar is that of the workspace,
         * the file is empty, 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
<<<<<<< file.rsl
         * 2-last+1 in the output workspace.  The number of unnamed calendars
         * is incremented by one.
=======
         * 2-last+1 in the output workspace.  The number of unnamed calendars
         * is incremented by on
>>>>>>> 1.12
         *)
        (exists (uc:UserCalendar)
            (uc = uws'.calendars[1]) and
            (uc.uid = uws.uid) and
            (uc.file = nil) and
            (not uc.requires_saving) and
            (uc.items = nil) and
            (#(uws'.calendars) = #(uws.calendars) + 1) and
            (forall (i:integer | (i >= 1) and (i <= #(uws.calendars)))
                uws'.calendars[i+1] = uws.calendars[i]
            )
        );

  end FileNew;

  operation FileOpen is
    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
            (uc.uid = uws.uid) and
            (exists (file in fs)
                (file.name = fn) and
                (uc = file.data)
            ) 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 is
    inputs: 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 is
    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;

  object AdminSettingsFile is
    components: passwd:AdminPassword and email:AdminEmailAddress and
        options:AdministrativeOptions;
    description: (*
       
    *);
  end AdminSettingsFile;

end File;