Merge pull request #1302 from GaloisInc/mergeSort-Prelude

A take at updating Cryptol's sort function from insertion sort to merge sort

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

lib/Cryptol.cry

@@ -964,18 +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 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)) = take zs.0
   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
+    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 -------------------------------------------
 

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

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

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:

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

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

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
 <interactive>::it called at safety.icry:3:7--3:37
 Counterexample

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