equal
deleted
inserted
replaced
35 |
35 |
36 fun print_specs thy specs = |
36 fun print_specs thy specs = |
37 map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n" |
37 map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n" |
38 ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs |
38 ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs |
39 |
39 |
40 (* TODO: *) |
40 fun overload_const thy s = the_default s (Option.map fst (AxClass.inst_of_param thy s)) |
41 fun overload_const thy s = s |
|
42 |
41 |
43 fun map_specs f specs = |
42 fun map_specs f specs = |
44 map (fn (s, ths) => (s, f ths)) specs |
43 map (fn (s, ths) => (s, f ths)) specs |
45 |
44 |
46 fun process_specification options specs thy' = |
45 fun process_specification options specs thy' = |
85 val specs = (get_specs prednames) @ fun_pred_specs |
84 val specs = (get_specs prednames) @ fun_pred_specs |
86 val (intross3, thy''') = process_specification options specs thy' |
85 val (intross3, thy''') = process_specification options specs thy' |
87 val _ = print_intross options thy''' "Introduction rules with new constants: " intross3 |
86 val _ = print_intross options thy''' "Introduction rules with new constants: " intross3 |
88 val intross4 = map_specs (maps remove_pointless_clauses) intross3 |
87 val intross4 = map_specs (maps remove_pointless_clauses) intross3 |
89 val _ = print_intross options thy''' "After removing pointless clauses: " intross4 |
88 val _ = print_intross options thy''' "After removing pointless clauses: " intross4 |
90 val intross5 = (*map (fn (s, ths) => (overload_const s, map (AxClass.overload thy''') ths))*) intross4 |
89 val intross5 = map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross4 |
91 val intross6 = map_specs (map (expand_tuples thy''')) intross4 |
90 val intross6 = map_specs (map (expand_tuples thy''')) intross5 |
92 val _ = print_intross options thy''' "introduction rules before registering: " intross6 |
91 val _ = print_intross options thy''' "introduction rules before registering: " intross6 |
93 val _ = print_step options "Registering introduction rules..." |
92 val _ = print_step options "Registering introduction rules..." |
94 val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy''' |
93 val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy''' |
95 in |
94 in |
96 thy'''' |
95 thy'''' |