|
1 (* Title: HOL/ex/Term_Of_Syntax.thy |
|
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Input syntax for term_of functions *} |
|
7 |
|
8 theory Term_Of_Syntax |
|
9 imports Code_Eval |
|
10 begin |
|
11 |
|
12 setup {* |
|
13 Sign.declare_const [] ((Name.binding "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn) |
|
14 #> snd |
|
15 *} |
|
16 |
|
17 notation (output) |
|
18 rterm_of ("\<guillemotleft>_\<guillemotright>") |
|
19 |
|
20 locale rterm_syntax = |
|
21 fixes rterm_of_syntax :: "'a \<Rightarrow> 'b" ("\<guillemotleft>_\<guillemotright>") |
|
22 |
|
23 parse_translation {* |
|
24 let |
|
25 fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t |
|
26 | rterm_of_tr ts = raise TERM ("rterm_of_tr", ts); |
|
27 in |
|
28 [(Syntax.fixedN ^ "rterm_of_syntax", rterm_of_tr)] |
|
29 end |
|
30 *} |
|
31 |
|
32 setup {* |
|
33 let |
|
34 val subst_rterm_of = Eval.mk_term |
|
35 (fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v)) |
|
36 (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))); |
|
37 fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t |
|
38 | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) = |
|
39 error ("illegal number of arguments for " ^ quote @{const_name rterm_of}) |
|
40 | subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts); |
|
41 fun subst_rterm_of'' t = |
|
42 let |
|
43 val t' = subst_rterm_of' (strip_comb t); |
|
44 in if t aconv t' |
|
45 then NONE |
|
46 else SOME t' |
|
47 end; |
|
48 fun check_rterm_of ts ctxt = |
|
49 let |
|
50 val ts' = map subst_rterm_of'' ts; |
|
51 in if exists is_some ts' |
|
52 then SOME (map2 the_default ts ts', ctxt) |
|
53 else NONE |
|
54 end; |
|
55 in |
|
56 Context.theory_map (Syntax.add_term_check 0 "rterm_of" check_rterm_of) |
|
57 end; |
|
58 *} |
|
59 |
|
60 end |