{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, NoMonomorphismRestriction #-}
import Prelude hiding ((.),id)
import Control.Category
import Control.Monad
import Control.Monad.Identity
import Control.Arrow

import Data.List

data (Monad m) => Hoar m a b = Hoar {
    action :: a -> m b,
    preconds :: [a -> Bool],
    postconds :: [b -> Bool] }

test :: [a -> Bool] -> a -> Bool
test fns x = all id $ ap fns [x]

hoar ::  (Monad m) => Hoar m a b -> a -> m b
hoar h x = if test (preconds h) x
             then do
                    y <- (action h) x
                    if test (postconds h) y
                       then return y
                       else fail "Postconditions failed"
              else fail "Preconditions failed"

hid ::  (Monad m) => Hoar m a a
hid = Hoar (return . id) [] []

instance (Monad m) => Category (Hoar m) where
    id = hid
    h1 . h2 = Hoar fg (preconds h2) (postconds h1)
        where
          fg = \x -> do
            y <- hoar h2 x
            hoar h1 y

instance (Monad m) => Arrow (Hoar m) where
    arr f = Hoar (return.f) [] []
    first (Hoar f p q) = Hoar f' p' q'
        where f' (b,d) = do
                  y <- f b
                  return (y,d)
              one f = fst.(first f)
              p' = map one p
              q' = map one q

-------------------------------------------------------------

sorted ::  (Ord a) => [a] -> Bool
sorted lst = lst == sort lst

hoarSort ::  (Monad m, Ord a) => Hoar m [a] [a]
hoarSort = Hoar {
    action = return.sort,
--     action = return,
    preconds = [],
    postconds = [sorted]
    }

main = do
    res <- hoar hoarSort [3,2,5,12,1]
    print res