author | haftmann |
Tue, 20 Sep 2005 08:21:49 +0200 | |
changeset 17496 | 26535df536ae |
parent 17412 | e26cb20ef0cc |
child 18708 | 4b3dadb4fe33 |
permissions | -rw-r--r-- |
15918 | 1 |
(* Title: Pure/Isar/term_style.ML |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
||
17221 | 5 |
Styles for terms, to use with the "term_style" and "thm_style" |
6 |
antiquotations. |
|
15918 | 7 |
*) |
8 |
||
15960 | 9 |
signature TERM_STYLE = |
15918 | 10 |
sig |
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
11 |
val the_style: theory -> string -> (Proof.context -> term -> term) |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
12 |
val add_style: string -> (Proof.context -> term -> term) -> theory -> theory |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
13 |
val print_styles: theory -> unit |
15918 | 14 |
end; |
15 |
||
15960 | 16 |
structure TermStyle: TERM_STYLE = |
15918 | 17 |
struct |
18 |
||
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
19 |
(* style data *) |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
20 |
|
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
21 |
fun err_dup_styles names = |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
22 |
error ("Duplicate declaration of antiquote style(s): " ^ commas_quote names); |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
23 |
|
16424 | 24 |
structure StyleData = TheoryDataFun |
25 |
(struct |
|
16541 | 26 |
val name = "Isar/antiquote_style"; |
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
27 |
type T = ((Proof.context -> term -> term) * stamp) Symtab.table; |
15960 | 28 |
val empty = Symtab.empty; |
15918 | 29 |
val copy = I; |
16424 | 30 |
val extend = I; |
17496 | 31 |
fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs |
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
32 |
handle Symtab.DUPS dups => err_dup_styles dups; |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
33 |
fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab)); |
16424 | 34 |
end); |
15918 | 35 |
|
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
36 |
val _ = Context.add_setup [StyleData.init]; |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
37 |
val print_styles = StyleData.print; |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
38 |
|
15918 | 39 |
|
40 |
(* accessors *) |
|
41 |
||
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
42 |
fun the_style thy name = |
17412 | 43 |
(case Symtab.lookup (StyleData.get thy) name of |
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
44 |
NONE => error ("Unknown antiquote style: " ^ quote name) |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
45 |
| SOME (style, _) => style); |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
46 |
|
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
47 |
fun add_style name style thy = |
17412 | 48 |
StyleData.map (Symtab.update_new (name, (style, stamp ()))) thy |
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
49 |
handle Symtab.DUP _ => err_dup_styles [name]; |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
50 |
|
15918 | 51 |
|
52 |
(* predefined styles *) |
|
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
53 |
|
15960 | 54 |
fun style_binargs ctxt t = |
16424 | 55 |
let |
56 |
val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt) |
|
57 |
(Logic.strip_imp_concl t) |
|
58 |
in |
|
15960 | 59 |
case concl of (_ $ l $ r) => (l, r) |
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
60 |
| _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl) |
15960 | 61 |
end; |
15918 | 62 |
|
16167 | 63 |
fun style_parm_premise i ctxt t = |
16424 | 64 |
let val prems = Logic.strip_imp_prems t in |
65 |
if i <= length prems then List.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) |
|
16160 | 68 |
end; |
16167 | 69 |
|
15990
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
70 |
val _ = Context.add_setup |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
71 |
[add_style "lhs" (fst oo style_binargs), |
4ef32dcbb44f
substantial tuning -- adapted to common conventions;
wenzelm
parents:
15961
diff
changeset
|
72 |
add_style "rhs" (snd oo style_binargs), |
16167 | 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), |
|
17392 | 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), |
|
16165 | 92 |
add_style "concl" (K Logic.strip_imp_concl)]; |
15918 | 93 |
end; |