author  wenzelm 
Thu, 11 Oct 2007 00:28:32 +0200  
changeset 24954  0664f10a4094 
parent 24951  834b8c2b9553 
child 24960  39d1dd215d73 
permissions  rwrr 
18997  1 
(* Title: Pure/Isar/local_syntax.ML 
2 
ID: $Id$ 

3 
Author: Makarius 

4 

5 
Local syntax depending on theory syntax. 

6 
*) 

7 

8 
val show_structs = ref false; 

9 

10 
signature LOCAL_SYNTAX = 

11 
sig 

12 
type T 

13 
val syn_of: T > Syntax.syntax 

14 
val structs_of: T > string list 

15 
val init: theory > T 

16 
val rebuild: theory > T > T 

19660  17 
val add_syntax: theory > (bool * (string * typ * mixfix)) list > T > T 
20785  18 
val set_mode: Syntax.mode > T > T 
19541  19 
val restore_mode: T > T > T 
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

20 
val update_modesyntax: theory > bool > Syntax.mode > 
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

21 
(bool * (string * typ * mixfix)) list > T > T 
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset

22 
val extern_term: T > term > term 
18997  23 
end; 
24 

19016  25 
structure LocalSyntax: LOCAL_SYNTAX = 
18997  26 
struct 
27 

28 
(* datatype T *) 

29 

19386  30 
type local_mixfix = 
24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

31 
(string * bool) * (*name, fixed?*) 
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

32 
((bool * Syntax.mode) * (string * typ * mixfix)); (*add?, mode, declaration*) 
19386  33 

18997  34 
datatype T = Syntax of 
35 
{thy_syntax: Syntax.syntax, 

36 
local_syntax: Syntax.syntax, 

20785  37 
mode: Syntax.mode, 
19386  38 
mixfixes: local_mixfix list, 
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset

39 
idents: string list * string list}; 
18997  40 

19541  41 
fun make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) = 
18997  42 
Syntax {thy_syntax = thy_syntax, local_syntax = local_syntax, 
19541  43 
mode = mode, mixfixes = mixfixes, idents = idents}; 
18997  44 

19541  45 
fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes, idents}) = 
46 
make_syntax (f (thy_syntax, local_syntax, mode, mixfixes, idents)); 

18997  47 

19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset

48 
fun is_consistent thy (Syntax {thy_syntax, ...}) = 
18997  49 
Syntax.eq_syntax (Sign.syn_of thy, thy_syntax); 
50 

51 
fun syn_of (Syntax {local_syntax, ...}) = local_syntax; 

52 
fun idents_of (Syntax {idents, ...}) = idents; 

53 
val structs_of = #1 o idents_of; 

54 

55 

56 
(* build syntax *) 

57 

19541  58 
fun build_syntax thy mode mixfixes (idents as (structs, _)) = 
18997  59 
let 
60 
val thy_syntax = Sign.syn_of thy; 

61 
val is_logtype = Sign.is_logtype thy; 

24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

62 
fun const_gram ((true, m), decls) = Syntax.extend_const_gram is_logtype m decls 
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

63 
 const_gram ((false, m), decls) = Syntax.remove_const_gram is_logtype m decls; 
18997  64 
val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs; 
65 
val local_syntax = thy_syntax 

66 
> Syntax.extend_trfuns 

19386  67 
(map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs, 
68 
map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs') 

24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

69 
> fold const_gram (AList.coalesce (op =) (rev (map snd mixfixes))); 
19541  70 
in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end; 
71 

72 
fun init thy = build_syntax thy Syntax.default_mode [] ([], []); 

18997  73 

19541  74 
fun rebuild thy (syntax as Syntax {mode, mixfixes, idents, ...}) = 
75 
if is_consistent thy syntax then syntax 

76 
else build_syntax thy mode mixfixes idents; 

18997  77 

19541  78 

18997  79 
(* mixfix declarations *) 
80 

81 
local 

82 

24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

83 
fun prep_mixfix _ (_, (_, _, Structure)) = NONE 
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

84 
 prep_mixfix mode (fixed, (x, T, mx)) = 
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

85 
let val c = if fixed then Syntax.fixedN ^ x else x 
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

86 
in SOME ((x, fixed), (mode, (c, T, mx))) end; 
19016  87 

88 
fun prep_struct (fixed, (c, _, Structure)) = 

89 
if fixed then SOME c 

24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

90 
else error ("Bad mixfix declaration for constant: " ^ quote c) 
19016  91 
 prep_struct _ = NONE; 
18997  92 

93 
in 

94 

24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

95 
fun update_syntax add thy raw_decls 
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

96 
(syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) = 
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

97 
(case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of 
19016  98 
[] => syntax 
99 
 decls => 

100 
let 

24954
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset

101 
val new_mixfixes = map_filter (prep_mixfix (add, mode)) decls; 
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset

102 
val new_structs = map_filter prep_struct decls; 
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset

103 
val mixfixes' = rev new_mixfixes @ mixfixes; 
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset

104 
val structs' = 
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset

105 
if add then structs @ new_structs 
0664f10a4094
update_modesyntax: may delete 'structure' notation as well;
wenzelm
parents:
24951
diff
changeset

106 
else subtract (op =) new_structs structs; 
20785  107 
val fixes' = fold (fn ((x, true), _) => cons x  _ => I) mixfixes' []; 
19541  108 
in build_syntax thy mode mixfixes' (structs', fixes') end); 
18997  109 

24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

110 
val add_syntax = update_syntax true; 
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

111 

18997  112 
end; 
113 

114 

19660  115 
(* syntax mode *) 
116 

117 
fun set_mode mode = map_syntax (fn (thy_syntax, local_syntax, _, mixfixes, idents) => 

118 
(thy_syntax, local_syntax, mode, mixfixes, idents)); 

119 

120 
fun restore_mode (Syntax {mode, ...}) = set_mode mode; 

121 

24951
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

122 
fun update_modesyntax thy add mode args syntax = 
834b8c2b9553
replaced add_modesyntax by general update_modesyntax (add or del);
wenzelm
parents:
20785
diff
changeset

123 
syntax > set_mode mode > update_syntax add thy args > restore_mode syntax; 
19660  124 

125 

18997  126 
(* extern_term *) 
127 

19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset

128 
fun extern_term syntax = 
18997  129 
let 
19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset

130 
val (structs, fixes) = idents_of syntax; 
18997  131 
fun map_free (t as Free (x, T)) = 
19618  132 
let val i = find_index (fn s => s = x) structs + 1 in 
18997  133 
if i = 0 andalso member (op =) fixes x then 
134 
Const (Syntax.fixedN ^ x, T) 

135 
else if i = 1 andalso not (! show_structs) then 

136 
Syntax.const "_struct" $ Syntax.const "_indexdefault" 

137 
else t 

138 
end 

139 
 map_free t = t; 

19369
a4374b41c9bf
simplified handling of authentic syntax (cf. early externing in consts.ML);
wenzelm
parents:
19016
diff
changeset

140 
in Term.map_aterms map_free end; 
18997  141 

142 
end; 