Basic program induction

pinducer.hs

{-# LANGUAGE GADTs #-}
import Control.Monad

-- Basic program inducer
--
-- usage:
-- take 5 $ solve [(1, 2::Int), (2, 3)]
-- => [(+ 1 X),(+ X 1),(+ 0 (+ 1 X)),(+ 0 (+ X 1)),(+ 1 (+ 0 X))]

-- Expressions of the target language
data Expr a where
  X   :: Expr Int
  I   :: Int  -> Expr Int
  B   :: Bool -> Expr Bool
  Add :: Expr Int -> Expr Int -> Expr Int
  Mul :: Expr Int -> Expr Int -> Expr Int
  Eq  :: Expr Int -> Expr Int -> Expr Bool

-- Rules for displaying expressions
instance Show (Expr a) where
  show X = "X"
  show (I n) = show n
  show (B b) = show b
  show (Add x y) = "(+ " ++ show x ++ " " ++ show y ++ ")"
  show (Mul x y) = "(* " ++ show x ++ " " ++ show y ++ ")"
  show (Eq x y) = "(== " ++ show x ++ " " ++ show y ++ ")"

-- Rules for evaluating expressions
eval :: Int -> Expr a -> a
eval x X = x
eval x (I n) = n
eval x (B b) = b
eval x (Add e1 e2) = eval x e1 + eval x e2
eval x (Mul e1 e2) = eval x e1 * eval x e2
eval x (Eq  e1 e2) = eval x e1 == eval x e2

-- check if f(x) = y
check :: (Eq y) => Expr y -> (Int, y) -> Bool
check f (x, y) = eval x f == y

-- check if f(xi) = yi for all i
checkAll :: (Eq y) => Expr y -> [(Int, y)] -> Bool
checkAll f = all (check f)

-- lazy list of programs that have the given input-output restrictions
solve :: (Eq y, Programs y) => [(Int, y)] -> [(Expr y)]
solve graph = lazy 1 where
  lazy n = (do
    program <- programs n
    guard (checkAll program graph)
    [program]) ++ lazy (n + 1)

-- class for creating programs that return this type
class Programs a where
  programs :: Int -> [Expr a]

-- programs with a given number of terms that return integers
instance Programs Int where
  programs 1 = [(I 0), (I 1), X]
  programs n = do
    k <- [1..(n-1)]
    lexpr <- programs k
    rexpr <- programs (n - k)
    [Add lexpr rexpr, Mul lexpr rexpr]

-- programs with a given number of terms that return boolean values
instance Programs Bool where
  programs 1 = [(B True), (B False)]
  programs n = do
    k <- [1..(n-1)]
    lexpr <- programs k
    rexpr <- programs (n - k)
    [Eq lexpr rexpr]