--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/LSC.thy Fri Mar 11 10:37:35 2011 +0100
@@ -0,0 +1,219 @@
+(* Author: Lukas Bulwahn, TU Muenchen *)
+
+header {* Counterexample generator based on LazySmallCheck *}
+
+theory LSC
+imports Main "~~/src/HOL/Library/Code_Char"
+uses ("~~/src/HOL/Tools/LSC/lazysmallcheck.ML")
+begin
+
+subsection {* Counterexample generator *}
+
+subsubsection {* LSC's deep representation of types of terms *}
+
+datatype type = SumOfProd "type list list"
+
+datatype "term" = Var "code_numeral list" type | Ctr code_numeral "term list"
+
+datatype 'a cons = C type "(term list => 'a) list"
+
+subsubsection {* auxilary functions for LSC *}
+
+definition nth :: "'a list => code_numeral => 'a"
+where
+ "nth xs i = List.nth xs (Code_Numeral.nat_of i)"
+
+lemma [code]:
+ "nth (x # xs) i = (if i = 0 then x else nth xs (i - 1))"
+unfolding nth_def by (cases i) simp
+
+definition error :: "char list => 'a"
+where
+ "error = undefined"
+
+code_const error ("Haskell" "error")
+
+definition toEnum' :: "code_numeral => char"
+where
+ "toEnum' = undefined"
+
+code_const toEnum' ("Haskell" "(toEnum . fromInteger)")
+
+subsubsection {* LSC's basic operations *}
+
+type_synonym 'a series = "code_numeral => 'a cons"
+
+definition empty :: "'a series"
+where
+ "empty d = C (SumOfProd []) []"
+
+definition cons :: "'a => 'a series"
+where
+ "cons a d = (C (SumOfProd [[]]) [(%_. a)])"
+
+fun conv :: "(term list => 'a) list => term => 'a"
+where
+ "conv cs (Var p _) = error (Char Nibble0 Nibble0 # map toEnum' p)"
+| "conv cs (Ctr i xs) = (nth cs i) xs"
+
+fun nonEmpty :: "type => bool"
+where
+ "nonEmpty (SumOfProd ps) = (\<not> (List.null ps))"
+
+definition "apply" :: "('a => 'b) series => 'a series => 'b series"
+where
+ "apply f a d =
+ (case f d of C (SumOfProd ps) cfs =>
+ case a (d - 1) of C ta cas =>
+ let
+ shallow = (d > 0 \<and> nonEmpty ta);
+ cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
+ in C (SumOfProd [ta # p. shallow, p <- ps]) cs)"
+
+definition sum :: "'a series => 'a series => 'a series"
+where
+ "sum a b d =
+ (case a d of C (SumOfProd ssa) ca =>
+ case b d of C (SumOfProd ssb) cb =>
+ C (SumOfProd (ssa @ ssb)) (ca @ cb))"
+
+definition cons0 :: "'a => 'a series"
+where
+ "cons0 f = cons f"
+
+
+subsubsection {* LSC's type class for enumeration *}
+
+class serial =
+ fixes series :: "code_numeral => 'a cons"
+
+definition cons1 :: "('a::serial => 'b) => 'b series"
+where
+ "cons1 f = apply (cons f) series"
+
+definition cons2 :: "('a :: serial => 'b :: serial => 'c) => 'c series"
+where
+ "cons2 f = apply (apply (cons f) series) series"
+
+instantiation unit :: serial
+begin
+
+definition
+ "series = cons0 ()"
+
+instance ..
+
+end
+
+instantiation bool :: serial
+begin
+
+definition
+ "series = sum (cons0 True) (cons0 False)"
+
+instance ..
+
+end
+
+instantiation option :: (serial) serial
+begin
+
+definition
+ "series = sum (cons0 None) (cons1 Some)"
+
+instance ..
+
+end
+
+instantiation sum :: (serial, serial) serial
+begin
+
+definition
+ "series = sum (cons1 Inl) (cons1 Inr)"
+
+instance ..
+
+end
+
+instantiation list :: (serial) serial
+begin
+
+function series_list :: "'a list series"
+where
+ "series_list d = sum (cons []) (apply (apply (cons Cons) series) series_list) d"
+by pat_completeness auto
+
+termination sorry
+
+instance ..
+
+end
+
+instantiation nat :: serial
+begin
+
+function series_nat :: "nat series"
+where
+ "series_nat d = sum (cons 0) (apply (cons Suc) series_nat) d"
+by pat_completeness auto
+
+termination sorry
+
+instance ..
+
+end
+
+instantiation Enum.finite_1 :: serial
+begin
+
+definition series_finite_1 :: "Enum.finite_1 series"
+where
+ "series_finite_1 = cons (Enum.finite_1.a\<^isub>1 :: Enum.finite_1)"
+
+instance ..
+
+end
+
+instantiation Enum.finite_2 :: serial
+begin
+
+definition series_finite_2 :: "Enum.finite_2 series"
+where
+ "series_finite_2 = sum (cons (Enum.finite_2.a\<^isub>1 :: Enum.finite_2)) (cons (Enum.finite_2.a\<^isub>2 :: Enum.finite_2))"
+
+instance ..
+
+end
+
+instantiation Enum.finite_3 :: serial
+begin
+
+definition series_finite_3 :: "Enum.finite_3 series"
+where
+ "series_finite_3 = sum (cons (Enum.finite_3.a\<^isub>1 :: Enum.finite_3)) (sum (cons (Enum.finite_3.a\<^isub>2 :: Enum.finite_3)) (cons (Enum.finite_3.a\<^isub>3 :: Enum.finite_3)))"
+
+instance ..
+
+end
+
+subsubsection {* class is_testable *}
+
+text {* The class is_testable ensures that all necessary type instances are generated. *}
+
+class is_testable
+
+instance bool :: is_testable ..
+
+instance "fun" :: ("{term_of, serial}", is_testable) is_testable ..
+
+definition ensure_testable :: "'a :: is_testable => 'a :: is_testable"
+where
+ "ensure_testable f = f"
+
+subsubsection {* Setting up the counterexample generator *}
+
+use "Tools/LSC/lazysmallcheck.ML"
+
+setup {* Lazysmallcheck.setup *}
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/LSC/LazySmallCheck.hs Fri Mar 11 10:37:35 2011 +0100
@@ -0,0 +1,110 @@
+module LazySmallCheck where {
+
+import Monad;
+import Control.Exception;
+import System.IO;
+import System.Exit;
+import Code;
+
+type Pos = [Integer];
+
+-- 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 (fromInteger 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 (toInteger . fromEnum) p)
+ Left e -> throw e);
+
+-- Refute
+
+str_of_list [] = "[]";
+str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
+
+report :: Result -> [Term] -> IO Integer;
+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 Integer;
+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 Integer;
+refute r = ref r (args r);
+
+sumMapM :: (a -> IO Integer) -> Integer -> [a] -> IO Integer;
+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 (Typerepa 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 (Integer -> Integer -> Result);
+
+run :: Testable a => ([Term] -> a) -> Integer -> Integer -> 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 => Integer -> 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 => Integer -> 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/LSC/lazysmallcheck.ML Fri Mar 11 10:37:35 2011 +0100
@@ -0,0 +1,101 @@
+(* 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 prefix = "LSC"
+ fun make_cmd files = getenv "EXEC_GHC" ^ " -fglasgow-exts -e \"Main.main\" " ^ (space_implode " " (map Path.implode files))
+ 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 10 (Code.value ())\n\n" ^
+ "}\n"
+ val _ = File.write code_file code
+ val _ = File.write lsc_file lsc_module
+ val _ = File.write main_file main
+ val cmd = make_cmd [code_file, lsc_file, main_file]
+ in
+ bash_output cmd
+ end
+ val result = Isabelle_System.with_tmp_dir prefix run
+ val _ = tracing (fst result)
+ 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);
+ val _ = tracing "after exec"
+ 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) []
+ val _ = tracing "end of compile generator..."
+ in
+ (t, NONE)
+ end;
+
+
+val setup =
+ Context.theory_map
+ (Quickcheck.add_generator ("lazy_exhaustive", compile_generator_expr))
+
+end;
\ No newline at end of file