adding compilation that allows existentials in Quickcheck_Narrowing
authorbulwahn
Tue Jun 07 11:10:42 2011 +0200 (2011-06-07)
changeset 432378f5c3c6c2909
parent 43221 2c88166938eb
child 43238 04c886a1d1a5
adding compilation that allows existentials in Quickcheck_Narrowing
src/HOL/Library/Quickcheck_Narrowing.thy
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Library/Quickcheck_Narrowing.thy	Mon Jun 06 23:46:02 2011 +0200
     1.2 +++ b/src/HOL/Library/Quickcheck_Narrowing.thy	Tue Jun 07 11:10:42 2011 +0200
     1.3 @@ -5,6 +5,8 @@
     1.4  theory Quickcheck_Narrowing
     1.5  imports Main "~~/src/HOL/Library/Code_Char"
     1.6  uses
     1.7 +  ("~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
     1.8 +  ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
     1.9    ("~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML")
    1.10  begin
    1.11  
    1.12 @@ -454,6 +456,17 @@
    1.13  
    1.14  end
    1.15  
    1.16 +datatype property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
    1.17 +
    1.18 +(* FIXME: hard-wired maximal depth of 100 here *)
    1.19 +fun exists :: "('a :: {narrowing, partial_term_of} => property) => property"
    1.20 +where
    1.21 +  "exists f = (case narrowing (100 :: code_int) of C ty cs => Existential ty (\<lambda> t. f (conv cs t)) (partial_term_of (TYPE('a))))"
    1.22 +
    1.23 +fun "all" :: "('a :: {narrowing, partial_term_of} => property) => property"
    1.24 +where
    1.25 +  "all f = (case narrowing (100 :: code_int) of C ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
    1.26 +
    1.27  subsubsection {* class @{text is_testable} *}
    1.28  
    1.29  text {* The class @{text is_testable} ensures that all necessary type instances are generated. *}
    1.30 @@ -492,13 +505,15 @@
    1.31  hide_const (open) Constant eval_cfun
    1.32  
    1.33  subsubsection {* Setting up the counterexample generator *}
    1.34 -  
    1.35 +
    1.36 +setup {* Thy_Load.provide_file (Path.explode ("~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")) *}
    1.37 +setup {* Thy_Load.provide_file (Path.explode ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")) *}
    1.38  use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
    1.39  
    1.40  setup {* Narrowing_Generators.setup *}
    1.41  
    1.42  hide_type (open) code_int narrowing_type narrowing_term cons
    1.43  hide_const (open) int_of of_int nth error toEnum map_index split_At empty
    1.44 -  C cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable
    1.45 +  C cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable all exists
    1.46  
    1.47  end
    1.48 \ No newline at end of file
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jun 06 23:46:02 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Jun 07 11:10:42 2011 +0200
     2.3 @@ -6,10 +6,15 @@
     2.4  
     2.5  signature NARROWING_GENERATORS =
     2.6  sig
     2.7 -  val test_term: Proof.context -> bool * bool -> term * term list -> Quickcheck.result
     2.8 -  val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
     2.9 +  val allow_existentials : bool Config.T
    2.10    val finite_functions : bool Config.T
    2.11    val overlord : bool Config.T
    2.12 +  val test_term: Proof.context -> bool * bool -> term * term list -> Quickcheck.result
    2.13 +  datatype counterexample = Universal_Counterexample of (term * counterexample)
    2.14 +    | Existential_Counterexample of (term * counterexample) list
    2.15 +    | Empty_Assignment
    2.16 +  val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
    2.17 +  val put_existential_counterexample : (unit -> counterexample option) -> Proof.context -> Proof.context
    2.18    val setup: theory -> theory
    2.19  end;
    2.20  
    2.21 @@ -18,6 +23,7 @@
    2.22  
    2.23  (* configurations *)
    2.24  
    2.25 +val allow_existentials = Attrib.setup_config_bool @{binding quickcheck_allow_existentials} (K true)
    2.26  val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true)
    2.27  val overlord = Attrib.setup_config_bool @{binding quickcheck_narrowing_overlord} (K false)
    2.28  
    2.29 @@ -165,18 +171,25 @@
    2.30    in
    2.31      eqs
    2.32    end
    2.33 -  
    2.34 +    
    2.35 +fun contains_recursive_type_under_function_types xs =
    2.36 +  exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
    2.37 +    (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false)))) xs
    2.38 +
    2.39  fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    2.40    let
    2.41      val _ = Datatype_Aux.message config "Creating narrowing generators ...";
    2.42      val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames);
    2.43    in
    2.44 -    thy
    2.45 -    |> Class.instantiation (tycos, vs, @{sort narrowing})
    2.46 -    |> Quickcheck_Common.define_functions
    2.47 -      (fn narrowings => mk_equations descr vs tycos narrowings (Ts, Us), NONE)
    2.48 -      prfx [] narrowingsN (map narrowingT (Ts @ Us))
    2.49 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    2.50 +    if not (contains_recursive_type_under_function_types descr) then
    2.51 +      thy
    2.52 +      |> Class.instantiation (tycos, vs, @{sort narrowing})
    2.53 +      |> Quickcheck_Common.define_functions
    2.54 +        (fn narrowings => mk_equations descr vs tycos narrowings (Ts, Us), NONE)
    2.55 +        prfx [] narrowingsN (map narrowingT (Ts @ Us))
    2.56 +      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    2.57 +    else
    2.58 +      thy
    2.59    end;
    2.60  
    2.61  (* testing framework *)
    2.62 @@ -186,6 +199,7 @@
    2.63  (** invocation of Haskell interpreter **)
    2.64  
    2.65  val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
    2.66 +val pnf_narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
    2.67  
    2.68  fun exec verbose code =
    2.69    ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
    2.70 @@ -196,7 +210,7 @@
    2.71      val _ = Isabelle_System.mkdirs path;
    2.72    in Exn.release (Exn.capture f path) end;
    2.73    
    2.74 -fun value ctxt (get, put, put_ml) (code, value_name) =
    2.75 +fun value contains_existentials ctxt (get, put, put_ml) (code, value_name) =
    2.76    let
    2.77      fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
    2.78      val tmp_prefix = "Quickcheck_Narrowing"
    2.79 @@ -216,16 +230,14 @@
    2.80          val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    2.81            (unprefix "module Code where {" code)
    2.82          val _ = File.write code_file code'
    2.83 -        val _ = File.write narrowing_engine_file narrowing_engine
    2.84 +        val _ = File.write narrowing_engine_file
    2.85 +          (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
    2.86          val _ = File.write main_file main
    2.87          val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
    2.88          val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
    2.89            (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
    2.90            " -o " ^ executable ^ ";"
    2.91 -        val _ = if bash cmd <> 0 then
    2.92 -          error "Compilation failed!"
    2.93 -        else
    2.94 -          ()
    2.95 +        val _ = if bash cmd <> 0 then error "Compilation with GHC failed" else ()
    2.96          fun with_size k =
    2.97            if k > Config.get ctxt Quickcheck.size then
    2.98              NONE
    2.99 @@ -252,10 +264,10 @@
   2.100        end
   2.101    in with_tmp_dir tmp_prefix run end;
   2.102  
   2.103 -fun dynamic_value_strict cookie thy postproc t =
   2.104 +fun dynamic_value_strict contains_existentials cookie thy postproc t =
   2.105    let
   2.106      val ctxt = Proof_Context.init_global thy
   2.107 -    fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value ctxt cookie)
   2.108 +    fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value contains_existentials ctxt cookie)
   2.109        (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
   2.110    in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
   2.111  
   2.112 @@ -267,6 +279,24 @@
   2.113    fun init _ () = error "Counterexample"
   2.114  )
   2.115  
   2.116 +datatype counterexample = Universal_Counterexample of (term * counterexample)
   2.117 +  | Existential_Counterexample of (term * counterexample) list
   2.118 +  | Empty_Assignment
   2.119 +  
   2.120 +fun map_counterexample f Empty_Assignment = Empty_Assignment
   2.121 +  | map_counterexample f (Universal_Counterexample (t, c)) =
   2.122 +      Universal_Counterexample (f t, map_counterexample f c)
   2.123 +  | map_counterexample f (Existential_Counterexample cs) =
   2.124 +      Existential_Counterexample (map (fn (t, c) => (f t, map_counterexample f c)) cs)
   2.125 +
   2.126 +structure Existential_Counterexample = Proof_Data
   2.127 +(
   2.128 +  type T = unit -> counterexample option
   2.129 +  fun init _ () = error "Counterexample"
   2.130 +)
   2.131 +
   2.132 +val put_existential_counterexample = Existential_Counterexample.put
   2.133 +
   2.134  val put_counterexample = Counterexample.put
   2.135  
   2.136  fun finitize_functions t =
   2.137 @@ -297,20 +327,83 @@
   2.138    end
   2.139  
   2.140  (** tester **)
   2.141 +
   2.142 +val rewrs =
   2.143 +  map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) (@{thms all_simps} @ @{thms ex_simps})
   2.144 +    @ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) [@{thm not_ex}, @{thm not_all}]
   2.145 +
   2.146 +fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t
   2.147 +
   2.148 +fun strip_quantifiers (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
   2.149 +    apfst (cons (@{const_name Ex}, (x, T))) (strip_quantifiers t)
   2.150 +  | strip_quantifiers (Const (@{const_name All}, _) $ Abs (x, T, t)) =
   2.151 +    apfst (cons (@{const_name All}, (x, T))) (strip_quantifiers t)
   2.152 +  | strip_quantifiers t = ([], t)
   2.153 +
   2.154 +fun contains_existentials t = exists (fn (Q, _) => Q = @{const_name Ex}) (fst (strip_quantifiers t))
   2.155 +
   2.156 +fun mk_property qs t =
   2.157 +  let
   2.158 +    fun enclose (@{const_name Ex}, (x, T)) t =
   2.159 +        Const (@{const_name Quickcheck_Narrowing.exists}, (T --> @{typ property}) --> @{typ property})
   2.160 +          $ Abs (x, T, t)
   2.161 +      | enclose (@{const_name All}, (x, T)) t =
   2.162 +        Const (@{const_name Quickcheck_Narrowing.all}, (T --> @{typ property}) --> @{typ property})
   2.163 +          $ Abs (x, T, t)
   2.164 +  in
   2.165 +    fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $
   2.166 +      (list_comb (t , map Bound (((length qs) - 1) downto 0))))
   2.167 +  end
   2.168 +
   2.169    
   2.170 -fun test_term  ctxt (limit_time, is_interactive) (t, eval_terms) =
   2.171 +fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
   2.172 +    fst (Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
   2.173 +      (t, mk_case_term ctxt (p - 1) qs' c)) cs))
   2.174 +  | mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) =
   2.175 +    if p = 0 then t else mk_case_term ctxt (p - 1) qs' c
   2.176 +
   2.177 +fun mk_terms ctxt qs result =
   2.178 +  let
   2.179 +    val
   2.180 +      ps = filter (fn (_, (@{const_name All}, _)) => true | _ => false) (map_index I qs)
   2.181 +    in
   2.182 +      map (fn (p, (_, (x, T))) => (x, mk_case_term ctxt p qs result)) ps
   2.183 +    end
   2.184 +  
   2.185 +fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
   2.186    let
   2.187      val thy = Proof_Context.theory_of ctxt
   2.188 -    val t' = list_abs_free (Term.add_frees t [], t)
   2.189 -    val t'' = if Config.get ctxt finite_functions then finitize_functions t' else t'
   2.190 -    fun ensure_testable t =
   2.191 -      Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   2.192 -    val result = dynamic_value_strict
   2.193 -      (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
   2.194 -      thy (Option.map o map) (ensure_testable t'')
   2.195 +    val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
   2.196 +    val pnf_t = make_pnf_term thy t'
   2.197    in
   2.198 -    Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) result,
   2.199 -      evaluation_terms = Option.map (K []) result, timings = [], reports = []}
   2.200 +    if Config.get ctxt allow_existentials andalso contains_existentials pnf_t then
   2.201 +      let
   2.202 +        val (qs, t') = strip_quantifiers pnf_t
   2.203 +        val prop_term = fold_rev (fn (_, (x, T)) => fn t => Abs (x, T, t)) qs t'
   2.204 +        val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
   2.205 +          ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
   2.206 +        val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt') 
   2.207 +        val result = dynamic_value_strict true
   2.208 +          (Existential_Counterexample.get, Existential_Counterexample.put,
   2.209 +            "Narrowing_Generators.put_existential_counterexample")
   2.210 +          thy' (Option.map o map_counterexample) (mk_property qs prop_def')
   2.211 +        val result' = Option.map (mk_terms ctxt' (fst (strip_quantifiers pnf_t))) result
   2.212 +      in
   2.213 +        Quickcheck.Result {counterexample = result', evaluation_terms = Option.map (K []) result,
   2.214 +          timings = [], reports = []}
   2.215 +      end
   2.216 +    else (let
   2.217 +      val t' = HOLogic.list_all (Term.add_frees t [], t)
   2.218 +      val t'' = if Config.get ctxt finite_functions then finitize_functions t' else t'
   2.219 +      fun ensure_testable t =
   2.220 +        Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   2.221 +      val result = dynamic_value_strict false
   2.222 +        (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
   2.223 +        thy (Option.map o map) (ensure_testable t'')
   2.224 +    in
   2.225 +      Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) result,
   2.226 +        evaluation_terms = Option.map (K []) result, timings = [], reports = []}
   2.227 +    end)
   2.228    end;
   2.229  
   2.230  fun test_goals ctxt (limit_time, is_interactive) insts goals =