{-# LANGUAGE FlexibleContexts      #-}

module SingleExamples where

import Generics.MultiRec.Base
import Generics.MultiRec.Rewriting.Rewriting
import Generics.MultiRec.Rewriting.Rules
--import Generics.MultiRec.Rewriting.AC

import SingleUse
import Single


-- | A rewrite rule for logical expressions.

rule1 :: Logic -> RuleSpec Logic
rule1 p = T :&&: p :~> T

-- | An example expression that matches the rule.

example1 = T :&&: F

-- | Testing generic rewriting

instance Rewrite LogicF

-- Does not type in GHC 6.8.3
testRewriting1 = rewrite Logic (rule Logic rule1) example1

-- | Testing generation of associative/commutative-equivalent terms
example2 = (Var "p" :&&: T) :->: F

-- Produces duplicates (have to test for equality)
example3 = example2 :||: example2

-- Fails to return (T || p || F), for instance
example4 = (Var "p") :||: (T :||: F)

--testAC1 = acTerms Logic [":&&:", ":||:"] example3