packages feed

regular-0.3.0: examples/Test.hs

{-# LANGUAGE TypeOperators      #-}
{-# LANGUAGE TypeFamilies       #-}
{-# LANGUAGE TemplateHaskell    #-}
{-# LANGUAGE EmptyDataDecls     #-}

module Test where

import Generics.Regular
import Generics.Regular.Functions
import qualified Generics.Regular.Functions.Show as G
import qualified Generics.Regular.Functions.Read as G
import Generics.Regular.Functions.Eq


-- Datatype representing logical expressions
data Logic = Var String
           | Logic :->:  Logic  -- implication
           | Logic :<->: Logic  -- equivalence
           | Logic :&&:  Logic  -- and (conjunction)
           | Logic :||:  Logic  -- or (disjunction)
           | Not Logic          -- not
           | T                  -- true
           | F                  -- false
           deriving Show

-- Instantiating Regular for Logic using TH
$(deriveAll ''Logic "PFLogic")
type instance PF Logic = PFLogic

-- Example logical expressions
l1, l2, l3 :: Logic
l1 = Var "p"
l2 = Not l1
l3 = l1 :->: l2

-- Testing flattening
ex0 :: [Logic]
ex0 = flattenr (from l3)

-- Testing generic equality
ex1, ex2 :: Bool
ex1 = eq l3 l3
ex2 = eq l3 l2

-- Testing generic show
ex3 :: String
ex3 = G.show l3

-- Testing generic read
ex4 :: Logic
ex4 = G.read ex3

-- Testing value generation
ex5, ex6 :: Logic
ex5 = left
ex6 = right

-- Testing folding
ex7 :: Bool
ex7 = fold (alg (\_ -> False)) l3 where
  alg env = (env & impl & (==) & (&&) & (||) & not & True & False)
  impl p q = not p || q

-- Testing unfolding
ex8 :: Int -> Logic
ex8 n = unfold alg n where
  alg :: CoAlgebra Logic Int
  alg n | odd n || n <= 0 = Left ""
        | even n          = Right (Left (n-1,n-2))

-- Testing conNames
ex9 = conNames (undefined :: Logic)