{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts #-}

import Control.Monad.Instances
import Coalgebra
import Search

-- F X = 1 + X
type F = Maybe

-- This will give the fixpoint, ie a coalgebra, because F is a functor
-- There is an element for every natural number, and an infinity element
type Natinfi = Nu F

-- The semantics from the following coalgebra to Natinfi is "the selection function"
-- In some sense this behaviour searches through all natural numbers
-- (searching for a witness x such that p x = True, in contrast to the paper)
instance Coalgebra F (Natinfi -> Bool) where
	psi p
		| p (phi Nothing) == True = Nothing
		| otherwise = Just (\x -> p $ phi $ Just x)

-- http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ says:
-- "What is going on here is that computable functionals are continuous"
-- In this case Natinfi is compact, so any computable predicate is known when we only inverstigate at depth n (for some n)
-- Hence forsome and others will always terminate.
test1 :: Natinfi -> Bool
test1 p = case q of
		Nothing -> False
		Just y -> True
	where q = psi p

test2 :: Natinfi -> Bool
test2 p = case q of
		Nothing -> False
		Just y -> False
	where q = psi p

-- Of course this will not always terminate!
toInt :: Natinfi -> Int
toInt s = case q of
		Nothing -> 0
		Just y -> 1 + toInt y
	where q = psi s

sNatinfi :: Searchable Natinfi
sNatinfi = S (semantics :: (Natinfi -> Bool) -> Natinfi)

output :: (Natinfi -> Bool) -> String
output p
	| forsome sNatinfi p == True = "There is an example, namely: " ++ (show $ toInt $ find sNatinfi p)
	| otherwise = "For all elements p is false"

main :: IO ()
main = do
	putStrLn $ output test1
	putStrLn $ output test2