rewriting 0.1 → 0.2
raw patch · 16 files changed
+909/−416 lines, 16 filesdep +regulardep ~basenew-uploader
Dependencies added: regular
Dependency ranges changed: base
Files
- LICENSE +1/−1
- examples/expr/Expr.expected +11/−0
- examples/expr/Expr.hs +141/−0
- examples/expr/run +1/−0
- examples/logic/Logic.hs +310/−0
- examples/logic/LogicGenerator.hs +9/−0
- examples/logic/LogicRules.hs +237/−0
- examples/logic/LogicStrategies.hs +90/−0
- examples/logic/run +1/−0
- rewriting.cabal +13/−4
- src/Generics/Regular/Rewriting.hs +53/−54
- src/Generics/Regular/Rewriting/Base.hs +5/−260
- src/Generics/Regular/Rewriting/Machinery.hs +9/−8
- src/Generics/Regular/Rewriting/Representations.hs +5/−68
- src/Generics/Regular/Rewriting/Rules.hs +10/−8
- src/Generics/Regular/Rewriting/Strategies.hs +13/−13
LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2008 Universiteit Utrecht+Copyright (c) 2009 Universiteit Utrecht All rights reserved. Redistribution and use in source and binary forms, with or without modification,
+ examples/expr/Expr.expected view
@@ -0,0 +1,11 @@+test1: Just (Const 2)+test2: Nothing+test3: Nothing+test4: Just (Const 2 :*: Const 4)+test5: Just (Const 4 :*: Const 2)+test6: Nothing+test7: Just (Const 4 :*: Const 2 :+: Const 7)+test8: Just (Const 2 :+: Const 1)+test9: Just (Const 2 :*: Const 3 :+: Const 2 :*: Const 4)+test10: Just (Const 1 :*: Const 2 :+: Const 1 :*: Const 3)+test11: Just (Const 2)
+ examples/expr/Expr.hs view
@@ -0,0 +1,141 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++import Generics.Regular.Rewriting+++-----------------------------------------------------------------------------+-- Types and conversions+-----------------------------------------------------------------------------++infixl 7 :**:+infixl 6 :++:++data Expr = Const Int | Expr :++: Expr | Expr :**: Expr deriving Show++type instance PF Expr = K Int :+: I :*: I :+: I :*: I+instance Regular Expr where+ from (Const n) = L (K n)+ from (e1 :++: e2) = R (L $ (I e1) :*: (I e2))+ from (e1 :**: e2) = R (R $ (I e1) :*: (I e2))++ to (L (K n)) = Const n+ to (R (L ((I r1) :*: (I r2)))) = r1 :++: r2+ to (R (R ((I r1) :*: (I r2)))) = r1 :**: r2++{-+ -- with Con type constructors to specify constructor names.+instance Regular Expr where+ type PF Expr = Con (K Int) :+: Con (I :*: I) :+: Con (I :*: I)++ from (Const n) = L (Con "Const" (K n))+ from (e1 :++: e2) = R (L (Con "(:++:)" $ (I e1) :*: (I e2)))+ from (e1 :**: e2) = R (R (Con "(:**:)" $ (I e1) :*: (I e2)))++ to (L (Con _ (K n))) = Const n+ to (R (L (Con _ ((I r1) :*: (I r2))))) = r1 :++: r2+ to (R (R (Con _ ((I r1) :*: (I r2))))) = r1 :**: r2+-}++instance Rewrite Expr++-----------------------------------------------------------------------------+-- Example rules+-----------------------------------------------------------------------------++rule1 :: Rule Expr+rule1 = + rule $ \x -> x :++: Const 0 :~>+ x++rule2 :: Rule Expr+rule2 = + rule $ \x -> x :++: x :~> + Const 2 :**: x++rule3 :: Rule Expr+rule3 =+ rule $ \x y -> x :++: y :~> + y :++: x++rule4 :: Rule Expr+rule4 = + rule $ \x y -> Const 2 :**: (x :++: y) :~>+ (Const 2 :**: x) :++: (Const 2 :**: y)++rule5 :: Rule Expr+rule5 = + rule $ \x y z -> x :**: (y :++: z) :~> + (x :**: y) :++: (x :**: z) ++rule6 :: Rule Expr+rule6 = + rule $ Const 1 :++: Const 1 :~>+ Const 2+++-----------------------------------------------------------------------------+-- Tests+-----------------------------------------------------------------------------++test1 :: Maybe Expr+test1 = rewriteM rule1 (Const 2 :++: Const 0)++test2 :: Maybe Expr+test2 = rewriteM rule1 (Const 2 :++: Const 3)++test3 :: Maybe Expr+test3 = rewriteM rule2 (Const 4 :++: Const 3)++test4 :: Maybe Expr+test4 = rewriteM rule2 (Const 4 :++: Const 4)++test5 :: Maybe Expr+test5 = one (rewriteM rule1) ((Const 4 :++: Const 0) :**: Const 2)++-- This does not work because the optimisation target is not+-- an immediate child.+test6 :: Maybe Expr+test6 = one (rewriteM rule1) (((Const 4 :++: Const 0) :**: Const 2) :++: Const 7)++-- This works well, because once applies the rule to the optimisation+-- target exactly once.+test7 :: Maybe Expr+test7 = once (rewriteM rule1) (((Const 4 :++: Const 0) :**: Const 2) :++: Const 7)++test8 :: Maybe Expr+test8 = rewriteM rule3 ((Const 1) :++: (Const 2))++test9 :: Maybe Expr+test9 = rewriteM rule4 ((Const 2) :**: ((Const 3) :++: (Const 4)))++test10 :: Maybe Expr+test10 = rewriteM rule5 ((Const 1) :**: ((Const 2) :++: (Const 3)))++test11 :: Maybe Expr+test11 = rewriteM rule6 (Const 1 :++: Const 1)++allTests :: [Maybe Expr]+allTests = [ test1+ , test2+ , test3+ , test4+ , test5+ , test6+ , test7+ , test8+ , test9+ , test10+ , test11+ ]+++-----------------------------------------------------------------------------+-- Running all the tests+-----------------------------------------------------------------------------++-- This main function is defined to solve a bug in GHC+main :: IO ()+main = do let resultsPP = zipWith resultPP [1..] allTests+ resultPP n result = "test" ++ show n ++ ": " ++ show result+ putStr (unlines resultsPP)
+ examples/expr/run view
@@ -0,0 +1,1 @@+ghci Expr.hs -i../../src/
+ examples/logic/Logic.hs view
@@ -0,0 +1,310 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++-----------------------------------------------------------------------------+-- Copyright 2008, Open Universiteit Nederland. This file is distributed +-- under the terms of the GNU General Public License. For more information, +-- see the file "LICENSE.txt", which is included in the distribution.+-----------------------------------------------------------------------------+-- |+-- Maintainer : bastiaan.heeren@ou.nl+-- Stability : provisional+-- Portability : portable (depends on ghc)+--+-----------------------------------------------------------------------------+module Logic (Logic(..), isDNF, foldLogic, size, height, metaVars, matchLogic, (|->)) where++import Data.List+import Data.Maybe+import qualified Data.Set as S+import qualified Data.Map as M+import Test.QuickCheck+import Control.Monad+import Data.Char++import Generics.Regular.Rewriting++infixr 1 :<->:+infixr 2 :->: +infixr 3 :||: +infixr 4 :&&:++-- | The data type Logic is the abstract syntax for the domain+-- | of logic 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, Eq, Ord)++-- | The type LogicAlg is the algebra for the data type Logic+-- | Used in the fold for Logic.+type LogicAlg a = (String -> a, a -> a -> a, a -> a -> a, a -> a -> a, a -> a -> a, a -> a, a, a)++-- | foldLogic is the standard fold for Logic.+foldLogic :: LogicAlg a -> Logic -> a+foldLogic (var, impl, equiv, and, or, not, true, false) = rec+ where+ rec logic = + case logic of+ Var x -> var x+ p :->: q -> rec p `impl` rec q+ p :<->: q -> rec p `equiv` rec q+ p :&&: q -> rec p `and` rec q+ p :||: q -> rec p `or` rec q+ Not p -> not (rec p)+ T -> true + F -> false+ +-- | evalLogic takes a function that gives a logic value to a variable,+-- | and a Logic expression, and evaluates the boolean expression.+evalLogic :: (String -> Bool) -> Logic -> Bool+evalLogic env = foldLogic (env, impl, (==), (&&), (||), not, True, False)+ where+ impl p q = not p || q++-- | eqLogic determines whether or not two Logic expression are logically +-- | equal, by evaluating the logic expressions on all valuations.+eqLogic p q = all (\f -> evalLogic f p == evalLogic f q) fs+ where + xs = varsLogic p `union` varsLogic q+ fs = map (flip elem) (subsets xs) ++ subsets :: [a] -> [[a]]+ subsets = foldr op [[]]+ where op a list = list ++ map (a:) list++-- | Functions noNot, noOr, and noAnd determine whether or not a Logic +-- | expression contains a not, or, and and constructor, respectively.+noNot, noOr, noAnd :: Logic -> Bool+noNot = foldLogic (const True, (&&), (&&), (&&), (&&), const False, True, True)+noOr = foldLogic (const True, (&&), (&&), (&&), \_ _ -> False, id, True, True)+noAnd = foldLogic (const True, (&&), (&&), \_ _ -> False, (&&), id, True, True)++-- | A Logic expression is atomic if it is a variable or a constant True or False.+isAtomic :: Logic -> Bool+isAtomic logic = + case logic of+ Var _ -> True+ Not (Var _) -> True+ _ -> False++-- | Functions isDNF, and isCNF determine whether or not a Logix expression+-- | is in disjunctive normal form, or conjunctive normal form, respectively. +isDNF, isCNF :: Logic -> Bool+isDNF = all isAtomic . concatMap conjunctions . disjunctions+isCNF = all isAtomic . concatMap disjunctions . conjunctions++-- | Function disjunctions returns all Logic expressions separated by an or+-- | operator at the top level.+disjunctions :: Logic -> [Logic]+disjunctions F = []+disjunctions (p :||: q) = disjunctions p ++ disjunctions q+disjunctions logic = [logic]++-- | Function conjunctions returns all Logic expressions separated by an and+-- | operator at the top level.+conjunctions :: Logic -> [Logic]+conjunctions T = []+conjunctions (p :&&: q) = conjunctions p ++ conjunctions q+conjunctions logic = [logic]++size :: Logic -> Int+size = foldLogic (const 1, bin, bin, bin, bin, succ, 1, 1)+ where bin x y = x+y+1++height :: Logic -> Int+height = foldLogic (const 1, bin, bin, bin, bin, succ, 1, 1)+ where bin x y = 1 + (x `max` y)+ +-- | Count the number of implicationsations :: Logic -> Int+countImplications :: Logic -> Int+countImplications = foldLogic (const 0, \x y -> x+y+1, (+), (+), (+), id, 0, 0)+ +-- | Count the number of equivalences+countEquivalences :: Logic -> Int+countEquivalences = foldLogic (const 0, (+), \x y -> x+y+1, (+), (+), id, 0, 0)++-- | Count the number of binary operators+countBinaryOperators :: Logic -> Int+countBinaryOperators = foldLogic (const 0, binop, binop, binop, binop, id, 0, 0)+ where binop x y = x + y + 1++-- | Count the number of double negations +countDoubleNegations :: Logic -> Int+countDoubleNegations = fst . foldLogic (const zero, bin, bin, bin, bin, notf, zero, zero)+ where+ zero = (0, False)+ bin (n, _) (m, _) = (n+m, False)+ notf (n, b) = if b then (n+1, False) else (n, True)++-- | Function varsLogic returns the variables that appear in a Logic expression.+varsLogic :: Logic -> [String]+varsLogic = foldLogic (return, union, union, union, union, id, [], []) ++test = associativityAnd $ (Var "a" :||: Var "b") :||: (Var "c" :||: Var "d" :||: Var "e")++associativityAnd, associativityOr :: Logic -> [Logic]+associativityAnd = associativity conjunctions (:&&:) [T]+associativityOr = associativity disjunctions (:||:) [F]++-- Helper function (polymorphic, domain independent)+associativity :: (a -> [a]) -> (a -> a -> a) -> [a] -> a -> [a]+associativity f op nil = rec . f+ where+ rec ps+ | n == 0 = nil+ | n == 1 = ps+ | otherwise = concatMap f [1 .. n-1]+ where+ n = length ps+ f i = let (xs, ys) = splitAt i ps+ in [ x `op` y | x <- rec xs, y <- rec ys ]++eqAssociative :: Logic -> Logic -> Bool+eqAssociative p q =+ case (p, q) of+ (Var x, Var y) -> x==y+ (p1 :->: p2, q1 :->: q2) -> eqAssociative p1 q1 && eqAssociative p2 q2+ (p1 :<->: p2, q1 :<->: q2) -> eqAssociative p1 q1 && eqAssociative p2 q2+ (_ :&&: _, _ :&&: _) -> and $ zipWith eqAssociative (conjunctions p) (conjunctions q)+ (_ :||: _, _ :||: _) -> and $ zipWith eqAssociative (disjunctions p) (disjunctions q)+ (Not p1, Not q1 ) -> eqAssociative p1 q1+ (T, T ) -> True+ (F, F ) -> True+ _ -> False++-- sized, no nested equivalences+-- arbLogic :: Bool -> Int -> Gen Logic+arbLogic b n+ | n <= 1 = frequency+ [ (1, oneof $ map return [F, T])+ , (3, oneof $ map (return . Var) ["p", "q", "r"])+ ]+ | otherwise = frequency+ [ (4, arbLogic b 0)+ , (2, bin (:->:))+ , (i, liftM2 (:<->:) recF recF)+ , (3, bin (:&&:))+ , (3, bin (:||:))+ , (3, liftM Not rec)+ ]+ where+ i = if b then 1 else 0+ rec = arbLogic b (n `div` 2)+ recF = arbLogic False (n `div` 2)+ bin f = liftM2 f rec rec++-----------------------------------------------------------+--- Unification++type Substitution = M.Map Char Logic++isMetaVar :: Logic -> Maybe Char+isMetaVar (Var ['_', c]) = Just c+isMetaVar _ = Nothing++metaVars :: [Logic]+metaVars = [ Var ['_', c] | c <- ['a' .. 'z'] ]++(|->) :: Substitution -> Logic -> Logic+(|->) sub = foldLogic (var, (:->:), (:<->:), (:&&:), (:||:), Not, T, F)+ where + var s = case isMetaVar (Var s) of+ Just i -> fromMaybe (Var s) (M.lookup i sub)+ _ -> Var s++matchLogic :: Logic -> Logic -> Maybe Substitution+matchLogic p q =+ case isMetaVar p of+ Just i -> return (M.singleton i q)+ Nothing ->+ case (p, q) of+ (Var x, Var y) | x==y -> return M.empty+ (p1 :->: p2, q1 :->: q2) -> matchPairs (p1, p2) (q1, q2)+ (p1 :<->: p2, q1 :<->: q2) -> matchPairs (p1, p2) (q1, q2)+ (p1 :&&: p2, q1 :&&: q2 ) -> matchPairs (p1, p2) (q1, q2)+ (p1 :||: p2, q1 :||: q2 ) -> matchPairs (p1, p2) (q1, q2)+ (Not p1, Not q1 ) -> matchLogic p1 q1+ (T, T ) -> return M.empty+ (F, F ) -> return M.empty+ _ -> Nothing+ where+ matchPairs :: (Logic, Logic) -> (Logic, Logic) -> Maybe Substitution+ matchPairs (x1, x2) (y1, y2) = do+ s1 <- matchLogic x1 y1+ s2 <- matchLogic (s1 |-> x2) y2+ return (M.union s1 s2)+++-----------------------------------------------------------+--- QuickCheck generator++instance Arbitrary Logic where+ arbitrary = sized (arbLogic True)+ coarbitrary logic = + case logic of+ Var x -> variant 0 . coarbitrary (map ord x)+ p :->: q -> variant 1 . coarbitrary p . coarbitrary q+ p :<->: q -> variant 2 . coarbitrary p . coarbitrary q+ p :&&: q -> variant 3 . coarbitrary p . coarbitrary q+ p :||: q -> variant 4 . coarbitrary p . coarbitrary q+ Not p -> variant 5 . coarbitrary p+ T -> variant 6 + F -> variant 7++#ifdef FixView+type instance PF Logic =+ (((K String) :+: I :*: I) :+: (I :*: I :+: I :*: I))+ :+:+ ((I :*: I :+: I) :+: (U :+: U))++instance Regular Logic where+ from (Var x) = L (L (L (K x)))+ from (p :<->: q) = L (L (R ((I (from p)) :*: (I (from q)))))+ from (p :->: q) = L (R (L ((I (from p)) :*: (I (from q)))))+ from (p :&&: q) = L (R (R ((I (from p)) :*: (I (from q)))))+ from (p :||: q) = R (L (L ((I (from p)) :*: (I (from q)))))+ from (Not p) = R (L (R (I (from p))))+ from T = R (R (L U))+ from F = R (R (R U))++ to (L (L (L (K x)))) = Var x+ to (L (L (R ((I p) :*: (I q))))) = to p :<->: to q+ to (L (R (L ((I p) :*: (I q))))) = to p :->: to q+ to (L (R (R ((I p) :*: (I q))))) = to p :&&: to q+ to (R (L (L ((I p) :*: (I q))))) = to p :||: to q+ to (R (L (R (I p)))) = Not (to p)+ to (R (R (L U))) = T+ to (R (R (R U))) = F+#else+type instance PF Logic =+ (((K String) :+: I :*: I) :+: (I :*: I :+: I :*: I))+ :+:+ ((I :*: I :+: I) :+: (U :+: U))++instance Regular Logic where+ from (Var x) = L (L (L (K x)))+ from (p :<->: q) = L (L (R ((I p) :*: (I q))))+ from (p :->: q) = L (R (L ((I p) :*: (I q))))+ from (p :&&: q) = L (R (R ((I p) :*: (I q))))+ from (p :||: q) = R (L (L ((I p) :*: (I q))))+ from (Not p) = R (L (R (I p)))+ from T = R (R (L U))+ from F = R (R (R U))++ to (L (L (L (K x)))) = Var x+ to (L (L (R ((I p) :*: (I q))))) = p :<->: q+ to (L (R (L ((I p) :*: (I q))))) = p :->: q+ to (L (R (R ((I p) :*: (I q))))) = p :&&: q+ to (R (L (L ((I p) :*: (I q))))) = p :||: q+ to (R (L (R (I p)))) = Not p+ to (R (R (L U))) = T+ to (R (R (R U))) = F+#endif++instance Rewrite Logic
+ examples/logic/LogicGenerator.hs view
@@ -0,0 +1,9 @@+module LogicGenerator () where + +import Control.Monad +import Data.Char +import System.Random +import Test.QuickCheck hiding (defaultConfig) ++import Logic +
+ examples/logic/LogicRules.hs view
@@ -0,0 +1,237 @@+----------------------------------------------------------------------------- +-- Copyright 2008, Open Universiteit Nederland. This file is distributed +-- under the terms of the GNU General Public License. For more information, +-- see the file "LICENSE.txt", which is included in the distribution. +----------------------------------------------------------------------------- +-- | +-- Maintainer : bastiaan.heeren@ou.nl +-- Stability : provisional +-- Portability : portable (depends on ghc) +-- +----------------------------------------------------------------------------- +module LogicRules where + +import qualified Data.Set as S +import Logic +import Generics.Regular.Rewriting+ +p |- q = p :~> q +makeRuleList _ = map rule +buggyRule = id +makeRule _ = rule + +{- +logicRules :: [LogicRule] +logicRules = [ ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd+ , ruleFalseZeroAnd, ruleDeMorganOr, ruleDeMorganAnd + , ruleNotBoolConst, ruleNotNot, ruleAndOverOr, ruleOrOverAnd + , ruleDefImpl, ruleDefEquiv + , ruleFalseInEquiv, ruleTrueInEquiv, ruleFalseInImpl+ , ruleTrueInImpl + , ruleComplOr, ruleComplAnd + , ruleIdempOr, ruleIdempAnd + , ruleAbsorpOr, ruleAbsorpAnd + , ruleCommOr, ruleCommAnd + ] + +logicBuggyRules :: [LogicRule] +logicBuggyRules = [ buggyRuleCommImp, buggyRuleAssImp] +-}++-- This main function is defined to solve a bug in GHC +main :: IO ()+main = do let resultsPP = zipWith undefined [1..] ([] :: [Logic])+ putStr (unlines resultsPP) + +ruleComplOr :: [Rule Logic] +ruleComplOr = makeRuleList "ComplOr" + [ \x -> (x :||: Not x) |- T + , \x -> (Not x :||: x) |- T + ] + +ruleComplAnd :: [Rule Logic] +ruleComplAnd = makeRuleList "ComplAnd" + [ \x -> (x :&&: Not x) |- F + , \x -> (Not x :&&: x) |- F + ] + +ruleDefImpl :: Rule Logic +ruleDefImpl = makeRule "DefImpl" $ + \x y -> (x :->: y) |- (Not x :||: y) + +ruleDefEquiv :: Rule Logic +ruleDefEquiv = makeRule "DefEquiv" $ + \x y -> (x :<->: y) |- ((x :&&: y) :||: (Not x :&&: Not y)) + +ruleFalseInEquiv :: [Rule Logic] +ruleFalseInEquiv = makeRuleList "FalseInEquiv" + [ \x -> (F :<->: x) |- (Not x) + , \x -> (x :<->: F) |- (Not x) + ] + +ruleTrueInEquiv :: [Rule Logic] +ruleTrueInEquiv = makeRuleList "TrueInEquiv" + [ \x -> (T :<->: x) |- x + , \x -> (x :<->: T) |- x + ] + +ruleFalseInImpl :: [Rule Logic] +ruleFalseInImpl = makeRuleList "FalseInImpl" + [ \x -> (F :->: x) |- T + , \x -> (x :->: F) |- (Not x) + ] + +ruleTrueInImpl :: [Rule Logic] +ruleTrueInImpl = makeRuleList "TrueInImpl" + [ \x -> (T :->: x) |- x + , \x -> (x :->: T) |- T + ] + +ruleFalseZeroOr :: [Rule Logic] +ruleFalseZeroOr = makeRuleList "FalseZeroOr" + [ \x -> (F :||: x) |- x + , \x -> (x :||: F) |- x + ] + +ruleTrueZeroOr :: [Rule Logic] +ruleTrueZeroOr = makeRuleList "TrueZeroOr" + [ \x -> (T :||: x) |- T + , \x -> (x :||: T) |- T + ] + +ruleTrueZeroAnd :: [Rule Logic] +ruleTrueZeroAnd = makeRuleList "TrueZeroAnd" + [ \x -> (T :&&: x) |- x + , \x -> (x :&&: T) |- x + ] + +ruleFalseZeroAnd :: [Rule Logic] +ruleFalseZeroAnd = makeRuleList "FalseZeroAnd" + [ \x -> (F :&&: x) |- F + , \x -> (x :&&: F) |- F + ] + +ruleDeMorganOr :: Rule Logic +ruleDeMorganOr = makeRule "DeMorganOr" $ + \x y -> (Not (x :||: y)) |- (Not x :&&: Not y) + +ruleDeMorganAnd :: Rule Logic +ruleDeMorganAnd = makeRule "DeMorganAnd" $ + \x y -> (Not (x :&&: y)) |- (Not x :||: Not y) + +ruleNotBoolConst :: [Rule Logic] +ruleNotBoolConst = makeRuleList "NotBoolConst" + [ (Not T) |- F + , (Not F) |- T + ] + +ruleNotNot :: Rule Logic +ruleNotNot = makeRule "NotNot" $ + \x -> (Not (Not x)) |- x + +ruleAndOverOr :: [Rule Logic] +ruleAndOverOr = makeRuleList "AndOverOr" + [ \x y z -> (x :&&: (y :||: z)) |- ((x :&&: y) :||: (x :&&: z)) + , \x y z -> ((x :||: y) :&&: z) |- ((x :&&: z) :||: (y :&&: z)) + ] + +ruleOrOverAnd :: [Rule Logic] +ruleOrOverAnd = makeRuleList "OrOverAnd" + [ \x y z -> (x :||: (y :&&: z)) |- ((x :||: y) :&&: (x :||: z)) + , \x y z -> ((x :&&: y) :||: z) |- ((x :||: z) :&&: (y :||: z)) + ] + +ruleIdempOr :: Rule Logic +ruleIdempOr = makeRule "IdempOr" $ + \x -> (x :||: x) |- x + + +ruleIdempAnd :: Rule Logic +ruleIdempAnd = makeRule "IdempAnd" $ + \x -> (x :&&: x) |- x + + +ruleAbsorpOr :: Rule Logic +ruleAbsorpOr = makeRule "AbsorpOr" $ + \x y -> (x :||: (x :&&: y)) |- x + + +ruleAbsorpAnd :: Rule Logic +ruleAbsorpAnd = makeRule "AbsorpAnd" $ + \x y -> (x :&&: (x :||: y)) |- x + +ruleCommOr :: Rule Logic +ruleCommOr = makeRule "CommOr" $ + \x y -> (x :||: y) |- (y :||: x) + + +ruleCommAnd :: Rule Logic +ruleCommAnd = makeRule "CommAnd" $ + \x y -> (x :&&: y) |- (y :&&: x) + + +-- Buggy rules:+ +buggyRuleCommImp :: Rule Logic +buggyRuleCommImp = buggyRule $ makeRule "CommImp" $ + \x y -> (x :->: y) |- (y :->: x) --this does not hold: T->T => T->x + + +buggyRuleAssImp :: [Rule Logic] +buggyRuleAssImp = buggyRule $ makeRuleList "AssImp" + [ \x y z -> (x :->: (y :->: z)) |- ((x :->: y) :->: z) + , \x y z -> ((x :->: y) :->: z) |- (x :->: (y :->: z)) + ] + +buggyRuleIdemImp :: Rule Logic +buggyRuleIdemImp = buggyRule $ makeRule "IdemImp" $ + \x -> (x :->: x) |- x + +buggyRuleIdemEqui :: Rule Logic +buggyRuleIdemEqui = buggyRule $ makeRule "IdemEqui" $ + \x -> (x :<->: x) |- x + +buggyRuleEquivElim :: [Rule Logic] +buggyRuleEquivElim = buggyRule $ makeRuleList "BuggyEquivElim" + [ \x y -> (x :<->: y) |- ((x :&&: y) :||: Not (x :&&: y)) + , \x y -> (x :<->: y) |- ((x :||: y) :&&: (Not x :||: Not y)) + , \x y -> (x :<->: y) |- ((x :&&: y) :||: (Not x :&&: y)) + , \x y -> (x :<->: y) |- ((x :&&: y) :||: ( x :&&: Not y)) + , \x y -> (x :<->: y) |- ((x :&&: y) :&&: (Not x :&&: Not y)) + ] + +buggyRuleImplElim :: Rule Logic +buggyRuleImplElim = buggyRule $ makeRule "BuggyImplElim" $ + \x y -> (x :->: y) |- Not (x :||: y) + +buggyRuleDeMorgan :: [Rule Logic] +buggyRuleDeMorgan = buggyRule $ makeRuleList "BuggyDeMorgan" + [ \x y -> (Not (x :&&: y)) |- (Not x :||: y) + , \x y -> (Not (x :&&: y)) |- (x :||: Not y) + , \x y -> (Not (x :&&: y)) |- (Not (Not x :||: Not y)) + , \x y -> (Not (x :||: y)) |- (Not x :&&: y) + , \x y -> (Not (x :||: y)) |- (x :&&: Not y) + , \x y -> (Not (x :||: y)) |- (Not (Not x :&&: Not y)) + ] +buggyRuleNotOverImpl :: Rule Logic +buggyRuleNotOverImpl = buggyRule $ makeRule "BuggyNotOverImpl" $ + \x y -> (Not(x :->: y)) |- (Not x :->: Not y) + +buggyRuleParenth :: [Rule Logic] +buggyRuleParenth = buggyRule $ makeRuleList "BuggyParenth" + [ \x y -> (Not (x :&&: y)) |- (Not x :&&: y) + , \x y -> (Not (x :||: y)) |- (Not x :||: y) + , \x y -> (Not (x :<->: y)) |- (Not(x :&&: y) :||: (Not x :&&: Not y)) + , \x y -> (Not(Not x :&&: y)) |- (x :&&: y) + , \x y -> (Not(Not x :||: y)) |- (x :||: y) + , \x y -> (Not(Not x :->: y)) |- (x :->: y) + , \x y -> (Not(Not x :<->: y)) |- (x :<->: y) + ] + +buggyRuleAssoc :: [Rule Logic] +buggyRuleAssoc = buggyRule $ makeRuleList "BuggyAssoc" + [ \x y z -> (x :||: (y :&&: z)) |- ((x :||: y) :&&: z) + , \x y z -> ((x :||: y) :&&: z) |- (x :||: (y :&&: z)) + , \x y z -> ((x :&&: y) :||: z) |- (x :&&: (y :||: z)) + , \x y z -> (x :&&: (y :||: z)) |- ((x :&&: y) :||: z) + ]
+ examples/logic/LogicStrategies.hs view
@@ -0,0 +1,90 @@+{-# LANGUAGE FlexibleContexts #-}+-----------------------------------------------------------------------------+-- Copyright 2008, Open Universiteit Nederland. This file is distributed +-- under the terms of the GNU General Public License. For more information, +-- see the file "LICENSE.txt", which is included in the distribution.+-----------------------------------------------------------------------------+-- |+-- Maintainer : bastiaan.heeren@ou.nl+-- Stability : provisional+-- Portability : portable (depends on ghc)+--+-----------------------------------------------------------------------------+module LogicStrategies where++import Prelude hiding (repeat)+import Logic+import LogicRules hiding (main)+import System.Random+import Test.QuickCheck hiding (label)++import Generics.Regular.Rewriting+++type Strategy a = a -> [a]++label _ = id+(s <*> t) a = [c | b <- s a, c <- t b]+(s <|> t) a = s a ++ t a+many s = return <|> (s <*> many s)+repeat s = many s <*> notS s+alternatives = foldr (<|>) (const [])+notS s a = if null (s a) then [a] else []++rewriteMl :: Rewrite a => [Rule a] -> Strategy a +rewriteMl = alternatives . map rewriteM++eliminateConstants :: Strategy (Logic)+eliminateConstants = repeat $ once $+ alternatives $+ [ rewriteMl ruleFalseZeroOr+ , rewriteMl ruleTrueZeroOr+ , rewriteMl ruleTrueZeroAnd+ , rewriteMl ruleFalseZeroAnd+ , rewriteMl ruleNotBoolConst+ , rewriteMl ruleFalseInEquiv+ , rewriteMl ruleTrueInEquiv+ , rewriteMl ruleFalseInImpl+ , rewriteMl ruleTrueInImpl+ ]++eliminateImplEquiv :: Strategy (Logic)+eliminateImplEquiv = repeat $ once $+ rewriteM ruleDefImpl+ <|> rewriteM ruleDefEquiv+ +eliminateNots :: Strategy (Logic)+eliminateNots = repeat $ once $ + rewriteM ruleDeMorganAnd+ <|> rewriteM ruleDeMorganOr+ <|> rewriteM ruleNotNot+ +orToTop :: Strategy (Logic)+orToTop = repeat $ once $ rewriteMl ruleAndOverOr++toDNF :: Strategy (Logic)+toDNF = label "Bring to dnf"+ $ label "Eliminate constants" eliminateConstants+ <*> label "Eliminate implications/equivalences" eliminateImplEquiv+ <*> label "Eliminate nots" eliminateNots + <*> label "Move ors to top" orToTop+ +propSound :: Logic -> Bool+propSound p = + case toDNF p of+ x:_ -> isDNF x+ _ -> False+ +propView :: Logic -> Bool+propView p = p == to (from p)++checks :: IO ()+checks = do+ quickCheck propView+ quickCheck propSound++main :: IO ()+main = print $ all checkOne [0..250]+ where+ checkOne n =+ propSound (generate n (mkStdGen n) arbitrary)
+ examples/logic/run view
@@ -0,0 +1,1 @@+ghci -cpp LogicStrategies.hs LogicRules.hs LogicGenerator.hs Logic.hs -i../../src/ -package QuickCheck-1.2.0.0
rewriting.cabal view
@@ -1,5 +1,5 @@ name: rewriting-version: 0.1+version: 0.2 synopsis: Generic rewriting library for regular datatypes. description: @@ -18,7 +18,7 @@ <http://www.cs.uu.nl/wiki/GenericProgramming/Rewriting>. category: Generics-copyright: (c) 2008 Universiteit Utrecht+copyright: (c) 2009 Universiteit Utrecht license: BSD3 license-file: LICENSE author: Thomas van Noort,@@ -30,8 +30,17 @@ stability: experimental build-type: Custom cabal-version: >= 1.2.1-tested-with: GHC == 6.10.0.20081007+tested-with: GHC == 6.10.1+extra-source-files: examples/expr/run+ examples/expr/Expr.hs+ examples/expr/Expr.expected+ examples/logic/Logic.hs+ examples/logic/LogicGenerator.hs+ examples/logic/LogicRules.hs+ examples/logic/LogicStrategies.hs+ examples/logic/run + -- Disabled the test flag for the moment since not all -- modules from the tests directory are properly included -- in the distribution generated by the sdist target@@ -50,7 +59,7 @@ Generics.Regular.Rewriting.Rules Generics.Regular.Rewriting.Strategies - build-depends: base >= 3.0, containers >= 0.1+ build-depends: base >= 4.0 && < 5, containers >= 0.1, regular >= 0.1 -- Disabled the test flag for the moment since not all -- modules from the tests directory are properly included
src/Generics/Regular/Rewriting.hs view
@@ -10,89 +10,88 @@ -- -- By importing this module, the user is able to use all the rewriting -- machinery. The user is only required to provide an instance of --- @Regular@ and @Rewrite@ for his datatype.+-- @Regular@ and @Rewrite@ for the datatype. -- -- Consider a datatype representing logical propositions: ----- @--- data Expr = Const Int | Expr :++: Expr | Expr :**: Expr deriving Show--- @+-- > data Expr = Const Int | Expr :++: Expr | Expr :**: Expr deriving Show+-- >+-- > infixr 5 :++:+-- > infixr 6 :**: -- -- An instance of @Regular@ would look like: ----- @--- instance Regular Expr where--- type PF Expr = K Int :+: Id :*: Id :+: Id :*: Id--- from (Const n) = L (K n)--- from (e1 :++: e2) = R (L $ (Id e1) :*: (Id e2))--- from (e1 :**: e2) = R (R $ (Id e1) :*: (Id e2))--- to (L (K n)) = Const n--- to (R (L ((Id r1) :*: (Id r2)))) = r1 :++: r2--- to (R (R ((Id r1) :*: (Id r2)))) = r1 :**: r2--- @+-- > data Const+-- > data Plus+-- > data Times+-- >+-- > instance Constructor Const where conName _ = "Const"+-- > instance Constructor Plus where +-- > conName _ = "(:++:)"+-- > conFixity _ = Infix RightAssociative 5+-- > instance Constructor Times where +-- > conName _ = "(:**:)"+-- > conFixity _ = Infix RightAssociative 6+-- >+-- > type instance PF Expr = C Const (K Int) +-- > :+: C Plus (I :*: I) +-- > :+: C Times (I :*: I)+-- >+-- > instance Regular Expr where+-- > from (Const n) = L (C (K n))+-- > from (e1 :++: e2) = R (L (C $ (I e1) :*: (I e2)))+-- > from (e1 :**: e2) = R (R (C $ (I e1) :*: (I e2)))+-- > to (L (C (K n))) = Const n+-- > to (R (L (C ((I r1) :*: (I r2))))) = r1 :++: r2+-- > to (R (R (C ((I r1) :*: (I r2))))) = r1 :**: r2 ----- Additionally, the instance @Rewrite@ would look like:+-- Alternatively, the above code could be derived using Template Haskell: ----- @--- instance Rewrite Expr--- @+-- > $(deriveConstructors ''Expr)+-- > $(deriveRegular ''Expr "PFExpr")+-- > type instance PF Expr = PFExpr ----- Build rules like this:+-- Additionally, the instance @Rewrite@ would look like: ----- @--- rule1 :: Rule Expr--- rule1 = --- rule $ \x -> x :++: Const 0 :~>--- x--- rule5 :: Rule Expr--- rule5 = --- rule $ \x y z -> x :**: (y :++: z) :~> --- (x :**: y) :++: (x :**: z) --- @+-- > instance Rewrite Expr ----- And apply them as follows:+-- Rules are built like this: ----- @--- test1 :: Maybe Expr--- test1 = rewriteM rule1 (Const 2 :++: Const 0)--- test10 :: Maybe Expr--- test10 = rewriteM rule5 ((Const 1) :**: ((Const 2) :++: (Const 3)))--- @+-- > rule1 :: Rule Expr+-- > rule1 = +-- > rule $ \x -> x :++: Const 0 :~>+-- > x+-- > rule5 :: Rule Expr+-- > rule5 = +-- > rule $ \x y z -> x :**: (y :++: z) :~>+-- > (x :**: y) :++: (x :**: z) ----- You may also wish to add constructor names in the representation to use--- generic show. However, constructor names are not yet a stable feature--- and will probably change in future versions of this library.+-- And applied as follows: ----- @--- instance Regular Expr where--- type PF Expr = Con (K Int) :+: Con (Id :*: Id) :+: Con (Id :*: Id)--- from (Const n) = L (Con \"Const\" (K n))--- from (e1 :++: e2) = R (L (Con \"(:++:)\" $ (Id e1) :*: (Id e2)))--- from (e1 :**: e2) = R (R (Con \"(:**:)\" $ (Id e1) :*: (Id e2)))--- to (L (Con _ (K n))) = Const n--- to (R (L (Con _ ((Id r1) :*: (Id r2))))) = r1 :++: r2--- to (R (R (Con _ ((Id r1) :*: (Id r2))))) = r1 :**: r2--- @+-- > test1 :: Maybe Expr+-- > test1 = rewriteM rule1 (Const 2 :++: Const 0)+-- > test10 :: Maybe Expr+-- > test10 = rewriteM rule5 ((Const 1) :**: ((Const 2) :++: (Const 3))) -- ----------------------------------------------------------------------------- module Generics.Regular.Rewriting ( - module Generics.Regular.Rewriting.Base,+ module Generics.Regular.Base,+ + module Generics.Regular.Functions, module Generics.Regular.Rewriting.Machinery, - module Generics.Regular.Rewriting.Representations,- module Generics.Regular.Rewriting.Rules, module Generics.Regular.Rewriting.Strategies ) where -import Generics.Regular.Rewriting.Base+import Generics.Regular.Base+import Generics.Regular.Functions import Generics.Regular.Rewriting.Machinery-import Generics.Regular.Rewriting.Representations import Generics.Regular.Rewriting.Rules import Generics.Regular.Rewriting.Strategies
src/Generics/Regular/Rewriting/Base.hs view
@@ -2,8 +2,6 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} -{-# OPTIONS_GHC -fno-warn-orphans #-}- ----------------------------------------------------------------------------- -- | -- Module : Generics.Regular.Rewriting.Base@@ -15,265 +13,12 @@ -- Portability : non-portable -- -- Summary: Base generic functions that are used for generic rewriting.+-- This module simply reexports "Generics.Regular.Functions", and is provided+-- for backwards-compatibility only. ----------------------------------------------------------------------------- module Generics.Regular.Rewriting.Base (-- -- * Functorial map function.- Functor (..),- - -- * Monadic functorial map function.- GMap (..),- - -- * Crush functions.- Crush (..),- flatten,-- -- * Zip functions.- Zip (..),- fzip,- fzip',-- -- * Equality function.- geq,-- -- * Show function.- GShow (..),- - -- * Functions for generating values that are different on top-level.- LRBase (..),- LR (..),- left,- right --) where--import Control.Monad--import Generics.Regular.Rewriting.Representations----------------------------------------------------------------------------------- Functorial map function.--------------------------------------------------------------------------------instance Functor Id where- fmap f (Id r) = Id (f r)--instance Functor (K a) where- fmap _ (K a) = K a--instance Functor Unit where- fmap _ Unit = Unit--instance (Functor f, Functor g) => Functor (f :+: g) where- fmap f (L x) = L (fmap f x)- fmap f (R y) = R (fmap f y)--instance (Functor f, Functor g) => Functor (f :*: g) where- fmap f (x :*: y) = fmap f x :*: fmap f y--instance Functor f => Functor (Con f) where- fmap f (Con con r) = Con con (fmap f r)----------------------------------------------------------------------------------- Monadic functorial map function.---------------------------------------------------------------------------------- | The @GMap@ class defines a monadic functorial map.-class GMap f where- fmapM :: Monad m => (a -> m b) -> f a -> m (f b)--instance GMap Id where- fmapM f (Id r) = liftM Id (f r)--instance GMap (K a) where- fmapM _ (K x) = return (K x)--instance GMap Unit where- fmapM _ Unit = return Unit--instance (GMap f, GMap g) => GMap (f :+: g) where- fmapM f (L x) = liftM L (fmapM f x)- fmapM f (R x) = liftM R (fmapM f x)--instance (GMap f, GMap g) => GMap (f :*: g) where- fmapM f (x :*: y) = liftM2 (:*:) (fmapM f x) (fmapM f y)--instance GMap f => GMap (Con f) where- fmapM f (Con c x) = liftM (Con c) (fmapM f x)----------------------------------------------------------------------------------- Crush functions.---------------------------------------------------------------------------------- | The @Crush@ class defines a crush on functorial values. In fact,--- @crush@ is a generalized @foldr@.-class Crush f where- crush :: (a -> b -> b) -> b -> f a -> b--instance Crush Id where- crush op e (Id x) = x `op` e--instance Crush (K a) where- crush _ e _ = e--instance Crush Unit where- crush _ e _ = e--instance (Crush f, Crush g) => Crush (f :+: g) where- crush op e (L x) = crush op e x- crush op e (R y) = crush op e y--instance (Crush f, Crush g) => Crush (f :*: g) where- crush op e (x :*: y) = crush op (crush op e y) x--instance Crush f => Crush (Con f) where- crush op e (Con _c x) = crush op e x---- | Flatten a structure by collecting all the elements present.-flatten :: Crush f => f a -> [a]-flatten = crush (:) []----------------------------------------------------------------------------------- Zip functions.---------------------------------------------------------------------------------- | The @Zip@ class defines a monadic zip on functorial values.-class Zip f where- fzipM :: Monad m => (a -> b -> m c) -> f a -> f b -> m (f c)--instance Zip Id where- fzipM f (Id x) (Id y) = liftM Id (f x y)--instance Eq a => Zip (K a) where- fzipM _ (K x) (K y) - | x == y = return (K x)- | otherwise = fail "fzipM: structure mismatch"--instance Zip Unit where- fzipM _ Unit Unit = return Unit--instance (Zip f, Zip g) => Zip (f :+: g) where- fzipM f (L x) (L y) = liftM L (fzipM f x y)- fzipM f (R x) (R y) = liftM R (fzipM f x y)- fzipM _ _ _ = fail "fzipM: structure mismatch"--instance (Zip f, Zip g) => Zip (f :*: g) where- fzipM f (x1 :*: y1) (x2 :*: y2) = - liftM2 (:*:) (fzipM f x1 x2)- (fzipM f y1 y2)--instance Zip f => Zip (Con f) where- fzipM f (Con c1 x) (Con _c2 y) = liftM (Con c1) (fzipM f x y)---- | Functorial zip with a non-monadic function, resulting in a monadic value.-fzip :: (Zip f, Monad m) => (a -> b -> c) -> f a -> f b -> m (f c)-fzip f = fzipM (\x y -> return (f x y))---- | Partial functorial zip with a non-monadic function.-fzip' :: Zip f => (a -> b -> c) -> f a -> f b -> f c-fzip' f x y = maybe (error "fzip': structure mismatch") id (fzip f x y)----------------------------------------------------------------------------------- Equality function.---------------------------------------------------------------------------------- | Equality on values based on their structural representation.-geq :: (b ~ PF a, Regular a, Crush b, Zip b) => a -> a -> Bool-geq x y = maybe False (crush (&&) True) (fzip geq (from x) (from y))----------------------------------------------------------------------------------- Show function.---------------------------------------------------------------------------------- | The @GShow@ class defines a show on values.-class GShow f where- gshow :: (a -> ShowS) -> f a -> ShowS--instance GShow Id where- gshow f (Id r) = f r--instance Show a => GShow (K a) where- gshow _ (K x) = shows x--instance GShow Unit where- gshow _ Unit = id--instance (GShow f, GShow g) => GShow (f :+: g) where- gshow f (L x) = gshow f x- gshow f (R x) = gshow f x--instance (GShow f, GShow g) => GShow (f :*: g) where- gshow f (x :*: y) = gshow f x . showChar ' ' . gshow f y--instance GShow f => GShow (Con f) where- gshow f (Con c x) = showParen True (showString c . showChar ' ' . gshow f x)----------------------------------------------------------------------------------- Functions for generating values that are different on top-level.---------------------------------------------------------------------------------- | The @LRBase@ class defines two functions, @leftb@ and @rightb@, which --- should produce different values.-class LRBase a where- leftb :: a- rightb :: a--instance LRBase Int where- leftb = 0- rightb = 1--instance LRBase Char where- leftb = 'L'- rightb = 'R'- -instance LRBase a => LRBase [a] where- leftb = []- rightb = [error "Should never be inspected"]---- | The @LR@ class defines two functions, @leftf@ and @rightf@, which should --- produce different functorial values.-class LR f where- leftf :: a -> f a- rightf :: a -> f a--instance LR Id where- leftf x = Id x- rightf x = Id x--instance LRBase a => LR (K a) where- leftf _ = K leftb- rightf _ = K rightb--instance LR Unit where- leftf _ = Unit- rightf _ = Unit--instance (LR f, LR g) => LR (f :+: g) where- leftf x = L (leftf x)- rightf x = R (rightf x)--instance (LR f, LR g) => LR (f :*: g) where- leftf x = leftf x :*: leftf x- rightf x = rightf x :*: rightf x--instance LR f => LR (Con f) where- leftf x = Con (error "Should never be inspected") (leftf x)- rightf x = Con (error "Should never be inspected") (rightf x)---- | Produces a value which should be different from the value returned by --- @right@.-left :: (Regular a, LR (PF a)) => a-left = to (leftf left)+ module Generics.Regular.Functions+ ) where --- | Produces a value which should be different from the value returned by --- @left@.-right :: (Regular a, LR (PF a)) => a-right = to (rightf right)+import Generics.Regular.Functions
src/Generics/Regular/Rewriting/Machinery.hs view
@@ -15,7 +15,7 @@ module Generics.Regular.Rewriting.Machinery ( - -- * Type class synonym summarizing generic functions+ -- * Type class synonym summarizing generic functions. Rewrite, -- * Applying a rule specification to a term.@@ -32,20 +32,21 @@ import qualified Data.Map as M import Data.Maybe -import Generics.Regular.Rewriting.Base-import Generics.Regular.Rewriting.Representations+import Generics.Regular.Base+import Generics.Regular.Functions import Generics.Regular.Rewriting.Rules -------------------------------------------------------------------------------- Type class synonym summarizing generic functions+-- Type class synonym summarizing generic functions. ----------------------------------------------------------------------------- -- | The @Rewrite@ is a type class synonym, hiding some of the implementation -- details. -- -- To be able to use the rewriting functions, the user is required to provide -- an instance of this type class.-class (Regular a, Crush (PF a), GMap (PF a), GShow (PF a), Zip (PF a), LR (PF a)) => Rewrite a+class (Regular a, CrushR (PF a), GMap (PF a), GShow (PF a)+ , Zip (PF a), LR (PF a), Functor (PF a)) => Rewrite a -----------------------------------------------------------------------------@@ -98,7 +99,7 @@ Metavar x -> return (M.singleton x (term, toScheme term)) PF r -> fzip (,) r (from term) >>=- crush matchOne (return M.empty)+ crushr matchOne (return M.empty) where matchOne (term1, term2) msubst = do subst1 <- msubst@@ -111,14 +112,14 @@ ----------------------------------------------------------------------------- -- | Applies a substitution to a term.-apply :: Regular a => Subst a -> SchemeOf a -> SchemeOf a+apply :: (Regular a, Functor (PF a)) => Subst a -> SchemeOf a -> SchemeOf a apply subst = foldScheme findMetavar pf where findMetavar x = maybe (metavar x) snd (M.lookup x subst) -- | Instantiates all the metavariables in a term, assuming that there are no -- unbound metavariables in the term.-inst :: Regular a => Subst a -> SchemeOf a -> a+inst :: (Regular a, Functor (PF a)) => Subst a -> SchemeOf a -> a inst subst = foldScheme findMetavar to where findMetavar x =
src/Generics/Regular/Rewriting/Representations.hs view
@@ -12,75 +12,12 @@ -- Stability : experimental -- Portability : non-portable ----- Summary: Types for structural representation.+-- Summary: Types for structural representation. This module simply reexports+-- "Generics.Regular.Base", and is provided for backwards-compatibility only. ----------------------------------------------------------------------------- module Generics.Regular.Rewriting.Representations (-- -- * Functorial structural representation types.- K (..),- Id (..),- Unit (..),- (:+:) (..),- (:*:) (..),- Con (..),-- -- * Fixed-point type.- Fix (..),-- -- * Type class capturing the structural representation of a type and the- -- | corresponding embedding-projection pairs.- Regular (..)- -) where----------------------------------------------------------------------------------- Functorial structural representation types.---------------------------------------------------------------------------------- | Structure type for constant values.-data K a r = K a---- | Structure type for recursive values.-data Id r = Id r---- | Structure type for empty constructors.-data Unit r = Unit---- | Structure type for alternatives in a type.-data (f :+: g) r = L (f r) | R (g r)---- | Structure type for fields of a constructor.-data (f :*: g) r = f r :*: g r---- | Structure type to store the name of a constructor.-data Con f r = Con String (f r)--infixr 6 :+:-infixr 7 :*:---------------------------------------------------------------------------------- Fixed-point type.---------------------------------------------------------------------------------- | The well-known fixed-point type.-newtype Fix f = In (f (Fix f))----------------------------------------------------------------------------------- Type class capturing the structural representation of a type and the--- | corresponding embedding-projection pairs.---------------------------------------------------------------------------------- | The type class @Regular@ captures the structural representation of a --- type and the corresponding embedding-projection pairs.------ To be able to use the rewriting functions, the user is required to provide--- an instance of this type class.-class Functor (PF a) => Regular a where- type PF a :: * -> *- from :: a -> PF a a- to :: PF a a -> a-+ module Generics.Regular.Base+ ) where +import Generics.Regular.Base
src/Generics/Regular/Rewriting/Rules.hs view
@@ -14,8 +14,6 @@ -- -- Summary: Functions for transforming a rule specification to a rule. ---- ----------------------------------------------------------------------------- module Generics.Regular.Rewriting.Rules (@@ -45,8 +43,8 @@ import Data.List -import Generics.Regular.Rewriting.Base-import Generics.Regular.Rewriting.Representations+import Generics.Regular.Base+import Generics.Regular.Functions -----------------------------------------------------------------------------@@ -101,7 +99,7 @@ schemeView (In (R r)) = PF r -- | Recursively converts a value to a @SchemeOf@ value.-toScheme :: Regular a => a -> SchemeOf a+toScheme :: (Regular a, Functor (PF a)) => a -> SchemeOf a toScheme = pf . fmap toScheme . from -- | Folds a @Scheme@ value given a function to apply to metavariables and a@@ -148,12 +146,16 @@ -- | Transforms a rule specification to a rule and throws a runtime error if -- an unbound metavariable occurs in the right-hand side of the rule.-rule :: (Builder r, Crush (PF (Target r)), Zip (PF (Target r))) => r -> Rule (Target r)+rule :: ( Builder r, CrushR (PF (Target r))+ , Functor (PF (Target r)), Zip (PF (Target r)))+ => r -> Rule (Target r) rule = maybe (error "rule: unbound metavariable") id . ruleM -- | Transforms a rule specification to a rule and returns @Nothing@ if -- an unbound metavariable occurs in the right-hand side of the rule.-ruleM :: (Builder r, Crush (PF (Target r)), Zip (PF (Target r))) => r -> Maybe (Rule (Target r))+ruleM :: ( Builder r, CrushR (PF (Target r))+ , Zip (PF (Target r)), Functor (PF (Target r)))+ => r -> Maybe (Rule (Target r)) ruleM f = checkMetavars $ foldr1 mergeRules rules where checkMetavars r @@ -163,7 +165,7 @@ allElem xs ys = all (`elem` ys) xs lMetavars = collectMetavars (lhsR r) [] rMetavars = collectMetavars (rhsR r) []- collectMetavars = foldScheme (:) (crush (.) id)+ collectMetavars = foldScheme (:) (crushr (.) id) mergeRules x y = mergeSchemes (lhsR x) (lhsR y) :~> mergeSchemes (rhsR x) (rhsR y)
src/Generics/Regular/Rewriting/Strategies.hs view
@@ -15,19 +15,19 @@ module Generics.Regular.Rewriting.Strategies ( - -- * Apply a function to the children of a value+ -- * Apply a function to the children of a value. once, one, - -- * Apply a (monadic) function exhaustively top-down+ -- * Apply a (monadic) function exhaustively top-down. topdownM, topdown, - -- * Apply a (monadic) function exhaustively bottom-up+ -- * Apply a (monadic) function exhaustively bottom-up. bottomupM, bottomup, - -- * Apply a (monadic) function to immediate children+ -- * Apply a (monadic) function to immediate children. composM, compos @@ -35,12 +35,12 @@ import Control.Monad -import Generics.Regular.Rewriting.Base-import Generics.Regular.Rewriting.Representations+import Generics.Regular.Base+import Generics.Regular.Functions -------------------------------------------------------------------------------- Functions to apply a function to the children of a value+-- Functions to apply a function to the children of a value. ----------------------------------------------------------------------------- {-# INLINE once #-}@@ -75,7 +75,7 @@ -------------------------------------------------------------------------------- Apply a (monadic) function exhaustively top-down+-- Apply a (monadic) function exhaustively top-down. ----------------------------------------------------------------------------- {-# INLINE topdownM #-}@@ -85,12 +85,12 @@ {-# INLINE topdown #-} -- | Applies a function exhaustively in a top-down fashion-topdown :: Regular a => (a -> a) -> a -> a+topdown :: (Regular a, Functor (PF a)) => (a -> a) -> a -> a topdown f x = compos (topdown f) (f x) -------------------------------------------------------------------------------- Apply a (monadic) function exhaustively bottom-up+-- Apply a (monadic) function exhaustively bottom-up. ----------------------------------------------------------------------------- {-# INLINE bottomupM #-}@@ -100,12 +100,12 @@ {-# INLINE bottomup #-} -- | Applies a function exhaustively in a bottom-up fashion-bottomup :: Regular a => (a -> a) -> a -> a+bottomup :: (Regular a, Functor (PF a)) => (a -> a) -> a -> a bottomup f x = f (compos (bottomup f) x) -------------------------------------------------------------------------------- Apply a (monadic) function to immediate children+-- Apply a (monadic) function to immediate children. ----------------------------------------------------------------------------- {-# INLINE composM #-}@@ -115,5 +115,5 @@ {-# INLINE compos #-} -- | Applies a function to all the immediate children of a value.-compos :: Regular a => (a -> a) -> a -> a+compos :: (Regular a, Functor (PF a)) => (a -> a) -> a -> a compos f = to . fmap f . from