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