automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option

--- a/src/HOL/Library/Quickcheck_Narrowing.thy	Mon May 30 12:20:04 2011 +0100
+++ b/src/HOL/Library/Quickcheck_Narrowing.thy	Mon May 30 13:57:59 2011 +0200
@@ -86,7 +86,7 @@
   "nat_of i = nat (int_of i)"
 
 
-code_datatype "number_of \<Colon> int \<Rightarrow> code_numeral"
+code_datatype "number_of \<Colon> int \<Rightarrow> code_int"
   
   
 instantiation code_int :: "{minus, linordered_semidom, semiring_div, linorder}"
@@ -200,16 +200,19 @@
 
 subsubsection {* Narrowing's deep representation of types and terms *}
 
-datatype type = SumOfProd "type list list"
+datatype narrowing_type = SumOfProd "narrowing_type list list"
 
-datatype "term" = Var "code_int list" type | Ctr code_int "term list"
-
-datatype 'a cons = C type "(term list => 'a) list"
+datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
+datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
 
 subsubsection {* From narrowing's deep representation of terms to Code_Evaluation's terms *}
 
 class partial_term_of = typerep +
-  fixes partial_term_of :: "'a itself => term => Code_Evaluation.term"
+  fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term"
+
+lemma partial_term_of_anything: "partial_term_of x nt \<equiv> t"
+  by (rule eq_reflection) (cases "partial_term_of x nt", cases t, simp)
+
 
 subsubsection {* Auxilary functions for Narrowing *}
 
@@ -241,12 +244,12 @@
 where
   "cons a d = (C (SumOfProd [[]]) [(%_. a)])"
 
-fun conv :: "(term list => 'a) list => term => 'a"
+fun conv :: "(narrowing_term list => 'a) list => narrowing_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"
+fun nonEmpty :: "narrowing_type => bool"
 where
   "nonEmpty (SumOfProd ps) = (\<not> (List.null ps))"
 
@@ -270,7 +273,7 @@
 lemma [fundef_cong]:
   assumes "a d = a' d" "b d = b' d" "d = d'"
   shows "sum a b d = sum a' b' d'"
-using assms unfolding sum_def by (auto split: cons.split type.split)
+using assms unfolding sum_def by (auto split: cons.split narrowing_type.split)
 
 lemma [fundef_cong]:
   assumes "f d = f' d" "(\<And>d'. 0 <= d' & d' < d ==> a d' = a' d')"
@@ -284,7 +287,7 @@
   have "int_of (of_int (int_of d' - int_of (of_int 1))) < int_of d'"
     by (simp add: of_int_inverse)
   ultimately show ?thesis
-    unfolding apply_def by (auto split: cons.split type.split simp add: Let_def)
+    unfolding apply_def by (auto split: cons.split narrowing_type.split simp add: Let_def)
 qed
 
 type_synonym pos = "code_int list"
@@ -459,7 +462,7 @@
 
 instance bool :: is_testable ..
 
-instance "fun" :: ("{term_of, narrowing}", is_testable) is_testable ..
+instance "fun" :: ("{term_of, narrowing, partial_term_of}", is_testable) is_testable ..
 
 definition ensure_testable :: "'a :: is_testable => 'a :: is_testable"
 where
@@ -494,8 +497,8 @@
 
 setup {* Narrowing_Generators.setup *}
 
-hide_type (open) code_int type "term" cons
+hide_type (open) code_int narrowing_type narrowing_term cons
 hide_const (open) int_of of_int nth error toEnum map_index split_At empty
-  cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable
+  C cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable
 
 end
\ No newline at end of file

--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon May 30 12:20:04 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon May 30 13:57:59 2011 +0200
@@ -10,20 +10,20 @@
 
 -- Term refinement
 
-new :: Pos -> [[Type]] -> [Terma];
+new :: Pos -> [[Narrowing_type]] -> [Narrowing_term];
 new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
            | (c, ts) <- zip [0..] ps ];
 
-refine :: Terma -> Pos -> [Terma];
+refine :: Narrowing_term -> Pos -> [Narrowing_term];
 refine (Var p (SumOfProd ss)) [] = new p ss;
 refine (Ctr c xs) p = map (Ctr c) (refineList xs p);
 
-refineList :: [Terma] -> Pos -> [[Terma]];
+refineList :: [Narrowing_term] -> Pos -> [[Narrowing_term]];
 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
 
-total :: Terma -> [Terma];
+total :: Narrowing_term -> [Narrowing_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];
 
@@ -42,13 +42,13 @@
 str_of_list [] = "[]";
 str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
 
-report :: Result -> [Terma] -> IO Int;
+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;
 
 eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
 eval p k u = answer p (\p -> answer p k u) u;
 
-ref :: Result -> [Terma] -> IO Int;
+ref :: Result -> [Narrowing_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 Int;
@@ -71,18 +71,18 @@
 };
 
 data Result =
