197 print_translation {* |
197 print_translation {* |
198 let |
198 let |
199 fun split_tr' [Abs (x, T, t as (Abs abs))] = |
199 fun split_tr' [Abs (x, T, t as (Abs abs))] = |
200 (* split (%x y. t) => %(x,y) t *) |
200 (* split (%x y. t) => %(x,y) t *) |
201 let |
201 let |
202 val (y, t') = atomic_abs_tr' abs; |
202 val (y, t') = Syntax_Trans.atomic_abs_tr' abs; |
203 val (x', t'') = atomic_abs_tr' (x, T, t'); |
203 val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t'); |
204 in |
204 in |
205 Syntax.const @{syntax_const "_abs"} $ |
205 Syntax.const @{syntax_const "_abs"} $ |
206 (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' |
206 (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' |
207 end |
207 end |
208 | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] = |
208 | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] = |
209 (* split (%x. (split (%y z. t))) => %(x,y,z). t *) |
209 (* split (%x. (split (%y z. t))) => %(x,y,z). t *) |
210 let |
210 let |
211 val Const (@{syntax_const "_abs"}, _) $ |
211 val Const (@{syntax_const "_abs"}, _) $ |
212 (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t]; |
212 (Const (@{syntax_const "_pattern"}, _) $ y $ z) $ t' = split_tr' [t]; |
213 val (x', t'') = atomic_abs_tr' (x, T, t'); |
213 val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, T, t'); |
214 in |
214 in |
215 Syntax.const @{syntax_const "_abs"} $ |
215 Syntax.const @{syntax_const "_abs"} $ |
216 (Syntax.const @{syntax_const "_pattern"} $ x' $ |
216 (Syntax.const @{syntax_const "_pattern"} $ x' $ |
217 (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t'' |
217 (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t'' |
218 end |
218 end |
219 | split_tr' [Const (@{const_syntax prod_case}, _) $ t] = |
219 | split_tr' [Const (@{const_syntax prod_case}, _) $ t] = |
220 (* split (split (%x y z. t)) => %((x, y), z). t *) |
220 (* split (split (%x y z. t)) => %((x, y), z). t *) |
221 split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *) |
221 split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *) |
222 | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] = |
222 | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] = |
223 (* split (%pttrn z. t) => %(pttrn,z). t *) |
223 (* split (%pttrn z. t) => %(pttrn,z). t *) |
224 let val (z, t) = atomic_abs_tr' abs in |
224 let val (z, t) = Syntax_Trans.atomic_abs_tr' abs in |
225 Syntax.const @{syntax_const "_abs"} $ |
225 Syntax.const @{syntax_const "_abs"} $ |
226 (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t |
226 (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t |
227 end |
227 end |
228 | split_tr' _ = raise Match; |
228 | split_tr' _ = raise Match; |
229 in [(@{const_syntax prod_case}, split_tr')] end |
229 in [(@{const_syntax prod_case}, split_tr')] end |
237 (case (head_of t) of |
237 (case (head_of t) of |
238 Const (@{const_syntax prod_case}, _) => raise Match |
238 Const (@{const_syntax prod_case}, _) => raise Match |
239 | _ => |
239 | _ => |
240 let |
240 let |
241 val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; |
241 val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; |
242 val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0); |
242 val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0); |
243 val (x', t'') = atomic_abs_tr' (x, xT, t'); |
243 val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t'); |
244 in |
244 in |
245 Syntax.const @{syntax_const "_abs"} $ |
245 Syntax.const @{syntax_const "_abs"} $ |
246 (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' |
246 (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' |
247 end) |
247 end) |
248 | split_guess_names_tr' T [t] = |
248 | split_guess_names_tr' T [t] = |
249 (case head_of t of |
249 (case head_of t of |
250 Const (@{const_syntax prod_case}, _) => raise Match |
250 Const (@{const_syntax prod_case}, _) => raise Match |
251 | _ => |
251 | _ => |
252 let |
252 let |
253 val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; |
253 val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; |
254 val (y, t') = atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0); |
254 val (y, t') = |
255 val (x', t'') = atomic_abs_tr' ("x", xT, t'); |
255 Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0); |
|
256 val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t'); |
256 in |
257 in |
257 Syntax.const @{syntax_const "_abs"} $ |
258 Syntax.const @{syntax_const "_abs"} $ |
258 (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' |
259 (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' |
259 end) |
260 end) |
260 | split_guess_names_tr' _ _ = raise Match; |
261 | split_guess_names_tr' _ _ = raise Match; |
274 [A, Abs(_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)] |
275 [A, Abs(_, _, (s as Const (@{const_syntax prod_case},_) $ t) $ Bound 0)] |
275 => if Term.is_dependent t then f ts else Syntax.const Q $ A $ s |
276 => if Term.is_dependent t then f ts else Syntax.const Q $ A $ s |
276 | _ => f ts; |
277 | _ => f ts; |
277 fun contract2 (Q,f) = (Q, contract Q f); |
278 fun contract2 (Q,f) = (Q, contract Q f); |
278 val pairs = |
279 val pairs = |
279 [Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"}, |
280 [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Ball} @{syntax_const "_Ball"}, |
280 Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}, |
281 Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax Bex} @{syntax_const "_Bex"}, |
281 Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}, |
282 Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFI} @{syntax_const "_INF"}, |
282 Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}] |
283 Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPR} @{syntax_const "_SUP"}] |
283 in map contract2 pairs end |
284 in map contract2 pairs end |
284 *} |
285 *} |
285 |
286 |
286 subsubsection {* Code generator setup *} |
287 subsubsection {* Code generator setup *} |
287 |
288 |