# HG changeset patch
# User bulwahn
# Date 1299836255 -3600
# Node ID e2611bc96022441bb4ab5db36f51f08852475998
# Parent  2ae19825f7b6676121aba4db3529c1dea7a678f4
adding files for prototype of lazysmallcheck

diff -r 2ae19825f7b6 -r e2611bc96022 src/HOL/Library/LSC.thy
--- /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
diff -r 2ae19825f7b6 -r e2611bc96022 src/HOL/Tools/LSC/LazySmallCheck.hs
--- /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");
+
+}
+
diff -r 2ae19825f7b6 -r e2611bc96022 src/HOL/Tools/LSC/lazysmallcheck.ML
--- /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