src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
changeset 43079 4022892a2f28
parent 43047 26774ccb1c74
child 44751 f523923d8182
     1.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon May 30 16:15:37 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon May 30 17:55:34 2011 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4  str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
     1.5  
     1.6  report :: Result -> [Narrowing_term] -> IO Int;
     1.7 -report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) $ head [ys | ys <- mapM total xs]) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
     1.8 +report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
     1.9  
    1.10  eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
    1.11  eval p k u = answer p (\p -> answer p k u) u;
    1.12 @@ -67,7 +67,8 @@
    1.13  instance Show Term where {
    1.14    show (Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
    1.15    show (App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
    1.16 -  show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";  
    1.17 +  show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
    1.18 +  show (Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
    1.19  };
    1.20  
    1.21  data Result =
    1.22 @@ -89,12 +90,12 @@
    1.23    property app = P $ \n d -> Result [] [] (app . reverse);
    1.24  };
    1.25  
    1.26 -instance (Term_of a, Narrowing a, Testable b) => Testable (a -> b) where {
    1.27 +instance (Partial_term_of a, Narrowing a, Testable b) => Testable (a -> b) where {
    1.28    property f = P $ \n d ->
    1.29      let C t c = narrowing d
    1.30          c' = conv c
    1.31          r = run (\(x:xs) -> f xs (c' x)) (n+1) d
    1.32 -    in  r { args = Var [n] t : args r, showArgs = (show . term_of . c') : showArgs r };
    1.33 +    in  r { args = Var [n] t : args r, showArgs = (show . partial_term_of (Type :: Itself a)) : showArgs r };
    1.34  };
    1.35  
    1.36  -- Top-level interface