clean up line_gap.sml (removed debug editing)
This commit is contained in:
533
src/line_gap.sml
533
src/line_gap.sml
@@ -41,94 +41,6 @@ struct
|
|||||||
, rightLines: int vector list
|
, rightLines: int vector list
|
||||||
}
|
}
|
||||||
|
|
||||||
fun lineBreaksToString vec =
|
|
||||||
(Vector.foldr (fn (el, acc) => Int.toString el ^ ", " ^ acc) "" vec) ^ "\n"
|
|
||||||
|
|
||||||
fun checkLineBreaks (v1, v2) =
|
|
||||||
if v1 = v2 then
|
|
||||||
()
|
|
||||||
else
|
|
||||||
let
|
|
||||||
val _ = print ("broken: " ^ (lineBreaksToString v1))
|
|
||||||
val _ = print ("fixed: " ^ (lineBreaksToString v2))
|
|
||||||
in
|
|
||||||
()
|
|
||||||
end
|
|
||||||
|
|
||||||
fun checkLineBreaksWithString (dir, str, lines) =
|
|
||||||
if countLineBreaks str <> lines then
|
|
||||||
let
|
|
||||||
val _ = print (dir ^ "\n")
|
|
||||||
val _ = print ("broken: " ^ lineBreaksToString lines)
|
|
||||||
val _ = print ("fixed: " ^ (lineBreaksToString (countLineBreaks str)))
|
|
||||||
val _ = raise Size
|
|
||||||
in
|
|
||||||
()
|
|
||||||
end
|
|
||||||
else
|
|
||||||
()
|
|
||||||
|
|
||||||
fun verifyReturn (buffer: t) =
|
|
||||||
let
|
|
||||||
val _ =
|
|
||||||
case (#leftStrings buffer, #leftLines buffer) of
|
|
||||||
(sHd :: _, lHd :: _) =>
|
|
||||||
let val _ = checkLineBreaksWithString ("left", sHd, lHd)
|
|
||||||
in ()
|
|
||||||
end
|
|
||||||
| (_, _) => ()
|
|
||||||
|
|
||||||
val _ =
|
|
||||||
case (#rightStrings buffer, #rightLines buffer) of
|
|
||||||
(sHd :: _, lHd :: _) =>
|
|
||||||
let val _ = checkLineBreaksWithString ("right", sHd, lHd)
|
|
||||||
in ()
|
|
||||||
end
|
|
||||||
| (_, _) => ()
|
|
||||||
|
|
||||||
in
|
|
||||||
buffer
|
|
||||||
end
|
|
||||||
|
|
||||||
|
|
||||||
local
|
|
||||||
fun goToStart (leftStrings, leftLines, accStrings, accLines) =
|
|
||||||
case (leftStrings, leftLines) of
|
|
||||||
(lsHd :: lsTl, llHd :: llTl) =>
|
|
||||||
goToStart (lsTl, llTl, lsHd :: accStrings, llHd :: accLines)
|
|
||||||
| (_, _) => (accStrings, accLines)
|
|
||||||
|
|
||||||
fun verifyLineList (strings, lines) =
|
|
||||||
case (strings, lines) of
|
|
||||||
(strHd :: strTl, lHd :: lTl) =>
|
|
||||||
let
|
|
||||||
val checkLines = countLineBreaks strHd
|
|
||||||
in
|
|
||||||
if checkLines = lHd then
|
|
||||||
verifyLineList (strTl, lTl)
|
|
||||||
else
|
|
||||||
let
|
|
||||||
val _ = print "line metadata is incorrect\n"
|
|
||||||
val _ = checkLineBreaks (lHd, checkLines)
|
|
||||||
in
|
|
||||||
raise Empty
|
|
||||||
end
|
|
||||||
end
|
|
||||||
| (_, _) => print "verified lines; no problems\n"
|
|
||||||
in
|
|
||||||
fun verifyLines (buffer: t) =
|
|
||||||
let
|
|
||||||
val (strings, lines) =
|
|
||||||
goToStart
|
|
||||||
( #leftStrings buffer
|
|
||||||
, #leftLines buffer
|
|
||||||
, #rightStrings buffer
|
|
||||||
, #rightLines buffer
|
|
||||||
)
|
|
||||||
in
|
|
||||||
verifyLineList (strings, lines)
|
|
||||||
end
|
|
||||||
end
|
|
||||||
|
|
||||||
val stringLimit = 1024
|
val stringLimit = 1024
|
||||||
val vecLimit = 32
|
val vecLimit = 32
|
||||||
@@ -181,7 +93,7 @@ struct
|
|||||||
val midVal = Vector.sub (lines, mid)
|
val midVal = Vector.sub (lines, mid)
|
||||||
in
|
in
|
||||||
if midVal = findNum then
|
if midVal = findNum then
|
||||||
(print "return 173\n"; mid)
|
mid
|
||||||
else if midVal < findNum then
|
else if midVal < findNum then
|
||||||
helpBinSearch (findNum, lines, mid + 1, high)
|
helpBinSearch (findNum, lines, mid + 1, high)
|
||||||
else
|
else
|
||||||
@@ -211,12 +123,11 @@ struct
|
|||||||
if isInLimit (strHd, newString, lineHd, newLines) then
|
if isInLimit (strHd, newString, lineHd, newLines) then
|
||||||
(* Fits in limit, so we can add to existing string/line vector.*)
|
(* Fits in limit, so we can add to existing string/line vector.*)
|
||||||
let
|
let
|
||||||
(* VERIFIED TO WORK *)
|
|
||||||
val _ = print "line 110\n"
|
|
||||||
val newIdx = curIdx + String.size newString
|
val newIdx = curIdx + String.size newString
|
||||||
val newStrHd = strHd ^ newString
|
val newStrHd = strHd ^ newString
|
||||||
val newLeftString = newStrHd :: strTl
|
val newLeftString = newStrHd :: strTl
|
||||||
val newLine = curLine + Vector.length newLines
|
val newLine = curLine + Vector.length newLines
|
||||||
|
|
||||||
val newLinesHd =
|
val newLinesHd =
|
||||||
Vector.tabulate
|
Vector.tabulate
|
||||||
( Vector.length lineHd + Vector.length newLines
|
( Vector.length lineHd + Vector.length newLines
|
||||||
@@ -229,30 +140,23 @@ struct
|
|||||||
)
|
)
|
||||||
val newLeftLines = newLinesHd :: lineTl
|
val newLeftLines = newLinesHd :: lineTl
|
||||||
in
|
in
|
||||||
verifyReturn
|
{ idx = newIdx
|
||||||
{ idx = newIdx
|
, line = newLine
|
||||||
, line = newLine
|
, leftStrings = newLeftString
|
||||||
, leftStrings = newLeftString
|
, leftLines = newLeftLines
|
||||||
, leftLines = newLeftLines
|
, rightStrings = rightStrings
|
||||||
, rightStrings = rightStrings
|
, rightLines = rightLines
|
||||||
, rightLines = rightLines
|
}
|
||||||
}
|
|
||||||
end
|
end
|
||||||
else
|
else
|
||||||
let
|
(* Does not fit in limit, so cons instead.*)
|
||||||
val _ = print "line 137\n"
|
{ idx = curIdx + String.size newString
|
||||||
(* VERIFIED TO WORK *)
|
, line = curLine + Vector.length newLines
|
||||||
in
|
, leftStrings = newString :: leftStrings
|
||||||
(* Does not fit in limit, so cons instead.*)
|
, leftLines = newLines :: leftLines
|
||||||
verifyReturn
|
, rightStrings = rightStrings
|
||||||
{ idx = curIdx + String.size newString
|
, rightLines = rightLines
|
||||||
, line = curLine + Vector.length newLines
|
}
|
||||||
, leftStrings = newString :: leftStrings
|
|
||||||
, leftLines = newLines :: leftLines
|
|
||||||
, rightStrings = rightStrings
|
|
||||||
, rightLines = rightLines
|
|
||||||
}
|
|
||||||
end
|
|
||||||
| (_, _) =>
|
| (_, _) =>
|
||||||
(*
|
(*
|
||||||
* Because movements between string/line lists in the gap buffer
|
* Because movements between string/line lists in the gap buffer
|
||||||
@@ -260,19 +164,13 @@ struct
|
|||||||
* also means that the other one is empty.
|
* also means that the other one is empty.
|
||||||
* So we don't need to perform addition or consing.
|
* So we don't need to perform addition or consing.
|
||||||
*)
|
*)
|
||||||
let
|
{ idx = String.size newString
|
||||||
val _ = print "line 156\n"
|
, line = Vector.length newLines
|
||||||
(* VERIFIED TO WORK *)
|
, leftStrings = [newString]
|
||||||
in
|
, leftLines = [newLines]
|
||||||
verifyReturn
|
, rightStrings = rightStrings
|
||||||
{ idx = String.size newString
|
, rightLines = rightLines
|
||||||
, line = Vector.length newLines
|
}
|
||||||
, leftStrings = [newString]
|
|
||||||
, leftLines = [newLines]
|
|
||||||
, rightStrings = rightStrings
|
|
||||||
, rightLines = rightLines
|
|
||||||
}
|
|
||||||
end
|
|
||||||
|
|
||||||
fun insInLeftList
|
fun insInLeftList
|
||||||
( idx
|
( idx
|
||||||
@@ -292,16 +190,9 @@ struct
|
|||||||
) : t =
|
) : t =
|
||||||
if idx = prevIdx then
|
if idx = prevIdx then
|
||||||
(* Need to insert at the start of the left list. *)
|
(* Need to insert at the start of the left list. *)
|
||||||
if
|
if isInLimit (newString, leftStringsHd, newLines, leftLinesHd) then
|
||||||
(*
|
|
||||||
isInLimit (newString, leftStringsHd, newLines, leftLinesHd)
|
|
||||||
*)
|
|
||||||
false
|
|
||||||
then
|
|
||||||
let
|
let
|
||||||
(* Create new vector, adjusting indices as needed. *)
|
(* Create new vector, adjusting indices as needed. *)
|
||||||
(* VERIFIED TO WORK *)
|
|
||||||
val _ = print "line 188\n"
|
|
||||||
val joinedLines =
|
val joinedLines =
|
||||||
Vector.tabulate
|
Vector.tabulate
|
||||||
( Vector.length newLines + Vector.length leftLinesHd
|
( Vector.length newLines + Vector.length leftLinesHd
|
||||||
@@ -313,30 +204,23 @@ struct
|
|||||||
+ String.size newString
|
+ String.size newString
|
||||||
)
|
)
|
||||||
in
|
in
|
||||||
verifyReturn
|
{ idx = curIdx + String.size newString
|
||||||
{ idx = curIdx + String.size newString
|
, line = curLine + Vector.length newLines
|
||||||
, line = curLine + Vector.length newLines
|
, leftStrings = (newString ^ leftStringsHd) :: leftStringsTl
|
||||||
, leftStrings = (newString ^ leftStringsHd) :: leftStringsTl
|
, leftLines = joinedLines :: leftLinesTl
|
||||||
, leftLines = joinedLines :: leftLinesTl
|
, rightStrings = rightStrings
|
||||||
, rightStrings = rightStrings
|
, rightLines = rightLines
|
||||||
, rightLines = rightLines
|
}
|
||||||
}
|
|
||||||
end
|
end
|
||||||
else
|
else
|
||||||
(* Just cons everything; no way we can join while staying in limit. *)
|
(* Just cons everything; no way we can join while staying in limit. *)
|
||||||
let
|
{ idx = curIdx + String.size newString
|
||||||
(* VERIFIED TO WORK *)
|
, line = curLine + Vector.length newLines
|
||||||
val _ = print "line 210\n"
|
, leftStrings = leftStringsHd :: newString :: leftStringsTl
|
||||||
in
|
, leftLines = leftLinesHd :: newLines :: leftLinesTl
|
||||||
verifyReturn
|
, rightStrings = rightStrings
|
||||||
{ idx = curIdx + String.size newString
|
, rightLines = rightLines
|
||||||
, line = curLine + Vector.length newLines
|
}
|
||||||
, leftStrings = leftStringsHd :: newString :: leftStringsTl
|
|
||||||
, leftLines = leftLinesHd :: newLines :: leftLinesTl
|
|
||||||
, rightStrings = rightStrings
|
|
||||||
, rightLines = rightLines
|
|
||||||
}
|
|
||||||
end
|
|
||||||
else
|
else
|
||||||
(* Need to insert in the middle of the left list. *)
|
(* Need to insert in the middle of the left list. *)
|
||||||
let
|
let
|
||||||
@@ -346,20 +230,12 @@ struct
|
|||||||
val strSub2 = String.substring
|
val strSub2 = String.substring
|
||||||
(leftStringsHd, strLength, String.size leftStringsHd - strLength)
|
(leftStringsHd, strLength, String.size leftStringsHd - strLength)
|
||||||
val midpoint = binSearch (String.size strSub1 - 1, leftLinesHd)
|
val midpoint = binSearch (String.size strSub1 - 1, leftLinesHd)
|
||||||
val _ = print ("lines in vec: " ^ lineBreaksToString leftLinesHd ^ "\n")
|
|
||||||
val _ = print
|
|
||||||
("vec size:" ^ Int.toString (Vector.length leftLinesHd) ^ "\n")
|
|
||||||
val _ = print ("midpoint:" ^ Int.toString (midpoint) ^ "\n")
|
|
||||||
in
|
in
|
||||||
if
|
if
|
||||||
(* isThreeInLimit (strSub1, newString, strSub2, leftLinesHd, newLines)
|
isThreeInLimit (strSub1, newString, strSub2, leftLinesHd, newLines)
|
||||||
* *)
|
|
||||||
false
|
|
||||||
then
|
then
|
||||||
(* Join three strings together. *)
|
(* Join three strings together. *)
|
||||||
let
|
let
|
||||||
(* VERIFIED TO WORK *)
|
|
||||||
val _ = print "line 233\n"
|
|
||||||
val joinedString = String.concat [strSub1, newString, strSub2]
|
val joinedString = String.concat [strSub1, newString, strSub2]
|
||||||
val joinedLines =
|
val joinedLines =
|
||||||
if Vector.length leftLinesHd > 0 then
|
if Vector.length leftLinesHd > 0 then
|
||||||
@@ -378,32 +254,21 @@ struct
|
|||||||
else
|
else
|
||||||
Vector.map (fn el => el + String.size strSub1) newLines
|
Vector.map (fn el => el + String.size strSub1) newLines
|
||||||
in
|
in
|
||||||
verifyReturn
|
{ idx = curIdx + String.size newString
|
||||||
{ idx = curIdx + String.size newString
|
, line = curLine + Vector.length newLines
|
||||||
, line = curLine + Vector.length newLines
|
, leftStrings = joinedString :: leftStringsTl
|
||||||
, leftStrings = joinedString :: leftStringsTl
|
, leftLines = joinedLines :: leftLinesTl
|
||||||
, leftLines = joinedLines :: leftLinesTl
|
, rightStrings = rightStrings
|
||||||
, rightStrings = rightStrings
|
, rightLines = rightLines
|
||||||
, rightLines = rightLines
|
}
|
||||||
}
|
|
||||||
end
|
end
|
||||||
else if
|
else if
|
||||||
false (*
|
String.size strSub1 + String.size newString <= stringLimit
|
||||||
String.size strSub1 + String.size newString <= stringLimit
|
andalso midpoint + Vector.length newLines <= vecLimit
|
||||||
andalso midpoint + Vector.length newLines <= vecLimit
|
|
||||||
*)
|
|
||||||
then
|
then
|
||||||
(* If we can join newString/lines with sub1 while
|
(* If we can join newString/lines with sub1 while
|
||||||
* staying in limit. *)
|
* staying in limit. *)
|
||||||
let
|
let
|
||||||
(* VERIFIED TO WORK *)
|
|
||||||
val _ = print "line 416\n\n\n"
|
|
||||||
val _ = print
|
|
||||||
("vector length: " ^ Int.toString (Vector.length newLines) ^ "\n")
|
|
||||||
val _ = print ("midpoint: " ^ Int.toString (midpoint) ^ "\n")
|
|
||||||
val _ = print ("leftLinesHd: " ^ lineBreaksToString leftLinesHd)
|
|
||||||
|
|
||||||
(* NEWLEFTLINES VERIFIED *)
|
|
||||||
val newLeftLines =
|
val newLeftLines =
|
||||||
if midpoint >= 0 then
|
if midpoint >= 0 then
|
||||||
(* Implicit: a binSearch match was found. *)
|
(* Implicit: a binSearch match was found. *)
|
||||||
@@ -420,9 +285,6 @@ struct
|
|||||||
else
|
else
|
||||||
Vector.map (fn el => el + String.size strSub1) newLines
|
Vector.map (fn el => el + String.size strSub1) newLines
|
||||||
|
|
||||||
val _ = print "line 275\n"
|
|
||||||
|
|
||||||
(* NEWRIGHTLINES VERIFIED *)
|
|
||||||
val newRightLines =
|
val newRightLines =
|
||||||
if midpoint >= 0 then
|
if midpoint >= 0 then
|
||||||
(* Implicit: a binSearch match was found. *)
|
(* Implicit: a binSearch match was found. *)
|
||||||
@@ -435,31 +297,25 @@ struct
|
|||||||
else
|
else
|
||||||
Vector.map (fn idx => idx - String.size strSub1) leftLinesHd
|
Vector.map (fn idx => idx - String.size strSub1) leftLinesHd
|
||||||
in
|
in
|
||||||
verifyReturn
|
{ idx = prevIdx + String.size strSub1 + String.size newString
|
||||||
{ idx = prevIdx + String.size strSub1 + String.size newString
|
, line =
|
||||||
, line =
|
(curLine - Vector.length leftLinesHd)
|
||||||
(curLine - Vector.length leftLinesHd)
|
+ Vector.length newLeftLines
|
||||||
+ Vector.length newLeftLines
|
, leftStrings = (strSub1 ^ newString) :: leftStringsTl
|
||||||
, leftStrings = (strSub1 ^ newString) :: leftStringsTl
|
, leftLines = newLeftLines :: leftLinesTl
|
||||||
, leftLines = newLeftLines :: leftLinesTl
|
, rightStrings = strSub2 :: rightStrings
|
||||||
, rightStrings = strSub2 :: rightStrings
|
, rightLines = newRightLines :: rightLines
|
||||||
, rightLines = newRightLines :: rightLines
|
}
|
||||||
}
|
|
||||||
end
|
end
|
||||||
else if
|
else if
|
||||||
(*
|
String.size newString + String.size strSub2 <= stringLimit
|
||||||
String.size newString + String.size strSub2 <= stringLimit
|
andalso
|
||||||
andalso
|
(Vector.length leftLinesHd - midpoint) + Vector.length newLines
|
||||||
(Vector.length leftLinesHd - midpoint) + Vector.length newLines
|
<= vecLimit
|
||||||
<= vecLimit
|
|
||||||
*)
|
|
||||||
false
|
|
||||||
then
|
then
|
||||||
(* If we can join newString/line with sub2 while staying
|
(* If we can join newString/line with sub2 while staying
|
||||||
* in limit. *)
|
* in limit. *)
|
||||||
let
|
let
|
||||||
(* VERIFIED TO WORK *)
|
|
||||||
val _ = print "line 478\n"
|
|
||||||
val newLeftLines =
|
val newLeftLines =
|
||||||
if midpoint >= 0 andalso Vector.length leftLinesHd > 0 then
|
if midpoint >= 0 andalso Vector.length leftLinesHd > 0 then
|
||||||
let
|
let
|
||||||
@@ -486,19 +342,17 @@ struct
|
|||||||
) - String.size strSub1 + String.size newString
|
) - String.size strSub1 + String.size newString
|
||||||
)
|
)
|
||||||
in
|
in
|
||||||
verifyReturn
|
{ idx = prevIdx + String.size strSub1
|
||||||
{ idx = prevIdx + String.size strSub1
|
, line = (curLine - Vector.length leftLinesHd) + midpoint
|
||||||
, line = (curLine - Vector.length leftLinesHd) + midpoint
|
, leftStrings = strSub1 :: leftStringsTl
|
||||||
, leftStrings = strSub1 :: leftStringsTl
|
, leftLines = newLeftLines :: leftLinesTl
|
||||||
, leftLines = newLeftLines :: leftLinesTl
|
, rightStrings = (newString ^ strSub2) :: rightStrings
|
||||||
, rightStrings = (newString ^ strSub2) :: rightStrings
|
, rightLines = newRightLines :: rightLines
|
||||||
, rightLines = newRightLines :: rightLines
|
}
|
||||||
}
|
|
||||||
end
|
end
|
||||||
else
|
else
|
||||||
(* Can't join on either side while staying in limit. *)
|
(* Can't join on either side while staying in limit. *)
|
||||||
let
|
let
|
||||||
(* VERIFIED TO WORK *)
|
|
||||||
val lineSub1 =
|
val lineSub1 =
|
||||||
if midpoint >= 0 andalso Vector.length leftLinesHd > 0 then
|
if midpoint >= 0 andalso Vector.length leftLinesHd > 0 then
|
||||||
let
|
let
|
||||||
@@ -516,16 +370,15 @@ struct
|
|||||||
Vector.sub (leftLinesHd, idx + Vector.length lineSub1)
|
Vector.sub (leftLinesHd, idx + Vector.length lineSub1)
|
||||||
- String.size strSub1)
|
- String.size strSub1)
|
||||||
in
|
in
|
||||||
verifyReturn
|
{ idx = prevIdx + String.size strSub1 + String.size newString
|
||||||
{ idx = prevIdx + String.size strSub1 + String.size newString
|
, line =
|
||||||
, line =
|
(curLine - String.size leftStringsHd) + midpoint
|
||||||
(curLine - String.size leftStringsHd) + midpoint
|
+ Vector.length newLines
|
||||||
+ Vector.length newLines
|
, leftStrings = newString :: strSub1 :: leftStringsTl
|
||||||
, leftStrings = newString :: strSub1 :: leftStringsTl
|
, leftLines = newLines :: lineSub1 :: leftLinesTl
|
||||||
, leftLines = newLines :: lineSub1 :: leftLinesTl
|
, rightStrings = strSub2 :: rightStrings
|
||||||
, rightStrings = strSub2 :: rightStrings
|
, rightLines = lineSub2 :: rightLines
|
||||||
, rightLines = lineSub2 :: rightLines
|
}
|
||||||
}
|
|
||||||
end
|
end
|
||||||
end
|
end
|
||||||
|
|
||||||
@@ -555,14 +408,11 @@ struct
|
|||||||
* *)
|
* *)
|
||||||
(case (rightStrings, rightLines) of
|
(case (rightStrings, rightLines) of
|
||||||
(rightStringsHd :: rightStringsTl, rightLinesHd :: rightLinesTl) =>
|
(rightStringsHd :: rightStringsTl, rightLinesHd :: rightLinesTl) =>
|
||||||
if false
|
if
|
||||||
(*
|
isInLimit
|
||||||
isInLimit
|
(leftStringsHd, rightStringsHd, leftLinesHd, rightLinesHd)
|
||||||
(leftStringsHd, rightStringsHd, leftLinesHd, rightLinesHd)
|
then
|
||||||
*) then
|
|
||||||
let
|
let
|
||||||
(* VERIFIED TO WORK *)
|
|
||||||
val _ = print "line 370\n"
|
|
||||||
val prevLine = curLine - Vector.length leftLinesHd
|
val prevLine = curLine - Vector.length leftLinesHd
|
||||||
val newRightStringsHd = leftStringsHd ^ rightStringsHd
|
val newRightStringsHd = leftStringsHd ^ rightStringsHd
|
||||||
|
|
||||||
@@ -638,14 +488,13 @@ struct
|
|||||||
| (_, _) =>
|
| (_, _) =>
|
||||||
(* Left list is empty, so need to cons or join.
|
(* Left list is empty, so need to cons or join.
|
||||||
* Just set left string/list as newString/newLines. *)
|
* Just set left string/list as newString/newLines. *)
|
||||||
verifyReturn
|
{ idx = String.size newString
|
||||||
{ idx = String.size newString
|
, line = Vector.length newLines
|
||||||
, line = Vector.length newLines
|
, leftStrings = [newString]
|
||||||
, leftStrings = [newString]
|
, leftLines = [newLines]
|
||||||
, leftLines = [newLines]
|
, rightStrings = rightStrings
|
||||||
, rightStrings = rightStrings
|
, rightLines = rightLines
|
||||||
, rightLines = rightLines
|
}
|
||||||
}
|
|
||||||
|
|
||||||
fun insInRightList
|
fun insInRightList
|
||||||
( idx
|
( idx
|
||||||
@@ -668,8 +517,6 @@ struct
|
|||||||
if isInLimit (newString, rightStringsHd, newLines, rightLinesHd) then
|
if isInLimit (newString, rightStringsHd, newLines, rightLinesHd) then
|
||||||
(* Allocate new string because we can do so while staying in limit. *)
|
(* Allocate new string because we can do so while staying in limit. *)
|
||||||
let
|
let
|
||||||
(* VERIFIED TO WORK *)
|
|
||||||
val _ = print "line 474\n"
|
|
||||||
val newRightStringsHd = rightStringsHd ^ newString
|
val newRightStringsHd = rightStringsHd ^ newString
|
||||||
val newRightLinesHd =
|
val newRightLinesHd =
|
||||||
Vector.tabulate
|
Vector.tabulate
|
||||||
@@ -682,30 +529,24 @@ struct
|
|||||||
+ String.size rightStringsHd
|
+ String.size rightStringsHd
|
||||||
)
|
)
|
||||||
in
|
in
|
||||||
verifyReturn
|
{ idx = curIdx
|
||||||
{ idx = curIdx
|
, line = curLine
|
||||||
, line = curLine
|
, leftStrings = leftStrings
|
||||||
, leftStrings = leftStrings
|
, leftLines = leftLines
|
||||||
, leftLines = leftLines
|
, rightStrings = newRightStringsHd :: rightStringsTl
|
||||||
, rightStrings = newRightStringsHd :: rightStringsTl
|
, rightLines = newRightLinesHd :: rightLinesTl
|
||||||
, rightLines = newRightLinesHd :: rightLinesTl
|
}
|
||||||
}
|
|
||||||
end
|
end
|
||||||
else
|
else
|
||||||
(* Cons newString and newLines to after-the-head,
|
(* Cons newString and newLines to after-the-head,
|
||||||
* because we can't join while staying in the limit.*)
|
* because we can't join while staying in the limit.*)
|
||||||
let
|
{ idx = curIdx
|
||||||
val _ = print "line 498\n"
|
, line = curLine
|
||||||
in
|
, leftStrings = leftStrings
|
||||||
verifyReturn
|
, leftLines = leftLines
|
||||||
{ idx = curIdx
|
, rightStrings = rightStringsHd :: newString :: rightStringsTl
|
||||||
, line = curLine
|
, rightLines = rightLinesHd :: newLines :: rightLinesTl
|
||||||
, leftStrings = leftStrings
|
}
|
||||||
, leftLines = leftLines
|
|
||||||
, rightStrings = rightStringsHd :: newString :: rightStringsTl
|
|
||||||
, rightLines = rightLinesHd :: newLines :: rightLinesTl
|
|
||||||
}
|
|
||||||
end
|
|
||||||
else
|
else
|
||||||
(* Have to split rightStringsHd and rightLinesHd in the middle. *)
|
(* Have to split rightStringsHd and rightLinesHd in the middle. *)
|
||||||
let
|
let
|
||||||
@@ -716,17 +557,11 @@ struct
|
|||||||
val midpoint = binSearch (String.size strSub1 - 1, rightLinesHd)
|
val midpoint = binSearch (String.size strSub1 - 1, rightLinesHd)
|
||||||
in
|
in
|
||||||
if
|
if
|
||||||
(*
|
isThreeInLimit (strSub1, newString, strSub2, rightLinesHd, newLines)
|
||||||
isThreeInLimit (strSub1, newString, strSub2, rightLinesHd, newLines)
|
|
||||||
*)
|
|
||||||
true
|
|
||||||
then
|
then
|
||||||
(* Join three strings together. *)
|
(* Join three strings together. *)
|
||||||
let
|
let
|
||||||
(* VERIFIED TO WORK *)
|
|
||||||
val _ = print "line 573\n"
|
|
||||||
val newRightStringsHd = String.concat [strSub1, newString, strSub2]
|
val newRightStringsHd = String.concat [strSub1, newString, strSub2]
|
||||||
|
|
||||||
val newRightLinesHd =
|
val newRightLinesHd =
|
||||||
if Vector.length rightLinesHd > 0 then
|
if Vector.length rightLinesHd > 0 then
|
||||||
Vector.tabulate
|
Vector.tabulate
|
||||||
@@ -744,30 +579,23 @@ struct
|
|||||||
)
|
)
|
||||||
else
|
else
|
||||||
Vector.map (fn el => el + String.size strSub1) newLines
|
Vector.map (fn el => el + String.size strSub1) newLines
|
||||||
|
|
||||||
in
|
in
|
||||||
verifyReturn
|
{ idx = curIdx
|
||||||
{ idx = curIdx
|
, line = curLine
|
||||||
, line = curLine
|
, leftStrings = leftStrings
|
||||||
, leftStrings = leftStrings
|
, leftLines = leftLines
|
||||||
, leftLines = leftLines
|
, rightStrings = newRightStringsHd :: rightStringsTl
|
||||||
, rightStrings = newRightStringsHd :: rightStringsTl
|
, rightLines = newRightLinesHd :: rightLinesTl
|
||||||
, rightLines = newRightLinesHd :: rightLinesTl
|
}
|
||||||
}
|
|
||||||
end
|
end
|
||||||
else if
|
else if
|
||||||
(*
|
String.size strSub1 + String.size newString <= stringLimit
|
||||||
String.size strSub1 + String.size newString <= stringLimit
|
andalso midpoint + Vector.length newLines <= vecLimit
|
||||||
andalso midpoint + Vector.length newLines <= vecLimit
|
|
||||||
*)
|
|
||||||
true
|
|
||||||
then
|
then
|
||||||
(* If we can join newString/lines with sub1 while
|
(* If we can join newString/lines with sub1 while
|
||||||
* staying in limit. *)
|
* staying in limit. *)
|
||||||
let
|
let
|
||||||
(* VERIFIED *)
|
|
||||||
(* strSub1 ^ newString is placed on the left list. *)
|
(* strSub1 ^ newString is placed on the left list. *)
|
||||||
val _ = print "line 552\n"
|
|
||||||
val newLeftStringsHd = strSub1 ^ newString
|
val newLeftStringsHd = strSub1 ^ newString
|
||||||
val newLeftLinesHd =
|
val newLeftLinesHd =
|
||||||
if midpoint >= 0 then
|
if midpoint >= 0 then
|
||||||
@@ -785,7 +613,6 @@ struct
|
|||||||
else
|
else
|
||||||
Vector.map (fn el => el + String.size strSub1) newLines
|
Vector.map (fn el => el + String.size strSub1) newLines
|
||||||
|
|
||||||
val _ = print "line 584\n"
|
|
||||||
val newRightLinesHd =
|
val newRightLinesHd =
|
||||||
if midpoint >= 0 then
|
if midpoint >= 0 then
|
||||||
(* Implicit: a binSearch match was found. *)
|
(* Implicit: a binSearch match was found. *)
|
||||||
@@ -798,29 +625,23 @@ struct
|
|||||||
else
|
else
|
||||||
Vector.map (fn idx => idx - String.size strSub1) rightLinesHd
|
Vector.map (fn idx => idx - String.size strSub1) rightLinesHd
|
||||||
in
|
in
|
||||||
verifyReturn
|
{ idx = curIdx + String.size newLeftStringsHd
|
||||||
{ idx = curIdx + String.size newLeftStringsHd
|
, line = curLine + Vector.length newLeftLinesHd
|
||||||
, line = curLine + Vector.length newLeftLinesHd
|
, leftStrings = newLeftStringsHd :: leftStrings
|
||||||
, leftStrings = newLeftStringsHd :: leftStrings
|
, leftLines = newLeftLinesHd :: leftLines
|
||||||
, leftLines = newLeftLinesHd :: leftLines
|
, rightStrings = strSub2 :: rightStringsTl
|
||||||
, rightStrings = strSub2 :: rightStringsTl
|
, rightLines = newRightLinesHd :: rightLinesTl
|
||||||
, rightLines = newRightLinesHd :: rightLinesTl
|
}
|
||||||
}
|
|
||||||
end
|
end
|
||||||
else if
|
else if
|
||||||
(*
|
|
||||||
String.size newString + String.size strSub2 <= stringLimit
|
String.size newString + String.size strSub2 <= stringLimit
|
||||||
andalso
|
andalso
|
||||||
(Vector.length rightLinesHd - midpoint) + Vector.length newLines
|
(Vector.length rightLinesHd - midpoint) + Vector.length newLines
|
||||||
<= vecLimit
|
<= vecLimit
|
||||||
*)
|
|
||||||
true
|
|
||||||
then
|
then
|
||||||
(* If we can join newString/line with sub2 while staying
|
(* If we can join newString/line with sub2 while staying
|
||||||
* in limit. *)
|
* in limit. *)
|
||||||
let
|
let
|
||||||
(* VERIFIED TO WORK *)
|
|
||||||
val _ = print "line 581\n"
|
|
||||||
val newLeftLinesHd =
|
val newLeftLinesHd =
|
||||||
if midpoint >= 0 then
|
if midpoint >= 0 then
|
||||||
let
|
let
|
||||||
@@ -849,20 +670,17 @@ struct
|
|||||||
)
|
)
|
||||||
|
|
||||||
in
|
in
|
||||||
verifyReturn
|
{ idx = curIdx + String.size strSub1
|
||||||
{ idx = curIdx + String.size strSub1
|
, line = curLine + Vector.length newLeftLinesHd
|
||||||
, line = curLine + Vector.length newLeftLinesHd
|
, leftStrings = strSub1 :: leftStrings
|
||||||
, leftStrings = strSub1 :: leftStrings
|
, leftLines = newLeftLinesHd :: leftLines
|
||||||
, leftLines = newLeftLinesHd :: leftLines
|
, rightStrings = newRightStringsHd :: rightStringsTl
|
||||||
, rightStrings = newRightStringsHd :: rightStringsTl
|
, rightLines = newRightLinesHd :: rightLinesTl
|
||||||
, rightLines = newRightLinesHd :: rightLinesTl
|
}
|
||||||
}
|
|
||||||
end
|
end
|
||||||
else
|
else
|
||||||
(* Can't join on either side while staying in limit. *)
|
(* Can't join on either side while staying in limit. *)
|
||||||
let
|
let
|
||||||
(* VERIFIED TO WORK *)
|
|
||||||
val _ = print "line 608\n"
|
|
||||||
val lineSub1 =
|
val lineSub1 =
|
||||||
if midpoint >= 0 andalso Vector.length rightLinesHd > 0 then
|
if midpoint >= 0 andalso Vector.length rightLinesHd > 0 then
|
||||||
let
|
let
|
||||||
@@ -880,16 +698,13 @@ struct
|
|||||||
Vector.sub (rightLinesHd, idx + Vector.length lineSub1)
|
Vector.sub (rightLinesHd, idx + Vector.length lineSub1)
|
||||||
- String.size strSub1)
|
- String.size strSub1)
|
||||||
in
|
in
|
||||||
verifyReturn
|
{ idx = curIdx + String.size strSub1 + String.size newString
|
||||||
{ idx = curIdx + String.size strSub1 + String.size newString
|
, line = curLine + Vector.length newLines + Vector.length lineSub1
|
||||||
, line =
|
, leftStrings = newString :: strSub1 :: leftStrings
|
||||||
curLine + Vector.length newLines
|
, leftLines = newLines :: lineSub1 :: leftLines
|
||||||
+ Vector.length lineSub1
|
, rightStrings = strSub2 :: rightStringsTl
|
||||||
, leftStrings = newString :: strSub1 :: leftStrings
|
, rightLines = lineSub2 :: rightLinesTl
|
||||||
, leftLines = newLines :: lineSub1 :: leftLines
|
}
|
||||||
, rightStrings = strSub2 :: rightStringsTl
|
|
||||||
, rightLines = lineSub2 :: rightLinesTl
|
|
||||||
}
|
|
||||||
end
|
end
|
||||||
end
|
end
|
||||||
|
|
||||||
@@ -914,15 +729,10 @@ struct
|
|||||||
(case (leftStrings, leftLines) of
|
(case (leftStrings, leftLines) of
|
||||||
(leftStringsHd :: leftStringsTl, leftLinesHd :: leftLinesTl) =>
|
(leftStringsHd :: leftStringsTl, leftLinesHd :: leftLinesTl) =>
|
||||||
if
|
if
|
||||||
(*
|
|
||||||
isInLimit
|
isInLimit
|
||||||
(leftStringsHd, rightStringsHd, leftLinesHd, rightLinesHd)
|
(leftStringsHd, rightStringsHd, leftLinesHd, rightLinesHd)
|
||||||
*)
|
|
||||||
true
|
|
||||||
then
|
then
|
||||||
let
|
let
|
||||||
(* VERIFIED TO WORK *)
|
|
||||||
val _ = print "line 650\n"
|
|
||||||
val nextLine = curLine + Vector.length rightLinesHd
|
val nextLine = curLine + Vector.length rightLinesHd
|
||||||
val newLeftStringsHd = leftStringsHd ^ rightStringsHd
|
val newLeftStringsHd = leftStringsHd ^ rightStringsHd
|
||||||
val newLeftLinesHd =
|
val newLeftLinesHd =
|
||||||
@@ -995,18 +805,13 @@ struct
|
|||||||
end
|
end
|
||||||
| (_, _) =>
|
| (_, _) =>
|
||||||
(* Right string/line is empty. *)
|
(* Right string/line is empty. *)
|
||||||
let
|
{ idx = curIdx
|
||||||
val _ = print "line 723\n"
|
, line = curLine
|
||||||
in
|
, leftStrings = leftStrings
|
||||||
verifyReturn
|
, leftLines = leftLines
|
||||||
{ idx = curIdx
|
, rightStrings = [newString]
|
||||||
, line = curLine
|
, rightLines = [newLines]
|
||||||
, leftStrings = leftStrings
|
}
|
||||||
, leftLines = leftLines
|
|
||||||
, rightStrings = [newString]
|
|
||||||
, rightLines = [newLines]
|
|
||||||
}
|
|
||||||
end
|
|
||||||
|
|
||||||
fun ins
|
fun ins
|
||||||
( idx
|
( idx
|
||||||
@@ -1072,4 +877,60 @@ struct
|
|||||||
, #rightLines buffer
|
, #rightLines buffer
|
||||||
)
|
)
|
||||||
end
|
end
|
||||||
|
|
||||||
|
|
||||||
|
(* TEST CODE *)
|
||||||
|
local
|
||||||
|
fun lineBreaksToString vec =
|
||||||
|
(Vector.foldr (fn (el, acc) => Int.toString el ^ ", " ^ acc) "" vec)
|
||||||
|
^ "\n"
|
||||||
|
|
||||||
|
fun checkLineBreaks (v1, v2) =
|
||||||
|
if v1 = v2 then
|
||||||
|
()
|
||||||
|
else
|
||||||
|
let
|
||||||
|
val _ = print ("broken: " ^ (lineBreaksToString v1))
|
||||||
|
val _ = print ("fixed: " ^ (lineBreaksToString v2))
|
||||||
|
in
|
||||||
|
()
|
||||||
|
end
|
||||||
|
|
||||||
|
fun goToStart (leftStrings, leftLines, accStrings, accLines) =
|
||||||
|
case (leftStrings, leftLines) of
|
||||||
|
(lsHd :: lsTl, llHd :: llTl) =>
|
||||||
|
goToStart (lsTl, llTl, lsHd :: accStrings, llHd :: accLines)
|
||||||
|
| (_, _) => (accStrings, accLines)
|
||||||
|
|
||||||
|
fun verifyLineList (strings, lines) =
|
||||||
|
case (strings, lines) of
|
||||||
|
(strHd :: strTl, lHd :: lTl) =>
|
||||||
|
let
|
||||||
|
val checkLines = countLineBreaks strHd
|
||||||
|
in
|
||||||
|
if checkLines = lHd then
|
||||||
|
verifyLineList (strTl, lTl)
|
||||||
|
else
|
||||||
|
let
|
||||||
|
val _ = print "line metadata is incorrect\n"
|
||||||
|
val _ = checkLineBreaks (lHd, checkLines)
|
||||||
|
in
|
||||||
|
raise Empty
|
||||||
|
end
|
||||||
|
end
|
||||||
|
| (_, _) => print "verified lines; no problems\n"
|
||||||
|
in
|
||||||
|
fun verifyLines (buffer: t) =
|
||||||
|
let
|
||||||
|
val (strings, lines) =
|
||||||
|
goToStart
|
||||||
|
( #leftStrings buffer
|
||||||
|
, #leftLines buffer
|
||||||
|
, #rightStrings buffer
|
||||||
|
, #rightLines buffer
|
||||||
|
)
|
||||||
|
in
|
||||||
|
verifyLineList (strings, lines)
|
||||||
|
end
|
||||||
|
end
|
||||||
end
|
end
|
||||||
|
|||||||
Reference in New Issue
Block a user