equal
deleted
inserted
replaced
1 (* Author: Lukas Bulwahn, TU Muenchen |
1 (* Author: Lukas Bulwahn, TU Muenchen |
2 |
2 |
3 Book-keeping datastructure for the predicate compiler |
3 Book-keeping datastructure for the predicate compiler |
4 |
4 |
5 *) |
5 *) |
6 signature PRED_COMPILE_DATA = |
6 signature PREDICATE_COMPILE_DATA = |
7 sig |
7 sig |
8 type specification_table; |
8 type specification_table; |
9 val make_const_spec_table : theory -> specification_table |
9 val make_const_spec_table : theory -> specification_table |
10 val get_specification : specification_table -> string -> thm list |
10 val get_specification : specification_table -> string -> thm list |
11 val obtain_specification_graph : theory -> specification_table -> string -> thm list Graph.T |
11 val obtain_specification_graph : theory -> specification_table -> string -> thm list Graph.T |
12 val normalize_equation : theory -> thm -> thm |
12 val normalize_equation : theory -> thm -> thm |
13 end; |
13 end; |
14 |
14 |
15 structure Pred_Compile_Data : PRED_COMPILE_DATA = |
15 structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA = |
16 struct |
16 struct |
17 |
17 |
18 open Predicate_Compile_Aux; |
18 open Predicate_Compile_Aux; |
19 |
19 |
20 structure Data = TheoryDataFun |
20 structure Data = TheoryDataFun |
117 th''' |
117 th''' |
118 end; |
118 end; |
119 |
119 |
120 fun normalize_equation thy th = |
120 fun normalize_equation thy th = |
121 mk_meta_equation th |
121 mk_meta_equation th |
122 |> Pred_Compile_Set.unfold_set_notation |
122 |> Predicate_Compile_Set.unfold_set_notation |
123 |> full_fun_cong_expand |
123 |> full_fun_cong_expand |
124 |> split_all_pairs thy |
124 |> split_all_pairs thy |
125 |> tap check_equation_format |
125 |> tap check_equation_format |
126 |
126 |
127 fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite |
127 fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite |
129 |
129 |
130 fun store_thm_in_table ignore_consts thy th= |
130 fun store_thm_in_table ignore_consts thy th= |
131 let |
131 let |
132 val th = th |
132 val th = th |
133 |> inline_equations thy |
133 |> inline_equations thy |
134 |> Pred_Compile_Set.unfold_set_notation |
134 |> Predicate_Compile_Set.unfold_set_notation |
135 |> AxClass.unoverload thy |
135 |> AxClass.unoverload thy |
136 val (const, th) = |
136 val (const, th) = |
137 if is_equationlike th then |
137 if is_equationlike th then |
138 let |
138 let |
139 val eq = normalize_equation thy th |
139 val eq = normalize_equation thy th |