author | wenzelm |
Thu, 27 Apr 2006 15:06:35 +0200 | |
changeset 19482 | 9f11af8f7ef9 |
parent 19467 | d75570e8aa97 |
child 19673 | 853f5a3cc06e |
permissions | -rw-r--r-- |
384 | 1 |
(* Title: Pure/Syntax/mixfix.ML |
2 |
ID: $Id$ |
|
551 | 3 |
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
384 | 4 |
|
18719
dca3ae4f6dd6
moved pure syntax to Syntax/syntax.ML and pure_thy.ML;
wenzelm
parents:
18673
diff
changeset
|
5 |
Mixfix declarations, infixes, binders. |
384 | 6 |
*) |
7 |
||
8 |
signature MIXFIX0 = |
|
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
9 |
sig |
384 | 10 |
datatype mixfix = |
11 |
NoSyn | |
|
12 |
Mixfix of string * int list * int | |
|
13 |
Delimfix of string | |
|
11651 | 14 |
InfixName of string * int | |
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
15 |
InfixlName of string * int | |
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
16 |
InfixrName of string * int | |
18565 | 17 |
Infix of int | (*obsolete*) |
18 |
Infixl of int | (*obsolete*) |
|
19 |
Infixr of int | (*obsolete*) |
|
18673 | 20 |
Binder of string * int * int | |
21 |
Structure |
|
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
22 |
end; |
384 | 23 |
|
24 |
signature MIXFIX1 = |
|
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
25 |
sig |
384 | 26 |
include MIXFIX0 |
12864 | 27 |
val literal: string -> mixfix |
4823 | 28 |
val no_syn: 'a * 'b -> 'a * 'b * mixfix |
19271 | 29 |
val pretty_mixfix: mixfix -> Pretty.T |
384 | 30 |
val type_name: string -> mixfix -> string |
31 |
val const_name: string -> mixfix -> string |
|
19373 | 32 |
val const_mixfix: string -> mixfix -> string * mixfix |
33 |
val mixfix_const: string -> mixfix -> string * bool |
|
18565 | 34 |
val unlocalize_mixfix: mixfix -> mixfix |
4823 | 35 |
val mixfix_args: mixfix -> int |
19020 | 36 |
val mixfix_content: mixfix -> string list list |
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
37 |
end; |
384 | 38 |
|
39 |
signature MIXFIX = |
|
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
40 |
sig |
384 | 41 |
include MIXFIX1 |
14903 | 42 |
val syn_ext_types: (string * int * mixfix) list -> SynExt.syn_ext |
43 |
val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> SynExt.syn_ext |
|
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
44 |
end; |
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
45 |
|
15751
65e4790c7914
identify binder translations only once (admits remove);
wenzelm
parents:
15570
diff
changeset
|
46 |
structure Mixfix: MIXFIX = |
384 | 47 |
struct |
48 |
||
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
49 |
|
384 | 50 |
(** mixfix declarations **) |
51 |
||
52 |
datatype mixfix = |
|
53 |
NoSyn | |
|
54 |
Mixfix of string * int list * int | |
|
55 |
Delimfix of string | |
|
11651 | 56 |
InfixName of string * int | |
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
57 |
InfixlName of string * int | |
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
58 |
InfixrName of string * int | |
18565 | 59 |
Infix of int | (*obsolete*) |
60 |
Infixl of int | (*obsolete*) |
|
61 |
Infixr of int | (*obsolete*) |
|
18673 | 62 |
Binder of string * int * int | |
63 |
Structure; |
|
384 | 64 |
|
12864 | 65 |
val literal = Delimfix o SynExt.escape_mfix; |
66 |
||
4823 | 67 |
fun no_syn (x, y) = (x, y, NoSyn); |
68 |
||
384 | 69 |
|
19271 | 70 |
(* pretty_mixfix *) |
71 |
||
72 |
local |
|
11920 | 73 |
|
19271 | 74 |
val quoted = Pretty.quote o Pretty.str; |
75 |
val keyword = Pretty.keyword; |
|
76 |
val parens = Pretty.enclose "(" ")"; |
|
77 |
val brackets = Pretty.enclose "[" "]"; |
|
78 |
val int = Pretty.str o string_of_int; |
|
79 |
||
80 |
in |
|
11920 | 81 |
|
19271 | 82 |
fun pretty_mixfix NoSyn = Pretty.str "" |
83 |
| pretty_mixfix (Mixfix (s, ps, p)) = |
|
84 |
parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p]) |
|
85 |
| pretty_mixfix (Delimfix s) = parens [quoted s] |
|
86 |
| pretty_mixfix (InfixName (s, p)) = parens (Pretty.breaks [keyword "infix", quoted s, int p]) |
|
87 |
| pretty_mixfix (InfixlName (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) |
|
88 |
| pretty_mixfix (InfixrName (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) |
|
89 |
| pretty_mixfix (Infix p) = parens (Pretty.breaks [keyword "infix", int p]) |
|
90 |
| pretty_mixfix (Infixl p) = parens (Pretty.breaks [keyword "infixl", int p]) |
|
91 |
| pretty_mixfix (Infixr p) = parens (Pretty.breaks [keyword "infixr", int p]) |
|
92 |
| pretty_mixfix (Binder (s, p1, p2)) = |
|
93 |
parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2]) |
|
94 |
| pretty_mixfix Structure = parens [keyword "structure"]; |
|
95 |
||
96 |
end; |
|
11920 | 97 |
|
98 |
||
12531 | 99 |
(* syntax specifications *) |
384 | 100 |
|
101 |
fun strip ("'" :: c :: cs) = c :: strip cs |
|
102 |
| strip ["'"] = [] |
|
103 |
| strip (c :: cs) = c :: strip cs |
|
104 |
| strip [] = []; |
|
105 |
||
4697 | 106 |
val strip_esc = implode o strip o Symbol.explode; |
384 | 107 |
|
17284
ca3eebbb3724
deprecated old-style infix declarations, which mix name and syntax;
wenzelm
parents:
16610
diff
changeset
|
108 |
fun deprecated c = (warning ("Unnamed infix operator " ^ quote c ^ " -- deprecated"); c); |
ca3eebbb3724
deprecated old-style infix declarations, which mix name and syntax;
wenzelm
parents:
16610
diff
changeset
|
109 |
|
11651 | 110 |
fun type_name t (InfixName _) = t |
111 |
| type_name t (InfixlName _) = t |
|
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
112 |
| type_name t (InfixrName _) = t |
17284
ca3eebbb3724
deprecated old-style infix declarations, which mix name and syntax;
wenzelm
parents:
16610
diff
changeset
|
113 |
| type_name t (Infix _) = deprecated (strip_esc t) |
ca3eebbb3724
deprecated old-style infix declarations, which mix name and syntax;
wenzelm
parents:
16610
diff
changeset
|
114 |
| type_name t (Infixl _) = deprecated (strip_esc t) |
ca3eebbb3724
deprecated old-style infix declarations, which mix name and syntax;
wenzelm
parents:
16610
diff
changeset
|
115 |
| type_name t (Infixr _) = deprecated (strip_esc t) |
384 | 116 |
| type_name t _ = t; |
117 |
||
11651 | 118 |
fun const_name c (InfixName _) = c |
119 |
| const_name c (InfixlName _) = c |
|
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
120 |
| const_name c (InfixrName _) = c |
17284
ca3eebbb3724
deprecated old-style infix declarations, which mix name and syntax;
wenzelm
parents:
16610
diff
changeset
|
121 |
| const_name c (Infix _) = "op " ^ deprecated (strip_esc c) |
ca3eebbb3724
deprecated old-style infix declarations, which mix name and syntax;
wenzelm
parents:
16610
diff
changeset
|
122 |
| const_name c (Infixl _) = "op " ^ deprecated (strip_esc c) |
ca3eebbb3724
deprecated old-style infix declarations, which mix name and syntax;
wenzelm
parents:
16610
diff
changeset
|
123 |
| const_name c (Infixr _) = "op " ^ deprecated (strip_esc c) |
384 | 124 |
| const_name c _ = c; |
125 |
||
19373 | 126 |
fun fix_mixfix c (Infix p) = InfixName (c, p) |
127 |
| fix_mixfix c (Infixl p) = InfixlName (c, p) |
|
128 |
| fix_mixfix c (Infixr p) = InfixrName (c, p) |
|
5056 | 129 |
| fix_mixfix _ mx = mx; |
130 |
||
19373 | 131 |
fun const_mixfix c mx = (const_name c mx, fix_mixfix c mx); |
132 |
||
133 |
fun mixfix_const c NoSyn = (c, true) |
|
134 |
| mixfix_const c _ = (Lexicon.constN ^ c, false); |
|
135 |
||
18565 | 136 |
fun map_mixfix _ NoSyn = NoSyn |
137 |
| map_mixfix f (Mixfix (sy, ps, p)) = Mixfix (f sy, ps, p) |
|
138 |
| map_mixfix f (Delimfix sy) = Delimfix (f sy) |
|
139 |
| map_mixfix f (InfixName (sy, p)) = InfixName (f sy, p) |
|
140 |
| map_mixfix f (InfixlName (sy, p)) = InfixlName (f sy, p) |
|
141 |
| map_mixfix f (InfixrName (sy, p)) = InfixrName (f sy, p) |
|
142 |
| map_mixfix f (Binder (sy, p, q)) = Binder (f sy, p, q) |
|
18673 | 143 |
| map_mixfix _ Structure = Structure |
18565 | 144 |
| map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix"); |
145 |
||
19467 | 146 |
fun unlocalize_mixfix mx = |
147 |
let val mx' = map_mixfix SynExt.unlocalize_mfix mx |
|
148 |
in if mx = mx' then NoSyn else mx' end; |
|
18565 | 149 |
|
4053 | 150 |
fun mixfix_args NoSyn = 0 |
5690 | 151 |
| mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy |
152 |
| mixfix_args (Delimfix sy) = SynExt.mfix_args sy |
|
12531 | 153 |
| mixfix_args (InfixName (sy, _)) = 2 + SynExt.mfix_args sy |
154 |
| mixfix_args (InfixlName (sy, _)) = 2 + SynExt.mfix_args sy |
|
155 |
| mixfix_args (InfixrName (sy, _)) = 2 + SynExt.mfix_args sy |
|
18341 | 156 |
| mixfix_args (Infix _) = 2 |
157 |
| mixfix_args (Infixl _) = 2 |
|
158 |
| mixfix_args (Infixr _) = 2 |
|
18673 | 159 |
| mixfix_args (Binder _) = 1 |
160 |
| mixfix_args Structure = 0; |
|
4053 | 161 |
|
162 |
||
384 | 163 |
(* syn_ext_types *) |
164 |
||
14903 | 165 |
fun syn_ext_types type_decls = |
384 | 166 |
let |
167 |
fun name_of (t, _, mx) = type_name t mx; |
|
168 |
||
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
169 |
fun mk_infix sy t p1 p2 p3 = |
5690 | 170 |
SynExt.Mfix ("(_ " ^ sy ^ "/ _)", |
12512
ab14b29dfc6d
removed special treatment of "_" in syntax (now covered by \<index> arg);
wenzelm
parents:
12149
diff
changeset
|
171 |
[SynExt.typeT, SynExt.typeT] ---> SynExt.typeT, t, [p1, p2], p3); |
384 | 172 |
|
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
173 |
fun mfix_of decl = |
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
174 |
let val t = name_of decl in |
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
175 |
(case decl of |
15531 | 176 |
(_, _, NoSyn) => NONE |
177 |
| (_, 2, InfixName (sy, p)) => SOME (mk_infix sy t (p + 1) (p + 1) p) |
|
178 |
| (_, 2, InfixlName (sy, p)) => SOME (mk_infix sy t p (p + 1) p) |
|
179 |
| (_, 2, InfixrName (sy, p)) => SOME (mk_infix sy t (p + 1) p p) |
|
180 |
| (sy, 2, Infix p) => SOME (mk_infix sy t (p + 1) (p + 1) p) |
|
181 |
| (sy, 2, Infixl p) => SOME (mk_infix sy t p (p + 1) p) |
|
182 |
| (sy, 2, Infixr p) => SOME (mk_infix sy t (p + 1) p p) |
|
14903 | 183 |
| _ => error ("Bad mixfix declaration for type: " ^ quote t)) |
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
184 |
end; |
384 | 185 |
|
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19467
diff
changeset
|
186 |
val mfix = map_filter mfix_of type_decls; |
384 | 187 |
val xconsts = map name_of type_decls; |
14903 | 188 |
in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end; |
384 | 189 |
|
190 |
||
191 |
(* syn_ext_consts *) |
|
192 |
||
15751
65e4790c7914
identify binder translations only once (admits remove);
wenzelm
parents:
15570
diff
changeset
|
193 |
val binder_stamp = stamp (); |
65e4790c7914
identify binder translations only once (admits remove);
wenzelm
parents:
15570
diff
changeset
|
194 |
|
14903 | 195 |
fun syn_ext_consts is_logtype const_decls = |
384 | 196 |
let |
197 |
fun name_of (c, _, mx) = const_name c mx; |
|
198 |
||
199 |
fun mk_infix sy ty c p1 p2 p3 = |
|
5690 | 200 |
[SynExt.Mfix ("op " ^ sy, ty, c, [], SynExt.max_pri), |
12512
ab14b29dfc6d
removed special treatment of "_" in syntax (now covered by \<index> arg);
wenzelm
parents:
12149
diff
changeset
|
201 |
SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)]; |
384 | 202 |
|
203 |
fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = |
|
204 |
[Type ("idts", []), ty2] ---> ty3 |
|
14903 | 205 |
| binder_typ c _ = error ("Bad type of binder: " ^ quote c); |
384 | 206 |
|
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
207 |
fun mfix_of decl = |
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
208 |
let val c = name_of decl in |
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
209 |
(case decl of |
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
210 |
(_, _, NoSyn) => [] |
5690 | 211 |
| (_, ty, Mixfix (sy, ps, p)) => [SynExt.Mfix (sy, ty, c, ps, p)] |
212 |
| (_, ty, Delimfix sy) => [SynExt.Mfix (sy, ty, c, [], SynExt.max_pri)] |
|
11651 | 213 |
| (_, ty, InfixName (sy, p)) => mk_infix sy ty c (p + 1) (p + 1) p |
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
214 |
| (_, ty, InfixlName (sy, p)) => mk_infix sy ty c p (p + 1) p |
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
215 |
| (_, ty, InfixrName (sy, p)) => mk_infix sy ty c (p + 1) p p |
11651 | 216 |
| (sy, ty, Infix p) => mk_infix sy ty c (p + 1) (p + 1) p |
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
217 |
| (sy, ty, Infixl p) => mk_infix sy ty c p (p + 1) p |
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
218 |
| (sy, ty, Infixr p) => mk_infix sy ty c (p + 1) p p |
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
219 |
| (_, ty, Binder (sy, p, q)) => |
18673 | 220 |
[SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, sy, [0, p], q)] |
221 |
| _ => error ("Bad mixfix declaration for const: " ^ quote c)) |
|
2199
bcb360f80dac
added Infixl/rName: specify infix name independently from syntax;
wenzelm
parents:
1952
diff
changeset
|
222 |
end; |
384 | 223 |
|
15531 | 224 |
fun binder (c, _, Binder (sy, _, _)) = SOME (sy, c) |
225 |
| binder _ = NONE; |
|
384 | 226 |
|
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19467
diff
changeset
|
227 |
val mfix = maps mfix_of const_decls; |
384 | 228 |
val xconsts = map name_of const_decls; |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19467
diff
changeset
|
229 |
val binders = map_filter binder const_decls; |
16610 | 230 |
val binder_trs = binders |> map (SynExt.stamp_trfun binder_stamp o |
231 |
apsnd K o SynTrans.mk_binder_tr); |
|
15751
65e4790c7914
identify binder translations only once (admits remove);
wenzelm
parents:
15570
diff
changeset
|
232 |
val binder_trs' = binders |> map (SynExt.stamp_trfun binder_stamp o |
16610 | 233 |
apsnd (K o SynTrans.non_typed_tr') o SynTrans.mk_binder_tr' o swap); |
14903 | 234 |
in |
235 |
SynExt.syn_ext' true is_logtype |
|
236 |
mfix xconsts ([], binder_trs, binder_trs', []) [] ([], []) |
|
237 |
end; |
|
384 | 238 |
|
19020 | 239 |
fun mixfix_content mx = |
240 |
let |
|
241 |
fun delims sy = SynExt.mfix_delims sy; |
|
242 |
fun op_delims sy = let val ds = delims sy in ["op" :: ds, ds] end; |
|
243 |
in |
|
244 |
case mx of |
|
245 |
Mixfix (sy, _, _) => [delims sy] |
|
246 |
| Delimfix sy => [delims sy] |
|
247 |
| InfixName (sy, _) => op_delims sy |
|
248 |
| InfixlName (sy, _) => op_delims sy |
|
249 |
| InfixrName (sy, _) => op_delims sy |
|
250 |
| Binder (sy, _, _) => [delims sy @ ["."]] |
|
251 |
| _ => [] |
|
252 |
end; |
|
253 |
||
384 | 254 |
end; |