{-# LANGUAGE FlexibleContexts      #-}

module SingleExamples where

import Generics.MultiRec.Base
import Generics.MultiRec.Rewriting.Rewriting
import Generics.MultiRec.Rewriting.Rules
import Generics.MultiRec.Rewriting.Strategies

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

testRewriting1 = rewrite Logic (rule Logic rule1) example1

-- | Example expression for testing strategies
example2 = (Var "p" :&&: T) :->: (Var "p" :&&: T) :->: F

-- | Example rule for testing strategies
rule2 p = (p :&&: T) :~> T

-- | Does not apply at top level
testRewriting2 = rewrite Logic (rule Logic rule2) example2

-- | Applies the rule at most once
testStrategy1 = once f Logic example2 where
  f :: LogicF ix -> ix -> Maybe ix
  f Logic = rewriteM Logic (rule Logic rule2)

-- | Applies the rule whenever possible
testStrategy2 = topdown f Logic example2 where
  f :: LogicF ix -> ix -> ix
  f Logic = rewrite Logic (rule Logic rule2)