src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 46309 693d8d7bc3cd
parent 46219 426ed18eba43
child 46316 1c9a548c0402
equal deleted inserted replaced
46308:e5abbec2697a 46309:693d8d7bc3cd
     8 sig
     8 sig
     9   val allow_existentials : bool Config.T
     9   val allow_existentials : bool Config.T
    10   val finite_functions : bool Config.T
    10   val finite_functions : bool Config.T
    11   val overlord : bool Config.T
    11   val overlord : bool Config.T
    12   val active : bool Config.T
    12   val active : bool Config.T
    13   val test_term: Proof.context -> term * term list -> Quickcheck.result
       
    14   datatype counterexample = Universal_Counterexample of (term * counterexample)
    13   datatype counterexample = Universal_Counterexample of (term * counterexample)
    15     | Existential_Counterexample of (term * counterexample) list
    14     | Existential_Counterexample of (term * counterexample) list
    16     | Empty_Assignment
    15     | Empty_Assignment
    17   val put_counterexample: (unit -> (bool * term list) option) -> Proof.context -> Proof.context
    16   val put_counterexample: (unit -> (bool * term list) option) -> Proof.context -> Proof.context
    18   val put_existential_counterexample : (unit -> counterexample option) -> Proof.context -> Proof.context
    17   val put_existential_counterexample : (unit -> counterexample option) -> Proof.context -> Proof.context
   428     in
   427     in
   429       map (fn (p, (_, (x, T))) => (x, mk_case_term ctxt p qs result)) ps
   428       map (fn (p, (_, (x, T))) => (x, mk_case_term ctxt p qs result)) ps
   430       |> map (apsnd post_process)
   429       |> map (apsnd post_process)
   431     end
   430     end
   432   
   431   
   433 fun test_term ctxt (t, eval_terms) =
   432 fun test_term ctxt catch_code_errors (t, eval_terms) =
   434   let
   433   let
   435     fun dest_result (Quickcheck.Result r) = r 
   434     fun dest_result (Quickcheck.Result r) = r 
   436     val opts =
   435     val opts =
   437       ((Config.get ctxt Quickcheck.genuine_only,
   436       ((Config.get ctxt Quickcheck.genuine_only,
   438        (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.verbose)),
   437        (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.verbose)),
   446         fun wrap f (qs, t) =
   445         fun wrap f (qs, t) =
   447           let val (qs1, qs2) = split_list qs in
   446           let val (qs1, qs2) = split_list qs in
   448           apfst (map2 pair qs1) (f (qs2, t)) end
   447           apfst (map2 pair qs1) (f (qs2, t)) end
   449         val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
   448         val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
   450         val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
   449         val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
   451         val (counterexample, result) = dynamic_value_strict (true, opts)
   450         val act = if catch_code_errors then try else (fn f => SOME o f)
       
   451         val execute = dynamic_value_strict (true, opts)
   452           ((K true, fn _ => error ""), (Existential_Counterexample.get, Existential_Counterexample.put,
   452           ((K true, fn _ => error ""), (Existential_Counterexample.get, Existential_Counterexample.put,
   453             "Narrowing_Generators.put_existential_counterexample"))
   453             "Narrowing_Generators.put_existential_counterexample"))
   454           thy (apfst o Option.map o map_counterexample) (mk_property qs prop_t)
   454           thy (apfst o Option.map o map_counterexample)
   455       in
   455       in  
   456         Quickcheck.Result
   456         case act execute (mk_property qs prop_t) of 
   457          {counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample,
   457           SOME (counterexample, result) => Quickcheck.Result
   458           evaluation_terms = Option.map (K []) counterexample,
   458             {counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample,
   459           timings = #timings (dest_result result), reports = #reports (dest_result result)}
   459             evaluation_terms = Option.map (K []) counterexample,
       
   460             timings = #timings (dest_result result), reports = #reports (dest_result result)}
       
   461         | NONE =>
       
   462           (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-narrowing");
       
   463            Quickcheck.empty_result)
   460       end
   464       end
   461     else
   465     else
   462       let
   466       let
   463         val frees = Term.add_frees t []
   467         val frees = Term.add_frees t []
   464         val t' = fold_rev absfree frees t
   468         val t' = fold_rev absfree frees t
   467         fun ensure_testable t =
   471         fun ensure_testable t =
   468           Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   472           Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   469         fun is_genuine (SOME (true, _)) = true 
   473         fun is_genuine (SOME (true, _)) = true 
   470           | is_genuine _ = false
   474           | is_genuine _ = false
   471         val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process))
   475         val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process))
   472         val (counterexample, result) = dynamic_value_strict (false, opts)
   476         val act = if catch_code_errors then try else (fn f => SOME o f)
       
   477         val execute = dynamic_value_strict (false, opts)
   473           ((is_genuine, counterexample_of),
   478           ((is_genuine, counterexample_of),
   474             (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample"))
   479             (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample"))
   475           thy (apfst o Option.map o apsnd o map) (ensure_testable (finitize t'))
   480           thy (apfst o Option.map o apsnd o map)
   476       in
   481       in
   477         Quickcheck.Result
   482         case act execute (ensure_testable (finitize t')) of 
   478          {counterexample = counterexample_of counterexample,
   483           SOME (counterexample, result) =>
   479           evaluation_terms = Option.map (K []) counterexample,
   484             Quickcheck.Result
   480           timings = #timings (dest_result result), reports = #reports (dest_result result)}
   485              {counterexample = counterexample_of counterexample,
       
   486               evaluation_terms = Option.map (K []) counterexample,
       
   487               timings = #timings (dest_result result),
       
   488               reports = #reports (dest_result result)}
       
   489         | NONE =>
       
   490           (Quickcheck.message ctxt ("Conjecture is not executable with Quickcheck-narrowing");
       
   491            Quickcheck.empty_result)
   481       end
   492       end
   482   end;
   493   end;
   483 
   494 
   484 fun test_goals ctxt _ insts goals =
   495 fun test_goals ctxt catch_code_errors insts goals =
   485   if (not (getenv "ISABELLE_GHC" = "")) then
   496   if (not (getenv "ISABELLE_GHC" = "")) then
   486     let
   497     let
   487       val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-narrowing...")
   498       val _ = Quickcheck.message ctxt ("Testing conjecture with Quickcheck-narrowing...")
   488       val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
   499       val correct_inst_goals = Quickcheck_Common.instantiate_goals ctxt insts goals
   489     in
   500     in
   490       Quickcheck_Common.collect_results (test_term ctxt) (maps (map snd) correct_inst_goals) []
   501       Quickcheck_Common.collect_results (test_term ctxt catch_code_errors)
       
   502         (maps (map snd) correct_inst_goals) []
   491     end
   503     end
   492   else
   504   else
   493     (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message
   505     (if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message
   494       ("Environment variable ISABELLE_GHC is not set. To use narrowing-based quickcheck, please set "
   506       ("Environment variable ISABELLE_GHC is not set. To use narrowing-based quickcheck, please set "
   495         ^ "this variable to your GHC Haskell compiler in your settings file. "
   507         ^ "this variable to your GHC Haskell compiler in your settings file. "