author | wenzelm |
Wed, 23 Jul 2014 21:01:28 +0200 | |
changeset 57625 | 2a9d8dcea893 |
parent 56204 | f70e69208a8c |
child 58011 | bc6bced136e5 |
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 |
|
56030 | 9 |
val setup: binding -> (Proof.context -> term -> term) parser -> theory -> theory |
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
|
10 |
val parse: (term -> term) context_parser |
22107 | 11 |
end; |
12 |
||
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
|
13 |
structure Term_Style: TERM_STYLE = |
22107 | 14 |
struct |
15 |
||
56030 | 16 |
(* theory data *) |
22107 | 17 |
|
56030 | 18 |
structure Data = Theory_Data |
22846 | 19 |
( |
56030 | 20 |
type T = (Proof.context -> term -> term) parser Name_Space.table; |
21 |
val empty : T = Name_Space.empty_table "antiquotation_style"; |
|
22107 | 22 |
val extend = I; |
56030 | 23 |
fun merge data : T = Name_Space.merge_tables data; |
22846 | 24 |
); |
22107 | 25 |
|
56030 | 26 |
val get_data = Data.get o Proof_Context.theory_of; |
27 |
val get_style = Name_Space.get o get_data; |
|
22107 | 28 |
|
56030 | 29 |
fun setup binding style thy = |
30 |
Data.map (#2 o Name_Space.define (Context.Theory thy) true (binding, style)) thy; |
|
22107 | 31 |
|
32 |
||
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
|
33 |
(* 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
|
34 |
|
56030 | 35 |
fun parse_single ctxt = |
56201 | 36 |
Parse.position Parse.xname -- Parse.args >> (fn (name, args) => |
56030 | 37 |
let |
56032
b034b9f0fa2a
clarified Args.check_src: retain name space information for error output;
wenzelm
parents:
56030
diff
changeset
|
38 |
val (src, parse) = Args.check_src ctxt (get_data ctxt) (Args.src name args); |
b034b9f0fa2a
clarified Args.check_src: retain name space information for error output;
wenzelm
parents:
56030
diff
changeset
|
39 |
val (f, _) = Args.syntax (Scan.lift parse) src ctxt; |
56030 | 40 |
in f ctxt end); |
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
|
41 |
|
50637 | 42 |
val parse = Args.context :|-- (fn ctxt => Scan.lift |
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
|
43 |
(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
|
44 |
>> 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
|
45 |
|| 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
|
46 |
|
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 |
|
22107 | 48 |
(* predefined styles *) |
49 |
||
32891 | 50 |
fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t => |
22107 | 51 |
let |
35625 | 52 |
val concl = |
42360 | 53 |
Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t) |
22107 | 54 |
in |
50637 | 55 |
(case concl of |
56030 | 56 |
_ $ l $ r => proj (l, r) |
50637 | 57 |
| _ => 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
|
58 |
end); |
22107 | 59 |
|
50638 | 60 |
val style_prem = Parse.nat >> (fn i => fn ctxt => fn t => |
32891 | 61 |
let |
62 |
val prems = Logic.strip_imp_prems t; |
|
63 |
in |
|
64 |
if i <= length prems then nth prems (i - 1) |
|
50637 | 65 |
else |
66 |
error ("Not enough premises for prem " ^ string_of_int i ^ |
|
67 |
" in propositon: " ^ Syntax.string_of_term ctxt t) |
|
32891 | 68 |
end); |
69 |
||
53021
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
50638
diff
changeset
|
70 |
fun sub_symbols (d :: s :: ss) = |
56203
76c72f4d0667
clarified bootstrap process: switch to ML with context and antiquotations earlier;
wenzelm
parents:
56201
diff
changeset
|
71 |
if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\<^") s) |
76c72f4d0667
clarified bootstrap process: switch to ML with context and antiquotations earlier;
wenzelm
parents:
56201
diff
changeset
|
72 |
then d :: "\<^sub>" :: sub_symbols (s :: ss) |
41685
e29ea98a76ce
term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)
krauss
parents:
36950
diff
changeset
|
73 |
else d :: s :: ss |
53021
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
50638
diff
changeset
|
74 |
| sub_symbols cs = cs; |
41685
e29ea98a76ce
term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)
krauss
parents:
36950
diff
changeset
|
75 |
|
53021
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
50638
diff
changeset
|
76 |
val sub_name = implode o rev o sub_symbols o rev o Symbol.explode; |
41685
e29ea98a76ce
term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)
krauss
parents:
36950
diff
changeset
|
77 |
|
53021
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
50638
diff
changeset
|
78 |
fun sub_term (Free (n, T)) = Free (sub_name n, T) |
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
50638
diff
changeset
|
79 |
| sub_term (Var ((n, idx), T)) = |
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
50638
diff
changeset
|
80 |
if idx <> 0 then Var ((sub_name (n ^ string_of_int idx), 0), T) |
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
50638
diff
changeset
|
81 |
else Var ((sub_name n, 0), T) |
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
50638
diff
changeset
|
82 |
| sub_term (t $ u) = sub_term t $ sub_term u |
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
50638
diff
changeset
|
83 |
| sub_term (Abs (n, T, b)) = Abs (sub_name n, T, sub_term b) |
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
50638
diff
changeset
|
84 |
| sub_term t = t; |
41685
e29ea98a76ce
term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)
krauss
parents:
36950
diff
changeset
|
85 |
|
53171 | 86 |
val _ = Theory.setup |
56204 | 87 |
(setup @{binding lhs} (style_lhs_rhs fst) #> |
88 |
setup @{binding rhs} (style_lhs_rhs snd) #> |
|
89 |
setup @{binding prem} style_prem #> |
|
90 |
setup @{binding concl} (Scan.succeed (K Logic.strip_imp_concl)) #> |
|
91 |
setup @{binding sub} (Scan.succeed (K sub_term))); |
|
22107 | 92 |
|
93 |
end; |