308 "\<lambda>(x, y). b" \<rightleftharpoons> "CONST uncurry (\<lambda>x y. b)" |
308 "\<lambda>(x, y). b" \<rightleftharpoons> "CONST uncurry (\<lambda>x y. b)" |
309 "_abs (CONST Pair x y) t" \<rightharpoonup> "\<lambda>(x, y). t" |
309 "_abs (CONST Pair x y) t" \<rightharpoonup> "\<lambda>(x, y). t" |
310 -- \<open>This rule accommodates tuples in @{text "case C \<dots> (x, y) \<dots> \<Rightarrow> \<dots>"}: |
310 -- \<open>This rule accommodates tuples in @{text "case C \<dots> (x, y) \<dots> \<Rightarrow> \<dots>"}: |
311 The @{text "(x, y)"} is parsed as @{text "Pair x y"} because it is @{text logic}, |
311 The @{text "(x, y)"} is parsed as @{text "Pair x y"} because it is @{text logic}, |
312 not @{text pttrn}.\<close> |
312 not @{text pttrn}.\<close> |
|
313 |
|
314 text \<open>print @{term "uncurry f"} as @{term "\<lambda>(x, y). f x y"} and |
|
315 @{term "uncurry (\<lambda>x. f x)"} as @{term "\<lambda>(x, y). f x y"}\<close> |
|
316 |
|
317 typed_print_translation \<open> |
|
318 let |
|
319 fun uncurry_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match |
|
320 | uncurry_guess_names_tr' T [Abs (x, xT, t)] = |
|
321 (case (head_of t) of |
|
322 Const (@{const_syntax uncurry}, _) => raise Match |
|
323 | _ => |
|
324 let |
|
325 val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; |
|
326 val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0); |
|
327 val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t'); |
|
328 in |
|
329 Syntax.const @{syntax_const "_abs"} $ |
|
330 (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' |
|
331 end) |
|
332 | uncurry_guess_names_tr' T [t] = |
|
333 (case head_of t of |
|
334 Const (@{const_syntax uncurry}, _) => raise Match |
|
335 | _ => |
|
336 let |
|
337 val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; |
|
338 val (y, t') = |
|
339 Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0); |
|
340 val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t'); |
|
341 in |
|
342 Syntax.const @{syntax_const "_abs"} $ |
|
343 (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' |
|
344 end) |
|
345 | uncurry_guess_names_tr' _ _ = raise Match; |
|
346 in [(@{const_syntax uncurry}, K uncurry_guess_names_tr')] end |
|
347 \<close> |
313 |
348 |
314 |
349 |
315 subsubsection \<open>Code generator setup\<close> |
350 subsubsection \<open>Code generator setup\<close> |
316 |
351 |
317 code_printing |
352 code_printing |