Quelle  Pattern_Aliases.thy

(*  Title:      HOL/Library/Pattern_Aliases.thy
    Author:     Lars Hupel, Ondrej Kuncar, Tobias Nipkow
*)

section ‹Input syntax for pattern aliases (or ``as-patterns'' in Haskell)›

theory Pattern_Aliases
imports Main
begin

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). All features are packed into a @{command bundle}.

 The following caveats should be kept in mind:
 ▪ The translation expects a term of the form prop‹f x y = rhs›, where ‹x› and ‹y› are patterns
 that may contain aliases. The result of the translation is a nested const‹Let›-expression on
 the right hand side. The code generator 🪙‹does not› print Isabelle pattern aliases to target
 language pattern aliases.
 ▪ The translation does not process nested equalities; only the top-level equality is translated.
 ▪ 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.
 ▪ The corresponding uncheck phase attempts to reverse the translation (no guarantee). The
 additionally introduced variables are bound using a ``fake quantifier'' that does not
 appear in the output.
 ▪ 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)! In some circumstances
 (using ‹let› to destructure tuples), the internal construction of functions stumbles over this
 rule and prints an error. To mitigate this, either
 ▪ activate the bundle locally (🪙‹context includes ... begin›) or
 ▪ rewrite the ‹let›-expression to use ‹case›: term‹let (a, b) = x in (b, a)› becomes
 term‹case x of (a, b) ==> (b, a)›.
 ▪ The bundle also adds the @{thm Let_def} rule to the simpset.
 ›


subsection ‹Definition›

consts
  as :: "'a ==> 'a ==> 'a"
  fake_quant :: "('a ==> prop) ==> prop"

lemma let_cong_unfolding: "M = N ==> f N = g N ==> Let M f = Let N g"
by simp

translations "P" <= "CONST fake_quant (λx. P)"

ML‹
 

  let_typ a b = a --> (a --> b) --> b
  as_typ a = a --> a --> a

  strip_all t =
 case try Logic.dest_all_global t of
 NONE => ([], t)
 | SOME (var, t) => apfst (cons var) (strip_all t)

  all_Frees t =
 fold_aterms (fn Free (x, t) => insert (op =) (x, t) | _ => I) t []

  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

(* adapted from logic.ML *)
fun fake_const T = Const (🍋‹fake_quant›, (T --> propT) --> propT);

fun dependent_fake_name v t =
  let
    val x = Term.term_name v
    val T = Term.fastype_of v
    val t' = Term.abstract_over (v, t)
  in if Term.is_dependent t' then fake_const T $ Abs (x, T, t') else t end

in

fun check_pattern_syntax t =
  case strip_all t of
    (vars, 🍋‹Trueprop› $ (Const (🍋‹HOL.eq›, _) $ lhs $ rhs)) =>
      let
        fun go (Const (🍋‹as›, _) $ pat $ var, rhs) =
              let
                val (pat', rhs') = go (pat, rhs)
                val _ = if is_Free var then () else error "Right-hand side of =: must be a free variable"
                val rhs'' =
                  Const (🍋‹Let›, let_typ (fastype_of var) (fastype_of rhs)) $
                    pat' $ lambda var rhs'
              in
                (pat', rhs'')
              end
          | go (t $ u, rhs) =
              let
                val (t', rhs') = go (t, rhs)
                val (u', rhs'') = go (u, rhs')
              in (t' $ u', rhs'') end
          | go (t, rhs) = (t, rhs)

        val (lhs', rhs') = go (lhs, rhs)

        val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs'))

        val frees = filter (member (op =) vars) (all_Frees res)
      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, 🍋‹Trueprop› $ (Const (🍋‹HOL.eq›, _) $ lhs $ rhs)) =>
      let
        (* restricted to going down abstractions; ignores eta-contracted rhs *)
        fun go lhs (rhs as Const (🍋‹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 (🍋‹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)
          |> fold dependent_fake_name frees
      in
        if null frees then t else res
      end
  | _ => t

end
›

bundle pattern_aliases begin

  notation as (infixr ‹=:› 1)

  declaration \<open>K (Syntax_Phases.term_check 98 "pattern_syntax" (K (map check_pattern_syntax)))\<close>
  declaration \<open>K (Syntax_Phases.term_uncheck 98 "pattern_syntax" (map o uncheck_pattern_syntax))\<close>

  declare let_cong_unfolding [fundef_cong]
  declare Let_def [simp]

end

hide_const as
hide_const fake_quant


subsection \<open>Usage\<close>

context includes pattern_aliases begin

text \<open>Not very useful for plain definitions, but works anyway.\<close>

private definition "test_1 x (y =: z) = y + z"

lemma "test_1 x y = y + y"
by (rule test_1_def[unfolded Let_def])

text \<open>Very useful for function definitions.\<close>

private fun test_2 where
"test_2 (y # (y' # ys =: x') =: x) = x @ x' @ x'" |
"test_2 _ = []"

lemma "test_2 (y # y' # ys) = (y # y' # ys) @ (y' # ys) @ (y' # ys)"
by (rule test_2.simps[unfolded Let_def])

ML\<open>
let
  val actual =
    @{thm test_2.simps(1)}
    |> Thm.prop_of
    |> Syntax.pretty_term \<^context>
    |> Pretty.pure_string_of
  val expected = "test_2 (?y # (?y' # ?ys =: x') =: x) = x @ x' @ x'"
in \<^assert> (actual = expected) end
\<close>

end

end