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

author | haftmann |

Sun, 06 Sep 2015 22:14:51 +0200 | |

changeset 61126 | e6b1236f9b3d |

parent 61125 | 4c68426800de |

child 61127 | 76cd7f1ec257 |

obsolete: if case_prod is fully applied, it is printed as proper case expression;
eta-contracted variants are read best as "uncurry" combinator

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

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

--- a/NEWS Sun Sep 06 22:14:51 2015 +0200 +++ b/NEWS Sun Sep 06 22:14:51 2015 +0200 @@ -189,6 +189,16 @@ * 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. INCOMPATIBILITY. * Some old and rarely used ASCII replacement syntax has been removed. @@ -199,6 +209,11 @@ type_notation Map.map (infixr "~=>" 0) notation Map.map_comp (infixl "o'_m" 55) +* Case combinator "prod_case" with eta-contracted body functions +has explicit "uncurry" notation, to provide a compact notation while +getting ride of a special case translation. Slight syntactic +INCOMPATIBILITY. + * Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has been removed. INCOMPATIBILITY.

--- a/src/HOL/Product_Type.thy Sun Sep 06 22:14:51 2015 +0200 +++ b/src/HOL/Product_Type.thy Sun Sep 06 22:14:51 2015 +0200 @@ -311,39 +311,6 @@ The @{text "(x, y)"} is parsed as @{text "Pair x y"} because it is @{text logic}, not @{text pttrn}.\<close> -(* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) -typed_print_translation \<open> - let - fun split_guess_names_tr' T [Abs (x, _, Abs _)] = raise Match - | split_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) - | split_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) - | split_guess_names_tr' _ _ = raise Match; - in [(@{const_syntax uncurry}, K split_guess_names_tr')] end -\<close> - subsubsection \<open>Code generator setup\<close>