Slice support routines
MakeSlices:
PROC [node: Node]
RETURNS [before, after: Slice ←
NIL] = {
before[0]=root; before[i]=Parent[before[i+1]]; before[before.length-1]=node
after[i]=Next[before[i]]
if node.child # NIL then after[before.length]=node.child
IF node#
NIL
THEN {
Slicer:
PROC [node: Node, height:
NAT]
RETURNS [before, after: Slice, level:
NAT] ~ {
IF node=
NIL
THEN {
-- have gone beyond root
RETURN[GetSlice[height], GetSlice[height+1], 0];
}
ELSE {
[before, after, level] ← Slicer[Parent[node], height+1];
before[level] ← node; after[level] ← Next[node];
RETURN[before, after, level+1];
};
};
[before, after, ] ← Slicer[node, 0];
Invariant[before.length=after.length+1];
after[before.length] ← node.child;
FOR i:
NAT
DECREASING
IN [0..after.length)
DO
-- delete trailing NILs from after
IF after[i]=NIL THEN after.length ← i ELSE EXIT;
ENDLOOP
};
};
MakeParentSlice:
PROC [node: Node]
RETURNS [slice: Slice ←
NIL] = {
result is same as MakeSlices[node].before
Slicer:
PROC [node: Node, height:
NAT]
RETURNS [slice: Slice, level:
NAT] ~ {
IF node=
NIL
THEN {
-- have gone beyond root
RETURN[GetSlice[height], 0];
}
ELSE {
[slice, level] ← Slicer[Parent[node], height+1];
slice[level] ← node;
RETURN[slice, level+1];
};
};
IF node#NIL THEN [slice, ] ← Slicer[node, 0];
};
InsertPrefix:
PROC [first, last: Slice, firstLen:
NAT]
RETURNS [new: Slice] = {
new[i]=first[i] for i in [0..firstLen)
new[i+firstLen]=last[i] for i in [0..last.length)
new.length=firstLen+last.length
Invariant[KindOfSlice[first]=before AND KindOfSlice[last]=before];
Invariant[firstLen>first.length];
new ← GetSlice[firstLen+last.length];
FOR i: NAT IN [0..firstLen) DO new[i] ← first[i]; ENDLOOP;
FOR i: NAT IN [0..last.length) DO new[firstLen+i] ← last[i]; ENDLOOP
};
DeletePrefix:
PUBLIC
PROC [slice: Slice, depth:
NAT] = {
remove entries from start of slice
newLen: NAT ~ slice.length-depth;
FOR i: NAT IN [0..newLen) DO slice[i] ← slice[depth+i]; ENDLOOP;
FOR i: NAT IN [newLen..slice.length) DO slice[i] ← NIL; ENDLOOP;
slice.length ← newLen;
};
NeedNestingChange:
PUBLIC
PROC [before, after, top, bottom: Slice, nesting:
INTEGER, depth:
NAT]
RETURNS [NeededNestingChange] = {
bandStart, afterOver: INTEGER;
topLen, botLen: NAT;
nesting ← MIN[1,nesting];
topLen ← top.length; botLen ← bottom.length;
bandStart ← before.length+nesting-(topLen-depth);
IF bandStart <= 0 THEN RETURN [needNest]; -- must be at least 1
afterOver ← after.length-(botLen-depth+bandStart);
IF afterOver > 1 THEN RETURN [needUnNest];
RETURN [ok]
};
Splice:
PUBLIC
PROC [before, after: Slice, beforeStart, afterStart:
NAT ← 0] = {
join slices
make after[afterStart+i] be successor of before[beforeStart+i]
if more after's than before's, adopt as children of last before
beforeLen: NAT ~ before.length-beforeStart;
afterLen: NAT ~ after.length-afterStart;
Invariant[KindOfSlice[before]=before AND KindOfSlice[after]=after];
Invariant[afterLen<=beforeLen+1];
FOR i:
NAT
DECREASING
IN [0..beforeLen]
DO
bi: NAT ~ i+beforeStart;
ai: NAT ~ i+afterStart;
b: Node ~ IF bi<before.length THEN before[bi] ELSE NIL;
p: Node ~ IF bi>0 THEN before[bi-1] ELSE NIL; -- b's parent
a: Node ~
IF ai<after.length
THEN after[ai]
ELSE
NIL;
-- b's successor
IF b=
NIL
THEN {
-- adopt children
IF p=
NIL
THEN {
IF a#NIL THEN ERROR; -- orphans!
}
ELSE {
p.child ← a;
IF a#NIL THEN LastSibling[a].next ← p;
};
}
ELSE {
-- link successor
IF a=
NIL
THEN {
-- no successor
b.next ← p; b.last ← TRUE;
}
ELSE {
-- has successor
IF a=b THEN RETURN;
b.next ← a; b.last ← FALSE;
LastSibling[a].next ← p;
};
};
ENDLOOP;
};
ReplaceBand:
PUBLIC
PROC [before, after, top, bottom: Slice, nesting:
INTEGER] = {
do Splices to insert (top..bottom) between (before..after)
nesting tells how to offset last of before vs. last of top
before[before.length-1+nesting] will be predecessor of top[top.length-1]
depth: NAT ~ MAX[1, before.length+MIN[nesting, 1]-top.length];
fullBottom: Slice ~ InsertPrefix[before, bottom, depth];
Splice[fullBottom, after];
Splice[before, top, depth];
FreeSlice[fullBottom]
};
BadBand:
PUBLIC
ERROR =
CODE;
DescribeBand:
PUBLIC
PROC [first, last: Node]
RETURNS [before, after, top, bottom: Slice ←
NIL, nesting:
INTEGER, depth:
NAT] = {
ENABLE UNWIND => { FreeSlice[before]; FreeSlice[after]; FreeSlice[top]; FreeSlice[bottom] };
top[top.length-1] = first
before[before.length-1+nesting] = predecessor of first
bottom[bottom.length-1] = last
raises BadBand error if last doesn't follow first in tree structure
or if first or last is root node
pred: Node ← StepBackward[first];
minDepth: NAT;
IF pred=NIL THEN ERROR BadBand; -- first is root node
IF pred=last THEN ERROR BadBand; -- this actually happened during testing!
[before, top] ← MakeSlices[pred];
nesting ← top.length-before.length; -- nesting of LastOfSlice[top] wrt LastOfSlice[before]
[bottom, after] ← MakeSlices[last];
minDepth ← MIN[before.length, bottom.length];
FOR depth ← 0, depth+1
UNTIL depth >= minDepth
DO
IF before[depth] # bottom[depth]
THEN {
-- check for legality
bot: Node ← bottom[depth];
FOR node: Node ← before[depth], Next[node]
DO
IF node=bot THEN EXIT;
IF node=NIL THEN ERROR BadBand; -- last must come before first
ENDLOOP;
EXIT;
};
ENDLOOP;
IF depth=0 THEN ERROR BadBand; -- different root nodes for first and last
check assertions
Invariant[LastOfSlice[top]=first AND LastOfSlice[bottom]=last];
Invariant[before[before.length+nesting-2]=Parent[first]];
};
DestSlices:
PUBLIC
PROC [dest: Node, where: Place]
RETURNS [before, after: Slice, nesting:
INTEGER] = {
where = after means insert starting as sibling after dest
where = child means insert starting as child of dest
where = before means insert starting as sibling before dest
SELECT where
FROM
after => { [before, after] ← MakeSlices[dest]; nesting ← 0 };
child => { [before, after] ← MakeSlices[dest]; nesting ← 1 };
before => {
pred: Node ← StepBackward[dest];
[before, after] ← MakeSlices[pred];
nesting ← after.length-before.length;
};
ENDCASE => ERROR;
};
CreateDest:
PUBLIC
PROC [depth:
NAT]
RETURNS [dest: Location] = {
create tree of parents
node: Node ← NIL;
THROUGH [0..depth)
DO
child: Node ~ NewNode[];
IF node#NIL THEN { node.child ← child; child.next ← node; child.last ← TRUE; };
node ← child;
ENDLOOP;
RETURN [[node, nodeItself]];
};
CopySpan:
PUBLIC
PROC [span: Span]
RETURNS [result: Span] = {
node, prev, parent, first: Node ← NIL;
IF (node ← span.start.node)=NIL THEN RETURN [nullSpan];
parent ← NewNode[]; -- parent for the span
DO
-- create new node each time through the loop
new: Node ~ NEW[NodeBody];
new.new ← TRUE;
new.rope ← node.rope;
new.runs ← node.runs;
Inherit[n: new, from: node, allprops: TRUE]; -- inherit properties from node
IF prev=NIL THEN parent.child ← new
ELSE { prev.last ← FALSE; prev.next ← new }; -- insert new
new.last ← TRUE; new.next ← parent;
IF node=span.start.node THEN first ← new;
IF node=span.end.node THEN RETURN [[[first, span.start.where], [new, span.end.where]]];
go to next node
prev ← new;
IF node.child#
NIL
THEN {
-- descend in the tree
node ← node.child; parent ← new; prev ← NIL;
}
ELSE
DO
-- move to next node, sibling or up* then sibling
IF node.last
THEN {
-- move up to node's parent
node ← node.next; -- node ← node.parent
IF node=NIL THEN RETURN [nullSpan]; -- bad arg span
Invariant[parent.last];
prev ← parent; -- next new node will be parent's sibling
parent ← parent.next; -- parent ← parent.parent
IF parent=
NIL
THEN {
-- need a new parent
parent ← NewNode[];
parent.child ← prev;
prev.next ← parent;
};
}
ELSE { node ← node.next; EXIT }; -- move to next sibling
ENDLOOP;
ENDLOOP;
};
CompareSliceOrder:
PUBLIC
PROC [s1, s2: Slice]
RETURNS [order: Order] = {
determines relative order in tree of last nodes in the slices
returns "same" if slices are identical
returns "before" if last node of s1 comes before last node of s2
returns "after" if last node of s1 comes after last node of s2
returns "disjoint" if slices are not from the same tree
IF s1=NIL OR s2=NIL OR s1.length=0 OR s2.length=0 THEN RETURN [disjoint];
Invariant[KindOfSlice[s1]=before AND KindOfSlice[s2]=before]; -- only valid for parent slices
IF s1[0]#s2[0] THEN RETURN [disjoint]; -- different roots
FOR i:
NAT
IN[1..
MIN[s1.length, s2.length])
DO
n1: Node ~ s1[i];
n2: Node ~ s2[i];
IF n1#n2
THEN {
-- they are siblings, so can check order by Next's
FOR n: Node ← Next[n1], Next[n]
DO
-- search from s1 to s2
IF n=n2 THEN RETURN [before]; -- n1 comes before n2
IF n=NIL THEN RETURN [after]; -- n2 not found, so n1 must be after n2
ENDLOOP;
};
ENDLOOP;
SELECT s1.length
FROM
<s2.length => RETURN [before]; -- s1Last is a parent of s2Last
=s2.length => RETURN [same]; -- s1Last=s2Last
>s2.length => RETURN [after]; -- s2Last is a parent of s1Last
ENDCASE => ERROR;
};
CompareNodeOrder:
PUBLIC
PROC [node1, node2: Node]
RETURNS [Order] = {
IF node1=NIL OR node2=NIL THEN RETURN [disjoint];
IF node1=node2 THEN RETURN [same]
ELSE {
s1: Slice ~ MakeParentSlice[node1];
s2: Slice ~ MakeParentSlice[node2];
order: Order ~ CompareSliceOrder[s1, s2];
FreeSlice[s1];
FreeSlice[s2];
RETURN[order];
};
};
DoSplits:
PUBLIC
PROC [world: World, alpha, beta: Span]
RETURNS [Span, Span] = {
split off head or tail sections of text
MakeSplit:
PROC [split: Location] ~ {
IF split.node#
NIL
AND split.where#nodeItself
THEN {
new: Node ~ Split[world, Root[split.node], split];
FixLoc:
PROC [old: Location]
RETURNS [Location] ~ {
IF old.node=split.node
THEN {
Invariant[old.where#nodeItself];
IF old.where>=split.where THEN RETURN [[new, old.where-split.where]];
};
RETURN[old];
};
alpha.start ← FixLoc[alpha.start];
alpha.end ← FixLoc[alpha.end];
beta.start ← FixLoc[beta.start];
beta.end ← FixLoc[beta.end]
};
};
IF alpha.start.where#nodeItself THEN MakeSplit[alpha.start];
IF beta.start.where#nodeItself THEN MakeSplit[beta.start];
IF alpha.end.where#nodeItself THEN MakeSplit[alpha.end];
IF beta.end.where#nodeItself THEN MakeSplit[beta.end];
RETURN [alpha, beta]
};
DoSplits2:
PUBLIC
PROC [world: World, dest: Location, source: Span, where: Place, nesting:
INTEGER]
RETURNS [Location, Span, Place,
INTEGER] = {
destLoc: Location;
destSpan: Span ← [dest, nullLocation];
[destSpan, source] ← DoSplits[world, destSpan, source];
destLoc ← destSpan.start;
IF dest.where # nodeItself
THEN {
-- did a split
destLoc ← BackLoc[destLoc]; where ← after; nesting ← 0;
};
RETURN [destLoc, source, where, nesting]
};
ReMerge:
PUBLIC
PROC [world: World, alpha, beta: Span, merge: Node, tail:
BOOL ←
FALSE]
RETURNS [Span, Span] = {
IF tail THEN merge ← StepForward[merge];
IF merge#
NIL
THEN {
loc: Location ~ Merge[world, Root[merge], merge];
FixLoc:
PROC [old: Location]
RETURNS [Location] = {
IF old.node=merge
THEN {
Invariant[old.where#nodeItself];
RETURN [[loc.node, loc.where+old.where]];
};
RETURN[old];
};
alpha.start ← FixLoc[alpha.start];
alpha.end ← FixLoc[alpha.end];
beta.start ← FixLoc[beta.start];
beta.end ← FixLoc[beta.end];
};
RETURN [alpha, beta]
};
UndoSplits:
PUBLIC
PROC [world: World, alpha, beta: Span]
RETURNS [Span, Span] = {
IF alpha.start.where#nodeItself
THEN
[alpha, beta] ← ReMerge[world, alpha, beta, alpha.start.node];
IF beta.start.where#nodeItself
THEN
[alpha, beta] ← ReMerge[world, alpha, beta, beta.start.node];
IF alpha.end.where#nodeItself
THEN
[alpha, beta] ← ReMerge[world, alpha, beta, alpha.end.node, TRUE];
IF beta.end.where#nodeItself
THEN
[alpha, beta] ← ReMerge[world, alpha, beta, beta.end.node, TRUE];
RETURN [alpha, beta];
};
UndoSplits2:
PUBLIC
PROC [world: World, dest: Location, source: Span]
RETURNS [Location, Span] = {
destSpan: Span ← [dest, nullLocation];
[destSpan, source] ← UndoSplits[world, destSpan, source];
RETURN [destSpan.end, source];
};
SliceOrder:
PUBLIC
PROC [alpha, beta: Span, aBefore, aBottom, bBefore, bBottom: Slice]
RETURNS [overlap:
BOOL, head, tail: Span, startOrder, endOrder: Order] = {
IF CompareSliceOrder[aBottom, bBefore]#after -- alphaend before betastart
OR CompareSliceOrder[aBefore, bBottom]#before -- alphastart after betaend
THEN { overlap ← FALSE; RETURN };
startOrder ← CompareSliceOrder[aBefore, bBefore];
endOrder ← CompareSliceOrder[aBottom, bBottom];
head ←
SELECT startOrder
FROM
before => [alpha.start, BackLoc[beta.start]],
same => nullSpan,
after => [beta.start, BackLoc[alpha.start]],
ENDCASE => ERROR;
tail ←
SELECT endOrder
FROM
before => [ForwardLoc[alpha.end], beta.end],
same => nullSpan,
after => [ForwardLoc[beta.end], alpha.end],
ENDCASE => ERROR;
overlap ← TRUE;
};