moving and renaming lazysmallcheck to narrowing which reflects the characteristical behaviour better

--- a/src/HOL/Tools/LSC/LazySmallCheck.hs	Fri Mar 11 15:21:13 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-module LazySmallCheck where {
-
-import Monad;
-import Control.Exception;
-import System.IO;
-import System.Exit;
-import Code;
-
-type Pos = [Int];
-
--- Term refinement
-
-new :: Pos -> [[Type]] -> [Term];
-new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
-           | (c, ts) <- zip [0..] ps ];
-
-refine :: Term -> Pos -> [Term];
-refine (Var p (SumOfProd ss)) [] = new p ss;
-refine (Ctr c xs) p = map (Ctr c) (refineList xs p);
-
-refineList :: [Term] -> Pos -> [[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 :: Term -> [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];
-
--- Answers
-
-answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
-answer a known unknown =
-  try (evaluate a) >>= (\res ->
-     case res of
-       Right b -> known b
-       Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
-       Left e -> throw e);
-
--- Refute
-
-str_of_list [] = "[]";
-str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
-
-report :: Result -> [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 -> [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;
-refute r = ref r (args r);
-
-sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
-sumMapM f n [] = return n;
-sumMapM f n (a:as) = seq n (do m <- f a ; sumMapM f (n+m) as);
-
--- Testable
-
-instance Show Typerep where {
-  show (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
-};
-
-instance Show Terma 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 ++ ")";  
-};
-
-data Result =
-  Result { args     :: [Term]
-         , showArgs :: [Term -> String]
-         , apply_fun    :: [Term] -> Bool
-         };
-
-data P = P (Int -> Int -> Result);
-
-run :: Testable a => ([Term] -> a) -> Int -> Int -> Result;
-run a = let P f = property a in f;
-
-class Testable a where {
-  property :: ([Term] -> a) -> P;
-};
-
-instance Testable Bool where {
-  property app = P $ \n d -> Result [] [] (app . reverse);
-};
-
-instance (Term_of a, Serial a, Testable b) => Testable (a -> b) where {
-  property f = P $ \n d ->
-    let C t c = series d
-        c' = conv c
-        r = run (\(x:xs) -> f xs (c' x)) (n+1) d
-    in  r { args = Var [n] t : args r, showArgs = (show . term_of . c') : showArgs r };
-};
-
--- Top-level interface
-
-depthCheck :: Testable a => Int -> a -> IO ();
-depthCheck d p =
-  (refute $ run (const p) 0 d) >>= (\n -> putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d);
-
-smallCheck :: Testable a => Int -> a -> IO ();
-smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE");
-
-}
-

--- a/src/HOL/Tools/LSC/lazysmallcheck.ML	Fri Mar 11 15:21:13 2011 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,103 +0,0 @@
-(*  Title:      HOL/Tools/LSC/lazysmallcheck.ML
-    Author:     Lukas Bulwahn, TU Muenchen
-
-Prototypic implementation to invoke lazysmallcheck in Isabelle
-
-*)
-
-signature LAZYSMALLCHECK =
-sig
-  val compile_generator_expr:
-    Proof.context -> term -> int -> term list option * Quickcheck.report option
-  val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
-  val setup: theory -> theory
-end;
-
-structure Lazysmallcheck : LAZYSMALLCHECK =
-struct
-
-(* invocation of Haskell interpreter *)
-
-val lsc_module = File.read (Path.explode "~~/src/HOL/Tools/LSC/LazySmallCheck.hs")
-
-fun exec verbose code =
-  ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
-
-fun value ctxt (get, put, put_ml) (code, value) =
-  let
-    val tmp_prefix = "LSC"
-    fun make_cmd executable files =
-      getenv "EXEC_GHC" ^ " -fglasgow-exts " ^ (space_implode " " (map Path.implode files)) ^
-        " -o " ^ executable ^ " && " ^ executable
-    fun run in_path = 
-      let
-        val code_file = Path.append in_path (Path.basic "Code.hs")
-        val lsc_file = Path.append in_path (Path.basic "LazySmallCheck.hs")
-        val main_file = Path.append in_path (Path.basic "Main.hs")
-        val main = "module Main where {\n\n" ^
-          "import LazySmallCheck;\n" ^
-          "import Code;\n\n" ^
-          "main = LazySmallCheck.smallCheck 7 (Code.value ())\n\n" ^
-          "}\n"
-        val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
-          (unprefix "module Code where {" code)
-        val _ = File.write code_file code'
-        val _ = File.write lsc_file lsc_module
-        val _ = File.write main_file main
-        val executable = Path.implode (Path.append in_path (Path.basic "isa_lsc"))
-        val cmd = make_cmd executable [code_file, lsc_file, main_file]
-      in
-        bash_output cmd
-      end 
-    val result = Isabelle_System.with_tmp_dir tmp_prefix run
-    val output_value = the_default "NONE"
-      (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
-    val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
-      ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
-    val ctxt' = ctxt
-      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
-      |> Context.proof_map (exec false ml_code);
-  in get ctxt' () end;
-
-fun evaluation cookie thy evaluator vs_t args =
-  let
-    val ctxt = ProofContext.init_global thy;
-    val (program_code, value_name) = evaluator vs_t;
-    val value_code = space_implode " "
-      (value_name :: "()" :: map (enclose "(" ")") args);
-  in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
-
-fun dynamic_value_strict cookie thy postproc t args =
-  let
-    fun evaluator naming program ((_, vs_ty), t) deps =
-      evaluation cookie thy (Code_Target.evaluator thy "Haskell" naming program deps) (vs_ty, t) args;
-  in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
-
-(* counterexample generator *)
-  
-structure Lazysmallcheck_Result = Proof_Data
-(
-  type T = unit -> term list option
-  fun init _ () = error "Lazysmallcheck_Result"
-)
-
-val put_counterexample = Lazysmallcheck_Result.put
-  
-fun compile_generator_expr ctxt t size =
-  let
-    val thy = ProofContext.theory_of ctxt
-    fun ensure_testable t =
-      Const (@{const_name LSC.ensure_testable}, fastype_of t --> fastype_of t) $ t
-    val t = dynamic_value_strict
-      (Lazysmallcheck_Result.get, Lazysmallcheck_Result.put, "Lazysmallcheck.put_counterexample")
-      thy (Option.map o map) (ensure_testable t) []
-  in
-    (t, NONE)
-  end;
-
-
-val setup =
-  Context.theory_map
-    (Quickcheck.add_generator ("lazy_exhaustive", compile_generator_expr))
-    
-end;
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Fri Mar 11 15:21:13 2011 +0100
@@ -0,0 +1,110 @@
+module LazySmallCheck where {
+
+import Monad;
+import Control.Exception;
+import System.IO;
+import System.Exit;
+import Code;
+
+type Pos = [Int];
+
+-- Term refinement
+
+new :: Pos -> [[Type]] -> [Term];
+new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
+           | (c, ts) <- zip [0..] ps ];
+
+refine :: Term -> Pos -> [Term];
+refine (Var p (SumOfProd ss)) [] = new p ss;
+refine (Ctr c xs) p = map (Ctr c) (refineList xs p);
+
+refineList :: [Term] -> Pos -> [[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 :: Term -> [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];
+
+-- Answers
+
+answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
+answer a known unknown =
+  try (evaluate a) >>= (\res ->
+     case res of
+       Right b -> known b
+       Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
+       Left e -> throw e);
+
+-- Refute
+
+str_of_list [] = "[]";
+str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
+
+report :: Result -> [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 -> [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;
+refute r = ref r (args r);
+
+sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
+sumMapM f n [] = return n;
+sumMapM f n (a:as) = seq n (do m <- f a ; sumMapM f (n+m) as);
+
+-- Testable
+
+instance Show Typerep where {
+  show (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
+};
+
+instance Show Terma 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 ++ ")";  
+};
+
+data Result =
+  Result { args     :: [Term]
+         , showArgs :: [Term -> String]
+         , apply_fun    :: [Term] -> Bool
+         };
+
+data P = P (Int -> Int -> Result);
+
+run :: Testable a => ([Term] -> a) -> Int -> Int -> Result;
+run a = let P f = property a in f;
+
+class Testable a where {
+  property :: ([Term] -> a) -> P;
+};
+
+instance Testable Bool where {
+  property app = P $ \n d -> Result [] [] (app . reverse);
+};
+
+instance (Term_of a, Serial a, Testable b) => Testable (a -> b) where {
+  property f = P $ \n d ->
+    let C t c = series d
+        c' = conv c
+        r = run (\(x:xs) -> f xs (c' x)) (n+1) d
+    in  r { args = Var [n] t : args r, showArgs = (show . term_of . c') : showArgs r };
+};
+
+-- Top-level interface
+
+depthCheck :: Testable a => Int -> a -> IO ();
+depthCheck d p =
+  (refute $ run (const p) 0 d) >>= (\n -> putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d);
+
+smallCheck :: Testable a => Int -> a -> IO ();
+smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE");
+
+}
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 11 15:21:13 2011 +0100
@@ -0,0 +1,103 @@
+(*  Title:      HOL/Tools/LSC/lazysmallcheck.ML
+    Author:     Lukas Bulwahn, TU Muenchen
+
+Prototypic implementation to invoke lazysmallcheck in Isabelle
+
+*)
+
+signature LAZYSMALLCHECK =
+sig
+  val compile_generator_expr:
+    Proof.context -> term -> int -> term list option * Quickcheck.report option
+  val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
+  val setup: theory -> theory
+end;
+
+structure Lazysmallcheck : LAZYSMALLCHECK =
+struct
+
+(* invocation of Haskell interpreter *)
+
+val lsc_module = File.read (Path.explode "~~/src/HOL/Tools/LSC/LazySmallCheck.hs")
+
+fun exec verbose code =
+  ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
+
+fun value ctxt (get, put, put_ml) (code, value) =
+  let
+    val tmp_prefix = "LSC"
+    fun make_cmd executable files =
+      getenv "EXEC_GHC" ^ " -fglasgow-exts " ^ (space_implode " " (map Path.implode files)) ^
+        " -o " ^ executable ^ " && " ^ executable
+    fun run in_path = 
+      let
+        val code_file = Path.append in_path (Path.basic "Code.hs")
+        val lsc_file = Path.append in_path (Path.basic "LazySmallCheck.hs")
+        val main_file = Path.append in_path (Path.basic "Main.hs")
+        val main = "module Main where {\n\n" ^
+          "import LazySmallCheck;\n" ^
+          "import Code;\n\n" ^
+          "main = LazySmallCheck.smallCheck 7 (Code.value ())\n\n" ^
+          "}\n"
+        val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
+          (unprefix "module Code where {" code)
+        val _ = File.write code_file code'
+        val _ = File.write lsc_file lsc_module
+        val _ = File.write main_file main
+        val executable = Path.implode (Path.append in_path (Path.basic "isa_lsc"))
+        val cmd = make_cmd executable [code_file, lsc_file, main_file]
+      in
+        bash_output cmd
+      end 
+    val result = Isabelle_System.with_tmp_dir tmp_prefix run
+    val output_value = the_default "NONE"
+      (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
+    val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
+      ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
+    val ctxt' = ctxt
+      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
+      |> Context.proof_map (exec false ml_code);
+  in get ctxt' () end;
+
+fun evaluation cookie thy evaluator vs_t args =
+  let
+    val ctxt = ProofContext.init_global thy;
+    val (program_code, value_name) = evaluator vs_t;
+    val value_code = space_implode " "
+      (value_name :: "()" :: map (enclose "(" ")") args);
+  in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
+
+fun dynamic_value_strict cookie thy postproc t args =
+  let
+    fun evaluator naming program ((_, vs_ty), t) deps =
+      evaluation cookie thy (Code_Target.evaluator thy "Haskell" naming program deps) (vs_ty, t) args;
+  in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
+
+(* counterexample generator *)
+  
+structure Lazysmallcheck_Result = Proof_Data
+(
+  type T = unit -> term list option
+  fun init _ () = error "Lazysmallcheck_Result"
+)
+
+val put_counterexample = Lazysmallcheck_Result.put
+  
+fun compile_generator_expr ctxt t size =
+  let
+    val thy = ProofContext.theory_of ctxt
+    fun ensure_testable t =
+      Const (@{const_name LSC.ensure_testable}, fastype_of t --> fastype_of t) $ t
+    val t = dynamic_value_strict
+      (Lazysmallcheck_Result.get, Lazysmallcheck_Result.put, "Lazysmallcheck.put_counterexample")
+      thy (Option.map o map) (ensure_testable t) []
+  in
+    (t, NONE)
+  end;
+
+
+val setup =
+  Context.theory_map
+    (Quickcheck.add_generator ("lazy_exhaustive", compile_generator_expr))
+    
+end;
\ No newline at end of file