--- a/src/Pure/Thy/thy_parse.ML Fri Dec 01 12:03:13 1995 +0100
+++ b/src/Pure/Thy/thy_parse.ML Fri Dec 01 12:22:07 1995 +0100
@@ -259,53 +259,46 @@
(* consts *)
-val simple_type = ident ||
- (kind TypeVar -- optional ("::" $$-- ident >> cat "::") "" >>
- (fn (tv, cl) => tv ^ cl));
+(*Parse an identifier, but only if it is not followed by colons or a comma;
+ the exclusion of a postfix comma can be controlled to allow expressions
+ like "(id, id)" but disallow ones like "'a => id id,id :: ..."*)
+fun ident_no_colon _ [] = eof_err()
+ | ident_no_colon allow_comma ((Ident, s, n) :: (rest as (Keyword, s2, n2) ::
+ toks)) =
+ if s2 = "::" orelse (not allow_comma andalso s2 = ",") then
+ syn_err (name_of_kind Ident) (quote s2) n2
+ else (s, rest)
+ | ident_no_colon _ ((Ident, s, n) :: toks) = (s, toks)
+ | ident_no_colon _ ((k, s, n) :: _) =
+ syn_err (name_of_kind Ident) (quote s) n;
-(*Types with type arguments, like e.g. "'a list list"*)
-fun complex_type toks =
- let val typ = simple_type || "(" $$-- complex_type --$$ ")" >> parens;
- val typ2 = complex_type || "(" $$-- complex_type --$$ ")" >> parens;
- in
- (typ -- repeat ident >> (fn (t, ts) => space_implode " " (t::ts)) ||
- "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 ident) >>
- (fn (tas, ts) => space_implode " " (parens (commas tas) :: ts))) toks
+fun const_type allow_comma toks =
+ let val simple_type =
+ (ident ||
+ kind TypeVar -- optional ("::" $$-- ident >> cat "::") "" >>
+ (fn (tv, cl) => cat tv cl)) --
+ repeat (ident_no_colon allow_comma) >>
+ (fn (args, ts) => cat args (space_implode " " ts)) ||
+ ("(" $$-- (list1 (const_type true)) --$$ ")" >> (parens o commas)) --
+ repeat1 (ident_no_colon allow_comma) >>
+ (fn (args, ts) => cat args (space_implode " " ts));
+
+ val appl_param =
+ simple_type || "(" $$-- const_type true --$$ ")" >> parens ||
+ "[" $$-- (list1 (const_type true)) --$$ "]" --$$ "=>" --
+ const_type allow_comma >>
+ (fn (src, dest) => mk_list src ^ " => " ^ dest);
+ in ("[" $$-- (list1 (const_type true)) --$$ "]" --$$ "=>" --
+ const_type allow_comma >>
+ (fn (src, dest) => mk_list src ^ " => " ^ dest) ||
+ repeat1 (appl_param --$$ "=>") -- const_type allow_comma >>
+ (fn (src, dest) => space_implode " => " (src@[dest])) ||
+ simple_type ||
+ "(" $$-- const_type true --$$ ")" >> parens) toks
end;
-(*Const type which is limited at the end by "=>", ")", "]" or ","*)
-fun param_type toks =
- ((complex_type || "(" $$-- param_type --$$ ")" >> parens ||
- "[" $$-- (list1 param_type) --$$ "]" >> mk_list) --
- repeat ("=>" $$-- param_type >> cat " =>") >>
- (fn (t, ts) => t ^ implode ts)) toks;
-
-(*Parse an identifier, but only if it is not followed by colons or a comma*)
-fun ident_no_colon [] = eof_err()
- | ident_no_colon ((Ident, s, n) :: (rest as (Keyword, s2, n2) :: toks)) =
- if s2 = "::" orelse s2 = "," then
- syn_err (name_of_kind Ident) (quote s2) n2
- else (s, rest)
- | ident_no_colon ((Ident, s, n) :: toks) = (s, toks)
- | ident_no_colon ((k, s, n) :: _) =
- syn_err (name_of_kind Ident) (quote s) n;
-
-(*Type after last "=>"*)
-val appl_last =
- (simple_type || "(" $$-- param_type --$$ ")" >> parens) --
- repeat ident_no_colon >> (fn (t, ts) => space_implode " " (t::ts));
-
-(*Type specified before "=>"*)
-val appl_param =
- (complex_type || "(" $$-- param_type --$$ ")" >> parens ||
- "[" $$-- !! (list1 param_type) --$$ "]" >> (brackets o commas)) --$$ "=>";
-
-(*Top level const type*)
-val const_type = repeat appl_param -- appl_last >>
- (fn (ts, t) => space_implode " => " (ts@[t]));
-
val const_decls = repeat1 (names1 --$$ "::" -- !!
- ((string || const_type>>quote) -- opt_mixfix)) >>
+ ((string || const_type false >> quote) -- opt_mixfix)) >>
(mk_big_list o map mk_triple2 o split_decls);