# HG changeset patch
# User bulwahn
# Date 1317025837 -7200
# Node ID f00e52acbd42d1546aa4a48b39374e807428351e
# Parent  b4f1beba1897927a28737daed476c2a2733d2ce4
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

diff -r b4f1beba1897 -r f00e52acbd42 src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Sun Sep 25 19:34:20 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon Sep 26 10:30:37 2011 +0200
@@ -4,28 +4,28 @@
 import Control.Exception;
 import System.IO;
 import System.Exit;
-import Generated_Code;
+import qualified Generated_Code;
 
 type Pos = [Int];
 
 -- Term refinement
 
-new :: Pos -> [[Narrowing_type]] -> [Narrowing_term];
-new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
+new :: Pos -> [[Generated_Code.Narrowing_type]] -> [Generated_Code.Narrowing_term];
+new p ps = [ Generated_Code.Ctr c (zipWith (\i t -> Generated_Code.Var (p++[i]) t) [0..] ts)
            | (c, ts) <- zip [0..] ps ];
 
-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);
+refine :: Generated_Code.Narrowing_term -> Pos -> [Generated_Code.Narrowing_term];
+refine (Generated_Code.Var p (Generated_Code.SumOfProd ss)) [] = new p ss;
+refine (Generated_Code.Ctr c xs) p = map (Generated_Code.Ctr c) (refineList xs p);
 
-refineList :: [Narrowing_term] -> Pos -> [[Narrowing_term]];
+refineList :: [Generated_Code.Narrowing_term] -> Pos -> [[Generated_Code.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 :: 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];
+total :: Generated_Code.Narrowing_term -> [Generated_Code.Narrowing_term];
+total (Generated_Code.Ctr c xs) = [Generated_Code.Ctr c ys | ys <- mapM total xs];
+total (Generated_Code.Var p (Generated_Code.SumOfProd ss)) = [y | x <- new p ss, y <- total x];
 
 -- Answers
 
@@ -47,13 +47,13 @@
 str_of_list [] = "[]";
 str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
 
-report :: Result -> [Narrowing_term] -> IO Int;
+report :: Result -> [Generated_Code.Narrowing_term] -> IO Int;
 report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) 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 -> [Narrowing_term] -> IO Int;
