19 type code_graph |
19 type code_graph |
20 val cert: code_graph -> string -> Code.cert |
20 val cert: code_graph -> string -> Code.cert |
21 val sortargs: code_graph -> string -> sort list |
21 val sortargs: code_graph -> string -> sort list |
22 val all: code_graph -> string list |
22 val all: code_graph -> string list |
23 val pretty: Proof.context -> code_graph -> Pretty.T |
23 val pretty: Proof.context -> code_graph -> Pretty.T |
24 val obtain: bool -> Proof.context -> string list -> term list -> code_algebra * code_graph |
24 val obtain: bool -> Proof.context -> string list -> term list -> |
|
25 { algebra: code_algebra, eqngr: code_graph } |
25 val dynamic_conv: Proof.context |
26 val dynamic_conv: Proof.context |
26 -> (code_algebra -> code_graph -> term -> conv) -> conv |
27 -> (code_algebra -> code_graph -> term -> conv) -> conv |
27 val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'b) |
28 val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'b) |
28 -> (code_algebra -> code_graph -> term -> 'a) -> term -> 'b |
29 -> (code_algebra -> code_graph -> term -> 'a) -> term -> 'b |
29 val static_conv: { ctxt: Proof.context, consts: string list } |
30 val static_conv: { ctxt: Proof.context, consts: string list } |
121 else Thm.transitive eq1 eq2; |
122 else Thm.transitive eq1 eq2; |
122 |
123 |
123 fun trans_conv_rule conv eq = trans_comb eq (conv (Thm.rhs_of eq)); |
124 fun trans_conv_rule conv eq = trans_comb eq (conv (Thm.rhs_of eq)); |
124 |
125 |
125 structure Sandwich : sig |
126 structure Sandwich : sig |
126 type T = Proof.context -> cterm -> (thm -> thm) * cterm; |
127 type T = Proof.context -> cterm -> (Proof.context -> thm -> thm) * cterm; |
127 val chain: T -> T -> T |
128 val chain: T -> T -> T |
128 val lift: (Proof.context -> cterm -> (cterm -> thm) * thm) -> T |
129 val lift: (Proof.context -> cterm -> (Proof.context -> cterm -> thm) * thm) -> T |
129 val conversion: T -> (Proof.context -> term -> conv) -> Proof.context -> conv; |
130 val conversion: T -> (Proof.context -> term -> conv) -> Proof.context -> conv; |
130 val computation: T -> ((term -> term) -> 'a -> 'b) -> |
131 val computation: T -> ((term -> term) -> 'a -> 'b) -> |
131 (Proof.context -> term -> 'a) -> Proof.context -> term -> 'b; |
132 (Proof.context -> term -> 'a) -> Proof.context -> term -> 'b; |
132 end = struct |
133 end = struct |
133 |
134 |
134 type T = Proof.context -> cterm -> (thm -> thm) * cterm; |
135 type T = Proof.context -> cterm -> (Proof.context -> thm -> thm) * cterm; |
135 |
136 |
136 fun chain sandwich2 sandwich1 ctxt = |
137 fun chain sandwich2 sandwich1 ctxt = |
137 sandwich1 ctxt |
138 sandwich1 ctxt |
138 ##>> sandwich2 ctxt |
139 ##>> sandwich2 ctxt |
139 #>> (op o); |
140 #>> (fn (f, g) => fn ctxt => f ctxt o g ctxt); |
140 |
141 |
141 fun lift conv_sandwhich ctxt ct = |
142 fun lift conv_sandwhich ctxt ct = |
142 let |
143 let |
143 val (postproc_conv, eq) = conv_sandwhich ctxt ct; |
144 val (postproc_conv, eq) = conv_sandwhich ctxt ct; |
144 fun potentail_trans_comb eq1 eq2 = |
145 fun potentail_trans_comb eq1 eq2 = |
145 if matches_transitive eq1 eq2 then trans_comb eq1 eq2 else eq2; |
146 if matches_transitive eq1 eq2 then trans_comb eq1 eq2 else eq2; |
146 (*weakened protocol for plain term evaluation*) |
147 (*weakened protocol for plain term evaluation*) |
147 in (trans_conv_rule postproc_conv o potentail_trans_comb eq, Thm.rhs_of eq) end; |
148 in (fn ctxt => trans_conv_rule (postproc_conv ctxt) o potentail_trans_comb eq, Thm.rhs_of eq) end; |
148 |
149 |
149 fun conversion sandwich conv ctxt ct = |
150 fun conversion sandwich conv ctxt ct = |
150 let |
151 let |
151 val (postproc, ct') = sandwich ctxt ct; |
152 val (postproc, ct') = sandwich ctxt ct; |
152 in postproc (conv ctxt (Thm.term_of ct') ct') end; |
153 val thm = conv ctxt (Thm.term_of ct') ct'; |
|
154 val thm' = postproc ctxt thm; |
|
155 in thm' end; |
153 |
156 |
154 fun computation sandwich lift_postproc eval ctxt t = |
157 fun computation sandwich lift_postproc eval ctxt t = |
155 let |
158 let |
156 val (postproc, ct') = sandwich ctxt (Thm.cterm_of ctxt t); |
159 val (postproc, ct') = sandwich ctxt (Thm.cterm_of ctxt t); |
157 in |
160 val result = eval ctxt (Thm.term_of ct'); |
158 Thm.term_of ct' |
161 val result' = lift_postproc |
159 |> eval ctxt |
162 (Thm.term_of o Thm.rhs_of o postproc ctxt o Thm.reflexive o Thm.cterm_of ctxt) |
160 |> lift_postproc (Thm.term_of o Thm.rhs_of o postproc o Thm.reflexive o Thm.cterm_of ctxt) |
163 result |
161 end; |
164 in result' end; |
162 |
165 |
163 end; |
166 end; |
164 |
167 |
165 |
168 |
166 (* post- and preprocessing *) |
169 (* post- and preprocessing *) |
176 val normalization = |
179 val normalization = |
177 map2 (fn (v, sort) => fn (v', _) => (((v', 0), sort), Thm.ctyp_of ctxt (TFree (v, sort)))) |
180 map2 (fn (v, sort) => fn (v', _) => (((v', 0), sort), Thm.ctyp_of ctxt (TFree (v, sort)))) |
178 vs_original vs_normalized; |
181 vs_original vs_normalized; |
179 in |
182 in |
180 if eq_list (eq_fst (op =)) (vs_normalized, vs_original) |
183 if eq_list (eq_fst (op =)) (vs_normalized, vs_original) |
181 then (I, ct) |
184 then (K I, ct) |
182 else |
185 else |
183 (Thm.instantiate (normalization, []) o Thm.varifyT_global, |
186 (K (Thm.instantiate (normalization, []) o Thm.varifyT_global), |
184 Thm.cterm_of ctxt (map_types normalize t)) |
187 Thm.cterm_of ctxt (map_types normalize t)) |
185 end; |
188 end; |
186 |
189 |
187 fun no_variables_sandwich ctxt ct = |
190 fun no_variables_sandwich ctxt ct = |
188 let |
191 let |
192 fun apply_beta var thm = Thm.combination thm (Thm.reflexive var) |
195 fun apply_beta var thm = Thm.combination thm (Thm.reflexive var) |
193 |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false))) |
196 |> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false))) |
194 |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false)); |
197 |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false)); |
195 in |
198 in |
196 if null all_vars |
199 if null all_vars |
197 then (I, ct) |
200 then (K I, ct) |
198 else (fold apply_beta all_vars, fold_rev Thm.lambda all_vars ct) |
201 else (K (fold apply_beta all_vars), fold_rev Thm.lambda all_vars ct) |
199 end; |
202 end; |
200 |
203 |
201 fun simplifier_conv_sandwich ctxt = |
204 fun simplifier_conv_sandwich ctxt = |
202 let |
205 let |
203 val thy = Proof_Context.theory_of ctxt; |
206 val thy = Proof_Context.theory_of ctxt; |
204 val pre = (#pre o the_thmproc) thy; |
207 val pre = (#pre o the_thmproc) thy; |
205 val post = (#post o the_thmproc) thy; |
208 val post = (#post o the_thmproc) thy; |
206 fun pre_conv ctxt' = |
209 fun pre_conv ctxt' = |
207 Simplifier.rewrite (put_simpset pre ctxt') |
210 Simplifier.rewrite (put_simpset pre ctxt') |
208 #> trans_conv_rule (Axclass.unoverload_conv ctxt') |
211 #> trans_conv_rule (Axclass.unoverload_conv ctxt') |
209 fun post_conv ctxt' = |
212 fun post_conv ctxt'' = |
210 Axclass.overload_conv ctxt' |
213 Axclass.overload_conv ctxt'' |
211 #> trans_conv_rule (Simplifier.rewrite (put_simpset post ctxt')) |
214 #> trans_conv_rule (Simplifier.rewrite (put_simpset post ctxt'')) |
212 in fn ctxt' => pre_conv ctxt' #> pair (post_conv ctxt') end; |
215 in fn ctxt' => pre_conv ctxt' #> pair post_conv end; |
213 |
216 |
214 fun simplifier_sandwich ctxt = Sandwich.lift (simplifier_conv_sandwich ctxt); |
217 fun simplifier_sandwich ctxt = |
|
218 Sandwich.lift (simplifier_conv_sandwich ctxt); |
215 |
219 |
216 fun value_sandwich ctxt = |
220 fun value_sandwich ctxt = |
217 normalized_tfrees_sandwich |
221 normalized_tfrees_sandwich |
218 |> Sandwich.chain no_variables_sandwich |
222 |> Sandwich.chain no_variables_sandwich |
219 |> Sandwich.chain (simplifier_sandwich ctxt); |
223 |> Sandwich.chain (simplifier_sandwich ctxt); |
546 * "evaluation" is a lifting of an evaluator |
550 * "evaluation" is a lifting of an evaluator |
547 *) |
551 *) |
548 |
552 |
549 fun obtain ignore_cache ctxt consts ts = apsnd snd |
553 fun obtain ignore_cache ctxt consts ts = apsnd snd |
550 (Wellsorted.change_yield (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt)) |
554 (Wellsorted.change_yield (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt)) |
551 (extend_arities_eqngr ctxt consts ts)); |
555 (extend_arities_eqngr ctxt consts ts)) |
|
556 |> (fn (algebra, eqngr) => { algebra = algebra, eqngr = eqngr }); |
552 |
557 |
553 fun dynamic_evaluation eval ctxt t = |
558 fun dynamic_evaluation eval ctxt t = |
554 let |
559 let |
555 val consts = fold_aterms |
560 val consts = fold_aterms |
556 (fn Const (c, _) => insert (op =) c | _ => I) t []; |
561 (fn Const (c, _) => insert (op =) c | _ => I) t []; |
557 val (algebra, eqngr) = obtain false ctxt consts [t]; |
562 val { algebra, eqngr } = obtain false ctxt consts [t]; |
558 in eval algebra eqngr t end; |
563 in eval algebra eqngr t end; |
559 |
564 |
560 fun static_evaluation ctxt consts eval = |
565 fun static_evaluation ctxt consts eval = |
561 let |
566 eval (obtain true ctxt consts []); |
562 val (algebra, eqngr) = obtain true ctxt consts []; |
|
563 in eval { algebra = algebra, eqngr = eqngr } end; |
|
564 |
567 |
565 fun dynamic_conv ctxt conv = |
568 fun dynamic_conv ctxt conv = |
566 Sandwich.conversion (value_sandwich ctxt) |
569 Sandwich.conversion (value_sandwich ctxt) |
567 (dynamic_evaluation conv) ctxt; |
570 (dynamic_evaluation conv) ctxt; |
568 |
571 |