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

module FileMenu;

  from GradedItems import Gradebook;
  from EditMenu import UserWorkSpace;
  export all;

  object FileSpace is File*
    description: (*
        A FileSpace is an abstract model of a file space in the operating
        environment in which the GraderTool is run.  The FileSpace is a 
        collection of zero or more files.
     *);
  end;

  object File is
    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 Grader 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 gradebook_type:GraderType or other_type:OtherType
    description: (*
        The type of file data is either GraderType 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 GraderType
    description: (*
        File data typing tag indicating that a file contains gradebook data
        created by the Grader Tool.
    *);
  end GraderType;

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

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

  operation FileNewClass is
    inputs: uws:UserWorkSpace;
    outputs: uws':UserWorkSpace;

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

    precondition: ;

    postcondition:
        (*
         * The output workspace has a new empty gradebook and that gradebook is
         * current.  The user id of the new gradebook is that of the workspace,
         * the file is empty, the options are the given global options input,
         * and the gradebook does not require saving.  The gradebooks in
         * positions 1-last in the the input workspace are in positions
         * 2-last+1 in the output workspace.
         *)
        (exists (gb:Gradebook)
            (gb = uws'.gradebooks[1]) and
            (gb.uid = uws.uid) and
            (gb.file = nil) and
            (not gb.requires_saving) and
            (gb.items = nil) and
            (#(uws'.gradebooks) = #(uws.gradebooks) +1) and
            (forall (i:integer | (i >= 2) and (i <= #(uws.gradebooks)))
                uws'.gradebooks[i+1] = uws.gradebooks[i+1]
            )
        );

  end FileNewClass;

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

    description: (*
        Open an existing gradebook 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 gradebook.
         *)
        exists (file in fs)
            (file.name = fn) and
            file.permissions.is_readable and
            file.file_type?GraderType;

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

  end FileOpenClass;

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

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

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

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

  end FileClose;

operation FileCloseAll is
    inputs: fs:FileSpace, uws:UserWorkSpace;
    outputs: uws':UserWorkSpace;

    description: (*
        Close all active gradebooks if they do not require saving.
    *);

    precondition:
        (*
         * The gradebooks do not require saving.
         *)
	(forall (i:integer | (i >= 1) and (i <= #(uws.gradebooks)))
                not (uws.gradebooks[i].requires_saving);
            );
        

    postcondition:
        (*
         * The workspace index is empty.
         *)

        #(uws.gradebooks) = 0;
          
        

  end FileCloseAll;

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

    description: (*
        If the gradebook 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
         * Grader Tool.  Note further that this precondition disallows the
         * case where the current gradebook file has been externally deleted
         * since it was opened by the Grader Tool.  That is, the file must
         * both exist and be writable at the time the save is attempted.
         *)
        (uws.gradebooks[1].requires_saving)

            and

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

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

operation FileSaveAs is
    inputs: fs:FileSpace, uws:UserWorkSpace;
    outputs: fs':FileSpace, uws':UserWorkSpace;

    description: (*
        Save the gradebook in the workspace in the file space specified.
    *);

    precondition:
        (*
         * None
         *);

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

operation FileSaveAll is
    inputs: fs:FileSpace, uws:UserWorkSpace;
    outputs: fs':FileSpace, uws':UserWorkSpace;

    description: (*
        If any of the gradebooks in the given workspace requires saving, save them in the
        given file space.
    *);

    precondition:
        (*
         * Any of the given workspaces require saving.  Also, there is a writable
         * file of the current workspace filename in the given FileSpace.
         *)
        (exists( gradebook in uws)
        (forall (i:integer | (i >= 1) and (i <= #(uws.gradebooks)))
                (uws.gradebooks[i].requires_saving) and
                (exists (file in fs)
            (file.name = uws.gradebooks[i].file.name) and
            (file.permissions.is_writable));
            )
        );
        

    postcondition:
        (*
         * There is a gradebook-type file in the resulting FileSpace containing
         * the current workspace gradebook as its file data for all saved workspaces.  
         * In the resulting workspaces, the requires saving indicator is false.
         *)
        (exists (file in fs')
            (file.name = uws'.gradebooks[1].file.name) and
            (file.data = uws'.gradebooks[1]) and
            (file.permissions.is_writable) and
            (file.file_type?GraderType) and
            (not uws'.gradebooks[1].requires_saving)
        );
  end FileSaveAll;

end FileMenu;