From 00123048544fd31ed6bd649d96c6432f61ed04a2 Mon Sep 17 00:00:00 2001 From: Humza Shahid Date: Wed, 3 Jul 2024 14:35:38 +0100 Subject: [PATCH] verify another if-statement case --- src/line_gap.sml | 50 ++++++++++++++++++++++++++++++++---------------- 1 file changed, 33 insertions(+), 17 deletions(-) diff --git a/src/line_gap.sml b/src/line_gap.sml index 6edd251..d068145 100644 --- a/src/line_gap.sml +++ b/src/line_gap.sml @@ -775,36 +775,52 @@ struct String.size strSub1 + String.size newString <= stringLimit andalso midpoint + Vector.length newLines <= vecLimit *) - false + true then (* If we can join newString/lines with sub1 while * staying in limit. *) let + (* VERIFIED *) (* strSub1 ^ newString is placed on the left list. *) val _ = print "line 552\n" val newLeftStringsHd = strSub1 ^ newString - (* - val newLeftLinesHd = - Vector.tabulate (Vector.length newLines + midpoint, fn idx => - if idx < midpoint then Vector.sub (rightLinesHd, idx) - else Vector.sub (newLines, idx - midpoint) + String.size strSub1) - *) - val _ = print "line 584\n" - (* - val newRightLinesHd = - VectorSlice.slice (rightLinesHd, midpoint, SOME - (Vector.length rightLinesHd - midpoint)) - val newRightLinesHd = VectorSlice.vector newRightLinesHd *) + val newLeftLinesHd = + if midpoint >= 0 then + (* Implicit: a binSearch match was found. *) + let + val newLeftLinesLength = midpoint + 1 + Vector.length newLines + in + Vector.tabulate (newLeftLinesLength, fn idx => + if idx <= midpoint then + Vector.sub (rightLinesHd, idx) + else + Vector.sub (newLines, idx - (midpoint + 1)) + + String.size strSub1) + end + else + Vector.map (fn el => el + String.size strSub1) newLines + + val _ = print "line 584\n" + val newRightLinesHd = + if midpoint >= 0 then + (* Implicit: a binSearch match was found. *) + Vector.tabulate + ( (Vector.length rightLinesHd - midpoint) - 1 + , fn idx => + Vector.sub (rightLinesHd, idx + midpoint + 1) + - String.size strSub1 + ) + else + Vector.map (fn idx => idx - String.size strSub1) rightLinesHd in verifyReturn { idx = curIdx + String.size newLeftStringsHd - , line = - curLine + Vector.length (countLineBreaks newLeftStringsHd) + , line = curLine + Vector.length newLeftLinesHd , leftStrings = newLeftStringsHd :: leftStrings - , leftLines = countLineBreaks newLeftStringsHd :: leftLines + , leftLines = newLeftLinesHd :: leftLines , rightStrings = strSub2 :: rightStringsTl - , rightLines = countLineBreaks strSub2 :: rightLinesTl + , rightLines = newRightLinesHd :: rightLinesTl } end else if