module undoredo
open std/ord
/*******************************************************/
/*Description of Editor - modelling of Eclipse Text Editor, Visual Studio, MS word, GVIM, VIM, MAC, etc except EMacs*/
/*
1. When the editor is opened, document change operations (keystrokes (typings), delete, cut, copy, paste operations)
 are available.
2. Only after a document changes, the undo operation is effective. 
3. Only when there's some redoable history (i.e the history of "undo"es), the redo operations is effective. 
3. The editor keeps track of an infinite size of an editing history. 
	(In other words, multiple undo /redo operations are allowed.)
4. The state of editor at any given point is described with 
	4.1 document = the state of document inside the editor
	4.2 clipboard = the document buffered in the clipboard
	4.3 selection = selected text
	4.4 pointer = the current position inside the editing history (i.e cur_pos) 
	4.5 editing history = history which maintains the state of document and selection in the past
5. The undo operations restore the selected region and document.
6. The editing history is structured as a doubly-linked list.
	6.1. "undo" operation makes the cur_pos to move one step backward inside the doubly linked list.
	6.2. "redo" operation makes the cur_pos to proceed one step forward inside the doubly linked list.
	6.3. Other operations add the current state of document and selection at the (cur_pos) of the list,
 and make the cur_pos to proceed one step forward. 
 
* Scenario *
	s1		s2		s3		s4
	      1:typing	->	2:cut	-> 	3:paste ->	
	       		<-      5:undo  <-      4:undo <-
			->      6:redo  ->      7:redo ->
			<-	9:undo	<-      8:undo <-
*/   			
sig Text {
}

sig Idx {
}  

/*******************************************************/
/* The state kept by the editor and editing functions  */

