author | wenzelm |
Sun, 08 Nov 2009 18:43:42 +0100 | |
changeset 33522 | 737589bb9bb8 |
parent 33184 | de8cc01e8d9e |
child 35625 | 9c818cab0dd0 |
permissions | -rw-r--r-- |
22107 | 1 |
(* Title: Pure/Thy/term_style.ML |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
||
32890
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
4 |
Styles for term printing. |
22107 | 5 |
*) |
6 |
||
7 |
signature TERM_STYLE = |
|
8 |
sig |
|
32890
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
9 |
val setup: string -> (Proof.context -> term -> term) parser -> theory -> theory |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
10 |
val parse: (term -> term) context_parser |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
11 |
val parse_bare: (term -> term) context_parser |
22107 | 12 |
end; |
13 |
||
32890
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
14 |
structure Term_Style: TERM_STYLE = |
22107 | 15 |
struct |
16 |
||
17 |
(* style data *) |
|
18 |
||
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23577
diff
changeset
|
19 |
fun err_dup_style name = |
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23577
diff
changeset
|
20 |
error ("Duplicate declaration of antiquote style: " ^ quote name); |
22107 | 21 |
|
33522 | 22 |
structure StyleData = Theory_Data |
22846 | 23 |
( |
32890
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
24 |
type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table; |
22107 | 25 |
val empty = Symtab.empty; |
26 |
val extend = I; |
|
33522 | 27 |
fun merge data : T = Symtab.merge (eq_snd (op =)) data |
23655
d2d1138e0ddc
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
wenzelm
parents:
23577
diff
changeset
|
28 |
handle Symtab.DUP dup => err_dup_style dup; |
22846 | 29 |
); |
22107 | 30 |
|
31 |
||
32 |
(* accessors *) |
|
33 |
||
34 |
fun the_style thy name = |
|
35 |
(case Symtab.lookup (StyleData.get thy) name of |
|
36 |
NONE => error ("Unknown antiquote style: " ^ quote name) |
|
37 |
| SOME (style, _) => style); |
|
38 |
||
32890
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
39 |
fun setup name style thy = |
22107 | 40 |
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
|
41 |
handle Symtab.DUP _ => err_dup_style name; |
22107 | 42 |
|
43 |
||
32890
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
44 |
(* style parsing *) |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
45 |
|
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
46 |
fun parse_single ctxt = OuterParse.position (OuterParse.xname -- Args.parse) |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
47 |
>> (fn x as ((name, _), _) => fst (Args.context_syntax "style" |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
48 |
(Scan.lift (the_style (ProofContext.theory_of ctxt) name)) |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
49 |
(Args.src x) ctxt |>> (fn f => f ctxt))); |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
50 |
|
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
51 |
val parse = Args.context :|-- (fn ctxt => Scan.lift |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
52 |
(Args.parens (parse_single ctxt ::: Scan.repeat (Args.$$$ "," |-- parse_single ctxt)) |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
53 |
>> fold I |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
54 |
|| Scan.succeed I)); |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
55 |
|
33184 | 56 |
val parse_bare = Args.context :|-- (fn ctxt => (Output.legacy_feature "Old-style antiquotation style."; |
57 |
Scan.lift Args.liberal_name |
|
32890
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
58 |
>> (fn name => fst (Args.context_syntax "style" |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
59 |
(Scan.lift (the_style (ProofContext.theory_of ctxt) name)) |
33184 | 60 |
(Args.src (("style", []), Position.none)) ctxt |>> (fn f => f ctxt))))); |
32890
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
61 |
|
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
62 |
|
22107 | 63 |
(* predefined styles *) |
64 |
||
32891 | 65 |
fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t => |
22107 | 66 |
let |
67 |
val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt) |
|
68 |
(Logic.strip_imp_concl t) |
|
69 |
in |
|
32890
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
70 |
case concl of (_ $ l $ r) => proj (l, r) |
24920 | 71 |
| _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl) |
32890
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
72 |
end); |
22107 | 73 |
|
32891 | 74 |
val style_prem = Args.name >> (fn raw_i => fn ctxt => fn t => |
75 |
let |
|
76 |
val i = (the o Int.fromString) raw_i; |
|
77 |
val prems = Logic.strip_imp_prems t; |
|
78 |
in |
|
79 |
if i <= length prems then nth prems (i - 1) |
|
80 |
else error ("Not enough premises for prem " ^ string_of_int i ^ |
|
81 |
" in propositon: " ^ Syntax.string_of_term ctxt t) |
|
82 |
end); |
|
83 |
||
32890
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
84 |
fun style_parm_premise i = Scan.succeed (fn ctxt => fn t => |
32891 | 85 |
let |
86 |
val i_str = string_of_int i; |
|
33184 | 87 |
val _ = Output.legacy_feature (quote ("prem" ^ i_str) |
88 |
^ " term style encountered; use explicit argument syntax " |
|
89 |
^ quote ("prem " ^ i_str) ^ " instead."); |
|
32891 | 90 |
val prems = Logic.strip_imp_prems t; |
91 |
in |
|
22107 | 92 |
if i <= length prems then nth prems (i - 1) |
33184 | 93 |
else error ("Not enough premises for prem" ^ i_str ^ |
24920 | 94 |
" in propositon: " ^ Syntax.string_of_term ctxt t) |
32890
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
95 |
end); |
22107 | 96 |
|
26463 | 97 |
val _ = Context.>> (Context.map_theory |
32891 | 98 |
(setup "lhs" (style_lhs_rhs fst) #> |
99 |
setup "rhs" (style_lhs_rhs snd) #> |
|
100 |
setup "prem" style_prem #> |
|
101 |
setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #> |
|
32890
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
102 |
setup "prem1" (style_parm_premise 1) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
103 |
setup "prem2" (style_parm_premise 2) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
104 |
setup "prem3" (style_parm_premise 3) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
105 |
setup "prem4" (style_parm_premise 4) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
106 |
setup "prem5" (style_parm_premise 5) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
107 |
setup "prem6" (style_parm_premise 6) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
108 |
setup "prem7" (style_parm_premise 7) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
109 |
setup "prem8" (style_parm_premise 8) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
110 |
setup "prem9" (style_parm_premise 9) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
111 |
setup "prem10" (style_parm_premise 10) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
112 |
setup "prem11" (style_parm_premise 11) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
113 |
setup "prem12" (style_parm_premise 12) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
114 |
setup "prem13" (style_parm_premise 13) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
115 |
setup "prem14" (style_parm_premise 14) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
116 |
setup "prem15" (style_parm_premise 15) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
117 |
setup "prem16" (style_parm_premise 16) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
118 |
setup "prem17" (style_parm_premise 17) #> |
77df12652210
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
haftmann
parents:
29606
diff
changeset
|
119 |
setup "prem18" (style_parm_premise 18) #> |
32891 | 120 |
setup "prem19" (style_parm_premise 19))); |
22107 | 121 |
|
122 |
end; |