syntax for pattern aliases
authorLars Hupel <lars.hupel@mytum.de>
Fri Aug 18 14:57:23 2017 +0200 (21 months ago)
changeset 664515be0b0604d71
parent 66450 a8299195ed82
child 66455 158c513a39f5
syntax for pattern aliases
NEWS
src/HOL/Library/Library.thy
src/HOL/Library/Pattern_Aliases.thy
     1.1 --- a/NEWS	Thu Aug 17 22:29:30 2017 +0200
     1.2 +++ b/NEWS	Fri Aug 18 14:57:23 2017 +0200
     1.3 @@ -121,6 +121,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Theory Library/Pattern_Aliases provides input syntax for pattern
     1.8 +aliases as known from Haskell, Scala and ML.
     1.9 +
    1.10  * Constant "subseq" in Topological_Spaces removed and subsumed by
    1.11  "strict_mono". Some basic lemmas specific to "subseq" have been renamed
    1.12  accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.
     2.1 --- a/src/HOL/Library/Library.thy	Thu Aug 17 22:29:30 2017 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Fri Aug 18 14:57:23 2017 +0200
     2.3 @@ -52,6 +52,7 @@
     2.4    Option_ord
     2.5    Order_Continuity
     2.6    Parallel
     2.7 +  Pattern_Aliases
     2.8    Periodic_Fun
     2.9    Perm
    2.10    Permutation
    2.11 @@ -82,4 +83,4 @@
    2.12    While_Combinator
    2.13  begin
    2.14  end
    2.15 -(*>*)
    2.16 \ No newline at end of file
    2.17 +(*>*)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Pattern_Aliases.thy	Fri Aug 18 14:57:23 2017 +0200
     3.3 @@ -0,0 +1,114 @@
     3.4 +(*  Title:      HOL/Library/Pattern_Aliases.thy
     3.5 +    Author:     Lars Hupel, Ondrej Kuncar
     3.6 +*)
     3.7 +
     3.8 +section \<open>Input syntax for pattern aliases (or ``as-patterns'' in Haskell)\<close>
     3.9 +
    3.10 +theory Pattern_Aliases
    3.11 +imports Main
    3.12 +begin
    3.13 +
    3.14 +text \<open>
    3.15 +  Most functional languages (Haskell, ML, Scala) support aliases in patterns. This allows to refer
    3.16 +  to a subpattern with a variable name. This theory implements this using a check phase. It works
    3.17 +  well for function definitions (see usage below).
    3.18 +
    3.19 +  The following caveats should be kept in mind:
    3.20 +  \<^item> The translation expects a term of the form @{prop "f x y = rhs"}, where \<open>x\<close> and \<open>y\<close> are patterns
    3.21 +    that may contain aliases. The result of the translation is a nested @{const Let}-expression on
    3.22 +    the right hand side. The code generator \<^emph>\<open>does not\<close> print Isabelle pattern aliases to target
    3.23 +    language pattern aliases.
    3.24 +  \<^item> The translation does not process nested equalities; only the top-level equality is translated.
    3.25 +  \<^item> Terms that do not adhere to the above shape may either stay untranslated or produce an error
    3.26 +    message. The @{command fun} command will complain if pattern aliases are left untranslated.
    3.27 +    In particular, there are no checks whether the patterns are wellformed or linear.
    3.28 +  \<^item> There is no corresonding uncheck phase, because it is unclear in which situations the
    3.29 +    translation should be reversed.
    3.30 +\<close>
    3.31 +
    3.32 +
    3.33 +subsection \<open>Definition\<close>
    3.34 +
    3.35 +consts as :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    3.36 +
    3.37 +ML\<open>
    3.38 +local
    3.39 +
    3.40 +fun let_typ a b = a --> (a --> b) --> b
    3.41 +
    3.42 +fun strip_all t =
    3.43 +  case try Logic.dest_all t of
    3.44 +    NONE => ([], t)
    3.45 +  | SOME (var, t) => apfst (cons var) (strip_all t)
    3.46 +
    3.47 +fun all_Frees t =
    3.48 +  fold_aterms (fn Free (x, t) => insert op = (x, t) | _ => I) t []
    3.49 +
    3.50 +in
    3.51 +
    3.52 +fun check_pattern_syntax t =
    3.53 +  case strip_all t of
    3.54 +    (vars, @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs)) =>
    3.55 +      let
    3.56 +        fun go (Const (@{const_name as}, _) $ pat $ var, rhs) =
    3.57 +              let
    3.58 +                val (pat', rhs') = go (pat, rhs)
    3.59 +                val _ = if is_Free var then () else error "Left-hand side of =: must be a free variable"
    3.60 +                val rhs'' =
    3.61 +                  Const (@{const_name Let}, let_typ (fastype_of var) (fastype_of rhs)) $
    3.62 +                    pat' $ lambda var rhs'
    3.63 +              in
    3.64 +                (pat', rhs'')
    3.65 +              end
    3.66 +          | go (t $ u, rhs) =
    3.67 +              let
    3.68 +                val (t', rhs') = go (t, rhs)
    3.69 +                val (u', rhs'') = go (u, rhs')
    3.70 +              in (t' $ u', rhs'') end
    3.71 +          | go (t, rhs) = (t, rhs)
    3.72 +
    3.73 +        val (lhs', rhs') = go (lhs, rhs)
    3.74 +
    3.75 +        val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs'))
    3.76 +
    3.77 +        val frees = filter (member op = vars) (all_Frees res)
    3.78 +      in fold (fn v => Logic.dependent_all_name ("", v)) (map Free frees) res end
    3.79 +  | _ => t
    3.80 +
    3.81 +end
    3.82 +\<close>
    3.83 +
    3.84 +bundle pattern_aliases begin
    3.85 +
    3.86 +  notation as (infixr "=:" 1)
    3.87 +
    3.88 +  declaration \<open>K (Syntax_Phases.term_check 98 "pattern_syntax" (K (map check_pattern_syntax)))\<close>
    3.89 +
    3.90 +end
    3.91 +
    3.92 +hide_const (open) as
    3.93 +
    3.94 +
    3.95 +subsection \<open>Usage\<close>
    3.96 +
    3.97 +context includes pattern_aliases begin
    3.98 +
    3.99 +text \<open>Not very useful for plain definitions, but works anyway.\<close>
   3.100 +
   3.101 +private definition "test_1 x (y =: z) = y + z"
   3.102 +
   3.103 +lemma "test_1 x y = y + y"
   3.104 +by (rule test_1_def[unfolded Let_def])
   3.105 +
   3.106 +text \<open>Very useful for function definitions.\<close>
   3.107 +
   3.108 +private fun test_2 where
   3.109 +"test_2 (y # (y' # ys =: x') =: x) = x @ x'" |
   3.110 +"test_2 _ = []"
   3.111 +
   3.112 +lemma "test_2 (y # y' # ys) = (y # y' # ys) @ y' # ys"
   3.113 +by (rule test_2.simps[unfolded Let_def])
   3.114 +
   3.115 +end
   3.116 +
   3.117 +end
   3.118 \ No newline at end of file