sig EditorState{
	// document associated with the editor
	document: set Text,
	// clipboard
	clipboard: option Text,
	// selection 
	selection: option Text,
	// current position inside the history list 
	cur_pos_history: Idx,
	// editing history
	undostack: EditingHistory
}{
	#(cur_pos_history) =1
	#(undostack) = 1
	selection in document
}
fact posLEQlength {
	// current position in the editing history is always less than or equal to the length of the editing history
	all p:EditorState |
		! (#OrdPrevs(p.cur_pos_history) > #OrdPrevs(p.undostack.length)) 
}
fact {
	all p,q: EditorState |
		p.document = q.document  && p.clipboard = q.clipboard && p.selection = q.selection && p.cur_pos_history = q.cur_pos_history 
		&& p.undostack = q.undostack  <=> p = q 
}
/*********************************************************************/
/*		Functions on EditorState	*/
// this function is used to compare the stae of document and selection 
fun same_document_selection(es1,es2:EditorState) {
	es1.document= es2.document
	es1.selection = es2.selection
}
// resets the selection, cur_pos_history, undostack, clipboard
fun init(es:EditorState) {
	// out.document has some Text 
	es.selection = none[Text] 
	es.clipboard = none[Text]
	es.cur_pos_history = Ord[Idx].first
	es.undostack.length = (Ord[Idx].first)
}
// run init for 5

// typing adds the document state into undostack, and resets the selection  
fun EditorState::typings (t:Text, out :EditorState) { 
	// store current document and selection into undostack
	some ds: DocumentState | (ds.document=this.document && ds.selection = this.selection) 
	&& (this.undostack)..insertAndEmptyRedoes(ds,this.cur_pos_history,out.undostack) 
	// t is added to document 
	&& out.document = this.document + t 
	//clipboard is the same
	&& out.clipboard = this.clipboard  
	//selection is reset
	&& out.selection = none[Text]
	// cur_pos increases 
	&& out.cur_pos_history = OrdNext(this.cur_pos_history) 
}
// typings either make the size of history to increase by 1 or discard outstanding redoable items after the current_position
assert typingseffect {
	all p,q:EditorState | all t:Text|
		p..typings(t,q) => (
		OrdPrev(q.undostack.length) = OrdPrev(p.undostack.length) + p.undostack.length ) ||
		(OrdPrev(q.undostack.length) = OrdPrev(q.cur_pos_history))
}
//check typingseffect for 10

// select does not add the document state into undo stack
fun EditorState::select ( out:EditorState) {
	out.document = this.document
	out.clipboard = this.clipboard
	some t:Text | out.selection = t
	out.cur_pos_history = this.cur_pos_history
	out.undostack = this.undostack
}
// copy does not add the document state into undo stack. (because it does not change the document..) 
fun EditorState::copy (out: EditorState) {
	out.document = this.document
	out.clipboard = if some this.selection then this.selection else this.clipboard
	out.selection = this.selection
	out.cur_pos_history = this.cur_pos_history
	out.undostack = this.undostack
}
// cut is only activated when there's selection. 	
fun EditorState::cut (out:EditorState) {
 	no this.selection => out = this,
	(
		//store current document and selection into undostack
		some ds: DocumentState | (ds.document=this.document && ds.selection = this.selection)
		&& (this.undostack)..insertAndEmptyRedoes(ds,this.cur_pos_history,out.undostack)
		// clipboard becomes current selection
		&& out.clipboard = this.selection
		// delete the selection from the current document		
		&& out.document = this.document - this.selection
		// selection is reset
		&& out.selection = none[Text]
		// cur_pos increases
		&& out.cur_pos_history = OrdNext(this.cur_pos_history) 
	)
}
// cuttings either make the size of history to increase by 1 or discard outstanding redoable items after the current_position
assert cuteffect {
	all p,q:EditorState | all t:Text|
		p..typings(t,q) => (
		OrdPrev(q.undostack.length) = OrdPrev(p.undostack.length) + p.undostack.length ) ||
		(OrdPrev(q.undostack.length) = OrdPrev(q.cur_pos_history))
}
// check cuteffect for 10

// delete is only activated when there's selection 
fun EditorState::delete( out:EditorState) {
	no this.selection => out = this, 
	(
		//store current document and selection into undostack
		some ds: DocumentState | (ds.document = this.document && ds.selection = this.selection) 
		&& (this.undostack)..insertAndEmptyRedoes(ds,this.cur_pos_history,out.undostack)
		// clipboard stays the same
		&& out.clipboard = this.clipboard
		// delete the selection from the current document
		&& out.document = this.document - this.selection
		// selection is reset
		&& out.selection = none[Text]
		// cur_pos increases
		&& out.cur_pos_history = OrdNext(this.cur_pos_history)
	)
}

// paste is only activated when there's something on the clipboard 
fun EditorState::paste (out:EditorState) {
	no this.clipboard => out = this, 
	(
		//store current document and selection into undostack
		some ds: DocumentState | (ds.document= this.document && ds.selection = this.selection) 
		&& (this.undostack)..insertAndEmptyRedoes(ds,this.cur_pos_history,out.undostack) 
		// clipboard stays the same
		&& out.clipboard = this.clipboard
		// add the clipboard content to the document
		&& out.document = this.document + this.clipboard
		// selection is reset
		&& out.selection = none[Text]
		// cur_pos increases
		&& out.cur_pos_history = OrdNext(this.cur_pos_history)
	)
}

// undo is only activated when there's something to undo, which means that the cur_pos of the edit history > 0
// undo reads the document state of the current position and restores that into the editor.  
// clipboard stays the same and undostack stays the same, only the cur_pos_history changes.
fun EditorState::undo(out:EditorState) { 
	(#OrdPrevs(this.cur_pos_history) > 0) => 
	( 
		some ds: DocumentState | (ds = (this.undostack)..stateAt(OrdPrev(this.cur_pos_history))) 
		//restore the previous state and selection from the undostack
		&& out.document = ds.document
		&& out.selection = ds.selection
		// clipboard stays the same
		&& out.clipboard = this.clipboard
		// cur_pos decreases
		&& out.cur_pos_history = OrdPrev(this.cur_pos_history)
		// undostack stays the same
		&& out.undostack = this.undostack
	), (out = this)
}
assert undoeffects {
	all p,q:EditorState | 
		p..undo(q) => p.undostack.length = q.undostack.length && 
			( 
				p.cur_pos_history = Ord[Idx].first || 
				#OrdPrevs(q.cur_pos_history) <#OrdPrevs(p.cur_pos_history) 
			)
			&& p.undostack = q.undostack
}
// check undoeffects for 10
// redo is only activated when there's some undo history previously, which means that the cur_pos_history < length -1
fun EditorState::redo(out:EditorState) {
	// cur_pos_history <length
	 #OrdPrevs(this.cur_pos_history) < #OrdPrevs((this.undostack).length) => 
	(
		// progress inside undo stack 
		some ds: DocumentState | ds=(this.undostack)..stateAt(OrdNext(this.cur_pos_history))
		// restore the state 
		&& out.document = ds.document
		&& out.selection = ds.selection
		// clipboard stays the same
		&& out.clipboard = this.clipboard
		// cur_pos increases
		&& out.cur_pos_history = OrdNext(this.cur_pos_history)
		// undostack stays the same 
		&& out.undostack = this.undostack
	), (out = this)
}
assert redoeffects {
	all p,q:EditorState |
		p..redo(q) => p.undostack.length = q.undostack.length && 
		(
			p.cur_pos_history = p.undostack.length ||
			#OrdPrevs(q.cur_pos_history) > #OrdPrevs(p.cur_pos_history)
		)
		&& p.undostack = q.undostack
	
}
// check redoeffects for 10
/****************************************************************************/
/*Assert statement */
//after typing and undoing, it returns to the document state before typing
assert type_undo {
	all p,q,r:EditorState | all t:Text |
		p..typings(t,q) && q..undo(r) => same_document_selection(p,r) 
}
check type_undo for 10
//after typing and undoing and redoing, it returns to the document state before undoing 
assert type_undo_redo_same {
	all k,p,q,r:EditorState | all t:Text | 
	k..typings(t,p)&& p..undo(q) && q..redo(r) => same_document_selection (p,r)
}
check type_undo_redo_same for 5
//right after initializing (open, load..), undo does not change the document 
assert cannot_undo_after_init {
	all p,q: EditorState | 
	init(p) && p..undo(q) => same_document_selection(p,q)
}
//right after initializing (open, load..) redo does not change the document 
assert cannot_redo_after_init{
	all p,q: EditorState |
	init(p) && p..redo(q) => same_document_selection(p,q) 
}

/*
	p1	->typings->	p2	->typings->	p3
	p5	<-undo<-	p4	<-undo	<-	
		->redo->	p6	->redo->	p7
	(p1=p5), (p2=p4=p6), (p3=p7) 
*/
assert two_undo_two_redo {
	all p1,p2,p3,p4,p5,p6,p7: EditorState | all t1,t2:Text |
	p1..typings(t1,p2) && p2..typings(t2,p3) && p3..undo(p4) && p4..undo(p5) && p5..redo(p6) && p6..redo(p7) 
	=> 
	same_document_selection (p1,p5)
	&& same_document_selection (p2,p4) 
	&& same_document_selection (p4,p6)
	&& same_document_selection (p7,p3)
}

check cannot_undo_after_init for 5
check cannot_redo_after_init for 5
check two_undo_two_redo for 5
/*
	p1	->typings->	p2	->typings->	p3
	p5	<-undo<-	p4	<-undo	<-	
		->typing->	p6	->redo(invalid)->p7
	(p1=p5),(p2=p4),(p2!=p6),(p6=p7)
*/
//once a document changes by (cut/copy/delete/type/paste) after redo, additional redoes cannot be performed.
assert two_undo_type_redo{
	all p1,p2,p3,p4,p5,p6,p7: EditorState | all t1,t2:Text |
	p1..typings(t1,p2) && p2..typings(t2,p3) && p3..undo(p4) && p4..undo(p5) && p5..typings(t1,p6) && p6..redo(p7) 
	=> 
	same_document_selection (p1,p5)
	&& same_document_selection (p2,p4) 
	&& !(same_document_selection (p2,p6))
	&& same_document_selection (p6,p7)
}
check two_undo_type_redo for 7
/*
	p1	->cut	->	p2	->typings->	p3
	p5	<-undo<-	p4	<-undo	<-	
		->paste	->	p6	
	(p1=p5),(p2=p4),(p2!=p6),(p5!=p6)
*/
//undo and redo does not affect the content inside the clipboard.
assert undo_clipboard {
	all p0,p1,p2,p3,p4,p5,p6,p7: EditorState | all t1,t2:Text |
	p0..select(p1) && p1..cut(p2) && p2..typings(t2,p3) 
	&& p3..undo(p4) && p4..undo(p5) && p5..paste(p6) 
	=> 
	same_document_selection (p1,p5)
	&& same_document_selection (p2,p4) 
	&& !(same_document_selection (p2,p6))
	&& !(same_document_selection (p5,p6))
}
check undo_clipboard for 10

/********************************************************/
/*   		Document State (restorable data) 	*/
sig DocumentState {
	document: set Text,
	selection: option Text
}{
	selection in document
}
fact {	all p,q: DocumentState | p.document = q.document && p.selection = q.selection <=> p = q }

/********************************************************/
/*		 Functions on EditingHistory		*/
/*	EditingHistory is implemented as an arraylist	*/
/*	stateAt(pos): get the state at the (pos)th	*/
/*	append(state): append the state at the end of list. */
/*	insertAndEmptyRedoes(state,pos): put the state at the (pos)th 
/*		and remove everything after (pos) th 	*/

sig EditingHistory {
	// length is the size of an array.
	// getState is a mapping from index to documentstate.
	getState: Idx -> ? DocumentState,
	length: Idx
}{
	// the constraints below force one to one mapping from Idx to DocumentState for each 0=<Idx<length
	(OrdNexts(length)+length).(getState) = none [DocumentState]
	OrdPrevs(length) = (getState).DocumentState
	#(length) = 1
}

fact {	all p,q:EditingHistory | p.getState = q.getState && p.length = q.length <=> p = q}

// access function inside editinghistory. if pos is invalid inside the editing history, it returns empty set
fun EditingHistory::stateAt (pos:Idx) : option DocumentState {
	result = pos.(this.getState)
}
// append the state at the end of the editing history
// always possible to append
fun EditingHistory::append(state:DocumentState, out: EditingHistory ){
	// all items before the length stay the same
	all i:Idx | i in (OrdPrevs(this.length)) => out..stateAt(i) = this..stateAt(i)
	//increase the length of history
	out.length = OrdNext(this.length)
	//store the given state in the last slot
	out.getState= this.getState + (this.length)->state	
}
assert appendlength {
	all p,q:EditingHistory,s: DocumentState| p..append(s,q) => 
		#OrdPrevs(q.length) = #OrdPrevs(p.length) + 1  
		&& q..stateAt(p.length) = s 
}
check appendlength for 10
// remove all items from pos and overwrite state on the (pos)th position
fun EditingHistory::insertAndEmptyRedoes (state:DocumentState, pos:Idx, out:EditingHistory) {
	// all items before (not including) the pos stay the same
	all i:Idx | i in OrdPrevs(pos) => out..stateAt(i) = this..stateAt(i)
	// put state at (pos)th position
	out..stateAt(pos) = state
	// all items after (not including) the pos gets removed
	out.getState = this.getState - (OrdNexts(pos) -> DocumentState) 
	// length becomes pos+1 
	out.length = OrdNext(pos)
}	
run insertAndEmptyRedoes for 10
assert cleaningundo {
	all p,q:EditingHistory,s:DocumentState,pos:Idx | p..insertAndEmptyRedoes(s,pos,q) =>
		q.length = OrdNext(pos) &&
		q..stateAt(OrdNext(pos)) = none[DocumentState] &&
		q..stateAt(OrdPrev(pos)) = p..stateAt(OrdPrev(pos))
}
check cleaningundo for 10

/********************************************************/
fun nullDocumentState (state:DocumentState) {
	state.selection = none [Text]
	state.document = none[Text]
}
/*******************************************************************************/
//test function 
fun EditingHistoryTest () {
	EditingHistory = univ[EditingHistory]
}
fun DocumentStateTest() {
	DocumentState = univ[DocumentState]
}
run EditingHistoryTest for 10 but 7 Idx 
run DocumentStateTest for 10 but 7 Idx
assert numLEQlength {
	all p:EditorState | ! (#(p.undostack.getState) > #OrdPrevs(p.undostack.length))
}
check numLEQlength for 5