1.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Fri Mar 11 15:21:13 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Fri Mar 11 15:21:13 2011 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -module LazySmallCheck where {
     1.5 +module Narrowing_Engine where {
     1.6  
     1.7  import Monad;
     1.8  import Control.Exception;
     1.9 @@ -10,20 +10,20 @@
    1.10  
    1.11  -- Term refinement
    1.12  
    1.13 -new :: Pos -> [[Type]] -> [Term];
    1.14 +new :: Pos -> [[Type]] -> [Terma];
    1.15  new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
    1.16             | (c, ts) <- zip [0..] ps ];
    1.17  
    1.18 -refine :: Term -> Pos -> [Term];
    1.19 +refine :: Terma -> Pos -> [Terma];
    1.20  refine (Var p (SumOfProd ss)) [] = new p ss;
    1.21  refine (Ctr c xs) p = map (Ctr c) (refineList xs p);
    1.22  
    1.23 -refineList :: [Term] -> Pos -> [[Term]];
    1.24 +refineList :: [Terma] -> Pos -> [[Terma]];
    1.25  refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
    1.26  
    1.27  -- Find total instantiations of a partial value
    1.28  
    1.29 -total :: Term -> [Term];
    1.30 +total :: Terma -> [Terma];
    1.31  total (Ctr c xs) = [Ctr c ys | ys <- mapM total xs];
    1.32  total (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- total x];
    1.33  
    1.34 @@ -42,13 +42,13 @@
    1.35  str_of_list [] = "[]";
    1.36  str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
    1.37  
    1.38 -report :: Result -> [Term] -> IO Int;
    1.39 +report :: Result -> [Terma] -> IO Int;
    1.40  report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) $ head [ys | ys <- mapM total xs]) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
    1.41  
    1.42  eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
    1.43  eval p k u = answer p (\p -> answer p k u) u;
    1.44  
    1.45 -ref :: Result -> [Term] -> IO Int;
    1.46 +ref :: Result -> [Terma] -> IO Int;
    1.47  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.48            
    1.49  refute :: Result -> IO Int;
    1.50 @@ -64,25 +64,25 @@
    1.51    show (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
    1.52  };
    1.53  
    1.54 -instance Show Terma where {
    1.55 +instance Show Term where {
    1.56    show (Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
    1.57    show (App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
    1.58    show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";  
    1.59  };
    1.60  
    1.61  data Result =
    1.62 -  Result { args     :: [Term]
    1.63 -         , showArgs :: [Term -> String]
    1.64 -         , apply_fun    :: [Term] -> Bool
    1.65 +  Result { args     :: [Terma]
    1.66 +         , showArgs :: [Terma -> String]
    1.67 +         , apply_fun    :: [Terma] -> Bool
    1.68           };
    1.69  
    1.70  data P = P (Int -> Int -> Result);
    1.71  
    1.72 -run :: Testable a => ([Term] -> a) -> Int -> Int -> Result;
    1.73 +run :: Testable a => ([Terma] -> a) -> Int -> Int -> Result;
    1.74  run a = let P f = property a in f;
    1.75  
    1.76  class Testable a where {
    1.77 -  property :: ([Term] -> a) -> P;
    1.78 +  property :: ([Terma] -> a) -> P;
    1.79  };
    1.80  
    1.81  instance Testable Bool where {

     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 11 15:21:13 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 11 15:21:13 2011 +0100
     2.3 @@ -34,9 +34,9 @@
     2.4          val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
     2.5          val main_file = Path.append in_path (Path.basic "Main.hs")
     2.6          val main = "module Main where {\n\n" ^
     2.7 -          "import LazySmallCheck;\n" ^
     2.8 +          "import Narrowing_Engine;\n" ^
     2.9            "import Code;\n\n" ^
    2.10 -          "main = LazySmallCheck.smallCheck 7 (Code.value ())\n\n" ^
    2.11 +          "main = Narrowing_Engine.smallCheck 7 (Code.value ())\n\n" ^
    2.12            "}\n"
    2.13          val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    2.14            (unprefix "module Code where {" code)