added statistics to values command for random generation
authorbulwahn
Mon Mar 29 17:30:45 2010 +0200 (2010-03-29)
changeset 3602729a15da9c63d
parent 36026 276ebec72082
child 36028 3837493fe4ab
added statistics to values command for random generation
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Mar 29 17:30:43 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Mar 29 17:30:45 2010 +0200
     1.3 @@ -235,6 +235,8 @@
     1.4  val opt_param_modes = Scan.optional (P.$$$ "[" |-- Args.$$$ "mode" |-- P.$$$ ":" |--
     1.5    P.enum ", " opt_mode --| P.$$$ "]" >> SOME) NONE
     1.6  
     1.7 +val stats = Scan.optional (Args.$$$ "stats" >> K true) false
     1.8 +
     1.9  val value_options =
    1.10    let
    1.11      val expected_values = Scan.optional (Args.$$$ "expected" |-- P.term >> SOME) NONE
    1.12 @@ -245,7 +247,8 @@
    1.13              compilation_names))
    1.14          (Pred, [])
    1.15    in
    1.16 -    Scan.optional (P.$$$ "[" |-- expected_values -- scan_compilation --| P.$$$ "]") (NONE, (Pred, []))
    1.17 +    Scan.optional (P.$$$ "[" |-- (expected_values -- stats) -- scan_compilation --| P.$$$ "]")
    1.18 +      ((NONE, false), (Pred, []))
    1.19    end
    1.20  
    1.21  (* code_pred command and values command *)
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:43 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:45 2010 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4    val code_pred : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
     2.5    val code_pred_cmd : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
     2.6    val values_cmd : string list -> Predicate_Compile_Aux.mode option list option
     2.7 -    -> (string option * (Predicate_Compile_Aux.compilation * int list))
     2.8 +    -> ((string option * bool) * (Predicate_Compile_Aux.compilation * int list))
     2.9      -> int -> string -> Toplevel.state -> unit
    2.10    val register_predicate : (string * thm list * thm) -> theory -> theory
    2.11    val register_intros : string * thm list -> theory -> theory
    2.12 @@ -42,6 +42,9 @@
    2.13    val new_random_dseq_eval_ref :
    2.14      (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence)
    2.15        option Unsynchronized.ref
    2.16 +  val new_random_dseq_stats_eval_ref :
    2.17 +    (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence)
    2.18 +      option Unsynchronized.ref
    2.19    val code_pred_intro_attrib : attribute
    2.20    
    2.21    (* used by Quickcheck_Generator *) 
    2.22 @@ -3136,6 +3139,9 @@
    2.23    Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) option);
    2.24  val new_random_dseq_eval_ref =
    2.25    Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) option)
    2.26 +val new_random_dseq_stats_eval_ref =
    2.27 +    Unsynchronized.ref (NONE :
    2.28 +      (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) option)
    2.29  
    2.30  (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
    2.31  fun analyze_compr thy compfuns param_user_modes (compilation, arguments) t_compr =
    2.32 @@ -3227,8 +3233,14 @@
    2.33        error "Evaluation with values is not possible because compilation with code_pred was not invoked"
    2.34    end
    2.35  
    2.36 -fun eval thy param_user_modes (options as (compilation, arguments)) k t_compr =
    2.37 +fun eval thy stats param_user_modes (options as (compilation, arguments)) k t_compr =
    2.38    let
    2.39 +    fun count xs x =
    2.40 +      let
    2.41 +        fun count' i [] = i
    2.42 +          | count' i (x' :: xs) = if x = x' then count' (i + 1) xs else count' i xs
    2.43 +      in count' 0 xs end
    2.44 +    fun accumulate xs = map (fn x => (x, count xs x)) (sort int_ord (distinct (op =) xs))
    2.45      val compfuns =
    2.46        case compilation of
    2.47          Random => PredicateCompFuns.compfuns
    2.48 @@ -3236,11 +3248,16 @@
    2.49        | Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns
    2.50        | New_Pos_Random_DSeq => New_Pos_Random_Sequence_CompFuns.compfuns
    2.51        | _ => PredicateCompFuns.compfuns
    2.52 -      
    2.53      val t = analyze_compr thy compfuns param_user_modes options t_compr;
    2.54      val T = dest_predT compfuns (fastype_of t);
    2.55 -    val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
    2.56 -    val ts =
    2.57 +    val t' =
    2.58 +      if stats andalso compilation = New_Pos_Random_DSeq then
    2.59 +        mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ code_numeral}))
    2.60 +          (absdummy (T, HOLogic.mk_prod (HOLogic.term_of_const T $ Bound 0,
    2.61 +            @{term Code_Numeral.of_nat} $ (HOLogic.size_const T $ Bound 0)))) t
    2.62 +      else
    2.63 +        mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
    2.64 +    val (ts, statistics) =
    2.65        case compilation of
    2.66         (* Random =>
    2.67            fst (Predicate.yieldn k
    2.68 @@ -3251,39 +3268,48 @@
    2.69            let
    2.70              val [nrandom, size, depth] = arguments
    2.71            in
    2.72 -            fst (DSequence.yieldn k
    2.73 +            rpair NONE (fst (DSequence.yieldn k
    2.74                (Code_Eval.eval NONE ("Predicate_Compile_Core.random_dseq_eval_ref", random_dseq_eval_ref)
    2.75                  (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
    2.76                    thy t' [] nrandom size
    2.77                  |> Random_Engine.run)
    2.78 -              depth true)
    2.79 +              depth true))
    2.80            end
    2.81        | DSeq =>
    2.82 -          fst (DSequence.yieldn k
    2.83 +          rpair NONE (fst (DSequence.yieldn k
    2.84              (Code_Eval.eval NONE ("Predicate_Compile_Core.dseq_eval_ref", dseq_eval_ref)
    2.85 -              DSequence.map thy t' []) (the_single arguments) true)
    2.86 +              DSequence.map thy t' []) (the_single arguments) true))
    2.87        | New_Pos_Random_DSeq =>
    2.88            let
    2.89              val [nrandom, size, depth] = arguments
    2.90              val seed = Random_Engine.next_seed ()
    2.91            in
    2.92 -            fst (Lazy_Sequence.yieldn k
    2.93 -              (Code_Eval.eval NONE
    2.94 -                ("Predicate_Compile_Core.new_random_dseq_eval_ref", new_random_dseq_eval_ref)
    2.95 -                (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
    2.96 -                  |> Lazy_Sequence.map proc)
    2.97 -                  thy t' [] nrandom size seed depth))
    2.98 +            if stats then
    2.99 +              apsnd (SOME o accumulate) (split_list
   2.100 +              (fst (Lazy_Sequence.yieldn k
   2.101 +                (Code_Eval.eval NONE
   2.102 +                  ("Predicate_Compile_Core.new_random_dseq_stats_eval_ref", new_random_dseq_stats_eval_ref)
   2.103 +                  (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
   2.104 +                    |> Lazy_Sequence.map (apfst proc))
   2.105 +                    thy t' [] nrandom size seed depth))))
   2.106 +            else rpair NONE
   2.107 +              (fst (Lazy_Sequence.yieldn k
   2.108 +                (Code_Eval.eval NONE
   2.109 +                  ("Predicate_Compile_Core.new_random_dseq_eval_ref", new_random_dseq_eval_ref)
   2.110 +                  (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
   2.111 +                    |> Lazy_Sequence.map proc)
   2.112 +                    thy t' [] nrandom size seed depth)))
   2.113            end
   2.114        | _ =>
   2.115 -          fst (Predicate.yieldn k
   2.116 +          rpair NONE (fst (Predicate.yieldn k
   2.117              (Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref)
   2.118 -              Predicate.map thy t' []))
   2.119 -  in (T, ts) end;
   2.120 -
   2.121 -fun values ctxt param_user_modes (raw_expected, comp_options) k t_compr =
   2.122 +              Predicate.map thy t' [])))
   2.123 +  in ((T, ts), statistics) end;
   2.124 +
   2.125 +fun values ctxt param_user_modes ((raw_expected, stats), comp_options) k t_compr =
   2.126    let
   2.127      val thy = ProofContext.theory_of ctxt
   2.128 -    val (T, ts) = eval thy param_user_modes comp_options k t_compr
   2.129 +    val ((T, ts), statistics) = eval thy stats param_user_modes comp_options k t_compr
   2.130      val setT = HOLogic.mk_setT T
   2.131      val elems = HOLogic.mk_set T ts
   2.132      val cont = Free ("...", setT)
   2.133 @@ -3298,20 +3324,36 @@
   2.134              "expected values: " ^ Syntax.string_of_term ctxt (Syntax.read_term ctxt s) ^ "\n" ^
   2.135              "computed values: " ^ Syntax.string_of_term ctxt elems ^ "\n")
   2.136    in
   2.137 -    if k = ~1 orelse length ts < k then elems
   2.138 -      else Const (@{const_abbrev Set.union}, setT --> setT --> setT) $ elems $ cont
   2.139 +    (if k = ~1 orelse length ts < k then elems
   2.140 +    else Const (@{const_abbrev Set.union}, setT --> setT --> setT) $ elems $ cont, statistics)
   2.141    end;
   2.142  
   2.143  fun values_cmd print_modes param_user_modes options k raw_t state =
   2.144    let
   2.145      val ctxt = Toplevel.context_of state
   2.146      val t = Syntax.read_term ctxt raw_t
   2.147 -    val t' = values ctxt param_user_modes options k t
   2.148 +    val (t', stats) = values ctxt param_user_modes options k t
   2.149      val ty' = Term.type_of t'
   2.150      val ctxt' = Variable.auto_fixes t' ctxt
   2.151 +    val pretty_stat =
   2.152 +      case stats of
   2.153 +          NONE => []
   2.154 +        | SOME xs =>
   2.155 +          let
   2.156 +            val total = fold (curry (op +)) (map snd xs) 0
   2.157 +            fun pretty_entry (s, n) =
   2.158 +              [Pretty.str "size", Pretty.brk 1,
   2.159 +               Pretty.str (string_of_int s), Pretty.str ":", Pretty.brk 1,
   2.160 +               Pretty.str (string_of_int n), Pretty.fbrk]
   2.161 +          in
   2.162 +            [Pretty.fbrk, Pretty.str "Statistics:", Pretty.fbrk,
   2.163 +             Pretty.str "total:", Pretty.brk 1, Pretty.str (string_of_int total), Pretty.fbrk]
   2.164 +             @ maps pretty_entry xs
   2.165 +          end
   2.166      val p = PrintMode.with_modes print_modes (fn () =>
   2.167 -      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
   2.168 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   2.169 +      Pretty.block ([Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
   2.170 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]
   2.171 +        @ pretty_stat)) ();
   2.172    in Pretty.writeln p end;
   2.173  
   2.174  end;