author | wenzelm |
Sun, 02 Nov 2014 17:36:52 +0100 | |
changeset 58884 | be4d203d35b3 |
parent 52144 | 9065615d0360 |
child 59152 | 66e6c539a36d |
permissions | -rw-r--r-- |
42240
5a4d30cd47a7
moved Isar/local_syntax.ML to Syntax/local_syntax.ML;
wenzelm
parents:
35429
diff
changeset
|
1 |
(* Title: Pure/Syntax/local_syntax.ML |
18997 | 2 |
Author: Makarius |
3 |
||
51655 | 4 |
Local syntax depending on theory syntax, with special support for |
5 |
implicit structure references. |
|
18997 | 6 |
*) |
7 |
||
8 |
signature LOCAL_SYNTAX = |
|
9 |
sig |
|
10 |
type T |
|
11 |
val syn_of: T -> Syntax.syntax |
|
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35412
diff
changeset
|
12 |
val idents_of: T -> {structs: string list, fixes: string list} |
18997 | 13 |
val init: theory -> T |
14 |
val rebuild: theory -> T -> T |
|
35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
15 |
datatype kind = Type | Const | Fixed |
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
16 |
val add_syntax: theory -> (kind * (string * typ * mixfix)) list -> T -> T |
20785 | 17 |
val set_mode: Syntax.mode -> T -> T |
19541 | 18 |
val restore_mode: T -> T -> T |
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
19 |
val update_modesyntax: theory -> bool -> Syntax.mode -> |
35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
20 |
(kind * (string * typ * mixfix)) list -> T -> T |
18997 | 21 |
end; |
22 |
||
33387 | 23 |
structure Local_Syntax: LOCAL_SYNTAX = |
18997 | 24 |
struct |
25 |
||
26 |
(* datatype T *) |
|
27 |
||
19386 | 28 |
type local_mixfix = |
35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
29 |
(string * bool) * (*name, fixed?*) |
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
30 |
((bool * bool * Syntax.mode) * (string * typ * mixfix)); (*type?, add?, mode, declaration*) |
19386 | 31 |
|
18997 | 32 |
datatype T = Syntax of |
33 |
{thy_syntax: Syntax.syntax, |
|
34 |
local_syntax: Syntax.syntax, |
|
20785 | 35 |
mode: Syntax.mode, |
19386 | 36 |
mixfixes: local_mixfix list, |
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset
|
37 |
idents: string list * string list}; |
18997 | 38 |
|
19541 | 39 |
fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) = |
18997 | 40 |
Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax, |
19541 | 41 |
mode = mode, mixfixes = mixfixes, idents = idents}; |
18997 | 42 |
|
19541 | 43 |
fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) = |
44 |
make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents)); |
|
18997 | 45 |
|
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset
|
46 |
fun is_consistent thy (Syntax {thy_syntax, ...}) = |
18997 | 47 |
Syntax.eq_syntax (Sign.syn_of thy, thy_syntax); |
48 |
||
49 |
fun syn_of (Syntax {local_syntax, ...}) = local_syntax; |
|
35429
afa8cf9e63d8
authentic syntax for classes and type constructors;
wenzelm
parents:
35412
diff
changeset
|
50 |
fun idents_of (Syntax {idents = (structs, fixes), ...}) = {structs = structs, fixes = fixes}; |
18997 | 51 |
|
52 |
||
53 |
(* build syntax *) |
|
54 |
||
19541 | 55 |
fun build_syntax thy mode mixfixes (idents as (structs, _)) = |
18997 | 56 |
let |
57 |
val thy_syntax = Sign.syn_of thy; |
|
35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
58 |
fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls |
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
59 |
| update_gram ((false, add, m), decls) = |
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
60 |
Syntax.update_const_gram add (Sign.is_logtype thy) m decls; |
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
61 |
|
18997 | 62 |
val local_syntax = thy_syntax |
25390
8bfa6566ac6b
syntax operations: turned extend'' into update'' (absorb duplicates);
wenzelm
parents:
25385
diff
changeset
|
63 |
|> Syntax.update_trfuns |
52144 | 64 |
([], [Syntax_Ext.mk_trfun (Syntax_Trans.struct_tr structs)], |
65 |
[], [Syntax_Ext.mk_trfun (Syntax_Trans.struct_ast_tr' structs)]) |
|
35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
66 |
|> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes))); |
19541 | 67 |
in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end; |
68 |
||
24960 | 69 |
fun init thy = build_syntax thy Syntax.mode_default [] ([], []); |
18997 | 70 |
|
19541 | 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; |
|
18997 | 74 |
|
19541 | 75 |
|
18997 | 76 |
(* mixfix declarations *) |
77 |
||
35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
78 |
datatype kind = Type | Const | Fixed; |
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
79 |
|
18997 | 80 |
local |
81 |
||
35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
82 |
fun prep_mixfix _ _ (_, (_, _, Structure)) = NONE |
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
83 |
| prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl)) |
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
84 |
| prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl)) |
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
85 |
| prep_mixfix add mode (Fixed, (x, T, mx)) = |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
42288
diff
changeset
|
86 |
SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx))); |
19016 | 87 |
|
35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
88 |
fun prep_struct (Fixed, (c, _, Structure)) = SOME c |
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
89 |
| prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c) |
19016 | 90 |
| prep_struct _ = NONE; |
18997 | 91 |
|
92 |
in |
|
93 |
||
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
94 |
fun update_syntax add thy raw_decls |
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
95 |
(syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) = |
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
96 |
(case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of |
19016 | 97 |
[] => syntax |
98 |
| decls => |
|
99 |
let |
|
35412
b8dead547d9e
more uniform treatment of syntax for types vs. consts;
wenzelm
parents:
33387
diff
changeset
|
100 |
val new_mixfixes = map_filter (prep_mixfix add mode) decls; |
24954
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset
|
101 |
val new_structs = map_filter prep_struct decls; |
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset
|
102 |
val mixfixes' = rev new_mixfixes @ mixfixes; |
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset
|
103 |
val structs' = |
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset
|
104 |
if add then structs @ new_structs |
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset
|
105 |
else subtract (op =) new_structs structs; |
20785 | 106 |
val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' []; |
19541 | 107 |
in build_syntax thy mode mixfixes' (structs', fixes') end); |
18997 | 108 |
|
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
109 |
val add_syntax = update_syntax true; |
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
110 |
|
18997 | 111 |
end; |
112 |
||
113 |
||
19660 | 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 |
||
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
121 |
fun update_modesyntax thy add mode args syntax = |
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset
|
122 |
syntax |> set_mode mode |> update_syntax add thy args |> restore_mode syntax; |
19660 | 123 |
|
18997 | 124 |
end; |