(****
 *
 * Module Spreadsheet defines the spreadsheet of a class for maintaing students grades.
*)

module Spreadsheet;
	
  	from File import FileSpace, File;
  	from Edit import Clipboard, Selection, SelectionContext;
	export GradedItem, Gradesheet, StudentInfo, UserWorkSpace, RequiresSaving, PreviousState;

	object UserWorkSpace is
    		components: Gradesheets:Gradesheet* and previous_state:PreviousState and clipboard:Clipboard
		and selection:Selection and context:SelectionContext;
    		
		description: (*
        		The UserWorkSpace contains the active gradesheets upon which the user is
		        working.  The first component is the UserId of the current user, which
		        is used as necessary by operations that input the workspace to
		        determine who the user is.  The Gradesheeet* component is the list of
		        active gradesheets; the list is maintained in the order visited by the
		        user, with the first element being the most recently visited, and hence
		        current, and the last element being the earliest visited.  The
		        UserOptions component is the list of individualized user options, some
		        of which may be different than the global gradesheet options.  The
		        previous_state component is used to support one level of command undo.
		        The Clipboard is used with the Edit cut, copy, and paste operations.
		*);
  	end UserWorkSpace;
	
	object PreviousState is
		components: StudentInfo*;
		description: (*
	        	PreviousState is the snapshot of students before the most
	        	recently performed operation used by EditUndo.  The
	        	Add, Edit, and Delete operations save the previous state to
	        	support Undo.
	    	*);
	end PreviousState;
	
	object RequiresSaving is boolean
    		description: (*
        		True if a gradesheet requires saving, which is the case if one or more
		        successful edit operations has been performed on the gradesheet since the
       			most recent save.  The gradesheet edit operations are Add, Edit,
        		and Delete.
    		*);
	end RequiresSaving;

	object Gradesheet is
		components: items:GradedItem* and si:StudentInfo* and ClassName and
		requires_saving:RequiresSaving;
		description: (*
			A Gradesheet is a spreadsheet in which the rows are made up of 
			Student objects plus whatever columns the instructor has created 
			for graded assignments such as homework and tests.
		*);
	end Gradesheet;

	object ClassName is
		components: Course and Quarter and Section;
		description: (*
			A ClassName identifies what class a particular gradesheet is for
			and appears in the title bar.
		*);
	end ClassName;

	object Course is
		components: Major and CNumber;
	end Course;

	object Major is string;
	object CNumber is integer;

	object Quarter is
		components: Season and Year;
	end Course;

	object Season is string;
	object Year is integer;
	object Section is integer;

	object StudentInfo is
		components: n:Name and i:ID and un:UserName and and GradedItem* and s:Score and
			Grade;
		description: (*
			StudentInfo is a row of cells inculding a students information 
			such as name, id, grade, ect.
		*);
	end StudentInfo;
	
	object Name is string;
	object ID is integer;
	object UserName is string;
	object Score is integer;
	object Grade is string;
	
	object GradedItem is
		components: t:Title and par:Parent and SDate and EDate and p:Points and pp:PointsPossible
			and Weight and Descript;
		description: (*
			A GradedItem is any type of item anf a student can recieve a
			grade for, such as an assignment, test or quiz.
		*);
	end GradedItem;

	object Title is string;

	object Parent is 
		components: Title;
	end Parent;

	object Points is integer;
	object PointsPossible is integer;

	object SDate is
		components: Date and Month and Year;
	end SDate;

	object EDate is
		components: Date and Month and Year;
	end EDate;

	object Date is integer;
	object Month is string;
	object Weight is integer;
	object Descript is string;

	operation AddItem is
		inputs: gs:Gradesheet, gi:GradedItem;
		outputs: gs':Gradesheet;

		description: (*
	        	Add the given GradedItem to the Gradesheet.  The Title of a GradedItem 
			must not be the same as an item already in the Gradesheet.  The 
			Title, Points and Weight are required.  The SDate, EDate and Description
			components are optional;
	    	*);

		precondition:
	        (*
	         * There is no item in the input Gradesheet with the same Name as the
	         * item to be added.
	         *)
	        (not (exists (gi' in gs) gi'.t = gi.t))

	            and

	        (*
	         * The Title of the given item is not empty.
	         *)
	        (gi.t != nil)

	            and

	        (*
	         * The Type is not empty.
	         *)
	        (gi.par != nil)

	            and

	        (*
	         * The PointsPossible is not empty.
	         *)
	        (gi.pp != nil);

		postcondition:
	        (*
	         * A item is in the output Gradesheet if and only if it is the new
	         * item to be added or it is in the input Gradesheet.
	         *)
	        forall (gi':GradedItem)
	            (gi' in gs') iff ((gi' = gi) or (gi' in gs));

	end AddItem;

	operation EditItem is
	    	inputs: gs:Gradesheet, old_it:GradedItem, new_it:GradedItem;
	    	outputs: gs':Gradesheet;
    
	    	description: (*
	        	Change the given old GradedItem to the given new item.  The old and
	        	new items must not be the same.  The old item must already be in
	        	the input gradesheet.  The new item must meet the same conditions as
			for the input to the AddItem operation. 
	    	*);

		precondition:
        	(*
	         * The old and new graded items are not the same.
        	 *)
        	(old_it != new_it)

	            and

	        (*
	         * The old item is in the given gradesheet.
	         *)
	        (old_it in gs)

	            and
	
        	(*
       		 * There is no graded item in the input gradesheet with the same title as the
       		 * new record to be added.
         	*)
	        (not (exists (new_it' in gs) new_it'.t = new_it.t))

        	    and

     	  	(*
         	 * The Title of the new item is not empty.
         	 *)
     		(new_it.t != nil)

	            and

	        (*
  	         * The point value is not empty.
        	 *)
        	(new_it.pp != nil);

	    postcondition:
     	    (*
             * A graded item is in the output gradesheet if and only if it is the new
	     * item to be added or it is in the input gradesheet, and it is not the old
             * item.
             *)
            (forall (gi':GradedItem)
            	(gi' in gs') iff (((gi' = new_it) or (gi' in gs)) and (gi' != old_it)));

	end EditItem;

	operation DeleteItem is
		inputs: gs:Gradesheet, gi:GradedItem;
	    	outputs: gs':Gradesheet;
    
		description: (*
	        	Delete the given item from the given Gradesheet.  The given item
	        	must already be in the input gradesheet.

		        In addition, delete the item from all StudentInfo objects.
	    	*);
		
		precondition:
        	(*
	         * The given graded item is in the given gradesheet.
        	 *)
        	gi in gs;

	   	postcondition:
	        (*
	         * A graded item is in the output gradesheet if and only if it is not the
	         * existing item to be deleted and it is in the input gradesheet.
	         *)
	        (forall (gi':GradedItem)
        	    (gi' in gs') iff ((gi' != gi) and (gi' in gs)));

	end DeleteItem;
	
	operation AddStudent is
		inputs: gs:Gradesheet, stu:StudentInfo;
		outputs: gs':Gradesheet;
	
		description: (*
	        	Add the given StudentInfo to the Gradesheet.  The information of a
			StudentInfo must not be the same as a student already in the Gradesheet.
			The Name, ID and Polylog are required.
	    	*);
	
		precondition:
	        (*
	         * There is no student in the input Gradesheet with the same Name as the
	         * student to be added.
	         *)
	        (not (exists (stu' in gs) stu'.n = stu.n))

	            and

	        (*
	         * The Name of the given student is not empty.
	         *)
	        (stu.n != nil)

	            and

	        (*
	         * The ID is not empty.
	         *)
	        (gi.i != nil);

		postcondition:
	        (*
	         * A student is in the output Gradesheet if and only if it is the new
	         * student to be added or it is in the input Gradesheet.
	         *)
	        forall (stu':GradedItem)
	            (stu' in gs') iff ((stu' = stu) or (stu' in gs));

	end AddStudent;

	operation EditStudent is
	    	inputs: gs:Gradesheet, old_stu:StudentInfo, new_stu:StudentInfo;
    		outputs: gs':Gradesheet;
    
    		description: (*
        		Change the given old StudentInfo to the given new student.  The old and
        		new students must not be the same.  The old student must already be in
        		the input gradesheet.  The new student must meet the same conditions as
			for the input to the AddStudent operation. 
	    	*);
	end EditStudent;

	operation DeleteStudent is
		inputs: gs:Gradesheet, stu:StudentInfo;
    		outputs: gs':Gradesheet;
    
		description: (*
       		 	Delete the given student from the given Gradesheet.  The given student
       		 	must already be in the input gradesheet.
		*);
	end DeleteStudent;

end Spreadsheet;