src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
changeset 45081 f00e52acbd42
parent 45003 7591039fb6b4
child 45685 e2e928af750b
     1.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Sun Sep 25 19:34:20 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Sep 26 10:30:37 2011 +0200
     1.3 @@ -4,28 +4,28 @@
     1.4  import Control.Exception;
     1.5  import System.IO;
     1.6  import System.Exit;
     1.7 -import Generated_Code;
     1.8 +import qualified Generated_Code;
     1.9  
    1.10  type Pos = [Int];
    1.11  
    1.12  -- Term refinement
    1.13  
    1.14 -new :: Pos -> [[Narrowing_type]] -> [Narrowing_term];
    1.15 -new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
    1.16 +new :: Pos -> [[Generated_Code.Narrowing_type]] -> [Generated_Code.Narrowing_term];
    1.17 +new p ps = [ Generated_Code.Ctr c (zipWith (\i t -> Generated_Code.Var (p++[i]) t) [0..] ts)
    1.18             | (c, ts) <- zip [0..] ps ];
    1.19  
    1.20 -refine :: Narrowing_term -> Pos -> [Narrowing_term];
    1.21 -refine (Var p (SumOfProd ss)) [] = new p ss;
    1.22 -refine (Ctr c xs) p = map (Ctr c) (refineList xs p);
    1.23 +refine :: Generated_Code.Narrowing_term -> Pos -> [Generated_Code.Narrowing_term];
    1.24 +refine (Generated_Code.Var p (Generated_Code.SumOfProd ss)) [] = new p ss;
    1.25 +refine (Generated_Code.Ctr c xs) p = map (Generated_Code.Ctr c) (refineList xs p);
    1.26  
    1.27 -refineList :: [Narrowing_term] -> Pos -> [[Narrowing_term]];
    1.28 +refineList :: [Generated_Code.Narrowing_term] -> Pos -> [[Generated_Code.Narrowing_term]];
    1.29  refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
    1.30  
    1.31  -- Find total instantiations of a partial value
    1.32  
    1.33 -total :: Narrowing_term -> [Narrowing_term];
    1.34 -total (Ctr c xs) = [Ctr c ys | ys <- mapM total xs];
    1.35 -total (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- total x];
    1.36 +total :: Generated_Code.Narrowing_term -> [Generated_Code.Narrowing_term];
    1.37 +total (Generated_Code.Ctr c xs) = [Generated_Code.Ctr c ys | ys <- mapM total xs];
    1.38 +total (Generated_Code.Var p (Generated_Code.SumOfProd ss)) = [y | x <- new p ss, y <- total x];
    1.39  
    1.40  -- Answers
    1.41  
    1.42 @@ -47,13 +47,13 @@
    1.43  str_of_list [] = "[]";
    1.44  str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
    1.45  
    1.46 -report :: Result -> [Narrowing_term] -> IO Int;
    1.47 +report :: Result -> [Generated_Code.Narrowing_term] -> IO Int;
    1.48  report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
    1.49  
    1.50  eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
    1.51  eval p k u = answer p (\p -> answer p k u) u;
    1.52  
    1.53 -ref :: Result -> [Narrowing_term] -> IO Int;
    1.54 +ref :: Result -> [Generated_Code.Narrowing_term] -> IO Int;
    1.55  ref r xs = eval (apply_fun r xs) (\res -> if res then return 1 else report r xs) (\p -> sumMapM (ref r) 1 (refineList xs p));
    1.56            
    1.57  refute :: Result -> IO Int;
    1.58 @@ -65,42 +65,43 @@
    1.59  
    1.60  -- Testable
    1.61  
    1.62 -instance Show Typerep where {
    1.63 -  show (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
    1.64 +instance Show Generated_Code.Typerep where {
    1.65 +  show (Generated_Code.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
    1.66  };
    1.67  
    1.68 -instance Show Term where {
    1.69 -  show (Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
    1.70 -  show (App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
    1.71 -  show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
    1.72 -  show (Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
    1.73 +instance Show Generated_Code.Term where {
    1.74 +  show (Generated_Code.Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
    1.75 +  show (Generated_Code.App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
    1.76 +  show (Generated_Code.Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
    1.77 +  show (Generated_Code.Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
    1.78  };
    1.79  
    1.80  data Result =
    1.81 -  Result { args     :: [Narrowing_term]
    1.82 -         , showArgs :: [Narrowing_term -> String]
    1.83 -         , apply_fun    :: [Narrowing_term] -> Bool
    1.84 +  Result { args     :: [Generated_Code.Narrowing_term]
    1.85 +         , showArgs :: [Generated_Code.Narrowing_term -> String]
    1.86 +         , apply_fun    :: [Generated_Code.Narrowing_term] -> Bool
    1.87           };
    1.88  
    1.89  data P = P (Int -> Int -> Result);
    1.90  
    1.91 -run :: Testable a => ([Narrowing_term] -> a) -> Int -> Int -> Result;
    1.92 +run :: Testable a => ([Generated_Code.Narrowing_term] -> a) -> Int -> Int -> Result;
    1.93  run a = let P f = property a in f;
    1.94  
    1.95  class Testable a where {
    1.96 -  property :: ([Narrowing_term] -> a) -> P;
    1.97 +  property :: ([Generated_Code.Narrowing_term] -> a) -> P;
    1.98  };
    1.99  
   1.100  instance Testable Bool where {
   1.101    property app = P $ \n d -> Result [] [] (app . reverse);
   1.102  };
   1.103  
   1.104 -instance (Partial_term_of a, Narrowing a, Testable b) => Testable (a -> b) where {
   1.105 +instance (Generated_Code.Partial_term_of a, Generated_Code.Narrowing a, Testable b) => Testable (a -> b) where {
   1.106    property f = P $ \n d ->
   1.107 -    let C t c = narrowing d
   1.108 -        c' = conv c
   1.109 +    let Generated_Code.C t c = Generated_Code.narrowing d
   1.110 +        c' = Generated_Code.conv c
   1.111          r = run (\(x:xs) -> f xs (c' x)) (n+1) d
   1.112 -    in  r { args = Var [n] t : args r, showArgs = (show . partial_term_of (Type :: Itself a)) : showArgs r };
   1.113 +    in  r { args = Generated_Code.Var [n] t : args r,
   1.114 +      showArgs = (show . Generated_Code.partial_term_of (Generated_Code.Type :: Generated_Code.Itself a)) : showArgs r };
   1.115  };
   1.116  
   1.117  -- Top-level interface