guarded-rewriting (empty) → 0.1
raw patch · 37 files changed
+3032/−0 lines, 37 filesdep +basedep +instant-genericssetup-changed
Dependencies added: base, instant-generics
Files
- LICENSE +28/−0
- Setup.hs +3/−0
- examples/BadRules.hs +67/−0
- examples/Test.hs +92/−0
- guarded-rewriting.cabal +62/−0
- performance/Common/Arith.hs +303/−0
- performance/Common/DNF.hs +101/−0
- performance/Common/GuardedRewriting.hs +46/−0
- performance/Common/Logic.hs +245/−0
- performance/Common/LogicGenerator.hs +61/−0
- performance/Common/LogicRules.hs +231/−0
- performance/Common/LogicStrategies.hs +124/−0
- performance/Common/Once.hs +47/−0
- performance/Gen/Arith/Rules.hs +148/−0
- performance/Gen/Arith/Test.hs +15/−0
- performance/Gen/DNF1/Test.hs +19/−0
- performance/Gen/DNF2/Test.hs +19/−0
- performance/Gen/DNF3/Test.hs +19/−0
- performance/Gen/DNF4/Test.hs +19/−0
- performance/Gen/Rules.hs +89/−0
- performance/Main.hs +193/−0
- performance/Makefile +14/−0
- performance/PM/Arith/Rules.hs +169/−0
- performance/PM/Arith/Test.hs +14/−0
- performance/PM/DNF1/Test.hs +19/−0
- performance/PM/DNF2/Test.hs +19/−0
- performance/PM/DNF3/Test.hs +19/−0
- performance/PM/DNF4/Test.hs +19/−0
- performance/PM/Rules.hs +62/−0
- performance/Uni/DNF1/Test.hs +19/−0
- performance/Uni/DNF2/Test.hs +19/−0
- performance/Uni/DNF3/Test.hs +19/−0
- performance/Uni/DNF4/Test.hs +19/−0
- performance/Uni/Rules.hs +82/−0
- performance/bin/description.txt +1/−0
- performance/out/description.txt +1/−0
- src/Generics/Instant/Rewriting.hs +606/−0
+ LICENSE view
@@ -0,0 +1,28 @@+Copyright (c) 2009 Universiteit Utrecht+All rights reserved.++Redistribution and use in source and binary forms, with or without modification,+are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice, this+ list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright notice,+ this list of conditions and the following disclaimer in the documentation+ and/or other materials provided with the distribution.++3. Neither the name of Universiteit Utrecht nor the names of its contributors+ may be used to endorse or promote products derived from this software without+ specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+
+ Setup.hs view
@@ -0,0 +1,3 @@+import Distribution.Simple++main = defaultMain
+ examples/BadRules.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++module BadRules where++import Generics.Instant.Rewriting+import Generics.Instant++-- Test datatypes+data Term = Val Int | Add Term Term | Mul Term Term+ deriving (Show, Typeable, Eq)++data RecTerm = Branch Int RecTerm RecTerm+ deriving (Show, Typeable, Eq)++-- SPVIew instances+instance Representable Term where+ type Rep Term = Var Int :+: Rec Term :*: Rec Term :+: Rec Term :*: Rec Term++ from (Val i) = L (Var i)+ from (Add x y) = R (L (Rec x :*: Rec y))+ from (Mul x y) = R (R (Rec x :*: Rec y))++ to (L (Var i)) = Val i+ to (R (L (Rec x :*: Rec y))) = Add x y+ to (R (R (Rec x :*: Rec y))) = Mul x y++instance Representable RecTerm where+ type Rep RecTerm = Var Int :*: Rec RecTerm :*: Rec RecTerm+ from (Branch i x y) = Var i :*: Rec x :*: Rec y+ to (Var i :*: Rec x :*: Rec y) = Branch i x y++-- Rewritable instances+instance Rewritable Term+instance Rewritable RecTerm+++-- Superfluous metavariable+-- Result: *** Exception: invalid rule+badApplication1 :: Rule Term+badApplication1 = synthesise badApplication1Template+ where badApplication1Template :: Term -> Term -> Term -> Template Term+ badApplication1Template x y z = Add x y +-> Add y x++-- Unbound metavariable in right-hand side+-- Result: *** Exception: user error (merging failure)+badApplication2 :: Rule Term+badApplication2 = synthesise badApplication2Template+ where badApplication2Template x y = Add x x +-> Add y x++-- Unbound metavariable in guard+-- Result: *** Exception: user error (merging failure)+badApplication3 :: Rule Term+badApplication3 = synthesise badApplication3Template+ where badApplication3Template x y = Add x x +-> Add y x // const True y+++-- Metavariable has no possible finite values+-- Result: would loop, but it is rejected at the type level+{-+badApplication4 :: Rule RecTerm+badApplication4 = synthesise badApplication4Template+ where badApplication4Template i x y = Branch i x y +-> Branch i y x+-}++main = (map validate [badApplication1, badApplication2, badApplication3])
+ examples/Test.hs view
@@ -0,0 +1,92 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleInstances #-}++module Test where++import Generics.Instant+import Generics.Instant.Rewriting++-------------------------------------------------------------------------------+-- Simple Datatype+-------------------------------------------------------------------------------++-- Example datatype+data Exp = Const Int | Plus Exp Exp deriving (Show, Typeable, Eq)++-- Representable instance+instance Representable Exp where+ type Rep Exp = Var Int :+: Rec Exp :*: Rec Exp++ from (Const n) = L (Var n)+ from (Plus e e') = R (Rec e :*: Rec e')++ to (L (Var n)) = Const n+ to (R (Rec e :*: Rec e')) = Plus e e'++-- Required Rewritable instance+instance Rewritable Exp++-- An example rule+silly :: Rule Exp+silly = synthesise $ \e n ->+ Plus e (Const n) +-> e // n == 0++-- Applying the rewriting mechanism+test1 :: String+test1 = show $ rewrite silly (Plus (Const 2) (Const 0))++-------------------------------------------------------------------------------+-- Mutually recursive datatypes+-------------------------------------------------------------------------------++data Decl = None | Seq Decl Decl | Assign String Expr+ deriving (Show, Typeable, Eq)++data Expr = V String | Lam String Expr | App Expr Expr | Let Decl Expr+ deriving (Show, Typeable, Eq)++instance Representable Decl where+ type Rep Decl = U :+: Rec Decl :*: Rec Decl :+: Var String :*: Rec Expr++ from None = L U+ from (Seq d1 d2) = R (L (Rec d1 :*: Rec d2))+ from (Assign v e) = R (R (Var v :*: Rec e))++ to (L U) = None+ to (R (L (Rec d1 :*: Rec d2))) = Seq d1 d2+ to (R (R (Var v :*: Rec e))) = Assign v e++instance Representable Expr where+ type Rep Expr = Var String :+: Var String :*: Rec Expr+ :+: Rec Expr :*: Rec Expr :+: Rec Decl :*: Rec Expr++ from (V x) = L (Var x)+ from (Lam v e) = R (L (Var v :*: Rec e))+ from (App f e) = R (R (L (Rec f :*: Rec e)))+ from (Let d e) = R (R (R (Rec d :*: Rec e)))++ to (L (Var x)) = V x+ to (R (L (Var v :*: Rec e))) = Lam v e+ to (R (R (L (Rec f :*: Rec e)))) = App f e+ to (R (R (R (Rec d :*: Rec e)))) = Let d e+ +instance Rewritable Decl+instance Rewritable Expr+instance Rewritable [Char]++remLet :: Rule Expr+remLet = synthesise $ \x e -> Let (Assign x e) (V x) +-> e++remX :: Rule Decl+remX = synthesise $ \v e -> Assign v e +-> None // v == "x"++test2 :: String+test2 = show $ rewrite remLet (Let (Assign "x" (V "y")) (V "x"))++test3 :: String+test3 = show $ rewrite remX (Assign "x" (V "y"))+++main = print [test1, test2, test3]
+ guarded-rewriting.cabal view
@@ -0,0 +1,62 @@+category: Generics+copyright: (c) 2010 Universiteit Utrecht+name: guarded-rewriting+version: 0.1+license: BSD3+license-file: LICENSE+author: Thomas van Noort, Alexey Rodriguez Yakushev,+ Stefan Holdermans, Johan Jeuring, Bastiaan Heeren,+ Jose Pedro Magalhaes+maintainer: generics@haskell.org+homepage: http://www.cs.uu.nl/wiki/GenericProgramming/GuardedRewriting+synopsis: Datatype-generic rewriting with preconditions+description: ++ This package provides rewriting functionality for datatypes. Most forms of + datatypes are supported, including parametrized and mutually-recursive.+ .+ This library has been described in the paper:+ .+ * Thomas van Noort, Alexey Rodriguez Yakushev, Stefan Holdermans, + Johan Jeuring, Bastiaan Heeren, Jose Pedro Magalhaes.+ /A Lightweight Approach to Datatype-Generic Rewriting./+ Journal of Functional Programming, Special Issue on Generic Programming, + 2010.+ .+ More information about this library can be found at+ <http://www.cs.uu.nl/wiki/GenericProgramming/GuardedRewriting>.++stability: provisional+build-type: Simple+cabal-version: >= 1.6+tested-with: GHC == 6.10.4, GHC == 6.12.1+extra-source-files: examples/BadRules.hs,+ examples/Test.hs,+ performance/Main.hs,+ performance/Makefile,+ performance/Common/*.hs,+ performance/Gen/Rules.hs,+ performance/Gen/Arith/*.hs,+ performance/Gen/DNF1/*.hs,+ performance/Gen/DNF2/*.hs,+ performance/Gen/DNF3/*.hs,+ performance/Gen/DNF4/*.hs,+ performance/PM/Rules.hs,+ performance/PM/Arith/*.hs,+ performance/PM/DNF1/*.hs,+ performance/PM/DNF2/*.hs,+ performance/PM/DNF3/*.hs,+ performance/PM/DNF4/*.hs,+ performance/Uni/Rules.hs,+ performance/Uni/DNF1/*.hs,+ performance/Uni/DNF2/*.hs,+ performance/Uni/DNF3/*.hs,+ performance/Uni/DNF4/*.hs,+ performance/out/description.txt,+ performance/bin/description.txt++library+ ghc-options: -Wall+ build-depends: base >= 3.0 && < 5, instant-generics >= 0.1 && < 1.0+ exposed-modules: Generics.Instant.Rewriting+ hs-source-dirs: src
+ performance/Common/Arith.hs view
@@ -0,0 +1,303 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}++module Common.Arith where++import Control.Monad+import Data.Ratio+import Data.Maybe+import Data.Typeable+import Test.QuickCheck+import System.Random+import Common.GuardedRewriting++propGen :: Int -> Gen (Prop (Equation Expr))+propGen n+ | n == 0 = frequency + [ (5, liftM VarP (sized eqGen))+ , (1, return T)+ , (1, return F)+ ]+ | otherwise = oneof + [ propGen 0+ , liftM2 (:\/:) rec rec+ , liftM2 (:/\:) rec rec+ , liftM Not rec + ]+ where+ rec = propGen (n `div` 2)++eqGen :: Int -> Gen (Equation Expr)+eqGen n = liftM2 (:==:) (exprGen n) constGen++-- Expression with exactly one variable+exprGen :: Int -> Gen Expr+exprGen 0 = return (Varia "x")+exprGen n = oneof+ [ return (Varia "x")+ , liftM2 (:+:) rec constGen, liftM2 (:+:) constGen rec+ , liftM2 (:-:) rec constGen, liftM2 (:-:) constGen rec+ , liftM2 (:**:) rec constGen, liftM2 (:**:) constGen rec+ , liftM2 (:/:) rec constGen, liftM2 (:/:) constGen rec+ , liftM2 (\a n -> a :^: Const (fromInteger (succ $ abs n))) rec arbitrary+ ]+ where+ rec = exprGen (n `div` 2)+ +constGen :: Gen Expr+constGen = liftM (Const . fromInteger) arbitrary++isSolved :: Prop (Equation Expr) -> Bool+isSolved prop =+ case prop of+ p :\/: q -> isSolved p && isSolved q+ p :/\: q -> isSolved p && isSolved q+ Not p -> isSolved p+ VarP p -> isSolvedEq p + _ -> True++isSolvedEq :: Equation Expr -> Bool+isSolvedEq (Varia _ :==: b) = noVaria b+isSolvedEq (a :==: b) = noVaria a && noVaria b++repeatM :: Monad m => m a -> m [a]+repeatM m = liftM2 (:) m (repeatM m)++formula :: [Prop (Equation Expr)]+formula = generate 100 (mkStdGen 280578) (repeatM (sized propGen))++formulas :: [Prop (Equation Expr)]+formulas = take 10000 formula++-----------------------------------++data Prop a = VarP a | T | F + | Prop a :\/: Prop a + | Prop a :/\: Prop a + | Not (Prop a)+ deriving (Show, Typeable, Eq)++data Equation a = a :==: a+ deriving (Show, Typeable, Eq)++infix 2 :==: +infixl 6 :+:, :-: +infixl 7 :**:, :/: +infixr 8 :^:++data Expr = Const Rational+ | Varia String+ | Expr :+: Expr+ | Expr :-: Expr+ | Expr :**: Expr+ | Expr :/: Expr+ | Expr :^: Expr+ deriving (Eq, Show, Typeable)++instance Functor Prop where+ fmap f (VarP a) = VarP (f a)+ fmap f T = T+ fmap f F = F+ fmap f (p :\/: q) = fmap f p :\/: fmap f q+ fmap f (p :/\: q) = fmap f p :/\: fmap f q+ fmap f (Not p) = Not (fmap f p)+ +instance Functor Equation where+ fmap f (a :==: b) = f a :==: f b+++isEven, isOdd :: Rational -> Bool+isEven r = denominator r == 1 && even (numerator r)+isOdd r = denominator r == 1 && odd (numerator r)++hasDivisionByZero :: Expr -> Bool+hasDivisionByZero expr =+ case expr of+ _ :/: Const 0 -> True+ a :+: b -> hasDivisionByZero a || hasDivisionByZero b+ a :-: b -> hasDivisionByZero a || hasDivisionByZero b+ a :**: b -> hasDivisionByZero a || hasDivisionByZero b+ a :/: b -> hasDivisionByZero a || hasDivisionByZero b+ a :^: b -> hasDivisionByZero a || hasDivisionByZero b+ _ -> False++noVaria, hasVaria :: Expr -> Bool+noVaria = not . hasVaria+hasVaria expr = + case expr of+ Const _ -> False+ Varia _ -> True+ a :+: b -> hasVaria a || hasVaria b+ a :-: b -> hasVaria a || hasVaria b+ a :**: b -> hasVaria a || hasVaria b+ a :/: b -> hasVaria a || hasVaria b+ a :^: b -> hasVaria a || hasVaria b++applyD :: (a -> Maybe a) -> a -> a+applyD f a = fromMaybe a (f a)++applyOne :: [a -> Maybe a] -> a -> Maybe a+applyOne fs a = case mapMaybe ($ a) fs of+ hd:_ -> Just hd+ _ -> Nothing+ ++applyBin :: (a -> Maybe a) -> (a -> a -> b) -> a -> a -> Maybe b+applyBin rec op a b = + case (rec a, rec b) of+ (Nothing, Nothing) -> Nothing+ (ma, mb) -> Just (fromMaybe a ma `op` fromMaybe b mb)++somewhereProp :: (Prop a -> Maybe (Prop a)) -> Prop a -> Maybe (Prop a)+somewhereProp f = rec+ where+ rec prop = + let make op a b = case applyBin rec op a b of+ Just c -> Just (applyD f c)+ Nothing -> f prop+ in case prop of+ p :\/: q -> make (:\/:) p q+ p :/\: q -> make (:/\:) p q+ Not p -> case rec p of+ Just p2 -> Just $ applyD f p2+ Nothing -> f prop+ _ -> f prop++somewhereExpr :: (Expr -> Maybe Expr) -> Expr -> Maybe Expr+somewhereExpr f = rec + where+ rec expr = + let make2 op a b = case applyBin rec op a b of+ Just c -> Just (applyD f c)+ Nothing -> f expr+ in case expr of+ a :+: b -> make2 (:+:) a b+ a :-: b -> make2 (:-:) a b+ a :**: b -> make2 (:**:) a b+ a :/: b -> make2 (:/:) a b+ a :^: b -> make2 (:^:) a b+ _ -> f expr++liftToEq :: (a -> Maybe a) -> Equation a -> Maybe (Equation a)+liftToEq f (a :==: b) =+ case (f a, f b) of+ (Nothing, Nothing) -> Nothing+ (ma, mb) -> Just $ fromMaybe a ma :==: fromMaybe b mb++liftToProp :: (a -> Maybe a) -> Prop a -> Maybe (Prop a)+liftToProp f = rec + where+ rec prop =+ case prop of+ p :\/: q -> applyBin rec (:\/:) p q+ p :/\: q -> applyBin rec (:/\:) p q+ Not p -> liftM Not (rec p)+ VarP a -> liftM VarP (f a)+ _ -> Nothing++transformExpr :: (Expr -> Expr) -> Expr -> Expr+transformExpr f = rec + where+ rec expr = f $+ case expr of+ a :+: b -> rec a :+: rec b+ a :-: b -> rec a :-: rec b+ a :**: b -> rec a :**: rec b+ a :/: b -> rec a :/: rec b+ a :^: b -> rec a :^: rec b+ _ -> expr++simplify :: Expr -> Expr+simplify = transformExpr f+ where+ f (Const a :+: Const b) = Const (a+b)+ f (Const a :-: Const b) = Const (a-b)+ f (Const a :**: Const b) = Const (a*b)+ f (Const a :/: Const b) = Const (a/b)+ f (Const a :^: Const b) | denominator b == 1 + = Const (a^numerator b)+ f a = a++-- Also counts the number of rules that hvae been applied (successfully)+solve :: [Prop (Equation Expr) -> Maybe (Prop (Equation Expr))]+ -> Prop (Equation Expr) -> Prop (Equation Expr)+solve rules = rec where+ rec p = + case applyOne rules p of+ Just a -> rec a+ Nothing -> p++-- Examples+ex :: Prop (Equation Expr)+ex = VarP p :\/: VarP q+ where+ x = Varia "x"+ p = (((x :-: Const 3) :^: Const 2) :/: Const 4) :==: Const 25+ q = (Const 1 :-: (Const 2 :/: (Const 1 :+: (x :**: Const 5)))) :==: Const 4 +ex2 = ((VarP (Const (5 % 1) :/: Varia "x" :==: Const (4 % 1)) :\/: VarP ((Const (6 % 1)+ :/: (Const ((-4) % 1) :+: Varia "x")) :^: Const (3 % 1) :==: Const ((-6) % 1)))+ :\/: VarP (Const ((-7) % 1) :**: (Const ((-5) % 1) :**: Varia "x") :==: Const (4 %+ 1))) :\/: (VarP (Varia "x" :==: Const ((-7) % 1)) :\/: VarP (Const (0 % 1) :/: ((Varia "x" :-: Const (0 % 1)) :+: Const (2 % 1)) :==: Const ((-3) % 1)))+ +-- Generic representation+instance (Representable a) => Representable (Prop a) where+ type Rep (Prop a) = Var a+ :+: U+ :+: U+ :+: Rec (Prop a) :*: Rec (Prop a)+ :+: Rec (Prop a) :*: Rec (Prop a)+ :+: Rec (Prop a)+ + from (VarP x) = L (Var x)+ from T = R (L U)+ from F = R (R (L U))+ from (p :\/: q) = R (R (R (L (Rec p :*: Rec q))))+ from (p :/\: q) = R (R (R (R (L (Rec p :*: Rec q)))))+ from (Not p) = R (R (R (R (R (Rec p)))))+ + to (L (Var x)) = VarP x+ to (R (L U)) = T+ to (R (R (L U))) = F+ to (R (R (R (L (Rec p :*: Rec q))))) = p :\/: q+ to (R (R (R (R (L (Rec p :*: Rec q)))))) = p :/\: q+ to (R (R (R (R (R (Rec p)))))) = p++instance (Representable a) => Representable (Equation a) where+ type Rep (Equation a) = Var a :*: Var a+ + from (x :==: y) = Var x :*: Var y+ to (Var x :*: Var y) = x :==: y++instance Representable Expr where+ type Rep Expr = Var Rational+ :+: Var String+ :+: Rec Expr :*: Rec Expr+ :+: Rec Expr :*: Rec Expr+ :+: Rec Expr :*: Rec Expr+ :+: Rec Expr :*: Rec Expr+ :+: Rec Expr :*: Rec Expr+ + from (Const r) = L (Var r)+ from (Varia s) = R (L (Var s))+ from (e1 :+: e2) = R (R (L (Rec e1 :*: Rec e2)))+ from (e1 :-: e2) = R (R (R (L (Rec e1 :*: Rec e2))))+ from (e1 :**: e2) = R (R (R (R (L (Rec e1 :*: Rec e2)))))+ from (e1 :/: e2) = R (R (R (R (R (L (Rec e1 :*: Rec e2))))))+ from (e1 :^: e2) = R (R (R (R (R (R (Rec e1 :*: Rec e2))))))+ + to (L (Var r)) = Const r+ to (R (L (Var s))) = Varia s+ to (R (R (L (Rec e1 :*: Rec e2)))) = e1 :+: e2+ to (R (R (R (L (Rec e1 :*: Rec e2))))) = e1 :-: e2+ to (R (R (R (R (L (Rec e1 :*: Rec e2)))))) = e1 :**: e2+ to (R (R (R (R (R (L (Rec e1 :*: Rec e2))))))) = e1 :/: e2+ to (R (R (R (R (R (R (Rec e1 :*: Rec e2))))))) = e1 :^: e2++ +instance (Rewritable a) => Rewritable (Prop a)+instance (Rewritable a) => Rewritable (Equation a)+instance Rewritable Expr+instance Rewritable String
+ performance/Common/DNF.hs view
@@ -0,0 +1,101 @@+{-# LANGUAGE FlexibleContexts #-}+{-# OPTIONS_GHC -cpp #-}++module Common.DNF (runStrategy, dnf1, dnf2, dnf3, dnf4, reportTick) where ++import Prelude hiding (repeat) +import Common.LogicRules() +import Common.Logic +import System.IO.Unsafe +import Data.IORef + +{- Which rules -} +#ifdef __PM +import PM.Rules +#endif +#ifdef __Uni +import Uni.Rules +#endif +#ifdef __Gen +import Gen.Rules +#endif + + +import Common.Once + +counting = False + + +type Strategy a = a -> [a] + +somewhere s = once s +(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 +try s = s <|> (notS s) +alternatives = foldr (<|>) (const []) +notS s a = if null (s a) then [a] else [] + +runStrategy :: Strategy a -> a -> a +runStrategy s p = case s p of + hd:_ -> hd + _ -> p + +data Count = C !Integer !Integer deriving Show + +tickRef :: IORef Count +tickRef = unsafePerformIO (newIORef (C 0 0)) + +reportTick :: IO () +reportTick = if counting then readIORef tickRef >>= print else return () + +tick :: (a -> [b]) -> a -> [b] +tick r a = if not counting then r a else unsafePerformIO $ do + xs <- return (r a) + c <- readIORef tickRef + seq c (writeIORef tickRef (update (null xs) c)) + return xs + +update :: Bool -> Count -> Count +update b (C x y) + | b = C (x+1) y + | otherwise = C x (y+1) + +--------------------------------------------------------------- + +allRules = conRules ++ defRules ++ notRules ++ disRules +conRules = map tick [ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd, ruleFalseZeroAnd, ruleNotBoolConst, ruleFalseInEquiv, ruleTrueInEquiv, ruleFalseInImpl, ruleTrueInImpl] +defRules = map tick [ruleDefImpl, ruleDefEquiv] +notRules = map tick [ruleDeMorganAnd, ruleDeMorganOr, ruleNotNot] +disRules = map tick [ruleAndOverOr] ++eliminateConstants :: Strategy (Logic) +eliminateConstants = repeat $ somewhere $ alternatives conRules ++eliminateImplEquiv :: Strategy (Logic) +eliminateImplEquiv = repeat $ somewhere $ alternatives defRules ++eliminateNots :: Strategy (Logic) +eliminateNots = repeat $ somewhere $ alternatives notRules + + +dnf1 :: Strategy (Logic) +dnf1 = repeat (somewhere (alternatives allRules)) + +dnf2 :: Strategy (Logic) +dnf2 = repeat (somewhere (alternatives conRules)) + <*> repeat (somewhere (alternatives defRules)) + <*> repeat (somewhere (alternatives notRules)) + <*> repeat (somewhere (alternatives disRules)) + +dnf3 :: Strategy (Logic) +dnf3 = repeat (oneTD (alternatives conRules)) + <*> repeat (oneBU (alternatives defRules)) + <*> repeat (oneTD (alternatives notRules)) + <*> repeat (somewhere (alternatives disRules)) ++dnf4 :: Strategy (Logic) +dnf4 = fullBU (repeat (alternatives (conRules ++ defRules))) + <*> fullTD (repeat (alternatives notRules)) + <*> fullBU (try (alternatives disRules <*> fullTD (try (alternatives disRules))))
+ performance/Common/GuardedRewriting.hs view
@@ -0,0 +1,46 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeSynonymInstances #-}++module Common.GuardedRewriting (+ module Generics.Instant.Rewriting,+ module Generics.Instant+ ) where++import Data.Ratio++import Generics.Instant.Rewriting+import Generics.Instant+++instance Extensible Rational where+ newtype Ext Rational gam = ExtRational Rational+ toExt = ExtRational++instance Matchable Rational where+ match' (ExtRational r) r' | r == r' = return empty+ | otherwise = fail "structure mismatch"++instance Substitutable Rational where+ subst' _ (ExtRational r) = return r++instance Sampleable Rational where+ left' = 1+ right' = 2++instance Empty Rational where+ empty' = 1++instance Diffable Rational where+ diff' (ExtRational r) (ExtRational r') | r == r' = Just (ExtRational r)+ | otherwise = Nothing++instance Validatable Rational++type instance Finite Rational = True++instance Rewritable Rational++instance Representable Rational where+ type Rep Rational = Rational+ from = id+ to = id
+ performance/Common/Logic.hs view
@@ -0,0 +1,245 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleInstances #-}++-----------------------------------------------------------------------------+-- 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 Common.Logic where++import Data.List+import Data.Maybe+import qualified Data.Set as S+import qualified Data.Map as M+import Data.Typeable+import Data.Data+import Common.GuardedRewriting++infixr 1 :<->:+infixr 2 :->: +infixr 3 :||: +infixr 4 :&&:++-- | The data type Logic is the abstract syntax for the domain+-- | of logic expressions.+data Logic = VarL 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, Typeable, Data)++-- | 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+ VarL 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+ VarL _ -> True+ Not (VarL _) -> 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]++-- | 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 $ (VarL "a" :||: VarL "b") :||: (VarL "c" :||: VarL "d" :||: VarL "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+ (VarL x, VarL 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++-----------------------------------------------------------+--- Unification++type Substitution = M.Map Char Logic++isMetaVar :: Logic -> Maybe Char+isMetaVar (VarL ['_', c]) = Just c+isMetaVar _ = Nothing++metaVars :: [Logic]+metaVars = [ VarL ['_', c] | c <- ['a' .. 'z'] ]++(|->) :: Substitution -> Logic -> Logic+(|->) sub = foldLogic (var, (:->:), (:<->:), (:&&:), (:||:), Not, T, F)+ where + var s = case isMetaVar (VarL s) of+ Just i -> fromMaybe (VarL s) (M.lookup i sub)+ _ -> VarL 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+ (VarL x, VarL 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)+++instance Rewritable Logic+instance Rewritable [Char]++instance Representable Logic where+ type Rep Logic =+ Var String+ :+: Rec Logic :*: Rec Logic+ :+: Rec Logic :*: Rec Logic+ :+: Rec Logic :*: Rec Logic+ :+: Rec Logic :*: Rec Logic+ :+: Rec Logic+ :+: U+ :+: U++ from (VarL x) = L (Var x)+ from (p :<->: q) = R (L (Rec p :*: Rec q))+ from (p :->: q) = R (R (L (Rec p :*: Rec q)))+ from (p :&&: q) = R (R (R (L (Rec p :*: Rec q))))+ from (p :||: q) = R (R (R (R (L (Rec p :*: Rec q)))))+ from (Not p) = R (R (R (R (R (L (Rec p))))))+ from T = R (R (R (R (R (R (L U))))))+ from F = R (R (R (R (R (R (R U))))))++ to (L (Var x)) = VarL x+ to (R (L (Rec p :*: Rec q))) = p :<->: q+ to (R (R (L (Rec p :*: Rec q)))) = p :->: q+ to (R (R (R (L (Rec p :*: Rec q))))) = p :&&: q+ to (R (R (R (R (L (Rec p :*: Rec q)))))) = p :||: q+ to (R (R (R (R (R (L (Rec p))))))) = Not p+ to (R (R (R (R (R (R (L U))))))) = T+ to (R (R (R (R (R (R (R U))))))) = F
+ performance/Common/LogicGenerator.hs view
@@ -0,0 +1,61 @@+----------------------------------------------------------------------------- +-- 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 Common.LogicGenerator where + +import Common.Logic +import Control.Monad +import Data.Char +import Test.QuickCheck hiding (defaultConfig) +import System.Random + +----------------------------------------------------------- +--- QuickCheck generator + +-- 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 . VarL) ["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 + +instance Arbitrary Logic where + arbitrary = sized (arbLogic True) + coarbitrary logic = + case logic of + VarL 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 + +repeatM :: Monad m => m a -> m [a] +repeatM m = liftM2 (:) m (repeatM m) + +formula :: [Logic] +formula = generate 100 (mkStdGen 280578) (repeatM arbitrary)
+ performance/Common/LogicRules.hs view
@@ -0,0 +1,231 @@+{-# OPTIONS -fglasgow-exts #-} +----------------------------------------------------------------------------- +-- 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 the distribution. +----------------------------------------------------------------------------- +-- | +-- Maintainer : bastiaan.heeren@ou.nl +-- Stability : provisional +-- Portability : portable (depends on ghc) +-- +----------------------------------------------------------------------------- +module Common.LogicRules where + +import qualified Data.Set as S +import Common.Logic +import Common.GuardedRewriting + + +p |- q = p +-> q +makeRuleList _ = map synthesise +buggyRule = id +makeRule _ = synthesise + +{- 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 + ] -} + +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)) --note the firstNot both formulas! + ] +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) + ]
+ performance/Common/LogicStrategies.hs view
@@ -0,0 +1,124 @@+----------------------------------------------------------------------------- +-- 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 Common.LogicStrategies where + +import Prelude hiding (repeat) +import Common.LogicRules +import Common.Logic +import Common.LogicGenerator +import Test.QuickCheck hiding (label) +import System.Random +import Common.GuardedRewriting +import Control.Monad + +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 [] + +-- -------------------------------------- +-- Strategies +-- -------------------------------------- +-- Same monad to that in the SYB3 paper +data S m a = S a (m a) + +instance MonadPlus m => Monad (S m) where + return x = S x mzero + (S x xs) >>= k + = S r (rs1 `mplus` rs2) + where + S r rs1 = k x + rs2 = do x <- xs + let S r _ = k x + return r + +-- This is like Stratego's one. +-- It applies f to one of the immediate children of x. +{- +one :: (Rewritable a, MonadPlus m, Functor m) => (a -> m a) -> a -> m a +one f x = fmap (from . In) rs + where + S _ rs = fmapM try_f $ out $ to x + try_f x = S x (f_str x) + f_str = fmap to . f . from +-} + +-- Apply f once to one of the nodes of x +-- Mirrors the corresponding definition in Stratego +once :: (Rewritable a, MonadPlus m, Functor m) => (a -> m a) -> a -> m a +once f x = f x `mplus` one (once f) x + + +-- applies a strategy at one location +-- see http://ideas.cs.uu.nl/trac/browser/Feedback/trunk/src/Common/Strategy.hs +somewhere :: Rewritable a => Strategy a -> Strategy a +somewhere = once ++lift :: Rewritable a => Rule' a -> Strategy a+lift r = (:[]) . rewrite' r+ +liftl :: Rewritable a => [Rule' a] -> Strategy a +liftl = alternatives . map lift + +eliminateConstants :: Strategy (Logic) +eliminateConstants = repeat $ somewhere $ + alternatives $ + [ liftl ruleFalseZeroOr, liftl ruleTrueZeroOr, liftl ruleTrueZeroAnd + , liftl ruleFalseZeroAnd, liftl ruleNotBoolConst, liftl ruleFalseInEquiv + , liftl ruleTrueInEquiv, liftl ruleFalseInImpl, liftl ruleTrueInImpl + ] + +eliminateImplEquiv :: Strategy (Logic) +eliminateImplEquiv = repeat $ somewhere $ + lift ruleDefImpl + <|> lift ruleDefEquiv + +eliminateNots :: Strategy (Logic) +eliminateNots = repeat $ somewhere $ + lift ruleDeMorganAnd + <|> lift ruleDeMorganOr + <|> lift ruleNotNot + +orToTop :: Strategy (Logic) +orToTop = repeat $ somewhere $ liftl 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 == from (to p) + +checks :: IO () +checks = do + quickCheck propView + quickCheck propSound + +main :: IO () +main = print $ all checkOne [0..1000] + where + checkOne n = + propSound (generate n (mkStdGen n) generateLogic)
+ performance/Common/Once.hs view
@@ -0,0 +1,47 @@+module Common.Once (once, oneTD, oneBU, fullTD, fullBU) where + +import Common.Logic + +once = somewhere + +somewhere :: (Logic -> [Logic]) -> Logic -> [Logic] +somewhere f p = f p ++ one (somewhere f) p + +oneTD :: (Logic -> [Logic]) -> Logic -> [Logic] +oneTD f p = f p +> one (oneTD f) p + +oneBU :: (Logic -> [Logic]) -> Logic -> [Logic] +oneBU f p = one (oneBU f) p +> f p + +fullTD :: (Logic -> [Logic]) -> Logic -> [Logic] +fullTD f p = [ p'' | p' <- f p, p'' <- full (fullTD f) p' ] + +fullBU :: (Logic -> [Logic]) -> Logic -> [Logic] +fullBU f p = [ p'' | p' <- full (fullBU f) p, p'' <- f p' ] + +one :: (Logic -> [Logic]) -> Logic -> [Logic] +one f p = + case p of + p :->: q -> make (:->: q) p ++ make (p :->:) q + p :<->: q -> make (:<->: q) p ++ make (p :<->:) q + p :&&: q -> make (:&&: q) p ++ make (p :&&:) q + p :||: q -> make (:||: q) p ++ make (p :||:) q + Not p -> make Not p + _ -> [] + where + make :: (Logic -> Logic) -> Logic -> [Logic] + make g = map g . f + +full :: (Logic -> [Logic]) -> Logic -> [Logic] +full f p = + case p of + p :->: q -> [ p' :->: q' | p' <- f p, q' <- f q ] + p :<->: q -> [ p' :<->: q' | p' <- f p, q' <- f q ] + p :&&: q -> [ p' :&&: q' | p' <- f p, q' <- f q ] + p :||: q -> [ p' :||: q' | p' <- f p, q' <- f q ] + Not p -> [ Not p' | p' <- f p ] + _ -> [p] + +(+>) :: [a] -> [a] -> [a] +[] +> ys = ys +xs +> _ = xs
+ performance/Gen/Arith/Rules.hs view
@@ -0,0 +1,148 @@+module Gen.Arith.Rules where++import Common.Arith+import Common.GuardedRewriting+import Test.QuickCheck+import Data.Maybe (isJust, fromJust, catMaybes)++type PropRule = Rule (Prop (Equation Expr))+type EqRule = Rule (Equation Expr)+type ExprRule = Rule Expr+++go = quickCheck $ forAll (sized propGen) (isSolved . solve rules)++rules :: [Prop (Equation Expr) -> Maybe (Prop (Equation Expr))]+rules = [ somewhereProp $ applyOne (map rewriteM propRules)+ , liftToProp $ applyOne (map rewriteM eqRules)+ , liftToProp $ liftToEq $ somewhereExpr $ applyOne (map rewriteM exprRules)+ ]+ where+ propRules :: [PropRule]+ propRules = + [ coverPowerEven, divisionByZero+ , eqSame, eqDifferent+ , andTrueLeft, andTrueRight, andFalseLeft, andFalseRight+ , orTrueLeft, orTrueRight, orFalseLeft, orFalseRight+ , notTrue, notFalse+ ]++ eqRules :: [EqRule]+ eqRules = + [ coverPlusLeft, coverPlusRight, coverMinLeft, coverMinRight+ , coverTimesLeft, coverTimesRight, coverDivLeft, coverDivRight+ , coverPowerOdd+ ]++ exprRules :: [ExprRule]+ exprRules = [timesZeroLeft, timesZeroRight]+++-- Rules+coverPlusLeft :: Rule (Equation Expr)+coverPlusLeft = synthesise $ \a b c -> + a :+: b :==: c +->+ a :==: c :-: b // hasVaria a && noVaria b++coverPlusRight = synthesise $ \a b c -> + a :+: b :==: c +->+ b :==: c :-: a // noVaria a && hasVaria b++coverMinLeft = synthesise $ \a b c ->+ a :-: b :==: c +-> + a :==: c :+: b // hasVaria a && noVaria b++coverMinRight = synthesise $ \a b c ->+ a :-: b :==: c +->+ b :==: a :-: c // noVaria a && hasVaria b+ +coverTimesLeft = synthesise $ \a b c -> + a :**: Const b :==: c +->+ a :==: c :/: Const b // hasVaria a && b /= 0+ +coverTimesRight = synthesise $ \a b c ->+ Const a :**: b :==: c +->+ b :==: c :/: Const a // a /= 0 && hasVaria b+ +coverDivLeft = synthesise $ \a b c ->+ a :/: Const b :==: c +->+ a :==: c :**: Const b // hasVaria a && b /= 0+ +coverDivRight = synthesise $ \a b c ->+ Const a :/: b :==: c +->+ b :==: Const a :/: c // hasVaria b -- and b should not be zero here!++coverPowerEven = synthesise $ \a n b -> let new = b :^: Const (1/n) in+ VarP (a :^: Const n :==: b) +->+ VarP (a :==: new) :\/: VarP (a :==: Const 0 :-: new)+ // hasVaria a && n > 0 && isEven n++coverPowerOdd = synthesise $ \a n b ->+ a :^: Const n :==: b +->+ a :==: b :^: Const (1/n) // hasVaria a && n > 0 && isOdd n++timesZeroLeft = synthesise $ \x ->+ Const 0 :**: x +->+ Const 0++timesZeroRight = synthesise $ \x -> + x :**: Const 0 +->+ Const 0++divisionByZero = synthesise $ \a b -> + VarP (a :==: b) +->+ F // hasDivisionByZero a || hasDivisionByZero b++--------------------------------------------------------+-- Rules for comparing the two sides of an equation+ +eqSame = synthesise $ \a b ->+ VarP (a :==: b) +->+ T // a == b++eqDifferent = synthesise $ \a b ->+ VarP (Const a :==: Const b) +->+ F // a /= b++----------------------------------+-- Propagating boolean constants++andTrueLeft = synthesise $ \p ->+ T :/\: p +->+ p++andTrueRight = synthesise $ \p ->+ p :/\: T +->+ p++andFalseLeft = synthesise $ \p ->+ F :/\: p +->+ F++andFalseRight = synthesise $ \p ->+ p :/\: F +->+ F++orTrueLeft = synthesise $ \p ->+ T :\/: p +->+ T++orTrueRight = synthesise $ \p ->+ p :\/: T +->+ T++orFalseLeft = synthesise $ \p ->+ F :\/: p +->+ p++orFalseRight = synthesise $ \p ->+ p :\/: F +->+ p++notTrue = synthesise $ + Not T +->+ F++notFalse = synthesise $ + Not F +->+ T
+ performance/Gen/Arith/Test.hs view
@@ -0,0 +1,15 @@+module Gen.Arith.Test (main) where + +import Common.Arith +import Gen.Arith.Rules +import System.CPUTime (getCPUTime) +import Common.GuardedRewriting + +main :: IO () +main = do + t1 <- getCPUTime + let p e = if isSolved (solve rules e) then True else error (show e) + if all p formulas then (return ()) else error "ERROR!" + t2 <- getCPUTime + let diff = fromInteger (t2 - t1) / (1000000000 :: Double) + putStrLn ("\t" ++ show diff)
+ performance/Gen/DNF1/Test.hs view
@@ -0,0 +1,19 @@+module Gen.DNF1.Test (main) where + +import Common.LogicGenerator +import Common.Logic +import Common.DNF +import System.CPUTime (getCPUTime) + + +dnf = dnf1 +nr = 10000 + +main :: IO () +main = do + t1 <- getCPUTime + let p l = if isDNF (runStrategy dnf l) then True else error (show l) + if all p $ take nr formula then reportTick else error "ERROR!" + t2 <- getCPUTime + let diff = fromInteger (t2 - t1) / (1000000000 :: Double) + putStrLn ("\t" ++ show diff)
+ performance/Gen/DNF2/Test.hs view
@@ -0,0 +1,19 @@+module Gen.DNF2.Test (main) where + +import Common.LogicGenerator +import Common.Logic +import Common.DNF +import System.CPUTime (getCPUTime) + + +dnf = dnf2 +nr = 50000 + +main :: IO () +main = do + t1 <- getCPUTime + let p l = if isDNF (runStrategy dnf l) then True else error (show l) + if all p $ take nr formula then reportTick else error "ERROR!" + t2 <- getCPUTime + let diff = fromInteger (t2 - t1) / (1000000000 :: Double) + putStrLn ("\t" ++ show diff)
+ performance/Gen/DNF3/Test.hs view
@@ -0,0 +1,19 @@+module Gen.DNF3.Test (main) where + +import Common.LogicGenerator +import Common.Logic +import Common.DNF +import System.CPUTime (getCPUTime) + + +dnf = dnf3 +nr = 50000 + +main :: IO () +main = do + t1 <- getCPUTime + let p l = if isDNF (runStrategy dnf l) then True else error (show l) + if all p $ take nr formula then reportTick else error "ERROR!" + t2 <- getCPUTime + let diff = fromInteger (t2 - t1) / (1000000000 :: Double) + putStrLn ("\t" ++ show diff)
+ performance/Gen/DNF4/Test.hs view
@@ -0,0 +1,19 @@+module Gen.DNF4.Test (main) where + +import Common.LogicGenerator +import Common.Logic +import Common.DNF +import System.CPUTime (getCPUTime) + + +dnf = dnf4 +nr = 100000 + +main :: IO () +main = do + t1 <- getCPUTime + let p l = if isDNF (runStrategy dnf l) then True else error (show l) + if all p $ take nr formula then reportTick else error "ERROR!" + t2 <- getCPUTime + let diff = fromInteger (t2 - t1) / (1000000000 :: Double) + putStrLn ("\t" ++ show diff)
+ performance/Gen/Rules.hs view
@@ -0,0 +1,89 @@+module Gen.Rules where + +import Data.Maybe +import Common.Logic +import Common.GuardedRewriting + + +(|-) :: Logic -> Logic -> Template Logic +p |- q = p +-> q // True + +makeRuleList _ = rewriteMl . map synthesise +makeRule s x = makeRuleList s [x] + +--rewriteMl :: [Rule (Pat (PF Logic))] -> Logic -> [Logic] +rewriteMl rs p = take 1 $ catMaybes $ map (`rewriteM` p) rs ++-- This main function is defined to solve a bug in GHC +main :: IO ()+main = do let resultsPP = zipWith undefined [1..] ([] :: [Logic])+ putStr (unlines resultsPP) + +ruleDefImpl = makeRule "DefImpl" $ + \x y -> (x :->: y) |- (Not x :||: y) + +ruleDefEquiv = makeRule "DefEquiv" $ + \x y -> (x :<->: y) |- ((x :&&: y) :||: (Not x :&&: Not y)) + +ruleFalseInEquiv = makeRuleList "FalseInEquiv" + [ \x -> (F :<->: x) |- (Not x) + , \x -> (x :<->: F) |- (Not x) + ] + +ruleTrueInEquiv = makeRuleList "TrueInEquiv" + [ \x -> (T :<->: x) |- x + , \x -> (x :<->: T) |- x + ] + +ruleFalseInImpl = makeRuleList "FalseInImpl" + [ \x -> (F :->: x) |- T + , \x -> (x :->: F) |- (Not x) + ] + +ruleTrueInImpl = makeRuleList "TrueInImpl" + [ \x -> (T :->: x) |- x + , \x -> (x :->: T) |- T + ] + +ruleFalseZeroOr = makeRuleList "FalseZeroOr" + [ \x -> (F :||: x) |- x + , \x -> (x :||: F) |- x + ] +ruleTrueZeroOr = makeRuleList "TrueZeroOr" + [ \x -> (T :||: x) |- T + , \x -> (x :||: T) |- T + ] + +ruleTrueZeroAnd = makeRuleList "TrueZeroAnd" + [ \x -> (T :&&: x) |- x + , \x -> (x :&&: T) |- x + ] + +ruleFalseZeroAnd = makeRuleList "FalseZeroAnd" + [ \x -> (F :&&: x) |- F + , \x -> (x :&&: F) |- F + ] + +ruleDeMorganOr = makeRule "DeMorganOr" $ + \x y -> (Not (x :||: y)) |- (Not x :&&: Not y) + +ruleDeMorganAnd = makeRule "DeMorganAnd" $ + \x y -> (Not (x :&&: y)) |- (Not x :||: Not y) + +ruleNotBoolConst = makeRuleList "NotBoolConst" + [ (Not T) |- F + , (Not F) |- T + ] + +ruleNotNot = makeRule "NotNot" $ + \x -> (Not (Not x)) |- x + +ruleAndOverOr = makeRuleList "AndOverOr" + [ \x y z -> (x :&&: (y :||: z)) |- ((x :&&: y) :||: (x :&&: z)) + , \x y z -> ((x :||: y) :&&: z) |- ((x :&&: z) :||: (y :&&: z)) + ] + +ruleOrOverAnd = makeRuleList "OrOverAnd" + [ \x y z -> (x :||: (y :&&: z)) |- ((x :||: y) :&&: (x :||: z)) + , \x y z -> ((x :&&: y) :||: z) |- ((x :||: z) :&&: (y :||: z)) + ]
+ performance/Main.hs view
@@ -0,0 +1,193 @@+module Main where + + +-- ParseArgs library +import System.Console.ParseArgs + +import System.CPUTime (cpuTimePrecision) +import Data.List (groupBy, sortBy, intersperse) +import System.FilePath ((</>)) +import System.Cmd (system) +import System.IO + (Handle, openFile, IOMode(..), stdout, hFlush, hIsEOF, hGetChar, hClose, hPutStrLn) +import System.Exit (ExitCode(..)) +import System.Info (os, arch, compilerVersion) + +data Mode = PM | Uni | Gen deriving (Eq, Ord, Show) +data Strategy = DNF1 | DNF2 | DNF3 | DNF4 | Arith deriving (Eq, Ord, Show) +data Test = Test { mode :: Mode, strategy :: Strategy} deriving (Eq, Ord) + +instance Show Test where + show t = show (mode t) ++ "-" ++ show (strategy t) + +tests = [Test PM DNF1, + Test PM DNF2, + Test PM DNF3, + Test PM DNF4, + Test PM Arith, + + Test Uni DNF1, + Test Uni DNF2, + Test Uni DNF3, + Test Uni DNF4, + + Test Gen DNF1, + Test Gen DNF2, + Test Gen DNF3, + Test Gen DNF4, + Test Gen Arith] + +inCommas :: [String] -> String +inCommas = concat . intersperse "," + + +printGroupStats :: (Enum a, Fractional a, Floating a, Num a) + => Handle -> IO [(Test, Int, a)] -> IO () +printGroupStats h l = do + l' <- l + let --group1 :: [[(Test, Int, a)]] + group1 = groupBy g (sortBy f l') + f (t1,_,_) (t2,_,_) = compare t1 t2 + g (t1,_,_) (t2,_,_) = t1 == t2 + --calcAvgStdDev :: [(Test, Int, a)] -> (Test, a, a) + calcAvgStdDev x = let avg l = sum' l / toEnum (length l) + stddev a = sqrt (avg [ (t,d,y - a) | (t,d,y) <- x ]) + in (fst' (head x), avg x, stddev (avg x)) + fst' (a,_,_) = a + --sum' :: [(Test, Int, a)] -> a + sum' [] = 0 + sum' ((_,_,d):ts) = d + sum' ts + sort2 l = sortBy f' l + f' (t1,_,_) (t2,_,_) = compare (strategy t1, mode t1) + (strategy t2, mode t2) + printTests h $ sort2 $ map calcAvgStdDev group1 + +printTests :: (Show a) => Handle -> [(Test, a, a)] -> IO () +printTests h l = sequence_ $ map (hPutStrLn h) [ inCommas [show t, show a, show d] | (t,a,d) <- l ] + +-- Arguments +data MyArgs = N | O | F | P deriving (Eq, Ord, Show) + +myArgs :: [Arg MyArgs] +myArgs = [ + Arg { argIndex = N, + argAbbr = Just 'n', + argName = Just "number-times", + argData = argDataDefaulted "int" ArgtypeInt 1, + argDesc = "Number of times to run the benchmark" + }, + Arg { argIndex = O, + argAbbr = Just 'o', + argName = Just "output", + argData = argDataOptional "file" ArgtypeString, + argDesc = "Output report file" + }, + Arg { argIndex = F, + argAbbr = Just 'f', + argName = Just "flags", + argData = argDataDefaulted "string" ArgtypeString "", + argDesc = "Extra flags to pass to the compiler" + }, + Arg { argIndex = P, + argAbbr = Just 'p', + argName = Just "profiling", + argData = Nothing, + argDesc = "Profile, do not benchmark" + } + ] + +sequenceProgress_ :: [IO ExitCode] -> IO () +sequenceProgress_ [] = return () +sequenceProgress_ l = do + let seq :: [IO ExitCode] -> Int -> IO () + seq [] _ = putStrLn "done." + seq (h:t) n = do + putStr ((show n) ++ " ") >> hFlush stdout + sequenceError_ [h] + seq t (n + 1) + putStr ("Total number of elements: " ++ show (length l) ++ ". ") + seq l 1 + +-- sequence_ accounting for errors +sequenceError_ :: [IO ExitCode] -> IO () +sequenceError_ [] = return () +sequenceError_ (h:t) = do + e <- h + case e of + ExitSuccess -> sequenceError_ t + ExitFailure n -> error ("Execution returned exit code " + ++ show n ++ ", aborted.") + +-- Stricter readFile +hGetContents' hdl = do e <- hIsEOF hdl + if e then return [] + else do c <- hGetChar hdl + cs <- hGetContents' hdl + return (c:cs) + +readFile' fn = do hdl <- openFile fn ReadMode + xs <- hGetContents' hdl + hClose hdl + return xs + + +main :: IO () +main = do + args <- parseArgsIO ArgsComplete myArgs + + -- Some variables + let profiling = gotArg args P + n :: Int + n = if profiling then 1 else (getRequiredArg args N) + extraFlags = getRequiredArg args F + flags t = "-fforce-recomp --make -iCommon -D__" ++ show (mode t) + ++ " -o bin" </> path t + ++ " -main-is " ++ show (mode t) ++ "." + ++ show (strategy t) ++ ".Test.main " + ++ (if profiling then " -prof -auto-all " else "") + ++ " -outputdir out " + ++ extraFlags ++ " " + path t = "Test" ++ show t + out t = "out" </> "Test" ++ show t ++ ".compile.out" + redirect t = " > " ++ out t ++ " 2>&1 " + cmd t = "ghc " ++ show (mode t) ++ "." ++ show (strategy t) + ++ ".Test " ++ flags t ++ redirect t + + -- Compilation + putStrLn "Compiling..." >> hFlush stdout + --sequence_ [ putStrLn (cmd t) | t <- tests ] + sequenceProgress_ [ system (cmd t) | t <- tests ] + + -- Running tests + let newout t m = "out" </> "Test" ++ show t ++ "." ++ show m ++ ".out" + newpath t = "bin" </> "Test" ++ show t + run t m = newpath t + ++ if profiling then " +RTS -p -RTS" else "" + ++ " > " ++ newout t m + do + putStrLn ("-------------------------------------") + putStrLn "Running tests..." >> hFlush stdout + --sequence_ [ putStrLn (run t m) | t <- tests, m <- [1..n]] + sequenceProgress_ [ system (run t m) | t <- tests, m <- [1..n]] + + -- Results output + h <- getArgStdio args O WriteMode + hPutStrLn h ("-------------------------------------") + hPutStrLn h "\nResults:" + hPutStrLn h ("Number of repetitions: " ++ show n) + hPutStrLn h ("Flags to the compiler: " ++ extraFlags) + hPutStrLn h ("Environment: " ++ inCommas [os, arch, show compilerVersion]) + hPutStrLn h ("CPU time precision: " ++ show (fromInteger cpuTimePrecision / (1000000000 :: Double)) ++ " (ms)") + hPutStrLn h "" + let parse :: Test -> Int -> IO Double + parse t m = readFile' (newout t m) >>= return . read . tail . dropWhile (/= '\t') + liftIOList :: [(a, b, IO c)] -> IO [(a, b, c)] + liftIOList [] = return [] + liftIOList ((a,b,c):t) = do c' <- c + t' <- liftIOList t + return ((a,b,c'):t') + if profiling + then hPutStrLn h ("Profiling run, no benchmarking results.") + else printGroupStats h (liftIOList [ (t, m, parse t m) | t <- tests, m <- [1..n]]) + hPutStrLn h ("-------------------------------------") + hClose h
+ performance/Makefile view
@@ -0,0 +1,14 @@+GHC=ghc++.default=PHONY++all: compile run++compile:+ $(GHC) --make -O1 Main++run:+ ./Main -n 5 -f "-O1 -package QuickCheck-1.2.0.0"++clean: + rm -rf bin/* out/*
+ performance/PM/Arith/Rules.hs view
@@ -0,0 +1,169 @@+module PM.Arith.Rules where++import Common.Arith+import Test.QuickCheck+import Data.Ratio++type Rule a = a -> Maybe a+type PropRule = Rule (Prop (Equation Expr))+type EqRule = Rule (Equation Expr)+type ExprRule = Rule Expr++rules :: [PropRule]+rules = [ somewhereProp $ applyOne propRules+ , liftToProp $ applyOne eqRules+ , liftToProp $ liftToEq $ somewhereExpr $ applyOne exprRules+ ]+ where+ propRules :: [PropRule]+ propRules = + [ coverPowerEven, divisionByZero+ , eqSame, eqDifferent+ , andTrueLeft, andTrueRight, andFalseLeft, andFalseRight+ , orTrueLeft, orTrueRight, orFalseLeft, orFalseRight+ , notTrue, notFalse+ ]++ eqRules :: [EqRule]+ eqRules = + [ coverPlusLeft, coverPlusRight, coverMinLeft, coverMinRight+ , coverTimesLeft, coverTimesRight, coverDivLeft, coverDivRight+ , coverPowerOdd+ ]++ exprRules :: [ExprRule]+ exprRules = [timesZeroLeft, timesZeroRight]+ +go = quickCheck $ forAll (sized propGen) (isSolved . solve rules)++-- Rules+coverPlusLeft :: EqRule+coverPlusLeft (a :+: b :==: c)+ | hasVaria a && noVaria b = + Just (a :==: c :-: b)+coverPlusLeft _ = Nothing++coverPlusRight :: EqRule+coverPlusRight (a :+: b :==: c)+ | noVaria a && hasVaria b =+ Just (b :==: c :-: a)+coverPlusRight _ = Nothing++coverMinLeft :: EqRule+coverMinLeft (a :-: b :==: c)+ | hasVaria a && noVaria b = + Just (a :==: c :+: b)+coverMinLeft _ = Nothing++coverMinRight :: EqRule+coverMinRight (a :-: b :==: c)+ | noVaria a && hasVaria b =+ Just (b :==: a :-: c)+coverMinRight _ = Nothing+ +coverTimesLeft :: EqRule+coverTimesLeft (a :**: Const b :==: c) + | hasVaria a && b /= 0 =+ Just (a :==: c :/: Const b)+coverTimesLeft _ = Nothing+ +coverTimesRight :: EqRule+coverTimesRight (Const a :**: b :==: c) + | a /= 0 && hasVaria b =+ Just (b :==: c :/: Const a)+coverTimesRight _ = Nothing+ +coverDivLeft :: EqRule+coverDivLeft (a :/: Const b :==: c) + | hasVaria a && b /= 0 =+ Just (a :==: c :**: Const b)+coverDivLeft _ = Nothing+ +coverDivRight :: EqRule+coverDivRight (Const a :/: b :==: c) + | hasVaria b =+ Just (b :==: Const a :/: c) -- and b should not be zero here!+coverDivRight _ = Nothing++coverPowerEven :: PropRule+coverPowerEven (VarP (a :^: Const n :==: b)) + | hasVaria a && n > 0 && isEven n =+ let new = b :^: Const (1/n) in+ Just (VarP (a :==: new) :\/: VarP (a :==: Const 0 :-: new))+coverPowerEven _ = Nothing++coverPowerOdd :: EqRule+coverPowerOdd (a :^: Const n :==: b)+ | hasVaria a && n > 0 && isOdd n =+ Just (a :==: b :^: Const (1/n))+coverPowerOdd _ = Nothing++timesZeroLeft :: ExprRule+timesZeroLeft (Const 0 :**: _) =+ Just (Const 0)+timesZeroLeft _ = Nothing++timesZeroRight :: ExprRule+timesZeroRight (_ :**: Const 0) =+ Just (Const 0)+timesZeroRight _ = Nothing++divisionByZero :: PropRule+divisionByZero (VarP (a :==: b)) + | hasDivisionByZero a || hasDivisionByZero b =+ Just F+divisionByZero _ = Nothing++--------------------------------------------------------+-- Rules for comparing the two sides of an equation+ +eqSame :: PropRule+eqSame (VarP (a :==: b)) | a == b = Just T+eqSame _ = Nothing ++eqDifferent :: PropRule+eqDifferent (VarP (Const a :==: Const b)) | a /= b = Just F+eqDifferent _ = Nothing ++----------------------------------+-- Propagating boolean constants++andTrueLeft :: PropRule +andTrueLeft (T :/\: p) = Just p+andTrueLeft _ = Nothing++andTrueRight :: PropRule +andTrueRight (p :/\: T) = Just p+andTrueRight _ = Nothing++andFalseLeft :: PropRule +andFalseLeft (F :/\: _) = Just F+andFalseLeft _ = Nothing++andFalseRight :: PropRule +andFalseRight (_ :/\: F) = Just F+andFalseRight _ = Nothing++orTrueLeft :: PropRule +orTrueLeft (T :\/: _) = Just T+orTrueLeft _ = Nothing++orTrueRight :: PropRule +orTrueRight (_ :\/: T) = Just T+orTrueRight _ = Nothing++orFalseLeft :: PropRule +orFalseLeft (F :\/: p) = Just p+orFalseLeft _ = Nothing++orFalseRight :: PropRule +orFalseRight (p :\/: F) = Just p+orFalseRight _ = Nothing++notTrue :: PropRule+notTrue (Not T) = Just F+notTrue _ = Nothing++notFalse :: PropRule+notFalse (Not F) = Just T+notFalse _ = Nothing
+ performance/PM/Arith/Test.hs view
@@ -0,0 +1,14 @@+module PM.Arith.Test (main) where + +import Common.Arith +import PM.Arith.Rules +import System.CPUTime (getCPUTime) + +main :: IO () +main = do + t1 <- getCPUTime + let p e = if isSolved (solve rules e) then True else error (show e) + if all p formulas then (return ()) else error "ERROR!" + t2 <- getCPUTime + let diff = fromInteger (t2 - t1) / (1000000000 :: Double) + putStrLn ("\t" ++ show diff)
+ performance/PM/DNF1/Test.hs view
@@ -0,0 +1,19 @@+module PM.DNF1.Test (main) where + +import Common.LogicGenerator +import Common.Logic +import Common.DNF +import System.CPUTime (getCPUTime) + + +dnf = dnf1 +nr = 10000 + +main :: IO () +main = do + t1 <- getCPUTime + let p l = if isDNF (runStrategy dnf l) then True else error (show l) + if all p $ take nr formula then reportTick else error "ERROR!" + t2 <- getCPUTime + let diff = fromInteger (t2 - t1) / (1000000000 :: Double) + putStrLn ("\t" ++ show diff)
+ performance/PM/DNF2/Test.hs view
@@ -0,0 +1,19 @@+module PM.DNF2.Test (main) where + +import Common.LogicGenerator +import Common.Logic +import Common.DNF +import System.CPUTime (getCPUTime) + + +dnf = dnf2 +nr = 50000 + +main :: IO () +main = do + t1 <- getCPUTime + let p l = if isDNF (runStrategy dnf l) then True else error (show l) + if all p $ take nr formula then reportTick else error "ERROR!" + t2 <- getCPUTime + let diff = fromInteger (t2 - t1) / (1000000000 :: Double) + putStrLn ("\t" ++ show diff)
+ performance/PM/DNF3/Test.hs view
@@ -0,0 +1,19 @@+module PM.DNF3.Test (main) where + +import Common.LogicGenerator +import Common.Logic +import Common.DNF +import System.CPUTime (getCPUTime) + + +dnf = dnf3 +nr = 50000 + +main :: IO () +main = do + t1 <- getCPUTime + let p l = if isDNF (runStrategy dnf l) then True else error (show l) + if all p $ take nr formula then reportTick else error "ERROR!" + t2 <- getCPUTime + let diff = fromInteger (t2 - t1) / (1000000000 :: Double) + putStrLn ("\t" ++ show diff)
+ performance/PM/DNF4/Test.hs view
@@ -0,0 +1,19 @@+module PM.DNF4.Test (main) where + +import Common.LogicGenerator +import Common.Logic +import Common.DNF +import System.CPUTime (getCPUTime) + + +dnf = dnf4 +nr = 100000 + +main :: IO () +main = do + t1 <- getCPUTime + let p l = if isDNF (runStrategy dnf l) then True else error (show l) + if all p $ take nr formula then reportTick else error "ERROR!" + t2 <- getCPUTime + let diff = fromInteger (t2 - t1) / (1000000000 :: Double) + putStrLn ("\t" ++ show diff)
+ performance/PM/Rules.hs view
@@ -0,0 +1,62 @@+module PM.Rules where + +import Common.Logic + +ruleDefImpl (x :->: y) = [Not x :||: y] +ruleDefImpl _ = [] + +ruleDefEquiv (x :<->: y) = [(x :&&: y) :||: (Not x :&&: Not y)] +ruleDefEquiv _ = [] + +ruleFalseInEquiv (F :<->: x) = [Not x] +ruleFalseInEquiv (x :<->: F) = [Not x] +ruleFalseInEquiv _ = [] + +ruleTrueInEquiv (T :<->: x) = [x] +ruleTrueInEquiv (x :<->: T) = [x] +ruleTrueInEquiv _ = [] + +ruleFalseInImpl (F :->: x) = [T] +ruleFalseInImpl (x :->: F) = [Not x] +ruleFalseInImpl _ = [] + +ruleTrueInImpl (T :->: x) = [x] +ruleTrueInImpl (x :->: T) = [T] +ruleTrueInImpl _ = [] + +ruleFalseZeroOr (F :||: x) = [x] +ruleFalseZeroOr (x :||: F) = [x] +ruleFalseZeroOr _ = [] + +ruleTrueZeroOr (T :||: x) = [T] +ruleTrueZeroOr (x :||: T) = [T] +ruleTrueZeroOr _ = [] + +ruleTrueZeroAnd (T :&&: x) = [x] +ruleTrueZeroAnd (x :&&: T) = [x] +ruleTrueZeroAnd _ = [] + +ruleFalseZeroAnd (F :&&: x) = [F] +ruleFalseZeroAnd (x :&&: F) = [F] +ruleFalseZeroAnd _ = [] + +ruleDeMorganOr (Not (x :||: y)) = [Not x :&&: Not y] +ruleDeMorganOr _ = [] + +ruleDeMorganAnd (Not (x :&&: y)) = [ Not x :||: Not y ] +ruleDeMorganAnd _ = [] + +ruleNotBoolConst (Not T) = [ F ] +ruleNotBoolConst (Not F) = [ T ] +ruleNotBoolConst _ = [] + +ruleNotNot (Not (Not x)) = [x] +ruleNotNot _ = [] + +ruleAndOverOr (x :&&: (y :||: z)) = [ (x :&&: y) :||: (x :&&: z) ] +ruleAndOverOr ((x :||: y) :&&: z) = [ (x :&&: z) :||: (y :&&: z) ] +ruleAndOverOr _ = [] + +ruleOrOverAnd (x :||: (y :&&: z)) = [ (x :||: y) :&&: (x :||: z) ] +ruleOrOverAnd ((x :&&: y) :||: z) = [ (x :||: z) :&&: (y :||: z) ] +ruleOrOverAnd _ = []
+ performance/Uni/DNF1/Test.hs view
@@ -0,0 +1,19 @@+module Uni.DNF1.Test (main) where + +import Common.LogicGenerator +import Common.Logic +import Common.DNF +import System.CPUTime (getCPUTime) + + +dnf = dnf1 +nr = 10000 + +main :: IO () +main = do + t1 <- getCPUTime + let p l = if isDNF (runStrategy dnf l) then True else error (show l) + if all p $ take nr formula then reportTick else error "ERROR!" + t2 <- getCPUTime + let diff = fromInteger (t2 - t1) / (1000000000 :: Double) + putStrLn ("\t" ++ show diff)
+ performance/Uni/DNF2/Test.hs view
@@ -0,0 +1,19 @@+module Uni.DNF2.Test (main) where + +import Common.LogicGenerator +import Common.Logic +import Common.DNF +import System.CPUTime (getCPUTime) + + +dnf = dnf2 +nr = 50000 + +main :: IO () +main = do + t1 <- getCPUTime + let p l = if isDNF (runStrategy dnf l) then True else error (show l) + if all p $ take nr formula then reportTick else error "ERROR!" + t2 <- getCPUTime + let diff = fromInteger (t2 - t1) / (1000000000 :: Double) + putStrLn ("\t" ++ show diff)
+ performance/Uni/DNF3/Test.hs view
@@ -0,0 +1,19 @@+module Uni.DNF3.Test (main) where + +import Common.LogicGenerator +import Common.Logic +import Common.DNF +import System.CPUTime (getCPUTime) + + +dnf = dnf3 +nr = 50000 + +main :: IO () +main = do + t1 <- getCPUTime + let p l = if isDNF (runStrategy dnf l) then True else error (show l) + if all p $ take nr formula then reportTick else error "ERROR!" + t2 <- getCPUTime + let diff = fromInteger (t2 - t1) / (1000000000 :: Double) + putStrLn ("\t" ++ show diff)
+ performance/Uni/DNF4/Test.hs view
@@ -0,0 +1,19 @@+module Uni.DNF4.Test (main) where + +import Common.LogicGenerator +import Common.Logic +import Common.DNF +import System.CPUTime (getCPUTime) + + +dnf = dnf4 +nr = 100000 + +main :: IO () +main = do + t1 <- getCPUTime + let p l = if isDNF (runStrategy dnf l) then True else error (show l) + if all p $ take nr formula then reportTick else error "ERROR!" + t2 <- getCPUTime + let diff = fromInteger (t2 - t1) / (1000000000 :: Double) + putStrLn ("\t" ++ show diff)
+ performance/Uni/Rules.hs view
@@ -0,0 +1,82 @@+module Uni.Rules where + +import Common.Logic + +x:y:z:_ = metaVars + +(|-) :: Logic -> Logic -> (Logic -> [Logic]) +(lhs |- rhs) a = case matchLogic lhs a of + Just s -> [s |-> rhs] + Nothing -> [] + +makeRuleList _ fs a = take 1 $ concatMap ($ a) fs +makeRule _ = id+ +ruleDefImpl = makeRule "DefImpl" $ + (x :->: y) |- (Not x :||: y) + +ruleDefEquiv = makeRule "DefEquiv" $ + (x :<->: y) |- ((x :&&: y) :||: (Not x :&&: Not y)) + +ruleFalseInEquiv = makeRuleList "FalseInEquiv" + [ (F :<->: x) |- (Not x) + , (x :<->: F) |- (Not x) + ] + +ruleTrueInEquiv = makeRuleList "TrueInEquiv" + [ (T :<->: x) |- x + , (x :<->: T) |- x + ] + +ruleFalseInImpl = makeRuleList "FalseInImpl" + [ (F :->: x) |- T + , (x :->: F) |- (Not x) + ] + +ruleTrueInImpl = makeRuleList "TrueInImpl" + [ (T :->: x) |- x + , (x :->: T) |- T + ] + +ruleFalseZeroOr = makeRuleList "FalseZeroOr" + [ (F :||: x) |- x + , (x :||: F) |- x + ] +ruleTrueZeroOr = makeRuleList "TrueZeroOr" + [ (T :||: x) |- T + , (x :||: T) |- T + ] + +ruleTrueZeroAnd = makeRuleList "TrueZeroAnd" + [ (T :&&: x) |- x + , (x :&&: T) |- x + ] + +ruleFalseZeroAnd = makeRuleList "FalseZeroAnd" + [ (F :&&: x) |- F + , (x :&&: F) |- F + ] + +ruleDeMorganOr = makeRule "DeMorganOr" $ + (Not (x :||: y)) |- (Not x :&&: Not y) + +ruleDeMorganAnd = makeRule "DeMorganAnd" $ + (Not (x :&&: y)) |- (Not x :||: Not y) + +ruleNotBoolConst = makeRuleList "NotBoolConst" + [ (Not T) |- F + , (Not F) |- T + ] + +ruleNotNot = makeRule "NotNot" $ + (Not (Not x)) |- x + +ruleAndOverOr = makeRuleList "AndOverOr" + [ (x :&&: (y :||: z)) |- ((x :&&: y) :||: (x :&&: z)) + , ((x :||: y) :&&: z) |- ((x :&&: z) :||: (y :&&: z)) + ] + +ruleOrOverAnd = makeRuleList "OrOverAnd" + [ (x :||: (y :&&: z)) |- ((x :||: y) :&&: (x :||: z)) + , ((x :&&: y) :||: z) |- ((x :||: z) :&&: (y :||: z)) + ]
+ performance/bin/description.txt view
@@ -0,0 +1,1 @@+Binaries will be placed here.
+ performance/out/description.txt view
@@ -0,0 +1,1 @@+Output files will be placed here.
+ src/Generics/Instant/Rewriting.hs view
@@ -0,0 +1,606 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE OverlappingInstances #-}++{-# OPTIONS_GHC -Wall #-}++-----------------------------------------------------------------------------+-- |+-- Module : Generics.Instant.Rewriting+-- Copyright : (c) 2010, Universiteit Utrecht+-- License : BSD3+--+-- Maintainer : generics@haskell.org+-- Stability : experimental+-- Portability : non-portable+--+-- This is the top module for the rewriting library. All functionality is+-- implemented in this module. For examples of how to use the library, see+-- the included files in the directory examples, or the benchmark in the+-- directory performance.+--+-----------------------------------------------------------------------------++module Generics.Instant.Rewriting (+ + -- * The class to signal availability of rewriting for a type+ Rewritable,+ + -- * Top-level functions+ rewrite, rewriteM, validate, synthesise,++ -- * Building rewrite rules+ Template(..), (+->), (//), Rule,+ + -- * Internal classes: might be necessary to add new base types+ Extensible(..),+ Matchable(..),+ Substitutable(..),+ Sampleable(..), Empty(..), HasRec(..), Finite, True, False,+ Diffable(..),+ Validatable(..),+ Nillable(..),++ -- * Re-exported for convenience+ Typeable+ + ) where++import Control.Monad (join, liftM, liftM2)+import Data.Maybe (fromJust, fromMaybe)+import Data.Typeable (Typeable, gcast)++import Generics.Instant.Base+import Generics.Instant.Instances ()++-------------------------------------------------------------------------------+-- | Typed references+-------------------------------------------------------------------------------++data Ref :: * -> * -> * where+ Rz :: Ref a (a :*: gam)+ Rs :: Ref a gam -> Ref a (b :*: gam)++instance Eq (Ref a gam) where+ Rz == Rz = True+ Rs r == Rs r' = r == r'+ _ == _ = False++-------------------------------------------------------------------------------+-- | The 'Rewritable' class is used to signal types that can be rewritten and +-- to ``tie the recursive knot'' of the generic functions.+-------------------------------------------------------------------------------++class (Representable a, Typeable a, Eq a, Empty (Rep a),+ Extensible (Rep a), Matchable (Rep a), Substitutable (Rep a),+ Sampleable (Rep a), Diffable (Rep a), Validatable (Rep a)) =>+ Rewritable a++instance Rewritable Int+instance Rewritable Float+instance Rewritable Char++-------------------------------------------------------------------------------+-- Rewrite rules+-------------------------------------------------------------------------------++-- Metavariables+type Metavar a gam = Ref a gam++-- | Schemes+class Extensible a where+ data Ext a :: * -> *+ toExt :: a -> Ext a U++type Scheme a gam = Ext (Rep a) gam :+: Metavar a gam++toScheme :: Rewritable a => a -> Scheme a U+toScheme = L . toExt . from++instance Extensible Int where+ newtype Ext Int gam = ExtInt Int+ toExt = ExtInt++instance Extensible Float where+ newtype Ext Float gam = ExtFloat Float+ toExt = ExtFloat++instance Extensible Char where+ newtype Ext Char gam = ExtChar Char+ toExt = ExtChar++instance (Extensible a, Extensible b) => Extensible (a :+: b) where+ newtype Ext (a :+: b) gam = ExtSum (Ext a gam :+: Ext b gam)++ toExt (L x) = ExtSum (L (toExt x))+ toExt (R y) = ExtSum (R (toExt y))++instance (Extensible a, Extensible b) => Extensible (a :*: b) where+ newtype Ext (a :*: b) gam = ExtCons (Ext a gam :*: Ext b gam)+ toExt (x :*: y) = ExtCons (toExt x :*: toExt y)++instance Extensible U where+ newtype Ext U gam = ExtNil U+ toExt = ExtNil++instance (Rewritable a) => Extensible (Rec a) where+ newtype Ext (Rec a) gam = ExtRec (Rec (Scheme a gam))+ toExt (Rec a) = ExtRec (Rec (toScheme a))++instance (Rewritable a) => Extensible (Var a) where+ newtype Ext (Var a) gam = ExtVar (Var (Scheme a gam))+ toExt (Var a) = ExtVar (Var (toScheme a))++instance (Extensible a) => Extensible (C c a) where+ newtype Ext (C c a) gam = ExtC (C c (Ext a gam))+ toExt (C a) = ExtC (C (toExt a))++-- Guards+type family Guard gam :: *+type instance Guard U = Bool+type instance Guard (a :*: gam) = a -> Guard gam++-- Rules+data Rule' a gam =+ Rule' { lhs :: Scheme a gam, rhs :: Scheme a gam, guard :: Guard gam }++-------------------------------------------------------------------------------+-- Rewriting+-------------------------------------------------------------------------------++-- Substitutions+data Subst :: * -> * where+ Sz :: Subst U+ Ss :: Rewritable a => Maybe a -> Subst gam -> Subst (a :*: gam)++(!!!) :: Subst gam -> Ref a gam -> Maybe a+Ss mb _ !!! Rz = mb+Ss _ s !!! Rs r = s !!! r+_ !!! _ = error "(!!!) failure"++total :: Monad m => Subst gam -> Ref a gam -> m a+total s r = maybe (fail "metavariable unbound") return (s !!! r)++class Nillable gam where+ empty :: Subst gam++instance Nillable U where+ empty = Sz++instance (Rewritable a, Nillable gam) => Nillable (a :*: gam) where+ empty = Ss Nothing empty++singleton :: Nillable gam => Ref a gam -> a -> Subst gam+singleton r x = update r x empty++update :: Ref a gam -> a -> Subst gam -> Subst gam+update Rz x (Ss _ s) = Ss (Just x) s+update (Rs r) x (Ss mb s) = Ss mb (update r x s)+update _ _ _ = error "update failure"++(+++) :: Monad m => Subst gam -> Subst gam -> m (Subst gam)+Sz +++ Sz = return Sz+Ss mb@(Just x) s +++ Ss (Just x') s' | x == x' = liftM (Ss mb) (s +++ s')+ | otherwise = fail "merging failure"+Ss mb@(Just _) s +++ Ss Nothing s' = liftM (Ss mb) (s +++ s')+Ss Nothing s +++ Ss mb s' = liftM (Ss mb) (s +++ s')+_ +++ _ = error "(+++) failure"++-- | Matching+class Matchable a where+ match' :: (Nillable gam, Monad m) => Ext a gam -> a -> m (Subst gam)++match :: (Rewritable a, Nillable gam, Monad m) =>+ Scheme a gam -> a -> m (Subst gam)+match (L ext) x = match' ext (from x)+match (R r) x = return (singleton r x)++instance Matchable Int where+ match' (ExtInt n) n' | n == n' = return empty+ | otherwise = fail "structure mismatch"++instance Matchable Char where+ match' (ExtChar c) c' | c == c' = return empty+ | otherwise = fail "structure mismatch"++instance Matchable Float where+ match' (ExtFloat f) f' | f == f' = return empty+ | otherwise = fail "structure mismatch"++instance (Matchable a, Matchable b) => Matchable (a :+: b) where+ match' (ExtSum (L ext)) (L x) = match' ext x+ match' (ExtSum (R ext)) (R y) = match' ext y+ match' _ _ = fail "structure mismatch"++instance (Matchable a, Matchable b) => Matchable (a :*: b) where+ match' (ExtCons (ext :*: ext')) (x :*: y) =+ join (liftM2 (+++) (match' ext x) (match' ext' y))++instance Matchable U where+ match' (ExtNil U) U = return empty++instance (Rewritable a) => Matchable (Var a) where+ match' (ExtVar (Var e)) (Var a) = match e a++instance (Rewritable a) => Matchable (Rec a) where+ match' (ExtRec (Rec e)) (Rec a) = match e a++instance (Matchable a) => Matchable (C c a) where+ match' (ExtC (C e)) (C a) = match' e a++-- | Substituting+class Substitutable a where+ subst' :: Monad m => Subst gam -> Ext a gam -> m a++subst :: (Rewritable a, Monad m) => Subst gam -> Scheme a gam -> m a+subst s (L ext) = liftM to (subst' s ext)+subst s (R r) = total s r++instance Substitutable Int where+ subst' _ (ExtInt n) = return n++instance Substitutable Char where+ subst' _ (ExtChar c) = return c++instance Substitutable Float where+ subst' _ (ExtFloat f) = return f++instance (Substitutable a, Substitutable b) => Substitutable (a :+: b) where+ subst' s (ExtSum (L ext)) = liftM L (subst' s ext)+ subst' s (ExtSum (R ext)) = liftM R (subst' s ext)++instance (Substitutable a, Substitutable b) => Substitutable (a :*: b) where+ subst' s (ExtCons (ext :*: ext')) = liftM2 (:*:) (subst' s ext) (subst' s ext')++instance Substitutable U where+ subst' _ (ExtNil U) = return U++instance (Rewritable a) => Substitutable (Rec a) where+ subst' s (ExtRec (Rec scheme)) = liftM Rec (subst s scheme)++instance (Rewritable a) => Substitutable (Var a) where+ subst' s (ExtVar (Var scheme)) = liftM Var (subst s scheme)++instance (Substitutable a) => Substitutable (C c a) where+ subst' s (ExtC (C ext)) = liftM C (subst' s ext)++-- | Testing preconditions+class Testable gam where+ test :: Subst gam -> Guard gam -> Bool++instance Testable U where+ test Sz b = b++instance Testable gam => Testable (a :*: gam) where+ test (Ss (Just x) s) f = test s (f x)+ test (Ss Nothing _) _ = error "invalid rule"++-- Rewriting+rewrite' :: (Rewritable a, Nillable gam, Testable gam) => Rule' a gam -> a -> a+rewrite' rule x = fromMaybe x (rewriteM' rule x)++rewriteM' :: (Rewritable a, Nillable gam, Testable gam, Monad m) + => Rule' a gam -> a -> m a+rewriteM' rule x =+ do s <- match (lhs rule) x+ if (test s (guard rule)) then subst s (rhs rule) else fail "guard failed"++-------------------------------------------------------------------------------+-- Synthesising rules+-------------------------------------------------------------------------------++-- | Sampling+class Sampleable a where+ left' :: a+ right' :: a++left, right :: Rewritable a => a+left = to left'+right = to right'++instance (Bounded a) => Sampleable a where+ left' = minBound+ right' = maxBound++instance Sampleable Float where+ left' = 0+ right' = 1++instance (Representable a, Empty (Rep a), Representable b, Empty (Rep b)) => Sampleable (a :+: b) where+ left' = L gempty+ right' = R gempty++instance (Sampleable a, Sampleable b) => Sampleable (a :*: b) where+ left' = left' :*: left'+ right' = right' :*: right'++instance Sampleable U where+ left' = U+ right' = U++instance (Rewritable a) => Sampleable (Rec a) where+ left' = Rec left+ right' = Rec right++instance (Rewritable a) => Sampleable (Var a) where+ left' = Var left+ right' = Var right++instance (Sampleable a) => Sampleable (C c a) where+ left' = C left' + right' = C right'++-- | Diff++class Diffable a where+ diff' :: Typeable b => Ext a gam -> Ext a gam -> Maybe (Ext a (b :*: gam))++diff :: (Rewritable a, Typeable b) =>+ Scheme a gam -> Scheme a gam -> Maybe (Scheme a (b :*: gam))+diff (L ext) (L ext') = + maybe (scast (R Rz)) (Just . L) (diff' ext ext')+diff (R r) (R r') | r == r' = Just (R (Rs r))+diff _ _ = Nothing++newtype FlipScheme gam a = Flip {unFlip :: Scheme a gam}++scast :: (Typeable a, Typeable b) =>+ Scheme b (b :*: gam) -> Maybe (Scheme a (b :*: gam))+scast = fmap unFlip . gcast . Flip++(><) :: (Rewritable a, Typeable b) =>+ Scheme a gam -> Scheme a gam -> (Scheme a (b :*: gam))+scheme >< scheme' = fromJust (diff scheme scheme')++instance Diffable Int where+ diff' (ExtInt n) (ExtInt n') | n == n' = Just (ExtInt n)+ | otherwise = Nothing++instance Diffable Char where+ diff' (ExtChar c) (ExtChar c') | c == c' = Just (ExtChar c)+ | otherwise = Nothing++instance Diffable Float where+ diff' (ExtFloat f) (ExtFloat f') | f == f' = Just (ExtFloat f)+ | otherwise = Nothing++instance (Diffable a, Diffable b) => Diffable (a :+: b) where+ diff' (ExtSum (L ext)) (ExtSum (L ext')) =+ fmap (ExtSum . L) (diff' ext ext')+ diff' (ExtSum (R ext)) (ExtSum (R ext')) =+ fmap (ExtSum . R) (diff' ext ext')+ diff' _ _ = Nothing++instance (Diffable a, Diffable b) => Diffable (a :*: b) where+ diff' (ExtCons (a :*: ext)) (ExtCons (b :*: ext')) =+ fmap ExtCons (liftM2 (:*:) (diff' a b) (diff' ext ext'))++instance Diffable U where+ diff' (ExtNil U) (ExtNil U) = Just (ExtNil U)++instance (Rewritable a) => Diffable (Rec a) where+ diff' (ExtRec (Rec s)) (ExtRec (Rec s')) = fmap ExtRec (liftM Rec (diff s s'))++instance (Rewritable a) => Diffable (Var a) where+ diff' (ExtVar (Var s)) (ExtVar (Var s')) = fmap ExtVar (liftM Var (diff s s'))++instance (Diffable a) => Diffable (C c a) where+ diff' (ExtC (C a)) (ExtC (C b)) = fmap ExtC (liftM C (diff' a b))++-- | Templates+data Template a = Template a a Bool++infix 0 //+infix 1 +->++(+->) :: a -> a -> Template a+l +-> r = Template l r True++(//) :: Template a -> Bool -> Template a+Template l r _ // g = Template l r g++-- | Synthesising rules from metasyntax specifications+class (Rewritable (Obj a)) => IsRule a where+ type Obj a :: *+ type Env a :: *++ synthesise' :: a -> Rule' (Obj a) (Env a)++instance (Rewritable a) => IsRule (Template a) where+ type Obj (Template a) = a+ type Env (Template a) = U++ synthesise' (Template l r g) =+ Rule' {lhs = toScheme l, rhs = toScheme r, guard = g}++instance (Rewritable a, IsRule b) => IsRule (a -> b) where+ type Obj (a -> b) = Obj b+ type Env (a -> b) = a :*: Env b++ synthesise' f = Rule'+ { lhs = lhs l >< lhs r+ , rhs = rhs l >< rhs r+ , guard = guard . synthesise' . f+ }+ where+ l = synthesise' (f left)+ r = synthesise' (f right)++-- | Validating synthesised rules+class Validatable a where+ record :: Ext a gam -> Record gam -> Record gam+ record _ = id++data Record :: * -> * where+ RNil :: Record U+ RCons :: Bool -> Record gam -> Record (a :*: gam)++class Recordable gam where+ blank :: Record gam++instance Recordable U where+ blank = RNil++instance Recordable gam => Recordable (a :*: gam) where+ blank = RCons False blank++record' :: Rewritable a => Scheme a gam -> Record gam -> Record gam+record' (L e) rec = record e rec+record' (R Rz) (RCons _ rec) = RCons True rec+record' (R (Rs r)) (RCons b rec) = RCons b (record' (R r) rec)+record' _ _ = error "record' failure"++instance Validatable Int+instance Validatable Float+instance Validatable Char+instance Validatable U++instance (Validatable a, Validatable b) => Validatable (a :+: b) where+ record (ExtSum (L e)) = record e+ record (ExtSum (R e)) = record e++instance (Validatable a, Validatable b) => Validatable (a :*: b) where+ record (ExtCons (e :*: es)) = record e . record es++instance (Rewritable a) => Validatable (Rec a) where+ record (ExtRec (Rec e)) = record' e++instance (Rewritable a) => Validatable (Var a) where+ record (ExtVar (Var e)) = record' e++instance (Validatable a) => Validatable (C c a) where+ record (ExtC (C e)) = record e++validate' :: forall a gam. (Rewritable a, Recordable gam)+ => Rule' a gam -> Bool+validate' r = conj (record' (lhs r) blank)+ where+ conj :: forall gam'. Record gam' -> Bool+ conj RNil = True+ conj (RCons b rec) = b && conj rec++-------------------------------------------------------------------------------+-- | Type level validation for the datatypes to be rewritten: there can be no+-- recursive calls on the leftmost constructor+-------------------------------------------------------------------------------++class Empty a where+ empty' :: a++instance Empty U where empty' = U+ +instance (HasRec a, Empty a, Empty b) => Empty (a :+: b) where+ empty' = if hasRec' (empty' :: a) then R empty' else L empty'+ +instance (Empty a, Empty b) => Empty (a :*: b) where+ empty' = empty' :*: empty'+ +instance (Empty a) => Empty (C c a) where+ empty' = C empty'++instance (Rewritable a) => Empty (Var a) where+ empty' = Var gempty++instance (Rewritable a) => Empty (Rec a) where+ empty' = Rec gempty++instance Empty Int where empty' = 0+instance Empty Float where empty' = 0+instance Empty Char where empty' = '\NUL'+++-- Dispatcher+gempty :: (Representable a, Empty (Rep a)) => a+gempty = to empty'+++-- Used to avoid producing infinite values+class HasRec a where+ hasRec' :: a -> Bool+ hasRec' _ = False+ +instance HasRec U+instance HasRec (Var a)++instance (HasRec a, HasRec b) => HasRec (a :*: b) where+ hasRec' (a :*: b) = hasRec' a || hasRec' b+ +instance (HasRec a, HasRec b) => HasRec (a :+: b) where+ hasRec' (L x) = hasRec' x+ hasRec' (R x) = hasRec' x++instance (HasRec a) => HasRec (C c a) where+ hasRec' (C x) = hasRec' x+ +instance HasRec (Rec a) where+ hasRec' _ = True+ +instance HasRec Int+instance HasRec Float+instance HasRec Char++type family Finite a :: *+type instance Finite Int = True+type instance Finite Float = True+type instance Finite Char = True+type instance Finite U = True+type instance Finite (a :+: b) = Or (Finite a) (Finite b)+type instance Finite (a :*: b) = And (Finite a) (Finite b)+type instance Finite (Rec a) = False+type instance Finite (Var a) = True+type instance Finite (C c a) = Finite a++data True+data False++type family And p q+type instance And True True = True+type instance And True False = False+type instance And False True = False+type instance And False False = False++type family Or p q+type instance Or True True = True+type instance Or True False = True+type instance Or False True = True+type instance Or False False = False++type family FiniteEnv gam+type instance FiniteEnv U = True+type instance FiniteEnv (a :*: gam) = And (Finite (Rep a)) (FiniteEnv gam)++-------------------------------------------------------------------------------+-- Convenience: hiding the environment to the user Rule' type+-------------------------------------------------------------------------------++-- | Rules+data Rule a where+ Rule :: (Nillable gam, Recordable gam, Testable gam)+ => Rule' a gam -> Rule a++-- | Validate a rewrite rule+validate :: Rewritable a => Rule a -> Bool+validate (Rule rule) = validate' rule++-- | Synthesise a function into a rewrite rule+synthesise :: (IsRule a, Nillable (Env a), Recordable (Env a), + Testable (Env a), FiniteEnv (Env a) ~ True)+ => a -> Rule (Obj a)+synthesise r = Rule (synthesise' r)++-- | Rewrite a term. The term is unchanged if the rule cannot be applied.+rewrite :: Rewritable a => Rule a -> a -> a+rewrite (Rule rule) x = rewrite' rule x++-- | Rewrite a term. Monad 'fail' is used if the rule cannot be applied.+rewriteM :: (Rewritable a, Monad m) => Rule a -> a -> m a+rewriteM (Rule rule) x = rewriteM' rule x