# HG changeset patch
# User bulwahn
# Date 1299836257 -3600
# Node ID 3bd9a21366d2ee547057c8a5e41fc5dd3a141f0c
# Parent  b04e16854c08105f8b8178d8926101946ae9dd09
changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent

diff -r b04e16854c08 -r 3bd9a21366d2 src/HOL/Library/LSC.thy
--- a/src/HOL/Library/LSC.thy	Fri Mar 11 10:37:37 2011 +0100
+++ b/src/HOL/Library/LSC.thy	Fri Mar 11 10:37:37 2011 +0100
@@ -9,39 +9,99 @@
 
 subsection {* Counterexample generator *}
 
+subsubsection {* Type code_int for Haskell's Int type *}
+
+typedef (open) code_int = "UNIV \<Colon> int set"
+  morphisms int_of of_int by rule
+
+lemma int_of_inject [simp]:
+  "int_of k = int_of l \<longleftrightarrow> k = l"
+  by (rule int_of_inject)
+
+
+instantiation code_int :: "{zero, one, minus, linorder}"
+begin
+
+definition [simp, code del]:
+  "0 = of_int 0"
+
+definition [simp, code del]:
+  "1 = of_int 1"
+
+definition [simp, code del]:
+  "n - m = of_int (int_of n - int_of m)"
+
+definition [simp, code del]:
+  "n \<le> m \<longleftrightarrow> int_of n \<le> int_of m"
+
+definition [simp, code del]:
+  "n < m \<longleftrightarrow> int_of n < int_of m"
+
+
+instance proof qed (auto)
+
+end
+(*
+lemma zero_code_int_code [code, code_unfold]:
+  "(0\<Colon>code_int) = Numeral0"
+  by (simp add: number_of_code_numeral_def Pls_def)
+lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
+  using zero_code_numeral_code ..
+
+lemma one_code_numeral_code [code, code_unfold]:
+  "(1\<Colon>code_int) = Numeral1"
+  by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
+lemma [code_post]: "Numeral1 = (1\<Colon>code_int)"
+  using one_code_numeral_code ..
+*)
+
+code_const "0 \<Colon> code_int"
+  (Haskell "0")
+
+code_const "1 \<Colon> code_int"
+  (Haskell "1")
+
+code_const "minus \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> code_int"
+  (Haskell "(_/ -/ _)")
+
+code_const "op \<le> \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
+  (Haskell infix 4 "<=")
+
+code_const "op < \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
+  (Haskell infix 4 "<")
+
+code_type code_int
+  (Haskell "Int")
+
 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 "term" = Var "code_int list" type | Ctr code_int "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)"
+consts nth :: "'a list => code_int => 'a"
 
-lemma [code]:
-  "nth (x # xs) i = (if i = 0 then x else nth xs (i - 1))"
-unfolding nth_def by (cases i) simp
+code_const nth ("Haskell" infixl 9  "!!")
 
-definition error :: "char list => 'a"
-where
-  "error = undefined"
+consts error :: "char list => 'a"
 
 code_const error ("Haskell" "error")
 
-definition toEnum' :: "code_numeral => char"
-where
-  "toEnum' = undefined"
+consts toEnum :: "code_int => char"
+
+code_const toEnum ("Haskell" "toEnum")
 
-code_const toEnum' ("Haskell" "(toEnum . fromInteger)")
+consts map_index :: "(code_int * 'a => 'b) => 'a list => 'b list"  
 
+consts split_At :: "code_int => 'a list => 'a list * 'a list"
+ 
 subsubsection {* LSC's basic operations *}
 
-type_synonym 'a series = "code_numeral => 'a cons"
+type_synonym 'a series = "code_int => 'a cons"
 
 definition empty :: "'a series"
 where
@@ -53,7 +113,7 @@
 
 fun conv :: "(term list => 'a) list => term => 'a"
 where
-  "conv cs (Var p _) = error (Char Nibble0 Nibble0 # map toEnum' p)"
+  "conv cs (Var p _) = error (Char Nibble0 Nibble0 # map toEnum p)"
 | "conv cs (Ctr i xs) = (nth cs i) xs"
 
 fun nonEmpty :: "type => bool"
@@ -81,11 +141,34 @@
 where
   "cons0 f = cons f"
 
+type_synonym pos = "code_int list"
+
+subsubsection {* Term refinement *}
+
+definition new :: "pos => type list list => term list"
+where
+  "new p ps = map_index (%(c, ts). Ctr c (map_index (%(i, t). Var (p @ [i]) t) ts)) ps"
+
+fun refine :: "term => pos => term list" and refineList :: "term list => pos => (term list) list"
+where
+  "refine (Var p (SumOfProd ss)) [] = new p ss"
+| "refine (Ctr c xs) p = map (Ctr c) (refineList xs p)"
+| "refineList xs (i # is) = (let (ls, xrs) = split_At i xs in (case xrs of x#rs => [ls @ y # rs. y <- refine x is]))"
+
+text {* Find total instantiations of a partial value *}
+
+function total :: "term => term list"
+where
+  "total (Ctr c xs) = [Ctr c ys. ys <- map total xs]"
+| "total (Var p (SumOfProd ss)) = [y. x <- new p ss, y <- total x]"
+by pat_completeness auto
+
+termination sorry
 
 subsubsection {* LSC's type class for enumeration *}
 
 class serial =
-  fixes series :: "code_numeral => 'a cons"
+  fixes series :: "code_int => 'a cons"
 
 definition cons1 :: "('a::serial => 'b) => 'b series"
 where
@@ -212,8 +295,10 @@
 
 subsubsection {* Setting up the counterexample generator *}
   
-use "Tools/LSC/lazysmallcheck.ML"
+use "~~/src/HOL/Tools/LSC/lazysmallcheck.ML"
 
 setup {* Lazysmallcheck.setup *}
 
+hide_const (open) empty
+
 end
\ No newline at end of file
diff -r b04e16854c08 -r 3bd9a21366d2 src/HOL/Tools/LSC/LazySmallCheck.hs
--- a/src/HOL/Tools/LSC/LazySmallCheck.hs	Fri Mar 11 10:37:37 2011 +0100
+++ b/src/HOL/Tools/LSC/LazySmallCheck.hs	Fri Mar 11 10:37:37 2011 +0100
@@ -6,7 +6,7 @@
 import System.Exit;
 import Code;
 
-type Pos = [Integer];
+type Pos = [Int];
 
 -- Term refinement
 
@@ -19,7 +19,7 @@
 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];
+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
 
@@ -34,7 +34,7 @@
   try (evaluate a) >>= (\res ->
      case res of
        Right b -> known b
-       Left (ErrorCall ('\0':p)) -> unknown (map (toInteger . fromEnum) p)
+       Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
        Left e -> throw e);
 
 -- Refute
@@ -42,26 +42,26 @@
 str_of_list [] = "[]";
 str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
 
-report :: Result -> [Term] -> IO Integer;
+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 Integer;
+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 Integer;
+refute :: Result -> IO Int;
 refute r = ref r (args r);
 
-sumMapM :: (a -> IO Integer) -> Integer -> [a] -> IO Integer;
+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 (Typerepa c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
+  show (Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
 };
 
 instance Show Terma where {
@@ -76,9 +76,9 @@
          , apply_fun    :: [Term] -> Bool
          };
 
-data P = P (Integer -> Integer -> Result);
+data P = P (Int -> Int -> Result);
 
-run :: Testable a => ([Term] -> a) -> Integer -> Integer -> Result;
+run :: Testable a => ([Term] -> a) -> Int -> Int -> Result;
 run a = let P f = property a in f;
 
 class Testable a where {
@@ -99,11 +99,11 @@
 
 -- Top-level interface
 
-depthCheck :: Testable a => Integer -> a -> IO ();
+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 => Integer -> a -> IO ();
+smallCheck :: Testable a => Int -> a -> IO ();
 smallCheck d p = mapM_ (`depthCheck` p) [0..d] >> putStrLn ("NONE");
 
 }
diff -r b04e16854c08 -r 3bd9a21366d2 src/HOL/Tools/LSC/lazysmallcheck.ML
--- a/src/HOL/Tools/LSC/lazysmallcheck.ML	Fri Mar 11 10:37:37 2011 +0100
+++ b/src/HOL/Tools/LSC/lazysmallcheck.ML	Fri Mar 11 10:37:37 2011 +0100
@@ -26,7 +26,9 @@
 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 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")
@@ -35,17 +37,17 @@
         val main = "module Main where {\n\n" ^
           "import LazySmallCheck;\n" ^
           "import Code;\n\n" ^
-          "main = LazySmallCheck.smallCheck 10 (Code.value ())\n\n" ^
+          "main = LazySmallCheck.smallCheck 7 (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]
+        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 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
@@ -53,7 +55,6 @@
     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 =
@@ -88,7 +89,6 @@
     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;