Theory TermPatternAntiquote_Tests

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory TermPatternAntiquote_Tests
imports
  TermPatternAntiquote
  Main
begin

text ‹
  Term pattern matching utility.

  Instead of writing monstrosities such as

  @{verbatim ‹
    case t of
      Const ("Pure.imp", _) $
        P $
        Const (@{const_name Trueprop}, _) $
          (Const ("HOL.eq", _) $
            (Const (@{const_name "my_func"}, _) $ x) $ y)
      => (P, x, y)
  ›}

  simply use a term pattern with variables:

  @{verbatim ‹
    case t of
      @{term_pat "PROP ?P ⟹ my_func ?x = ?y"} => (P, x, y)
  ›}

  Each ‹term_pat› generates an ML pattern that can be used in any
  case-expression or name binding.
  The ML pattern matches directly on the term datatype; it does not
  perform matching in the Isabelle logic.

  Schematic variables in the pattern generate ML variables.
  The variables must obey ML's pattern matching rules, i.e.
  each can appear only once.

  Due to the difficulty of enforcing this rule for type variables,
  schematic type variables are ignored and not checked.
›

text ‹
  Example: evaluate arithmetic expressions in ML.
›
ML_val ‹
fun eval_num @{term_pat "numeral ?n"} = HOLogic.dest_numeral n
  | eval_num @{term_pat "Suc ?n"} = eval_num n + 1
  | eval_num @{term_pat "0"} = 0
  | eval_num @{term_pat "1"} = 1
  | eval_num @{term_pat "?x + ?y"} = eval_num x + eval_num y
  | eval_num @{term_pat "?x - ?y"} = eval_num x - eval_num y
  | eval_num @{term_pat "?x * ?y"} = eval_num x * eval_num y
  | eval_num @{term_pat "?x div ?y"} = eval_num x div eval_num y
  | eval_num t = raise TERM ("eval_num", [t]);

eval_num @{term "(1 + 2) * 3 - 4 div 5"}
›

text ‹Regression test: backslash handling›
ML_val ‹
val @{term_pat "α"} = @{term "α"}
›

text ‹Regression test: special-casing for dummy vars›
ML_val ‹
val @{term_pat "λx y. _"} = @{term "λx y. z"}
›

end