summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Tue, 22 Sep 2015 11:48:22 +0200 | |

changeset 61226 | af7bed1360f3 |

parent 61225 | 1a690dce8cfc |

child 61227 | 19ee25fe9737 |

effective revert of e6b1236f9b3d: spontaneous eta-contraction happens on the print translation level and can only be suppressed on the print translation level

NEWS | file | annotate | diff | comparison | revisions | |

src/HOL/Product_Type.thy | file | annotate | diff | comparison | revisions |

--- a/NEWS Tue Sep 22 14:31:22 2015 +0200 +++ b/NEWS Tue Sep 22 11:48:22 2015 +0200 @@ -202,16 +202,10 @@ * Combinator to represent case distinction on products is named "uncurry", with "split" and "prod_case" retained as input abbreviations. -Partially applied occurences of "uncurry" with eta-contracted body -terms are not printed with special syntax, to provide a compact -notation and getting rid of a special-case print translation. Hence, the "uncurry"-expressions are printed the following way: a) fully applied "uncurry f p": explicit case-expression; -b) partially applied with explicit double lambda abstraction in -the body term "uncurry (%a b. t [a, b])": explicit paired abstraction; -c) partially applied with eta-contracted body term "uncurry f": -no special syntax, plain "uncurry" combinator. -This aims for maximum readability in a given subterm. +b) partially applied "uncurry f": explicit paired abstraction; +c) unapplied "uncurry": as it is. INCOMPATIBILITY. * Some old and rarely used ASCII replacement syntax has been removed.

--- a/src/HOL/Product_Type.thy Tue Sep 22 14:31:22 2015 +0200 +++ b/src/HOL/Product_Type.thy Tue Sep 22 11:48:22 2015 +0200 @@ -311,6 +311,41 @@ The @{text "(x, y)"} is parsed as @{text "Pair x y"} because it is @{text logic}, not @{text pttrn}.\<close> +text \<open>print @{term "uncurry f"} as @{term "\<lambda>(x, y). f x y"} and + @{term "uncurry (\<lambda>x. f x)"} as @{term "\<lambda>(x, y). f x y"}\<close> + +typed_print_translation \<open> + let + fun uncurry_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match + | uncurry_guess_names_tr' T [Abs (x, xT, t)] = + (case (head_of t) of + Const (@{const_syntax uncurry}, _) => raise Match + | _ => + let + val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; + val (y, t') = Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 1 t $ Bound 0); + val (x', t'') = Syntax_Trans.atomic_abs_tr' (x, xT, t'); + in + Syntax.const @{syntax_const "_abs"} $ + (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' + end) + | uncurry_guess_names_tr' T [t] = + (case head_of t of + Const (@{const_syntax uncurry}, _) => raise Match + | _ => + let + val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match; + val (y, t') = + Syntax_Trans.atomic_abs_tr' ("y", yT, incr_boundvars 2 t $ Bound 1 $ Bound 0); + val (x', t'') = Syntax_Trans.atomic_abs_tr' ("x", xT, t'); + in + Syntax.const @{syntax_const "_abs"} $ + (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t'' + end) + | uncurry_guess_names_tr' _ _ = raise Match; + in [(@{const_syntax uncurry}, K uncurry_guess_names_tr')] end +\<close> + subsubsection \<open>Code generator setup\<close>