Hutton.hs

 {-# LANGUAGE FlexibleInstances, RankNTypes #-}

module Hutton where

import Test.QuickCheck

-- Hutton's razor
--
data Expr = Val Integer
          | Expr `Add` Expr
      deriving Show

-- interpreter (i.e. semantics)
--
eval :: Expr -> Integer
eval (Val n) = n
eval (m `Add` n) = eval m + eval n

-- constructive induction
--
--eval' :: Expr -> (Integer -> Integer) -> Integer
eval' :: Expr -> ({-forall k .-} (Integer -> k) -> k)





eval' (m `Add` n) c = eval' m c''
  where c'' em = eval' n (c . (em +))
{-
eval' (m `Add` n) c = eval' n (c . (eval m +))
  where c'' em = eval' n (c . (em +))
        
eval' (m `Add` n) c = eval' n (c . (eval m +))

eval' (m `Add` n) c = c' (eval n)
  where c' = c . (eval m +)

eval' (m `Add` n) c = c' (eval n)
  where c' = c . (eval m +)

eval' (m `Add` n) c = c (eval m + eval n)
-}
eval' (Val n) c = c n

--eval' e c = c (eval e) -- (OWK)

-- eval e = eval' e (\x->x)

data CONT = HALT
          | NEXT Expr CONT
          | ADD Integer CONT

-- constructive induction
--
eval'' :: Expr -> (CONT -> Integer)

eval'' (m `Add` n) st = eval'' m (NEXT n st)
{-
eval'' (m `Add` n) st = exec (NEXT n st) (eval m)

eval'' (m `Add` n) st =     eval'' n (ADD (eval m) st)
  where exec (NEXT y c) n = eval'' y (ADD n        c )

eval'' (m `Add` n) st = eval'' n (ADD (eval m) st)

eval'' (m `Add` n) st = exec (ADD (eval m) st) (eval n)

eval'' (m `Add` n) st = exec st (eval m + eval n)
  where exec (ADD n c) m = exec c (m + n)
eval'' (m `Add` n) st = exec st (eval (m `Add` n))
-}
eval'' (Val n) st = (exec st) n


eval'' e st = (exec st) (eval e) -- (OWK)

exec :: CONT -> (Integer -> Integer)
exec HALT n = n
exec (NEXT y c) n = eval'' y (ADD n c) --next y (exec c)
               --where next y c n = eval'' y (ADD n c) 
exec (ADD n c) m = exec c (n + m)

-- TEST
--
prop_eval :: Expr -> (Integer -> Integer) -> Property
prop_eval e c = eval' e c === c (eval e)

--prop_eval'' :: Expr -> (CONT Integer) -> Property
--prop_eval'' e = eval'' e HALT === exec HALT (eval e)

test = quickCheck prop_eval

instance Arbitrary Expr where
  arbitrary = frequency [ (3, Val <$> arbitrary)
                        , (2, Add <$> arbitrary <*> arbitrary) ]

instance Show (Integer -> Integer) where
  show _ = "<some continuation>"


--comp ast = \inp -> interpr ast inp