+ref :: Result -> [Generated_Code.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;
@@ -65,42 +65,43 @@
 
 -- Testable
 
-instance Show Typerep where {
-  show (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
+instance Show Generated_Code.Typerep where {
+  show (Generated_Code.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
 };
 
-instance Show Term where {
-  show (Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
-  show (App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
-  show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
-  show (Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
+instance Show Generated_Code.Term where {
+  show (Generated_Code.Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
+  show (Generated_Code.App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
+  show (Generated_Code.Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
+  show (Generated_Code.Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
 };
 
 data Result =
-  Result { args     :: [Narrowing_term]
-         , showArgs :: [Narrowing_term -> String]
-         , apply_fun    :: [Narrowing_term] -> Bool
+  Result { args     :: [Generated_Code.Narrowing_term]
+         , showArgs :: [Generated_Code.Narrowing_term -> String]
+         , apply_fun    :: [Generated_Code.Narrowing_term] -> Bool
          };
 
 data P = P (Int -> Int -> Result);
 
-run :: Testable a => ([Narrowing_term] -> a) -> Int -> Int -> Result;
+run :: Testable a => ([Generated_Code.Narrowing_term] -> a) -> Int -> Int -> Result;
 run a = let P f = property a in f;
 
 class Testable a where {
-  property :: ([Narrowing_term] -> a) -> P;
+  property :: ([Generated_Code.Narrowing_term] -> a) -> P;
 };
 
 instance Testable Bool where {
   property app = P $ \n d -> Result [] [] (app . reverse);
 };
 
-instance (Partial_term_of a, Narrowing a, Testable b) => Testable (a -> b) where {
+instance (Generated_Code.Partial_term_of a, Generated_Code.Narrowing a, Testable b) => Testable (a -> b) where {
   property f = P $ \n d ->
-    let C t c = narrowing d
-        c' = conv c
+    let Generated_Code.C t c = Generated_Code.narrowing d
+        c' = Generated_Code.conv c
         r = run (\(x:xs) -> f xs (c' x)) (n+1) d
-    in  r { args = Var [n] t : args r, showArgs = (show . partial_term_of (Type :: Itself a)) : showArgs r };
+    in  r { args = Generated_Code.Var [n] t : args r,
+      showArgs = (show . Generated_Code.partial_term_of (Generated_Code.Type :: Generated_Code.Itself a)) : showArgs r };
 };
 
 -- Top-level interface
diff -r b4f1beba1897 -r f00e52acbd42 src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Sun Sep 25 19:34:20 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Mon Sep 26 10:30:37 2011 +0200
@@ -8,7 +8,7 @@
 import System.Exit
 import Maybe
 import List (partition, findIndex)
-import Generated_Code
+import qualified Generated_Code
 
 
 type Pos = [Int]
@@ -25,11 +25,11 @@
 tailPosEdge (VN pos ty) = VN (tail pos) ty
 tailPosEdge (CtrB pos ts) = CtrB (tail pos) ts
 
-termOf :: Pos -> Path -> Narrowing_term
-termOf pos (CtrB [] i : es) = Ctr i (termListOf pos es)
-termOf pos [VN [] ty] = Var pos ty
+termOf :: Pos -> Path -> Generated_Code.Narrowing_term
+termOf pos (CtrB [] i : es) = Generated_Code.Ctr i (termListOf pos es)
+termOf pos [VN [] ty] = Generated_Code.Var pos ty
 
-termListOf :: Pos -> Path -> [Narrowing_term]
+termListOf :: Pos -> Path -> [Generated_Code.Narrowing_term]
 termListOf pos es = termListOf' 0 es
   where
     termListOf' i [] = []
@@ -93,11 +93,11 @@
 orOp (UnknownValue b1) (UnknownValue b2) = UnknownValue (b1 && b2)
 
 
-data Edge = VN Pos Narrowing_type | CtrB Pos Int
+data Edge = VN Pos Generated_Code.Narrowing_type | CtrB Pos Int
 type Path = [Edge]
 
 data QuantTree = Node EvaluationResult
-  | VarNode Quantifier EvaluationResult Pos Narrowing_type QuantTree
+  | VarNode Quantifier EvaluationResult Pos Generated_Code.Narrowing_type QuantTree
   | CtrBranch Quantifier EvaluationResult Pos [QuantTree]
 {-
 instance Show QuantTree where
@@ -148,12 +148,12 @@
 refineTree es p t = updateTree refine (pathPrefix p es) t
   where
     pathPrefix p es = takeWhile (\e -> posOf e /= p) es  
-    refine (VarNode q r p (SumOfProd ps) t) =
+    refine (VarNode q r p (Generated_Code.SumOfProd ps) t) =
       CtrBranch q r p [ foldr (\(i,ty) t -> VarNode q r (p++[i]) ty t) t (zip [0..] ts) | ts <- ps ]
 
 -- refute
 
-refute :: ([Narrowing_term] -> Bool) -> Int -> QuantTree -> IO QuantTree
+refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Int -> QuantTree -> IO QuantTree
 refute exec d t = ref t
   where
     ref t =
@@ -165,7 +165,7 @@
             UnknownValue True -> ref t'
             _ -> return t'
 
-depthCheck :: Int -> Property -> IO ()
+depthCheck :: Int -> Generated_Code.Property -> IO ()
 depthCheck d p = refute (checkOf p) d (treeOf 0 p) >>= (\t -> 
   case evalOf t of
    Eval False -> putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")")  
@@ -175,15 +175,15 @@
 -- presentation of counterexample
 
 
-instance Show Typerep where {
-  show (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
+instance Show Generated_Code.Typerep where {
+  show (Generated_Code.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
 };
 
-instance Show Term where {
-  show (Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
-  show (App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
-  show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
-  show (Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
+instance Show Generated_Code.Term where {
+  show (Generated_Code.Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
+  show (Generated_Code.App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
+  show (Generated_Code.Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
+  show (Generated_Code.Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
 };
 {-
 posOf :: Edge -> Pos
@@ -226,10 +226,10 @@
   else
     error ""
 -}
-termlist_of :: Pos -> ([Narrowing_term], QuantTree) -> ([Narrowing_term], QuantTree)
+termlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> ([Generated_Code.Narrowing_term], QuantTree)
 termlist_of p' (terms, Node b) = (terms, Node b) 
 termlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
-    termlist_of p' (terms ++ [Var p ty], t)
+    termlist_of p' (terms ++ [Generated_Code.Var p ty], t)
   else
     (terms, VarNode q r p ty t)
 termlist_of p' (terms, CtrBranch q r p ts) = if p' == take (length p') p then
@@ -237,17 +237,17 @@
       Just i = findIndex (\t -> evalOf t == Eval False) ts
       (subterms, t') = fixp (\j -> termlist_of (p ++ [j])) 0 ([], ts !! i)
     in
-      (terms ++ [Ctr i subterms], t')
+      (terms ++ [Generated_Code.Ctr i subterms], t')
   else
     (terms, CtrBranch q r p ts)
   where
     fixp f j s = if length (fst (f j s)) == length (fst s) then s else fixp f (j + 1) (f j s)
 
 
-alltermlist_of :: Pos -> ([Narrowing_term], QuantTree) -> [([Narrowing_term], QuantTree)]
+alltermlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> [([Generated_Code.Narrowing_term], QuantTree)]
 alltermlist_of p' (terms, Node b) = [(terms, Node b)] 
 alltermlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
-    alltermlist_of p' (terms ++ [Var p ty], t)
+    alltermlist_of p' (terms ++ [Generated_Code.Var p ty], t)
   else
     [(terms, VarNode q r p ty t)]
 alltermlist_of p' (terms, CtrBranch q r p ts) =
@@ -256,7 +256,7 @@
       its = filter (\(i, t) -> evalOf t == Eval False) (zip [0..] ts)
     in
       concatMap
-        (\(i, t) -> map (\(subterms, t') -> (terms ++ [Ctr i subterms], t'))
+        (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Ctr i subterms], t'))
            (fixp (\j -> alltermlist_of (p ++ [j])) 0 ([], t))) its
   else
     [(terms, CtrBranch q r p ts)]
@@ -265,7 +265,7 @@
       [s'] -> if length (fst s') == length (fst s) then [s'] else concatMap (fixp f (j + 1)) (f j s)
       _ -> concatMap (fixp f (j + 1)) (f j s)
 
-data Example = UnivExample Narrowing_term Example | ExExample [(Narrowing_term, Example)] | EmptyExample
+data Example = UnivExample Generated_Code.Narrowing_term Example | ExExample [(Generated_Code.Narrowing_term, Example)] | EmptyExample
 
 quantifierOf (VarNode q _ _ _ _) = q
 quantifierOf (CtrBranch q _ _ _) = q
@@ -281,8 +281,8 @@
      ExistentialQ ->
        ExExample (map (\([term], rt) -> (term, exampleOf (p + 1) rt)) (alltermlist_of [p] ([], t)))
 
-data Counterexample = Universal_Counterexample (Term, Counterexample)
-  | Existential_Counterexample [(Term, Counterexample)] | Empty_Assignment
+data Counterexample = Universal_Counterexample (Generated_Code.Term, Counterexample)
+  | Existential_Counterexample [(Generated_Code.Term, Counterexample)] | Empty_Assignment
   
 instance Show Counterexample where {
 show Empty_Assignment = "Narrowing_Generators.Empty_Assignment";
@@ -290,25 +290,25 @@
 show (Existential_Counterexample x) = "Narrowing_Generators.Existential_Counterexample" ++ show x;
 };
 
-counterexampleOf :: [Narrowing_term -> Term] -> Example -> Counterexample
+counterexampleOf :: [Generated_Code.Narrowing_term -> Generated_Code.Term] -> Example -> Counterexample
 counterexampleOf [] EmptyExample = Empty_Assignment
 counterexampleOf (reify : reifys) (UnivExample t ex) = Universal_Counterexample (reify t, counterexampleOf reifys ex)
 counterexampleOf (reify : reifys) (ExExample exs) = Existential_Counterexample (map (\(t, ex) -> (reify t, counterexampleOf reifys ex)) exs)
 
-checkOf :: Property -> [Narrowing_term] -> Bool
-checkOf (Property b) = (\[] -> b)
-checkOf (Universal _ f _) = (\(t : ts) -> checkOf (f t) ts)
-checkOf (Existential _ f _) = (\(t : ts) -> checkOf (f t) ts)
+checkOf :: Generated_Code.Property -> [Generated_Code.Narrowing_term] -> Bool
+checkOf (Generated_Code.Property b) = (\[] -> b)
+checkOf (Generated_Code.Universal _ f _) = (\(t : ts) -> checkOf (f t) ts)
+checkOf (Generated_Code.Existential _ f _) = (\(t : ts) -> checkOf (f t) ts)
 
-dummy = Var [] (SumOfProd [[]])
+dummy = Generated_Code.Var [] (Generated_Code.SumOfProd [[]])
 
-treeOf :: Int -> Property -> QuantTree
-treeOf n (Property _) = Node uneval
-treeOf n (Universal ty f _)  = VarNode UniversalQ uneval [n] ty (treeOf (n + 1) (f dummy)) 
-treeOf n (Existential ty f _) = VarNode ExistentialQ uneval [n] ty (treeOf (n + 1) (f dummy))
+treeOf :: Int -> Generated_Code.Property -> QuantTree
+treeOf n (Generated_Code.Property _) = Node uneval
+treeOf n (Generated_Code.Universal ty f _)  = VarNode UniversalQ uneval [n] ty (treeOf (n + 1) (f dummy)) 
+treeOf n (Generated_Code.Existential ty f _) = VarNode ExistentialQ uneval [n] ty (treeOf (n + 1) (f dummy))
 
-reifysOf :: Property -> [Narrowing_term -> Term]
-reifysOf (Property _) = []
-reifysOf (Universal _ f r)  = (r : (reifysOf (f dummy)))
-reifysOf (Existential _ f r) = (r : (reifysOf (f dummy)))
+reifysOf :: Generated_Code.Property -> [Generated_Code.Narrowing_term -> Generated_Code.Term]
+reifysOf (Generated_Code.Property _) = []
+reifysOf (Generated_Code.Universal _ f r)  = (r : (reifysOf (f dummy)))
+reifysOf (Generated_Code.Existential _ f r) = (r : (reifysOf (f dummy)))