Skip to content

Instantly share code, notes, and snippets.

@sebastiaanvisser
Last active December 22, 2015 01:39
Show Gist options
  • Save sebastiaanvisser/6397813 to your computer and use it in GitHub Desktop.
Save sebastiaanvisser/6397813 to your computer and use it in GitHub Desktop.
Rule domain datatype.
{-# 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)
]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment