-- weird.hs: conjures some weird or unintuitive functions
--
-- Copyright (C) 2025 Rudy Matela
-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
--
-- This file conjures some weird or unintuitive functions.
-- It is here to make sure we do not overprune!
--
-- For simplicity,
-- we do not use partial definitions here.
-- We use fully defined functions to conjure themselves.
import Conjure
import Test.LeanCheck.Error (errorToNothing)
import Data.Maybe (isNothing)
-- | An undefined function.
bottom :: Int
bottom = undefined
-- | A specification for the above undefined function.
bottomSpec :: Int -> [Property]
bottomSpec bottom = [property $ isError bottom]
where
isError = isNothing . errorToNothing -- TODO: add to LeanCheck.Error?
-- | xor for integers
--
-- returns the sum but only when one of the arguments is 0
(^^^) :: Int -> Int -> Int
0 ^^^ y = y
x ^^^ 0 = x
_ ^^^ _ = 0
-- | inc or square based on boolean argument
-- except for 0 where the answer is swapped
isq :: Bool -> Int -> Int
isq False 0 = 0
isq True 0 = 1
isq False x = x + 1
isq True x = x * x
main :: IO ()
main = do
-- We try to ask Conjure to generate undefined
-- Conjure complains about not being able to reify specification.
-- Fair enough: there's no way to distinguish an undefined function
-- from an empty specification.
conjure "bottom" bottom []
-- With a spec, Conjure finds the "implementation"
conjureFromSpec "bottom" bottomSpec []
conjure "isq" isq ingredients
conjure "^^^" (^^^) ingredients
conjure "^^^" (^^^) $ ingredients ++ [singlePattern]
-- This example is quite the degenerate case,
-- it takes a while to conjure even with just 2 ingredients.
-- I am leaving it commented-out for now...
-- conjure "thirty" thirty [pr (0::Int), fun "+" ((+) :: Int -> Int -> Int)]
ingredients :: [Ingredient]
ingredients =
[ con (0::Int)
, con (1::Int)
, fun "+" ((+) :: Int -> Int -> Int)
, fun "*" ((*) :: Int -> Int -> Int)
, fun "==" ((==) :: Int -> Int -> Bool)
, fun "&&" (&&)
, fun "||" (||)
, iif (undefined :: Int)
-- guard does not play well with usePatterns = False yet
]
-- | returns the sum when one of the arguments is 0
--
-- Naming: thirty/30, sum of __3__, when one is __0__
thirty :: Int -> Int -> Int -> Int
thirty 0 y z = y + z
thirty x 0 z = x + z
thirty x y 0 = x + y
thirty x y z = 0