# HG changeset patch
# User bulwahn
# Date 1300102450 -3600
# Node ID d8c3b26b3da4118bf0e4a314e5366d527241de34
# Parent  27a61a3266d86424aa4a9f5944e9c7ebcffc7a0c
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)

diff -r 27a61a3266d8 -r d8c3b26b3da4 src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Mar 14 12:34:09 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Mar 14 12:34:10 2011 +0100
@@ -87,11 +87,11 @@
 fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
   --> @{typ "Code_Evaluation.term list option"}
 
-fun mk_equations thy descr vs tycos exhaustives (Ts, Us) =
+fun mk_equations descr vs tycos exhaustives (Ts, Us) =
   let
     fun mk_call T =
       let
-        val exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)        
+        val exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
       in
         (T, (fn t => exhaustive $
           (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
@@ -173,7 +173,7 @@
     |> (if define_foundationally then
       let
         val exhaustives = map2 (fn name => fn T => Free (name, exhaustiveT T)) exhaustivesN (Ts @ Us)
-        val eqs = mk_equations thy descr vs tycos exhaustives (Ts, Us)
+        val eqs = mk_equations descr vs tycos exhaustives (Ts, Us)
       in
         Function.add_function
           (map (fn (name, T) =>
@@ -206,7 +206,7 @@
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   end handle FUNCTION_TYPE =>
     (Datatype_Aux.message config
-      "Creation of exhaustivevalue generators failed because the datatype contains a function type";
+      "Creation of exhaustive generators failed because the datatype contains a function type";
     thy)
 
 (** building and compiling generator expressions **)
diff -r 27a61a3266d8 -r d8c3b26b3da4 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Mar 14 12:34:09 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Mar 14 12:34:10 2011 +0100
@@ -15,6 +15,100 @@
 structure Narrowing_Generators : NARROWING_GENERATORS =
 struct
 
+fun mk_undefined T = Const(@{const_name undefined}, T)
+
+(* narrowing specific names and types *)
+
+exception FUNCTION_TYPE;
+
+val narrowingN = "narrowing";
+
+fun narrowingT T =
+  @{typ Quickcheck_Narrowing.code_int} --> Type (@{type_name Quickcheck_Narrowing.cons}, [T])
+
+fun mk_empty T = Const (@{const_name Quickcheck_Narrowing.empty}, narrowingT T)
+
+fun mk_cons c T = Const (@{const_name Quickcheck_Narrowing.cons}, T --> narrowingT T) $ Const (c, T)
+
+fun mk_apply (T, t) (U, u) =
+  let
+    val (_, U') = dest_funT U
+  in
+    (U', Const (@{const_name Quickcheck_Narrowing.apply},
+      narrowingT U --> narrowingT T --> narrowingT U') $ u $ t)
+  end
+  
+fun mk_sum (t, u) =
+  let
+    val T = fastype_of t
+  in
+    Const (@{const_name Quickcheck_Narrowing.sum}, T --> T --> T) $ t $ u
+  end
+
+(* creating narrowing instances *)
+
+fun mk_equations descr vs tycos narrowings (Ts, Us) =
+  let
+    fun mk_call T =
+      let
+        val narrowing =
+          Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T)
+      in
+        (T, narrowing)
+      end
+    fun mk_aux_call fTs (k, _) (tyco, Ts) =
+      let
+        val T = Type (tyco, Ts)
+        val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
+      in
+        (T, nth narrowings k)
+      end
+    fun mk_consexpr simpleT (c, xs) =
+      let
+        val Ts = map fst xs
+      in snd (fold mk_apply xs (Ts ---> simpleT, mk_cons c (Ts ---> simpleT))) end
+    fun mk_rhs exprs = foldr1 mk_sum exprs
+    val rhss =
+      Datatype_Aux.interpret_construction descr vs
+        { atyp = mk_call, dtyp = mk_aux_call }
+      |> (map o apfst) Type
+      |> map (fn (T, cs) => map (mk_consexpr T) cs)
+      |> map mk_rhs
+    val lhss = narrowings
+    val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
+  in
+    eqs
+  end
+
+
+fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
+  let
+    val _ = Datatype_Aux.message config "Creating narrowing generators ...";
+    val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames);
+  in
+    thy
+    |> Class.instantiation (tycos, vs, @{sort narrowing})
+    |> (fold_map (fn (name, T) => Local_Theory.define
+          ((Binding.conceal (Binding.name name), NoSyn),
+            (apfst Binding.conceal Attrib.empty_binding, mk_undefined (narrowingT T)))
+        #> apfst fst) (narrowingsN ~~ (Ts @ Us))
+      #> (fn (narrowings, lthy) =>
+        let
+          val eqs_t = mk_equations descr vs tycos narrowings (Ts, Us)
+          val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
+            (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
+        in
+          fold (fn (name, eq) => Local_Theory.note
+          ((Binding.conceal (Binding.qualify true prfx
+             (Binding.qualify true name (Binding.name "simps"))),
+             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
+               [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (narrowingsN ~~ eqs) lthy
+        end))
+    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
+  end;
+
+(* testing framework *)
+
 val target = "Haskell"
 
 (* invocation of Haskell interpreter *)
@@ -43,9 +137,10 @@
         val _ = File.write narrowing_engine_file narrowing_engine
         val _ = File.write main_file main
         val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
-        val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
+        val cmd = "\"$ISABELLE_GHC\" -fglasgow-exts " ^
           (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
           " -o " ^ executable ^ " && " ^ executable
+          (* FIXME: should use bash command exec but does not work with && *) 
       in
         bash_output cmd
       end
@@ -97,7 +192,9 @@
 
 
 val setup =
-  Context.theory_map
+  Datatype.interpretation
+    (Quickcheck_Common.ensure_sort_datatype (@{sort narrowing}, instantiate_narrowing_datatype))
+  #> Context.theory_map
     (Quickcheck.add_generator ("narrowing", compile_generator_expr))
     
 end;
\ No newline at end of file
diff -r 27a61a3266d8 -r d8c3b26b3da4 src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Mon Mar 14 12:34:09 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Mon Mar 14 12:34:10 2011 +0100
@@ -112,23 +112,6 @@
 by (simp add: set_of')
 
 declare is_ord.simps(1)[code] is_ord_mkt[code]
-                 
-subsection {* Necessary instantiation for quickcheck generator *}
-
-instantiation tree :: (narrowing) narrowing
-begin
-
-function narrowing_tree
-where
-  "narrowing_tree d = sum (cons ET) (apply (apply (apply (apply (cons MKT) narrowing) narrowing_tree) narrowing_tree) narrowing) d"
-by pat_completeness auto
-
-termination proof (relation "measure nat_of")
-qed (auto simp add: of_int_inverse nat_of_def)
-
-instance ..
-
-end
 
 subsubsection {* Invalid Lemma due to typo in lbal *}