From 2375055403fdd7f8bee25156797809e2503918d5 Mon Sep 17 00:00:00 2001 From: Sean Weaver Date: Thu, 4 Nov 2021 16:25:39 -0400 Subject: [PATCH 1/5] A take at updating Cryptol's sort function from insertion sort to merge sort. This implementation is much more computationally efficient. --- lib/Cryptol.cry | 35 +++++++++++++++++++++++++---------- 1 file changed, 25 insertions(+), 10 deletions(-) diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 8264abf4b..01b6ea887 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -964,17 +964,32 @@ sort = sortBy (<=) * pair of elements that are equivalent according to the order relation. */ sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a -sortBy le vs = - if `n == (0 : Integer) then vs - else drop`{1 - min 1 n} (insertBy (vs@0) (sortBy le (drop`{min 1 n} vs))) +sortBy le ((xs : [n/2]a) # (ys : [n/^2]a)) = merge le xs' ys' where - insertBy : {k} (fin k) => a -> [k]a -> [k+1]a - insertBy x0 ys = xys.0 # [last xs] - where - xs : [k+1]a - xs = [x0] # xys.1 - xys : [k](a, a) - xys = [ if le x y then (x, y) else (y, x) | x <- xs | y <- ys ] + xs' = if `(n/2) == 1 then xs else sortBy le xs + ys' = if `(n/^2) == 1 then ys else sortBy le ys + +private +merge : {a, n, m} (fin n, fin m) + => (a -> a -> Bit) -> [n]a -> [m]a -> [n + m]a +merge le xs ys = take zs.0 + where + zs = + [ if i == `n then (ys@j, i , j+1) + | j == `m then (xs@i, i+1, j ) + | le (xs@i) (ys@j) then (xs@i, i+1, j ) + else (ys@j, i , j+1) + | (_, i, j) <- [(undefined, 0, 0)] # zs + ] + +private +merge' : {a, n, m} (fin n, fin m) + => (a -> a -> Bit) -> [n]a -> [m]a -> [n + m]a +merge' le xs ys = + if `n == 0 \/ `m == 0 then xs # ys + | le (xs@0) (ys@0) + then drop`{1 - min 1 n} ([xs@0] # merge' le (drop`{min 1 n} xs) ys) + else drop`{1 - min 1 m} ([ys@0] # merge' le xs (drop`{min 1 m} ys)) // GF_2^n polynomial computations ------------------------------------------- From c064d408dce633339fcf36715267d6463b650c06 Mon Sep 17 00:00:00 2001 From: Sean Weaver Date: Sat, 6 Nov 2021 10:11:55 -0400 Subject: [PATCH 2/5] Updating private scoping --- lib/Cryptol.cry | 39 +++++++++++++++++++-------------------- 1 file changed, 19 insertions(+), 20 deletions(-) diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 01b6ea887..75d22b925 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -970,27 +970,26 @@ sortBy le ((xs : [n/2]a) # (ys : [n/^2]a)) = merge le xs' ys' ys' = if `(n/^2) == 1 then ys else sortBy le ys private -merge : {a, n, m} (fin n, fin m) - => (a -> a -> Bit) -> [n]a -> [m]a -> [n + m]a -merge le xs ys = take zs.0 - where - zs = - [ if i == `n then (ys@j, i , j+1) - | j == `m then (xs@i, i+1, j ) - | le (xs@i) (ys@j) then (xs@i, i+1, j ) - else (ys@j, i , j+1) - | (_, i, j) <- [(undefined, 0, 0)] # zs - ] - -private -merge' : {a, n, m} (fin n, fin m) - => (a -> a -> Bit) -> [n]a -> [m]a -> [n + m]a -merge' le xs ys = - if `n == 0 \/ `m == 0 then xs # ys - | le (xs@0) (ys@0) - then drop`{1 - min 1 n} ([xs@0] # merge' le (drop`{min 1 n} xs) ys) - else drop`{1 - min 1 m} ([ys@0] # merge' le xs (drop`{min 1 m} ys)) + merge : {a, n, m} (fin n, fin m) + => (a -> a -> Bit) -> [n]a -> [m]a -> [n + m]a + merge le xs ys = take zs.0 + where + zs = + [ if i == `n then (ys@j, i , j+1) + | j == `m then (xs@i, i+1, j ) + | le (xs@i) (ys@j) then (xs@i, i+1, j ) + else (ys@j, i , j+1) + | (_, i, j) <- [(undefined, 0, 0)] # zs + ] + + merge' : {a, n, m} (fin n, fin m) + => (a -> a -> Bit) -> [n]a -> [m]a -> [n + m]a + merge' le xs ys = + if `n == 0 \/ `m == 0 then xs # ys + | le (xs@0) (ys@0) + then drop`{1 - min 1 n} ([xs@0] # merge' le (drop`{min 1 n} xs) ys) + else drop`{1 - min 1 m} ([ys@0] # merge' le xs (drop`{min 1 m} ys)) // GF_2^n polynomial computations ------------------------------------------- From 3fabe4a21f92191e845f571997b5bdc338c7437e Mon Sep 17 00:00:00 2001 From: Sean Weaver Date: Fri, 12 Nov 2021 22:00:13 -0500 Subject: [PATCH 3/5] selected the first merge option --- lib/Cryptol.cry | 30 +++++++----------------------- 1 file changed, 7 insertions(+), 23 deletions(-) diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 75d22b925..9e7c681e4 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -964,32 +964,16 @@ sort = sortBy (<=) * pair of elements that are equivalent according to the order relation. */ sortBy : {a, n} (fin n) => (a -> a -> Bit) -> [n]a -> [n]a -sortBy le ((xs : [n/2]a) # (ys : [n/^2]a)) = merge le xs' ys' +sortBy le ((xs : [n/2]a) # (ys : [n/^2]a)) = take zs.0 where xs' = if `(n/2) == 1 then xs else sortBy le xs ys' = if `(n/^2) == 1 then ys else sortBy le ys - -private - - merge : {a, n, m} (fin n, fin m) - => (a -> a -> Bit) -> [n]a -> [m]a -> [n + m]a - merge le xs ys = take zs.0 - where - zs = - [ if i == `n then (ys@j, i , j+1) - | j == `m then (xs@i, i+1, j ) - | le (xs@i) (ys@j) then (xs@i, i+1, j ) - else (ys@j, i , j+1) - | (_, i, j) <- [(undefined, 0, 0)] # zs - ] - - merge' : {a, n, m} (fin n, fin m) - => (a -> a -> Bit) -> [n]a -> [m]a -> [n + m]a - merge' le xs ys = - if `n == 0 \/ `m == 0 then xs # ys - | le (xs@0) (ys@0) - then drop`{1 - min 1 n} ([xs@0] # merge' le (drop`{min 1 n} xs) ys) - else drop`{1 - min 1 m} ([ys@0] # merge' le xs (drop`{min 1 m} ys)) + zs = [ if i == `(n/2) then (ys'@j, i , j+1) + | j == `(n/^2) then (xs'@i, i+1, j ) + | le (xs'@i) (ys'@j) then (xs'@i, i+1, j ) + else (ys'@j, i , j+1) + | (_, i, j) <- [ (undefined, 0, 0) ] # zs + ] // GF_2^n polynomial computations ------------------------------------------- From b62960034b922095464fe5d3f2120b2695f866a3 Mon Sep 17 00:00:00 2001 From: Sean Weaver Date: Thu, 18 Nov 2021 12:36:26 -0500 Subject: [PATCH 4/5] Updating issues and regression tests to work w/ latest prelude --- tests/issues/T146.icry.stdout | 8 ++++---- tests/issues/issue1024.icry.stdout | 12 ++++++------ tests/issues/issue103.icry.stdout | 2 +- tests/issues/issue290v2.icry.stdout | 4 ++-- tests/issues/issue723.icry.stdout | 4 ++-- tests/regression/safety.icry.stdout | 2 +- tests/regression/tc-errors.icry.stdout | 8 ++++---- 7 files changed, 20 insertions(+), 20 deletions(-) diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout index f7afeafff..3bdd0b554 100644 --- a/tests/issues/T146.icry.stdout +++ b/tests/issues/T146.icry.stdout @@ -4,15 +4,15 @@ Loading module Main [error] at T146.cry:1:18--6:10: The type ?a is not sufficiently polymorphic. - It cannot depend on quantified variables: fv`829 + It cannot depend on quantified variables: fv`912 When checking type of field 'v0' where ?a is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24 - fv`829 is signature variable 'fv' at T146.cry:11:10--11:12 + fv`912 is signature variable 'fv' at T146.cry:11:10--11:12 [error] at T146.cry:5:19--5:24: The type ?b is not sufficiently polymorphic. - It cannot depend on quantified variables: fv`829 + It cannot depend on quantified variables: fv`912 When checking signature variable 'fv' where ?b is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24 - fv`829 is signature variable 'fv' at T146.cry:11:10--11:12 + fv`912 is signature variable 'fv' at T146.cry:11:10--11:12 diff --git a/tests/issues/issue1024.icry.stdout b/tests/issues/issue1024.icry.stdout index e17455a4d..71a37184e 100644 --- a/tests/issues/issue1024.icry.stdout +++ b/tests/issues/issue1024.icry.stdout @@ -13,20 +13,20 @@ Loading module Main Unused name: g [error] at issue1024a.cry:1:6--1:11: - Illegal kind assigned to type variable: f`826 + Illegal kind assigned to type variable: f`909 Unexpected: # -> * where - f`826 is signature variable 'f' at issue1024a.cry:1:12--1:24 + f`909 is signature variable 'f' at issue1024a.cry:1:12--1:24 [error] at issue1024a.cry:2:6--2:13: - Illegal kind assigned to type variable: f`827 + Illegal kind assigned to type variable: f`910 Unexpected: Prop where - f`827 is signature variable 'f' at issue1024a.cry:2:14--2:24 + f`910 is signature variable 'f' at issue1024a.cry:2:14--2:24 [error] at issue1024a.cry:4:13--4:49: - Illegal kind assigned to type variable: f`829 + Illegal kind assigned to type variable: f`912 Unexpected: # -> * where - f`829 is signature variable 'f' at issue1024a.cry:4:22--4:32 + f`912 is signature variable 'f' at issue1024a.cry:4:22--4:32 Loading module Cryptol Loading module Main 0xffff diff --git a/tests/issues/issue103.icry.stdout b/tests/issues/issue103.icry.stdout index f8e810618..effdc3da5 100644 --- a/tests/issues/issue103.icry.stdout +++ b/tests/issues/issue103.icry.stdout @@ -2,7 +2,7 @@ Loading module Cryptol Run-time error: undefined -- Backtrace -- -Cryptol::error called at Cryptol:1045:13--1045:18 +Cryptol::error called at Cryptol:1043:13--1043:18 Cryptol::undefined called at issue103.icry:1:9--1:18 Using exhaustive testing. Testing... ERROR for the following inputs: diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout index 182171248..acf1d7522 100644 --- a/tests/issues/issue290v2.icry.stdout +++ b/tests/issues/issue290v2.icry.stdout @@ -4,9 +4,9 @@ Loading module Main [error] at issue290v2.cry:2:1--2:19: Unsolved constraints: - • n`826 == 1 + • n`909 == 1 arising from checking a pattern: type of 1st argument of Main::minMax at issue290v2.cry:2:8--2:11 where - n`826 is signature variable 'n' at issue290v2.cry:1:11--1:12 + n`909 is signature variable 'n' at issue290v2.cry:1:11--1:12 diff --git a/tests/issues/issue723.icry.stdout b/tests/issues/issue723.icry.stdout index a391ffdb8..49332bac7 100644 --- a/tests/issues/issue723.icry.stdout +++ b/tests/issues/issue723.icry.stdout @@ -10,9 +10,9 @@ Loading module Main assuming • fin k the following constraints hold: - • k == n`826 + • k == n`909 arising from matching types at issue723.cry:7:17--7:19 where - n`826 is signature variable 'n' at issue723.cry:1:6--1:7 + n`909 is signature variable 'n' at issue723.cry:1:6--1:7 diff --git a/tests/regression/safety.icry.stdout b/tests/regression/safety.icry.stdout index 7313a61a3..05731e84b 100644 --- a/tests/regression/safety.icry.stdout +++ b/tests/regression/safety.icry.stdout @@ -3,7 +3,7 @@ Counterexample (\x -> assert x "asdf" "asdf") False ~> ERROR Run-time error: asdf -- Backtrace -- -Cryptol::error called at Cryptol:1053:41--1053:46 +Cryptol::error called at Cryptol:1051:41--1051:46 Cryptol::assert called at safety.icry:3:14--3:20 ::it called at safety.icry:3:7--3:37 Counterexample diff --git a/tests/regression/tc-errors.icry.stdout b/tests/regression/tc-errors.icry.stdout index 99e08fda9..93ecff11a 100644 --- a/tests/regression/tc-errors.icry.stdout +++ b/tests/regression/tc-errors.icry.stdout @@ -83,19 +83,19 @@ Loading module Main [error] at tc-errors-5.cry:2:5--2:7: Inferred type is not sufficiently polymorphic. - Quantified variable: a`826 + Quantified variable: a`909 cannot match type: [0]?a When checking the type of 'Main::f' where ?a is type of sequence member at tc-errors-5.cry:2:5--2:7 - a`826 is signature variable 'a' at tc-errors-5.cry:1:6--1:7 + a`909 is signature variable 'a' at tc-errors-5.cry:1:6--1:7 Loading module Cryptol Loading module Main [error] at tc-errors-6.cry:4:7--4:8: The type ?a is not sufficiently polymorphic. - It cannot depend on quantified variables: b`830 + It cannot depend on quantified variables: b`913 When checking the type of 'g' where ?a is the type of 'x' at tc-errors-6.cry:1:3--1:4 - b`830 is signature variable 'b' at tc-errors-6.cry:3:8--3:9 + b`913 is signature variable 'b' at tc-errors-6.cry:3:8--3:9 From b9d76689e35836f2f91581f1fc60d671dac75d3e Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 24 Nov 2021 10:40:07 -0800 Subject: [PATCH 5/5] Update changelog regarding `sortBy` --- CHANGES.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index ade29c41a..d27ab0ff4 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,11 @@ +# NEXT + +## Language changes + +* Update the implementation of the Prelude function `sortBy` to use + a merge sort instead of an insertion sort. This improves the both + asymptotic and observed performance on sorting tasks. + # 2.12.0 ## Language changes