diff -r a87c0aeae92f -r 31aed965135c src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue Jan 31 16:12:56 2006 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Tue Jan 31 16:14:37 2006 +0100 @@ -13,38 +13,31 @@ | IFun of itype * itype | IVarT of vname * sort | IDictT of (string * itype) list; - datatype ipat = - ICons of (string * ipat list) * itype - | IVarP of vname * itype; datatype iexpr = - IConst of string * itype + IConst of (string * itype) * ClassPackage.sortlookup list list | IVarE of vname * itype | IApp of iexpr * iexpr - | IInst of iexpr * ClassPackage.sortlookup list | IAbs of (vname * itype) * iexpr - | ICase of iexpr * (ipat * iexpr) list + | ICase of iexpr * (iexpr * iexpr) list | IDictE of (string * iexpr) list | ILookup of (string list * vname); val mk_funs: itype list * itype -> itype; val mk_apps: iexpr * iexpr list -> iexpr; val mk_abss: (vname * itype) list * iexpr -> iexpr; val pretty_itype: itype -> Pretty.T; - val pretty_ipat: ipat -> Pretty.T; val pretty_iexpr: iexpr -> Pretty.T; val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list; val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a; val unfold_fun: itype -> itype list * itype; val unfold_app: iexpr -> iexpr * iexpr list; val unfold_abs: iexpr -> (vname * itype) list * iexpr; - val unfold_let: iexpr -> (ipat * iexpr) list * iexpr; + val unfold_let: iexpr -> (iexpr * iexpr) list * iexpr; + val unfold_const_app: iexpr -> + (((string * itype) * ClassPackage.sortlookup list list) * iexpr list) option; val itype_of_iexpr: iexpr -> itype; - val itype_of_ipat: ipat -> itype; - val ipat_of_iexpr: iexpr -> ipat; - val iexpr_of_ipat: ipat -> iexpr; val eq_itype: itype * itype -> bool; val tvars_of_itypes: itype list -> string list; - val vars_of_ipats: ipat list -> string list; - val vars_of_iexprs: iexpr list -> string list; + val names_of_iexprs: iexpr list -> string list; val `%% : string * itype list -> itype; val `-> : itype * itype -> itype; @@ -54,7 +47,7 @@ val `|-> : (vname * itype) * iexpr -> iexpr; val `|--> : (vname * itype) list * iexpr -> iexpr; - type funn = (ipat list * iexpr) list * (ClassPackage.sortcontext * itype); + type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype); datatype prim = Pretty of Pretty.T | Name of string; @@ -69,7 +62,9 @@ | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)) * string list | Classmember of class - | Classinst of (class * (string * (vname * sort) list)) * (string * funn) list; + | Classinst of ((class * (string * (vname * sort) list)) + * (class * (string * ClassPackage.sortlookup list list)) list) + * (string * funn) list; type module; type transact; type 'dst transact_fin; @@ -90,10 +85,8 @@ -> string -> transact -> transact; val start_transact: (transact -> 'a * transact) -> module -> 'a * module; - val extract_defs: iexpr -> string list; val eta_expand: (string -> int) -> module -> module; val eta_expand_poly: module -> module; - val eliminate_classes: module -> module; val debug_level: int ref; val debug: int -> ('a -> string) -> 'a -> 'a; @@ -164,17 +157,12 @@ (*ML auxiliary*) | IDictT of (string * itype) list; -datatype ipat = - ICons of (string * ipat list) * itype - | IVarP of vname * itype; - datatype iexpr = - IConst of string * itype + IConst of (string * itype) * ClassPackage.sortlookup list list | IVarE of vname * itype | IApp of iexpr * iexpr - | IInst of iexpr * ClassPackage.sortlookup list | IAbs of (vname * itype) * iexpr - | ICase of iexpr * (ipat * iexpr) list + | ICase of iexpr * (iexpr * iexpr) list (*ML auxiliary*) | IDictE of (string * iexpr) list | ILookup of (string list * vname); @@ -231,6 +219,11 @@ (fn ICase (e, [(p, e')]) => SOME ((p, e), e') | _ => NONE); +fun unfold_const_app e = + case unfold_app e + of (IConst x, es) => SOME (x, es) + | _ => NONE; + fun map_itype f_itype (IType (tyco, tys)) = tyco `%% map f_itype tys | map_itype f_itype (IFun (t1, t2)) = @@ -238,27 +231,20 @@ | 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)) = +fun map_iexpr f_itype 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)) = + | map_iexpr f_itype 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 _) = + | map_iexpr f_itype f_iexpr (ICase (e, ps)) = + ICase (f_iexpr e, map (fn (p, e) => (f_iexpr p, f_iexpr e)) ps) + | map_iexpr _ _ (e as IConst _) = e - | map_iexpr _ _ _ (e as IVarE _) = + | map_iexpr _ _ (e as IVarE _) = e - | map_iexpr f_itype f_ipat f_iexpr (IDictE ms) = + | map_iexpr f_itype f_iexpr (IDictE ms) = IDictE (map (apsnd f_iexpr) ms) - | map_iexpr _ _ _ (e as ILookup _) = - e ; + | map_iexpr _ _ (e as ILookup _) = + e; fun fold_itype f_itype (IFun (t1, t2)) = f_itype t1 #> f_itype t2 @@ -267,22 +253,15 @@ | 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)) = +fun fold_iexpr f_itype 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)) = + | fold_iexpr f_itype 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 _) = + | fold_iexpr f_itype f_iexpr (ICase (e, ps)) = + f_iexpr e #> fold (fn (p, e) => f_iexpr p #> f_iexpr e) ps + | fold_iexpr _ _ (e as IConst _) = I - | fold_iexpr _ _ _ (e as IVarE _) = + | fold_iexpr _ _ (e as IVarE _) = I; @@ -325,20 +304,12 @@ | pretty_itype (IDictT _) = Pretty.str ""; -fun pretty_ipat (ICons ((cons, ps), ty)) = - Pretty.enum " " "(" ")" - (Pretty.str cons :: map pretty_ipat ps @ [Pretty.str ":: ", pretty_itype ty]) - | pretty_ipat (IVarP (v, ty)) = - Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty]; - -fun pretty_iexpr (IConst (f, ty)) = - Pretty.block [Pretty.str (f ^ "::"), pretty_itype ty] +fun pretty_iexpr (IConst ((c, ty), _)) = + Pretty.block [Pretty.str (c ^ "::"), pretty_itype ty] | pretty_iexpr (IVarE (v, ty)) = Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty] | pretty_iexpr (IApp (e1, e2)) = Pretty.enclose "(" ")" [pretty_iexpr e1, Pretty.brk 1, pretty_iexpr e2] - | pretty_iexpr (IInst (e, c)) = - pretty_iexpr e | pretty_iexpr (IAbs ((v, ty), e)) = Pretty.enclose "(" ")" [Pretty.str ("?" ^ v ^ " |->"), Pretty.brk 1, pretty_iexpr e] | pretty_iexpr (ICase (e, cs)) = @@ -347,7 +318,7 @@ pretty_iexpr e, Pretty.enclose "(" ")" (map (fn (p, e) => Pretty.block [ - pretty_ipat p, + pretty_iexpr p, Pretty.str " => ", pretty_iexpr e ] @@ -361,7 +332,18 @@ (* language auxiliary *) -fun itype_of_iexpr (IConst (_, ty)) = ty + +fun instant_itype (v, sty) ty = + let + fun instant (IType (tyco, tys)) = + tyco `%% map instant tys + | instant (IFun (ty1, ty2)) = + instant ty1 `-> instant ty2 + | instant (w as (IVarT (u, _))) = + if v = u then sty else w + in instant ty end; + +fun itype_of_iexpr (IConst ((_, ty), s)) = ty | itype_of_iexpr (IVarE (_, ty)) = ty | itype_of_iexpr (e as IApp (e1, e2)) = (case itype_of_iexpr e1 of (IFun (ty2, ty')) => @@ -371,29 +353,9 @@ ^ ", " ^ (Pretty.output o pretty_itype) ty2 ^ " vs. " ^ (Pretty.output o pretty_itype o itype_of_iexpr) e2) | _ => error ("expression is not a function: " ^ Pretty.output (pretty_iexpr e1))) - | itype_of_iexpr (IInst (e, cs)) = itype_of_iexpr e | itype_of_iexpr (IAbs ((_, ty1), e2)) = ty1 `-> itype_of_iexpr e2 | itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e; -fun itype_of_ipat (ICons (_, ty)) = ty - | itype_of_ipat (IVarP (_, ty)) = ty; - -fun ipat_of_iexpr (IConst (f, ty)) = ICons ((f, []), ty) - | ipat_of_iexpr (IVarE v) = IVarP v - | ipat_of_iexpr (e as IApp _) = - (case unfold_app e - of (IConst (f, ty), es) => - ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty) - | (IInst (IConst (f, ty), _), es) => - ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty) - | _ => error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e)) - | ipat_of_iexpr e = - error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e); - -fun iexpr_of_ipat (ICons ((co, ps), ty)) = - IConst (co, map itype_of_ipat ps `--> ty) `$$ map iexpr_of_ipat ps - | iexpr_of_ipat (IVarP v) = IVarE v; - fun tvars_of_itypes tys = let fun vars (IType (_, tys)) = @@ -404,18 +366,10 @@ insert (op =) v in fold vars tys [] end; -fun vars_of_ipats ps = +fun names_of_iexprs es = let - fun vars (ICons ((_, ps), _)) = - fold vars ps - | vars (IVarP (v, _)) = - insert (op =) v - in fold vars ps [] end; - -fun vars_of_iexprs es = - let - fun vars (IConst (f, _)) = - I + fun vars (IConst ((c, _), _)) = + insert (op =) c | vars (IVarE (v, _)) = insert (op =) v | vars (IApp (e1, e2)) = @@ -425,32 +379,19 @@ #> vars e | vars (ICase (e, cs)) = vars e - #> fold (fn (p, e) => fold (insert (op =)) (vars_of_ipats [p]) #> vars e) cs - | vars (IInst (e, lookup)) = - vars e + #> fold (fn (p, e) => vars p #> vars e) cs | vars (IDictE ms) = fold (vars o snd) ms | vars (ILookup (_, v)) = cons v in fold vars es [] end; -fun instant_itype (v, sty) ty = - let - fun instant (IType (tyco, tys)) = - tyco `%% map instant tys - | instant (IFun (ty1, ty2)) = - instant ty1 `-> instant ty2 - | instant (w as (IVarT (u, _))) = - if v = u then sty else w - in instant ty end; - - (** language module system - definitions, modules, transactions **) (* type definitions *) -type funn = (ipat list * iexpr) list * (ClassPackage.sortcontext * itype); +type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype); datatype prim = Pretty of Pretty.T @@ -467,7 +408,9 @@ | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)) * string list | Classmember of class - | Classinst of (class * (string * (vname * sort) list)) * (string * funn) list; + | Classinst of ((class * (string * (vname * sort) list)) + * (class * (string * ClassPackage.sortlookup list list)) list) + * (string * funn) list; datatype node = Def of def | Module of node Graph.T; type module = node Graph.T; @@ -489,7 +432,7 @@ Pretty.enum " |" "" "" ( map (fn (ps, body) => Pretty.block [ - Pretty.enum "," "[" "]" (map pretty_ipat ps), + Pretty.enum "," "[" "]" (map pretty_iexpr ps), Pretty.str " |->", Pretty.brk 1, pretty_iexpr body, @@ -531,7 +474,7 @@ Pretty.str "class member belonging to ", Pretty.str clsname ] - | pretty_def (Classinst ((clsname, (tyco, arity)), _)) = + | pretty_def (Classinst (((clsname, (tyco, arity)), _), _)) = Pretty.block [ Pretty.str "class instance (", Pretty.str clsname, @@ -748,16 +691,16 @@ 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 map_def_fun f_iexpr (Fun (eqs, cty)) = + Fun (map (fn (ps, rhs) => (map f_iexpr ps, f_iexpr rhs)) eqs, cty) + | map_def_fun _ def = def; -fun transform_defs f_def f_ipat f_iexpr s modl = +fun transform_defs f_def 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')) + |> map_defs (map_def_fun (f_iexpr s')) end; fun merge_module modl12 = @@ -850,7 +793,7 @@ else error "attempted to add class with bare instances" | check_prep_def modl (Classmember _) = error "attempted to add bare class member" - | check_prep_def modl (Classinst ((d as (class, (tyco, arity)), memdefs))) = + | check_prep_def modl (Classinst ((d as ((class, (tyco, arity)), _), memdefs))) = let val Class ((_, (v, membrs)), _) = get_def modl class; val _ = if length memdefs > length memdefs @@ -881,7 +824,7 @@ #> add_dep (name, m) ) membrs ) - | postprocess_def (name, Classinst ((class, (tyco, _)), _)) = + | postprocess_def (name, Classinst (((class, (tyco, _)), _), _)) = map_def class (fn Datatype (d, insts) => Datatype (d, name::insts) | d => d) #> map_def class (fn Class (d, insts) => Class (d, name::insts)) @@ -979,25 +922,9 @@ (** generic transformation **) -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; - fun eta_expand query = let - fun eta_app ((f, ty), es) = + fun eta_app (((f, ty), ls), es) = let val delta = query f - length es; val add_n = if delta < 0 then 0 else delta; @@ -1006,20 +933,16 @@ |> curry Library.drop (length es) |> curry Library.take add_n val add_vars = - Term.invent_names (vars_of_iexprs es) "x" add_n ~~ tys; + Term.invent_names (names_of_iexprs es) "x" add_n ~~ tys; in - Library.foldr IAbs (add_vars, IConst (f, ty) `$$ es `$$ (map IVarE add_vars)) + Library.foldr IAbs (add_vars, + IConst ((f, ty), ls) `$$ 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 eta_iexpr e = + case unfold_const_app e + of SOME x => eta_app x + | NONE => map_iexpr I eta_iexpr e; + in map_defs (map_def_fun eta_iexpr) end; val eta_expand_poly = let @@ -1029,124 +952,11 @@ then def else let - val add_var = (hd (Term.invent_names (vars_of_iexprs [e]) "x" 1), ty1) - in (Fun ([([IVarP add_var], IAbs (add_var, e))], cty)) end + val add_var = (hd (Term.invent_names (names_of_iexprs [e]) "x" 1), ty1) + in (Fun ([([IVarE add_var], IAbs (add_var, e))], cty)) end | map_def_fun def = def; in map_defs map_def_fun end; -(*fun eliminate_classes module = - let - fun transform_itype (IVarT (v, s)) = - IVarT (v, []) - | transform_itype (ty as IDictT _) = - ty - | transform_itype ty = - map_itype transform_itype ty; - fun transform_ipat p = - map_ipat transform_itype transform_ipat p; - fun transform_iexpr vname_alist (IInst (e, ls)) = - let - fun transform_lookup (ClassPackage.Instance ((cdict, idict), ls)) = - ls - |> transform_lookups - |-> (fn tys => - curry mk_apps (IConst (idict, cdict `%% tys)) - #> pair (cdict `%% tys)) - | 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 cls, ILookup (deriv, v')) end - and transform_lookups lss = - map_yield (map_yield transform_lookup - #> apfst ** - #> apsnd XXe) lss - in transform_iexpr vname_alist e `$$ (snd o transform_lookups) ls end - | transform_iexpr vname_alist e = - map_iexpr transform_itype transform_ipat (transform_iexpr vname_alist) e; - fun elim_sorts (Fun (eqs, ([], ty))) = - Fun (map (fn (ps, rhs) => (map transform_ipat ps, transform_iexpr [] rhs)) eqs, - ([], transform_itype ty)) - | elim_sorts (Fun (eqs, (sortctxt, ty))) = - let - val varnames_ctxt = - burrow - (Term.invent_names ((vars_of_iexprs o map snd) eqs @ - (vars_of_ipats o Library.flat o map fst) eqs) "d" o length) - (map snd sortctxt); - val vname_alist = map2 (fn (vt, sort) => fn vs => (vt, vs ~~ sort)) - sortctxt varnames_ctxt; - val ty' = map (op ** o (fn (vt, vss) => map (fn (_, cls) => - cls `%% [IVarT (vt, [])]) vss)) vname_alist - `--> transform_itype ty; - val ps_add = map (XXp o (fn (vt, vss) => map (fn (v, cls) => - IVarP (v, cls `%% [IVarT (vt, [])])) vss)) vname_alist; - in Fun (map (fn (ps, rhs) => (ps_add @ map transform_ipat ps, transform_iexpr vname_alist rhs)) eqs, ([], ty')) end - | elim_sorts (Datatype (vars, constrs, insts)) = - Datatype (map (fn (v, _) => (v, [])) vars, map (apsnd (map transform_itype)) constrs, insts) - | elim_sorts (Typesyn (vars, ty)) = - Typesyn (map (fn (v, _) => (v, [])) vars, transform_itype ty) - | elim_sorts d = d; - fun mk_cls_typ_map v (supclss, membrs) ty_inst = - (map (fn class => (class, IType (class, [ty_inst]))) supclss, - map (fn (m, (mctxt, ty)) => - (m, ty |> instant_itype (v, ty_inst))) membrs); - fun extract_members (cls, Class (supclss, v, membrs, _)) = - let - val ty_cls = cls `%% [IVarT (v, [])]; - val w = "d"; - val add_supclss = if null supclss then I else cons (v, supclss); - fun mk_fun (m, (mctxt, ty)) = (m, Fun ([([IVarP (w, ty_cls)], ILookup ([m], w))], - (add_supclss mctxt, ty `-> ty_cls))); - in fold (cons o mk_fun) membrs end - | extract_members _ = I; - fun introduce_dicts (Class (supclss, v, membrs, insts)) = - let - val varname_cls = Term.invent_names (tvars_of_itypes (map (snd o snd) membrs)) "a" 1 |> hd - in - Typesyn ([(varname_cls, supclss)], IDictT ((op @) (mk_cls_typ_map v (supclss, membrs) (IVarT (varname_cls, []))))) - end - | introduce_dicts (Classinst ((clsname, (tyco, arity)), (supinsts, memdefs))) = - let - val Class (supclss, v, members, _) = - if clsname = class_eq - then - Class ([], "a", [(fun_eq, ([], IVarT ("a", []) `-> IVarT ("a", []) `-> Type_bool))], []) - else - get_def module clsname; - val ty = tyco `%% map IVarT arity; - val (supinst_typ_map, mem_typ_map) = mk_cls_typ_map v (supclss, members) ty; - fun mk_meminst (m, ty) = - let - val (instname, instlookup) = (the o AList.lookup (op =) memdefs) m; - in - IInst (IConst (instname, ty), instlookup) - |> pair m - end; - val memdefs_ty = map mk_meminst mem_typ_map; - fun mk_supinst (supcls, dictty) = - let - val (instname, instlookup) = (the o AList.lookup (op =) supinsts) supcls; - in - IInst (IConst (instname, dictty), instlookup) - |> pair supcls - end; - val instdefs_ty = map mk_supinst supinst_typ_map; - in - Fun ([([], IDictE (instdefs_ty @ memdefs_ty))], - (arity, IType (clsname, [ty]))) - end - | introduce_dicts d = d; - in - module - |> `(fn module => fold_defs extract_members module []) - |-> (fn membrs => fold (fn (name, f) => map_def name (K f)) membrs) - |> map_defs introduce_dicts - |> map_defs elim_sorts - end;*) - -fun eliminate_classes module = module; (** generic serialization **)