34 |
39 |
35 (** mixfix declarations **) |
40 (** mixfix declarations **) |
36 |
41 |
37 datatype mixfix = |
42 datatype mixfix = |
38 NoSyn | |
43 NoSyn | |
39 Mixfix of string * int list * int | |
44 Mixfix of Input.source * int list * int * Position.range | |
40 Delimfix of string | |
45 Delimfix of Input.source * Position.range | |
41 Infix of string * int | |
46 Infix of Input.source * int * Position.range | |
42 Infixl of string * int | |
47 Infixl of Input.source * int * Position.range | |
43 Infixr of string * int | |
48 Infixr of Input.source * int * Position.range | |
44 Binder of string * int * int | |
49 Binder of Input.source * int * int * Position.range | |
45 Structure; |
50 Structure of Position.range; |
|
51 |
|
52 fun is_empty NoSyn = true |
|
53 | is_empty _ = false; |
|
54 |
|
55 fun equal (NoSyn, NoSyn) = true |
|
56 | equal (Mixfix (sy, ps, p, _), Mixfix (sy', ps', p', _)) = |
|
57 Input.equal_content (sy, sy') andalso ps = ps' andalso p = p' |
|
58 | equal (Delimfix (sy, _), Delimfix (sy', _)) = Input.equal_content (sy, sy') |
|
59 | equal (Infix (sy, p, _), Infix (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p' |
|
60 | equal (Infixl (sy, p, _), Infixl (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p' |
|
61 | equal (Infixr (sy, p, _), Infixr (sy', p', _)) = Input.equal_content (sy, sy') andalso p = p' |
|
62 | equal (Binder (sy, p, q, _), Binder (sy', p', q', _)) = |
|
63 Input.equal_content (sy, sy') andalso p = p' andalso q = q' |
|
64 | equal (Structure _, Structure _) = true |
|
65 | equal _ = false; |
|
66 |
|
67 fun set_range range mx = |
|
68 (case mx of |
|
69 NoSyn => NoSyn |
|
70 | Mixfix (sy, ps, p, _) => Mixfix (sy, ps, p, range) |
|
71 | Delimfix (sy, _) => Delimfix (sy, range) |
|
72 | Infix (sy, p, _) => Infix (sy, p, range) |
|
73 | Infixl (sy, p, _) => Infixl (sy, p, range) |
|
74 | Infixr (sy, p, _) => Infixr (sy, p, range) |
|
75 | Binder (sy, p, q, _) => Binder (sy, p, q, range) |
|
76 | Structure _ => Structure range); |
|
77 |
|
78 fun range_of NoSyn = Position.no_range |
|
79 | range_of (Mixfix (_, _, _, range)) = range |
|
80 | range_of (Delimfix (_, range)) = range |
|
81 | range_of (Infix (_, _, range)) = range |
|
82 | range_of (Infixl (_, _, range)) = range |
|
83 | range_of (Infixr (_, _, range)) = range |
|
84 | range_of (Binder (_, _, _, range)) = range |
|
85 | range_of (Structure range) = range; |
|
86 |
|
87 val pos_of = Position.set_range o range_of; |
46 |
88 |
47 |
89 |
48 (* pretty_mixfix *) |
90 (* pretty_mixfix *) |
49 |
91 |
50 local |
92 local |
51 |
93 |
52 val quoted = Pretty.quote o Pretty.str; |
94 val quoted = Pretty.quote o Pretty.str o Input.source_content; |
53 val keyword = Pretty.keyword2; |
95 val keyword = Pretty.keyword2; |
54 val parens = Pretty.enclose "(" ")"; |
96 val parens = Pretty.enclose "(" ")"; |
55 val brackets = Pretty.enclose "[" "]"; |
97 val brackets = Pretty.enclose "[" "]"; |
56 val int = Pretty.str o string_of_int; |
98 val int = Pretty.str o string_of_int; |
57 |
99 |
58 in |
100 in |
59 |
101 |
60 fun pretty_mixfix NoSyn = Pretty.str "" |
102 fun pretty_mixfix NoSyn = Pretty.str "" |
61 | pretty_mixfix (Mixfix (s, ps, p)) = |
103 | pretty_mixfix (Mixfix (s, ps, p, _)) = |
62 parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p]) |
104 parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p]) |
63 | pretty_mixfix (Delimfix s) = parens [quoted s] |
105 | pretty_mixfix (Delimfix (s, _)) = parens [quoted s] |
64 | pretty_mixfix (Infix (s, p)) = parens (Pretty.breaks [keyword "infix", quoted s, int p]) |
106 | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p]) |
65 | pretty_mixfix (Infixl (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) |
107 | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) |
66 | pretty_mixfix (Infixr (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) |
108 | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p]) |
67 | pretty_mixfix (Binder (s, p1, p2)) = |
109 | pretty_mixfix (Binder (s, p1, p2, _)) = |
68 parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2]) |
110 parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2]) |
69 | pretty_mixfix Structure = parens [keyword "structure"]; |
111 | pretty_mixfix (Structure _) = parens [keyword "structure"]; |
70 |
112 |
71 end; |
113 end; |
72 |
114 |
73 |
115 |
74 (* syntax specifications *) |
116 (* syntax specifications *) |
75 |
117 |
76 fun mixfix_args NoSyn = 0 |
118 fun mixfix_args NoSyn = 0 |
77 | mixfix_args (Mixfix (sy, _, _)) = Syntax_Ext.mfix_args sy |
119 | mixfix_args (Mixfix (sy, _, _, _)) = Syntax_Ext.mixfix_args sy |
78 | mixfix_args (Delimfix sy) = Syntax_Ext.mfix_args sy |
120 | mixfix_args (Delimfix (sy, _)) = Syntax_Ext.mixfix_args sy |
79 | mixfix_args (Infix (sy, _)) = 2 + Syntax_Ext.mfix_args sy |
121 | mixfix_args (Infix (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy |
80 | mixfix_args (Infixl (sy, _)) = 2 + Syntax_Ext.mfix_args sy |
122 | mixfix_args (Infixl (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy |
81 | mixfix_args (Infixr (sy, _)) = 2 + Syntax_Ext.mfix_args sy |
123 | mixfix_args (Infixr (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy |
82 | mixfix_args (Binder _) = 1 |
124 | mixfix_args (Binder _) = 1 |
83 | mixfix_args Structure = 0; |
125 | mixfix_args (Structure _) = 0; |
84 |
126 |
85 fun mixfixT (Binder _) = (dummyT --> dummyT) --> dummyT |
127 fun mixfixT (Binder _) = (dummyT --> dummyT) --> dummyT |
86 | mixfixT mx = replicate (mixfix_args mx) dummyT ---> dummyT; |
128 | mixfixT mx = replicate (mixfix_args mx) dummyT ---> dummyT; |
87 |
129 |
88 |
130 |
91 val typeT = Type ("type", []); |
133 val typeT = Type ("type", []); |
92 fun make_type n = replicate n typeT ---> typeT; |
134 fun make_type n = replicate n typeT ---> typeT; |
93 |
135 |
94 fun syn_ext_types type_decls = |
136 fun syn_ext_types type_decls = |
95 let |
137 let |
96 fun mk_infix sy ty t p1 p2 p3 = Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3); |
138 fun mk_infix sy ty t p1 p2 p3 = |
|
139 Syntax_Ext.Mfix |
|
140 (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)", |
|
141 ty, t, [p1, p2], p3); |
97 |
142 |
98 fun mfix_of (_, _, NoSyn) = NONE |
143 fun mfix_of (_, _, NoSyn) = NONE |
99 | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syntax_Ext.Mfix (sy, ty, t, ps, p)) |
144 | mfix_of (t, ty, Mixfix (sy, ps, p, _)) = |
100 | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], 1000)) |
145 SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, ps, p)) |
101 | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p) |
146 | mfix_of (t, ty, Delimfix (sy, _)) = |
102 | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p) |
147 SOME (Syntax_Ext.Mfix (Input.source_explode sy, ty, t, [], 1000)) |
103 | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p) |
148 | mfix_of (t, ty, Infix (sy, p, _)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p) |
|
149 | mfix_of (t, ty, Infixl (sy, p, _)) = SOME (mk_infix sy ty t p (p + 1) p) |
|
150 | mfix_of (t, ty, Infixr (sy, p, _)) = SOME (mk_infix sy ty t (p + 1) p p) |
104 | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t); |
151 | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t); |
105 |
152 |
106 fun check_args (_, ty, _) (SOME (mfix as Syntax_Ext.Mfix (sy, _, _, _, _))) = |
153 fun check_args (_, ty, mx) (SOME (mfix as Syntax_Ext.Mfix (sy, _, _, _, _))) = |
107 if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then () |
154 if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then () |
108 else Syntax_Ext.err_in_mfix "Bad number of type constructor arguments" mfix |
155 else |
|
156 error ("Bad number of type constructor arguments in mixfix annotation" ^ |
|
157 Position.here (pos_of mx)) |
109 | check_args _ NONE = (); |
158 | check_args _ NONE = (); |
110 |
159 |
111 val mfix = map mfix_of type_decls; |
160 val mfix = map mfix_of type_decls; |
112 val _ = map2 check_args type_decls mfix; |
161 val _ = map2 check_args type_decls mfix; |
113 val consts = map (fn (t, _, _) => (t, "")) type_decls; |
162 val consts = map (fn (t, _, _) => (t, "")) type_decls; |
120 val binder_name = suffix "_binder"; |
169 val binder_name = suffix "_binder"; |
121 |
170 |
122 fun syn_ext_consts logical_types const_decls = |
171 fun syn_ext_consts logical_types const_decls = |
123 let |
172 let |
124 fun mk_infix sy ty c p1 p2 p3 = |
173 fun mk_infix sy ty c p1 p2 p3 = |
125 [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], 1000), |
174 [Syntax_Ext.Mfix |
126 Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)]; |
175 (Symbol_Pos.explode0 "op " @ Input.source_explode sy, ty, c, [], 1000), |
|
176 Syntax_Ext.Mfix |
|
177 (Symbol_Pos.explode0 "(_ " @ Input.source_explode sy @ Symbol_Pos.explode0 "/ _)", |
|
178 ty, c, [p1, p2], p3)]; |
127 |
179 |
128 fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = |
180 fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) = |
129 [Type ("idts", []), ty2] ---> ty3 |
181 [Type ("idts", []), ty2] ---> ty3 |
130 | binder_typ c _ = error ("Bad type of binder: " ^ quote c); |
182 | binder_typ c _ = error ("Bad type of binder: " ^ quote c); |
131 |
183 |
132 fun mfix_of (_, _, NoSyn) = [] |
184 fun mfix_of (_, _, NoSyn) = [] |
133 | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syntax_Ext.Mfix (sy, ty, c, ps, p)] |
185 | mfix_of (c, ty, Mixfix (sy, ps, p, _)) = |
134 | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], 1000)] |
186 [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, ps, p)] |
135 | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p |
187 | mfix_of (c, ty, Delimfix (sy, _)) = |
136 | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p |
188 [Syntax_Ext.Mfix (Input.source_explode sy, ty, c, [], 1000)] |
137 | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p |
189 | mfix_of (c, ty, Infix (sy, p, _)) = mk_infix sy ty c (p + 1) (p + 1) p |
138 | mfix_of (c, ty, Binder (sy, p, q)) = |
190 | mfix_of (c, ty, Infixl (sy, p, _)) = mk_infix sy ty c p (p + 1) p |
139 [Syntax_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)] |
191 | mfix_of (c, ty, Infixr (sy, p, _)) = mk_infix sy ty c (p + 1) p p |
140 | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c); |
192 | mfix_of (c, ty, Binder (sy, p, q, _)) = |
|
193 [Syntax_Ext.Mfix |
|
194 (Symbol_Pos.explode0 "(3" @ Input.source_explode sy @ Symbol_Pos.explode0 "_./ _)", |
|
195 binder_typ c ty, (binder_name c), [0, p], q)] |
|
196 | mfix_of (c, _, mx) = |
|
197 error ("Bad mixfix declaration for " ^ quote c ^ Position.here (pos_of mx)); |
141 |
198 |
142 fun binder (c, _, Binder _) = SOME (binder_name c, c) |
199 fun binder (c, _, Binder _) = SOME (binder_name c, c) |
143 | binder _ = NONE; |
200 | binder _ = NONE; |
144 |
201 |
145 val mfix = maps mfix_of const_decls; |
202 val mfix = maps mfix_of const_decls; |