extended complex_typ
authorclasohm
Thu Nov 02 12:45:58 1995 +0100 (1995-11-02 ago)
changeset 1316ce35d42d2190
parent 1315 1b731d0b5ad3
child 1317 83ce32aa4e9b
extended complex_typ
src/HOL/thy_syntax.ML
     1.1 --- a/src/HOL/thy_syntax.ML	Fri Oct 27 12:21:02 1995 +0100
     1.2 +++ b/src/HOL/thy_syntax.ML	Thu Nov 02 12:45:58 1995 +0100
     1.3 @@ -139,17 +139,25 @@
     1.4  
     1.5    (*parsers*)
     1.6    val tvars = type_args >> map (cat "dtVar");
     1.7 +
     1.8 +  val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote) ||
     1.9 +    type_var >> cat "dtVar";
    1.10 +
    1.11    fun complex_typ toks =
    1.12 -    (("(" $$-- complex_typ  --$$ ")" >> (fn x => [x]) || tvars)
    1.13 -     -- (ident>>quote) >> (cat "dtTyp" o mk_pair o apfst mk_list)
    1.14 -     || type_var >> cat "dtVar") toks;
    1.15 -  val simple_typ = ident>>(cat "dtTyp" o curry mk_pair "[]" o quote) ||
    1.16 -    type_var >> cat "dtVar";
    1.17 +    let val typ = simple_typ || "(" $$-- complex_typ --$$ ")";
    1.18 +        val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")";
    1.19 +    in
    1.20 +     (typ -- repeat (ident>>quote) >>
    1.21 +        (foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y))) ||
    1.22 +      "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 (ident>>quote)) >>
    1.23 +       (fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^
    1.24 +                         mk_pair (brackets x, y)) (commas fst, ids))) toks
    1.25 +    end;
    1.26 +
    1.27    val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")"));
    1.28    val constructor = name -- opt_typs -- opt_mixfix;
    1.29  in
    1.30    val datatype_decl =
    1.31 -    (* FIXME tvars -> type_args *)
    1.32      tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params;
    1.33  end;
    1.34