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