3 Author: Florian Haftmann, TU Muenchen |
3 Author: Florian Haftmann, TU Muenchen |
4 |
4 |
5 Styles for terms, to use with the "term_style" and "thm_style" antiquotations |
5 Styles for terms, to use with the "term_style" and "thm_style" antiquotations |
6 *) |
6 *) |
7 |
7 |
8 signature STYLE = |
8 (* style data *) |
|
9 signature TERM_STYLE = |
9 sig |
10 sig |
10 val get_style: theory -> string -> (Term.term -> Term.term) |
11 val lookup_style: theory -> string -> (Proof.context -> term -> term) |
11 val put_style: string -> (Term.term -> Term.term) -> theory -> theory |
12 val update_style: string -> (Proof.context -> term -> term) -> theory -> theory |
12 end; |
13 end; |
13 |
14 |
14 structure Style: STYLE = |
15 structure TermStyle: TERM_STYLE = |
15 struct |
16 struct |
16 |
17 |
17 (* exception *) |
|
18 exception STYLE of string; |
|
19 |
|
20 (* style data *) |
|
21 structure StyleArgs = |
18 structure StyleArgs = |
22 struct |
19 struct |
23 val name = "Isar/style"; |
20 val name = "Isar/style"; |
24 type T = (string * (Term.term -> Term.term)) list; |
21 type T = (Proof.context -> term -> term) Symtab.table; |
25 val empty = []; |
22 val empty = Symtab.empty; |
26 val copy = I; |
23 val copy = I; |
27 val prep_ext = I; |
24 val prep_ext = I; |
28 fun merge (a1, a2) = Library.foldl Library.overwrite (a1, a2); |
25 val merge = Symtab.merge (K true); |
29 (* piecewise update of a1 by a2 *) |
26 fun print _ table = |
30 fun print _ _ = raise (STYLE "cannot print style (not implemented)"); |
27 Pretty.strs ("defined styles:" :: (Symtab.keys table)) |
|
28 |> Pretty.writeln; |
31 end; |
29 end; |
32 |
30 |
33 structure StyleData = TheoryDataFun(StyleArgs); |
31 structure StyleData = TheoryDataFun(StyleArgs); |
34 |
32 |
35 (* accessors *) |
33 (* accessors *) |
36 fun get_style thy name = |
34 fun lookup_style thy name = |
37 case Library.assoc_string ((StyleData.get thy), name) |
35 case Symtab.lookup ((StyleData.get thy), name) |
38 of NONE => raise (STYLE ("no style named " ^ name)) |
36 of NONE => raise (ERROR_MESSAGE ("no style named " ^ name)) |
39 | SOME style => style |
37 | SOME style => style |
40 |
38 |
41 fun put_style name style thy = |
39 fun update_style name style thy = |
42 StyleData.put (Library.overwrite ((StyleData.get thy), (name, style))) thy; |
40 thy |
|
41 |> StyleData.put (Symtab.update ((name, style), StyleData.get thy)); |
43 |
42 |
44 (* predefined styles *) |
43 (* predefined styles *) |
45 fun style_lhs (Const ("==", _) $ t $ _) = t |
44 fun style_binargs ctxt t = |
46 | style_lhs (Const ("Trueprop", _) $ t) = style_lhs t |
45 let val concl = ObjectLogic.drop_judgment (ProofContext.sign_of ctxt) (Logic.strip_imp_concl t) in |
47 | style_lhs (Const ("==>", _) $ _ $ t) = style_lhs t |
46 case concl of (_ $ l $ r) => (l, r) |
48 | style_lhs (_ $ t $ _) = t |
47 | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl) |
49 | style_lhs _ = error ("Binary operator expected") |
48 end; |
50 |
|
51 fun style_rhs (Const ("==", _) $ _ $ t) = t |
|
52 | style_rhs (Const ("Trueprop", _) $ t) = style_rhs t |
|
53 | style_rhs (Const ("==>", _) $ _ $ t) = style_rhs t |
|
54 | style_rhs (_ $ _ $ t) = t |
|
55 | style_rhs _ = error ("Binary operator expected") |
|
56 |
49 |
57 (* initialization *) |
50 (* initialization *) |
58 val _ = Context.add_setup [StyleData.init, |
51 val _ = Context.add_setup [StyleData.init, |
59 put_style "lhs" style_lhs, |
52 update_style "lhs" (fst oo style_binargs), |
60 put_style "rhs" style_rhs, |
53 update_style "rhs" (snd oo style_binargs), |
61 put_style "conclusion" Logic.strip_imp_concl |
54 update_style "conclusion" (K Logic.strip_imp_concl) |
62 ]; |
55 ]; |
63 |
56 |
64 end; |
57 end; |