--- a/src/Pure/Tools/codegen_thingol.ML Mon Nov 14 18:25:34 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Tue Nov 15 10:11:52 2005 +0100
@@ -11,7 +11,8 @@
datatype itype =
IType of string * itype list
| IFun of itype * itype
- | IVarT of vname * sort;
+ | IVarT of vname * sort
+ | IDictT of (string * itype) list;
datatype ipat =
ICons of (string * ipat list) * itype
| IVarP of vname * itype;
@@ -21,7 +22,9 @@
| IApp of iexpr * iexpr
| IInst of iexpr * ClassPackage.sortlookup list list
| IAbs of (vname * itype) * iexpr
- | ICase of iexpr * (ipat * iexpr) list;
+ | ICase of iexpr * (ipat * iexpr) list
+ | IDictE of (string * iexpr) list
+ | ILookup of (string list * vname);
val eq_itype: itype * itype -> bool
val eq_ipat: ipat * ipat -> bool
val eq_iexpr: iexpr * iexpr -> bool
@@ -38,15 +41,15 @@
val ipat_of_iexpr: iexpr -> ipat;
val vars_of_ipats: ipat list -> vname list;
val instant_itype: vname * itype -> itype -> itype;
- val invent_tvar_names: itype list -> int -> vname list -> vname -> vname list;
- val invent_evar_names: iexpr list -> int -> vname list -> vname -> vname list;
+ val invent_var_t_names: itype list -> int -> vname list -> vname -> vname list;
+ val invent_var_e_names: iexpr list -> int -> vname list -> vname -> vname list;
datatype def =
Nop
| Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype)
- | Typsyn of (vname * string list) list * itype
- | Datatyp of (vname * string list) list * string list * string list
- | Datatypcons of string * itype list
+ | Typesyn of (vname * string list) list * itype
+ | Datatype of (vname * string list) list * string list * string list
+ | Datatypecons of string * itype list
| Class of string list * string list * string list
| Classmember of string * vname * itype
| Classinst of string * (string * string list list) * (string * string) list;
@@ -60,10 +63,6 @@
val pretty_module: module -> Pretty.T;
val empty_module: module;
val get_def: module -> string -> def;
- val map_defs: (def -> def) -> module -> module;
- val add_deps: (string * def -> (string * string) list) -> module -> module;
- val fold_defs: (string * def -> 'a -> 'a) -> module -> 'a -> 'a;
- val fold_map_defs: (string * def -> 'a -> def * 'a) -> module -> 'a -> module * 'a;
val merge_module: module * module -> module;
val partof: string list -> module -> module;
val succeed: 'a -> transact -> 'a transact_fin;
@@ -73,6 +72,14 @@
val gen_ensure_def: (string * gen_defgen) list -> string
-> string -> transact -> transact;
+ val prims: string list;
+ val extract_defs: iexpr -> string list;
+ val eta_expand: (string -> int) -> module -> module;
+ val connect_datatypes_clsdecls: module -> module;
+ val tupelize_cons: module -> module;
+ val eliminate_dtconstr: module -> module;
+ val eliminate_classes: module -> module;
+
val debug_level : int ref;
val debug : int -> ('a -> string) -> 'a -> 'a;
end;
@@ -122,6 +129,13 @@
| SOME (x1, x2) =>
let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
+fun map_yield f [] = ([], [])
+ | map_yield f (x::xs) =
+ let
+ val (y, x') = f x
+ val (ys, xs') = map_yield f xs
+ in (y::ys, x'::xs') end;
+
fun get_prefix eq ([], ys) = ([], [], ys)
| get_prefix eq (xs, []) = ([], xs, [])
| get_prefix eq (xs as x::xs', ys as y::ys') =
@@ -146,7 +160,9 @@
datatype itype =
IType of string * itype list
| IFun of itype * itype
- | IVarT of vname * sort;
+ | IVarT of vname * sort
+ (*ML auxiliary*)
+ | IDictT of (string * itype) list;
datatype ipat =
ICons of (string * ipat list) * itype
@@ -158,7 +174,10 @@
| IApp of iexpr * iexpr
| IInst of iexpr * ClassPackage.sortlookup list list
| IAbs of (vname * itype) * iexpr
- | ICase of iexpr * (ipat * iexpr) list;
+ | ICase of iexpr * (ipat * iexpr) list
+ (*ML auxiliary*)
+ | IDictE of (string * iexpr) list
+ | ILookup of (string list * vname);
val eq_itype = (op =);
val eq_ipat = (op =);
@@ -185,6 +204,56 @@
(fn ICase (e, [(p, e')]) => SOME ((p, e), e')
| _ => NONE);
+fun map_itype f_itype (IType (tyco, tys)) =
+ tyco `%% map f_itype tys
+ | map_itype f_itype (IFun (t1, t2)) =
+ f_itype t1 `-> f_itype t2
+ | map_itype _ (ty as IVarT _) =
+ ty;
+
+fun map_ipat f_itype f_ipat (ICons ((c, ps), ty)) =
+ ICons ((c, map f_ipat ps), f_itype ty)
+ | map_ipat _ _ (p as IVarP _) =
+ p;
+
+fun map_iexpr f_itype f_ipat f_iexpr (IApp (e1, e2)) =
+ f_iexpr e1 `$ f_iexpr e2
+ | map_iexpr f_itype f_ipat f_iexpr (IInst (e, c)) =
+ IInst (f_iexpr e, c)
+ | map_iexpr f_itype f_ipat f_iexpr (IAbs (v, e)) =
+ IAbs (v, f_iexpr e)
+ | map_iexpr f_itype f_ipat f_iexpr (ICase (e, ps)) =
+ ICase (f_iexpr e, map (fn (p, e) => (f_ipat p, f_iexpr e)) ps)
+ | map_iexpr _ _ _ (e as IConst _) =
+ e
+ | map_iexpr _ _ _ (e as IVarE _) =
+ e;
+
+fun fold_itype f_itype (IFun (t1, t2)) =
+ f_itype t1 #> f_itype t2
+ | fold_itype _ (ty as IType _) =
+ I
+ | fold_itype _ (ty as IVarT _) =
+ I;
+
+fun fold_ipat f_itype f_ipat (ICons ((_, ps), ty)) =
+ f_itype ty #> fold f_ipat ps
+ | fold_ipat f_itype f_ipat (p as IVarP _) =
+ I;
+
+fun fold_iexpr f_itype f_ipat f_iexpr (IApp (e1, e2)) =
+ f_iexpr e1 #> f_iexpr e2
+ | fold_iexpr f_itype f_ipat f_iexpr (IInst (e, c)) =
+ f_iexpr e
+ | fold_iexpr f_itype f_ipat f_iexpr (IAbs (v, e)) =
+ f_iexpr e
+ | fold_iexpr f_itype f_ipat f_iexpr (ICase (e, ps)) =
+ f_iexpr e #> fold (fn (p, e) => f_ipat p #> f_iexpr e) ps
+ | fold_iexpr _ _ _ (e as IConst _) =
+ I
+ | fold_iexpr _ _ _ (e as IVarE _) =
+ I;
+
(* simple diagnosis *)
@@ -265,7 +334,7 @@
if v = u then sty else w
in instant ty end;
-fun invent_tvar_names tys n used a =
+fun invent_var_t_names tys n used a =
let
fun invent (IType (_, tys)) =
fold invent tys
@@ -275,7 +344,7 @@
cons v
in Term.invent_names (fold invent tys used) a n end;
-fun invent_evar_names es n used a =
+fun invent_var_e_names es n used a =
let
fun invent (IConst (f, _)) =
I
@@ -301,9 +370,9 @@
datatype def =
Nop
| Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype)
- | Typsyn of (vname * string list) list * itype
- | Datatyp of (vname * string list) list * string list * string list
- | Datatypcons of string * itype list
+ | Typesyn of (vname * string list) list * itype
+ | Datatype of (vname * string list) list * string list * string list
+ | Datatypecons of string * itype list
| Class of string list * string list * string list
| Classmember of string * string * itype
| Classinst of string * (string * string list list) * (string * string) list;
@@ -335,13 +404,13 @@
pretty_itype ty
]) eqs
)
- | pretty_def (Typsyn (vs, ty)) =
+ | pretty_def (Typesyn (vs, ty)) =
Pretty.block [
Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
Pretty.str " |=> ",
pretty_itype ty
]
- | pretty_def (Datatyp (vs, cs, clss)) =
+ | pretty_def (Datatype (vs, cs, clss)) =
Pretty.block [
Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
Pretty.str " |=> ",
@@ -349,7 +418,7 @@
Pretty.str ", instance of ",
Pretty.gen_list "," "[" "]" (map Pretty.str clss)
]
- | pretty_def (Datatypcons (dtname, tys)) =
+ | pretty_def (Datatypecons (dtname, tys)) =
Pretty.block [
Pretty.str "cons ",
Pretty.gen_list " ->" "" "" (map pretty_itype tys @ [Pretty.str dtname])
@@ -471,6 +540,18 @@
apfst Module o Graph.fold_map_nodes (foldmap (prfix @ [name])) modl
in Graph.fold_map_nodes (foldmap []) end;
+fun map_def_fun f_ipat f_iexpr (Fun (eqs, cty)) =
+ Fun (map (fn (ps, rhs) => (map f_ipat ps, f_iexpr rhs)) eqs, cty)
+ | map_def_fun _ _ def = def;
+
+fun transform_defs f_def f_ipat f_iexpr s modl =
+ let
+ val (modl', s') = fold_map_defs f_def modl s
+ in
+ modl'
+ |> map_defs (map_def_fun (f_ipat s') (f_iexpr s'))
+ end;
+
fun merge_module modl12 =
let
fun join_module (Module m1, Module m2) =
@@ -484,12 +565,12 @@
fun partof names modl =
let
datatype pathnode = PN of (string list * (string * pathnode) list);
- fun mk_path ([], base) (PN (defs, modls)) =
+ fun mk_ipath ([], base) (PN (defs, modls)) =
PN (base :: defs, modls)
- | mk_path (n::ns, base) (PN (defs, modls)) =
+ | mk_ipath (n::ns, base) (PN (defs, modls)) =
modls
|> AList.default (op =) (n, PN ([], []))
- |> AList.map_entry (op =) n (mk_path (ns, base))
+ |> AList.map_entry (op =) n (mk_ipath (ns, base))
|> (pair defs #> PN);
fun select (PN (defs, modls)) (Module module) =
module
@@ -498,15 +579,15 @@
|> Module;
in
Module modl
- |> select (fold (mk_path o dest_name) (filter NameSpace.is_qualified names) (PN ([], [])))
+ |> select (fold (mk_ipath o dest_name) (filter NameSpace.is_qualified names) (PN ([], [])))
|> dest_modl
end;
-fun add_check_transform (name, (Datatypcons (dtname, _))) =
+fun add_check_transform (name, (Datatypecons (dtname, _))) =
([([dtname],
- fn [Datatyp (_, _, [])] => NONE | _ => "attempted to add constructor to already instantiating datatype" |> SOME)],
+ fn [Datatype (_, _, [])] => NONE | _ => "attempted to add constructor to already instantiating datatype" |> SOME)],
[(dtname,
- fn Datatyp (vs, cs, clss) => Datatyp (vs, name::cs, clss)
+ fn Datatype (vs, cs, clss) => Datatype (vs, name::cs, clss)
| def => "attempted to add datatype constructor to non-datatype: "
^ (Pretty.output o pretty_def) def |> error)])
| add_check_transform (name, Classmember (clsname, v, ty)) =
@@ -537,7 +618,7 @@
fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] =
let
val mtyp_i' = instant_itype (v, tyco `%%
- map2 IVarT ((invent_tvar_names [mtyp_c] (length arity) [] "a"), arity)) mtyp_c;
+ map2 IVarT ((invent_var_t_names [mtyp_c] (length arity) [] "a"), arity)) mtyp_c;
in if eq_itype (mtyp_i', mtyp_i) (*! PERHAPS TOO STRICT !*)
then NONE
else "wrong type signature for class member: "
@@ -550,7 +631,7 @@
| def => "attempted to add class instance to non-class"
^ (Pretty.output o pretty_def) def |> error),
(tyco,
- fn Datatyp (vs, cs, clss) => Datatyp (vs, cs, clsname::clss)
+ fn Datatype (vs, cs, clss) => Datatype (vs, cs, clsname::clss)
| Nop => Nop
| def => "attempted to instantiate non-type to class instance"
^ (Pretty.output o pretty_def) def |> error)])
@@ -620,6 +701,277 @@
|-> (fn names => pair (names@deps))
end;
+
+
+(** primitive language constructs **)
+
+val class_eq = "Eqtype"; (*defined for all primitve types and extensionally for all datatypes*)
+val type_bool = "Bool";
+val type_integer = "Integer"; (*infinite!*)
+val type_float = "Float";
+val type_pair = "Pair";
+val type_list = "List";
+val cons_true = "True";
+val cons_false = "False";
+val cons_not = "not";
+val cons_pair = "Pair";
+val cons_nil = "Nil";
+val cons_cons = "Cons";
+val fun_primeq = "primeq"; (*defined for all primitive types*)
+val fun_eq = "eq"; (*to class eq*)
+val fun_not = "not";
+val fun_and = "and";
+val fun_or = "or";
+val fun_if = "if";
+val fun_fst = "fst";
+val fun_snd = "snd";
+val fun_add = "add";
+val fun_mult = "mult";
+val fun_minus = "minus";
+val fun_lt = "lt";
+val fun_le = "le";
+val fun_wfrec = "wfrec";
+
+local
+
+val A = IVarT ("a", []);
+val B = IVarT ("b", []);
+val E = IVarT ("e", [class_eq]);
+
+in
+
+val Type_bool = type_bool `%% [];
+val Type_integer = type_integer `%% [];
+val Type_float = type_float `%% [];
+fun Type_pair a b = type_pair `%% [a, b];
+fun Type_list a = type_list `%% [a];
+val Cons_true = IConst (cons_true, Type_bool);
+val Cons_false = IConst (cons_false, Type_bool);
+val Cons_pair = IConst (cons_pair, A `-> B `-> Type_pair A B);
+val Cons_nil = IConst (cons_nil, Type_list A);
+val Cons_cons = IConst (cons_cons, A `-> Type_list A `-> Type_list A);
+val Fun_eq = IConst (fun_eq, E `-> E `-> Type_bool);
+val Fun_not = IConst (fun_not, Type_bool `-> Type_bool);
+val Fun_and = IConst (fun_and, Type_bool `-> Type_bool `-> Type_bool);
+val Fun_or = IConst (fun_or, Type_bool `-> Type_bool `-> Type_bool);
+val Fun_if = IConst (fun_if, Type_bool `-> A `-> A `-> A);
+val Fun_fst = IConst (fun_fst, Type_pair A B `-> A);
+val Fun_snd = IConst (fun_snd, Type_pair A B `-> B);
+val Fun_0 = IConst ("0", Type_integer);
+val Fun_1 = IConst ("1", Type_integer);
+val Fun_add = IConst (fun_add, Type_integer `-> Type_integer `-> Type_integer);
+val Fun_mult = IConst (fun_mult, Type_integer `-> Type_integer `-> Type_integer);
+val Fun_minus = IConst (fun_minus, Type_integer `-> Type_integer);
+val Fun_lt = IConst (fun_lt, Type_integer `-> Type_integer `-> Type_bool);
+val Fun_le = IConst (fun_le, Type_integer `-> Type_integer `-> Type_bool);
+val Fun_wfrec = IConst (fun_wfrec, ((A `-> B) `-> A `-> B) `-> A `-> B);
+
+infix 7 xx;
+infix 5 **;
+infix 5 &&;
+
+fun a xx b = Type_pair a b;
+fun a ** b =
+ let
+ val ty_a = itype_of_iexpr a;
+ val ty_b = itype_of_iexpr b;
+ in IConst (cons_pair, ty_a `-> ty_b `-> ty_a xx ty_b) `$ a `$ b end;
+fun a && b =
+ let
+ val ty_a = itype_of_ipat a;
+ val ty_b = itype_of_ipat b;
+ in ICons ((cons_pair, [a, b]), ty_a xx ty_b) end;
+
+end; (* local *)
+
+val prims = [class_eq, type_bool, type_integer, type_float, type_pair, type_list,
+ cons_true, cons_false, cons_pair, cons_nil, cons_cons, fun_primeq, fun_eq, fun_not, fun_and,
+ fun_or, fun_if, fun_fst, fun_snd, fun_add, fun_mult, fun_minus, fun_lt, fun_le, fun_wfrec];
+
+fun extract_defs e =
+ let
+ fun extr_itype (ty as IType (tyco, _)) =
+ cons tyco #> fold_itype extr_itype ty
+ | extr_itype ty =
+ fold_itype extr_itype ty
+ fun extr_ipat (p as ICons ((c, _), _)) =
+ cons c #> fold_ipat extr_itype extr_ipat p
+ | extr_ipat p =
+ fold_ipat extr_itype extr_ipat p
+ fun extr_iexpr (e as IConst (f, _)) =
+ cons f #> fold_iexpr extr_itype extr_ipat extr_iexpr e
+ | extr_iexpr e =
+ fold_iexpr extr_itype extr_ipat extr_iexpr e
+ in extr_iexpr e [] end;
+
+
+
+(** generic transformation **)
+
+fun eta_expand query =
+ let
+ fun eta_app ((f, ty), es) =
+ let
+ val delta = query f - length es;
+ val add_n = if delta < 0 then 0 else delta;
+ val add_vars =
+ invent_var_e_names es add_n [] "x" ~~ Library.drop (length es, (fst o unfold_fun) ty);
+ in
+ Library.foldr IAbs (add_vars, IConst (f, ty) `$$ es `$$ (map IVarE add_vars))
+ end;
+ fun eta_iexpr' e = map_iexpr I I eta_iexpr e
+ and eta_iexpr (IConst (f, ty)) =
+ eta_app ((f, ty), [])
+ | eta_iexpr (e as IApp _) =
+ (case (unfold_app e)
+ of (IConst (f, ty), es) =>
+ eta_app ((f, ty), map eta_iexpr es)
+ | _ => eta_iexpr' e)
+ | eta_iexpr e = eta_iexpr' e;
+ in map_defs (map_def_fun I eta_iexpr) end;
+
+fun connect_datatypes_clsdecls module =
+ let
+ fun extract_dep (name, Datatypecons (dtname, _)) =
+ [(dtname, name)]
+ | extract_dep (name, Classmember (cls, _, _)) =
+ [(cls, name)]
+ | extract_dep (name, def) = []
+ in add_deps extract_dep module end;
+
+fun tupelize_cons module =
+ let
+ fun replace_def (_, (def as Datatypecons (_, []))) acc =
+ (def, acc)
+ | replace_def (_, (def as Datatypecons (_, [_]))) acc =
+ (def, acc)
+ | replace_def (name, (Datatypecons (tyco, tys))) acc =
+ (Datatypecons (tyco,
+ [foldl' (op xx) (NONE, tys)]), name::acc)
+ | replace_def (_, def) acc = (def, acc);
+ fun replace_app cs ((f, ty), es) =
+ if member (op =) cs f
+ then
+ let
+ val (tys, ty') = unfold_fun ty
+ in IConst (f, foldr' (op xx) (tys, NONE) `-> ty') `$ foldl' (op **) (NONE, es) end
+ else IConst (f, ty) `$$ es;
+ fun replace_iexpr cs (IConst (f, ty)) =
+ replace_app cs ((f, ty), [])
+ | replace_iexpr cs (e as IApp _) =
+ (case unfold_app e
+ of (IConst fty, es) => replace_app cs (fty, map (replace_iexpr cs) es)
+ | _ => map_iexpr I I (replace_iexpr cs) e)
+ | replace_iexpr cs e = map_iexpr I I (replace_iexpr cs) e;
+ fun replace_ipat cs (p as ICons ((c, ps), ty)) =
+ if member (op =) cs c then
+ ICons ((c, [(foldl' (op &&) (NONE, map (replace_ipat cs) ps))]), ty)
+ else map_ipat I (replace_ipat cs) p
+ | replace_ipat cs p = map_ipat I (replace_ipat cs) p;
+ in
+ transform_defs replace_def replace_ipat replace_iexpr [cons_cons] module
+ end;
+
+fun eliminate_dtconstr module =
+ let
+ fun replace_def (name, (Datatype (vs, cs, is))) acc =
+ (Datatype (map (fn (v, _) => (v, [])) vs, cs, is), (name, vs)::acc)
+ | replace_def (_, def) acc = (def, acc);
+ fun constrain (ty as IType _, _) =
+ ty
+ | constrain (IVarT (v, sort1), (_, sort2)) =
+ IVarT (v, gen_union (op =) (sort1, sort2));
+ fun replace_ty tycos (ty as (IType (tyco, tys))) =
+ (case AList.lookup (op =) tycos tyco
+ of NONE => ty
+ | SOME vs => IType (tyco, map2 constrain (tys, vs)))
+ | replace_ty tycos ty =
+ map_itype (replace_ty tycos) ty;
+ in
+ transform_defs replace_def
+ (*! HIER FEHLT NOCH: ÄNDERN VON TYP UND SORTCTXT BEI FUNS !*)
+ (fn tycos => map_ipat (replace_ty tycos) I)
+ (fn tycos => map_iexpr (replace_ty tycos) (map_ipat (replace_ty tycos) I) I) [] module
+ end;
+
+fun eliminate_classes module =
+ let
+ fun mk_cls_typ_map memberdecls ty_inst =
+ map (fn (memname, (v, ty)) =>
+ (memname, ty |> instant_itype (v, ty_inst))) memberdecls;
+ fun transform_dicts (Class (supcls, members, insts)) =
+ let
+ val memberdecls = AList.make
+ ((fn Classmember (_, v, ty) => (v, ty)) o get_def module) members;
+ val varname_cls = invent_var_t_names (map (snd o snd) memberdecls) 1 [] "a" |> hd;
+ in
+ Typesyn ([(varname_cls, [])], IDictT (mk_cls_typ_map memberdecls (IVarT (varname_cls, []))))
+ end
+ | transform_dicts (Classinst (tyco, (cls, arity), memdefs)) =
+ let
+ val Class (_, members, _) = get_def module cls;
+ val memberdecls = AList.make
+ ((fn Classmember (_, v, ty) => (v, ty)) o get_def module) members;
+ val ty_arity = tyco `%% map IVarT (invent_var_t_names (map (snd o snd) memberdecls)
+ (length arity) [] "a" ~~ arity);
+ val inst_typ_map = mk_cls_typ_map memberdecls ty_arity;
+ val memdefs_ty = map (fn (memname, memprim) =>
+ (memname, (memprim, (the o AList.lookup (op =) inst_typ_map) memname))) memdefs;
+ in
+ Fun ([([], IDictE (map (apsnd IConst) memdefs_ty))],
+ ([], IDictT inst_typ_map))
+ end
+ | transform_dicts d = d
+ fun transform_defs (Fun (ds, (sortctxt, ty))) =
+ let
+ fun reduce f xs = foldl' f (NONE, xs);
+ val varnames_ctxt =
+ sortctxt
+ |> length o Library.flat o map snd
+ |> (fn used => invent_var_e_names (map snd ds) used ((vars_of_ipats o fst o hd) ds) "d")
+ |> unflat (map snd sortctxt);
+ val vname_alist = map2 (fn ((vt, sort), vs) => (vt, vs ~~ sort)) (sortctxt, varnames_ctxt);
+ fun add_typarms ty =
+ map (reduce (op xx) o (fn (vt, vss) => map (fn (_, cls) => cls `%% [IVarT (vt, [])]) vss)) vname_alist
+ `--> ty;
+ fun add_parms ps =
+ map (reduce (op &&) o (fn (vt, vss) => map (fn (v, cls) => IVarP (v, cls `%% [IVarT (vt, [])])) vss)) vname_alist
+ @ ps;
+ fun transform_itype (IVarT (v, s)) =
+ IVarT (v, [])
+ | transform_itype ty =
+ map_itype transform_itype ty;
+ fun transform_ipat p =
+ map_ipat transform_itype transform_ipat p;
+ fun transform_lookup (ClassPackage.Instance ((cdict, idict), ls)) =
+ ls
+ |> transform_lookups
+ |-> (fn ty =>
+ curry mk_apps (IConst (idict, cdict `%% ty))
+ #> pair (cdict `%% ty))
+ | transform_lookup (ClassPackage.Lookup (deriv, (v, i))) =
+ let
+ val (v', cls) =
+ (nth o the oo AList.lookup (op =)) vname_alist v i;
+ fun mk_parm tyco = tyco `%% [IVarT (v, [])];
+ in (mk_parm (hd (deriv)), ILookup (rev deriv, v')) end
+ and transform_lookups lss =
+ map_yield (map_yield transform_lookup
+ #> apfst (reduce (op xx))
+ #> apsnd (reduce (op **))) lss;
+ fun transform_iexpr (IInst (e, ls)) =
+ transform_iexpr e `$$ (snd o transform_lookups) ls
+ | transform_iexpr e =
+ map_iexpr transform_itype transform_ipat transform_iexpr e;
+ fun transform_rhs (ps, rhs) = (add_parms ps, transform_iexpr rhs)
+ in Fun (map transform_rhs ds, ([], add_typarms ty)) end
+ | transform_defs d = d
+ in
+ module
+ |> map_defs transform_dicts
+ |> map_defs transform_defs
+ end;
+
end; (* struct *)
@@ -629,4 +981,3 @@
open CodegenThingolOp;
end; (* struct *)
-