1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory TermPatternAntiquote_Tests
8imports
9  Lib.TermPatternAntiquote
10  Main
11begin
12
13text \<open>
14  Term pattern matching utility.
15
16  Instead of writing monstrosities such as
17
18  @{verbatim \<open>
19    case t of
20      Const ("Pure.imp", _) $
21        P $
22        Const (@{const_name Trueprop}, _) $
23          (Const ("HOL.eq", _) $
24            (Const (@{const_name "my_func"}, _) $ x) $ y)
25      => (P, x, y)
26  \<close>}
27
28  simply use a term pattern with variables:
29
30  @{verbatim \<open>
31    case t of
32      @{term_pat "PROP ?P \<Longrightarrow> my_func ?x = ?y"} => (P, x, y)
33  \<close>}
34
35  Each term_pat generates an ML pattern that can be used in any
36  case-expression or name binding.
37  The ML pattern matches directly on the term datatype; it does not
38  perform matching in the Isabelle logic.
39
40  Schematic variables in the pattern generate ML variables.
41  The variables must obey ML's pattern matching rules, i.e.
42  each can appear only once.
43
44  Due to the difficulty of enforcing this rule for type variables,
45  schematic type variables are ignored and not checked.
46\<close>
47
48text \<open>
49  Example: evaluate arithmetic expressions in ML.
50\<close>
51ML_val \<open>
52fun eval_num @{term_pat "numeral ?n"} = HOLogic.dest_numeral n
53  | eval_num @{term_pat "Suc ?n"} = eval_num n + 1
54  | eval_num @{term_pat "0"} = 0
55  | eval_num @{term_pat "1"} = 1
56  | eval_num @{term_pat "?x + ?y"} = eval_num x + eval_num y
57  | eval_num @{term_pat "?x - ?y"} = eval_num x - eval_num y
58  | eval_num @{term_pat "?x * ?y"} = eval_num x * eval_num y
59  | eval_num @{term_pat "?x div ?y"} = eval_num x div eval_num y
60  | eval_num t = raise TERM ("eval_num", [t]);
61
62eval_num @{term "(1 + 2) * 3 - 4 div 5"}
63\<close>
64
65text \<open>Regression test: backslash handling\<close>
66ML_val \<open>
67val @{term_pat "\<alpha>"} = @{term "\<alpha>"}
68\<close>
69
70text \<open>Regression test: special-casing for dummy vars\<close>
71ML_val \<open>
72val @{term_pat "\<lambda>x y. _"} = @{term "\<lambda>x y. z"}
73\<close>
74
75end