src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
changeset 46758 4106258260b3
parent 46335 0fd9ab902b5a
child 55676 fb46f1c379b5
     1.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Fri Mar 02 09:35:33 2012 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Fri Mar 02 09:35:35 2012 +0100
     1.3 @@ -11,12 +11,12 @@
     1.4  -- Term refinement
     1.5  
     1.6  new :: Pos -> [[Generated_Code.Narrowing_type]] -> [Generated_Code.Narrowing_term];
     1.7 -new p ps = [ Generated_Code.Ctr c (zipWith (\i t -> Generated_Code.Var (p++[i]) t) [0..] ts)
     1.8 +new p ps = [ Generated_Code.Narrowing_constructor c (zipWith (\i t -> Generated_Code.Narrowing_variable (p++[i]) t) [0..] ts)
     1.9             | (c, ts) <- zip [0..] ps ];
    1.10  
    1.11  refine :: Generated_Code.Narrowing_term -> Pos -> [Generated_Code.Narrowing_term];
    1.12 -refine (Generated_Code.Var p (Generated_Code.SumOfProd ss)) [] = new p ss;
    1.13 -refine (Generated_Code.Ctr c xs) p = map (Generated_Code.Ctr c) (refineList xs p);
    1.14 +refine (Generated_Code.Narrowing_variable p (Generated_Code.Narrowing_sum_of_products ss)) [] = new p ss;
    1.15 +refine (Generated_Code.Narrowing_constructor c xs) p = map (Generated_Code.Narrowing_constructor c) (refineList xs p);
    1.16  
    1.17  refineList :: [Generated_Code.Narrowing_term] -> Pos -> [[Generated_Code.Narrowing_term]];
    1.18  refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
    1.19 @@ -24,8 +24,8 @@
    1.20  -- Find total instantiations of a partial value
    1.21  
    1.22  total :: Generated_Code.Narrowing_term -> [Generated_Code.Narrowing_term];
    1.23 -total (Generated_Code.Ctr c xs) = [Generated_Code.Ctr c ys | ys <- mapM total xs];
    1.24 -total (Generated_Code.Var p (Generated_Code.SumOfProd ss)) = [y | x <- new p ss, y <- total x];
    1.25 +total (Generated_Code.Narrowing_constructor c xs) = [Generated_Code.Narrowing_constructor c ys | ys <- mapM total xs];
    1.26 +total (Generated_Code.Narrowing_variable p (Generated_Code.Narrowing_sum_of_products ss)) = [y | x <- new p ss, y <- total x];
    1.27  
    1.28  -- Answers
    1.29  
    1.30 @@ -99,10 +99,10 @@
    1.31  
    1.32  instance (Generated_Code.Partial_term_of a, Generated_Code.Narrowing a, Testable b) => Testable (a -> b) where {
    1.33    property f = P $ \n d ->
    1.34 -    let Generated_Code.C t c = Generated_Code.narrowing d
    1.35 +    let Generated_Code.Narrowing_cons t c = Generated_Code.narrowing d
    1.36          c' = Generated_Code.conv c
    1.37          r = run (\(x:xs) -> f xs (c' x)) (n+1) d
    1.38 -    in  r { args = Generated_Code.Var [n] t : args r,
    1.39 +    in  r { args = Generated_Code.Narrowing_variable [n] t : args r,
    1.40        showArgs = (show . Generated_Code.partial_term_of (Generated_Code.Type :: Generated_Code.Itself a)) : showArgs r };
    1.41  };
    1.42