7 |
7 |
8 signature RECFUN_CODEGEN = |
8 signature RECFUN_CODEGEN = |
9 sig |
9 sig |
10 val add: string option -> attribute |
10 val add: string option -> attribute |
11 val del: attribute |
11 val del: attribute |
12 val get_rec_equations: theory -> string * typ -> (term list * term) list * typ |
|
13 val get_thm_equations: theory -> string * typ -> (thm list * typ) option |
12 val get_thm_equations: theory -> string * typ -> (thm list * typ) option |
14 val setup: theory -> theory |
13 val setup: theory -> theory |
15 end; |
14 end; |
16 |
15 |
17 structure RecfunCodegen : RECFUN_CODEGEN = |
16 structure RecfunCodegen : RECFUN_CODEGEN = |
78 NONE => (case get_defn thy defs s T of |
77 NONE => (case get_defn thy defs s T of |
79 NONE => thyname_of_const s thy |
78 NONE => thyname_of_const s thy |
80 | SOME ((_, (thyname, _)), _) => thyname) |
79 | SOME ((_, (thyname, _)), _) => thyname) |
81 | SOME thyname => thyname) |
80 | SOME thyname => thyname) |
82 end); |
81 end); |
83 |
|
84 fun get_rec_equations thy (s, T) = |
|
85 Symtab.lookup (CodegenData.get thy) s |
|
86 |> Option.map (fn thms => |
|
87 List.filter (fn (thm, _) => is_instance thy T ((snd o const_of o prop_of) thm)) thms |
|
88 |> del_redundant thy []) |
|
89 |> Option.mapPartial (fn thms => if null thms then NONE else SOME thms) |
|
90 |> Option.map (fn thms => |
|
91 (preprocess thy (map fst thms), |
|
92 (snd o const_of o prop_of o fst o hd) thms)) |
|
93 |> the_default ([], dummyT) |
|
94 |> apfst (map prop_of) |
|
95 |> apfst (map (Codegen.rename_term #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> apfst (strip_comb #> snd))) |
|
96 |
82 |
97 fun get_thm_equations thy (c, ty) = |
83 fun get_thm_equations thy (c, ty) = |
98 Symtab.lookup (CodegenData.get thy) c |
84 Symtab.lookup (CodegenData.get thy) c |
99 |> Option.map (fn thms => |
85 |> Option.map (fn thms => |
100 List.filter (fn (thm, _) => is_instance thy ty ((snd o const_of o prop_of) thm)) thms |
86 List.filter (fn (thm, _) => is_instance thy ty ((snd o const_of o prop_of) thm)) thms |