Rule domain datatype.

gistfile1.hs

{-# LANGUAGE GADTs #-}
module Test where

type Var = String

type Program = [(String, Expr ())]

data Expr a where
  Intro :: (Expr a -> Expr b) -> Expr ()
  Apply :: Expr (a -> b) -> Expr a -> Expr b
  Var   :: Var          -> Expr a
  Conj  :: Expr Bool -> Expr Bool -> Expr Bool
  Rule  :: Expr Bool -> Expr Bool -> Expr ()

infixl @:
(@:) :: Expr (a -> b) -> Expr a -> Expr b
(@:) = Apply

infixr 2 -:
(-:) :: Expr Bool -> Expr Bool -> Expr ()
(-:) = Rule

infixr 6 &
(&) :: Expr Bool -> Expr Bool -> Expr Bool
(&) = Conj

intro2 :: (Expr a -> Expr b -> Expr d) -> Expr ()
intro2 b = Intro $ \f -> Intro $ \g -> b f g

intro3 :: (Expr a -> Expr b -> Expr c -> Expr d) -> Expr ()
intro3 b = Intro $ \f -> Intro $ \g -> Intro $ \h -> b f g h


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

req :: Expr a -> Expr a -> Expr Bool
req f g = Var "req" @: f @: g

create :: Expr a -> Expr b -> Expr a -> Expr Bool
create f p g = Var "create" @: f @: p @: g

source :: Expr a -> Expr Bool
source f = Var "source" @: f

includes :: Expr a -> Expr a -> Expr Bool
includes f g = Var "includes" @: f @: g

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

req0 :: Expr ()
req0 = Intro $ \f -> req f f -: source f

req1 :: Expr ()
req1 = intro2 $ \f g -> req f g -: includes f g

req2 :: Expr ()
req2 = intro3 $ \f g p -> req f g -: create f p g

req3 :: Expr ()
req3 = intro3 $ \f g h -> req f g -: req f h & req h g

myProgram :: Program
myProgram =
  [ ("req", req0)
  , ("req", req1)
  , ("req", req2)
  , ("req", req3)
  ]