162 |
163 |
163 (*get nonterminal for lhs*) |
164 (*get nonterminal for lhs*) |
164 val typ_to_nonterm1 = typ_to_nt logic; |
165 val typ_to_nonterm1 = typ_to_nt logic; |
165 |
166 |
166 |
167 |
|
168 (* scan_mixfix, mixfix_args *) |
|
169 |
|
170 local |
|
171 fun is_meta c = c mem ["(", ")", "/", "_"]; |
|
172 |
|
173 fun scan_delim_char ("'" :: c :: cs) = |
|
174 if is_blank c then raise LEXICAL_ERROR else (c, cs) |
|
175 | scan_delim_char ["'"] = error "Trailing escape character" |
|
176 | scan_delim_char (chs as c :: cs) = |
|
177 if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs) |
|
178 | scan_delim_char [] = raise LEXICAL_ERROR; |
|
179 |
|
180 val scan_sym = |
|
181 $$ "_" >> K (Argument ("", 0)) || |
|
182 $$ "(" -- Term.scan_int >> (Bg o #2) || |
|
183 $$ ")" >> K En || |
|
184 $$ "/" -- $$ "/" >> K (Brk ~1) || |
|
185 $$ "/" -- scan_any is_blank >> (Brk o length o #2) || |
|
186 scan_any1 is_blank >> (Space o implode) || |
|
187 repeat1 scan_delim_char >> (Delim o implode); |
|
188 |
|
189 val scan_symb = |
|
190 scan_sym >> Some || |
|
191 $$ "'" -- scan_one is_blank >> K None; |
|
192 |
|
193 val scan_symbs = mapfilter I o #1 o repeat scan_symb; |
|
194 in |
|
195 val scan_mixfix = scan_symbs o SymbolFont.read_charnames o explode; |
|
196 end; |
|
197 |
|
198 fun mixfix_args mx = |
|
199 foldl (fn (i, Argument _) => i + 1 | (i, _) => i) (0, scan_mixfix mx); |
|
200 |
|
201 |
167 (* mfix_to_xprod *) |
202 (* mfix_to_xprod *) |
168 |
203 |
169 fun mfix_to_xprod convert logtypes (Mfix (sy, typ, const, pris, pri)) = |
204 fun mfix_to_xprod convert logtypes (Mfix (sy, typ, const, pris, pri)) = |
170 let |
205 let |
171 fun err msg = |
206 fun err msg = |
172 (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " ^ quote const); |
207 (if msg = "" then () else error_msg msg; |
173 error msg); |
208 error ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const)); |
174 fun post_err () = error ("The error(s) above occurred in mixfix annotation " ^ |
|
175 quote sy ^ " for " ^ quote const); |
|
176 |
209 |
177 fun check_pri p = |
210 fun check_pri p = |
178 if p >= 0 andalso p <= max_pri then () |
211 if p >= 0 andalso p <= max_pri then () |
179 else err ("precedence out of range: " ^ string_of_int p); |
212 else err ("Precedence out of range: " ^ string_of_int p); |
180 |
213 |
181 fun blocks_ok [] 0 = true |
214 fun blocks_ok [] 0 = true |
182 | blocks_ok [] _ = false |
215 | blocks_ok [] _ = false |
183 | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1) |
216 | blocks_ok (Bg _ :: syms) n = blocks_ok syms (n + 1) |
184 | blocks_ok (En :: _) 0 = false |
217 | blocks_ok (En :: _) 0 = false |
185 | blocks_ok (En :: syms) n = blocks_ok syms (n - 1) |
218 | blocks_ok (En :: syms) n = blocks_ok syms (n - 1) |
186 | blocks_ok (_ :: syms) n = blocks_ok syms n; |
219 | blocks_ok (_ :: syms) n = blocks_ok syms n; |
187 |
220 |
188 fun check_blocks syms = |
221 fun check_blocks syms = |
189 if blocks_ok syms 0 then () |
222 if blocks_ok syms 0 then () |
190 else err "unbalanced block parentheses"; |
223 else err "Unbalanced block parentheses"; |
191 |
|
192 |
|
193 local |
|
194 fun is_meta c = c mem ["(", ")", "/", "_"]; |
|
195 |
|
196 fun scan_delim_char ("'" :: c :: cs) = |
|
197 if is_blank c then raise LEXICAL_ERROR else (c, cs) |
|
198 | scan_delim_char ["'"] = err "trailing escape character" |
|
199 | scan_delim_char (chs as c :: cs) = |
|
200 if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs) |
|
201 | scan_delim_char [] = raise LEXICAL_ERROR; |
|
202 |
|
203 val scan_sym = |
|
204 $$ "_" >> K (Argument ("", 0)) || |
|
205 $$ "(" -- scan_int >> (Bg o #2) || |
|
206 $$ ")" >> K En || |
|
207 $$ "/" -- $$ "/" >> K (Brk ~1) || |
|
208 $$ "/" -- scan_any is_blank >> (Brk o length o #2) || |
|
209 scan_any1 is_blank >> (Space o implode) || |
|
210 repeat1 scan_delim_char >> (Delim o implode); |
|
211 |
|
212 val scan_symb = |
|
213 scan_sym >> Some || |
|
214 $$ "'" -- scan_one is_blank >> K None; |
|
215 in |
|
216 val scan_symbs = mapfilter I o #1 o repeat scan_symb; |
|
217 end; |
|
218 |
224 |
219 |
225 |
220 val cons_fst = apfst o cons; |
226 val cons_fst = apfst o cons; |
221 |
227 |
222 fun add_args [] ty [] = ([], typ_to_nonterm1 ty) |
228 fun add_args [] ty [] = ([], typ_to_nonterm1 ty) |
223 | add_args [] _ _ = err "too many precedences" |
229 | add_args [] _ _ = err "Too many precedences" |
224 | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] = |
230 | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] = |
225 cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys []) |
231 cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys []) |
226 | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) = |
232 | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) = |
227 cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps) |
233 cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps) |
228 | add_args (Argument _ :: _) _ _ = |
234 | add_args (Argument _ :: _) _ _ = |
229 err "more arguments than in corresponding type" |
235 err "More arguments than in corresponding type" |
230 | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps); |
236 | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps); |
231 |
237 |
232 |
238 |
233 fun is_arg (Argument _) = true |
239 fun is_arg (Argument _) = true |
234 | is_arg _ = false; |
240 | is_arg _ = false; |