1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7text \<open>
8  term_pat: ML antiquotation for pattern matching on terms.
9
10  See TermPatternAntiquote_Tests for examples and tests.
11\<close>
12theory TermPatternAntiquote imports
13  Pure
14begin
15
16ML \<open>
17structure Term_Pattern_Antiquote = struct
18
19val quote_string = quote
20
21(* typ matching; doesn't support matching on named TVars.
22 * This is because each TVar is likely to appear many times in the pattern. *)
23fun gen_typ_pattern (TVar _) = "_"
24  | gen_typ_pattern (TFree (v, sort)) =
25      "Term.TFree (" ^ quote_string v ^ ", [" ^ commas (map quote_string sort) ^ "])"
26  | gen_typ_pattern (Type (typ_head, args)) =
27      "Term.Type (" ^ quote_string typ_head ^ ", [" ^ commas (map gen_typ_pattern args) ^ "])"
28
29(* term matching; does support matching on named (non-dummy) Vars.
30 * The ML var generated will be identical to the Var name except in
31 * indexed names like "?v1.2", which creates the var "v12". *)
32fun gen_term_pattern (Var (("_dummy_", _), _)) = "_"
33  | gen_term_pattern (Var ((v, 0), _)) = v
34  | gen_term_pattern (Var ((v, n), _)) = v ^ string_of_int n
35  | gen_term_pattern (Const (n, typ)) =
36      "Term.Const (" ^ quote_string n ^ ", " ^ gen_typ_pattern typ ^ ")"
37  | gen_term_pattern (Free (n, typ)) =
38      "Term.Free (" ^ quote_string n ^ ", " ^ gen_typ_pattern typ ^ ")"
39  | gen_term_pattern (t as f $ x) =
40      (* (read_term_pattern "_") "helpfully" generates a dummy var that is
41       * applied to all bound vars in scope. We go back and remove them. *)
42      let fun default () = "(" ^ gen_term_pattern f ^ " $ " ^ gen_term_pattern x ^ ")";
43      in case strip_comb t of
44             (h as Var (("_dummy_", _), _), bs) =>
45               if forall is_Bound bs then gen_term_pattern h else default ()
46           | _ => default () end
47  | gen_term_pattern (Abs (_, typ, t)) =
48      "Term.Abs (_, " ^ gen_typ_pattern typ ^ ", " ^ gen_term_pattern t ^ ")"
49  | gen_term_pattern (Bound n) = "Bound " ^ string_of_int n
50
51(* Create term pattern. All Var names must be distinct in order to generate ML variables. *)
52fun term_pattern_antiquote ctxt s =
53  let val pat = Proof_Context.read_term_pattern ctxt s
54      val add_var_names' = fold_aterms (fn Var (v, _) => curry (::) v | _ => I);
55      val vars = add_var_names' pat [] |> filter (fn (n, _) => n <> "_dummy_")
56      val _ = if vars = distinct (=) vars then () else
57                raise TERM ("Pattern contains duplicate vars", [pat])
58  in "(" ^ gen_term_pattern pat ^ ")" end
59
60end;
61val _ = Context.>> (Context.map_theory (
62    ML_Antiquotation.inline @{binding "term_pat"}
63      ((Args.context -- Scan.lift Args.embedded_inner_syntax)
64         >> uncurry Term_Pattern_Antiquote.term_pattern_antiquote)))
65\<close>
66
67end
68