Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Get the examples to compile.

  • Loading branch information...
commit 34aaaaa67ea5627980a59224c00dc466090f79a7 1 parent 1d16a53
@leepike authored
View
4 examples/Div0.hs
@@ -63,8 +63,8 @@ div1 m = divSubTerms m ==> eval m /= Nothing
-- div0 (A _ _) = property False
-- div0 _ = property True
-main :: IO ()
-main = smartCheck args div1
+divTest :: IO ()
+divTest = smartCheck args div1
where
args = scStdArgs { qcArgs = stdArgs
{ maxSuccess = 100
View
108 examples/Heap_Program.hs
@@ -2,13 +2,12 @@
-- Copied from QuickCheck2's examples.
-module Main where
+module Heap_Program where
--------------------------------------------------------------------------
-- imports
import Test.QuickCheck
-import Test.QuickCheck.Text
import Test.QuickCheck.All
import Test.QuickCheck.Poly
@@ -17,15 +16,58 @@ import Data.List
, (\\)
)
-import Control.Monad
- ( liftM
- , liftM2
- )
-
+import qualified Data.Tree as T
import Data.Data
import qualified Test.SmartCheck as SC
--------------------------------------------------------------------------
+-- SmartCheck Testing. Comment out shrink instance if you want to be more
+-- impressed. :)
+--------------------------------------------------------------------------
+
+instance Read OrdA where
+ readsPrec _ i = [ (OrdA j, str) | (j, str) <- reads i ]
+
+deriving instance Data OrdA
+deriving instance Typeable OrdA
+
+heapProgramTest :: IO ()
+heapProgramTest = SC.smartCheck SC.scStdArgs (\h -> property (prop_ToSortedList h))
+
+instance (Ord a, Arbitrary a, Data a, Show a) => SC.SubTypes (Heap a) where
+ subTypes Nil = []
+ subTypes (Node x h0 h1) =
+ [ T.Node (SC.subT x) []
+ , T.Node (SC.subT h0) (SC.subTypes h0)
+ , T.Node (SC.subT h1) (SC.subTypes h1)
+ ]
+
+instance (Arbitrary a, Data a, Show a) => SC.SubTypes (HeapP a) where
+ subTypes Empty = []
+ subTypes (Unit a) = [ T.Node (SC.subT a) [] ]
+ subTypes (Insert i h) =
+ [ T.Node (SC.subT i) []
+ , T.Node (SC.subT h) (SC.subTypes h)
+ ]
+ subTypes (SafeRemoveMin h) =
+ [ T.Node (SC.subT h) (SC.subTypes h) ]
+ subTypes (Merge h0 h1) =
+ [ T.Node (SC.subT h0) (SC.subTypes h0)
+ , T.Node (SC.subT h1) (SC.subTypes h1)
+ ]
+ subTypes (FromList a) = [ T.Node (SC.subT a) [] ]
+
+instance (Ord a, Arbitrary a, Data a, Show a) => SC.SubTypes (HeapPP a) where
+ subTypes (HeapPP hp h) =
+ [ T.Node (SC.subT hp) (SC.subTypes hp)
+ , T.Node (SC.subT h) (SC.subTypes h)
+ ]
+
+instance (Ord a, Arbitrary a) => Arbitrary (Heap a) where
+ arbitrary = do p <- arbitrary :: Gen (HeapP a)
+ return $ heap p
+
+--------------------------------------------------------------------------
-- skew heaps
data Heap a
@@ -33,9 +75,6 @@ data Heap a
| Nil
deriving ( Eq, Ord, Show, Read, Data, Typeable )
--- instance Read a => Read (Heap a) where
--- readsPrec _ =
-
empty :: Heap a
empty = Nil
@@ -132,18 +171,18 @@ instance Arbitrary a => Arbitrary (HeapP a) where
s2 = s`div`2
- shrink (Unit x) = [ Unit x' | x' <- shrink x ]
- shrink (FromList xs) = [ Unit x | x <- xs ]
- ++ [ FromList xs' | xs' <- shrink xs ]
- shrink (Insert x p) = [ p ]
- ++ [ Insert x p' | p' <- shrink p ]
- ++ [ Insert x' p | x' <- shrink x ]
- shrink (SafeRemoveMin p) = [ p ]
- ++ [ SafeRemoveMin p' | p' <- shrink p ]
- shrink (Merge p q) = [ p, q ]
- ++ [ Merge p' q | p' <- shrink p ]
- ++ [ Merge p q' | q' <- shrink q ]
- shrink _ = []
+ -- shrink (Unit x) = [ Unit x' | x' <- shrink x ]
+ -- shrink (FromList xs) = [ Unit x | x <- xs ]
+ -- ++ [ FromList xs' | xs' <- shrink xs ]
+ -- shrink (Insert x p) = [ p ]
+ -- ++ [ Insert x p' | p' <- shrink p ]
+ -- ++ [ Insert x' p | x' <- shrink x ]
+ -- shrink (SafeRemoveMin p) = [ p ]
+ -- ++ [ SafeRemoveMin p' | p' <- shrink p ]
+ -- shrink (Merge p q) = [ p, q ]
+ -- ++ [ Merge p' q | p' <- shrink p ]
+ -- ++ [ Merge p q' | q' <- shrink q ]
+ -- shrink _ = []
data HeapPP a = HeapPP (HeapP a) (Heap a)
deriving (Show, Read, Data, Typeable)
@@ -197,30 +236,7 @@ prop_ToSortedList (HeapPP _ h) =
--------------------------------------------------------------------------
-- main
-main = $(quickCheckAll)
+-- main = $(quickCheckAll)
--------------------------------------------------------------------------
-- the end.
-
-instance Read OrdA where
- readsPrec _ i = [ (OrdA j, str) | (j, str) <- reads i ]
-
-deriving instance Data OrdA
-deriving instance Typeable OrdA
-
-sc :: IO ()
-sc = SC.smartCheck stdArgs (\h -> property (prop_ToSortedList h))
-
-instance (Arbitrary a, Data a, Show a) => SC.SubTypes (HeapPP a) where
- subTypes (HeapPP hp _) =
- [ SC.Node (SC.subT hp) (SC.subTypes hp)
- ]
-
-instance (Arbitrary a, Data a, Show a) => SC.SubTypes (HeapP a) where
- subTypes (Insert _ h) = [ SC.Node (SC.subT h) (SC.subTypes h) ]
- subTypes (SafeRemoveMin h) = [ SC.Node (SC.subT h) (SC.subTypes h) ]
- subTypes (Merge h0 h1) =
- [ SC.Node (SC.subT h0) (SC.subTypes h0)
- , SC.Node (SC.subT h1) (SC.subTypes h1)
- ]
- subTypes _ = []
View
7 examples/MutualRecData.hs
@@ -5,6 +5,7 @@ module MutualRecData where
import Test.SmartCheck
import Test.QuickCheck hiding (Result)
+import Data.Tree
import Data.Data
import Control.Monad.State
@@ -63,11 +64,11 @@ prop0 :: M -> Bool
prop0 (M _ _ a) = a < 100
prop0 _ = True
-main :: IO ()
-main = smartCheck args p
+mutRecTest :: IO ()
+mutRecTest = smartCheck args p
where
p = \a -> property (prop0 a)
- args = stdArgs { maxSuccess = 1000 }
+ args = scStdArgs { qcArgs = stdArgs {maxSuccess = 1000} }
---------------------------------------------------------------------------------
View
15 examples/Tests.hs
@@ -0,0 +1,15 @@
+module Tests where
+
+import Div0
+import MutualRecData
+import Heap_Program
+import LambdaCalc
+--import Protocol
+
+main :: IO ()
+main = do
+ divTest
+ mutRecTest
+ heapProgramTest
+ lambdaTest
+-- protocolTest
View
77 src/Test/SmartCheck/Render.hs
@@ -9,6 +9,7 @@ import Test.SmartCheck.DataToTree
import Data.Tree
import Data.Data
import Data.List
+import Data.Char
---------------------------------------------------------------------------------
@@ -20,24 +21,11 @@ smartPrtLn = putStrLn . (smartPrefix ++)
---------------------------------------------------------------------------------
--- Make a Tree out of a Data value. On each level, we just use the user-defined
--- Show instance. This is good in that it's what user expects, but it's bad in
--- that we show the entire subtree at each level.
---
--- XXX Also, it's inconsistent since toConstr is not part of the user-defined
--- show instances.
-mkShowTree :: SubTypes a => a -> Tree String
-mkShowTree d = Node (show $ toConstr d) (strForest $ subTypes d)
-
-strForest :: Forest SubT -> Forest String
-strForest =
- fmap (\(Node r forest) -> Node (show r) (strForest forest))
-
----------------------------------------------------------------------------------
-
renderWithVars :: SubTypes a => Format -> a -> [Idx] -> IO ()
renderWithVars format d idxs = do
putStrLn $ "forall " ++ unwords (take (length idxs) vars) ++ ":"
+ -- XXX
+ putStrLn $ show idxs
putStrLn ""
putStrLn $ replaceWithVars format d idxs vars
putStrLn ""
@@ -56,7 +44,7 @@ replaceWithVars format d idxs vars =
-- matching substrings to replace, since the same substring may show up in
-- multiple places. Rather, we have to recursively descend down the tree of
-- substrings, finding matches, til we hit our variable.
--- PrntString -> foldl' g (show d) vis
+ PrntString -> error "not implemented" --foldl' g (show d) vis
where
t = mkShowTree d
@@ -66,26 +54,26 @@ replaceWithVars format d idxs vars =
f tree (var, idx) = let forest = sub (subForest tree) idx var False in
Node (rootLabel tree) forest
- subF = mkSubstForest d
+ -- subF = mkSubstForest d
- g :: String -> (String, Idx) -> String
- g showTree (var, idx) =
- let subPath = sub subF idx Subst True in
- replaceStr showTree var idx subPath
+ -- g :: String -> (String, Idx) -> String
+ -- g showTree (var, idx) =
+ -- let subPath = sub subF idx Subst True in
+ -- replaceStr showTree var idx subPath
---------------------------------------------------------------------------------
-printTree :: Tree String -> String
-printTree (Node str forest) =
- str ++ " " ++ concatMap printTree' forest
- where
- printTree' (Node s []) = s ++ " "
- printTree' (Node s f) = "(" ++ s ++ ")" --" " ++ concatMap printTree' f ++ ")"
+-- printTree :: Tree String -> String
+-- printTree (Node str forest) =
+-- str ++ " " ++ concatMap printTree' forest
+-- where
+-- printTree' (Node s []) = s ++ " "
+-- printTree' (Node s f) = "(" ++ s ++ ")" --" " ++ concatMap printTree' f ++ ")"
---------------------------------------------------------------------------------
-replaceStr :: String -> String -> Idx -> Forest Subst -> String
-replaceStr tree var idx subPath = undefined
+-- replaceStr :: String -> String -> Idx -> Forest Subst -> String
+-- replaceStr tree var idx subPath = undefined
---------------------------------------------------------------------------------
@@ -97,3 +85,34 @@ replaceStr tree var idx subPath = undefined
-- Just i -> take i ls ++ b : drop (i+1) ls
---------------------------------------------------------------------------------
+
+-- Make a Tree out of a Data value. On each level, we just use the user-defined
+-- Show instance. This is good in that it's what user expects, but it's bad in
+-- that we show the entire subtree at each level.
+--
+-- XXX Also, it's inconsistent since toConstr is not part of the user-defined
+-- show instances.
+mkShowTree :: SubTypes a => a -> Tree String
+mkShowTree d = Node (show $ toConstr d) (strForest $ subTypes d)
+
+strForest :: Forest SubT -> Forest String
+strForest = fmap prtTree
+
+ where
+ prtTree (Node r forest) =
+ let rec = strForest forest in
+ let nextLevel = fmap rootLabel rec in
+ Node (stripSuffix (show r) nextLevel) rec
+
+ -- If the proposed suffix is not actually a suffix, we just return the
+ -- original string. We eat spaces and parentheses. XXX, yes, this is a bit
+ -- of a hack.
+ stripSuffix :: String -> [String] -> String
+ stripSuffix st ls =
+ let suffix = concat ls in
+ let st' = filter (\c -> c /= '(' && c /= ')' && (not . isSpace) c) st in
+ case stripPrefix (reverse suffix) (reverse st') of
+ Nothing -> st
+ Just x -> reverse x
+
+---------------------------------------------------------------------------------
Please sign in to comment.
Something went wrong with that request. Please try again.