Theory Pattern_Aliases

theory Pattern_Aliases
imports Main
(*  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

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 (@{theory_text ‹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›

  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)"


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
    NONE => ([], t)
  | SOME (var, t) => apfst (cons var) (strip_all t)

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

fun subst_once (old, new) t =
    fun go t =
      if t = old then
        (new, true)
        case t of
          u $ v =>
              val (u', substituted) = go u
              if substituted then
                (u' $ v, true)
                case go v of (v', substituted) => (u $ v', substituted)
        | 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 (@{const_name fake_quant}, (T --> propT) --> propT);

fun dependent_fake_name v t =
    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


fun check_pattern_syntax t =
  case strip_all t of
    (vars, @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs)) =>
        fun go (Const (@{const_name as}, _) $ pat $ var, rhs) =
                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 (@{const_name Let}, let_typ (fastype_of var) (fastype_of rhs)) $
                    pat' $ lambda var rhs'
                (pat', rhs'')
          | go (t $ u, rhs) =
                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, @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs)) =>
        (* restricted to going down abstractions; ignores eta-contracted rhs *)
        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
                  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)
                  go lhs' rhs' ctxt' (Free (name', typ) :: frees)
                (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
        if null frees then t else res
  | _ => t


bundle pattern_aliases begin

  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]
  declare Let_def [simp]


hide_const as
hide_const fake_quant

subsection ‹Usage›

context includes pattern_aliases begin

text ‹Not very useful for plain definitions, but works anyway.›

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 ‹Very useful for function definitions.›

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])

  val actual =
    @{thm test_2.simps(1)}
    |> Thm.prop_of
    |> Syntax.string_of_term @{context}
    |> YXML.content_of
  val expected = "test_2 (?y # (?y' # ?ys =: x') =: x) = x @ x' @ x'"
in @{assert} (actual = expected) end