adamc@1272: (* Copyright (c) 2008-2010, Adam Chlipala adamc@448: * All rights reserved. adamc@448: * adamc@448: * Redistribution and use in source and binary forms, with or without adamc@448: * modification, are permitted provided that the following conditions are met: adamc@448: * adamc@448: * - Redistributions of source code must retain the above copyright notice, adamc@448: * this list of conditions and the following disclaimer. adamc@448: * - Redistributions in binary form must reproduce the above copyright notice, adamc@448: * this list of conditions and the following disclaimer in the documentation adamc@448: * and/or other materials provided with the distribution. adamc@448: * - The names of contributors may not be used to endorse or promote products adamc@448: * derived from this software without specific prior written permission. adamc@448: * adamc@448: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@448: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@448: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@448: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@448: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@448: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@448: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@448: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@448: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@448: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@448: * POSSIBILITY OF SUCH DAMAGE. adamc@448: *) adamc@448: adamc@448: (* Remove nested function definitions *) adamc@448: adamc@448: structure Unnest :> UNNEST = struct adamc@448: adamc@448: open Elab adamc@448: adamc@448: structure E = ElabEnv adamc@448: structure U = ElabUtil adamc@448: adamc@448: structure IS = IntBinarySet adamc@448: adamc@487: fun liftExpInExp by = adamc@623: U.Exp.mapB {kind = fn _ => fn k => k, adamc@487: con = fn _ => fn c => c, adamc@487: exp = fn bound => fn e => adamc@487: case e of adamc@487: ERel xn => adamc@487: if xn < bound then adamc@487: e adamc@487: else adamc@487: ERel (xn + by) adamc@487: | _ => e, adamc@487: bind = fn (bound, U.Exp.RelE _) => bound + 1 adamc@487: | (bound, _) => bound} adamc@487: adamc@487: val subExpInExp = adamc@623: U.Exp.mapB {kind = fn _ => fn k => k, adamc@487: con = fn _ => fn c => c, adamc@487: exp = fn (xn, rep) => fn e => adamc@487: case e of adamc@487: ERel xn' => adamc@487: if xn' = xn then adamc@487: #1 rep adamc@487: else adamc@487: e adamc@487: | _ => e, adamc@487: bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, E.liftExpInExp 0 rep) adamc@487: | ((xn, rep), U.Exp.RelC _) => (xn, E.liftConInExp 0 rep) adamc@487: | (ctx, _) => ctx} adamc@487: adamc@623: val fvsCon = U.Con.foldB {kind = fn (_, _, st) => st, adamc@448: con = fn (cb, c, cvs) => adamc@448: case c of adamc@448: CRel n => adamc@448: if n >= cb then adamc@448: IS.add (cvs, n - cb) adamc@448: else adamc@448: cvs adamc@448: | _ => cvs, adamc@448: bind = fn (cb, b) => adamc@448: case b of adamc@623: U.Con.RelC _ => cb + 1 adamc@448: | _ => cb} adamc@448: 0 IS.empty adamc@448: adamc@623: fun fvsExp nr = U.Exp.foldB {kind = fn (_, _, st) => st, adamc@448: con = fn ((cb, eb), c, st as (cvs, evs)) => adamc@448: case c of adamc@448: CRel n => adamc@448: if n >= cb then adamc@448: (IS.add (cvs, n - cb), evs) adamc@448: else adamc@448: st adamc@448: | _ => st, adamc@448: exp = fn ((cb, eb), e, st as (cvs, evs)) => adamc@448: case e of adamc@448: ERel n => adamc@448: if n >= eb then adamc@448: (cvs, IS.add (evs, n - eb)) adamc@448: else adamc@448: st adamc@448: | _ => st, adamc@448: bind = fn (ctx as (cb, eb), b) => adamc@448: case b of adamc@448: U.Exp.RelC _ => (cb + 1, eb) adamc@448: | U.Exp.RelE _ => (cb, eb + 1) adamc@448: | _ => ctx} adamc@448: (0, nr) (IS.empty, IS.empty) adamc@448: adamc@448: fun positionOf (x : int) ls = adamc@448: let adamc@448: fun po n ls = adamc@448: case ls of adamc@448: [] => raise Fail "Unnest.positionOf" adamc@448: | x' :: ls' => adamc@448: if x' = x then adamc@448: n adamc@448: else adamc@448: po (n + 1) ls' adamc@448: in adamc@448: po 0 ls adamc@487: handle Fail _ => raise Fail ("Unnest.positionOf(" adamc@448: ^ Int.toString x adamc@448: ^ ", " adamc@448: ^ String.concatWith ";" (map Int.toString ls) adamc@448: ^ ")") adamc@448: end adamc@448: adamc@448: fun squishCon cfv = adamc@623: U.Con.mapB {kind = fn _ => fn k => k, adamc@448: con = fn cb => fn c => adamc@448: case c of adamc@448: CRel n => adamc@448: if n >= cb then adamc@448: CRel (positionOf (n - cb) cfv + cb) adamc@448: else adamc@448: c adamc@448: | _ => c, adamc@448: bind = fn (cb, b) => adamc@448: case b of adamc@623: U.Con.RelC _ => cb + 1 adamc@448: | _ => cb} adamc@448: 0 adamc@448: adamc@448: fun squishExp (nr, cfv, efv) = adamc@623: U.Exp.mapB {kind = fn _ => fn k => k, adamc@448: con = fn (cb, eb) => fn c => adamc@448: case c of adamc@448: CRel n => adamc@448: if n >= cb then adamc@448: CRel (positionOf (n - cb) cfv + cb) adamc@448: else adamc@448: c adamc@448: | _ => c, adamc@448: exp = fn (cb, eb) => fn e => adamc@448: case e of adamc@448: ERel n => adamc@448: if n >= eb then adamc@487: ERel (positionOf (n - eb) efv + eb - nr) adamc@448: else adamc@448: e adamc@448: | _ => e, adamc@448: bind = fn (ctx as (cb, eb), b) => adamc@448: case b of adamc@448: U.Exp.RelC _ => (cb + 1, eb) adamc@448: | U.Exp.RelE _ => (cb, eb + 1) adamc@448: | _ => ctx} adamc@448: (0, nr) adamc@448: adamc@448: type state = { adamc@448: maxName : int, adamc@455: decls : (string * int * con * exp) list adamc@448: } adamc@448: adamc@623: fun kind (_, k, st) = (k, st) adamc@448: adam@1888: val basis = ref 0 adam@1888: adamc@453: fun exp ((ks, ts), e as old, st : state) = adamc@448: case e of adamc@825: ELet (eds, e, t) => adamc@448: let adamc@487: (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*) adamc@453: adamc@487: fun doSubst' (e, subs) = foldl (fn (p, e) => subExpInExp p e) e subs adamc@448: adamc@487: fun doSubst (e, subs, by) = adamc@487: let adamc@487: val e = doSubst' (e, subs) adamc@487: in adamc@487: liftExpInExp (~by) (length subs) e adamc@487: end adamc@487: adam@1888: fun functionInside (t : con) = adam@1888: case #1 t of adam@1888: TFun _ => true adam@1888: | CApp ((CModProj (basis', [], "transaction"), _), _) => basis' = !basis adam@1888: | _ => false adam@1888: adam@1888: val eds = map (fn ed => adam@1888: case #1 ed of adam@1888: EDVal ((PVar (x, _), _), t, e) => adam@1888: if functionInside t then adam@1888: (EDValRec [(x, t, E.liftExpInExp 0 e)], #2 ed) adam@1888: else adam@1888: ed adam@1888: | _ => ed) eds adam@1888: adamc@487: val (eds, (ts, maxName, ds, subs, by)) = adamc@448: ListUtil.foldlMapConcat adamc@487: (fn (ed, (ts, maxName, ds, subs, by)) => adamc@448: case #1 ed of adamc@825: EDVal (p, t, e) => adamc@487: let adamc@487: val e = doSubst (e, subs, by) adamc@825: adamc@825: fun doVars ((p, _), ts) = adamc@825: case p of adamc@825: PWild => ts adamc@825: | PVar xt => xt :: ts adamc@825: | PPrim _ => ts adamc@825: | PCon (_, _, _, NONE) => ts adamc@825: | PCon (_, _, _, SOME p) => doVars (p, ts) adamc@825: | PRecord xpcs => adamc@825: foldl (fn ((_, p, _), ts) => doVars (p, ts)) adamc@825: ts xpcs adamc@1272: adamc@1272: fun bindOne subs = ((0, (ERel 0, #2 ed)) adamc@1272: :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs) adamc@1272: adamc@1272: fun bindMany (n, subs) = adamc@1272: case n of adamc@1272: 0 => subs adamc@1272: | _ => bindMany (n - 1, bindOne subs) adamc@487: in adamc@825: ([(EDVal (p, t, e), #2 ed)], adamc@825: (doVars (p, ts), adamc@487: maxName, ds, adamc@1272: bindMany (E.patBindsN p, subs), adamc@487: by)) adamc@487: end adamc@448: | EDValRec vis => adamc@448: let adamc@448: val loc = #2 ed adamc@448: adamc@448: val nr = length vis adamc@490: val subsLocal = List.filter (fn (_, (ERel _, _)) => false adamc@490: | _ => true) subs adamc@490: val subsLocal = map (fn (n, e) => (n + nr, liftExpInExp nr 0 e)) adamc@490: subsLocal adamc@490: adamc@490: val vis = map (fn (x, t, e) => adamc@490: (x, t, doSubst' (e, subsLocal))) vis adamc@490: adamc@448: val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) => adamc@448: let adamc@448: val (cfv', efv') = fvsExp nr e adamc@448: (*val () = Print.prefaces "fvsExp" adamc@448: [("e", ElabPrint.p_exp E.empty e), adamc@448: ("cfv", Print.PD.string adamc@448: (Int.toString (IS.numItems cfv'))), adamc@448: ("efv", Print.PD.string adamc@448: (Int.toString (IS.numItems efv')))]*) adamc@448: val cfv'' = fvsCon t adamc@448: in adamc@448: (IS.union (cfv, IS.union (cfv', cfv'')), adamc@448: IS.union (efv, efv')) adamc@448: end) adamc@448: (IS.empty, IS.empty) vis adamc@448: adamc@826: (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*) adamc@826: (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*) adamc@826: (*val () = app (fn (x, t) => adamc@453: Print.prefaces "Var" [("x", Print.PD.string x), adamc@826: ("t", ElabPrint.p_con E.empty t)]) ts adamc@826: val () = IS.app (fn n => print ("Free: " ^ Int.toString n ^ "\n")) efv*) adamc@487: adamc@448: val cfv = IS.foldl (fn (x, cfv) => adamc@448: let adamc@448: (*val () = print (Int.toString x ^ "\n")*) adamc@448: val (_, t) = List.nth (ts, x) adamc@448: in adamc@448: IS.union (cfv, fvsCon t) adamc@448: end) adamc@448: cfv efv adamc@448: (*val () = print "B\n"*) adamc@448: adamc@448: val (vis, maxName) = adamc@448: ListUtil.foldlMap (fn ((x, t, e), maxName) => adamc@448: ((x, maxName, t, e), adamc@448: maxName + 1)) adamc@448: maxName vis adamc@448: adamc@487: val subs = map (fn (n, e) => (n + nr, adamc@487: case e of adamc@487: (ERel _, _) => e adamc@487: | _ => liftExpInExp nr 0 e)) adamc@487: subs adamc@487: adamc@448: val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) => adamc@448: let adamc@487: val e = (ENamed n, loc) adamc@487: adamc@487: val e = IS.foldr (fn (x, e) => adamc@487: (ECApp (e, (CRel x, loc)), loc)) adamc@487: e cfv adamc@487: adamc@487: val e = IS.foldr (fn (x, e) => adamc@487: (EApp (e, (ERel (nr + x), loc)), adamc@487: loc)) adamc@487: e efv adamc@448: in adamc@487: (nr - i - 1, e) adamc@448: end) adamc@450: vis adamc@450: adamc@448: val cfv = IS.listItems cfv adamc@448: val efv = IS.listItems efv adamc@448: adamc@487: val subs = subs' @ subs adamc@448: adamc@448: val vis = map (fn (x, n, t, e) => adamc@448: let adamc@448: (*val () = Print.prefaces "preSubst" adamc@448: [("e", ElabPrint.p_exp E.empty e)]*) adamc@490: val e = doSubst' (e, subs') adamc@448: adamc@448: (*val () = Print.prefaces "squishCon" adamc@448: [("t", ElabPrint.p_con E.empty t)]*) adamc@448: val t = squishCon cfv t adamc@448: (*val () = Print.prefaces "squishExp" adamc@448: [("e", ElabPrint.p_exp E.empty e)]*) adamc@487: val e = squishExp (nr, cfv, efv) e adamc@448: adamc@487: (*val () = print ("Avail: " ^ Int.toString (length ts) ^ "\n")*) adamc@453: val (e, t) = foldl (fn (ex, (e, t)) => adamc@448: let adamc@487: (*val () = print (Int.toString ex ^ "\n")*) adamc@448: val (name, t') = List.nth (ts, ex) adamc@1272: val t' = squishCon cfv t' adamc@448: in adamc@448: ((EAbs (name, adamc@448: t', adamc@448: t, adamc@448: e), loc), adamc@448: (TFun (t', adamc@448: t), loc)) adamc@448: end) adamc@448: (e, t) efv adamc@487: (*val () = print "Done\n"*) adamc@448: adamc@453: val (e, t) = foldl (fn (cx, (e, t)) => adamc@448: let adamc@448: val (name, k) = List.nth (ks, cx) adamc@448: in adamc@448: ((ECAbs (Explicit, adamc@448: name, adamc@448: k, adamc@448: e), loc), adamc@448: (TCFun (Explicit, adamc@448: name, adamc@448: k, adamc@448: t), loc)) adamc@448: end) adamc@448: (e, t) cfv adamc@448: in adamc@487: (*Print.prefaces "Have a vi" adamc@487: [("x", Print.PD.string x), adamc@487: ("e", ElabPrint.p_exp ElabEnv.empty e)];*) adamc@1017: ("$" ^ x, n, t, e) adamc@448: end) adamc@448: vis adamc@448: adamc@487: val ts = List.revAppend (map (fn (x, _, t, _) => (x, t)) vis, ts) adamc@448: in adamc@487: ([], (ts, maxName, vis @ ds, subs, by + nr)) adamc@448: end) adamc@487: (ts, #maxName st, #decls st, [], 0) eds adamc@487: adamc@487: val e' = doSubst (e, subs, by) adamc@448: in adamc@487: (*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e), adamc@487: ("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))), adamc@487: ("e'", ElabPrint.p_exp ElabEnv.empty e')];*) adamc@1272: (*Print.prefaces "Let" [("Before", ElabPrint.p_exp ElabEnv.empty (old, ErrorMsg.dummySpan)), adamc@1272: ("After", ElabPrint.p_exp ElabEnv.empty (ELet (eds, e', t), ErrorMsg.dummySpan))];*) adamc@825: (ELet (eds, e', t), adamc@448: {maxName = maxName, adamc@448: decls = ds}) adamc@487: (*(ELet (eds, doSubst (liftExpInExp (~(length subs - numRemaining)) (length subs) e) subs),*) adamc@448: end adamc@448: adamc@448: | _ => (e, st) adamc@448: adamc@448: fun default (ctx, d, st) = (d, st) adamc@448: adamc@448: fun bind ((ks, ts), b) = adamc@448: case b of adamc@448: U.Decl.RelC p => (p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts) adamc@448: | U.Decl.RelE p => (ks, p :: ts) adamc@448: | _ => (ks, ts) adamc@448: adamc@448: val unnestDecl = U.Decl.foldMapB {kind = kind, adamc@448: con = default, adamc@448: exp = exp, adamc@448: sgn_item = default, adamc@448: sgn = default, adamc@448: str = default, adamc@448: decl = default, adamc@448: bind = bind} adamc@448: ([], []) adamc@448: adamc@448: fun unnest file = adamc@448: let adamc@448: fun doDecl (all as (d, loc), st : state) = adamc@448: let adamc@448: fun default () = ([all], st) adamc@448: fun explore () = adamc@448: let adamc@448: val (d, st) = unnestDecl st all adamc@455: adamc@455: val ds = adamc@455: case #1 d of adamc@455: DValRec vis => [(DValRec (vis @ #decls st), #2 d)] adamc@455: | _ => [(DValRec (#decls st), #2 d), d] adamc@448: in adamc@455: (ds, adamc@448: {maxName = #maxName st, adamc@448: decls = []}) adamc@448: end adamc@448: in adamc@448: case d of adamc@448: DCon _ => default () adamc@448: | DDatatype _ => default () adamc@448: | DDatatypeImp _ => default () adamc@448: | DVal _ => explore () adamc@448: | DValRec _ => explore () adamc@448: | DSgn _ => default () adamc@448: | DStr (x, n, sgn, str) => adamc@448: let adamc@448: val (str, st) = doStr (str, st) adamc@448: in adamc@448: ([(DStr (x, n, sgn, str), loc)], st) adamc@448: end adam@1888: | DFfiStr ("Basis", n, _) => (basis := n; default ()) adamc@448: | DFfiStr _ => default () adamc@448: | DConstraint _ => default () adamc@448: | DExport _ => default () adamc@448: | DTable _ => default () adamc@448: | DSequence _ => default () adamc@754: | DView _ => default () adamc@448: | DDatabase _ => default () adamc@459: | DCookie _ => default () adamc@718: | DStyle _ => default () adamc@1075: | DTask _ => explore () adamc@1199: | DPolicy _ => explore () adam@1294: | DOnError _ => default () adamc@448: end adamc@448: adamc@448: and doStr (all as (str, loc), st) = adamc@448: let adamc@448: fun default () = (all, st) adamc@448: in adamc@448: case str of adamc@448: StrConst ds => adamc@448: let adamc@448: val (ds, st) = ListUtil.foldlMapConcat doDecl st ds adamc@448: in adamc@448: ((StrConst ds, loc), st) adamc@448: end adamc@448: | StrVar _ => default () adamc@448: | StrProj _ => default () adamc@448: | StrFun (x, n, dom, ran, str) => adamc@448: let adamc@448: val (str, st) = doStr (str, st) adamc@448: in adamc@448: ((StrFun (x, n, dom, ran, str), loc), st) adamc@448: end adamc@448: | StrApp _ => default () adamc@448: | StrError => raise Fail "Unnest: StrError" adamc@448: end adamc@448: adamc@448: val (ds, _) = ListUtil.foldlMapConcat doDecl adamc@448: {maxName = U.File.maxName file + 1, adamc@448: decls = []} file adamc@448: in adamc@448: ds adamc@448: end adamc@448: adamc@448: end