14 val funcs: T -> CodegenConsts.const -> thm list |
14 val funcs: T -> CodegenConsts.const -> thm list |
15 val typ: T -> CodegenConsts.const -> typ |
15 val typ: T -> CodegenConsts.const -> typ |
16 val deps: T -> CodegenConsts.const list -> CodegenConsts.const list list |
16 val deps: T -> CodegenConsts.const list -> CodegenConsts.const list list |
17 val all: T -> CodegenConsts.const list |
17 val all: T -> CodegenConsts.const list |
18 val norm_varnames: theory -> thm list -> thm list |
18 val norm_varnames: theory -> thm list -> thm list |
19 val expand_eta: theory -> int -> thm -> thm |
|
20 val print_codethms: theory -> CodegenConsts.const list -> unit |
19 val print_codethms: theory -> CodegenConsts.const list -> unit |
21 structure Constgraph : GRAPH |
20 structure Constgraph : GRAPH |
22 end; |
21 end; |
23 |
22 |
24 structure CodegenFuncgr: CODEGEN_FUNCGR = |
23 structure CodegenFuncgr: CODEGEN_FUNCGR = |
49 val _ = Context.add_setup Funcgr.init; |
48 val _ = Context.add_setup Funcgr.init; |
50 |
49 |
51 |
50 |
52 (** theorem purification **) |
51 (** theorem purification **) |
53 |
52 |
54 fun expand_eta thy k thm = |
|
55 let |
|
56 val (lhs, rhs) = (Logic.dest_equals o Drule.plain_prop_of) thm; |
|
57 val (head, args) = strip_comb lhs; |
|
58 val l = Int.max (0, k - length args); |
|
59 val used = Name.make_context (map (fst o fst) (Term.add_vars lhs [])); |
|
60 fun get_name _ 0 used = ([], used) |
|
61 | get_name (Abs (v, ty, t)) k used = |
|
62 used |
|
63 |> Name.variants [CodegenNames.purify_var v] |
|
64 ||>> get_name t (k - 1) |
|
65 |>> (fn ([v'], vs') => (v', ty) :: vs') |
|
66 | get_name t k used = |
|
67 let |
|
68 val (tys, _) = (strip_type o fastype_of) t |
|
69 in case tys |
|
70 of [] => raise TERM ("expand_eta", [t]) |
|
71 | ty :: _ => |
|
72 used |
|
73 |> Name.variants [""] |
|
74 |-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1) |
|
75 #>> (fn vs' => (v, ty) :: vs')) |
|
76 end; |
|
77 val (vs, _) = get_name rhs l used; |
|
78 val vs_refl = map (fn (v, ty) => Thm.reflexive (Thm.cterm_of thy (Var ((v, 0), ty)))) vs; |
|
79 in |
|
80 fold (fn refl => fn thm => Thm.combination thm refl) vs_refl thm |
|
81 end; |
|
82 |
|
83 fun norm_args thy thms = |
53 fun norm_args thy thms = |
84 let |
54 let |
85 val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals; |
55 val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals; |
86 val k = fold (curry Int.max o num_args_of o Drule.plain_prop_of) thms 0; |
56 val k = fold (curry Int.max o num_args_of o Drule.plain_prop_of) thms 0; |
87 in |
57 in |
88 thms |
58 thms |
89 |> map (expand_eta thy k) |
59 |> map (CodegenFunc.expand_eta thy k) |
90 |> map (Drule.fconv_rule Drule.beta_eta_conversion) |
60 |> map (Drule.fconv_rule Drule.beta_eta_conversion) |
91 end; |
61 end; |
92 |
62 |
93 fun canonical_tvars thy thm = |
63 fun canonical_tvars thy thm = |
94 let |
64 let |