# HG changeset patch
# User bulwahn
# Date 1306770934 -7200
# Node ID 4022892a2f283eb14fc3c7aa2fa453f724cb223c
# Parent  e2631aaf1e1e5ba3fefa446feb8f23b5a2f7c401
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms

diff -r e2631aaf1e1e -r 4022892a2f28 src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon May 30 16:15:37 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon May 30 17:55:34 2011 +0200
@@ -43,7 +43,7 @@
 str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
 
 report :: Result -> [Narrowing_term] -> IO Int;
-report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) $ head [ys | ys <- mapM total xs]) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
+report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) 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;
@@ -67,7 +67,8 @@
 instance Show Term 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 ++ ")";  
+  show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
+  show (Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
 };
 
 data Result =
@@ -89,12 +90,12 @@
   property app = P $ \n d -> Result [] [] (app . reverse);
 };
 
-instance (Term_of a, Narrowing a, Testable b) => Testable (a -> b) where {
+instance (Partial_term_of a, Narrowing a, Testable b) => Testable (a -> b) where {
   property f = P $ \n d ->
     let C t c = narrowing 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 };
+    in  r { args = Var [n] t : args r, showArgs = (show . partial_term_of (Type :: Itself a)) : showArgs r };
 };
 
 -- Top-level interface
diff -r e2631aaf1e1e -r 4022892a2f28 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 30 16:15:37 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 30 17:55:34 2011 +0200
@@ -10,6 +10,7 @@
     Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
   val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
   val finite_functions : bool Config.T
+  val overlord : bool Config.T
   val setup: theory -> theory
 end;
 
@@ -63,7 +64,7 @@
   let
     val frees = map Free (Name.names Name.context "a" (map (K @{typ narrowing_term}) tys))
     val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i
-      $ (HOLogic.mk_list @{typ narrowing_term} frees)
+      $ (HOLogic.mk_list @{typ narrowing_term} (rev frees))
     val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
         (map mk_partial_term_of (frees ~~ tys))
         (@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty))
@@ -86,7 +87,14 @@
     val cs = (map o apsnd o apsnd o map o map_atyps)
       (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
     val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco);
-    val eqs = map_index (mk_partial_term_of_eq thy ty) cs;
+    val var_insts = map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
+        [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Var p tt"},
+          @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty]
+    val var_eq =
+      @{thm partial_term_of_anything}
+      |> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] var_insts
+      |> Thm.varifyT_global
+    val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs;
  in
     thy
     |> Code.del_eqns const
@@ -183,7 +191,7 @@
 fun exec verbose code =
   ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
 
-fun with_tmp_dir name f =
+fun with_overlord_dir name f =
   let
     val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ()))
     val _ = Isabelle_System.mkdirs path;
@@ -192,8 +200,8 @@
 fun value ctxt (get, put, put_ml) (code, value) size =
   let
     val tmp_prefix = "Quickcheck_Narrowing"
-    val with_tmp_dir = if Config.get ctxt overlord 
-      then Isabelle_System.with_tmp_dir else Quickcheck_Narrowing.with_tmp_dir 
+    val with_tmp_dir =
+      if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
     fun run in_path = 
       let
         val code_file = Path.append in_path (Path.basic "Code.hs")