tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
authorbulwahn
Mon Mar 14 12:34:10 2011 +0100 (2011-03-14)
changeset 41963d8c3b26b3da4
parent 41962 27a61a3266d8
child 41964 13904699c859
tuned exhaustive generator compilation; added narrowing generator compilation; removed exec as does not work properly here (reverting changeset 994d088fbfbc)
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/ex/Quickcheck_Narrowing_Examples.thy
     1.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Mar 14 12:34:09 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Mon Mar 14 12:34:10 2011 +0100
     1.3 @@ -87,11 +87,11 @@
     1.4  fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
     1.5    --> @{typ "Code_Evaluation.term list option"}
     1.6  
     1.7 -fun mk_equations thy descr vs tycos exhaustives (Ts, Us) =
     1.8 +fun mk_equations descr vs tycos exhaustives (Ts, Us) =
     1.9    let
    1.10      fun mk_call T =
    1.11        let
    1.12 -        val exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)        
    1.13 +        val exhaustive = Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.exhaustive"}, exhaustiveT T)
    1.14        in
    1.15          (T, (fn t => exhaustive $
    1.16            (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
    1.17 @@ -173,7 +173,7 @@
    1.18      |> (if define_foundationally then
    1.19        let
    1.20          val exhaustives = map2 (fn name => fn T => Free (name, exhaustiveT T)) exhaustivesN (Ts @ Us)
    1.21 -        val eqs = mk_equations thy descr vs tycos exhaustives (Ts, Us)
    1.22 +        val eqs = mk_equations descr vs tycos exhaustives (Ts, Us)
    1.23        in
    1.24          Function.add_function
    1.25            (map (fn (name, T) =>
    1.26 @@ -206,7 +206,7 @@
    1.27      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.28    end handle FUNCTION_TYPE =>
    1.29      (Datatype_Aux.message config
    1.30 -      "Creation of exhaustivevalue generators failed because the datatype contains a function type";
    1.31 +      "Creation of exhaustive generators failed because the datatype contains a function type";
    1.32      thy)
    1.33  
    1.34  (** building and compiling generator expressions **)
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Mar 14 12:34:09 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Mar 14 12:34:10 2011 +0100
     2.3 @@ -15,6 +15,100 @@
     2.4  structure Narrowing_Generators : NARROWING_GENERATORS =
     2.5  struct
     2.6  
     2.7 +fun mk_undefined T = Const(@{const_name undefined}, T)
     2.8 +
     2.9 +(* narrowing specific names and types *)
    2.10 +
    2.11 +exception FUNCTION_TYPE;
    2.12 +
    2.13 +val narrowingN = "narrowing";
    2.14 +
    2.15 +fun narrowingT T =
    2.16 +  @{typ Quickcheck_Narrowing.code_int} --> Type (@{type_name Quickcheck_Narrowing.cons}, [T])
    2.17 +
    2.18 +fun mk_empty T = Const (@{const_name Quickcheck_Narrowing.empty}, narrowingT T)
    2.19 +
    2.20 +fun mk_cons c T = Const (@{const_name Quickcheck_Narrowing.cons}, T --> narrowingT T) $ Const (c, T)
    2.21 +
    2.22 +fun mk_apply (T, t) (U, u) =
    2.23 +  let
    2.24 +    val (_, U') = dest_funT U
    2.25 +  in
    2.26 +    (U', Const (@{const_name Quickcheck_Narrowing.apply},
    2.27 +      narrowingT U --> narrowingT T --> narrowingT U') $ u $ t)
    2.28 +  end
    2.29 +  
    2.30 +fun mk_sum (t, u) =
    2.31 +  let
    2.32 +    val T = fastype_of t
    2.33 +  in
    2.34 +    Const (@{const_name Quickcheck_Narrowing.sum}, T --> T --> T) $ t $ u
    2.35 +  end
    2.36 +
    2.37 +(* creating narrowing instances *)
    2.38 +
    2.39 +fun mk_equations descr vs tycos narrowings (Ts, Us) =
    2.40 +  let
    2.41 +    fun mk_call T =
    2.42 +      let
    2.43 +        val narrowing =
    2.44 +          Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T)
    2.45 +      in
    2.46 +        (T, narrowing)
    2.47 +      end
    2.48 +    fun mk_aux_call fTs (k, _) (tyco, Ts) =
    2.49 +      let
    2.50 +        val T = Type (tyco, Ts)
    2.51 +        val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
    2.52 +      in
    2.53 +        (T, nth narrowings k)
    2.54 +      end
    2.55 +    fun mk_consexpr simpleT (c, xs) =
    2.56 +      let
    2.57 +        val Ts = map fst xs
    2.58 +      in snd (fold mk_apply xs (Ts ---> simpleT, mk_cons c (Ts ---> simpleT))) end
    2.59 +    fun mk_rhs exprs = foldr1 mk_sum exprs
    2.60 +    val rhss =
    2.61 +      Datatype_Aux.interpret_construction descr vs
    2.62 +        { atyp = mk_call, dtyp = mk_aux_call }
    2.63 +      |> (map o apfst) Type
    2.64 +      |> map (fn (T, cs) => map (mk_consexpr T) cs)
    2.65 +      |> map mk_rhs
    2.66 +    val lhss = narrowings
    2.67 +    val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
    2.68 +  in
    2.69 +    eqs
    2.70 +  end
    2.71 +
    2.72 +
    2.73 +fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    2.74 +  let
    2.75 +    val _ = Datatype_Aux.message config "Creating narrowing generators ...";
    2.76 +    val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames);
    2.77 +  in
    2.78 +    thy
    2.79 +    |> Class.instantiation (tycos, vs, @{sort narrowing})
    2.80 +    |> (fold_map (fn (name, T) => Local_Theory.define
    2.81 +          ((Binding.conceal (Binding.name name), NoSyn),
    2.82 +            (apfst Binding.conceal Attrib.empty_binding, mk_undefined (narrowingT T)))
    2.83 +        #> apfst fst) (narrowingsN ~~ (Ts @ Us))
    2.84 +      #> (fn (narrowings, lthy) =>
    2.85 +        let
    2.86 +          val eqs_t = mk_equations descr vs tycos narrowings (Ts, Us)
    2.87 +          val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
    2.88 +            (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
    2.89 +        in
    2.90 +          fold (fn (name, eq) => Local_Theory.note
    2.91 +          ((Binding.conceal (Binding.qualify true prfx
    2.92 +             (Binding.qualify true name (Binding.name "simps"))),
    2.93 +             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
    2.94 +               [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (narrowingsN ~~ eqs) lthy
    2.95 +        end))
    2.96 +    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    2.97 +  end;
    2.98 +
    2.99 +(* testing framework *)
   2.100 +
   2.101  val target = "Haskell"
   2.102  
   2.103  (* invocation of Haskell interpreter *)
   2.104 @@ -43,9 +137,10 @@
   2.105          val _ = File.write narrowing_engine_file narrowing_engine
   2.106          val _ = File.write main_file main
   2.107          val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
   2.108 -        val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
   2.109 +        val cmd = "\"$ISABELLE_GHC\" -fglasgow-exts " ^
   2.110            (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
   2.111            " -o " ^ executable ^ " && " ^ executable
   2.112 +          (* FIXME: should use bash command exec but does not work with && *) 
   2.113        in
   2.114          bash_output cmd
   2.115        end
   2.116 @@ -97,7 +192,9 @@
   2.117  
   2.118  
   2.119  val setup =
   2.120 -  Context.theory_map
   2.121 +  Datatype.interpretation
   2.122 +    (Quickcheck_Common.ensure_sort_datatype (@{sort narrowing}, instantiate_narrowing_datatype))
   2.123 +  #> Context.theory_map
   2.124      (Quickcheck.add_generator ("narrowing", compile_generator_expr))
   2.125      
   2.126  end;
   2.127 \ No newline at end of file
     3.1 --- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Mon Mar 14 12:34:09 2011 +0100
     3.2 +++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Mon Mar 14 12:34:10 2011 +0100
     3.3 @@ -112,23 +112,6 @@
     3.4  by (simp add: set_of')
     3.5  
     3.6  declare is_ord.simps(1)[code] is_ord_mkt[code]
     3.7 -                 
     3.8 -subsection {* Necessary instantiation for quickcheck generator *}
     3.9 -
    3.10 -instantiation tree :: (narrowing) narrowing
    3.11 -begin
    3.12 -
    3.13 -function narrowing_tree
    3.14 -where
    3.15 -  "narrowing_tree d = sum (cons ET) (apply (apply (apply (apply (cons MKT) narrowing) narrowing_tree) narrowing_tree) narrowing) d"
    3.16 -by pat_completeness auto
    3.17 -
    3.18 -termination proof (relation "measure nat_of")
    3.19 -qed (auto simp add: of_int_inverse nat_of_def)
    3.20 -
    3.21 -instance ..
    3.22 -
    3.23 -end
    3.24  
    3.25  subsubsection {* Invalid Lemma due to typo in lbal *}
    3.26