Templates for n-ary logic functions

LogicTemplates.hs

{-# LANGUAGE TemplateHaskell #-}

module LogicTemplates (true,
                       false,
                       eq,
                       taut,
                       cont)
    where

import Language.Haskell.TH
import Language.Haskell.TH.Syntax (lift, Lift)


true :: Int -> Q Exp
true = cnst True

false :: Int -> Q Exp
false = cnst False


eq :: Int -> Q Exp
eq n = return $
  LamE [VarP f, VarP g]
       (AppE (VarE (mkName "and"))
             (CompE (bind vars ++ 
                     [NoBindS (InfixE (Just (apply f vars))
                                      (VarE (mkName "=="))
                                      (Just (apply g vars)))])))
    where [f, g] = map mkName ["f", "g"]
          vars   = mkVars n


taut :: Int -> Q Exp
taut n = return $
  LamE [VarP f]
       (AppE (VarE (mkName "and"))
             (CompE (bind vars ++ 
                     [NoBindS (InfixE (Just (apply f vars))
                                      (VarE (mkName "=="))
                                      (Just (ConE (mkName "True"))))])))
    where f    = mkName "f"
          vars = mkVars n


cont :: Int -> Q Exp
cont n = return $
  LamE [VarP f]
       (AppE (VarE (mkName "and"))
             (CompE (bind vars ++ 
                     [NoBindS (InfixE (Just (apply f vars))
                                      (VarE (mkName "=="))
                                      (Just (ConE (mkName "False"))))])))
    where f    = mkName "f"
          vars = mkVars n


cnst :: Lift a => a -> Int -> Q Exp
cnst x n = fmap (LamE ps) $ lift x
    where ps = replicate n WildP

mkVars :: Int -> [Name]
mkVars n = [mkName $ "v" ++ show n | n <- [1..n]]

bind :: [Name] -> [Stmt]
bind = map binding
    where binding var = BindS (VarP var)
                              (ListE [ConE (mkName "True"),
                                      ConE (mkName "False")])

apply :: Name -> [Name] -> Exp
apply f (var:vars) = foldr (\var acc -> AppE acc (VarE var))
                           (AppE (VarE f) (VarE var))
                           vars


-- usage:
--
-- *LogicTemplates> $(taut 1) (\p -> p || not p)
-- True
-- *LogicTemplates> $(taut 1) $(true 1)
-- True
-- *LogicTemplates> $(taut 2) (\p q -> (p && q) || not (p && q))
-- True
-- *LogicTemplates> $(cont 1) (\p -> p && not p)
-- True
-- *LogicTemplates> $(cont 2) $(false 2)
-- True
-- *LogicTemplates> $(eq 2) (\p q -> p && q) (\p q -> not (not p || not q))
-- True