output syntax for pattern aliases
authorLars Hupel <lars.hupel@mytum.de>
Tue Aug 22 08:55:07 2017 +0200 (21 months ago)
changeset 66481d35f7a9f92e2
parent 66480 4b8d1df8933b
child 66482 5dc8671bec73
child 66483 123acfd5fe35
output syntax for pattern aliases
NEWS
src/HOL/Library/Pattern_Aliases.thy
     1.1 --- a/NEWS	Mon Aug 21 20:49:15 2017 +0200
     1.2 +++ b/NEWS	Tue Aug 22 08:55:07 2017 +0200
     1.3 @@ -240,8 +240,8 @@
     1.4  
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 -* Theory "HOL-Library.Pattern_Aliases" provides input syntax for pattern
     1.8 -aliases as known from Haskell, Scala and ML.
     1.9 +* Theory "HOL-Library.Pattern_Aliases" provides input and output syntax
    1.10 +for pattern aliases as known from Haskell, Scala and ML.
    1.11  
    1.12  * Session HOL-Analysis: more material involving arcs, paths, covering
    1.13  spaces, innessential maps, retracts, material on infinite products.
     2.1 --- a/src/HOL/Library/Pattern_Aliases.thy	Mon Aug 21 20:49:15 2017 +0200
     2.2 +++ b/src/HOL/Library/Pattern_Aliases.thy	Tue Aug 22 08:55:07 2017 +0200
     2.3 @@ -11,7 +11,7 @@
     2.4  text \<open>
     2.5    Most functional languages (Haskell, ML, Scala) support aliases in patterns. This allows to refer
     2.6    to a subpattern with a variable name. This theory implements this using a check phase. It works
     2.7 -  well for function definitions (see usage below).
     2.8 +  well for function definitions (see usage below). All features are packed into a @{command bundle}.
     2.9  
    2.10    The following caveats should be kept in mind:
    2.11    \<^item> The translation expects a term of the form @{prop "f x y = rhs"}, where \<open>x\<close> and \<open>y\<close> are patterns
    2.12 @@ -22,8 +22,10 @@
    2.13    \<^item> Terms that do not adhere to the above shape may either stay untranslated or produce an error
    2.14      message. The @{command fun} command will complain if pattern aliases are left untranslated.
    2.15      In particular, there are no checks whether the patterns are wellformed or linear.
    2.16 -  \<^item> There is no corresonding uncheck phase, because it is unclear in which situations the
    2.17 -    translation should be reversed.
    2.18 +  \<^item> The corresponding uncheck phase attempts to reverse the translation (no guarantee).
    2.19 +  \<^item> To obtain reasonable induction principles in function definitions, the bundle also declares
    2.20 +    a custom congruence rule for @{const Let} that only affects @{command fun}. This congruence
    2.21 +    rule might lead to an explosion in term size (although that is rare)!
    2.22  \<close>
    2.23  
    2.24  
    2.25 @@ -31,10 +33,14 @@
    2.26  
    2.27  consts as :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    2.28  
    2.29 +lemma let_cong_unfolding: "M = N \<Longrightarrow> f N = g N \<Longrightarrow> Let M f = Let N g"
    2.30 +by simp
    2.31 +
    2.32  ML\<open>
    2.33  local
    2.34  
    2.35  fun let_typ a b = a --> (a --> b) --> b
    2.36 +fun as_typ a = a --> a --> a
    2.37  
    2.38  fun strip_all t =
    2.39    case try Logic.dest_all t of
    2.40 @@ -44,6 +50,27 @@
    2.41  fun all_Frees t =
    2.42    fold_aterms (fn Free (x, t) => insert op = (x, t) | _ => I) t []
    2.43  
    2.44 +fun subst_once (old, new) t =
    2.45 +  let
    2.46 +    fun go t =
    2.47 +      if t = old then
    2.48 +        (new, true)
    2.49 +      else
    2.50 +        case t of
    2.51 +          u $ v =>
    2.52 +            let
    2.53 +              val (u', substituted) = go u
    2.54 +            in
    2.55 +              if substituted then
    2.56 +                (u' $ v, true)
    2.57 +              else
    2.58 +                case go v of (v', substituted) => (u $ v', substituted)
    2.59 +            end
    2.60 +        | Abs (name, typ, t) =>
    2.61 +            (case go t of (t', substituted) => (Abs (name, typ, t'), substituted))
    2.62 +        | _ => (t, false)
    2.63 +  in fst (go t) end
    2.64 +
    2.65  in
    2.66  
    2.67  fun check_pattern_syntax t =
    2.68 @@ -53,7 +80,7 @@
    2.69          fun go (Const (@{const_name as}, _) $ pat $ var, rhs) =
    2.70                let
    2.71                  val (pat', rhs') = go (pat, rhs)
    2.72 -                val _ = if is_Free var then () else error "Left-hand side of =: must be a free variable"
    2.73 +                val _ = if is_Free var then () else error "Right-hand side of =: must be a free variable"
    2.74                  val rhs'' =
    2.75                    Const (@{const_name Let}, let_typ (fastype_of var) (fastype_of rhs)) $
    2.76                      pat' $ lambda var rhs'
    2.77 @@ -75,6 +102,35 @@
    2.78        in fold (fn v => Logic.dependent_all_name ("", v)) (map Free frees) res end
    2.79    | _ => t
    2.80  
    2.81 +fun uncheck_pattern_syntax ctxt t =
    2.82 +  case strip_all t of
    2.83 +    (vars, @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs)) =>
    2.84 +      let
    2.85 +        fun go lhs (rhs as Const (@{const_name Let}, _) $ pat $ Abs (name, typ, t)) ctxt frees =
    2.86 +              if exists_subterm (fn t' => t' = pat) lhs then
    2.87 +                let
    2.88 +                  val ([name'], ctxt') = Variable.variant_fixes [name] ctxt
    2.89 +                  val free = Free (name', typ)
    2.90 +                  val subst = (pat, Const (@{const_name as}, as_typ typ) $ pat $ free)
    2.91 +                  val lhs' = subst_once subst lhs
    2.92 +                  val rhs' = subst_bound (free, t)
    2.93 +                in
    2.94 +                  go lhs' rhs' ctxt' (Free (name', typ) :: frees)
    2.95 +                end
    2.96 +              else
    2.97 +                (lhs, rhs, ctxt, frees)
    2.98 +          | go lhs rhs ctxt frees = (lhs, rhs, ctxt, frees)
    2.99 +
   2.100 +        val (lhs', rhs', _, frees) = go lhs rhs ctxt []
   2.101 +
   2.102 +        val res =
   2.103 +          HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs'))
   2.104 +          |> fold (fn v => Logic.dependent_all_name ("", v)) (map Free vars @ frees)
   2.105 +      in
   2.106 +        if null frees then t else res
   2.107 +      end
   2.108 +  | _ => t
   2.109 +
   2.110  end
   2.111  \<close>
   2.112  
   2.113 @@ -83,6 +139,9 @@
   2.114    notation as (infixr "=:" 1)
   2.115  
   2.116    declaration \<open>K (Syntax_Phases.term_check 98 "pattern_syntax" (K (map check_pattern_syntax)))\<close>
   2.117 +  declaration \<open>K (Syntax_Phases.term_uncheck 98 "pattern_syntax" (map o uncheck_pattern_syntax))\<close>
   2.118 +
   2.119 +  declare let_cong_unfolding [fundef_cong]
   2.120  
   2.121  end
   2.122  
   2.123 @@ -103,12 +162,23 @@
   2.124  text \<open>Very useful for function definitions.\<close>
   2.125  
   2.126  private fun test_2 where
   2.127 -"test_2 (y # (y' # ys =: x') =: x) = x @ x'" |
   2.128 +"test_2 (y # (y' # ys =: x') =: x) = x @ x' @ x'" |
   2.129  "test_2 _ = []"
   2.130  
   2.131 -lemma "test_2 (y # y' # ys) = (y # y' # ys) @ y' # ys"
   2.132 +lemma "test_2 (y # y' # ys) = (y # y' # ys) @ (y' # ys) @ (y' # ys)"
   2.133  by (rule test_2.simps[unfolded Let_def])
   2.134  
   2.135 +ML\<open>
   2.136 +let
   2.137 +  val actual =
   2.138 +    @{thm test_2.simps(1)}
   2.139 +    |> Thm.prop_of
   2.140 +    |> Syntax.string_of_term @{context}
   2.141 +    |> YXML.content_of
   2.142 +  val expected = "\<And>x x'. test_2 (?y # (?y' # ?ys =: x') =: x) = x @ x' @ x'"
   2.143 +in @{assert} (actual = expected) end
   2.144 +\<close>
   2.145 +
   2.146  end
   2.147  
   2.148  end
   2.149 \ No newline at end of file