(****
 *
 * QuestionBank.rsl
 * By: Tyson Tate
 *
 * The QuestionBank module defines objects and methods related to the Question Bank window. This
 * includes adding, editing, viewing, duplicating, removing, and browsing questions. Synchronizing
 * questions with the server is an important operation for this module.
 *
 * NOTE: Not completed. Needs more work, specifically in the add, edit, and delete operations.
 *)

module QuestionBank;

	from Question import all;
	export all;

	object Bank is
		components: questions:FullQuestion*;
		description: (*
			A collection of FullQuestion objects representing a library of avialable questions that
			can be added to, deleted from, edited, and synchronized with a server.
		*);
	end Bank;

	operation addQuestion is
		inputs: q:FullQuestion and bank:Bank and validUsers:ValidUsers
			and systemDateTime:SystemDateTime;
		outputs: bank':Bank;
		precondition:
			(* The new question must be valid. *)
			(IsValidQuestion(q, validUsers))

			and

			(* The date added must be the system's date and time that this question was added. Also,
			the date last used and date last modified must be nil because they can't possibly have
			been used or modified yet, because we have just added this question*)

			(q.dateAdded = systemDateTime) and (q.dateModified = nil) and (q.dateLastUsed = nil);
		postcondition:
			(* All the questions in the new bank must have existed in the old bank or must be the
			new question. *)
			forall (q':FullQuestion)
				(q' in bank') iff ((q' in bank) or (q' = q));
		description: (*
			Takes in a QuestionBank and a FullQuestion and adds the supplied FullQuestion to the
			QuestionBank, outputting the resulting QuestionBank.
		*);
	end addQuestion;

	function IsValidQuestion(q:FullQuestion, validUsers:ValidUsers)-> boolean = (
		(* The required information must be filled in *)
		(q.class != nil and q.keywords!= nil and q.difficulty != nil
			and q.timeToComplete!= nil and q.owner != nil)

		and

		(* Difficulty number must be in the correct range (1 to 10, inclusive) *)
		(q.difficulty < 11) and (q.difficulty > 0)

		and

		(* Owner must be a valid user as recognized by the Grader Tool.*)
		(exists (owner':User) ((owner' = q.owner) and (owner' in validUsers)))
	);

	object SystemDateTime is Date
		description: (*
			This object represents the computer system's current date and time as a Date object.
		*);
	end systemDateTime;

	object ValidUsers is
		components: User*;
		description: (*
			A list of the valid users on a system.
		*);
	end ValidUsers;

	operation changeQuestion is
		inputs: bank:Bank and q_old:FullQuestion and q_new:FullQuestion and validUsers:ValidUsers
			and systemDateTime:SystemDateTime;
		outputs: bank':Bank;
		precondition:
			(* We know this question is valid based on the preconditions that exist or will exist
			in the other operations leading up to the ability to edit a question. *)

			(* The question being replaced must exist in the bank. *)
			(q_old in bank)

			and

			(* The question being replaced must not be the same as the one replacing it. *)
			(q_new != q_old)

			and

			(* The non-user-changeable information (aside from the date modified) must not have
			been changed. *)
			(q_old.dateAdded = q_new.dateAdded) and (q_old.dateLastUsed = q_new.dateLastUsed)
				and (q_old.id = q_new.id)

			and

			(* The date modified must be the current system time. *)
			(q_new.dateModified = systemDateTime)

			and

			(* The new question must be valid. *)
			IsValidQuestion(q_new, validUsers);
		postcondition:
			(* All the questions in the new bank must have existed in the old bank or must be the
			new question. *)
			forall (q':FullQuestion)
				(q' in bank') iff ((q' in bank) or (q' = q_new))

			and

			(* The old question does not exist in the new bank. *)

			(not (q_old in bank'));
		 description: (*
			Takes in a FullQuestion, lets the user edit it, and then returns the changed
			FullQuestion.
		 *);
	end editQuestion;

	operation viewQuestion is
		inputs: q:FullQuestion;
		description: (*
			Displays the supplied FullQuestion in a non-editable window.
		*);
	end viewQuestion;

	operation deleteQuestion is
		inputs: bank:Bank and q:FullQuestion;
		outputs: bank':Bank;
		precondition:
			(* The given question is in the bank. *)
			q in bank;
		postcondition:
			(* All the questions in the bank are not the one we just deleted nd is in the input
			question bank. *)
			(forall (q':FullQuestion)
				(q' in bank') iff ((q' != q) and (q' in bank)));
		description: (*
			Removes a FullQuestion object from a Bank object.
		*);
	end addQuestion;

	operation duplicateQuestion is
		inputs: bank:Bank and id:FullQuestion.ID;
		outputs: bank':Bank;
		description: (*
			Makes a new copy of the FullQuestion in the supplied Bank with the supplied ID number
			and changes the Owner, if necessary, to the current user's username and returns the
			Bank with the duplicated question added.
		*);
	end duplicateQuestion;

	operation synchronizeWithServer is
		inputs: bank:Bank and serverAddress:string;
		outputs: bank':Bank;
		description: (*
			Synchronizes the supplied Bank with the central server, which is choses in the Test
			Tool's preferences. Only the questions that the user wants synchronized are
			synchronized.
		*);
	end synchronizeWithServer;
end QuestionBank;