1.1 --- a/src/Pure/Thy/syntax.ML Thu Feb 03 13:56:44 1994 +0100
1.2 +++ b/src/Pure/Thy/syntax.ML Thu Feb 03 13:57:04 1994 +0100
1.3 @@ -25,6 +25,8 @@
1.4
1.5 fun pair(a, b) = parent(a ^ ", " ^ b);
1.6
1.7 +fun triple(a, b, c) = parent(a ^ ", " ^ b ^ ", " ^ c);
1.8 +
1.9 fun pair_quote(a, b) = pair(quote a, quote b);
1.10
1.11 fun pair_quote2(a, b) = pair(a, quote b);
1.12 @@ -54,14 +56,28 @@
1.13
1.14
1.15 datatype pfix_or_mfix = Pref of string | Mixf of string;
1.16 +datatype type_or_abbr = Typed of pfix_or_mfix | Abbrd of pfix_or_mfix;
1.17
1.18 fun pm_proj(Pref s) = s
1.19 | pm_proj(Mixf s) = s;
1.20
1.21 +fun ta_proj(Typed s) = s
1.22 + | ta_proj(Abbrd s) = s;
1.23 +
1.24 fun split_decls l =
1.25 let val (p, m) = partition (fn Pref _ => true | _ => false) l;
1.26 in (big_bracket_comma_ind " " (map pm_proj p), map pm_proj m) end;
1.27
1.28 +fun split_decls_type l =
1.29 + let val (t,a) = partition (fn Typed _ => true | _ => false) l
1.30 + val (tp,tm) = partition (fn Pref _ => true | _ => false) (map ta_proj t)
1.31 + val (ap,am) = partition (fn Pref _ => true | _ => false) (map ta_proj a)
1.32 + in (big_bracket_comma_ind " " (map pm_proj tp),
1.33 + big_bracket_comma_ind " " (map pm_proj ap),
1.34 + (map pm_proj tm) @ (map pm_proj am))
1.35 + end;
1.36 +
1.37 +
1.38 fun delim_mix (s, None) = Delimfix(s)
1.39 | delim_mix (s, Some(l, n)) = Mixfix(s, l, n);
1.40
1.41 @@ -94,15 +110,19 @@
1.42 Mixf(mk_mfix((c, ty), mfix)) :: mk_mixfix((cs, ty), Some(mfix))
1.43 | mk_mixfix(([], _), _) = [];
1.44
1.45 -fun mk_type_decl((ts, n), None) = [Pref(pair(bracket_comma_quote ts, n))]
1.46 +fun mk_type_decl((ts, n), None) = [Typed(Pref(pair(bracket_comma_quote ts, n)))]
1.47 | mk_type_decl((t::ts, n), Some(tinfix)) =
1.48 - [Pref(pair(bracket(quote t), n)), Mixf(mk_mfix((t, n), tinfix))] @
1.49 + [Typed(Pref(pair(bracket(quote t), n))), Typed(Mixf(mk_mfix((t, n), tinfix)))] @
1.50 mk_type_decl((ts, n), Some(tinfix))
1.51 | mk_type_decl(([], n), Some(tinfix)) = [];
1.52
1.53 +fun mk_abbr_decl(((ts, a), b), None) =
1.54 + [Abbrd(Pref(triple(quote a, ts, quote b)))]
1.55 + | mk_abbr_decl(((ts, a), b), Some(tinfix)) =
1.56 + [Abbrd(Pref(triple(quote a, ts, quote b))), Abbrd(Mixf(mk_mfix((a, "0"), tinfix)))];
1.57
1.58 -fun mk_extension (((((((cl, def), (ty, tinfix)), ar), (co, mfix)), tr), ax), ml) =
1.59 - ((cl, def, ty, ar, co, ax), big_bracket_comma_ind " " tinfix,
1.60 +fun mk_extension (((((((cl, def), (ty, ab, tinfix)), ar), (co, mfix)), tr), ax), ml) =
1.61 + ((cl, def, ty, ab, ar, co, ax), big_bracket_comma_ind " " tinfix,
1.62 big_bracket_comma_ind " " mfix, big_bracket_comma_ind " " tr, ml);
1.63
1.64 fun add_val((id, _), s) = "val " ^ id ^ " = get_axiom thy " ^ quote id ^ "\n" ^ s;
1.65 @@ -130,8 +150,8 @@
1.66 fun mk_simple_sext mfix =
1.67 "Some (Syntax.simple_sext\n " ^ mfix ^ ")";
1.68
1.69 -fun mk_ext ((cl, def, ty, ar, co, ax), sext) =
1.70 - " (" ^ space_implode ",\n " [cl, def, ty, "[]",ar, co, sext] ^ ")\n " ^ ax ^ "\n";
1.71 +fun mk_ext ((cl, def, ty, ab, ar, co, ax), sext) =
1.72 + " (" ^ space_implode ",\n " [cl, def, ty, ab, ar, co, sext] ^ ")\n " ^ ax ^ "\n";
1.73
1.74 fun mk_ext_thy (base, name, ext, sext) =
1.75 "extend_theory (" ^ base ^ ")\n " ^ quote name ^ "\n" ^ mk_ext (ext, sext);
1.76 @@ -149,7 +169,7 @@
1.77
1.78 fun mk_structure ((name, base), Some (ext, tinfix, mfix, trans, ml)) =
1.79 let
1.80 - val noext = ("[]", "[]", "[]", "[]", "[]", "[]");
1.81 + val noext = ("[]", "[]", "[]", "[]", "[]", "[]", "[]");
1.82 val basethy =
1.83 if tinfix = "[]" then base ^ (quote name)
1.84 else mk_ext_thy (base ^ (quote name), name ^ "(type infix)", noext, mk_simple_sext tinfix);
1.85 @@ -189,6 +209,7 @@
1.86 (* -> "[id1, id2, ..., idn]" *)
1.87
1.88 val stgorids = list_of1 (stg || id);
1.89 +val stgorid = stg || id;
1.90
1.91 val sort = id >> (bracket o quote)
1.92 || "{" $$-- (ids || emptyl) --$$ "}";
1.93 @@ -232,21 +253,35 @@
1.94
1.95 (*-------------------- TYPES PARSER ----------------------*)
1.96
1.97 +val xtypevar = typevar >> quote;
1.98
1.99 -val type_decl = stgorids -- nat;
1.100 +val type_vars_decl = xtypevar >> (fn t => [t])
1.101 + || "(" $$-- list_of1(xtypevar) --$$ ")"
1.102 + || empty >> K [];
1.103 +
1.104 +val abbr_vars_decl = xtypevar >> bracket
1.105 + || "(" $$-- list_of1(xtypevar) --$$ ")" >> bracket_comma
1.106 + || empty >> K "[]";
1.107 +
1.108 +val type_decl = stgorids -- nat
1.109 + || type_vars_decl -- stgorid
1.110 + >> (fn (ns,t) => ([t], string_of_int(length(ns))));
1.111 +
1.112 +val abbr_decl = abbr_vars_decl -- stgorid --$$ "=" -- stg;
1.113
1.114 val tyinfix = infxl >> (Some o TInfixl)
1.115 || infxr >> (Some o TInfixr);
1.116
1.117 -val type_infix = "(" $$-- !! (tyinfix --$$ ")")
1.118 +val type_infix = "(" $$-- tyinfix --$$ ")"
1.119 || empty >> K None;
1.120
1.121 val types = "types" $$--
1.122 - !! (repeat1 (type_decl -- type_infix >> mk_type_decl))
1.123 - >> (split_decls o flat)
1.124 - || empty >> (K ("[]", []));
1.125 + !! (repeat1 ((abbr_decl -- type_infix >> mk_abbr_decl)
1.126 + || (type_decl -- type_infix >> mk_type_decl)))
1.127 + >> (split_decls_type o flat)
1.128 + || empty >> (K ("[]", "[]", []));
1.129
1.130 - (* ==> ("[(id, nat), ... ]", [strg, ...]) *)
1.131 + (* ==> ("[(id, nat), ... ]", "[(id, typevars, stg), ...]", [strg, ...]) *)
1.132
1.133
1.134