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