only add relevant predicates to the list of extra modes
authorbulwahn
Wed Apr 21 12:10:52 2010 +0200 (2010-04-21)
changeset 362515fd5d732a4ea
parent 36250 ad558b642a15
child 36252 beba03215d8f
only add relevant predicates to the list of extra modes
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Apr 21 12:10:52 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Apr 21 12:10:52 2010 +0200
     1.3 @@ -38,6 +38,7 @@
     1.4    (* premises *)
     1.5    datatype indprem = Prem of term | Negprem of term | Sidecond of term
     1.6      | Generator of (string * typ)
     1.7 +  val dest_indprem : indprem -> term
     1.8    (* general syntactic functions *)
     1.9    val conjuncts : term -> term list
    1.10    val is_equationlike : thm -> bool
    1.11 @@ -388,6 +389,11 @@
    1.12  datatype indprem = Prem of term | Negprem of term | Sidecond of term
    1.13    | Generator of (string * typ);
    1.14  
    1.15 +fun dest_indprem (Prem t) = t
    1.16 +  | dest_indprem (Negprem t) = t
    1.17 +  | dest_indprem (Sidecond t) = t
    1.18 +  | dest_indprem (Generator _) = raise Fail "cannot destruct generator"
    1.19 +
    1.20  (* general syntactic functions *)
    1.21  
    1.22  (*Like dest_conj, but flattens conjunctions however nested*)
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 21 12:10:52 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 21 12:10:52 2010 +0200
     2.3 @@ -1485,13 +1485,26 @@
     2.4      val prednames = map fst preds
     2.5      (* extramodes contains all modes of all constants, should we only use the necessary ones
     2.6         - what is the impact on performance? *)
     2.7 +    fun predname_of (Prem t) =
     2.8 +        (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
     2.9 +      | predname_of (Negprem t) =
    2.10 +        (case try dest_Const (fst (strip_comb t)) of SOME (c, _) => insert (op =) c | NONE => I)
    2.11 +      | predname_of _ = I
    2.12 +    val relevant_prednames = fold (fn (_, clauses') =>
    2.13 +      fold (fn (_, ps) => fold Term.add_const_names (map dest_indprem ps)) clauses') clauses []
    2.14      val extra_modes =
    2.15        if #infer_pos_and_neg_modes mode_analysis_options then
    2.16          let
    2.17            val pos_extra_modes =
    2.18 -            all_modes_of compilation thy |> filter_out (fn (name, _) => member (op =) prednames name)
    2.19 +            map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
    2.20 +            relevant_prednames
    2.21 +            (* all_modes_of compilation thy *)
    2.22 +            |> filter_out (fn (name, _) => member (op =) prednames name)
    2.23            val neg_extra_modes =
    2.24 -            all_modes_of (negative_compilation_of compilation) thy
    2.25 +          map_filter (fn name => Option.map (pair name)
    2.26 +            (try (modes_of (negative_compilation_of compilation) thy) name))
    2.27 +            relevant_prednames
    2.28 +          (*all_modes_of (negative_compilation_of compilation) thy*)
    2.29              |> filter_out (fn (name, _) => member (op =) prednames name)
    2.30          in
    2.31            map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)
    2.32 @@ -1500,7 +1513,10 @@
    2.33          end
    2.34        else
    2.35          map (fn (s, ms) => (s, (add_polarity_and_random_bit s true ms)))
    2.36 -          (all_modes_of compilation thy |> filter_out (fn (name, _) => member (op =) prednames name))
    2.37 +          (map_filter (fn name => Option.map (pair name) (try (modes_of compilation thy) name))
    2.38 +            relevant_prednames
    2.39 +          (*all_modes_of compilation thy*)
    2.40 +          |> filter_out (fn (name, _) => member (op =) prednames name))
    2.41      val _ = print_extra_modes options extra_modes
    2.42      val start_modes =
    2.43        if #infer_pos_and_neg_modes mode_analysis_options then
    2.44 @@ -2639,9 +2655,9 @@
    2.45        prepare_intrs options compilation thy prednames (maps (intros_of thy) prednames)
    2.46      val _ = print_step options "Infering modes..."
    2.47      val ((moded_clauses, errors), thy') =
    2.48 -      (*Output.cond_timeit true "Infering modes"
    2.49 -      (fn _ =>*) infer_modes mode_analysis_options
    2.50 -        options compilation preds all_modes param_vs clauses thy
    2.51 +      Output.cond_timeit true "Infering modes"
    2.52 +      (fn _ => infer_modes mode_analysis_options
    2.53 +        options compilation preds all_modes param_vs clauses thy)
    2.54      val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
    2.55      val _ = check_expected_modes preds options modes
    2.56      (*val _ = check_proposed_modes preds options modes (fst extra_modes) errors*)