87 fun remove_pointless_clauses intro = |
87 fun remove_pointless_clauses intro = |
88 if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then |
88 if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then |
89 [] |
89 [] |
90 else [intro] |
90 else [intro] |
91 |
91 |
|
92 |
|
93 fun print_intross thy msg intross = |
|
94 tracing (msg ^ |
|
95 (space_implode "; " (map |
|
96 (fn intros => commas (map (Display.string_of_thm_global thy) intros)) intross))) |
|
97 |
|
98 |
92 fun preprocess_strong_conn_constnames gr constnames thy = |
99 fun preprocess_strong_conn_constnames gr constnames thy = |
93 let |
100 let |
94 val get_specs = map (fn k => (k, Graph.get_node gr k)) |
101 val get_specs = map (fn k => (k, Graph.get_node gr k)) |
95 val _ = priority ("Preprocessing scc of " ^ commas constnames) |
102 val _ = priority ("Preprocessing scc of " ^ commas constnames) |
96 val (prednames, funnames) = List.partition (is_pred thy) constnames |
103 val (prednames, funnames) = List.partition (is_pred thy) constnames |
101 thy |> not (null funnames) ? Predicate_Compile_Fun.define_predicates |
108 thy |> not (null funnames) ? Predicate_Compile_Fun.define_predicates |
102 (get_specs funnames) |
109 (get_specs funnames) |
103 val _ = priority "Compiling predicates to flat introrules..." |
110 val _ = priority "Compiling predicates to flat introrules..." |
104 val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess |
111 val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess |
105 (get_specs prednames) thy') |
112 (get_specs prednames) thy') |
106 val _ = tracing ("Flattened introduction rules: " ^ |
113 val _ = print_intross thy'' "Flattened introduction rules: " intross1 |
107 commas (map (Display.string_of_thm_global thy'') (flat intross1))) |
|
108 val _ = priority "Replacing functions in introrules..." |
114 val _ = priority "Replacing functions in introrules..." |
109 (* val _ = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross *) |
115 (* val _ = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross *) |
110 val intross2 = |
116 val intross2 = |
111 if fail_safe_mode then |
117 if fail_safe_mode then |
112 case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of |
118 case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of |
113 SOME intross => intross |
119 SOME intross => intross |
114 | NONE => let val _ = warning "Function replacement failed!" in intross1 end |
120 | NONE => let val _ = warning "Function replacement failed!" in intross1 end |
115 else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1 |
121 else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1 |
116 val _ = tracing ("Introduction rules with replaced functions: " ^ |
122 val _ = print_intross thy'' "Introduction rules with replaced functions: " intross2 |
117 commas (map (Display.string_of_thm_global thy'') (flat intross2))) |
123 val intross3 = map (maps remove_pointless_clauses) intross2 |
118 val intross3 = burrow (maps remove_pointless_clauses) intross2 |
124 val _ = print_intross thy'' "After removing pointless clauses: " intross3 |
119 val intross4 = burrow (map (AxClass.overload thy'')) intross3 |
125 val intross4 = burrow (map (AxClass.overload thy'')) intross3 |
120 val intross5 = burrow (map (simplify_fst_snd o expand_tuples thy'')) intross4 |
126 val intross5 = burrow (map (simplify_fst_snd o expand_tuples thy'')) intross4 |
|
127 val _ = print_intross thy'' "introduction rules before registering: " intross5 |
121 val _ = priority "Registering intro rules..." |
128 val _ = priority "Registering intro rules..." |
122 val thy''' = fold Predicate_Compile_Core.register_intros intross5 thy'' |
129 val thy''' = fold Predicate_Compile_Core.register_intros intross5 thy'' |
123 in |
130 in |
124 thy''' |
131 thy''' |
125 end; |
132 end; |