src/Pure/Thy/thy_parse.ML
changeset 1321 9a6e7bd2bfaf
parent 1250 000ecb4fc700
child 1371 2f97fc253763
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Fri Nov 03 12:00:46 1995 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Nov 07 12:57:20 1995 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4    val strip_quotes: string -> string
     1.5  end;
     1.6  
     1.7 -functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE =
     1.8 +functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE=
     1.9  struct
    1.10  
    1.11  open ThyScan;
    1.12 @@ -253,13 +253,58 @@
    1.13  val type_decl = type_args -- name -- optional ("=" $$-- !! string >> Some) None
    1.14    -- opt_infix >> mk_type_decl;
    1.15  
    1.16 -val type_decls = repeat1 (old_type_decl || type_decl) >> (mk_type_decls o flat);
    1.17 +val type_decls = repeat1 (old_type_decl || type_decl) >>
    1.18 +                 (mk_type_decls o flat);
    1.19  
    1.20  
    1.21  (* consts *)
    1.22  
    1.23 -val const_decls = repeat1 (names1 --$$ "::" -- !! (string -- opt_mixfix))
    1.24 -  >> (mk_big_list o map mk_triple2 o split_decls);
    1.25 +val simple_type = ident || kind TypeVar;
    1.26 +
    1.27 +(*Types with type arguments, like e.g. "'a list list"*)
    1.28 +fun complex_type toks =
    1.29 +  let val typ = simple_type || "(" $$-- complex_type --$$ ")" >> parens;
    1.30 +      val typ2 = complex_type || "(" $$-- complex_type --$$ ")" >> parens;
    1.31 +  in
    1.32 +   (typ -- repeat ident >> (fn (t, ts) => space_implode " " (t::ts)) ||
    1.33 +    "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 ident) >>
    1.34 +      (fn (tas, ts) => space_implode " " (parens (commas tas) :: ts))) toks
    1.35 +  end;
    1.36 +
    1.37 +(*Const type which is limited at the end by "=>", ")", "]" or ","*)
    1.38 +fun param_type toks =
    1.39 +  ((complex_type || "(" $$-- param_type --$$ ")" >> parens ||
    1.40 +    "[" $$-- !! (list1 param_type) --$$ "]" >> mk_list) --
    1.41 +     repeat ("=>" $$-- param_type >> cat " =>") >>
    1.42 +     (fn (t, ts) => t ^ implode ts)) toks;
    1.43 +
    1.44 +(*Parse an identifier, but only if it is not followed by colons or a comma*)
    1.45 +fun ident_no_colon [] = eof_err()
    1.46 +  | ident_no_colon ((Ident, s, n) :: (rest as (Keyword, s2, n2) :: toks)) =
    1.47 +      if s2 = "::" orelse s2 = "," then
    1.48 +        syn_err (name_of_kind Ident) (quote s2) n2
    1.49 +      else (s, rest)
    1.50 +  | ident_no_colon ((Ident, s, n) :: toks) = (s, toks)
    1.51 +  | ident_no_colon ((k, s, n) :: _) =
    1.52 +      syn_err (name_of_kind Ident) (quote s) n;
    1.53 +
    1.54 +(*Type after last "=>"*)
    1.55 +val appl_last =
    1.56 +  (simple_type || "(" $$-- param_type --$$ ")" >> parens) --
    1.57 +  repeat ident_no_colon >> (fn (t, ts) => space_implode " " (t::ts));
    1.58 +
    1.59 +(*Type specified before "=>"*)
    1.60 +val appl_param =
    1.61 +  (complex_type || "(" $$-- param_type --$$ ")" >> parens ||
    1.62 +   "[" $$-- !! (list1 param_type) --$$ "]" >> (brackets o commas)) --$$ "=>";
    1.63 +
    1.64 +(*Top level const type*)
    1.65 +val const_type = repeat appl_param -- appl_last >>
    1.66 +  (fn (ts, t) => space_implode " => " (ts@[t]));
    1.67 +
    1.68 +val const_decls = repeat1 (names1 --$$ "::" -- !!
    1.69 +                    ((string || const_type>>quote) -- opt_mixfix)) >>
    1.70 +                  (mk_big_list o map mk_triple2 o split_decls);
    1.71  
    1.72  
    1.73  (* translations *)