(****
 *
 * 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.CurrentWorkingCalendar, CalendarDB.RequiresSaving, CalendarDB.GlobalOptions, CalendarDB.UserId, CalendarDB.UserOptions;
  import Admin.Id;
  export FileSpace, File;

  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 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;
  object FilePermissions =  readable:boolean and writable:boolean;
  object FileType =  calendar_type:CalendarType or other_type:OtherType
    description: (*
        The type of file data is either CalendarType data (which we care about)
        or any other type of data that can be stored in a file, which we don't
        care about.
    *);
  end FileType;

  object CalendarType;
  object OtherType;
  object FileData =  UserCalendar;

  operation FileNew
    inputs: uws:UserWorkSpace, go:GlobalOptions;
    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, and the options are the given global options
         * input.  The normal "no junk, no confusion" condition holds for the
         * output workspace.
         *)
        (exists (uc:UserCalendar)
            (uc = uws'.calendars[1]) and
            (uws'.current = 1) and
	    (uc.uid = uws.uid) and
            (uc.file = nil) and
	    (uc.options = go) and
	    (forall (uc':UserCalendar | uc' != uc)
		(uc in uws'.calendars) iff (uc in uws.calendars))
        );

  end FileNew;

  operation FileOpen
    inputs: fs:FileSpace, fn:FileName, uws:UserWorkSpace;
    outputs: fs':FileSpace, 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.permissions.readable and
            file.file_type?.calendar_type;

    postcondition:
        (* 
         * The calendar data in the input file is added to the calendars list
         * in the output workspace; the current calendar is the input calendar;
         * the workspace does not require saving.
         *)
        exists (file in fs) (
            (file.data in uws'.calendars) and
            (not uws'.calendars[uws.current].requires_saving) and
            (exists (n:integer)
                (uws'.calendars[n] = file.data) and
                (uws'.current = n)
            ) and
            (not uws'.calendars[uws.current].requires_saving)
        );

  end FileOpen;

  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[uws.current].requires_saving)

            and

        (exists (file in fs)
            (file.name = uws.calendars[uws.current].file.name) and
            (file.permissions.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 and is false.
         *)
        (exists (file in fs')
            (file.name = uws'.calendars[uws.current].file.name) and
            (file.permissions.writable) and
            (file.file_type?.calendar_type) and
            (not uws'.calendars[uws.current].requires_saving)
        );
  end FileSave;

  op Foo(fs:FileSpace, uws:UserWorkSpace) = (
    (fs = FileOpen.fsx) and
    (fs = FileOpen(fs, "xyz", uws).fs')
  );

end File;