src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 43237 8f5c3c6c2909
parent 43114 b9fca691addd
child 43240 da47097bd589
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jun 06 23:46:02 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Tue Jun 07 11:10:42 2011 +0200
     1.3 @@ -6,10 +6,15 @@
     1.4  
     1.5  signature NARROWING_GENERATORS =
     1.6  sig
     1.7 -  val test_term: Proof.context -> bool * bool -> term * term list -> Quickcheck.result
     1.8 -  val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
     1.9 +  val allow_existentials : bool Config.T
    1.10    val finite_functions : bool Config.T
    1.11    val overlord : bool Config.T
    1.12 +  val test_term: Proof.context -> bool * bool -> term * term list -> Quickcheck.result
    1.13 +  datatype counterexample = Universal_Counterexample of (term * counterexample)
    1.14 +    | Existential_Counterexample of (term * counterexample) list
    1.15 +    | Empty_Assignment
    1.16 +  val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
    1.17 +  val put_existential_counterexample : (unit -> counterexample option) -> Proof.context -> Proof.context
    1.18    val setup: theory -> theory
    1.19  end;
    1.20  
    1.21 @@ -18,6 +23,7 @@
    1.22  
    1.23  (* configurations *)
    1.24  
    1.25 +val allow_existentials = Attrib.setup_config_bool @{binding quickcheck_allow_existentials} (K true)
    1.26  val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true)
    1.27  val overlord = Attrib.setup_config_bool @{binding quickcheck_narrowing_overlord} (K false)
    1.28  
    1.29 @@ -165,18 +171,25 @@
    1.30    in
    1.31      eqs
    1.32    end
    1.33 -  
    1.34 +    
    1.35 +fun contains_recursive_type_under_function_types xs =
    1.36 +  exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
    1.37 +    (case Datatype_Aux.strip_dtyp dT of (_ :: _, Datatype.DtRec _) => true | _ => false)))) xs
    1.38 +
    1.39  fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    1.40    let
    1.41      val _ = Datatype_Aux.message config "Creating narrowing generators ...";
    1.42      val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames);
    1.43    in
    1.44 -    thy
    1.45 -    |> Class.instantiation (tycos, vs, @{sort narrowing})
    1.46 -    |> Quickcheck_Common.define_functions
    1.47 -      (fn narrowings => mk_equations descr vs tycos narrowings (Ts, Us), NONE)
    1.48 -      prfx [] narrowingsN (map narrowingT (Ts @ Us))
    1.49 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.50 +    if not (contains_recursive_type_under_function_types descr) then
    1.51 +      thy
    1.52 +      |> Class.instantiation (tycos, vs, @{sort narrowing})
    1.53 +      |> Quickcheck_Common.define_functions
    1.54 +        (fn narrowings => mk_equations descr vs tycos narrowings (Ts, Us), NONE)
    1.55 +        prfx [] narrowingsN (map narrowingT (Ts @ Us))
    1.56 +      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.57 +    else
    1.58 +      thy
    1.59    end;
    1.60  
    1.61  (* testing framework *)
    1.62 @@ -186,6 +199,7 @@
    1.63  (** invocation of Haskell interpreter **)
    1.64  
    1.65  val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
    1.66 +val pnf_narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
    1.67  
    1.68  fun exec verbose code =
    1.69    ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
    1.70 @@ -196,7 +210,7 @@
    1.71      val _ = Isabelle_System.mkdirs path;
    1.72    in Exn.release (Exn.capture f path) end;
    1.73    
    1.74 -fun value ctxt (get, put, put_ml) (code, value_name) =
    1.75 +fun value contains_existentials ctxt (get, put, put_ml) (code, value_name) =
    1.76    let
    1.77      fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
    1.78      val tmp_prefix = "Quickcheck_Narrowing"
    1.79 @@ -216,16 +230,14 @@
    1.80          val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    1.81            (unprefix "module Code where {" code)
    1.82          val _ = File.write code_file code'
    1.83 -        val _ = File.write narrowing_engine_file narrowing_engine
    1.84 +        val _ = File.write narrowing_engine_file
    1.85 +          (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
    1.86          val _ = File.write main_file main
    1.87          val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
    1.88          val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
    1.89            (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
    1.90            " -o " ^ executable ^ ";"
    1.91 -        val _ = if bash cmd <> 0 then
    1.92 -          error "Compilation failed!"
    1.93 -        else
    1.94 -          ()
    1.95 +        val _ = if bash cmd <> 0 then error "Compilation with GHC failed" else ()
    1.96          fun with_size k =
    1.97            if k > Config.get ctxt Quickcheck.size then
    1.98              NONE
    1.99 @@ -252,10 +264,10 @@
   1.100        end
   1.101    in with_tmp_dir tmp_prefix run end;
   1.102  
   1.103 -fun dynamic_value_strict cookie thy postproc t =
   1.104 +fun dynamic_value_strict contains_existentials cookie thy postproc t =
   1.105    let
   1.106      val ctxt = Proof_Context.init_global thy
   1.107 -    fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value ctxt cookie)
   1.108 +    fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value contains_existentials ctxt cookie)
   1.109        (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
   1.110    in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
   1.111  
   1.112 @@ -267,6 +279,24 @@
   1.113    fun init _ () = error "Counterexample"
   1.114  )
   1.115  
   1.116 +datatype counterexample = Universal_Counterexample of (term * counterexample)
   1.117 +  | Existential_Counterexample of (term * counterexample) list
   1.118 +  | Empty_Assignment
   1.119 +  
   1.120 +fun map_counterexample f Empty_Assignment = Empty_Assignment
   1.121 +  | map_counterexample f (Universal_Counterexample (t, c)) =
   1.122 +      Universal_Counterexample (f t, map_counterexample f c)
   1.123 +  | map_counterexample f (Existential_Counterexample cs) =
   1.124 +      Existential_Counterexample (map (fn (t, c) => (f t, map_counterexample f c)) cs)
   1.125 +
   1.126 +structure Existential_Counterexample = Proof_Data
   1.127 +(
   1.128 +  type T = unit -> counterexample option
   1.129 +  fun init _ () = error "Counterexample"
   1.130 +)
   1.131 +
   1.132 +val put_existential_counterexample = Existential_Counterexample.put
   1.133 +
   1.134  val put_counterexample = Counterexample.put
   1.135  
   1.136  fun finitize_functions t =
   1.137 @@ -297,20 +327,83 @@
   1.138    end
   1.139  
   1.140  (** tester **)
   1.141 +
   1.142 +val rewrs =
   1.143 +  map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) (@{thms all_simps} @ @{thms ex_simps})
   1.144 +    @ map (HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) [@{thm not_ex}, @{thm not_all}]
   1.145 +
   1.146 +fun make_pnf_term thy t = Pattern.rewrite_term thy rewrs [] t
   1.147 +
   1.148 +fun strip_quantifiers (Const (@{const_name Ex}, _) $ Abs (x, T, t)) =
   1.149 +    apfst (cons (@{const_name Ex}, (x, T))) (strip_quantifiers t)
   1.150 +  | strip_quantifiers (Const (@{const_name All}, _) $ Abs (x, T, t)) =
   1.151 +    apfst (cons (@{const_name All}, (x, T))) (strip_quantifiers t)
   1.152 +  | strip_quantifiers t = ([], t)
   1.153 +
   1.154 +fun contains_existentials t = exists (fn (Q, _) => Q = @{const_name Ex}) (fst (strip_quantifiers t))
   1.155 +
   1.156 +fun mk_property qs t =
   1.157 +  let
   1.158 +    fun enclose (@{const_name Ex}, (x, T)) t =
   1.159 +        Const (@{const_name Quickcheck_Narrowing.exists}, (T --> @{typ property}) --> @{typ property})
   1.160 +          $ Abs (x, T, t)
   1.161 +      | enclose (@{const_name All}, (x, T)) t =
   1.162 +        Const (@{const_name Quickcheck_Narrowing.all}, (T --> @{typ property}) --> @{typ property})
   1.163 +          $ Abs (x, T, t)
   1.164 +  in
   1.165 +    fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $
   1.166 +      (list_comb (t , map Bound (((length qs) - 1) downto 0))))
   1.167 +  end
   1.168 +
   1.169    
   1.170 -fun test_term  ctxt (limit_time, is_interactive) (t, eval_terms) =
   1.171 +fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
   1.172 +    fst (Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
   1.173 +      (t, mk_case_term ctxt (p - 1) qs' c)) cs))
   1.174 +  | mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) =
   1.175 +    if p = 0 then t else mk_case_term ctxt (p - 1) qs' c
   1.176 +
   1.177 +fun mk_terms ctxt qs result =
   1.178 +  let
   1.179 +    val
   1.180 +      ps = filter (fn (_, (@{const_name All}, _)) => true | _ => false) (map_index I qs)
   1.181 +    in
   1.182 +      map (fn (p, (_, (x, T))) => (x, mk_case_term ctxt p qs result)) ps
   1.183 +    end
   1.184 +  
   1.185 +fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
   1.186    let
   1.187      val thy = Proof_Context.theory_of ctxt
   1.188 -    val t' = list_abs_free (Term.add_frees t [], t)
   1.189 -    val t'' = if Config.get ctxt finite_functions then finitize_functions t' else t'
   1.190 -    fun ensure_testable t =
   1.191 -      Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   1.192 -    val result = dynamic_value_strict
   1.193 -      (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
   1.194 -      thy (Option.map o map) (ensure_testable t'')
   1.195 +    val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
   1.196 +    val pnf_t = make_pnf_term thy t'
   1.197    in
   1.198 -    Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) result,
   1.199 -      evaluation_terms = Option.map (K []) result, timings = [], reports = []}
   1.200 +    if Config.get ctxt allow_existentials andalso contains_existentials pnf_t then
   1.201 +      let
   1.202 +        val (qs, t') = strip_quantifiers pnf_t
   1.203 +        val prop_term = fold_rev (fn (_, (x, T)) => fn t => Abs (x, T, t)) qs t'
   1.204 +        val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
   1.205 +          ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
   1.206 +        val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt') 
   1.207 +        val result = dynamic_value_strict true
   1.208 +          (Existential_Counterexample.get, Existential_Counterexample.put,
   1.209 +            "Narrowing_Generators.put_existential_counterexample")
   1.210 +          thy' (Option.map o map_counterexample) (mk_property qs prop_def')
   1.211 +        val result' = Option.map (mk_terms ctxt' (fst (strip_quantifiers pnf_t))) result
   1.212 +      in
   1.213 +        Quickcheck.Result {counterexample = result', evaluation_terms = Option.map (K []) result,
   1.214 +          timings = [], reports = []}
   1.215 +      end
   1.216 +    else (let
   1.217 +      val t' = HOLogic.list_all (Term.add_frees t [], t)
   1.218 +      val t'' = if Config.get ctxt finite_functions then finitize_functions t' else t'
   1.219 +      fun ensure_testable t =
   1.220 +        Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   1.221 +      val result = dynamic_value_strict false
   1.222 +        (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
   1.223 +        thy (Option.map o map) (ensure_testable t'')
   1.224 +    in
   1.225 +      Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) result,
   1.226 +        evaluation_terms = Option.map (K []) result, timings = [], reports = []}
   1.227 +    end)
   1.228    end;
   1.229  
   1.230  fun test_goals ctxt (limit_time, is_interactive) insts goals =