diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-11-01 21:19:43 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-11-01 21:19:43 -0400 |
commit | 047a2f193646e08db526768dca8376b7270eecb5 (patch) | |
tree | 2be405017cad5af57826b17c1715d9579eb06d1b /src | |
parent | 9a22207b565607db64f95dda5fdc1c9e56224ec9 (diff) |
Almost have that nested save function compiling
Diffstat (limited to 'src')
-rw-r--r-- | src/cjrize.sml | 19 | ||||
-rw-r--r-- | src/core_util.sml | 2 | ||||
-rw-r--r-- | src/elab_util.sml | 21 | ||||
-rw-r--r-- | src/especialize.sml | 149 | ||||
-rw-r--r-- | src/expl_print.sml | 1 | ||||
-rw-r--r-- | src/expl_util.sml | 2 | ||||
-rw-r--r-- | src/mono_opt.sml | 15 | ||||
-rw-r--r-- | src/mono_reduce.sig | 4 | ||||
-rw-r--r-- | src/shake.sml | 28 | ||||
-rw-r--r-- | src/sources | 6 | ||||
-rw-r--r-- | src/termination.sml | 10 | ||||
-rw-r--r-- | src/unnest.sml | 35 |
12 files changed, 208 insertions, 84 deletions
diff --git a/src/cjrize.sml b/src/cjrize.sml index 05ceb0f9..db2bd48f 100644 --- a/src/cjrize.sml +++ b/src/cjrize.sml @@ -39,6 +39,7 @@ structure Sm :> sig val find : t * (string * L.typ) list * (string * L'.typ) list -> t * int val declares : t -> (int * (string * L'.typ) list) list + val clearDeclares : t -> t end = struct structure FM = BinaryMapFn(struct @@ -61,6 +62,8 @@ fun find ((n, m, ds), xts, xts') = fun declares (_, _, ds) = ds +fun clearDeclares (n, m, _) = (n, m, []) + end fun cifyTyp x = @@ -520,23 +523,25 @@ fun cjrize ds = val (dsF, ds, ps, sm) = foldl (fn (d, (dsF, ds, ps, sm)) => let val (dop, pop, sm) = cifyDecl (d, sm) + val (dsF, ds) = case dop of NONE => (dsF, ds) - | SOME (d as (L'.DDatatype (dk, x, n, _), loc)) => - ((L'.DDatatypeForward (dk, x, n), loc) :: dsF, - d :: ds) + | SOME (d as (L'.DDatatype _, loc)) => + (d :: dsF, ds) | SOME d => (dsF, d :: ds) + + val dsF = map (fn v => (L'.DStruct v, ErrorMsg.dummySpan)) (Sm.declares sm) + @ dsF + val ps = case pop of NONE => ps | SOME p => p :: ps in - (dsF, ds, ps, sm) + (dsF, ds, ps, Sm.clearDeclares sm) end) ([], [], [], Sm.empty) ds in - (List.revAppend (dsF, - List.revAppend (map (fn v => (L'.DStruct v, ErrorMsg.dummySpan)) (Sm.declares sm), - rev ds)), + (List.revAppend (dsF, rev ds), ps) end diff --git a/src/core_util.sml b/src/core_util.sml index 2a690736..2450562f 100644 --- a/src/core_util.sml +++ b/src/core_util.sml @@ -492,7 +492,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = fn t' => S.bind2 (mfe ctx e1, fn e1' => - S.map2 (mfe ctx e2, + S.map2 (mfe (bind (ctx, RelE (x, t'))) e2, fn e2' => (ELet (x, t', e1', e2'), loc)))) diff --git a/src/elab_util.sml b/src/elab_util.sml index 2e190d1e..57a94486 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -375,14 +375,19 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = | ELet (des, e) => let val (des, ctx) = foldl (fn (ed, (des, ctx)) => - (S.bind2 (des, - fn des' => - S.map2 (mfed ctx ed, + let + val ctx' = + case #1 ed of + EDVal (x, t, _) => bind (ctx, RelE (x, t)) + | EDValRec vis => + foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis + in + (S.bind2 (des, + fn des' => + S.map2 (mfed ctx ed, fn ed' => des' @ [ed'])), - case #1 ed of - EDVal (x, t, _) => bind (ctx, RelE (x, t)) - | EDValRec vis => - foldl (fn ((x, t, _), env) => bind (ctx, RelE (x, t))) ctx vis)) + ctx') + end) (S.return2 [], ctx) des in S.bind2 (des, @@ -400,7 +405,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = (EDVal vi', loc)) | EDValRec vis => let - val ctx = foldl (fn ((x, t, _), env) => bind (ctx, RelE (x, t))) ctx vis + val ctx = foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis in S.map2 (ListUtil.mapfold (mfvi ctx) vis, fn vis' => diff --git a/src/especialize.sml b/src/especialize.sml index b2f0c7e6..d5e93680 100644 --- a/src/especialize.sml +++ b/src/especialize.sml @@ -32,17 +32,43 @@ open Core structure E = CoreEnv structure U = CoreUtil -structure ILK = struct -type ord_key = int list -val compare = Order.joinL Int.compare +datatype skey = + Named of int + | App of skey * skey + +structure K = struct +type ord_key = skey list +fun compare' (k1, k2) = + case (k1, k2) of + (Named n1, Named n2) => Int.compare (n1, n2) + | (Named _, _) => LESS + | (_, Named _) => GREATER + + | (App (x1, y1), App (x2, y2)) => Order.join (compare' (x1, x2), fn () => compare' (y1, y2)) + +val compare = Order.joinL compare' end -structure ILM = BinaryMapFn(ILK) +structure KM = BinaryMapFn(K) structure IM = IntBinaryMap +fun skeyIn (e, _) = + case e of + ENamed n => SOME (Named n) + | EApp (e1, e2) => + (case (skeyIn e1, skeyIn e2) of + (SOME k1, SOME k2) => SOME (App (k1, k2)) + | _ => NONE) + | _ => NONE + +fun skeyOut (k, loc) = + case k of + Named n => (ENamed n, loc) + | App (k1, k2) => (EApp (skeyOut (k1, loc), skeyOut (k2, loc)), loc) + type func = { name : string, - args : int ILM.map, + args : int KM.map, body : exp, typ : con, tag : string @@ -62,14 +88,21 @@ fun exp (e, st : state) = fun getApp e = case e of ENamed f => SOME (f, [], []) - | EApp (e1, (ENamed x, _)) => - (case getApp (#1 e1) of - NONE => NONE - | SOME (f, xs, xs') => SOME (f, xs @ [x], xs')) | EApp (e1, e2) => (case getApp (#1 e1) of NONE => NONE - | SOME (f, xs, xs') => SOME (f, xs, xs' @ [e2])) + | SOME (f, xs, xs') => + let + val k = + if List.null xs' then + skeyIn e2 + else + NONE + in + case k of + NONE => SOME (f, xs, xs' @ [e2]) + | SOME k => SOME (f, xs @ [k], xs') + end) | _ => NONE in case getApp e of @@ -77,21 +110,30 @@ fun exp (e, st : state) = | SOME (_, [], _) => (e, st) | SOME (f, xs, xs') => case IM.find (#funcs st, f) of - NONE => (e, st) + NONE => ((*print "SHOT DOWN!\n";*) (e, st)) | SOME {name, args, body, typ, tag} => - case ILM.find (args, xs) of - SOME f' => (#1 (foldl (fn (e, arg) => (EApp (e, arg), ErrorMsg.dummySpan)) - (ENamed f', ErrorMsg.dummySpan) xs'), - st) + case KM.find (args, xs) of + SOME f' => ((*Print.prefaces "Pre-existing" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))];*) + (#1 (foldl (fn (e, arg) => (EApp (e, arg), ErrorMsg.dummySpan)) + (ENamed f', ErrorMsg.dummySpan) xs'), + st)) | NONE => let + (*val () = Print.prefaces "New" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))]*) + fun subBody (body, typ, xs) = case (#1 body, #1 typ, xs) of (_, _, []) => SOME (body, typ) | (EAbs (_, _, _, body'), TFun (_, typ'), x :: xs) => - subBody (E.subExpInExp (0, (ENamed x, ErrorMsg.dummySpan)) body', - typ', - xs) + let + val body'' = E.subExpInExp (0, skeyOut (x, #2 body)) body' + in + (*Print.prefaces "espec" [("body'", CorePrint.p_exp CoreEnv.empty body'), + ("body''", CorePrint.p_exp CoreEnv.empty body'')];*) + subBody (body'', + typ', + xs) + end | _ => NONE in case subBody (body, typ, xs) of @@ -99,8 +141,9 @@ fun exp (e, st : state) = | SOME (body', typ') => let val f' = #maxName st + (*val () = print ("f' = " ^ Int.toString f' ^ "\n")*) val funcs = IM.insert (#funcs st, f, {name = name, - args = ILM.insert (args, xs, f'), + args = KM.insert (args, xs, f'), body = body, typ = typ, tag = tag}) @@ -128,10 +171,27 @@ fun decl (d, st) = (d, st) val specDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl} -fun specialize file = +fun specialize' file = let - fun doDecl (d, st) = + fun doDecl (d, (st : state, changed)) = let + val funcs = #funcs st + val funcs = + case #1 d of + DValRec vis => + foldl (fn ((x, n, c, e, tag), funcs) => + IM.insert (funcs, n, {name = x, + args = KM.empty, + body = e, + typ = c, + tag = tag})) + funcs vis + | _ => funcs + + val st = {maxName = #maxName st, + funcs = funcs, + decls = []} + val (d', st) = specDecl st d val funcs = #funcs st @@ -139,37 +199,42 @@ fun specialize file = case #1 d of DVal (x, n, c, e as (EAbs _, _), tag) => IM.insert (funcs, n, {name = x, - args = ILM.empty, + args = KM.empty, body = e, typ = c, tag = tag}) - | DValRec vis => - foldl (fn ((x, n, c, e, tag), funcs) => - IM.insert (funcs, n, {name = x, - args = ILM.empty, - body = e, - typ = c, - tag = tag})) - funcs vis | _ => funcs - val ds = + val (changed, ds) = case #decls st of - [] => [d'] - | vis => [(DValRec vis, ErrorMsg.dummySpan), d'] + [] => (changed, [d']) + | vis => + (true, case d' of + (DValRec vis', _) => [(DValRec (vis @ vis'), ErrorMsg.dummySpan)] + | _ => [(DValRec vis, ErrorMsg.dummySpan), d']) in - (ds, {maxName = #maxName st, - funcs = funcs, - decls = []}) + (ds, ({maxName = #maxName st, + funcs = funcs, + decls = []}, changed)) end - val (ds, _) = ListUtil.foldlMapConcat doDecl - {maxName = U.File.maxName file + 1, - funcs = IM.empty, - decls = []} - file + val (ds, (_, changed)) = ListUtil.foldlMapConcat doDecl + ({maxName = U.File.maxName file + 1, + funcs = IM.empty, + decls = []}, false) + file + in + (changed, ds) + end + +fun specialize file = + let + val (changed, file) = specialize' file in - ds + if changed then + specialize file + else + file end diff --git a/src/expl_print.sml b/src/expl_print.sml index b19a6eff..aecc3a84 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -370,6 +370,7 @@ fun p_exp' par env (e, loc) = string x, space, string ":", + space, p_con env t, space, string "=", diff --git a/src/expl_util.sml b/src/expl_util.sml index e12186b0..337ea8d6 100644 --- a/src/expl_util.sml +++ b/src/expl_util.sml @@ -331,7 +331,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = fn t' => S.bind2 (mfe ctx e1, fn e1' => - S.map2 (mfe ctx e2, + S.map2 (mfe (bind (ctx, RelE (x, t))) e2, fn e2' => (ELet (x, t', e1', e2'), loc)))) in diff --git a/src/mono_opt.sml b/src/mono_opt.sml index 3cf2bcd4..b22f053b 100644 --- a/src/mono_opt.sml +++ b/src/mono_opt.sml @@ -89,7 +89,7 @@ fun sqlifyFloat n = attrifyFloat n ^ "::float8" fun sqlifyString s = "E'" ^ String.translate (fn #"'" => "\\'" | ch => str ch) (String.toString s) ^ "'::text" - + fun exp e = case e of EPrim (Prim.String s) => @@ -287,6 +287,19 @@ fun exp e = {disc = disc, result = (TRecord [], loc)}), loc) + | EApp ((ECase (discE, pes, {disc, ...}), loc), arg as (ERecord [], _)) => + let + fun doBody e = + case #1 e of + EAbs (_, _, _, body) => MonoReduce.subExpInExp (0, arg) body + | _ => (EApp (e, arg), loc) + in + optExp (ECase (discE, + map (fn (p, e) => (p, doBody e)) pes, + {disc = disc, + result = (TRecord [], loc)}), loc) + end + | EWrite (EQuery {exps, tables, state, query, initial = (EPrim (Prim.String ""), _), body = (EStrcat ((EPrim (Prim.String s), _), diff --git a/src/mono_reduce.sig b/src/mono_reduce.sig index 3769a0f5..2495c7f9 100644 --- a/src/mono_reduce.sig +++ b/src/mono_reduce.sig @@ -30,5 +30,7 @@ signature MONO_REDUCE = sig val reduce : Mono.file -> Mono.file - + + val subExpInExp : int * Mono.exp -> Mono.exp -> Mono.exp + end diff --git a/src/shake.sml b/src/shake.sml index 38d72cc5..4ebd1b0b 100644 --- a/src/shake.sml +++ b/src/shake.sml @@ -55,14 +55,19 @@ fun shake file = val (cdef, edef) = foldl (fn ((DCon (_, n, _, c), _), (cdef, edef)) => (IM.insert (cdef, n, [c]), edef) | ((DDatatype (_, n, _, xncs), _), (cdef, edef)) => (IM.insert (cdef, n, List.mapPartial #3 xncs), edef) - | ((DVal (_, n, t, e, _), _), (cdef, edef)) => (cdef, IM.insert (edef, n, (t, e))) + | ((DVal (_, n, t, e, _), _), (cdef, edef)) => (cdef, IM.insert (edef, n, ([], t, e))) | ((DValRec vis, _), (cdef, edef)) => - (cdef, foldl (fn ((_, n, t, e, _), edef) => IM.insert (edef, n, (t, e))) edef vis) + let + val all_ns = map (fn (_, n, _, _, _) => n) vis + in + (cdef, foldl (fn ((_, n, t, e, _), edef) => + IM.insert (edef, n, (all_ns, t, e))) edef vis) + end | ((DExport _, _), acc) => acc | ((DTable (_, n, c, _), _), (cdef, edef)) => - (cdef, IM.insert (edef, n, (c, dummye))) + (cdef, IM.insert (edef, n, ([], c, dummye))) | ((DSequence (_, n, _), _), (cdef, edef)) => - (cdef, IM.insert (edef, n, (dummyt, dummye))) + (cdef, IM.insert (edef, n, ([], dummyt, dummye))) | ((DDatabase _, _), acc) => acc) (IM.empty, IM.empty) file @@ -96,9 +101,15 @@ fun shake file = val s' = {exp = IS.add (#exp s, n), con = #con s} in + (*print ("Need " ^ Int.toString n ^ "\n");*) case IM.find (edef, n) of NONE => s' - | SOME (t, e) => shakeExp (shakeCon s' t) e + | SOME (ns, t, e) => + let + val s' = shakeExp (shakeCon s' t) e + in + foldl (fn (n, s') => exp (ENamed n, s')) s' ns + end end | _ => s @@ -109,7 +120,12 @@ fun shake file = val s = foldl (fn (n, s) => case IM.find (edef, n) of NONE => raise Fail "Shake: Couldn't find 'val'" - | SOME (t, e) => shakeExp (shakeCon s t) e) s page_es + | SOME (ns, t, e) => + let + val s = shakeExp (shakeCon s t) e + in + foldl (fn (n, s) => exp (ENamed n, s)) s ns + end) s page_es val s = foldl (fn (c, s) => shakeCon s c) s table_cs in diff --git a/src/sources b/src/sources index 984b5e23..504013d8 100644 --- a/src/sources +++ b/src/sources @@ -116,15 +116,15 @@ mono_print.sml monoize.sig monoize.sml +mono_reduce.sig +mono_reduce.sml + mono_opt.sig mono_opt.sml untangle.sig untangle.sml -mono_reduce.sig -mono_reduce.sml - mono_shake.sig mono_shake.sml diff --git a/src/termination.sml b/src/termination.sml index 6ed4d92f..2db5bb11 100644 --- a/src/termination.sml +++ b/src/termination.sml @@ -293,7 +293,15 @@ fun declOk' env (d, loc) = | EUnif (ref (SOME e)) => exp parent (penv, calls) e | EUnif (ref NONE) => (Rabble, calls) - | ELet (_, e) => exp parent (penv, calls) e + | ELet (eds, e) => + let + fun extPenv ((ed, _), penv) = + case ed of + EDVal _ => Rabble :: penv + | EDValRec vis => foldl (fn (_, penv) => Rabble :: penv) penv vis + in + exp parent (foldl extPenv penv eds, calls) e + end end fun doVali (i, (_, f, _, e), calls) = diff --git a/src/unnest.sml b/src/unnest.sml index b305b467..f226a678 100644 --- a/src/unnest.sml +++ b/src/unnest.sml @@ -124,7 +124,7 @@ fun squishExp (nr, cfv, efv) = case e of ERel n => if n >= eb then - ERel (positionOf (n - eb) efv + eb) + ERel (positionOf (n - eb) efv + eb) else e | _ => e, @@ -142,17 +142,21 @@ type state = { fun kind (k, st) = (k, st) -fun exp ((ks, ts), e, st : state) = +fun exp ((ks, ts), e as old, st : state) = case e of ELet (eds, e) => let + (*val () = Print.prefaces "let" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*) + val doSubst = foldl (fn (p, e) => E.subExpInExp p e) - val (eds, (maxName, ds, subs)) = + val (eds, (ts, maxName, ds, subs)) = ListUtil.foldlMapConcat - (fn (ed, (maxName, ds, subs)) => + (fn (ed, (ts, maxName, ds, subs)) => case #1 ed of - EDVal _ => ([ed], (maxName, ds, map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)) + EDVal (x, t, _) => ([ed], + ((x, t) :: ts, + maxName, ds, map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)) | EDValRec vis => let val loc = #2 ed @@ -174,7 +178,10 @@ fun exp ((ks, ts), e, st : state) = end) (IS.empty, IS.empty) vis - (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*) + (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n") + val () = app (fn (x, t) => + Print.prefaces "Var" [("x", Print.PD.string x), + ("t", ElabPrint.p_con E.empty t)]) ts*) val cfv = IS.foldl (fn (x, cfv) => let (*val () = print (Int.toString x ^ "\n")*) @@ -193,11 +200,11 @@ fun exp ((ks, ts), e, st : state) = fun apply e = let - val e = IS.foldl (fn (x, e) => + val e = IS.foldr (fn (x, e) => (ECApp (e, (CRel x, loc)), loc)) e cfv in - IS.foldl (fn (x, e) => + IS.foldr (fn (x, e) => (EApp (e, (ERel x, loc)), loc)) e efv end @@ -237,9 +244,9 @@ fun exp ((ks, ts), e, st : state) = val t = squishCon cfv t (*val () = Print.prefaces "squishExp" [("e", ElabPrint.p_exp E.empty e)]*) - val e = squishExp (nr, cfv, efv) e + val e = squishExp (0(*nr*), cfv, efv) e - val (e, t) = foldr (fn (ex, (e, t)) => + val (e, t) = foldl (fn (ex, (e, t)) => let val (name, t') = List.nth (ts, ex) in @@ -252,7 +259,7 @@ fun exp ((ks, ts), e, st : state) = end) (e, t) efv - val (e, t) = foldr (fn (cx, (e, t)) => + val (e, t) = foldl (fn (cx, (e, t)) => let val (name, k) = List.nth (ks, cx) in @@ -272,10 +279,12 @@ fun exp ((ks, ts), e, st : state) = vis val d = (DValRec vis, #2 ed) + + val ts = map (fn (x, _, t, _) => (x, t)) vis @ ts in - ([], (maxName, d :: ds, subs)) + ([], (ts, maxName, d :: ds, subs)) end) - (#maxName st, #decls st, []) eds + (ts, #maxName st, #decls st, []) eds in (ELet (eds, doSubst e subs), {maxName = maxName, |