author | wenzelm |
Thu, 06 Jun 2024 12:53:02 +0200 | |
changeset 80268 | 979f3893aa37 |
parent 78690 | e10ef4f9c848 |
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"; |
|
22 |
fun merge data : T = Name_Space.merge_tables data; |
|
22846 | 23 |
); |
22107 | 24 |
|
56030 | 25 |
val get_data = Data.get o Proof_Context.theory_of; |
22107 | 26 |
|
56030 | 27 |
fun setup binding style thy = |
28 |
Data.map (#2 o Name_Space.define (Context.Theory thy) true (binding, style)) thy; |
|
22107 | 29 |
|
30 |
||
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
|
31 |
(* 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
|
32 |
|
56030 | 33 |
fun parse_single ctxt = |
62969 | 34 |
Parse.token Parse.name ::: Parse.args >> (fn src0 => |
56030 | 35 |
let |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61470
diff
changeset
|
36 |
val (src, parse) = Token.check_src ctxt get_data src0; |
78690 | 37 |
val f = Token.read ctxt parse src; |
56030 | 38 |
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
|
39 |
|
50637 | 40 |
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
|
41 |
(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
|
42 |
>> 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
|
43 |
|| 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
|
44 |
|
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 |
|
22107 | 46 |
(* predefined styles *) |
47 |
||
32891 | 48 |
fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t => |
22107 | 49 |
let |
59970 | 50 |
val concl = Object_Logic.drop_judgment ctxt (Logic.strip_imp_concl t); |
22107 | 51 |
in |
50637 | 52 |
(case concl of |
56030 | 53 |
_ $ l $ r => proj (l, r) |
50637 | 54 |
| _ => 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
|
55 |
end); |
22107 | 56 |
|
50638 | 57 |
val style_prem = Parse.nat >> (fn i => fn ctxt => fn t => |
32891 | 58 |
let |
59 |
val prems = Logic.strip_imp_prems t; |
|
60 |
in |
|
61 |
if i <= length prems then nth prems (i - 1) |
|
50637 | 62 |
else |
63 |
error ("Not enough premises for prem " ^ string_of_int i ^ |
|
64 |
" in propositon: " ^ Syntax.string_of_term ctxt t) |
|
32891 | 65 |
end); |
66 |
||
53021
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
50638
diff
changeset
|
67 |
fun sub_symbols (d :: s :: ss) = |
61470 | 68 |
if Symbol.is_ascii_digit d andalso not (Symbol.is_control s) |
56203
76c72f4d0667
clarified bootstrap process: switch to ML with context and antiquotations earlier;
wenzelm
parents:
56201
diff
changeset
|
69 |
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
|
70 |
else d :: s :: ss |
53021
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
50638
diff
changeset
|
71 |
| 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
|
72 |
|
53021
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
50638
diff
changeset
|
73 |
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
|
74 |
|
53021
d0fa3f446b9d
discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end;
wenzelm
parents:
50638
diff
changeset
|
75 |
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
|
76 |
| 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
|
77 |
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
|
78 |
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
|
79 |
| 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
|
80 |
| 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
|
81 |
| 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
|
82 |
|
53171 | 83 |
val _ = Theory.setup |
67147 | 84 |
(setup \<^binding>\<open>lhs\<close> (style_lhs_rhs fst) #> |
85 |
setup \<^binding>\<open>rhs\<close> (style_lhs_rhs snd) #> |
|
86 |
setup \<^binding>\<open>prem\<close> style_prem #> |
|
87 |
setup \<^binding>\<open>concl\<close> (Scan.succeed (K Logic.strip_imp_concl)) #> |
|
88 |
setup \<^binding>\<open>sub\<close> (Scan.succeed (K sub_term))); |
|
22107 | 89 |
|
90 |
end; |