1 (* Title: Pure/Isar/term_style.ML |
|
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
|
4 |
|
5 Styles for terms, to use with the "term_style" and "thm_style" |
|
6 antiquotations. |
|
7 *) |
|
8 |
|
9 signature TERM_STYLE = |
|
10 sig |
|
11 val the_style: theory -> string -> (Proof.context -> term -> term) |
|
12 val add_style: string -> (Proof.context -> term -> term) -> theory -> theory |
|
13 val print_styles: theory -> unit |
|
14 end; |
|
15 |
|
16 structure TermStyle: TERM_STYLE = |
|
17 struct |
|
18 |
|
19 (* style data *) |
|
20 |
|
21 fun err_dup_styles names = |
|
22 error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names); |
|
23 |
|
24 structure StyleData = TheoryDataFun |
|
25 (struct |
|
26 val name = "Isar/antiquote_style"; |
|
27 type T = ((Proof.context -> term -> term) * stamp) Symtab.table; |
|
28 val empty = Symtab.empty; |
|
29 val copy = I; |
|
30 val extend = I; |
|
31 fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs |
|
32 handle Symtab.DUPS dups => err_dup_styles dups; |
|
33 fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab)); |
|
34 end); |
|
35 |
|
36 val _ = Context.add_setup StyleData.init; |
|
37 val print_styles = StyleData.print; |
|
38 |
|
39 |
|
40 (* accessors *) |
|
41 |
|
42 fun the_style thy name = |
|
43 (case Symtab.lookup (StyleData.get thy) name of |
|
44 NONE => error ("Unknown antiquote style: " ^ quote name) |
|
45 | SOME (style, _) => style); |
|
46 |
|
47 fun add_style name style thy = |
|
48 StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy |
|
49 handle Symtab.DUP _ => err_dup_styles [name]; |
|
50 |
|
51 |
|
52 (* predefined styles *) |
|
53 |
|
54 fun style_binargs ctxt t = |
|
55 let |
|
56 val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt) |
|
57 (Logic.strip_imp_concl t) |
|
58 in |
|
59 case concl of (_ $ l $ r) => (l, r) |
|
60 | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl) |
|
61 end; |
|
62 |
|
63 fun style_parm_premise i ctxt t = |
|
64 let val prems = Logic.strip_imp_prems t in |
|
65 if i <= length prems then nth prems (i - 1) |
|
66 else error ("Not enough premises for prem" ^ string_of_int i ^ |
|
67 " in propositon: " ^ ProofContext.string_of_term ctxt t) |
|
68 end; |
|
69 |
|
70 val _ = Context.add_setup |
|
71 (add_style "lhs" (fst oo style_binargs) #> |
|
72 add_style "rhs" (snd oo style_binargs) #> |
|
73 add_style "prem1" (style_parm_premise 1) #> |
|
74 add_style "prem2" (style_parm_premise 2) #> |
|
75 add_style "prem3" (style_parm_premise 3) #> |
|
76 add_style "prem4" (style_parm_premise 4) #> |
|
77 add_style "prem5" (style_parm_premise 5) #> |
|
78 add_style "prem6" (style_parm_premise 6) #> |
|
79 add_style "prem7" (style_parm_premise 7) #> |
|
80 add_style "prem8" (style_parm_premise 8) #> |
|
81 add_style "prem9" (style_parm_premise 9) #> |
|
82 add_style "prem10" (style_parm_premise 10) #> |
|
83 add_style "prem11" (style_parm_premise 11) #> |
|
84 add_style "prem12" (style_parm_premise 12) #> |
|
85 add_style "prem13" (style_parm_premise 13) #> |
|
86 add_style "prem14" (style_parm_premise 14) #> |
|
87 add_style "prem15" (style_parm_premise 15) #> |
|
88 add_style "prem16" (style_parm_premise 16) #> |
|
89 add_style "prem17" (style_parm_premise 17) #> |
|
90 add_style "prem18" (style_parm_premise 18) #> |
|
91 add_style "prem19" (style_parm_premise 19) #> |
|
92 add_style "concl" (K Logic.strip_imp_concl)); |
|
93 |
|
94 end; |
|