author  wenzelm 
Sat, 25 May 2013 16:55:27 +0200  
changeset 52144  9065615d0360 
parent 52143  36ffe23b25f8 
child 59152  66e6c539a36d 
permissions  rwrr 
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; 