importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
authorbulwahn
Mon Sep 26 10:30:37 2011 +0200 (2011-09-26)
changeset 45081f00e52acbd42
parent 45080 b4f1beba1897
child 45082 54c4e12bb5e0
importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
     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
     2.1 --- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Sun Sep 25 19:34:20 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Mon Sep 26 10:30:37 2011 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  import System.Exit
     2.5  import Maybe
     2.6  import List (partition, findIndex)
     2.7 -import Generated_Code
     2.8 +import qualified Generated_Code
     2.9  
    2.10  
    2.11  type Pos = [Int]
    2.12 @@ -25,11 +25,11 @@
    2.13  tailPosEdge (VN pos ty) = VN (tail pos) ty
    2.14  tailPosEdge (CtrB pos ts) = CtrB (tail pos) ts
    2.15  
    2.16 -termOf :: Pos -> Path -> Narrowing_term
    2.17 -termOf pos (CtrB [] i : es) = Ctr i (termListOf pos es)
    2.18 -termOf pos [VN [] ty] = Var pos ty
    2.19 +termOf :: Pos -> Path -> Generated_Code.Narrowing_term
    2.20 +termOf pos (CtrB [] i : es) = Generated_Code.Ctr i (termListOf pos es)
    2.21 +termOf pos [VN [] ty] = Generated_Code.Var pos ty
    2.22  
    2.23 -termListOf :: Pos -> Path -> [Narrowing_term]
    2.24 +termListOf :: Pos -> Path -> [Generated_Code.Narrowing_term]
    2.25  termListOf pos es = termListOf' 0 es
    2.26    where
    2.27      termListOf' i [] = []
    2.28 @@ -93,11 +93,11 @@
    2.29  orOp (UnknownValue b1) (UnknownValue b2) = UnknownValue (b1 && b2)
    2.30  
    2.31  
    2.32 -data Edge = VN Pos Narrowing_type | CtrB Pos Int
    2.33 +data Edge = VN Pos Generated_Code.Narrowing_type | CtrB Pos Int
    2.34  type Path = [Edge]
    2.35  
    2.36  data QuantTree = Node EvaluationResult
    2.37 -  | VarNode Quantifier EvaluationResult Pos Narrowing_type QuantTree
    2.38 +  | VarNode Quantifier EvaluationResult Pos Generated_Code.Narrowing_type QuantTree
    2.39    | CtrBranch Quantifier EvaluationResult Pos [QuantTree]
    2.40  {-
    2.41  instance Show QuantTree where
    2.42 @@ -148,12 +148,12 @@
    2.43  refineTree es p t = updateTree refine (pathPrefix p es) t
    2.44    where
    2.45      pathPrefix p es = takeWhile (\e -> posOf e /= p) es  
    2.46 -    refine (VarNode q r p (SumOfProd ps) t) =
    2.47 +    refine (VarNode q r p (Generated_Code.SumOfProd ps) t) =
    2.48        CtrBranch q r p [ foldr (\(i,ty) t -> VarNode q r (p++[i]) ty t) t (zip [0..] ts) | ts <- ps ]
    2.49  
    2.50  -- refute
    2.51  
    2.52 -refute :: ([Narrowing_term] -> Bool) -> Int -> QuantTree -> IO QuantTree
    2.53 +refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Int -> QuantTree -> IO QuantTree
    2.54  refute exec d t = ref t
    2.55    where
    2.56      ref t =
    2.57 @@ -165,7 +165,7 @@
    2.58              UnknownValue True -> ref t'
    2.59              _ -> return t'
    2.60  
    2.61 -depthCheck :: Int -> Property -> IO ()
    2.62 +depthCheck :: Int -> Generated_Code.Property -> IO ()
    2.63  depthCheck d p = refute (checkOf p) d (treeOf 0 p) >>= (\t -> 
    2.64    case evalOf t of
    2.65     Eval False -> putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")")  
    2.66 @@ -175,15 +175,15 @@
    2.67  -- presentation of counterexample
    2.68  
    2.69  
    2.70 -instance Show Typerep where {
    2.71 -  show (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
    2.72 +instance Show Generated_Code.Typerep where {
    2.73 +  show (Generated_Code.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
    2.74  };
    2.75  
    2.76 -instance Show Term where {
    2.77 -  show (Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
    2.78 -  show (App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
    2.79 -  show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
    2.80 -  show (Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
    2.81 +instance Show Generated_Code.Term where {
    2.82 +  show (Generated_Code.Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
    2.83 +  show (Generated_Code.App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
    2.84 +  show (Generated_Code.Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
    2.85 +  show (Generated_Code.Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
    2.86  };
    2.87  {-
    2.88  posOf :: Edge -> Pos
    2.89 @@ -226,10 +226,10 @@
    2.90    else
    2.91      error ""
    2.92  -}
    2.93 -termlist_of :: Pos -> ([Narrowing_term], QuantTree) -> ([Narrowing_term], QuantTree)
    2.94 +termlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> ([Generated_Code.Narrowing_term], QuantTree)
    2.95  termlist_of p' (terms, Node b) = (terms, Node b) 
    2.96  termlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
    2.97 -    termlist_of p' (terms ++ [Var p ty], t)
    2.98 +    termlist_of p' (terms ++ [Generated_Code.Var p ty], t)
    2.99    else
   2.100      (terms, VarNode q r p ty t)
   2.101  termlist_of p' (terms, CtrBranch q r p ts) = if p' == take (length p') p then
   2.102 @@ -237,17 +237,17 @@
   2.103        Just i = findIndex (\t -> evalOf t == Eval False) ts
   2.104        (subterms, t') = fixp (\j -> termlist_of (p ++ [j])) 0 ([], ts !! i)
   2.105      in
   2.106 -      (terms ++ [Ctr i subterms], t')
   2.107 +      (terms ++ [Generated_Code.Ctr i subterms], t')
   2.108    else
   2.109      (terms, CtrBranch q r p ts)
   2.110    where
   2.111      fixp f j s = if length (fst (f j s)) == length (fst s) then s else fixp f (j + 1) (f j s)
   2.112  
   2.113  
   2.114 -alltermlist_of :: Pos -> ([Narrowing_term], QuantTree) -> [([Narrowing_term], QuantTree)]
   2.115 +alltermlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> [([Generated_Code.Narrowing_term], QuantTree)]
   2.116  alltermlist_of p' (terms, Node b) = [(terms, Node b)] 
   2.117  alltermlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
   2.118 -    alltermlist_of p' (terms ++ [Var p ty], t)
   2.119 +    alltermlist_of p' (terms ++ [Generated_Code.Var p ty], t)
   2.120    else
   2.121      [(terms, VarNode q r p ty t)]
   2.122  alltermlist_of p' (terms, CtrBranch q r p ts) =
   2.123 @@ -256,7 +256,7 @@
   2.124        its = filter (\(i, t) -> evalOf t == Eval False) (zip [0..] ts)
   2.125      in
   2.126        concatMap
   2.127 -        (\(i, t) -> map (\(subterms, t') -> (terms ++ [Ctr i subterms], t'))
   2.128 +        (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Ctr i subterms], t'))
   2.129             (fixp (\j -> alltermlist_of (p ++ [j])) 0 ([], t))) its
   2.130    else
   2.131      [(terms, CtrBranch q r p ts)]
   2.132 @@ -265,7 +265,7 @@
   2.133        [s'] -> if length (fst s') == length (fst s) then [s'] else concatMap (fixp f (j + 1)) (f j s)
   2.134        _ -> concatMap (fixp f (j + 1)) (f j s)
   2.135  
   2.136 -data Example = UnivExample Narrowing_term Example | ExExample [(Narrowing_term, Example)] | EmptyExample
   2.137 +data Example = UnivExample Generated_Code.Narrowing_term Example | ExExample [(Generated_Code.Narrowing_term, Example)] | EmptyExample
   2.138  
   2.139  quantifierOf (VarNode q _ _ _ _) = q
   2.140  quantifierOf (CtrBranch q _ _ _) = q
   2.141 @@ -281,8 +281,8 @@
   2.142       ExistentialQ ->
   2.143         ExExample (map (\([term], rt) -> (term, exampleOf (p + 1) rt)) (alltermlist_of [p] ([], t)))
   2.144  
   2.145 -data Counterexample = Universal_Counterexample (Term, Counterexample)
   2.146 -  | Existential_Counterexample [(Term, Counterexample)] | Empty_Assignment
   2.147 +data Counterexample = Universal_Counterexample (Generated_Code.Term, Counterexample)
   2.148 +  | Existential_Counterexample [(Generated_Code.Term, Counterexample)] | Empty_Assignment
   2.149    
   2.150  instance Show Counterexample where {
   2.151  show Empty_Assignment = "Narrowing_Generators.Empty_Assignment";
   2.152 @@ -290,25 +290,25 @@
   2.153  show (Existential_Counterexample x) = "Narrowing_Generators.Existential_Counterexample" ++ show x;
   2.154  };
   2.155  
   2.156 -counterexampleOf :: [Narrowing_term -> Term] -> Example -> Counterexample
   2.157 +counterexampleOf :: [Generated_Code.Narrowing_term -> Generated_Code.Term] -> Example -> Counterexample
   2.158  counterexampleOf [] EmptyExample = Empty_Assignment
   2.159  counterexampleOf (reify : reifys) (UnivExample t ex) = Universal_Counterexample (reify t, counterexampleOf reifys ex)
   2.160  counterexampleOf (reify : reifys) (ExExample exs) = Existential_Counterexample (map (\(t, ex) -> (reify t, counterexampleOf reifys ex)) exs)
   2.161  
   2.162 -checkOf :: Property -> [Narrowing_term] -> Bool
   2.163 -checkOf (Property b) = (\[] -> b)
   2.164 -checkOf (Universal _ f _) = (\(t : ts) -> checkOf (f t) ts)
   2.165 -checkOf (Existential _ f _) = (\(t : ts) -> checkOf (f t) ts)
   2.166 +checkOf :: Generated_Code.Property -> [Generated_Code.Narrowing_term] -> Bool
   2.167 +checkOf (Generated_Code.Property b) = (\[] -> b)
   2.168 +checkOf (Generated_Code.Universal _ f _) = (\(t : ts) -> checkOf (f t) ts)
   2.169 +checkOf (Generated_Code.Existential _ f _) = (\(t : ts) -> checkOf (f t) ts)
   2.170  
   2.171 -dummy = Var [] (SumOfProd [[]])
   2.172 +dummy = Generated_Code.Var [] (Generated_Code.SumOfProd [[]])
   2.173  
   2.174 -treeOf :: Int -> Property -> QuantTree
   2.175 -treeOf n (Property _) = Node uneval
   2.176 -treeOf n (Universal ty f _)  = VarNode UniversalQ uneval [n] ty (treeOf (n + 1) (f dummy)) 
   2.177 -treeOf n (Existential ty f _) = VarNode ExistentialQ uneval [n] ty (treeOf (n + 1) (f dummy))
   2.178 +treeOf :: Int -> Generated_Code.Property -> QuantTree
   2.179 +treeOf n (Generated_Code.Property _) = Node uneval
   2.180 +treeOf n (Generated_Code.Universal ty f _)  = VarNode UniversalQ uneval [n] ty (treeOf (n + 1) (f dummy)) 
   2.181 +treeOf n (Generated_Code.Existential ty f _) = VarNode ExistentialQ uneval [n] ty (treeOf (n + 1) (f dummy))
   2.182  
   2.183 -reifysOf :: Property -> [Narrowing_term -> Term]
   2.184 -reifysOf (Property _) = []
   2.185 -reifysOf (Universal _ f r)  = (r : (reifysOf (f dummy)))
   2.186 -reifysOf (Existential _ f r) = (r : (reifysOf (f dummy)))
   2.187 +reifysOf :: Generated_Code.Property -> [Generated_Code.Narrowing_term -> Generated_Code.Term]
   2.188 +reifysOf (Generated_Code.Property _) = []
   2.189 +reifysOf (Generated_Code.Universal _ f r)  = (r : (reifysOf (f dummy)))
   2.190 +reifysOf (Generated_Code.Existential _ f r) = (r : (reifysOf (f dummy)))
   2.191