equal
deleted
inserted
replaced
216 |
216 |
217 val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'"); |
217 val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (~$$ "'"); |
218 val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs; |
218 val read_symbs = map_filter I o the o Scan.read Symbol.stopper scan_symbs; |
219 |
219 |
220 fun unique_index xsymbs = |
220 fun unique_index xsymbs = |
221 if length (List.filter is_index xsymbs) <= 1 then xsymbs |
221 if length (filter is_index xsymbs) <= 1 then xsymbs |
222 else error "Duplicate index arguments (\\<index>)"; |
222 else error "Duplicate index arguments (\\<index>)"; |
223 |
223 |
224 in |
224 in |
225 |
225 |
226 val read_mfix = unique_index o read_symbs o Symbol.explode; |
226 val read_mfix = unique_index o read_symbs o Symbol.explode; |
227 |
227 |
228 fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) []; |
228 fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) []; |
229 val mfix_args = length o List.filter is_argument o read_mfix; |
229 val mfix_args = length o filter is_argument o read_mfix; |
230 |
230 |
231 val escape_mfix = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode; |
231 val escape_mfix = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode; |
232 |
232 |
233 end; |
233 end; |
234 |
234 |
274 if s <> "prop" andalso is_logtype s then Argument (logic, p) else a |
274 if s <> "prop" andalso is_logtype s then Argument (logic, p) else a |
275 | logify_types a = a; |
275 | logify_types a = a; |
276 |
276 |
277 |
277 |
278 val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix; |
278 val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix; |
279 val args = List.filter (fn Argument _ => true | _ => false) raw_symbs; |
279 val args = filter (fn Argument _ => true | _ => false) raw_symbs; |
280 val (const', typ', parse_rules) = |
280 val (const', typ', parse_rules) = |
281 if not (exists is_index args) then (const, typ, []) |
281 if not (exists is_index args) then (const, typ, []) |
282 else |
282 else |
283 let |
283 let |
284 val indexed_const = if const <> "" then "_indexed_" ^ const |
284 val indexed_const = if const <> "" then "_indexed_" ^ const |
310 |
310 |
311 val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs'); |
311 val _ = (List.app check_pri pris; check_pri pri; check_blocks symbs'); |
312 val xprod' = |
312 val xprod' = |
313 if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix |
313 if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix |
314 else if const <> "" then xprod |
314 else if const <> "" then xprod |
315 else if length (List.filter is_argument symbs') <> 1 then |
315 else if length (filter is_argument symbs') <> 1 then |
316 err_in_mfix "Copy production must have exactly one argument" mfix |
316 err_in_mfix "Copy production must have exactly one argument" mfix |
317 else if exists is_terminal symbs' then xprod |
317 else if exists is_terminal symbs' then xprod |
318 else XProd (lhs', map rem_pri symbs', "", chain_pri); |
318 else XProd (lhs', map rem_pri symbs', "", chain_pri); |
319 |
319 |
320 in (xprod', parse_rules) end; |
320 in (xprod', parse_rules) end; |