# HG changeset patch # User haftmann # Date 1423137672 -3600 # Node ID 74f638efffcb85cbfcf6c0380948cefdf8a7dddb # Parent 61d6d5cbbcd3b820205eee4b2b4f684ea564a3bb dropped dead code; tuned diff -r 61d6d5cbbcd3 -r 74f638efffcb src/HOL/Tools/Predicate_Compile/core_data.ML --- a/src/HOL/Tools/Predicate_Compile/core_data.ML Thu Feb 05 13:01:12 2015 +0100 +++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Thu Feb 05 13:01:12 2015 +0100 @@ -230,7 +230,7 @@ fun PEEK f dependent_tactic st = dependent_tactic (f st) st fun meta_eq_of th = th RS @{thm eq_reflection} val tuple_rew_rules = map meta_eq_of [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}] - fun instantiate i n {context, params, prems, asms, concl, schematics} = + fun instantiate i n {prems, ...} = let fun term_pair_of (ix, (ty,t)) = (Var (ix,ty), t) fun inst_of_matches tts = fold (Pattern.match thy) tts (Vartab.empty, Vartab.empty) diff -r 61d6d5cbbcd3 -r 74f638efffcb src/HOL/Tools/Predicate_Compile/mode_inference.ML --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Thu Feb 05 13:01:12 2015 +0100 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Thu Feb 05 13:01:12 2015 +0100 @@ -198,13 +198,6 @@ in (v, (s :: names, HOLogic.mk_eq (v, t) :: eqs)) end -(* - if is_constrt thy t then (t, (names, eqs)) else - let - val s = singleton (Name.variant_list names) "x" - val v = Free (s, fastype_of t) - in (v, (s::names, HOLogic.mk_eq (v, t)::eqs)) end; -*) fun is_possible_output ctxt vs t = forall @@ -250,21 +243,6 @@ (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2)) (derivations_of ctxt modes vs t1 m1) (derivations_of ctxt modes vs t2 m2) | derivations_of ctxt modes vs t (m as Fun _) = - (*let - val (p, args) = strip_comb t - in - (case lookup_mode modes p of - SOME ms => map_filter (fn (Context m, []) => let - val ms = strip_fun_mode m - val (argms, restms) = chop (length args) ms - val m' = fold_rev (curry Fun) restms Bool - in - if forall (fn m => eq_mode (Input, m)) argms andalso eq_mode (m', mode) then - SOME (fold (curry Mode_App) (map Term argms) (Context m), missing_vars vs t) - else NONE - end) ms - | NONE => (if is_all_input mode then [(Context mode, [])] else [])) - end*) (case try (all_derivations_of ctxt modes vs) t of SOME derivs => filter (fn (d, _) => eq_mode (mode_of d, m) andalso null (output_terms (t, d))) derivs @@ -361,7 +339,7 @@ (* prefer recursive calls *) fun is_rec_premise t = case fst (strip_comb t) of Const (c, _) => c = pred | _ => false - fun recursive_ord ((t1, _, _), (t2, deriv2, _)) = + fun recursive_ord ((t1, _, _), (t2, _, _)) = int_ord (if is_rec_premise t1 then 0 else 1, if is_rec_premise t2 then 0 else 1) val ord = lexl_ord [mvars_ord, fun_ord, random_mode_ord, output_mode_ord, recursive_ord] @@ -397,7 +375,7 @@ val vTs = distinct (op =) (fold Term.add_frees (map dest_indprem ps) (fold Term.add_frees ts [])) val modes' = modes @ (param_vs ~~ map (fn x => [((true, x), false), ((false, x), false)]) (ho_arg_modes_of mode)) fun retrieve_modes_of_pol pol = map (fn (s, ms) => - (s, map_filter (fn ((p, m), _) => if p = pol then SOME m else NONE | _ => NONE) ms)) + (s, map_filter (fn ((p, m), _) => if p = pol then SOME m else NONE) ms)) val (pos_modes', neg_modes') = if #infer_pos_and_neg_modes mode_analysis_options then (retrieve_modes_of_pol pol modes', retrieve_modes_of_pol (not pol) modes') @@ -512,9 +490,8 @@ fun infer_modes mode_analysis_options options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses = let - fun add_needs_random s (false, m) = ((false, m), false) - | add_needs_random s (true, m) = ((true, m), needs_random s m) - fun add_polarity_and_random_bit s b ms = map (fn m => add_needs_random s (b, m)) ms + fun add_polarity_and_random_bit s b = + map (fn m => ((b, m), b andalso needs_random s m)) val prednames = map fst preds (* extramodes contains all modes of all constants, should we only use the necessary ones - what is the impact on performance? *)