# HG changeset patch # User Lars Hupel # Date 1503384907 -7200 # Node ID d35f7a9f92e22b6586060be5d9ea585c9ff69d71 # Parent 4b8d1df8933b0b85cf643e579b312d839304cee1 output syntax for pattern aliases diff -r 4b8d1df8933b -r d35f7a9f92e2 NEWS --- a/NEWS Mon Aug 21 20:49:15 2017 +0200 +++ b/NEWS Tue Aug 22 08:55:07 2017 +0200 @@ -240,8 +240,8 @@ INCOMPATIBILITY. -* Theory "HOL-Library.Pattern_Aliases" provides input syntax for pattern -aliases as known from Haskell, Scala and ML. +* Theory "HOL-Library.Pattern_Aliases" provides input and output syntax +for pattern aliases as known from Haskell, Scala and ML. * Session HOL-Analysis: more material involving arcs, paths, covering spaces, innessential maps, retracts, material on infinite products. diff -r 4b8d1df8933b -r d35f7a9f92e2 src/HOL/Library/Pattern_Aliases.thy --- a/src/HOL/Library/Pattern_Aliases.thy Mon Aug 21 20:49:15 2017 +0200 +++ b/src/HOL/Library/Pattern_Aliases.thy Tue Aug 22 08:55:07 2017 +0200 @@ -11,7 +11,7 @@ text \ Most functional languages (Haskell, ML, Scala) support aliases in patterns. This allows to refer to a subpattern with a variable name. This theory implements this using a check phase. It works - well for function definitions (see usage below). + well for function definitions (see usage below). All features are packed into a @{command bundle}. The following caveats should be kept in mind: \<^item> The translation expects a term of the form @{prop "f x y = rhs"}, where \x\ and \y\ are patterns @@ -22,8 +22,10 @@ \<^item> Terms that do not adhere to the above shape may either stay untranslated or produce an error message. The @{command fun} command will complain if pattern aliases are left untranslated. In particular, there are no checks whether the patterns are wellformed or linear. - \<^item> There is no corresonding uncheck phase, because it is unclear in which situations the - translation should be reversed. + \<^item> The corresponding uncheck phase attempts to reverse the translation (no guarantee). + \<^item> To obtain reasonable induction principles in function definitions, the bundle also declares + a custom congruence rule for @{const Let} that only affects @{command fun}. This congruence + rule might lead to an explosion in term size (although that is rare)! \ @@ -31,10 +33,14 @@ consts as :: "'a \ 'a \ 'a" +lemma let_cong_unfolding: "M = N \ f N = g N \ Let M f = Let N g" +by simp + ML\ local fun let_typ a b = a --> (a --> b) --> b +fun as_typ a = a --> a --> a fun strip_all t = case try Logic.dest_all t of @@ -44,6 +50,27 @@ fun all_Frees t = fold_aterms (fn Free (x, t) => insert op = (x, t) | _ => I) t [] +fun subst_once (old, new) t = + let + fun go t = + if t = old then + (new, true) + else + case t of + u $ v => + let + val (u', substituted) = go u + in + if substituted then + (u' $ v, true) + else + case go v of (v', substituted) => (u $ v', substituted) + end + | Abs (name, typ, t) => + (case go t of (t', substituted) => (Abs (name, typ, t'), substituted)) + | _ => (t, false) + in fst (go t) end + in fun check_pattern_syntax t = @@ -53,7 +80,7 @@ fun go (Const (@{const_name as}, _) $ pat $ var, rhs) = let val (pat', rhs') = go (pat, rhs) - val _ = if is_Free var then () else error "Left-hand side of =: must be a free variable" + val _ = if is_Free var then () else error "Right-hand side of =: must be a free variable" val rhs'' = Const (@{const_name Let}, let_typ (fastype_of var) (fastype_of rhs)) $ pat' $ lambda var rhs' @@ -75,6 +102,35 @@ in fold (fn v => Logic.dependent_all_name ("", v)) (map Free frees) res end | _ => t +fun uncheck_pattern_syntax ctxt t = + case strip_all t of + (vars, @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs)) => + let + fun go lhs (rhs as Const (@{const_name Let}, _) $ pat $ Abs (name, typ, t)) ctxt frees = + if exists_subterm (fn t' => t' = pat) lhs then + let + val ([name'], ctxt') = Variable.variant_fixes [name] ctxt + val free = Free (name', typ) + val subst = (pat, Const (@{const_name as}, as_typ typ) $ pat $ free) + val lhs' = subst_once subst lhs + val rhs' = subst_bound (free, t) + in + go lhs' rhs' ctxt' (Free (name', typ) :: frees) + end + else + (lhs, rhs, ctxt, frees) + | go lhs rhs ctxt frees = (lhs, rhs, ctxt, frees) + + val (lhs', rhs', _, frees) = go lhs rhs ctxt [] + + val res = + HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs')) + |> fold (fn v => Logic.dependent_all_name ("", v)) (map Free vars @ frees) + in + if null frees then t else res + end + | _ => t + end \ @@ -83,6 +139,9 @@ notation as (infixr "=:" 1) declaration \K (Syntax_Phases.term_check 98 "pattern_syntax" (K (map check_pattern_syntax)))\ + declaration \K (Syntax_Phases.term_uncheck 98 "pattern_syntax" (map o uncheck_pattern_syntax))\ + + declare let_cong_unfolding [fundef_cong] end @@ -103,12 +162,23 @@ text \Very useful for function definitions.\ private fun test_2 where -"test_2 (y # (y' # ys =: x') =: x) = x @ x'" | +"test_2 (y # (y' # ys =: x') =: x) = x @ x' @ x'" | "test_2 _ = []" -lemma "test_2 (y # y' # ys) = (y # y' # ys) @ y' # ys" +lemma "test_2 (y # y' # ys) = (y # y' # ys) @ (y' # ys) @ (y' # ys)" by (rule test_2.simps[unfolded Let_def]) +ML\ +let + val actual = + @{thm test_2.simps(1)} + |> Thm.prop_of + |> Syntax.string_of_term @{context} + |> YXML.content_of + val expected = "\x x'. test_2 (?y # (?y' # ?ys =: x') =: x) = x @ x' @ x'" +in @{assert} (actual = expected) end +\ + end end \ No newline at end of file