src/HOL/Tools/smallvalue_generators.ML
changeset 41903 39fd77f0ae59
parent 41902 1941b3315952
child 41904 2ae19825f7b6
equal deleted inserted replaced
41902:1941b3315952 41903:39fd77f0ae59
    13   val put_counterexample: (unit -> int -> term list option)
    13   val put_counterexample: (unit -> int -> term list option)
    14     -> Proof.context -> Proof.context
    14     -> Proof.context -> Proof.context
    15   val put_counterexample_batch: (unit -> (int -> term list option) list)
    15   val put_counterexample_batch: (unit -> (int -> term list option) list)
    16     -> Proof.context -> Proof.context
    16     -> Proof.context -> Proof.context
    17   val smart_quantifier : bool Config.T;
    17   val smart_quantifier : bool Config.T;
       
    18   val quickcheck_pretty : bool Config.T;
    18   val setup: theory -> theory
    19   val setup: theory -> theory
    19 end;
    20 end;
    20 
    21 
    21 structure Smallvalue_Generators : SMALLVALUE_GENERATORS =
    22 structure Smallvalue_Generators : SMALLVALUE_GENERATORS =
    22 struct
    23 struct
    28 (* dynamic options *)
    29 (* dynamic options *)
    29 
    30 
    30 val (smart_quantifier, setup_smart_quantifier) =
    31 val (smart_quantifier, setup_smart_quantifier) =
    31   Attrib.config_bool "quickcheck_smart_quantifier" (K true)
    32   Attrib.config_bool "quickcheck_smart_quantifier" (K true)
    32 
    33 
       
    34 val (quickcheck_pretty, setup_quickcheck_pretty) =
       
    35   Attrib.config_bool "quickcheck_pretty" (K true)
       
    36  
    33 (** general term functions **)
    37 (** general term functions **)
    34 
    38 
    35 fun mk_measure f =
    39 fun mk_measure f =
    36   let
    40   let
    37     val Type ("fun", [T, @{typ nat}]) = fastype_of f 
    41     val Type ("fun", [T, @{typ nat}]) = fastype_of f 
   334   | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
   338   | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
   335   | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
   339   | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
   336   
   340   
   337 fun post_process_term t =
   341 fun post_process_term t =
   338   let
   342   let
   339     (*val _ = tracing ("post_process:" ^ Syntax.string_of_term ctxt t)*)
   343     val _ = tracing (Syntax.string_of_term @{context} t)
   340     fun map_Abs f t =
   344     fun map_Abs f t =
   341       case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) 
   345       case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) 
   342     fun process_args t = case strip_comb t of
   346     fun process_args t = case strip_comb t of
   343       (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) 
   347       (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) 
   344   in
   348   in
   358                 (case t of
   362                 (case t of
   359                   Abs(_, _, Const(@{const_name None}, _)) => fst #> make_map T1 T2
   363                   Abs(_, _, Const(@{const_name None}, _)) => fst #> make_map T1 T2
   360                 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
   364                 | Abs(_, _, Const (@{const_name undefined}, _)) => fst #> make_map T1 T2
   361                 | _ => make_fun_upds T1 T2) 
   365                 | _ => make_fun_upds T1 T2) 
   362             | _ => make_fun_upds T1 T2)
   366             | _ => make_fun_upds T1 T2)
   363         | NONE => raise TERM ("post_process_term", [t]))
   367         | NONE => process_args t)
   364     | _ => process_args t
   368     | _ => process_args t
   365   end
   369   end
   366 
   370 
   367 (** generator compiliation **)
   371 (** generator compiliation **)
   368 
   372 
   374         ctxt t;
   378         ctxt t;
   375     val compile = Code_Runtime.dynamic_value_strict
   379     val compile = Code_Runtime.dynamic_value_strict
   376       (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
   380       (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
   377       thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
   381       thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
   378   in
   382   in
   379     fn size => rpair NONE (compile size |> Option.map (map post_process_term))
   383     fn size => rpair NONE (compile size |> 
       
   384       (if Config.get ctxt quickcheck_pretty then Option.map (map post_process_term) else I))
   380   end;
   385   end;
   381 
   386 
   382 fun compile_generator_exprs ctxt ts =
   387 fun compile_generator_exprs ctxt ts =
   383   let
   388   let
   384     val thy = ProofContext.theory_of ctxt
   389     val thy = ProofContext.theory_of ctxt
   399 
   404 
   400 val setup =
   405 val setup =
   401   Datatype.interpretation
   406   Datatype.interpretation
   402     (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
   407     (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
   403   #> setup_smart_quantifier
   408   #> setup_smart_quantifier
       
   409   #> setup_quickcheck_pretty
   404   #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
   410   #> Context.theory_map (Quickcheck.add_generator ("exhaustive", compile_generator_expr))
   405   #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs));
   411   #> Context.theory_map (Quickcheck.add_batch_generator ("exhaustive", compile_generator_exprs));
   406 
   412 
   407 end;
   413 end;