moving and renaming lazysmallcheck to narrowing which reflects the characteristical behaviour better
authorbulwahn
Fri Mar 11 15:21:13 2011 +0100 (2011-03-11)
changeset 419254b9fdfd23752
parent 41924 107bf5c959d3
child 41926 b09a67a3dc1e
moving and renaming lazysmallcheck to narrowing which reflects the characteristical behaviour better
src/HOL/Tools/LSC/LazySmallCheck.hs
src/HOL/Tools/LSC/lazysmallcheck.ML
src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Tools/LSC/LazySmallCheck.hs	Fri Mar 11 15:21:13 2011 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,110 +0,0 @@
     1.4 -module LazySmallCheck where {
     1.5 -
     1.6 -import Monad;
     1.7 -import Control.Exception;
     1.8 -import System.IO;
     1.9 -import System.Exit;
    1.10 -import Code;
    1.11 -
    1.12 -type Pos = [Int];
    1.13 -
    1.14 --- Term refinement
    1.15 -
    1.16 -new :: Pos -> [[Type]] -> [Term];
    1.17 -new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
    1.18 -           | (c, ts) <- zip [0..] ps ];
    1.19 -
    1.20 -refine :: Term -> Pos -> [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 -
    1.24 -refineList :: [Term] -> Pos -> [[Term]];
    1.25 -refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
    1.26 -
    1.27 --- Find total instantiations of a partial value
    1.28 -
    1.29 -total :: Term -> [Term];
    1.30 -total (Ctr c xs) = [Ctr c ys | ys <- mapM total xs];
    1.31 -total (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- total x];
    1.32 -
    1.33 --- Answers
    1.34 -
    1.35 -answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
    1.36 -answer a known unknown =
    1.37 -  try (evaluate a) >>= (\res ->
    1.38 -     case res of
    1.39 -       Right b -> known b
    1.40 -       Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
    1.41 -       Left e -> throw e);
    1.42 -
    1.43 --- Refute
    1.44 -
    1.45 -str_of_list [] = "[]";
    1.46 -str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
    1.47 -
    1.48 -report :: Result -> [Term] -> IO Int;
    1.49 -report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) $ head [ys | ys <- mapM total xs]) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
    1.50 -
    1.51 -eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
    1.52 -eval p k u = answer p (\p -> answer p k u) u;
    1.53 -
    1.54 -ref :: Result -> [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 -refute r = ref r (args r);
    1.59 -
    1.60 -sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
    1.61 -sumMapM f n [] = return n;
    1.62 -sumMapM f n (a:as) = seq n (do m <- f a ; sumMapM f (n+m) as);
    1.63 -
    1.64 --- Testable
    1.65 -
    1.66 -instance Show Typerep where {
    1.67 -  show (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
    1.68 -};
    1.69 -
    1.70 -instance Show Terma where {
    1.71 -  show (Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
    1.72 -  show (App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
    1.73 -  show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";  
    1.74 -};
    1.75 -
    1.76 -data Result =
    1.77 -  Result { args     :: [Term]
    1.78 -         , showArgs :: [Term -> String]
    1.79 -         , apply_fun    :: [Term] -> Bool
    1.80 -         };
    1.81 -
    1.82 -data P = P (Int -> Int -> Result);
    1.83 -
    1.84 -run :: Testable a => ([Term] -> a) -> Int -> Int -> Result;
    1.85 -run a = let P f = property a in f;
    1.86 -
    1.87 -class Testable a where {
    1.88 -  property :: ([Term] -> a) -> P;
    1.89 -};
    1.90 -
    1.91 -instance Testable Bool where {
    1.92 -  property app = P $ \n d -> Result [] [] (app . reverse);
    1.93 -};
    1.94 -
    1.95 -instance (Term_of a, Serial a, Testable b) => Testable (a -> b) where {
    1.96 -  property f = P $ \n d ->
    1.97 -    let C t c = series d
    1.98 -        c' = conv c
    1.99 -        r = run (\(x:xs) -> f xs (c' x)) (n+1) d
   1.100 -    in  r { args = Var [n] t : args r, showArgs = (show . term_of . c') : showArgs r };
   1.101 -};
   1.102 -
   1.103 --- Top-level interface
   1.104 -
   1.105 -depthCheck :: Testable a => Int -> a -> IO ();
   1.106 -depthCheck d p =
   1.107 -  (refute $ run (const p) 0 d) >>= (\n -> putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d);
   1.108 -
   1.109 -smallCheck :: Testable a => Int -> a -> IO ();
   1.110 -smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE");
   1.111 -
   1.112 -}
   1.113 -
     2.1 --- a/src/HOL/Tools/LSC/lazysmallcheck.ML	Fri Mar 11 15:21:13 2011 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,103 +0,0 @@
     2.4 -(*  Title:      HOL/Tools/LSC/lazysmallcheck.ML
     2.5 -    Author:     Lukas Bulwahn, TU Muenchen
     2.6 -
     2.7 -Prototypic implementation to invoke lazysmallcheck in Isabelle
     2.8 -
     2.9 -*)
    2.10 -
    2.11 -signature LAZYSMALLCHECK =
    2.12 -sig
    2.13 -  val compile_generator_expr:
    2.14 -    Proof.context -> term -> int -> term list option * Quickcheck.report option
    2.15 -  val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
    2.16 -  val setup: theory -> theory
    2.17 -end;
    2.18 -
    2.19 -structure Lazysmallcheck : LAZYSMALLCHECK =
    2.20 -struct
    2.21 -
    2.22 -(* invocation of Haskell interpreter *)
    2.23 -
    2.24 -val lsc_module = File.read (Path.explode "~~/src/HOL/Tools/LSC/LazySmallCheck.hs")
    2.25 -
    2.26 -fun exec verbose code =
    2.27 -  ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
    2.28 -
    2.29 -fun value ctxt (get, put, put_ml) (code, value) =
    2.30 -  let
    2.31 -    val tmp_prefix = "LSC"
    2.32 -    fun make_cmd executable files =
    2.33 -      getenv "EXEC_GHC" ^ " -fglasgow-exts " ^ (space_implode " " (map Path.implode files)) ^
    2.34 -        " -o " ^ executable ^ " && " ^ executable
    2.35 -    fun run in_path = 
    2.36 -      let
    2.37 -        val code_file = Path.append in_path (Path.basic "Code.hs")
    2.38 -        val lsc_file = Path.append in_path (Path.basic "LazySmallCheck.hs")
    2.39 -        val main_file = Path.append in_path (Path.basic "Main.hs")
    2.40 -        val main = "module Main where {\n\n" ^
    2.41 -          "import LazySmallCheck;\n" ^
    2.42 -          "import Code;\n\n" ^
    2.43 -          "main = LazySmallCheck.smallCheck 7 (Code.value ())\n\n" ^
    2.44 -          "}\n"
    2.45 -        val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    2.46 -          (unprefix "module Code where {" code)
    2.47 -        val _ = File.write code_file code'
    2.48 -        val _ = File.write lsc_file lsc_module
    2.49 -        val _ = File.write main_file main
    2.50 -        val executable = Path.implode (Path.append in_path (Path.basic "isa_lsc"))
    2.51 -        val cmd = make_cmd executable [code_file, lsc_file, main_file]
    2.52 -      in
    2.53 -        bash_output cmd
    2.54 -      end 
    2.55 -    val result = Isabelle_System.with_tmp_dir tmp_prefix run
    2.56 -    val output_value = the_default "NONE"
    2.57 -      (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
    2.58 -    val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
    2.59 -      ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
    2.60 -    val ctxt' = ctxt
    2.61 -      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    2.62 -      |> Context.proof_map (exec false ml_code);
    2.63 -  in get ctxt' () end;
    2.64 -
    2.65 -fun evaluation cookie thy evaluator vs_t args =
    2.66 -  let
    2.67 -    val ctxt = ProofContext.init_global thy;
    2.68 -    val (program_code, value_name) = evaluator vs_t;
    2.69 -    val value_code = space_implode " "
    2.70 -      (value_name :: "()" :: map (enclose "(" ")") args);
    2.71 -  in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
    2.72 -
    2.73 -fun dynamic_value_strict cookie thy postproc t args =
    2.74 -  let
    2.75 -    fun evaluator naming program ((_, vs_ty), t) deps =
    2.76 -      evaluation cookie thy (Code_Target.evaluator thy "Haskell" naming program deps) (vs_ty, t) args;
    2.77 -  in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
    2.78 -
    2.79 -(* counterexample generator *)
    2.80 -  
    2.81 -structure Lazysmallcheck_Result = Proof_Data
    2.82 -(
    2.83 -  type T = unit -> term list option
    2.84 -  fun init _ () = error "Lazysmallcheck_Result"
    2.85 -)
    2.86 -
    2.87 -val put_counterexample = Lazysmallcheck_Result.put
    2.88 -  
    2.89 -fun compile_generator_expr ctxt t size =
    2.90 -  let
    2.91 -    val thy = ProofContext.theory_of ctxt
    2.92 -    fun ensure_testable t =
    2.93 -      Const (@{const_name LSC.ensure_testable}, fastype_of t --> fastype_of t) $ t
    2.94 -    val t = dynamic_value_strict
    2.95 -      (Lazysmallcheck_Result.get, Lazysmallcheck_Result.put, "Lazysmallcheck.put_counterexample")
    2.96 -      thy (Option.map o map) (ensure_testable t) []
    2.97 -  in
    2.98 -    (t, NONE)
    2.99 -  end;
   2.100 -
   2.101 -
   2.102 -val setup =
   2.103 -  Context.theory_map
   2.104 -    (Quickcheck.add_generator ("lazy_exhaustive", compile_generator_expr))
   2.105 -    
   2.106 -end;
   2.107 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Fri Mar 11 15:21:13 2011 +0100
     3.3 @@ -0,0 +1,110 @@
     3.4 +module LazySmallCheck where {
     3.5 +
     3.6 +import Monad;
     3.7 +import Control.Exception;
     3.8 +import System.IO;
     3.9 +import System.Exit;
    3.10 +import Code;
    3.11 +
    3.12 +type Pos = [Int];
    3.13 +
    3.14 +-- Term refinement
    3.15 +
    3.16 +new :: Pos -> [[Type]] -> [Term];
    3.17 +new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
    3.18 +           | (c, ts) <- zip [0..] ps ];
    3.19 +
    3.20 +refine :: Term -> Pos -> [Term];
    3.21 +refine (Var p (SumOfProd ss)) [] = new p ss;
    3.22 +refine (Ctr c xs) p = map (Ctr c) (refineList xs p);
    3.23 +
    3.24 +refineList :: [Term] -> Pos -> [[Term]];
    3.25 +refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
    3.26 +
    3.27 +-- Find total instantiations of a partial value
    3.28 +
    3.29 +total :: Term -> [Term];
    3.30 +total (Ctr c xs) = [Ctr c ys | ys <- mapM total xs];
    3.31 +total (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- total x];
    3.32 +
    3.33 +-- Answers
    3.34 +
    3.35 +answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
    3.36 +answer a known unknown =
    3.37 +  try (evaluate a) >>= (\res ->
    3.38 +     case res of
    3.39 +       Right b -> known b
    3.40 +       Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
    3.41 +       Left e -> throw e);
    3.42 +
    3.43 +-- Refute
    3.44 +
    3.45 +str_of_list [] = "[]";
    3.46 +str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
    3.47 +
    3.48 +report :: Result -> [Term] -> IO Int;
    3.49 +report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) $ head [ys | ys <- mapM total xs]) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
    3.50 +
    3.51 +eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
    3.52 +eval p k u = answer p (\p -> answer p k u) u;
    3.53 +
    3.54 +ref :: Result -> [Term] -> IO Int;
    3.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));
    3.56 +          
    3.57 +refute :: Result -> IO Int;
    3.58 +refute r = ref r (args r);
    3.59 +
    3.60 +sumMapM :: (a -> IO Int) -> Int -> [a] -> IO Int;
    3.61 +sumMapM f n [] = return n;
    3.62 +sumMapM f n (a:as) = seq n (do m <- f a ; sumMapM f (n+m) as);
    3.63 +
    3.64 +-- Testable
    3.65 +
    3.66 +instance Show Typerep where {
    3.67 +  show (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
    3.68 +};
    3.69 +
    3.70 +instance Show Terma where {
    3.71 +  show (Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
    3.72 +  show (App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
    3.73 +  show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";  
    3.74 +};
    3.75 +
    3.76 +data Result =
    3.77 +  Result { args     :: [Term]
    3.78 +         , showArgs :: [Term -> String]
    3.79 +         , apply_fun    :: [Term] -> Bool
    3.80 +         };
    3.81 +
    3.82 +data P = P (Int -> Int -> Result);
    3.83 +
    3.84 +run :: Testable a => ([Term] -> a) -> Int -> Int -> Result;
    3.85 +run a = let P f = property a in f;
    3.86 +
    3.87 +class Testable a where {
    3.88 +  property :: ([Term] -> a) -> P;
    3.89 +};
    3.90 +
    3.91 +instance Testable Bool where {
    3.92 +  property app = P $ \n d -> Result [] [] (app . reverse);
    3.93 +};
    3.94 +
    3.95 +instance (Term_of a, Serial a, Testable b) => Testable (a -> b) where {
    3.96 +  property f = P $ \n d ->
    3.97 +    let C t c = series d
    3.98 +        c' = conv c
    3.99 +        r = run (\(x:xs) -> f xs (c' x)) (n+1) d
   3.100 +    in  r { args = Var [n] t : args r, showArgs = (show . term_of . c') : showArgs r };
   3.101 +};
   3.102 +
   3.103 +-- Top-level interface
   3.104 +
   3.105 +depthCheck :: Testable a => Int -> a -> IO ();
   3.106 +depthCheck d p =
   3.107 +  (refute $ run (const p) 0 d) >>= (\n -> putStrLn $ "OK, required " ++ show n ++ " tests at depth " ++ show d);
   3.108 +
   3.109 +smallCheck :: Testable a => Int -> a -> IO ();
   3.110 +smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE");
   3.111 +
   3.112 +}
   3.113 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 11 15:21:13 2011 +0100
     4.3 @@ -0,0 +1,103 @@
     4.4 +(*  Title:      HOL/Tools/LSC/lazysmallcheck.ML
     4.5 +    Author:     Lukas Bulwahn, TU Muenchen
     4.6 +
     4.7 +Prototypic implementation to invoke lazysmallcheck in Isabelle
     4.8 +
     4.9 +*)
    4.10 +
    4.11 +signature LAZYSMALLCHECK =
    4.12 +sig
    4.13 +  val compile_generator_expr:
    4.14 +    Proof.context -> term -> int -> term list option * Quickcheck.report option
    4.15 +  val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
    4.16 +  val setup: theory -> theory
    4.17 +end;
    4.18 +
    4.19 +structure Lazysmallcheck : LAZYSMALLCHECK =
    4.20 +struct
    4.21 +
    4.22 +(* invocation of Haskell interpreter *)
    4.23 +
    4.24 +val lsc_module = File.read (Path.explode "~~/src/HOL/Tools/LSC/LazySmallCheck.hs")
    4.25 +
    4.26 +fun exec verbose code =
    4.27 +  ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
    4.28 +
    4.29 +fun value ctxt (get, put, put_ml) (code, value) =
    4.30 +  let
    4.31 +    val tmp_prefix = "LSC"
    4.32 +    fun make_cmd executable files =
    4.33 +      getenv "EXEC_GHC" ^ " -fglasgow-exts " ^ (space_implode " " (map Path.implode files)) ^
    4.34 +        " -o " ^ executable ^ " && " ^ executable
    4.35 +    fun run in_path = 
    4.36 +      let
    4.37 +        val code_file = Path.append in_path (Path.basic "Code.hs")
    4.38 +        val lsc_file = Path.append in_path (Path.basic "LazySmallCheck.hs")
    4.39 +        val main_file = Path.append in_path (Path.basic "Main.hs")
    4.40 +        val main = "module Main where {\n\n" ^
    4.41 +          "import LazySmallCheck;\n" ^
    4.42 +          "import Code;\n\n" ^
    4.43 +          "main = LazySmallCheck.smallCheck 7 (Code.value ())\n\n" ^
    4.44 +          "}\n"
    4.45 +        val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    4.46 +          (unprefix "module Code where {" code)
    4.47 +        val _ = File.write code_file code'
    4.48 +        val _ = File.write lsc_file lsc_module
    4.49 +        val _ = File.write main_file main
    4.50 +        val executable = Path.implode (Path.append in_path (Path.basic "isa_lsc"))
    4.51 +        val cmd = make_cmd executable [code_file, lsc_file, main_file]
    4.52 +      in
    4.53 +        bash_output cmd
    4.54 +      end 
    4.55 +    val result = Isabelle_System.with_tmp_dir tmp_prefix run
    4.56 +    val output_value = the_default "NONE"
    4.57 +      (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
    4.58 +    val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
    4.59 +      ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
    4.60 +    val ctxt' = ctxt
    4.61 +      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
    4.62 +      |> Context.proof_map (exec false ml_code);
    4.63 +  in get ctxt' () end;
    4.64 +
    4.65 +fun evaluation cookie thy evaluator vs_t args =
    4.66 +  let
    4.67 +    val ctxt = ProofContext.init_global thy;
    4.68 +    val (program_code, value_name) = evaluator vs_t;
    4.69 +    val value_code = space_implode " "
    4.70 +      (value_name :: "()" :: map (enclose "(" ")") args);
    4.71 +  in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
    4.72 +
    4.73 +fun dynamic_value_strict cookie thy postproc t args =
    4.74 +  let
    4.75 +    fun evaluator naming program ((_, vs_ty), t) deps =
    4.76 +      evaluation cookie thy (Code_Target.evaluator thy "Haskell" naming program deps) (vs_ty, t) args;
    4.77 +  in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
    4.78 +
    4.79 +(* counterexample generator *)
    4.80 +  
    4.81 +structure Lazysmallcheck_Result = Proof_Data
    4.82 +(
    4.83 +  type T = unit -> term list option
    4.84 +  fun init _ () = error "Lazysmallcheck_Result"
    4.85 +)
    4.86 +
    4.87 +val put_counterexample = Lazysmallcheck_Result.put
    4.88 +  
    4.89 +fun compile_generator_expr ctxt t size =
    4.90 +  let
    4.91 +    val thy = ProofContext.theory_of ctxt
    4.92 +    fun ensure_testable t =
    4.93 +      Const (@{const_name LSC.ensure_testable}, fastype_of t --> fastype_of t) $ t
    4.94 +    val t = dynamic_value_strict
    4.95 +      (Lazysmallcheck_Result.get, Lazysmallcheck_Result.put, "Lazysmallcheck.put_counterexample")
    4.96 +      thy (Option.map o map) (ensure_testable t) []
    4.97 +  in
    4.98 +    (t, NONE)
    4.99 +  end;
   4.100 +
   4.101 +
   4.102 +val setup =
   4.103 +  Context.theory_map
   4.104 +    (Quickcheck.add_generator ("lazy_exhaustive", compile_generator_expr))
   4.105 +    
   4.106 +end;
   4.107 \ No newline at end of file