# HG changeset patch # User haftmann # Date 1147177120 -7200 # Node ID 07eeb832f28dd2ee7d2e0e084cc263138d084b8f # Parent 01e23aa70d3af5099e7a27e492642b75bebaf3e0 introduced characters for code generator; some improved code lemmas for some list functions diff -r 01e23aa70d3a -r 07eeb832f28d src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue May 09 11:00:32 2006 +0200 +++ b/src/HOL/HOL.thy Tue May 09 14:18:40 2006 +0200 @@ -1410,8 +1410,5 @@ "op =" (* an intermediate solution for polymorphic equality *) ml (infixl 6 "=") haskell (infixl 4 "==") - arbitrary - ml ("raise/ (Fail/ \"non-defined-result\")") - haskell ("error/ \"non-defined result\"") end diff -r 01e23aa70d3a -r 07eeb832f28d src/HOL/List.thy --- a/src/HOL/List.thy Tue May 09 11:00:32 2006 +0200 +++ b/src/HOL/List.thy Tue May 09 14:18:40 2006 +0200 @@ -265,6 +265,12 @@ by (rule measure_induct [of length]) iprover +subsubsection {* @{text null} *} + +lemma null_empty: "null xs = (xs = [])" + by (cases xs) simp_all + + subsubsection {* @{text length} *} text {* @@ -1080,6 +1086,18 @@ lemma last_conv_nth: "xs\[] \ last xs = xs!(length xs - 1)" by(induct xs)(auto simp:neq_Nil_conv) +lemma last_code [code]: + "last (x # xs) = (if null xs then x else last xs)" +by (cases xs) simp_all + +declare last.simps [code del] + +lemma butlast_code [code]: + "butlast [] = []" + "butlast (x # xs) = (if null xs then [] else x # butlast xs)" +by (simp, cases xs) simp_all + +declare butlast.simps [code del] subsubsection {* @{text take} and @{text drop} *} @@ -1441,17 +1459,23 @@ lemma list_all2_lengthD [intro?]: "list_all2 P xs ys ==> length xs = length ys" -by (simp add: list_all2_def) - -lemma list_all2_Nil [iff,code]: "list_all2 P [] ys = (ys = [])" -by (simp add: list_all2_def) - -lemma list_all2_Nil2[iff]: "list_all2 P xs [] = (xs = [])" -by (simp add: list_all2_def) - -lemma list_all2_Cons [iff,code]: -"list_all2 P (x # xs) (y # ys) = (P x y \ list_all2 P xs ys)" -by (auto simp add: list_all2_def) + by (simp add: list_all2_def) + +lemma list_all2_Nil [iff]: "list_all2 P [] ys = (ys = [])" + by (simp add: list_all2_def) + +lemma list_all2_Nil2 [iff]: "list_all2 P xs [] = (xs = [])" + by (simp add: list_all2_def) + +lemma list_all2_Nil_code [code]: "list_all2 P [] ys = null ys" + unfolding null_empty by simp + +lemma list_all2_Nil2_code [code]: "list_all2 P xs [] = null xs" + unfolding null_empty by simp + +lemma list_all2_Cons [iff, code]: + "list_all2 P (x # xs) (y # ys) = (P x y \ list_all2 P xs ys)" + by (auto simp add: list_all2_def) lemma list_all2_Cons1: "list_all2 P (x # xs) ys = (\z zs. ys = z # zs \ P x z \ list_all2 P xs zs)" @@ -2174,15 +2198,15 @@ subsubsection {* @{const splice} *} -lemma splice_Nil2[simp]: +lemma splice_Nil2 [simp, code]: "splice xs [] = xs" by (cases xs) simp_all -lemma splice_Cons_Cons[simp]: +lemma splice_Cons_Cons [simp, code]: "splice (x#xs) (y#ys) = x # y # splice xs ys" by simp -declare splice.simps(2)[simp del] +declare splice.simps(2) [simp del, code del] subsubsection{*Sets of Lists*} @@ -2666,24 +2690,35 @@ (gr, HOLogic.dest_list t) in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE; -fun dest_nibble (Const (s, _)) = int_of_nibble (unprefix "List.nibble.Nibble" s) - | dest_nibble _ = raise Match; - -fun char_codegen thy defs gr dep thyname b (Const ("List.char.Char", _) $ c1 $ c2) = - (let val c = chr (dest_nibble c1 * 16 + dest_nibble c2) - in if Symbol.is_printable c then SOME (gr, Pretty.quote (Pretty.str c)) - else NONE - end handle Fail _ => NONE | Match => NONE) - | char_codegen thy defs gr dep thyname b _ = NONE; +fun dest_char (Const ("List.char.Char", _) $ c1 $ c2) = + let + fun dest_nibble (Const (s, _)) = (int_of_nibble o unprefix "List.nibble.Nibble") s + | dest_nibble _ = raise Match; + in + (SOME (dest_nibble c1 * 16 + dest_nibble c2) + handle Fail _ => NONE | Match => NONE) + end + | dest_char _ = NONE; + +fun char_codegen thy defs gr dep thyname b t = + case (Option.map chr o dest_char) t + of SOME c => + if Symbol.is_printable c + then SOME (gr, (Pretty.quote o Pretty.str) c) + else NONE + | NONE => NONE; in val list_codegen_setup = - Codegen.add_codegen "list_codegen" list_codegen #> - Codegen.add_codegen "char_codegen" char_codegen #> - fold (CodegenPackage.add_pretty_list "Nil" "Cons") [ - ("ml", (7, "::")), - ("haskell", (5, ":"))]; + Codegen.add_codegen "list_codegen" list_codegen + #> Codegen.add_codegen "char_codegen" char_codegen + #> fold (CodegenPackage.add_pretty_list "Nil" "Cons") [ + ("ml", (7, "::")), + ("haskell", (5, ":")) + ] + #> CodegenPackage.add_appconst + ("List.char.Char", ((2, 2), CodegenPackage.appgen_char dest_char)); end; *} @@ -2729,6 +2764,11 @@ ml (target_atom "[]") haskell (target_atom "[]") +code_syntax_tyco + char + ml (target_atom "char") + haskell (target_atom "Char") + setup list_codegen_setup setup CodegenPackage.rename_inconsistent diff -r 01e23aa70d3a -r 07eeb832f28d src/HOL/Main.thy --- a/src/HOL/Main.thy Tue May 09 11:00:32 2006 +0200 +++ b/src/HOL/Main.thy Tue May 09 14:18:40 2006 +0200 @@ -11,8 +11,6 @@ text {* Theory @{text Main} includes everything. Note that theory @{text PreList} already includes most HOL theories. -*} - text {* \medskip Late clause setup: installs \emph{all} simprules and claset rules into the clause cache; cf.\ theory @{text diff -r 01e23aa70d3a -r 07eeb832f28d src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Tue May 09 11:00:32 2006 +0200 +++ b/src/Pure/Tools/codegen_package.ML Tue May 09 14:18:40 2006 +0200 @@ -47,6 +47,7 @@ val appgen_split: (int -> term -> term list * term) -> appgen; val appgen_number_of: (theory -> term -> IntInf.int) -> appgen; + val appgen_char: (term -> int option) -> appgen; val appgen_wfrec: appgen; val add_case_const: string -> (string * int) list -> theory -> theory; @@ -827,9 +828,20 @@ in trns |> exprgen_type thy tabs ty - |-> (fn ty => pair (CodegenThingol.INum ((i, ty), ()))) + |-> (fn _ => pair (CodegenThingol.INum (i, ()))) end; +fun appgen_char char_to_index thy tabs (app as ((_, ty), _)) trns = + case (char_to_index o list_comb o apfst Const) app + of SOME i => + trns + |> exprgen_type thy tabs ty + ||>> appgen_default thy tabs app + |-> (fn (_, e0) => pair (IChar (chr i, e0))) + | NONE => + trns + |> appgen_default thy tabs app; + fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns = let val ty_def = (op ---> o apfst tl o strip_type o Type.unvarifyT o Sign.the_const_type thy) c; diff -r 01e23aa70d3a -r 07eeb832f28d src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Tue May 09 11:00:32 2006 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Tue May 09 14:18:40 2006 +0200 @@ -86,20 +86,14 @@ fun brackify_infix infx fxy_ctxt ps = gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps); -fun from_app mk_app from_expr const_syntax fxy ((c, ty), es) = - let - fun mk NONE es = - brackify fxy (mk_app c es) - | mk (SOME ((i, k), pr)) es = - (*if i <= length es then*) - let - val (es1, es2) = chop k es; - in - brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2) - end - (*else - error ("illegal const_syntax")*) - in mk (const_syntax c) es end; +fun from_app mk_app from_expr const_syntax fxy (const as (c, _), es) = + case (const_syntax c) + of NONE => brackify fxy (mk_app c es) + | SOME ((i, k), pr) => + if i <= length es + then case chop k es of (es1, es2) => + brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2) + else from_expr fxy (CodegenThingol.eta_expand (const, es) i); fun fillin_mixfix fxy_this ms fxy_ctxt pr args = let @@ -218,7 +212,7 @@ | (p, ss) => error ("Malformed definition: " ^ quote s ^ " - " ^ commas ss); -(* abstract serializer *) +(* generic abstract serializer *) type serializer = string list list @@ -231,7 +225,7 @@ * OuterParse.token list; fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc) - postprocess preprocess (class_syntax, tyco_syntax, const_syntax) + postprocess (class_syntax, tyco_syntax, const_syntax) select module = let fun pretty_of_prim resolv (name, primdef) = @@ -251,8 +245,6 @@ module |> debug_msg (fn _ => "selecting submodule...") |> (if is_some select then (CodegenThingol.project_module o the) select else I) - |> debug_msg (fn _ => "preprocessing...") - |> preprocess |> debug_msg (fn _ => "serializing...") |> CodegenThingol.serialize (from_defs (pretty_of_prim, (class_syntax : string -> string option, tyco_syntax, const_syntax))) from_module' validator postproc nspgrp name_root @@ -371,7 +363,7 @@ (CodegenTheorems.proper_name o NameSpace.base) name | mk reserved_ml (name, i) = (CodegenTheorems.proper_name o NameSpace.base) name ^ replicate_string i "'"; - fun is_valid reserved_ml = not o member (op = : string * string -> bool) reserved_ml; + fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml; fun maybe_unique _ _ = NONE; fun re_mangle _ dst = error ("no such definition name: " ^ quote dst); ); @@ -499,12 +491,18 @@ str "=>", ml_from_expr NOBR e ] - | ml_from_expr fxy (INum ((n, ty), _)) = + | ml_from_expr fxy (INum (n, _)) = brackify BR [ (str o IntInf.toString) n, - str ":", - ml_from_type NOBR ty + str ":IntInf.int" ] + | ml_from_expr _ (IChar (c, _)) = + (str o prefix "#" o quote) + (let val i = (Char.ord o the o Char.fromString) c + in if i < 32 + then prefix "\\" c + else c + end) | ml_from_expr fxy (IAbs (((ve, vty), be), _)) = brackify BR [ str "fn", @@ -552,10 +550,10 @@ [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)] else (str o resolv) f :: map (ml_from_expr BR) es - and ml_from_app fxy ((c, (lss, ty)), es) = + and ml_from_app fxy (app_expr as ((c, (lss, ty)), es)) = case map (ml_from_sortlookup BR) lss of [] => - from_app ml_mk_app ml_from_expr const_syntax fxy ((c, ty), es) + from_app ml_mk_app ml_from_expr const_syntax fxy app_expr | lss => brackify fxy ( (str o resolv) c @@ -574,6 +572,24 @@ in Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])]) end; + fun eta_expand_poly_fun (funn as (_, (_::_, _))) = + funn + | eta_expand_poly_fun (funn as (eqs, sctxt_ty as (_, ty))) = + let + fun no_eta (_::_, _) = I + | no_eta (_, _ `|-> _) = I + | no_eta (_, IAbs (_, _)) = I + | no_eta ([], e) = K false; + fun has_tyvars (_ `%% tys) = + exists has_tyvars tys + | has_tyvars (ITyVar _) = + true + | has_tyvars (ty1 `-> ty2) = + has_tyvars ty1 orelse has_tyvars ty2; + in if (not o has_tyvars) ty orelse fold no_eta eqs true + then funn + else (map (fn ([], rhs) => ([IVar "x"], rhs `$ IVar "x")) eqs, sctxt_ty) + end; fun ml_from_funs (defs as def::defs_tl) = let fun mk_definer [] [] = "val" @@ -608,10 +624,11 @@ :: map (mk_eq "|") eq_tl ) end; + val def' :: defs' = map (apsnd eta_expand_poly_fun o constructive_fun) defs in chunk_defs ( - (mk_fun (the (fold check_args defs NONE)) o constructive_fun) def - :: map (mk_fun "and" o constructive_fun) defs_tl + (mk_fun (the (fold check_args defs NONE))) def' + :: map (mk_fun "and") defs' ) end; fun ml_from_datatypes (defs as (def::defs_tl)) = @@ -818,14 +835,6 @@ let val l = AList.lookup (op =) cs s |> the |> length in if l >= 2 then l else 0 end else 0; - fun preprocess const_syntax module = - module - |> debug_msg (fn _ => "eta-expanding...") - |> CodegenThingol.eta_expand (eta_expander module const_syntax) - |> debug_msg (fn _ => "eta-expanding polydefs...") - |> CodegenThingol.eta_expand_poly - (*|> debug 3 (fn _ => "unclashing expression/type variables...") - |> CodegenThingol.unclash_vars_tvars*); val parse_multi = OuterParse.name #-> (fn "dir" => @@ -838,7 +847,7 @@ || parse_internal serializer || parse_single_file serializer) >> (fn seri => fn (class_syntax, tyco_syntax, const_syntax) => seri - (preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax)) + (class_syntax, tyco_syntax, const_syntax)) end; fun mk_flat_ml_resolver names = @@ -926,13 +935,15 @@ hs_from_expr NOBR e ]) end - | hs_from_expr fxy (INum ((n, ty), _)) = - brackify BR [ - (str o (fn s => if nth_string s 0 = "~" - then enclose "(" ")" ("negate " ^ unprefix "~" s) else s) o IntInf.toString) n, - str "::", - hs_from_type NOBR ty - ] + | hs_from_expr fxy (INum (n, _)) = + (str o IntInf.toString) n + | hs_from_expr fxy (IChar (c, _)) = + (str o enclose "'" "'") + (let val i = (Char.ord o the o Char.fromString) c + in if i < 32 + then Library.prefix "\\" c + else c + end) | hs_from_expr fxy (e as IAbs _) = let val (es, e) = CodegenThingol.unfold_abs e @@ -975,8 +986,8 @@ ] end and hs_mk_app c es = (str o resolv) c :: map (hs_from_expr BR) es - and hs_from_app fxy ((c, (ty, ls)), es) = - from_app hs_mk_app hs_from_expr const_syntax fxy ((c, ty), es); + and hs_from_app fxy = + from_app hs_mk_app hs_from_expr const_syntax fxy fun hs_from_funeqs (def as (name, _)) = let fun from_eq (args, rhs) = @@ -1101,15 +1112,11 @@ const_syntax c |> Option.map (fst o fst) |> the_default 0; - fun preprocess const_syntax module = - module - |> debug_msg (fn _ => "eta-expanding...") - |> CodegenThingol.eta_expand (eta_expander const_syntax) in (Scan.optional (OuterParse.name >> (fn "no_typs" => false | s => Scan.fail_with (fn _ => "illegal flag: " ^ quote s) true)) true #-> (fn with_typs => parse_multi_file ((K o K) NONE) "hs" (serializer with_typs))) >> (fn (seri) => fn (class_syntax, tyco_syntax, const_syntax) => seri - (preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax)) + (class_syntax, tyco_syntax, const_syntax)) end; end; (* local *) diff -r 01e23aa70d3a -r 07eeb832f28d src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue May 09 11:00:32 2006 +0200 +++ b/src/Pure/Tools/codegen_thingol.ML Tue May 09 14:18:40 2006 +0200 @@ -28,7 +28,8 @@ | IVar of vname | `$ of iexpr * iexpr | `|-> of (vname * itype) * iexpr - | INum of (IntInf.int (*positive!*) * itype) * unit + | INum of IntInf.int (*positive!*) * unit + | IChar of string (*length one!*) * iexpr | IAbs of ((iexpr * itype) * iexpr) * iexpr (* (((binding expression (ve), binding type (vty)), body expression (be)), native expression (e0)) *) @@ -58,6 +59,10 @@ val add_varnames: iexpr -> string list -> string list; val is_pat: iexpr -> bool; val map_pure: (iexpr -> 'a) -> iexpr -> 'a; + val resolve_tycos: (string -> string) -> itype * iexpr list -> itype * iexpr list; + val resolve_consts: (string -> string) -> iexpr -> iexpr; + val eta_expand: (string * (iclasslookup list list * itype)) * iexpr list -> int -> iexpr; + type funn = (iexpr list * iexpr) list * (sortcontext * itype); type datatyp = sortcontext * (string * itype list) list; @@ -98,10 +103,6 @@ -> string -> transact -> transact; val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module; - val eta_expand: (string -> int) -> module -> module; - val eta_expand_poly: module -> module; - val unclash_vars_tvars: module -> module; - val debug: bool ref; val debug_msg: ('a -> string) -> 'a -> 'a; val soft_exc: bool ref; @@ -171,7 +172,8 @@ | IVar of vname | `$ of iexpr * iexpr | `|-> of (vname * itype) * iexpr - | INum of (IntInf.int (*positive!*) * itype) * unit + | INum of IntInf.int (*positive!*) * unit + | IChar of string (*length one!*) * iexpr | IAbs of ((iexpr * itype) * iexpr) * iexpr | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr; (*see also signature*) @@ -225,8 +227,10 @@ | pretty_iexpr ((v, ty) `|-> e) = (Pretty.enclose "(" ")" o Pretty.breaks) [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iexpr e] - | pretty_iexpr (INum ((n, _), _)) = + | pretty_iexpr (INum (n, _)) = (Pretty.str o IntInf.toString) n + | pretty_iexpr (IChar (c, _)) = + (Pretty.str o quote) c | pretty_iexpr (IAbs (((e1, _), e2), _)) = (Pretty.enclose "(" ")" o Pretty.breaks) [pretty_iexpr e1, Pretty.str "|->", pretty_iexpr e2] @@ -272,32 +276,6 @@ | map_itype f (t1 `-> t2) = f t1 `-> f t2; -fun map_iexpr _ (e as IConst _) = - e - | map_iexpr _ (e as IVar _) = - e - | map_iexpr f (e1 `$ e2) = - f e1 `$ f e2 - | map_iexpr f ((v, ty) `|-> e) = - (v, ty) `|-> f e - | map_iexpr _ (e as INum _) = - e - | map_iexpr f (IAbs (((ve, vty), be), e0)) = - IAbs (((f ve, vty), f be), e0) - | map_iexpr f (ICase (((de, dty), bses), e0)) = - ICase (((f de, dty), map (fn (se, be) => (f se, f be)) bses), e0); - -fun map_iexpr_itype f = - let - fun mapp ((v, ty) `|-> e) = (v, f ty) `|-> mapp e - | mapp (INum ((n, ty), e)) = INum ((n, f ty), e) - | mapp (IAbs (((ve, vty), be), e0)) = - IAbs (((mapp ve, f vty), mapp be), e0) - | mapp (ICase (((de, dty), bses), e0)) = - ICase (((mapp de, f dty), map (fn (se, be) => (mapp se, mapp be)) bses), e0) - | mapp e = map_iexpr mapp e; - in mapp end; - fun eq_ityp ((sctxt1, ty1), (sctxt2, ty2)) = let exception NO_MATCH; @@ -337,6 +315,7 @@ | is_pat (e as (e1 `$ e2)) = is_pat e1 andalso is_pat e2 | is_pat (e as INum _) = true + | is_pat (e as IChar _) = true | is_pat e = false; fun map_pure f (e as IConst _) = @@ -349,17 +328,15 @@ f e | map_pure _ (INum _) = error ("sorry, no pure representation of numerals so far") + | map_pure f (IChar (_, e0)) = + f e0 | map_pure f (IAbs (_, e0)) = f e0 | map_pure f (ICase (_, e0)) = f e0; -fun has_tyvars (_ `%% tys) = - exists has_tyvars tys - | has_tyvars (ITyVar _) = - true - | has_tyvars (ty1 `-> ty2) = - has_tyvars ty1 orelse has_tyvars ty2; +fun resolve_tycos _ = error ""; +fun resolve_consts _ = error ""; fun add_constnames (IConst (c, _)) = insert (op =) c @@ -371,6 +348,8 @@ add_constnames e | add_constnames (INum _) = I + | add_constnames (IChar _) = + I | add_constnames (IAbs (_, e)) = add_constnames e | add_constnames (ICase (_, e)) = @@ -386,6 +365,8 @@ insert (op =) v #> add_varnames e | add_varnames (INum _) = I + | add_varnames (IChar _) = + I | add_varnames (IAbs (((ve, _), be), _)) = add_varnames ve #> add_varnames be | add_varnames (ICase (((de, _), bses), _)) = @@ -396,6 +377,14 @@ val x = Term.variant used seed in (x, x :: used) end; +fun eta_expand (c as (_, (_, ty)), es) k = + let + val j = length es; + val l = k - j; + val tys = (curry Library.take l o curry Library.drop j o fst o unfold_fun) ty; + val vs = [] |> fold add_varnames es |> fold_map invent (replicate l "x") |> fst; + in vs ~~ tys `|--> IConst c `$$ es @ map IVar vs end; + (** language module system - definitions, modules, transactions **) @@ -958,69 +947,6 @@ -(** generic transformation **) - -fun map_def_fun f (Fun funn) = - Fun (f funn) - | map_def_fun _ def = def; - -fun map_def_fun_expr f (eqs, cty) = - (map (fn (ps, rhs) => (map f ps, f rhs)) eqs, cty); - -fun eta_expand query = - let - fun eta e = - case unfold_const_app e - of SOME (const as (c, (_, ty)), es) => - let - val delta = query c - length es; - val add_n = if delta < 0 then 0 else delta; - val tys = - (fst o unfold_fun) ty - |> curry Library.drop (length es) - |> curry Library.take add_n - val vs = (Term.invent_names (fold add_varnames es []) "x" add_n) - in - vs ~~ tys `|--> IConst const `$$ map eta es `$$ map IVar vs - end - | NONE => map_iexpr eta e; - in (map_defs o map_def_fun o map_def_fun_expr) eta end; - -val eta_expand_poly = - let - fun eta (funn as ([([], e)], cty as (sctxt, (ty as (ty1 `-> ty2))))) = - if (not o null) sctxt - orelse (not o has_tyvars) ty - then funn - else (case unfold_abs e - of ([], e) => - let - val add_var = IVar (hd (Term.invent_names (add_varnames e []) "x" 1)) - in (([([add_var], e `$ add_var)], cty)) end - | _ => funn) - | eta funn = funn; - in (map_defs o map_def_fun) eta end; - -val unclash_vars_tvars = - let - fun unclash (eqs, (sortctxt, ty)) = - let - val used_expr = - fold (fn (pats, rhs) => fold add_varnames pats #> add_varnames rhs) eqs []; - val used_type = map fst sortctxt; - val clash = gen_union (op =) (used_expr, used_type); - val rename_map = fold_map (fn c => invent c #-> (fn c' => pair (c, c'))) clash [] |> fst; - val rename = - perhaps (AList.lookup (op =) rename_map); - val rename_typ = instant_itype (ITyVar o rename); - val rename_expr = map_iexpr_itype rename_typ; - fun rename_eq (args, rhs) = (map rename_expr args, rename_expr rhs) - in - (map rename_eq eqs, (map (apfst rename) sortctxt, rename_typ ty)) - end; - in (map_defs o map_def_fun) unclash end; - - (** generic serialization **) (* resolving *)