-  Result { args     :: [Terma]
-         , showArgs :: [Terma -> String]
-         , apply_fun    :: [Terma] -> Bool
+  Result { args     :: [Narrowing_term]
+         , showArgs :: [Narrowing_term -> String]
+         , apply_fun    :: [Narrowing_term] -> Bool
          };
 
 data P = P (Int -> Int -> Result);
 
-run :: Testable a => ([Terma] -> a) -> Int -> Int -> Result;
+run :: Testable a => ([Narrowing_term] -> a) -> Int -> Int -> Result;
 run a = let P f = property a in f;
 
 class Testable a where {
-  property :: ([Terma] -> a) -> P;
+  property :: ([Narrowing_term] -> a) -> P;
 };
 
 instance Testable Bool where {

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 30 12:20:04 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 30 13:57:59 2011 +0200
@@ -19,8 +19,89 @@
 (* configurations *)
 
 val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true)
+val overlord = Attrib.setup_config_bool @{binding quickcheck_narrowing_overlord} (K false)
 
-(* narrowing specific names and types *)
+(* partial_term_of instances *)
+
+fun mk_partial_term_of (x, T) =
+  Const (@{const_name Quickcheck_Narrowing.partial_term_of_class.partial_term_of},
+    Term.itselfT T --> @{typ narrowing_term} --> @{typ Code_Evaluation.term})
+      $ Const ("TYPE", Term.itselfT T) $ x
+
+(** formal definition **)
+
+fun add_partial_term_of tyco raw_vs thy =
+  let
+    val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
+    val ty = Type (tyco, map TFree vs);
+    val lhs = Const (@{const_name partial_term_of},
+        Term.itselfT ty --> @{typ narrowing_term} --> @{typ Code_Evaluation.term})
+      $ Free ("x", Term.itselfT ty) $ Free ("t", @{typ narrowing_term});
+    val rhs = @{term "undefined :: Code_Evaluation.term"};
+    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
+    fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
+      o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
+  in
+    thy
+    |> Class.instantiation ([tyco], vs, @{sort partial_term_of})
+    |> `(fn lthy => Syntax.check_term lthy eq)
+    |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
+    |> snd
+    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+  end;
+
+fun ensure_partial_term_of (tyco, (raw_vs, _)) thy =
+  let
+    val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort partial_term_of})
+      andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
+  in if need_inst then add_partial_term_of tyco raw_vs thy else thy end;
+
+
+(** code equations for datatypes **)
+
+fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
+  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)
+    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))
+    val insts =
+      map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
+        [Free ("ty", Term.itselfT ty), narrowing_term, rhs]
+    val cty = Thm.ctyp_of thy ty;
+  in
+    @{thm partial_term_of_anything}
+    |> Drule.instantiate' [SOME cty] insts
+    |> Thm.varifyT_global
+  end
+
+fun add_partial_term_of_code tyco raw_vs raw_cs thy =
+  let
+    val algebra = Sign.classes_of thy;
+    val vs = map (fn (v, sort) =>
+      (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
+    val ty = Type (tyco, map TFree vs);
+    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;
+ in
+    thy
+    |> Code.del_eqns const
+    |> fold Code.add_eqn eqs
+  end;
+
+fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy =
+  let
+    val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort partial_term_of};
+  in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end;
+
+
+(* narrowing generators *)
+
+(** narrowing specific names and types **)
 
 exception FUNCTION_TYPE;
 
@@ -48,7 +129,7 @@
     Const (@{const_name Quickcheck_Narrowing.sum}, T --> T --> T) $ t $ u
   end
 
-(* creating narrowing instances *)
+(** deriving narrowing instances **)
 
 fun mk_equations descr vs tycos narrowings (Ts, Us) =
   let
@@ -95,16 +176,24 @@
 
 val target = "Haskell"
 
-(* invocation of Haskell interpreter *)
+(** invocation of Haskell interpreter **)
 
 val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
 
 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 =
+  let
+    val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ()))
+    val _ = Isabelle_System.mkdirs path;
+  in Exn.release (Exn.capture f path) end;
+  
 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 
     fun run in_path = 
       let
         val code_file = Path.append in_path (Path.basic "Code.hs")
@@ -127,7 +216,7 @@
       in
         bash_output cmd
       end
-    val result = Isabelle_System.with_tmp_dir tmp_prefix run
+    val result = with_tmp_dir tmp_prefix run
     val output_value = the_default "NONE"
       (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
       |> translate_string (fn s => if s = "\\" then "\\\\" else s)
@@ -152,7 +241,7 @@
       evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args size;
   in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
 
-(* counterexample generator *)
+(** counterexample generator **)
   
 structure Counterexample = Proof_Data
 (
@@ -203,9 +292,12 @@
     (result, NONE)
   end;
 
+(* setup *)
 
 val setup =
-  Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
+  Code.datatype_interpretation ensure_partial_term_of
+  #> Code.datatype_interpretation ensure_partial_term_of_code
+  #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
     (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
   #> Context.theory_map
     (Quickcheck.add_generator ("narrowing", compile_generator_expr))