From cfb8ffaf94885d8dc1b492a050830a9b4ffc3d04 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 1 Nov 2008 15:58:55 -0400 Subject: First Unnest tests working --- src/unnest.sml | 369 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 369 insertions(+) create mode 100644 src/unnest.sml (limited to 'src/unnest.sml') diff --git a/src/unnest.sml b/src/unnest.sml new file mode 100644 index 00000000..e5eddc42 --- /dev/null +++ b/src/unnest.sml @@ -0,0 +1,369 @@ +(* Copyright (c) 2008, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +(* Remove nested function definitions *) + +structure Unnest :> UNNEST = struct + +open Elab + +structure E = ElabEnv +structure U = ElabUtil + +structure IS = IntBinarySet + +val fvsCon = U.Con.foldB {kind = fn (_, st) => st, + con = fn (cb, c, cvs) => + case c of + CRel n => + if n >= cb then + IS.add (cvs, n - cb) + else + cvs + | _ => cvs, + bind = fn (cb, b) => + case b of + U.Con.Rel _ => cb + 1 + | _ => cb} + 0 IS.empty + +fun fvsExp nr = U.Exp.foldB {kind = fn (_, st) => st, + con = fn ((cb, eb), c, st as (cvs, evs)) => + case c of + CRel n => + if n >= cb then + (IS.add (cvs, n - cb), evs) + else + st + | _ => st, + exp = fn ((cb, eb), e, st as (cvs, evs)) => + case e of + ERel n => + if n >= eb then + (cvs, IS.add (evs, n - eb)) + else + st + | _ => st, + bind = fn (ctx as (cb, eb), b) => + case b of + U.Exp.RelC _ => (cb + 1, eb) + | U.Exp.RelE _ => (cb, eb + 1) + | _ => ctx} + (0, nr) (IS.empty, IS.empty) + +fun positionOf (x : int) ls = + let + fun po n ls = + case ls of + [] => raise Fail "Unnest.positionOf" + | x' :: ls' => + if x' = x then + n + else + po (n + 1) ls' + in + po 0 ls + handle Fail _ => raise Fail ("Unnset.positionOf(" + ^ Int.toString x + ^ ", " + ^ String.concatWith ";" (map Int.toString ls) + ^ ")") + end + +fun squishCon cfv = + U.Con.mapB {kind = fn k => k, + con = fn cb => fn c => + case c of + CRel n => + if n >= cb then + CRel (positionOf (n - cb) cfv + cb) + else + c + | _ => c, + bind = fn (cb, b) => + case b of + U.Con.Rel _ => cb + 1 + | _ => cb} + 0 + +fun squishExp (nr, cfv, efv) = + U.Exp.mapB {kind = fn k => k, + con = fn (cb, eb) => fn c => + case c of + CRel n => + if n >= cb then + CRel (positionOf (n - cb) cfv + cb) + else + c + | _ => c, + exp = fn (cb, eb) => fn e => + case e of + ERel n => + if n >= eb then + ERel (positionOf (n - eb) efv + eb) + else + e + | _ => e, + bind = fn (ctx as (cb, eb), b) => + case b of + U.Exp.RelC _ => (cb + 1, eb) + | U.Exp.RelE _ => (cb, eb + 1) + | _ => ctx} + (0, nr) + +type state = { + maxName : int, + decls : decl list +} + +fun kind (k, st) = (k, st) + +fun exp ((ks, ts), e, st : state) = + case e of + ELet (eds, e) => + let + val doSubst = foldl (fn (p, e) => E.subExpInExp p e) + + val (eds, (maxName, ds, subs)) = + ListUtil.foldlMapConcat + (fn (ed, (maxName, ds, subs)) => + case #1 ed of + EDVal _ => ([ed], (maxName, ds, map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)) + | EDValRec vis => + let + val loc = #2 ed + + val nr = length vis + val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) => + let + val (cfv', efv') = fvsExp nr e + (*val () = Print.prefaces "fvsExp" + [("e", ElabPrint.p_exp E.empty e), + ("cfv", Print.PD.string + (Int.toString (IS.numItems cfv'))), + ("efv", Print.PD.string + (Int.toString (IS.numItems efv')))]*) + val cfv'' = fvsCon t + in + (IS.union (cfv, IS.union (cfv', cfv'')), + IS.union (efv, efv')) + end) + (IS.empty, IS.empty) vis + + (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*) + val cfv = IS.foldl (fn (x, cfv) => + let + (*val () = print (Int.toString x ^ "\n")*) + val (_, t) = List.nth (ts, x) + in + IS.union (cfv, fvsCon t) + end) + cfv efv + (*val () = print "B\n"*) + + val (vis, maxName) = + ListUtil.foldlMap (fn ((x, t, e), maxName) => + ((x, maxName, t, e), + maxName + 1)) + maxName vis + + fun apply e = + let + val e = IS.foldl (fn (x, e) => + (ECApp (e, (CRel x, loc)), loc)) + e cfv + in + IS.foldl (fn (x, e) => + (EApp (e, (ERel x, loc)), loc)) + e efv + end + + val subs = map (fn (n, e) => (n + nr, E.liftExpInExp nr e)) subs + + val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) => + let + val e = apply (ENamed n, loc) + in + (0, E.liftExpInExp (nr - i - 1) e) + end) + vis + val subs' = rev subs' + + val cfv = IS.listItems cfv + val efv = IS.listItems efv + val efn = length efv + + (*val subsInner = subs + @ map (fn (i, e) => + (i + efn, + E.liftExpInExp efn e)) subs'*) + + val subs = subs @ subs' + + val vis = map (fn (x, n, t, e) => + let + (*val () = Print.prefaces "preSubst" + [("e", ElabPrint.p_exp E.empty e)]*) + val e = doSubst e subs(*Inner*) + + (*val () = Print.prefaces "squishCon" + [("t", ElabPrint.p_con E.empty t)]*) + 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, t) = foldr (fn (ex, (e, t)) => + let + val (name, t') = List.nth (ts, ex) + in + ((EAbs (name, + t', + t, + e), loc), + (TFun (t', + t), loc)) + end) + (e, t) efv + + val (e, t) = foldr (fn (cx, (e, t)) => + let + val (name, k) = List.nth (ks, cx) + in + ((ECAbs (Explicit, + name, + k, + e), loc), + (TCFun (Explicit, + name, + k, + t), loc)) + end) + (e, t) cfv + in + (x, n, t, e) + end) + vis + + val d = (DValRec vis, #2 ed) + in + ([], (maxName, d :: ds, subs)) + end) + (#maxName st, #decls st, []) eds + in + (ELet (eds, doSubst e subs), + {maxName = maxName, + decls = ds}) + end + + | _ => (e, st) + +fun default (ctx, d, st) = (d, st) + +fun bind ((ks, ts), b) = + case b of + U.Decl.RelC p => (p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts) + | U.Decl.RelE p => (ks, p :: ts) + | _ => (ks, ts) + +val unnestDecl = U.Decl.foldMapB {kind = kind, + con = default, + exp = exp, + sgn_item = default, + sgn = default, + str = default, + decl = default, + bind = bind} + ([], []) + +fun unnest file = + let + fun doDecl (all as (d, loc), st : state) = + let + fun default () = ([all], st) + fun explore () = + let + val (d, st) = unnestDecl st all + in + (rev (d :: #decls st), + {maxName = #maxName st, + decls = []}) + end + in + case d of + DCon _ => default () + | DDatatype _ => default () + | DDatatypeImp _ => default () + | DVal _ => explore () + | DValRec _ => explore () + | DSgn _ => default () + | DStr (x, n, sgn, str) => + let + val (str, st) = doStr (str, st) + in + ([(DStr (x, n, sgn, str), loc)], st) + end + | DFfiStr _ => default () + | DConstraint _ => default () + | DExport _ => default () + | DTable _ => default () + | DSequence _ => default () + | DClass _ => default () + | DDatabase _ => default () + end + + and doStr (all as (str, loc), st) = + let + fun default () = (all, st) + in + case str of + StrConst ds => + let + val (ds, st) = ListUtil.foldlMapConcat doDecl st ds + in + ((StrConst ds, loc), st) + end + | StrVar _ => default () + | StrProj _ => default () + | StrFun (x, n, dom, ran, str) => + let + val (str, st) = doStr (str, st) + in + ((StrFun (x, n, dom, ran, str), loc), st) + end + | StrApp _ => default () + | StrError => raise Fail "Unnest: StrError" + end + + val (ds, _) = ListUtil.foldlMapConcat doDecl + {maxName = U.File.maxName file + 1, + decls = []} file + in + ds + end + +end -- cgit v1.2.3