<> <> <> <> <> <> <> <<>> DIRECTORY Tioga, TiogaPrivate; EditSpanSupportImpl: CEDAR MONITOR IMPORTS Tioga, TiogaPrivate EXPORTS Tioga, TiogaPrivate = BEGIN OPEN TiogaPrivate, Tioga; World: TYPE ~ TiogaPrivate.World; WorldRep: PUBLIC TYPE ~ TiogaPrivate.WorldRep; Invariant: PROC [predicate: BOOL] ~ INLINE { true: BOOL[TRUE..TRUE] ~ predicate; }; <> freeSlice: Slice; -- free list of slices numFreeSlices: NAT _ 0; maxFreeSlices: NAT = 15; minSliceSize: NAT = 10; GetSlice: PUBLIC ENTRY PROC [len: NAT] RETURNS [Slice] = { prev: Slice _ NIL; FOR slice: Slice _ freeSlice, (prev _ slice).next UNTIL slice=NIL DO IF slice.maxLength>=len THEN { -- take this one IF prev=NIL THEN freeSlice _ slice.next ELSE prev.next _ slice.next; slice.next _ NIL; slice.length _ len; numFreeSlices _ numFreeSlices-1; RETURN [slice]; }; ENDLOOP; RETURN [NEW[SliceArray[MAX[len, minSliceSize]]]]; }; FreeSlice: PUBLIC ENTRY PROC [slice: Slice] = { IF slice=NIL OR slice.maxLength=maxFreeSlices THEN NULL ELSE { FOR i: NAT IN [0..slice.length) DO slice[i] _ NIL ENDLOOP; slice.next _ freeSlice; freeSlice _ slice; numFreeSlices _ numFreeSlices+1; }; }; <> MakeSlices: PROC [node: Node] RETURNS [before, after: Slice _ NIL] = { <<>> <> <> <> <<>> 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] = { <> 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] = { <<>> <> <> <> <<>> 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] = { <<>> <> <<>> 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] = { <<>> <> <> <> <<>> 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 bi0 THEN before[bi-1] ELSE NIL; -- b's parent a: Node ~ IF ai> <> <> <> <<>> 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] }; <<>> <> <> <> <> <> <<>> 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 <<>> <> 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] = { <<>> <> <> <> <<>> 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] = { <> 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]]]; <> 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] = { <<>> <> <> <> <> <> <<>> 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 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] = { <<>> <> 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; }; <> ApplyToSpan: PUBLIC PROC [span: Span, proc: ApplyToSpanProc] = { node, last: Node; start, lastLen: INT; IF (node _ span.start.node) = NIL THEN RETURN; IF (last _ span.end.node) = NIL THEN RETURN; IF (start _ span.start.where)=nodeItself THEN start _ 0; IF span.end.where=nodeItself THEN lastLen _ maxLen ELSE IF span.end.where=maxLen THEN lastLen _ maxLen ELSE { lastLen _ span.end.where+1; IF node=last THEN lastLen _ lastLen-start }; DO IF proc[node, start, IF node=last THEN lastLen ELSE maxLen] THEN RETURN; IF node=last OR (node _ StepForward[node])=NIL THEN RETURN; start _ 0; ENDLOOP; }; BackLoc: PUBLIC PROC [loc: Location] RETURNS [new: Location] = { new.node _ StepBackward[loc.node]; new.where _ IF loc.where=nodeItself THEN nodeItself ELSE Size[new.node]; }; ForwardLoc: PUBLIC PROC [loc: Location] RETURNS [new: Location] = { new.node _ StepForward[loc.node]; new.where _ IF loc.where=nodeItself THEN nodeItself ELSE 0; }; END.