simplified parser for constType
authorclasohm
Fri Dec 01 12:22:07 1995 +0100 (1995-12-01)
changeset 1377f800f533aa83
parent 1376 92f83b9d17e1
child 1378 042899454032
simplified parser for constType
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Dec 01 12:03:13 1995 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Fri Dec 01 12:22:07 1995 +0100
     1.3 @@ -259,53 +259,46 @@
     1.4  
     1.5  (* consts *)
     1.6  
     1.7 -val simple_type = ident ||
     1.8 -  (kind TypeVar -- optional ("::" $$-- ident >> cat "::") "" >>
     1.9 -   (fn (tv, cl) => tv ^ cl));
    1.10 +(*Parse an identifier, but only if it is not followed by colons or a comma;
    1.11 +  the exclusion of a postfix comma can be controlled to allow expressions
    1.12 +  like "(id, id)" but disallow ones like "'a => id id,id :: ..."*)
    1.13 +fun ident_no_colon _ [] = eof_err()
    1.14 +  | ident_no_colon allow_comma ((Ident, s, n) :: (rest as (Keyword, s2, n2) ::
    1.15 +                                toks)) =
    1.16 +      if s2 = "::" orelse (not allow_comma andalso s2 = ",") then
    1.17 +        syn_err (name_of_kind Ident) (quote s2) n2
    1.18 +      else (s, rest)
    1.19 +  | ident_no_colon _ ((Ident, s, n) :: toks) = (s, toks)
    1.20 +  | ident_no_colon _ ((k, s, n) :: _) =
    1.21 +      syn_err (name_of_kind Ident) (quote s) n;
    1.22  
    1.23 -(*Types with type arguments, like e.g. "'a list list"*)
    1.24 -fun complex_type toks =
    1.25 -  let val typ = simple_type || "(" $$-- complex_type --$$ ")" >> parens;
    1.26 -      val typ2 = complex_type || "(" $$-- complex_type --$$ ")" >> parens;
    1.27 -  in
    1.28 -   (typ -- repeat ident >> (fn (t, ts) => space_implode " " (t::ts)) ||
    1.29 -    "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 ident) >>
    1.30 -      (fn (tas, ts) => space_implode " " (parens (commas tas) :: ts))) toks
    1.31 +fun const_type allow_comma toks =
    1.32 +  let val simple_type =
    1.33 +        (ident ||
    1.34 +         kind TypeVar -- optional ("::" $$-- ident >> cat "::") "" >>
    1.35 +           (fn (tv, cl) => cat tv cl)) --
    1.36 +           repeat (ident_no_colon allow_comma) >>
    1.37 +           (fn (args, ts) => cat args (space_implode " " ts)) ||
    1.38 +         ("(" $$-- (list1 (const_type true)) --$$ ")" >> (parens o commas)) --
    1.39 +           repeat1 (ident_no_colon allow_comma) >>
    1.40 +           (fn (args, ts) => cat args (space_implode " " ts));
    1.41 +
    1.42 +      val appl_param =
    1.43 +        simple_type || "(" $$-- const_type true --$$ ")" >> parens || 
    1.44 +        "[" $$-- (list1 (const_type true)) --$$ "]" --$$ "=>" --
    1.45 +          const_type allow_comma >>
    1.46 +          (fn (src, dest) => mk_list src ^ " => " ^ dest);
    1.47 +  in ("[" $$-- (list1 (const_type true)) --$$ "]" --$$ "=>" --
    1.48 +        const_type allow_comma >>
    1.49 +        (fn (src, dest) => mk_list src ^ " => " ^ dest) ||
    1.50 +      repeat1 (appl_param --$$ "=>") -- const_type allow_comma >>
    1.51 +        (fn (src, dest) => space_implode " => " (src@[dest])) ||
    1.52 +      simple_type ||
    1.53 +      "(" $$-- const_type true --$$ ")" >> parens) toks
    1.54    end;
    1.55  
    1.56 -(*Const type which is limited at the end by "=>", ")", "]" or ","*)
    1.57 -fun param_type toks =
    1.58 -  ((complex_type || "(" $$-- param_type --$$ ")" >> parens ||
    1.59 -    "[" $$-- (list1 param_type) --$$ "]" >> mk_list) --
    1.60 -     repeat ("=>" $$-- param_type >> cat " =>") >>
    1.61 -     (fn (t, ts) => t ^ implode ts)) toks;
    1.62 -
    1.63 -(*Parse an identifier, but only if it is not followed by colons or a comma*)
    1.64 -fun ident_no_colon [] = eof_err()
    1.65 -  | ident_no_colon ((Ident, s, n) :: (rest as (Keyword, s2, n2) :: toks)) =
    1.66 -      if s2 = "::" orelse s2 = "," then
    1.67 -        syn_err (name_of_kind Ident) (quote s2) n2
    1.68 -      else (s, rest)
    1.69 -  | ident_no_colon ((Ident, s, n) :: toks) = (s, toks)
    1.70 -  | ident_no_colon ((k, s, n) :: _) =
    1.71 -      syn_err (name_of_kind Ident) (quote s) n;
    1.72 -
    1.73 -(*Type after last "=>"*)
    1.74 -val appl_last =
    1.75 -  (simple_type || "(" $$-- param_type --$$ ")" >> parens) --
    1.76 -  repeat ident_no_colon >> (fn (t, ts) => space_implode " " (t::ts));
    1.77 -
    1.78 -(*Type specified before "=>"*)
    1.79 -val appl_param =
    1.80 -  (complex_type || "(" $$-- param_type --$$ ")" >> parens ||
    1.81 -   "[" $$-- !! (list1 param_type) --$$ "]" >> (brackets o commas)) --$$ "=>";
    1.82 -
    1.83 -(*Top level const type*)
    1.84 -val const_type = repeat appl_param -- appl_last >>
    1.85 -  (fn (ts, t) => space_implode " => " (ts@[t]));
    1.86 -
    1.87  val const_decls = repeat1 (names1 --$$ "::" -- !!
    1.88 -                    ((string || const_type>>quote) -- opt_mixfix)) >>
    1.89 +                    ((string || const_type false >> quote) -- opt_mixfix)) >>
    1.90                    (mk_big_list o map mk_triple2 o split_decls);
    1.91  
    1.92