src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 36027 29a15da9c63d
parent 36025 d25043e7843f
child 36028 3837493fe4ab
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:43 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 17:30:45 2010 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4    val code_pred : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
     1.5    val code_pred_cmd : Predicate_Compile_Aux.options -> string -> Proof.context -> Proof.state
     1.6    val values_cmd : string list -> Predicate_Compile_Aux.mode option list option
     1.7 -    -> (string option * (Predicate_Compile_Aux.compilation * int list))
     1.8 +    -> ((string option * bool) * (Predicate_Compile_Aux.compilation * int list))
     1.9      -> int -> string -> Toplevel.state -> unit
    1.10    val register_predicate : (string * thm list * thm) -> theory -> theory
    1.11    val register_intros : string * thm list -> theory -> theory
    1.12 @@ -42,6 +42,9 @@
    1.13    val new_random_dseq_eval_ref :
    1.14      (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence)
    1.15        option Unsynchronized.ref
    1.16 +  val new_random_dseq_stats_eval_ref :
    1.17 +    (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence)
    1.18 +      option Unsynchronized.ref
    1.19    val code_pred_intro_attrib : attribute
    1.20    
    1.21    (* used by Quickcheck_Generator *) 
    1.22 @@ -3136,6 +3139,9 @@
    1.23    Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) option);
    1.24  val new_random_dseq_eval_ref =
    1.25    Unsynchronized.ref (NONE : (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) option)
    1.26 +val new_random_dseq_stats_eval_ref =
    1.27 +    Unsynchronized.ref (NONE :
    1.28 +      (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) option)
    1.29  
    1.30  (*FIXME turn this into an LCF-guarded preprocessor for comprehensions*)
    1.31  fun analyze_compr thy compfuns param_user_modes (compilation, arguments) t_compr =
    1.32 @@ -3227,8 +3233,14 @@
    1.33        error "Evaluation with values is not possible because compilation with code_pred was not invoked"
    1.34    end
    1.35  
    1.36 -fun eval thy param_user_modes (options as (compilation, arguments)) k t_compr =
    1.37 +fun eval thy stats param_user_modes (options as (compilation, arguments)) k t_compr =
    1.38    let
    1.39 +    fun count xs x =
    1.40 +      let
    1.41 +        fun count' i [] = i
    1.42 +          | count' i (x' :: xs) = if x = x' then count' (i + 1) xs else count' i xs
    1.43 +      in count' 0 xs end
    1.44 +    fun accumulate xs = map (fn x => (x, count xs x)) (sort int_ord (distinct (op =) xs))
    1.45      val compfuns =
    1.46        case compilation of
    1.47          Random => PredicateCompFuns.compfuns
    1.48 @@ -3236,11 +3248,16 @@
    1.49        | Pos_Random_DSeq => Random_Sequence_CompFuns.compfuns
    1.50        | New_Pos_Random_DSeq => New_Pos_Random_Sequence_CompFuns.compfuns
    1.51        | _ => PredicateCompFuns.compfuns
    1.52 -      
    1.53      val t = analyze_compr thy compfuns param_user_modes options t_compr;
    1.54      val T = dest_predT compfuns (fastype_of t);
    1.55 -    val t' = mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t;
    1.56 -    val ts =
    1.57 +    val t' =
    1.58 +      if stats andalso compilation = New_Pos_Random_DSeq then
    1.59 +        mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ code_numeral}))
    1.60 +          (absdummy (T, HOLogic.mk_prod (HOLogic.term_of_const T $ Bound 0,
    1.61 +            @{term Code_Numeral.of_nat} $ (HOLogic.size_const T $ Bound 0)))) t
    1.62 +      else
    1.63 +        mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
    1.64 +    val (ts, statistics) =
    1.65        case compilation of
    1.66         (* Random =>
    1.67            fst (Predicate.yieldn k
    1.68 @@ -3251,39 +3268,48 @@
    1.69            let
    1.70              val [nrandom, size, depth] = arguments
    1.71            in
    1.72 -            fst (DSequence.yieldn k
    1.73 +            rpair NONE (fst (DSequence.yieldn k
    1.74                (Code_Eval.eval NONE ("Predicate_Compile_Core.random_dseq_eval_ref", random_dseq_eval_ref)
    1.75                  (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
    1.76                    thy t' [] nrandom size
    1.77                  |> Random_Engine.run)
    1.78 -              depth true)
    1.79 +              depth true))
    1.80            end
    1.81        | DSeq =>
    1.82 -          fst (DSequence.yieldn k
    1.83 +          rpair NONE (fst (DSequence.yieldn k
    1.84              (Code_Eval.eval NONE ("Predicate_Compile_Core.dseq_eval_ref", dseq_eval_ref)
    1.85 -              DSequence.map thy t' []) (the_single arguments) true)
    1.86 +              DSequence.map thy t' []) (the_single arguments) true))
    1.87        | New_Pos_Random_DSeq =>
    1.88            let
    1.89              val [nrandom, size, depth] = arguments
    1.90              val seed = Random_Engine.next_seed ()
    1.91            in
    1.92 -            fst (Lazy_Sequence.yieldn k
    1.93 -              (Code_Eval.eval NONE
    1.94 -                ("Predicate_Compile_Core.new_random_dseq_eval_ref", new_random_dseq_eval_ref)
    1.95 -                (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
    1.96 -                  |> Lazy_Sequence.map proc)
    1.97 -                  thy t' [] nrandom size seed depth))
    1.98 +            if stats then
    1.99 +              apsnd (SOME o accumulate) (split_list
   1.100 +              (fst (Lazy_Sequence.yieldn k
   1.101 +                (Code_Eval.eval NONE
   1.102 +                  ("Predicate_Compile_Core.new_random_dseq_stats_eval_ref", new_random_dseq_stats_eval_ref)
   1.103 +                  (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
   1.104 +                    |> Lazy_Sequence.map (apfst proc))
   1.105 +                    thy t' [] nrandom size seed depth))))
   1.106 +            else rpair NONE
   1.107 +              (fst (Lazy_Sequence.yieldn k
   1.108 +                (Code_Eval.eval NONE
   1.109 +                  ("Predicate_Compile_Core.new_random_dseq_eval_ref", new_random_dseq_eval_ref)
   1.110 +                  (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
   1.111 +                    |> Lazy_Sequence.map proc)
   1.112 +                    thy t' [] nrandom size seed depth)))
   1.113            end
   1.114        | _ =>
   1.115 -          fst (Predicate.yieldn k
   1.116 +          rpair NONE (fst (Predicate.yieldn k
   1.117              (Code_Eval.eval NONE ("Predicate_Compile_Core.eval_ref", eval_ref)
   1.118 -              Predicate.map thy t' []))
   1.119 -  in (T, ts) end;
   1.120 -
   1.121 -fun values ctxt param_user_modes (raw_expected, comp_options) k t_compr =
   1.122 +              Predicate.map thy t' [])))
   1.123 +  in ((T, ts), statistics) end;
   1.124 +
   1.125 +fun values ctxt param_user_modes ((raw_expected, stats), comp_options) k t_compr =
   1.126    let
   1.127      val thy = ProofContext.theory_of ctxt
   1.128 -    val (T, ts) = eval thy param_user_modes comp_options k t_compr
   1.129 +    val ((T, ts), statistics) = eval thy stats param_user_modes comp_options k t_compr
   1.130      val setT = HOLogic.mk_setT T
   1.131      val elems = HOLogic.mk_set T ts
   1.132      val cont = Free ("...", setT)
   1.133 @@ -3298,20 +3324,36 @@
   1.134              "expected values: " ^ Syntax.string_of_term ctxt (Syntax.read_term ctxt s) ^ "\n" ^
   1.135              "computed values: " ^ Syntax.string_of_term ctxt elems ^ "\n")
   1.136    in
   1.137 -    if k = ~1 orelse length ts < k then elems
   1.138 -      else Const (@{const_abbrev Set.union}, setT --> setT --> setT) $ elems $ cont
   1.139 +    (if k = ~1 orelse length ts < k then elems
   1.140 +    else Const (@{const_abbrev Set.union}, setT --> setT --> setT) $ elems $ cont, statistics)
   1.141    end;
   1.142  
   1.143  fun values_cmd print_modes param_user_modes options k raw_t state =
   1.144    let
   1.145      val ctxt = Toplevel.context_of state
   1.146      val t = Syntax.read_term ctxt raw_t
   1.147 -    val t' = values ctxt param_user_modes options k t
   1.148 +    val (t', stats) = values ctxt param_user_modes options k t
   1.149      val ty' = Term.type_of t'
   1.150      val ctxt' = Variable.auto_fixes t' ctxt
   1.151 +    val pretty_stat =
   1.152 +      case stats of
   1.153 +          NONE => []
   1.154 +        | SOME xs =>
   1.155 +          let
   1.156 +            val total = fold (curry (op +)) (map snd xs) 0
   1.157 +            fun pretty_entry (s, n) =
   1.158 +              [Pretty.str "size", Pretty.brk 1,
   1.159 +               Pretty.str (string_of_int s), Pretty.str ":", Pretty.brk 1,
   1.160 +               Pretty.str (string_of_int n), Pretty.fbrk]
   1.161 +          in
   1.162 +            [Pretty.fbrk, Pretty.str "Statistics:", Pretty.fbrk,
   1.163 +             Pretty.str "total:", Pretty.brk 1, Pretty.str (string_of_int total), Pretty.fbrk]
   1.164 +             @ maps pretty_entry xs
   1.165 +          end
   1.166      val p = PrintMode.with_modes print_modes (fn () =>
   1.167 -      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
   1.168 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   1.169 +      Pretty.block ([Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
   1.170 +        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]
   1.171 +        @ pretty_stat)) ();
   1.172    in Pretty.writeln p end;
   1.173  
   1.174  end;