1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 10 10:21:25 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 10 10:59:07 2010 +0200
     1.3 @@ -73,9 +73,12 @@
     1.4    type 'a pred_mode_table = (string * ((bool * mode) * 'a) list) list
     1.5  
     1.6    val infer_modes : 
     1.7 -    mode_analysis_options -> options -> compilation -> (string * typ) list -> (string * mode list) list ->
     1.8 -      string list -> (string *  (Term.term list * Predicate_Compile_Aux.indprem list) list) list ->
     1.9 -      theory -> ((moded_clause list pred_mode_table * string list) * theory)
    1.10 +    mode_analysis_options -> options ->
    1.11 +     (string -> Predicate_Compile_Aux.mode list) * (string -> Predicate_Compile_Aux.mode list)
    1.12 +       * (string -> Predicate_Compile_Aux.mode -> bool) -> Proof.context -> (string * typ) list ->
    1.13 +      (string * mode list) list ->
    1.14 +      string list -> (string * (Term.term list * Predicate_Compile_Aux.indprem list) list) list ->
    1.15 +      ((moded_clause list pred_mode_table * (string * mode list) list) * string list)
    1.16  end;
    1.17  
    1.18  structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
    1.19 @@ -1498,13 +1501,13 @@
    1.20        cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map string_of_ext_mode ms)) modes))
    1.21    else ()
    1.22  
    1.23 -fun infer_modes mode_analysis_options options compilation preds all_modes param_vs clauses thy =
    1.24 +fun infer_modes mode_analysis_options options (lookup_mode, lookup_neg_mode, needs_random) ctxt
    1.25 +  preds all_modes param_vs clauses =
    1.26    let
    1.27 -    val ctxt = ProofContext.init_global thy  
    1.28      val collect_errors = false
    1.29      fun appair f (x1, x2) (y1, y2) = (f x1 y1, f x2 y2)
    1.30      fun add_needs_random s (false, m) = ((false, m), false)
    1.31 -      | add_needs_random s (true, m) = ((true, m), needs_random ctxt s m)
    1.32 +      | add_needs_random s (true, m) = ((true, m), needs_random s m)
    1.33      fun add_polarity_and_random_bit s b ms = map (fn m => add_needs_random s (b, m)) ms
    1.34      val prednames = map fst preds
    1.35      (* extramodes contains all modes of all constants, should we only use the necessary ones
    1.36 @@ -1516,18 +1519,16 @@
    1.37        | predname_of _ = I
    1.38      val relevant_prednames = fold (fn (_, clauses') =>
    1.39        fold (fn (_, ps) => fold Term.add_const_names (map dest_indprem ps)) clauses') clauses []
    1.40 +      |> filter_out (fn name => member (op =) prednames name)
    1.41      val extra_modes =
    1.42        if #infer_pos_and_neg_modes mode_analysis_options then
    1.43          let
    1.44            val pos_extra_modes =
    1.45 -            map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
    1.46 +            map_filter (fn name => Option.map (pair name) (try lookup_mode name))
    1.47              relevant_prednames
    1.48 -            |> filter_out (fn (name, _) => member (op =) prednames name)
    1.49            val neg_extra_modes =
    1.50 -          map_filter (fn name => Option.map (pair name)
    1.51 -            (try (modes_of (negative_compilation_of compilation) ctxt) name))
    1.52 -            relevant_prednames
    1.53 -            |> filter_out (fn (name, _) => member (op =) prednames name)
    1.54 +            map_filter (fn name => Option.map (pair name) (try lookup_neg_mode name))
    1.55 +              relevant_prednames
    1.56          in
    1.57            map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)
    1.58                  @ add_polarity_and_random_bit s false (the (AList.lookup (op =) neg_extra_modes s))))
    1.59 @@ -1535,9 +1536,8 @@
    1.60          end
    1.61        else
    1.62          map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)))
    1.63 -          (map_filter (fn name => Option.map (pair name) (try (modes_of compilation ctxt) name))
    1.64 -            relevant_prednames
    1.65 -          |> filter_out (fn (name, _) => member (op =) prednames name))
    1.66 +          (map_filter (fn name => Option.map (pair name) (try lookup_mode name))
    1.67 +            relevant_prednames)
    1.68      val _ = print_extra_modes options extra_modes
    1.69      val start_modes =
    1.70        if #infer_pos_and_neg_modes mode_analysis_options then
    1.71 @@ -1559,11 +1559,11 @@
    1.72            (fixp (fn modes => map fst (iteration modes)) start_modes, []))
    1.73      val moded_clauses = map (get_modes_pred' mode_analysis_options ctxt param_vs clauses
    1.74        (modes @ extra_modes)) modes
    1.75 -    val thy' = fold (fn (s, ms) => if member (op =) (map fst preds) s then
    1.76 -      set_needs_random s (map_filter (fn ((true, m), true) => SOME m | _ => NONE) ms) else I)
    1.77 -      modes thy
    1.78 +    val need_random = fold (fn (s, ms) => if member (op =) (map fst preds) s then
    1.79 +      cons (s, (map_filter (fn ((true, m), true) => SOME m | _ => NONE) ms)) else I)
    1.80 +      modes []
    1.81    in
    1.82 -    ((moded_clauses, errors), thy')
    1.83 +    ((moded_clauses, need_random), errors)
    1.84    end;
    1.85  
    1.86  (* term construction *)
    1.87 @@ -2845,10 +2845,13 @@
    1.88      val (preds, all_vs, param_vs, all_modes, clauses) =
    1.89        prepare_intrs options compilation thy prednames (maps (intros_of ctxt) prednames)
    1.90      val _ = print_step options "Infering modes..."
    1.91 -    val ((moded_clauses, errors), thy') =
    1.92 +    val (lookup_mode, lookup_neg_mode, needs_random) = (modes_of compilation ctxt,
    1.93 +      modes_of (negative_compilation_of compilation) ctxt, needs_random ctxt)
    1.94 +    val ((moded_clauses, needs_random), errors) =
    1.95        Output.cond_timeit (!Quickcheck.timing) "Infering modes"
    1.96        (fn _ => infer_modes mode_analysis_options
    1.97 -        options compilation preds all_modes param_vs clauses thy)
    1.98 +        options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses)
    1.99 +    val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random thy
   1.100      val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
   1.101      val _ = check_expected_modes preds options modes
   1.102      val _ = check_proposed_modes preds options modes errors