1 (* Title: Pure/Isar/local_syntax.ML |
|
2 Author: Makarius |
|
3 |
|
4 Local syntax depending on theory syntax. |
|
5 *) |
|
6 |
|
7 signature LOCAL_SYNTAX = |
|
8 sig |
|
9 type T |
|
10 val syn_of: T -> Syntax.syntax |
|
11 val idents_of: T -> {structs: string list, fixes: string list} |
|
12 val init: theory -> T |
|
13 val rebuild: theory -> T -> T |
|
14 datatype kind = Type | Const | Fixed |
|
15 val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T |
|
16 val set_mode: Syntax.mode -> T -> T |
|
17 val restore_mode: T -> T -> T |
|
18 val update_modesyntax: theory -> bool -> Syntax.mode -> |
|
19 (kind * (string * typ * mixfix)) list -> T -> T |
|
20 end; |
|
21 |
|
22 structure Local_Syntax: LOCAL_SYNTAX = |
|
23 struct |
|
24 |
|
25 (* datatype T *) |
|
26 |
|
27 type local_mixfix = |
|
28 (string * bool) * (*name, fixed?*) |
|
29 ((bool * bool * Syntax.mode) * (string * typ * mixfix)); (*type?, add?, mode, declaration*) |
|
30 |
|
31 datatype T = Syntax of |
|
32 {thy_syntax: Syntax.syntax, |
|
33 local_syntax: Syntax.syntax, |
|
34 mode: Syntax.mode, |
|
35 mixfixes: local_mixfix list, |
|
36 idents: string list * string list}; |
|
37 |
|
38 fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) = |
|
39 Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax, |
|
40 mode = mode, mixfixes = mixfixes, idents = idents}; |
|
41 |
|
42 fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) = |
|
43 make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents)); |
|
44 |
|
45 fun is_consistent thy (Syntax {thy_syntax, ...}) = |
|
46 Syntax.eq_syntax (Sign.syn_of thy, thy_syntax); |
|
47 |
|
48 fun syn_of (Syntax {local_syntax, ...}) = local_syntax; |
|
49 fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes}; |
|
50 |
|
51 |
|
52 (* build syntax *) |
|
53 |
|
54 fun build_syntax thy mode mixfixes (idents as (structs, _)) = |
|
55 let |
|
56 val thy_syntax = Sign.syn_of thy; |
|
57 fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls |
|
58 | update_gram ((false, add, m), decls) = |
|
59 Syntax.update_const_gram add (Sign.is_logtype thy) m decls; |
|
60 |
|
61 val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs; |
|
62 val local_syntax = thy_syntax |
|
63 |> Syntax.update_trfuns |
|
64 (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs, |
|
65 map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs') |
|
66 |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes))); |
|
67 in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end; |
|
68 |
|
69 fun init thy = build_syntax thy Syntax.mode_default [] ([], []); |
|
70 |
|
71 fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) = |
|
72 if is_consistent thy syntax then syntax |
|
73 else build_syntax thy mode mixfixes idents; |
|
74 |
|
75 |
|
76 (* mixfix declarations *) |
|
77 |
|
78 datatype kind = Type | Const | Fixed; |
|
79 |
|
80 local |
|
81 |
|
82 fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE |
|
83 | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl)) |
|
84 | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl)) |
|
85 | prep_mixfix add mode (Fixed, (x, T, mx)) = |
|
86 SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx))); |
|
87 |
|
88 fun prep_struct (Fixed, (c, _, Structure)) = SOME c |
|
89 | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c) |
|
90 | prep_struct _ = NONE; |
|
91 |
|
92 in |
|
93 |
|
94 fun update_syntax add thy raw_decls |
|
95 (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) = |
|
96 (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of |
|
97 [] => syntax |
|
98 | decls => |
|
99 let |
|
100 val new_mixfixes = map_filter (prep_mixfix add mode) decls; |
|
101 val new_structs = map_filter prep_struct decls; |
|
102 val mixfixes' = rev new_mixfixes @ mixfixes; |
|
103 val structs' = |
|
104 if add then structs @ new_structs |
|
105 else subtract (op =) new_structs structs; |
|
106 val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' []; |
|
107 in build_syntax thy mode mixfixes' (structs', fixes') end); |
|
108 |
|
109 val add_syntax = update_syntax true; |
|
110 |
|
111 end; |
|
112 |
|
113 |
|
114 (* syntax mode *) |
|
115 |
|
116 fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) => |
|
117 (thy_syntax, local_syntax, mode, mixfixes, idents)); |
|
118 |
|
119 fun restore_mode (Syntax {mode, ...}) = set_mode mode; |
|
120 |
|
121 fun update_modesyntax thy add mode args syntax = |
|
122 syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax; |
|
123 |
|
124 end; |
|