src/HOL/Tools/Quickcheck/Narrowing_Engine.hs

--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon May 30 12:20:04 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon May 30 13:57:59 2011 +0200
@@ -10,20 +10,20 @@
 
 -- Term refinement
 
-new :: Pos -> [[Type]] -> [Terma];
+new :: Pos -> [[Narrowing_type]] -> [Narrowing_term];
 new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
            | (c, ts) <- zip [0..] ps ];
 
-refine :: Terma -> Pos -> [Terma];
+refine :: Narrowing_term -> Pos -> [Narrowing_term];
 refine (Var p (SumOfProd ss)) [] = new p ss;
 refine (Ctr c xs) p = map (Ctr c) (refineList xs p);
 
-refineList :: [Terma] -> Pos -> [[Terma]];
+refineList :: [Narrowing_term] -> Pos -> [[Narrowing_term]];
 refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
 
 -- Find total instantiations of a partial value
 
-total :: Terma -> [Terma];
+total :: Narrowing_term -> [Narrowing_term];
 total (Ctr c xs) = [Ctr c ys | ys <- mapM total xs];
 total (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- total x];
 
@@ -42,13 +42,13 @@
 str_of_list [] = "[]";
 str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
 
-report :: Result -> [Terma] -> IO Int;
+report :: Result -> [Narrowing_term] -> IO Int;
 report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) $ head [ys | ys <- mapM total xs]) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
 
 eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
 eval p k u = answer p (\p -> answer p k u) u;
 
-ref :: Result -> [Terma] -> IO Int;
+ref :: Result -> [Narrowing_term] -> IO Int;
 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));
           
 refute :: Result -> IO Int;
@@ -71,18 +71,18 @@
 };
 
 data Result =
-  Result { args     :: [Terma]
-         , showArgs :: [Terma -> String]
-         , apply_fun    :: [Terma] -> Bool
+  Result { args     :: [Narrowing_term]
+         , showArgs :: [Narrowing_term -> String]
+         , apply_fun    :: [Narrowing_term] -> Bool
          };
 
 data P = P (Int -> Int -> Result);
 
-run :: Testable a => ([Terma] -> a) -> Int -> Int -> Result;
+run :: Testable a => ([Narrowing_term] -> a) -> Int -> Int -> Result;
 run a = let P f = property a in f;
 
 class Testable a where {
-  property :: ([Terma] -> a) -> P;
+  property :: ([Narrowing_term] -> a) -> P;
 };
 
 instance Testable Bool where {