code-conjure-0.7.6: eg/sort.hs

-- sort.hs: conjuring a sort function
--
-- Copyright (C) 2021-2025 Rudy Matela
-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
import Conjure
import Data.List (insert)

sort' :: [Int] -> [Int]
sort' []       =  []
sort' [0]      =  [0]
sort' [1]      =  [1]
sort' [0,2]    =  [0,2]
sort' [1,0]    =  [0,1]
sort' [0,1,2]  =  [0,1,2]
sort' [2,1,0]  =  [0,1,2]
sort' [1,0,1]  =  [0,1,1]
sort' [0,1,0,1]  =  [0,0,1,1]

insert' :: Int -> [Int] -> [Int]
insert' 0 []  =  [0]
insert' 0 [1,2]  =  [0,1,2]
insert' 1 [0,2]  =  [0,1,2]
insert' 2 [0,1]  =  [0,1,2]

merge' :: [Int] -> [Int] -> [Int]
merge' [] []  =  []
merge' [0] []  =  [0]
merge' [] [0]  =  [0]
merge' [0] [1]  =  [0,1]
merge' [1] [0]  =  [0,1]
merge' [1] [0,2]  =  [0,1,2]
merge' [0,2] [1]  =  [0,1,2]
merge' [2] [0,1]  =  [0,1,2]
merge' [0,1] [0,1]  =  [0,0,1,1]
merge' [0,1] [2,3]  =  [0,1,2,3]
merge' [0,2] [1,3]  =  [0,1,2,3]
merge' [0,1] [1,2]  =  [0,1,1,2]
merge' [1,2] [0,1]  =  [0,1,1,2]

main :: IO ()
main = do
  -- an insert function
  conjure "insert" insert'
    [ fun "[]" ([] :: [Int])
    , fun ":" ((:) :: Int -> [Int] -> [Int])
    , fun "<=" ((<=) :: Int -> Int -> Bool)
    , guard
    ]

  -- recursive insertion sort
  conjure "sort" sort'
    [ con ([] :: [Int])
    , fun "insert" (insert :: Int -> [Int] -> [Int])
    ]

  -- folding insertion sort
  conjure "sort" sort'
    [ con ([] :: [Int])
    , fun "insert" (insert :: Int -> [Int] -> [Int])
    , fun "foldr" (foldr :: (Int -> [Int] -> [Int]) -> [Int] -> [Int] -> [Int])
    ]

  -- found!  candidate #309279 @ size 22 after ~11s
  -- merge [] xs  =  xs
  -- merge (x:xs) []  =  x:xs
  -- merge (x:xs) (y:ys)
  --   | x <= y  =  x:merge xs (y:ys)
  --   | otherwise  =  y:merge ys (x:xs)
  -- set target to 360 000 to reach it
  conjure "merge" merge'
    [ con ([] :: [Int])
    , fun ":" ((:) :: Int -> [Int] -> [Int])
    , fun "<=" ((<=) :: Int -> Int -> Bool)
    , guard
    , maxTests 1080
    , target 3600  -- set to 360 000 to reach solution
    ]

  -- Produces a inefficient degenerate version of qsort
  -- where filter is applied _after_ sorting.
  conjure "qsort" sort'
    [ con ([] :: [Int])
    , fun ":" ((:) :: Int -> [Int] -> [Int])
    , fun "++" ((++) :: [Int] -> [Int] -> [Int])
    , fun "<=" ((<=) :: Int -> Int -> Bool)
    , fun ">"  ((>)  :: Int -> Int -> Bool)
    , fun "filter" (filter :: (Int -> Bool) -> [Int] -> [Int])
    -- if we disable the descent requirement and carry on,
    -- we eventually get the efficient qsort
    -- , dontRequireDescent
    -- , carryOn
    ]