# HG changeset patch # User wenzelm # Date 1323814947 -3600 # Node ID 3fd2cd187299334a19d5119fc5916e916c1a02db # Parent fe1ef1f3ee55c5d89748c011248ed83e375a4c28# Parent 43a5b86bc1026fd8ec31142f5a07c929dfe39c34 merged diff -r fe1ef1f3ee55 -r 3fd2cd187299 NEWS --- a/NEWS Tue Dec 13 22:44:16 2011 +0100 +++ b/NEWS Tue Dec 13 23:22:27 2011 +0100 @@ -53,6 +53,8 @@ *** HOL *** +* 'datatype' specifications allow explicit sort constraints. + * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, use theory HOL/Library/Nat_Bijection instead. diff -r fe1ef1f3ee55 -r 3fd2cd187299 doc-src/IsarRef/Thy/HOL_Specific.thy --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Dec 13 22:44:16 2011 +0100 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Dec 13 23:22:27 2011 +0100 @@ -693,7 +693,7 @@ @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +) ; - spec: @{syntax typespec} @{syntax mixfix}? '=' (cons + '|') + spec: @{syntax typespec_sorts} @{syntax mixfix}? '=' (cons + '|') ; cons: @{syntax name} (@{syntax type} * ) @{syntax mixfix}? "} diff -r fe1ef1f3ee55 -r 3fd2cd187299 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Dec 13 22:44:16 2011 +0100 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Dec 13 23:22:27 2011 +0100 @@ -1036,7 +1036,7 @@ \rail@endplus \rail@end \rail@begin{2}{\isa{spec}} -\rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[] +\rail@nont{\hyperlink{syntax.typespec-sorts}{\mbox{\isa{typespec{\isaliteral{5F}{\isacharunderscore}}sorts}}}}[] \rail@bar \rail@nextbar{1} \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[] diff -r fe1ef1f3ee55 -r 3fd2cd187299 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Tue Dec 13 22:44:16 2011 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Tue Dec 13 23:22:27 2011 +0100 @@ -99,7 +99,7 @@ val (_,thy1) = fold_map (fn ak => fn thy => - let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)]) + let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [@{typ nat}], NoSyn)]) val (dt_names, thy1) = Datatype.add_datatype Datatype.default_config [dt] thy; val injects = maps (#inject o Datatype.the_info thy1) dt_names; diff -r fe1ef1f3ee55 -r 3fd2cd187299 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Tue Dec 13 22:44:16 2011 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Tue Dec 13 23:22:27 2011 +0100 @@ -6,9 +6,7 @@ signature NOMINAL_DATATYPE = sig - val add_nominal_datatype : Datatype.config -> - (string list * binding * mixfix * (binding * string list * mixfix) list) list -> - theory -> theory + val add_nominal_datatype : Datatype.config -> Datatype.spec_cmd list -> theory -> theory type descr type nominal_datatype_info val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table @@ -37,18 +35,17 @@ val Collect_False_empty = @{thm empty_def [THEN sym, THEN eq_reflection]}; val empty_iff = @{thm empty_iff}; -open Datatype_Aux; open NominalAtoms; (** FIXME: Datatype should export this function **) local -fun dt_recs (DtTFree _) = [] - | dt_recs (DtType (_, dts)) = maps dt_recs dts - | dt_recs (DtRec i) = [i]; +fun dt_recs (Datatype_Aux.DtTFree _) = [] + | dt_recs (Datatype_Aux.DtType (_, dts)) = maps dt_recs dts + | dt_recs (Datatype_Aux.DtRec i) = [i]; -fun dt_cases (descr: descr) (_, args, constrs) = +fun dt_cases (descr: Datatype_Aux.descr) (_, args, constrs) = let fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i))); val bnames = map the_bname (distinct op = (maps dt_recs args)); @@ -72,7 +69,9 @@ (* theory data *) -type descr = (int * (string * dtyp list * (string * (dtyp list * dtyp) list) list)) list; +type descr = + (int * (string * Datatype_Aux.dtyp list * + (string * (Datatype_Aux.dtyp list * Datatype_Aux.dtyp) list) list)) list; type nominal_datatype_info = {index : int, @@ -186,30 +185,16 @@ fun fresh_star_const T U = Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT); -fun gen_add_nominal_datatype prep_typ config dts thy = +fun gen_add_nominal_datatype prep_specs config dts thy = let - val new_type_names = map (Binding.name_of o #2) dts; - + val new_type_names = map (fn ((tname, _, _), _) => Binding.name_of tname) dts; - (* this theory is used just for parsing *) - - val tmp_thy = thy |> - Theory.copy |> - Sign.add_types_global (map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dts); + val (dts', _) = prep_specs dts thy; val atoms = atoms_of thy; - fun prep_constr (cname, cargs, mx) (constrs, sorts) = - let val (cargs', sorts') = fold_map (prep_typ tmp_thy) cargs sorts - in (constrs @ [(cname, cargs', mx)], sorts') end - - fun prep_dt_spec (tvs, tname, mx, constrs) (dts, sorts) = - let val (constrs', sorts') = fold prep_constr constrs ([], sorts) - in (dts @ [(tvs, tname, mx, constrs')], sorts') end - - val (dts', sorts) = fold prep_dt_spec dts ([], []); - val tyvars = map (map (fn s => - (s, the (AList.lookup (op =) sorts s))) o #1) dts'; + val tyvars = map (fn ((_, tvs, _), _) => tvs) dts'; + val sorts = flat tyvars; fun inter_sort thy S S' = Sign.inter_sort thy (S, S'); fun augment_sort_typ thy S = @@ -219,12 +204,12 @@ end; fun augment_sort thy S = map_types (augment_sort_typ thy S); - val types_syntax = map (fn (tvs, tname, mx, constrs) => (tname, mx)) dts'; - val constr_syntax = map (fn (tvs, tname, mx, constrs) => + val types_syntax = map (fn ((tname, tvs, mx), constrs) => (tname, mx)) dts'; + val constr_syntax = map (fn (_, constrs) => map (fn (cname, cargs, mx) => (cname, mx)) constrs) dts'; - val ps = map (fn (_, n, _, _) => - (Sign.full_name tmp_thy n, Sign.full_name tmp_thy (Binding.suffix_name "_Rep" n))) dts; + val ps = map (fn ((n, _, _), _) => + (Sign.full_name thy n, Sign.full_name thy (Binding.suffix_name "_Rep" n))) dts; val rps = map Library.swap ps; fun replace_types (Type ("Nominal.ABS", [T, U])) = @@ -233,8 +218,8 @@ Type (the_default s (AList.lookup op = ps s), map replace_types Ts) | replace_types T = T; - val dts'' = map (fn (tvs, tname, mx, constrs) => - (tvs, Binding.suffix_name "_Rep" tname, NoSyn, + val dts'' = map (fn ((tname, tvs, mx), constrs) => + ((Binding.suffix_name "_Rep" tname, tvs, NoSyn), map (fn (cname, cargs, mx) => (Binding.suffix_name "_Rep" cname, map replace_types cargs, NoSyn)) constrs)) dts'; @@ -243,7 +228,7 @@ val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy; val {descr, induct, ...} = Datatype.the_info thy1 (hd full_new_type_names'); - fun nth_dtyp i = typ_of_dtyp descr (DtRec i); + fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr (Datatype_Aux.DtRec i); val big_name = space_implode "_" new_type_names; @@ -256,7 +241,7 @@ let val T = nth_dtyp i in permT --> T --> T end) descr; val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => - "perm_" ^ name_of_typ (nth_dtyp i)) descr); + "perm_" ^ Datatype_Aux.name_of_typ (nth_dtyp i)) descr); val perm_names = replicate (length new_type_names) "Nominal.perm" @ map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names)); val perm_names_types = perm_names ~~ perm_types; @@ -266,16 +251,16 @@ let val T = nth_dtyp i in map (fn (cname, dts) => let - val Ts = map (typ_of_dtyp descr) dts; + val Ts = map (Datatype_Aux.typ_of_dtyp descr) dts; val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); val args = map Free (names ~~ Ts); val c = Const (cname, Ts ---> T); fun perm_arg (dt, x) = let val T = type_of x - in if is_rec_type dt then + in if Datatype_Aux.is_rec_type dt then let val Us = binder_types T in list_abs (map (pair "x") Us, - Free (nth perm_names_types' (body_index dt)) $ pi $ + Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $ list_comb (x, map (fn (i, U) => Const ("Nominal.perm", permT --> U --> U) $ (Const ("List.rev", permT --> permT) $ pi) $ @@ -309,7 +294,7 @@ val unfolded_perm_eq_thms = if length descr = length new_type_names then [] - else map Drule.export_without_context (List.drop (split_conj_thm + else map Drule.export_without_context (List.drop (Datatype_Aux.split_conj_thm (Goal.prove_global thy2 [] [] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn (c as (s, T), x) => @@ -329,7 +314,7 @@ val perm_empty_thms = maps (fn a => let val permT = mk_permT (Type (a, [])) - in map Drule.export_without_context (List.take (split_conj_thm + in map Drule.export_without_context (List.take (Datatype_Aux.split_conj_thm (Goal.prove_global thy2 [] [] (augment_sort thy2 [pt_class_of thy2 a] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj @@ -361,7 +346,7 @@ val pt_inst = pt_inst_of thy2 a; val pt2' = pt_inst RS pt2; val pt2_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a); - in List.take (map Drule.export_without_context (split_conj_thm + in List.take (map Drule.export_without_context (Datatype_Aux.split_conj_thm (Goal.prove_global thy2 [] [] (augment_sort thy2 [pt_class_of thy2 a] (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj @@ -396,7 +381,7 @@ val pt3' = pt_inst RS pt3; val pt3_rev' = at_inst RS (pt_inst RS pt3_rev); val pt3_ax = Global_Theory.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a); - in List.take (map Drule.export_without_context (split_conj_thm + in List.take (map Drule.export_without_context (Datatype_Aux.split_conj_thm (Goal.prove_global thy2 [] [] (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies (HOLogic.mk_Trueprop (Const ("Nominal.prm_eq", @@ -447,7 +432,7 @@ at_inst RS (pt_inst RS pt_perm_compose_rev) RS sym] end)) val sort = Sign.minimize_sort thy (Sign.certify_sort thy (cp_class :: pt_class)); - val thms = split_conj_thm (Goal.prove_global thy [] [] + val thms = Datatype_Aux.split_conj_thm (Goal.prove_global thy [] [] (augment_sort thy sort (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn ((s, T), x) => @@ -499,24 +484,26 @@ val _ = warning "representing sets"; - val rep_set_names = Datatype_Prop.indexify_names - (map (fn (i, _) => name_of_typ (nth_dtyp i) ^ "_set") descr); + val rep_set_names = + Datatype_Prop.indexify_names + (map (fn (i, _) => Datatype_Aux.name_of_typ (nth_dtyp i) ^ "_set") descr); val big_rep_name = space_implode "_" (Datatype_Prop.indexify_names (map_filter (fn (i, ("Nominal.noption", _, _)) => NONE - | (i, _) => SOME (name_of_typ (nth_dtyp i))) descr)) ^ "_set"; + | (i, _) => SOME (Datatype_Aux.name_of_typ (nth_dtyp i))) descr)) ^ "_set"; val _ = warning ("big_rep_name: " ^ big_rep_name); - fun strip_option (dtf as DtType ("fun", [dt, DtRec i])) = + fun strip_option (dtf as Datatype_Aux.DtType ("fun", [dt, Datatype_Aux.DtRec i])) = (case AList.lookup op = descr i of SOME ("Nominal.noption", _, [(_, [dt']), _]) => apfst (cons dt) (strip_option dt') | _ => ([], dtf)) - | strip_option (DtType ("fun", [dt, DtType ("Nominal.noption", [dt'])])) = + | strip_option (Datatype_Aux.DtType ("fun", + [dt, Datatype_Aux.DtType ("Nominal.noption", [dt'])])) = apfst (cons dt) (strip_option dt') | strip_option dt = ([], dt); - val dt_atomTs = distinct op = (map (typ_of_dtyp descr) + val dt_atomTs = distinct op = (map (Datatype_Aux.typ_of_dtyp descr) (maps (fn (_, (_, _, cs)) => maps (maps (fst o strip_option) o snd) cs) descr)); val dt_atoms = map (fst o dest_Type) dt_atomTs; @@ -525,20 +512,20 @@ fun mk_prem dt (j, j', prems, ts) = let val (dts, dt') = strip_option dt; - val (dts', dt'') = strip_dtyp dt'; - val Ts = map (typ_of_dtyp descr) dts; - val Us = map (typ_of_dtyp descr) dts'; - val T = typ_of_dtyp descr dt''; - val free = mk_Free "x" (Us ---> T) j; - val free' = app_bnds free (length Us); + val (dts', dt'') = Datatype_Aux.strip_dtyp dt'; + val Ts = map (Datatype_Aux.typ_of_dtyp descr) dts; + val Us = map (Datatype_Aux.typ_of_dtyp descr) dts'; + val T = Datatype_Aux.typ_of_dtyp descr dt''; + val free = Datatype_Aux.mk_Free "x" (Us ---> T) j; + val free' = Datatype_Aux.app_bnds free (length Us); fun mk_abs_fun T (i, t) = let val U = fastype_of t in (i + 1, Const ("Nominal.abs_fun", [T, U, T] ---> - Type ("Nominal.noption", [U])) $ mk_Free "y" T i $ t) + Type ("Nominal.noption", [U])) $ Datatype_Aux.mk_Free "y" T i $ t) end in (j + 1, j' + length Ts, case dt'' of - DtRec k => list_all (map (pair "x") Us, + Datatype_Aux.DtRec k => list_all (map (pair "x") Us, HOLogic.mk_Trueprop (Free (nth rep_set_names k, T --> HOLogic.boolT) $ free')) :: prems | _ => prems, @@ -584,7 +571,7 @@ (perm_indnames ~~ descr); fun mk_perm_closed name = map (fn th => Drule.export_without_context (th RS mp)) - (List.take (split_conj_thm (Goal.prove_global thy4 [] [] + (List.take (Datatype_Aux.split_conj_thm (Goal.prove_global thy4 [] [] (augment_sort thy4 (pt_class_of thy4 name :: map (cp_class_of thy4 name) (remove (op =) name dt_atoms)) (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map @@ -717,8 +704,8 @@ (fn ((i, ("Nominal.noption", _, _)), p) => p | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr; - fun reindex (DtType (s, dts)) = DtType (s, map reindex dts) - | reindex (DtRec i) = DtRec (the (AList.lookup op = ty_idxs i)) + fun reindex (Datatype_Aux.DtType (s, dts)) = Datatype_Aux.DtType (s, map reindex dts) + | reindex (Datatype_Aux.DtRec i) = Datatype_Aux.DtRec (the (AList.lookup op = ty_idxs i)) | reindex dt = dt; fun strip_suffix i s = implode (List.take (raw_explode s, size s - i)); (* FIXME Symbol.explode (?) *) @@ -754,14 +741,14 @@ map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs)) (constrs ~~ idxss)))) (descr'' ~~ ndescr); - fun nth_dtyp' i = typ_of_dtyp descr'' (DtRec i); + fun nth_dtyp' i = Datatype_Aux.typ_of_dtyp descr'' (Datatype_Aux.DtRec i); val rep_names = map (fn s => Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names; val abs_names = map (fn s => Sign.intern_const thy7 ("Abs_" ^ s)) new_type_names; - val recTs = get_rec_types descr''; + val recTs = Datatype_Aux.get_rec_types descr''; val newTs' = take (length new_type_names) recTs'; val newTs = take (length new_type_names) recTs; @@ -772,17 +759,18 @@ let fun constr_arg (dts, dt) (j, l_args, r_args) = let - val xs = map (fn (dt, i) => mk_Free "x" (typ_of_dtyp descr'' dt) i) - (dts ~~ (j upto j + length dts - 1)) - val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts) + val xs = + map (fn (dt, i) => Datatype_Aux.mk_Free "x" (Datatype_Aux.typ_of_dtyp descr'' dt) i) + (dts ~~ (j upto j + length dts - 1)) + val x = Datatype_Aux.mk_Free "x" (Datatype_Aux.typ_of_dtyp descr'' dt) (j + length dts) in (j + length dts + 1, xs @ x :: l_args, fold_rev mk_abs_fun xs (case dt of - DtRec k => if k < length new_type_names then - Const (nth rep_names k, typ_of_dtyp descr'' dt --> - typ_of_dtyp descr dt) $ x + Datatype_Aux.DtRec k => if k < length new_type_names then + Const (nth rep_names k, Datatype_Aux.typ_of_dtyp descr'' dt --> + Datatype_Aux.typ_of_dtyp descr dt) $ x else error "nested recursion not (yet) supported" | _ => x) :: r_args) end @@ -900,10 +888,12 @@ fun constr_arg (dts, dt) (j, l_args, r_args) = let - val Ts = map (typ_of_dtyp descr'') dts; - val xs = map (fn (T, i) => mk_Free "x" T i) - (Ts ~~ (j upto j + length dts - 1)) - val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts) + val Ts = map (Datatype_Aux.typ_of_dtyp descr'') dts; + val xs = + map (fn (T, i) => Datatype_Aux.mk_Free "x" T i) + (Ts ~~ (j upto j + length dts - 1)); + val x = + Datatype_Aux.mk_Free "x" (Datatype_Aux.typ_of_dtyp descr'' dt) (j + length dts); in (j + length dts + 1, xs @ x :: l_args, @@ -950,11 +940,14 @@ fun make_inj (dts, dt) (j, args1, args2, eqs) = let - val Ts_idx = map (typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1); - val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx; - val ys = map (fn (T, i) => mk_Free "y" T i) Ts_idx; - val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts); - val y = mk_Free "y" (typ_of_dtyp descr'' dt) (j + length dts); + val Ts_idx = + map (Datatype_Aux.typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1); + val xs = map (fn (T, i) => Datatype_Aux.mk_Free "x" T i) Ts_idx; + val ys = map (fn (T, i) => Datatype_Aux.mk_Free "y" T i) Ts_idx; + val x = + Datatype_Aux.mk_Free "x" (Datatype_Aux.typ_of_dtyp descr'' dt) (j + length dts); + val y = + Datatype_Aux.mk_Free "y" (Datatype_Aux.typ_of_dtyp descr'' dt) (j + length dts); in (j + length dts + 1, xs @ (x :: args1), ys @ (y :: args2), @@ -993,9 +986,11 @@ fun process_constr (dts, dt) (j, args1, args2) = let - val Ts_idx = map (typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1); - val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx; - val x = mk_Free "x" (typ_of_dtyp descr'' dt) (j + length dts); + val Ts_idx = + map (Datatype_Aux.typ_of_dtyp descr'') dts ~~ (j upto j + length dts - 1); + val xs = map (fn (T, i) => Datatype_Aux.mk_Free "x" T i) Ts_idx; + val x = + Datatype_Aux.mk_Free "x" (Datatype_Aux.typ_of_dtyp descr'' dt) (j + length dts); in (j + length dts + 1, xs @ (x :: args1), fold_rev mk_abs_fun xs x :: args2) @@ -1034,14 +1029,16 @@ fun mk_indrule_lemma (((i, _), T), U) (prems, concls) = let - val Rep_t = Const (nth rep_names i, T --> U) $ mk_Free "x" T i; + val Rep_t = Const (nth rep_names i, T --> U) $ Datatype_Aux.mk_Free "x" T i; val Abs_t = Const (nth abs_names i, U --> T); - in (prems @ [HOLogic.imp $ + in + (prems @ [HOLogic.imp $ (Const (nth rep_set_names'' i, U --> HOLogic.boolT) $ Rep_t) $ - (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))], - concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i]) + (Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))], + concls @ + [Datatype_Aux.mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ Datatype_Aux.mk_Free "x" T i]) end; val (indrule_lemma_prems, indrule_lemma_concls) = @@ -1049,8 +1046,8 @@ val indrule_lemma = Goal.prove_global thy8 [] [] (Logic.mk_implies - (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems), - HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY + (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_prems), + HOLogic.mk_Trueprop (Datatype_Aux.mk_conj indrule_lemma_concls))) (fn _ => EVERY [REPEAT (etac conjE 1), REPEAT (EVERY [TRY (rtac conjI 1), full_simp_tac (HOL_basic_ss addsimps Rep_inverse_thms) 1, @@ -1090,7 +1087,7 @@ val finite_supp_thms = map (fn atom => let val atomT = Type (atom, []) in map Drule.export_without_context (List.take - (split_conj_thm (Goal.prove_global thy8 [] [] + (Datatype_Aux.split_conj_thm (Goal.prove_global thy8 [] [] (augment_sort thy8 (fs_class_of thy8 atom :: pt_cp_sort) (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn (s, T) => @@ -1160,11 +1157,11 @@ fun make_ind_prem fsT f k T ((cname, cargs), idxs) = let - val recs = filter is_rec_type cargs; - val Ts = map (typ_of_dtyp descr'') cargs; - val recTs' = map (typ_of_dtyp descr'') recs; + val recs = filter Datatype_Aux.is_rec_type cargs; + val Ts = map (Datatype_Aux.typ_of_dtyp descr'') cargs; + val recTs' = map (Datatype_Aux.typ_of_dtyp descr'') recs; val tnames = Name.variant_list pnames (Datatype_Prop.make_tnames Ts); - val rec_tnames = map fst (filter (is_rec_type o snd) (tnames ~~ cargs)); + val rec_tnames = map fst (filter (Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs)); val frees = tnames ~~ Ts; val frees' = partition_cargs idxs frees; val z = (singleton (Name.variant_list tnames) "z", fsT); @@ -1172,9 +1169,12 @@ fun mk_prem ((dt, s), T) = let val (Us, U) = strip_type T; - val l = length Us - in list_all (z :: map (pair "x") Us, HOLogic.mk_Trueprop - (make_pred fsT (body_index dt) U $ Bound l $ app_bnds (Free (s, T)) l)) + val l = length Us; + in + list_all (z :: map (pair "x") Us, + HOLogic.mk_Trueprop + (make_pred fsT (Datatype_Aux.body_index dt) U $ Bound l $ + Datatype_Aux.app_bnds (Free (s, T)) l)) end; val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs'); @@ -1432,7 +1432,7 @@ (1 upto (length descr'')); val rec_set_names = map (Sign.full_bname thy10) rec_set_names'; - val rec_fns = map (uncurry (mk_Free "f")) + val rec_fns = map (uncurry (Datatype_Aux.mk_Free "f")) (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts))); val rec_sets' = map (fn c => list_comb (Free c, rec_fns)) (rec_set_names' ~~ rec_set_Ts); @@ -1457,13 +1457,13 @@ fun make_rec_intr T p rec_set ((cname, cargs), idxs) (rec_intr_ts, rec_prems, rec_prems', rec_eq_prems, l) = let - val Ts = map (typ_of_dtyp descr'') cargs; + val Ts = map (Datatype_Aux.typ_of_dtyp descr'') cargs; val frees = map (fn i => "x" ^ string_of_int i) (1 upto length Ts) ~~ Ts; val frees' = partition_cargs idxs frees; val binders = maps fst frees'; val atomTs = distinct op = (maps (map snd o fst) frees'); val recs = map_filter - (fn ((_, DtRec i), p) => SOME (i, p) | _ => NONE) + (fn ((_, Datatype_Aux.DtRec i), p) => SOME (i, p) | _ => NONE) (partition_cargs idxs cargs ~~ frees'); val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~ map (fn (i, _) => nth rec_result_Ts i) recs; @@ -1525,7 +1525,7 @@ let val permT = mk_permT aT; val pi = Free ("pi", permT); - val rec_fns_pi = map (mk_perm [] pi o uncurry (mk_Free "f")) + val rec_fns_pi = map (mk_perm [] pi o uncurry (Datatype_Aux.mk_Free "f")) (rec_fn_Ts ~~ (1 upto (length rec_fn_Ts))); val rec_sets_pi = map (fn c => list_comb (Const c, rec_fns_pi)) (rec_set_names ~~ rec_set_Ts); @@ -1536,7 +1536,7 @@ in (R $ x $ y, R' $ mk_perm [] pi x $ mk_perm [] pi y) end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ rec_sets_pi ~~ (1 upto length recTs)); - val ths = map (fn th => Drule.export_without_context (th RS mp)) (split_conj_thm + val ths = map (fn th => Drule.export_without_context (th RS mp)) (Datatype_Aux.split_conj_thm (Goal.prove_global thy11 [] [] (augment_sort thy1 pt_cp_sort (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps)))) @@ -1568,7 +1568,7 @@ (finite $ (Const ("Nominal.supp", T --> aset) $ f))) (rec_fns ~~ rec_fn_Ts) in - map (fn th => Drule.export_without_context (th RS mp)) (split_conj_thm + map (fn th => Drule.export_without_context (th RS mp)) (Datatype_Aux.split_conj_thm (Goal.prove_global thy11 [] (map (augment_sort thy11 fs_cp_sort) fins) (augment_sort thy11 fs_cp_sort @@ -1705,7 +1705,7 @@ (Const ("Finite_Set.finite", HOLogic.mk_setT aT --> HOLogic.boolT) $ (Const ("Nominal.supp", fsT' --> HOLogic.mk_setT aT) $ rec_ctxt))) dt_atomTs; - val rec_unique_thms = split_conj_thm (Goal.prove + val rec_unique_thms = Datatype_Aux.split_conj_thm (Goal.prove (Proof_Context.init_global thy11) (map fst rec_unique_frees) (map (augment_sort thy11 fs_cp_sort) (flat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems')) @@ -1718,7 +1718,7 @@ apfst (pair T) (chop k xs)) dt_atomTs prems; val (finite_ctxt_ths, ths2) = chop (length dt_atomTs) ths1; val (P_ind_ths, fcbs) = chop k ths2; - val P_ths = map (fn th => th RS mp) (split_conj_thm + val P_ths = map (fn th => th RS mp) (Datatype_Aux.split_conj_thm (Goal.prove context (map fst (rec_unique_frees'' @ rec_unique_frees')) [] (augment_sort thy11 fs_cp_sort @@ -2065,11 +2065,11 @@ thy13 end; -val add_nominal_datatype = gen_add_nominal_datatype Datatype.read_typ; +val add_nominal_datatype = gen_add_nominal_datatype Datatype.read_specs; val _ = Outer_Syntax.command "nominal_datatype" "define inductive datatypes" Keyword.thy_decl - (Parse.and_list1 Datatype.parse_decl + (Parse.and_list1 Datatype.spec_cmd >> (Toplevel.theory o add_nominal_datatype Datatype.default_config)); end diff -r fe1ef1f3ee55 -r 3fd2cd187299 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Tue Dec 13 22:44:16 2011 +0100 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Tue Dec 13 23:22:27 2011 +0100 @@ -306,8 +306,7 @@ in (thy |> Datatype.add_datatype {strict = true, quiet = true} - [([], tyb, NoSyn, - map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |> + [((tyb, [], NoSyn), map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |> add_enum_type s tyname, tyname) end diff -r fe1ef1f3ee55 -r 3fd2cd187299 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Tue Dec 13 22:44:16 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Tue Dec 13 23:22:27 2011 +0100 @@ -10,13 +10,17 @@ signature DATATYPE = sig include DATATYPE_DATA - val add_datatype: config -> - (string list * binding * mixfix * (binding * typ list * mixfix) list) list -> - theory -> string list * theory - val add_datatype_cmd: - (string list * binding * mixfix * (binding * string list * mixfix) list) list -> - theory -> theory - val parse_decl: (string list * binding * mixfix * (binding * string list * mixfix) list) parser + type spec = + (binding * (string * sort) list * mixfix) * + (binding * typ list * mixfix) list + type spec_cmd = + (binding * (string * string option) list * mixfix) * + (binding * string list * mixfix) list + val read_specs: spec_cmd list -> theory -> spec list * Proof.context + val check_specs: spec list -> theory -> spec list * Proof.context + val add_datatype: config -> spec list -> theory -> string list * theory + val add_datatype_cmd: spec_cmd list -> theory -> theory + val spec_cmd: spec_cmd parser end; structure Datatype : DATATYPE = @@ -670,27 +674,74 @@ (** datatype definition **) -fun gen_add_datatype prep_typ config dts thy = +(* specifications *) + +type spec = (binding * (string * sort) list * mixfix) * (binding * typ list * mixfix) list; + +type spec_cmd = + (binding * (string * string option) list * mixfix) * (binding * string list * mixfix) list; + +local + +fun parse_spec ctxt ((b, args, mx), constrs) = + ((b, map (apsnd (Typedecl.read_constraint ctxt)) args, mx), + constrs |> map (fn (c, Ts, mx') => (c, map (Syntax.parse_typ ctxt) Ts, mx'))); + +fun check_specs ctxt (specs: spec list) = + let + fun prep_spec ((tname, args, mx), constrs) tys = + let + val (args', tys1) = chop (length args) tys; + val (constrs', tys3) = (constrs, tys1) |-> fold_map (fn (cname, cargs, mx') => fn tys2 => + let val (cargs', tys3) = chop (length cargs) tys2; + in ((cname, cargs', mx'), tys3) end); + in (((tname, map dest_TFree args', mx), constrs'), tys3) end; + + val all_tys = + specs |> maps (fn ((_, args, _), cs) => map TFree args @ maps #2 cs) + |> Syntax.check_typs ctxt; + + in #1 (fold_map prep_spec specs all_tys) end; + +fun prep_specs parse raw_specs thy = + let + val ctxt = thy + |> Theory.copy + |> Sign.add_types_global (map (fn ((b, args, mx), _) => (b, length args, mx)) raw_specs) + |> Proof_Context.init_global + |> fold (fn ((_, args, _), _) => fold (fn (a, _) => + Variable.declare_typ (TFree (a, dummyS))) args) raw_specs; + val specs = check_specs ctxt (map (parse ctxt) raw_specs); + in (specs, ctxt) end; + +in + +val read_specs = prep_specs parse_spec; +val check_specs = prep_specs (K I); + +end; + + +(* main commands *) + +fun gen_add_datatype prep_specs config raw_specs thy = let val _ = Theory.requires thy "Datatype" "datatype definitions"; - (* this theory is used just for parsing *) - val tmp_thy = thy - |> Theory.copy - |> Sign.add_types_global (map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dts); - val tmp_ctxt = Proof_Context.init_global tmp_thy; + val (dts, spec_ctxt) = prep_specs raw_specs thy; + val ((_, tyvars, _), _) :: _ = dts; + val string_of_tyvar = Syntax.string_of_typ spec_ctxt o TFree; - val (tyvars, _, _, _) ::_ = dts; - val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) => - let val full_tname = Sign.full_name tmp_thy tname in + val (new_dts, types_syntax) = dts |> map (fn ((tname, tvs, mx), _) => + let val full_tname = Sign.full_name thy tname in (case duplicates (op =) tvs of [] => if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx)) - else error ("Mutually recursive datatypes must have same type parameters") + else error "Mutually recursive datatypes must have same type parameters" | dups => error ("Duplicate parameter(s) for datatype " ^ Binding.print tname ^ - " : " ^ commas dups)) - end) dts); + " : " ^ commas (map string_of_tyvar dups))) + end) |> split_list; val dt_names = map fst new_dts; val _ = @@ -698,45 +749,37 @@ [] => () | dups => error ("Duplicate datatypes: " ^ commas_quote dups)); - fun prep_dt_spec (tvs, tname, mx, constrs) (dts', constr_syntax, sorts, i) = + fun prep_dt_spec ((tname, tvs, mx), constrs) (dts', constr_syntax, i) = let - fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') = + fun prep_constr (cname, cargs, mx') (constrs, constr_syntax') = let - val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts'; val _ = - (case subtract (op =) tvs (fold Term.add_tfree_namesT cargs' []) of + (case subtract (op =) tvs (fold Term.add_tfreesT cargs []) of [] => () - | vs => error ("Extra type variables on rhs: " ^ commas vs)); - val c = Sign.full_name_path tmp_thy (Binding.name_of tname) cname; + | vs => error ("Extra type variables on rhs: " ^ commas (map string_of_tyvar vs))); + val c = Sign.full_name_path thy (Binding.name_of tname) cname; in - (constrs @ [(c, map (Datatype_Aux.dtyp_of_typ new_dts) cargs')], - constr_syntax' @ [(cname, mx')], sorts'') + (constrs @ [(c, map (Datatype_Aux.dtyp_of_typ new_dts) cargs)], + constr_syntax' @ [(cname, mx')]) end handle ERROR msg => cat_error msg ("The error above occurred in constructor " ^ Binding.print cname ^ " of datatype " ^ Binding.print tname); - val (constrs', constr_syntax', sorts') = fold prep_constr constrs ([], [], sorts); + val (constrs', constr_syntax') = fold prep_constr constrs ([], []); in (case duplicates (op =) (map fst constrs') of [] => - (dts' @ [(i, (Sign.full_name tmp_thy tname, tvs, constrs'))], - constr_syntax @ [constr_syntax'], sorts', i + 1) + (dts' @ [(i, (Sign.full_name thy tname, map Datatype_Aux.DtTFree tvs, constrs'))], + constr_syntax @ [constr_syntax'], i + 1) | dups => error ("Duplicate constructors " ^ commas_quote dups ^ " in datatype " ^ Binding.print tname)) end; - val (dts0, constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0); - val tmp_ctxt' = tmp_ctxt |> fold (Variable.declare_typ o TFree) sorts'; - - val dts' = dts0 |> map (fn (i, (name, tvs, cs)) => - let - val args = tvs |> - map (fn a => Datatype_Aux.DtTFree (a, Proof_Context.default_sort tmp_ctxt' (a, ~1))); - in (i, (name, args, cs)) end); + val (dts', constr_syntax, i) = fold prep_dt_spec dts ([], [], 0); val dt_info = Datatype_Data.get_all thy; - val (descr, _) = Datatype_Aux.unfold_datatypes tmp_ctxt dts' dt_info dts' i; + val (descr, _) = Datatype_Aux.unfold_datatypes spec_ctxt dts' dt_info dts' i; val _ = Datatype_Aux.check_nonempty descr handle (exn as Datatype_Aux.Datatype_Empty s) => @@ -745,7 +788,7 @@ val _ = Datatype_Aux.message config - ("Constructing datatype(s) " ^ commas_quote (map (Binding.name_of o #2) dts)); + ("Constructing datatype(s) " ^ commas_quote (map (Binding.name_of o #1 o #1) dts)); in thy |> representation_proofs config dt_info descr types_syntax constr_syntax @@ -754,20 +797,20 @@ Datatype_Data.derive_datatype_props config dt_names descr induct inject distinct) end; -val add_datatype = gen_add_datatype Datatype_Data.cert_typ; -val add_datatype_cmd = snd oo gen_add_datatype Datatype_Data.read_typ Datatype_Aux.default_config; +val add_datatype = gen_add_datatype check_specs; +val add_datatype_cmd = snd oo gen_add_datatype read_specs Datatype_Aux.default_config; -(* concrete syntax *) +(* outer syntax *) -val parse_decl = - Parse.type_args -- Parse.binding -- Parse.opt_mixfix -- +val spec_cmd = + Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix)) - >> (fn (((vs, t), mx), cons) => (vs, t, mx, map Parse.triple1 cons)); + >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons)); val _ = Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl - (Parse.and_list1 parse_decl >> (Toplevel.theory o add_datatype_cmd)); + (Parse.and_list1 spec_cmd >> (Toplevel.theory o add_datatype_cmd)); open Datatype_Data; diff -r fe1ef1f3ee55 -r 3fd2cd187299 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Tue Dec 13 22:44:16 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Tue Dec 13 23:22:27 2011 +0100 @@ -57,7 +57,7 @@ exception Datatype exception Datatype_Empty of string val name_of_typ : typ -> string - val dtyp_of_typ : (string * string list) list -> typ -> dtyp + val dtyp_of_typ : (string * (string * sort) list) list -> typ -> dtyp val mk_Free : string -> typ -> int -> term val is_rec_type : dtyp -> bool val typ_of_dtyp : descr -> dtyp -> typ @@ -242,7 +242,7 @@ (case AList.lookup (op =) new_dts tname of NONE => DtType (tname, map (dtyp_of_typ new_dts) Ts) | SOME vs => - if map (try (fst o dest_TFree)) Ts = map SOME vs then + if map (try dest_TFree) Ts = map SOME vs then DtRec (find_index (curry op = tname o fst) new_dts) else error ("Illegal occurrence of recursive type " ^ quote tname)); diff -r fe1ef1f3ee55 -r 3fd2cd187299 src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Tue Dec 13 22:44:16 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Tue Dec 13 23:22:27 2011 +0100 @@ -28,8 +28,6 @@ val make_case : Proof.context -> Datatype_Case.config -> string list -> term -> (term * term) list -> term val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option - val read_typ: theory -> string -> (string * sort) list -> typ * (string * sort) list - val cert_typ: theory -> typ -> (string * sort) list -> typ * (string * sort) list val mk_case_names_induct: descr -> attribute val setup: theory -> theory end; @@ -171,27 +169,6 @@ (** various auxiliary **) -(* prepare datatype specifications *) - -fun read_typ thy str sorts = - let - val ctxt = Proof_Context.init_global thy - |> fold (Variable.declare_typ o TFree) sorts; - val T = Syntax.read_typ ctxt str; - in (T, Term.add_tfreesT T sorts) end; - -fun cert_typ sign raw_T sorts = - let - val T = Type.no_tvars (Sign.certify_typ sign raw_T) - handle TYPE (msg, _, _) => error msg; - val sorts' = Term.add_tfreesT T sorts; - val _ = - (case duplicates (op =) (map fst sorts') of - [] => () - | dups => error ("Inconsistent sort constraints for " ^ commas dups)); - in (T, sorts') end; - - (* case names *) local @@ -427,8 +404,7 @@ (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T); val cs = map (apsnd (map norm_constr)) raw_cs; - val dtyps_of_typ = - map (Datatype_Aux.dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) o binder_types; + val dtyps_of_typ = map (Datatype_Aux.dtyp_of_typ (map (rpair vs o fst) cs)) o binder_types; val dt_names = map fst cs; fun mk_spec (i, (tyco, constr)) = diff -r fe1ef1f3ee55 -r 3fd2cd187299 src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Tue Dec 13 22:44:16 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Tue Dec 13 23:22:27 2011 +0100 @@ -277,6 +277,7 @@ val quotspec_parser = Parse.and_list1 ((Parse.type_args -- Parse.binding) -- + (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *) Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) -- (Parse.$$$ "/" |-- (partial -- Parse.term)) -- Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))) diff -r fe1ef1f3ee55 -r 3fd2cd187299 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Tue Dec 13 22:44:16 2011 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Dec 13 23:22:27 2011 +0100 @@ -69,8 +69,9 @@ filter_out (equal Extraction.nullT) (map (Logic.unvarifyT_global o Extraction.etype_of thy vs []) (prems_of intr)), NoSyn); - in (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs, tname, NoSyn, - map constr_of_intr intrs) + in + ((tname, map (rpair dummyS) (map (fn a => "'" ^ a) vs @ map (fst o fst) iTs), NoSyn), + map constr_of_intr intrs) end; fun mk_rlz T = Const ("realizes", [T, HOLogic.boolT] ---> HOLogic.boolT); @@ -233,8 +234,9 @@ end) concls rec_names) end; -fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) = - if Binding.eq_name (name, s) then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs)) +fun add_dummy name dname (x as (_, ((s, vs, mx), cs))) = + if Binding.eq_name (name, s) + then (true, ((s, vs, mx), (dname, [HOLogic.unitT], NoSyn) :: cs)) else x; fun add_dummies f [] _ thy = diff -r fe1ef1f3ee55 -r 3fd2cd187299 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Tue Dec 13 22:44:16 2011 +0100 +++ b/src/HOL/Tools/record.ML Tue Dec 13 23:22:27 2011 +0100 @@ -49,8 +49,6 @@ val updateN: string val ext_typeN: string val extN: string - val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list - val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list val setup: theory -> theory end; @@ -1489,24 +1487,6 @@ (** theory extender interface **) -(* prepare arguments *) - -fun read_typ ctxt raw_T env = - let - val ctxt' = fold (Variable.declare_typ o TFree) env ctxt; - val T = Syntax.read_typ ctxt' raw_T; - val env' = Term.add_tfreesT T env; - in (T, env') end; - -fun cert_typ ctxt raw_T env = - let - val thy = Proof_Context.theory_of ctxt; - val T = Type.no_tvars (Sign.certify_typ thy raw_T) - handle TYPE (msg, _, _) => error msg; - val env' = Term.add_tfreesT T env; - in (T, env') end; - - (* attributes *) fun case_names_fields x = Rule_Cases.case_names ["fields"] x; diff -r fe1ef1f3ee55 -r 3fd2cd187299 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Dec 13 22:44:16 2011 +0100 +++ b/src/Pure/Isar/isar_syn.ML Tue Dec 13 23:22:27 2011 +0100 @@ -113,13 +113,11 @@ (Parse.type_args -- Parse.binding -- Parse.opt_mixfix >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd)); -val type_abbrev = - Parse.type_args -- Parse.binding -- - (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')); - val _ = Outer_Syntax.local_theory "type_synonym" "declare type abbreviation" Keyword.thy_decl - (type_abbrev >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)); + (Parse.type_args -- Parse.binding -- + (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')) + >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)); val _ = Outer_Syntax.command "nonterminal"