adamc@315: (* Copyright (c) 2008, Adam Chlipala
adamc@315:  * All rights reserved.
adamc@315:  *
adamc@315:  * Redistribution and use in source and binary forms, with or without
adamc@315:  * modification, are permitted provided that the following conditions are met:
adamc@315:  *
adamc@315:  * - Redistributions of source code must retain the above copyright notice,
adamc@315:  *   this list of conditions and the following disclaimer.
adamc@315:  * - Redistributions in binary form must reproduce the above copyright notice,
adamc@315:  *   this list of conditions and the following disclaimer in the documentation
adamc@315:  *   and/or other materials provided with the distribution.
adamc@315:  * - The names of contributors may not be used to endorse or promote products
adamc@315:  *   derived from this software without specific prior written permission.
adamc@315:  *
adamc@315:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@315:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@315:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@315:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@315:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adamc@315:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@315:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@315:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@315:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@315:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@315:  * POSSIBILITY OF SUCH DAMAGE.
adamc@315:  *)
adamc@315: 
adamc@315: (* Simplify a Core program by repeating polymorphic function definitions *)
adamc@315: 
adamc@315: structure Unpoly :> UNPOLY = struct
adamc@315: 
adamc@315: open Core
adamc@315: 
adamc@315: structure E = CoreEnv
adamc@315: structure U = CoreUtil
adamc@315: 
adamc@315: structure IS = IntBinarySet
adamc@315: structure IM = IntBinaryMap
adamc@315: 
adamc@315: 
adamc@315: (** The actual specialization *)
adamc@315: 
adamc@315: val liftConInCon = E.liftConInCon
adamc@315: val subConInCon = E.subConInCon
adamc@315: 
adamc@315: val liftConInExp = E.liftConInExp
adamc@315: val subConInExp = E.subConInExp
adamc@315: 
adamc@316: fun unpolyNamed (xn, rep) =
adamc@316:     U.Exp.map {kind = fn k => k,
adamc@316:                con = fn c => c,
adamc@316:                exp = fn e =>
adamc@316:                         case e of
adamc@316:                             ENamed xn' =>
adamc@316:                             if xn' = xn then
adamc@316:                                 rep
adamc@316:                             else
adamc@316:                                 e
adamc@325:                           | ECApp (e', _) =>
adamc@325:                             let
adamc@325:                                 fun isTheOne (e, _) =
adamc@325:                                     case e of
adamc@325:                                         ENamed xn' => xn' = xn
adamc@325:                                       | ECApp (e, _) => isTheOne e
adamc@325:                                       | _ => false
adamc@325:                             in
adamc@325:                                 if isTheOne e' then
adamc@325:                                     #1 e'
adamc@325:                                 else
adamc@325:                                     e
adamc@325:                             end
adamc@316:                           | _ => e}
adamc@316: 
adamc@315: type state = {
adamc@315:      funcs : (kind list * (string * int * con * exp * string) list) IM.map,
adamc@315:      decls : decl list,
adamc@315:      nextName : int
adamc@315: }
adamc@315: 
adamc@315: fun kind (k, st) = (k, st)
adamc@315: 
adamc@315: fun con (c, st) = (c, st)
adamc@315: 
adamc@315: fun exp (e, st : state) =
adamc@315:     case e of
adamc@315:         ECApp _ =>
adamc@315:         let
adamc@315:             (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty (e, ErrorMsg.dummySpan))]*)
adamc@315: 
adamc@315:             fun unravel (e, cargs) =
adamc@315:                 case e of
adamc@315:                     ECApp ((e, _), c) => unravel (e, c :: cargs)
adamc@315:                   | ENamed n => SOME (n, rev cargs)
adamc@315:                   | _ => NONE
adamc@315:         in
adamc@315:             case unravel (e, []) of
adamc@315:                 NONE => (e, st)
adamc@315:               | SOME (n, cargs) =>
adamc@315:                 case IM.find (#funcs st, n) of
adamc@315:                     NONE => (e, st)
adamc@315:                   | SOME (ks, vis) =>
adamc@315:                     let
adamc@315:                         val (vis, nextName) = ListUtil.foldlMap
adamc@315:                                              (fn ((x, n, t, e, s), nextName) =>
adamc@315:                                                  ((x, nextName, n, t, e, s), nextName + 1))
adamc@315:                                              (#nextName st) vis
adamc@315: 
adamc@315:                         fun specialize (x, n, n_old, t, e, s) =
adamc@315:                             let
adamc@315:                                 fun trim (t, e, cargs) =
adamc@315:                                     case (t, e, cargs) of
adamc@315:                                         ((TCFun (_, _, t), _),
adamc@315:                                          (ECAbs (_, _, e), _),
adamc@315:                                          carg :: cargs) =>
adamc@315:                                         let
adamc@315:                                             val t = subConInCon (length cargs, carg) t
adamc@315:                                             val e = subConInExp (length cargs, carg) e
adamc@315:                                         in
adamc@315:                                             trim (t, e, cargs)
adamc@315:                                         end
adamc@316:                                       | (_, _, []) =>
adamc@316:                                         let
adamc@316:                                             val e = foldl (fn ((_, n, n_old, _, _, _), e) =>
adamc@316:                                                               unpolyNamed (n_old, ENamed n) e)
adamc@325:                                                           e vis
adamc@316:                                         in
adamc@316:                                             SOME (t, e)
adamc@316:                                         end
adamc@315:                                       | _ => NONE
adamc@315:                             in
adamc@315:                                 (*Print.prefaces "specialize"
adamc@315:                                                [("t", CorePrint.p_con CoreEnv.empty t),
adamc@315:                                                 ("e", CorePrint.p_exp CoreEnv.empty e),
adamc@315:                                                 ("|cargs|", Print.PD.string (Int.toString (length cargs)))];*)
adamc@315:                                 Option.map (fn (t, e) => (x, n, n_old, t, e, s))
adamc@315:                                 (trim (t, e, cargs))
adamc@315:                             end
adamc@315: 
adamc@315:                         val vis = List.map specialize vis
adamc@315:                     in
adamc@316:                         if List.exists (not o Option.isSome) vis orelse length cargs > length ks then
adamc@315:                             (e, st)
adamc@315:                         else
adamc@315:                             let
adamc@315:                                 val vis = List.mapPartial (fn x => x) vis
adamc@316:                                 val vis = map (fn (x, n, n_old, t, e, s) =>
adamc@316:                                                    (x ^ "_unpoly", n, n_old, t, e, s)) vis
adamc@315:                                 val vis' = map (fn (x, n, _, t, e, s) =>
adamc@316:                                                    (x, n, t, e, s)) vis
adamc@316: 
adamc@316:                                 val ks' = List.drop (ks, length cargs)
adamc@315:                             in
adamc@315:                                 case List.find (fn (_, _, n_old, _, _, _) => n_old = n) vis of
adamc@315:                                     NONE => raise Fail "Unpoly: Inconsistent 'val rec' record"
adamc@315:                                   | SOME (_, n, _, _, _, _) =>
adamc@315:                                     (ENamed n,
adamc@316:                                      {funcs = foldl (fn (vi, funcs) =>
adamc@316:                                                         IM.insert (funcs, #2 vi, (ks', vis')))
adamc@316:                                                     (#funcs st) vis',
adamc@315:                                       decls = (DValRec vis', ErrorMsg.dummySpan) :: #decls st,
adamc@315:                                       nextName = nextName})
adamc@315:                             end
adamc@315:                     end
adamc@315:         end
adamc@315:       | _ => (e, st)
adamc@315: 
adamc@315: fun decl (d, st : state) =
adamc@315:     case d of
adamc@315:         DValRec (vis as ((x, n, t, e, s) :: rest)) =>
adamc@315:         let
adamc@315:             fun unravel (e, cargs) =
adamc@315:                 case e of
adamc@315:                     (ECAbs (_, k, e), _) =>
adamc@315:                     unravel (e, k :: cargs)
adamc@315:                   | _ => rev cargs
adamc@315: 
adamc@315:             val cargs = unravel (e, [])
adamc@315: 
adamc@315:             fun unravel (e, cargs) =
adamc@315:                 case (e, cargs) of
adamc@315:                     ((ECAbs (_, k, e), _), k' :: cargs) =>
adamc@315:                     U.Kind.compare (k, k') = EQUAL
adamc@315:                     andalso unravel (e, cargs)
adamc@315:                   | (_, []) => true
adamc@315:                   | _ => false
adamc@315:         in
adamc@315:             if List.exists (fn vi => not (unravel (#4 vi, cargs))) rest then
adamc@315:                 (d, st)
adamc@315:             else
adamc@315:                 let
adamc@315:                     val ns = IS.addList (IS.empty, map #2 vis)
adamc@315:                     val nargs = length cargs
adamc@315: 
adamc@315:                     fun deAbs (e, cargs) =
adamc@315:                         case (e, cargs) of
adamc@315:                             ((ECAbs (_, _, e), _), _ :: cargs) => deAbs (e, cargs)
adamc@315:                           | (_, []) => e
adamc@315:                           | _ => raise Fail "Unpoly: deAbs"
adamc@315: 
adamc@315:                     (** Verifying lack of polymorphic recursion *)
adamc@315: 
adamc@315:                     fun kind _ = false
adamc@315:                     fun con _ = false
adamc@315: 
adamc@315:                     fun exp e =
adamc@315:                         case e of
adamc@315:                             ECApp (e, c) =>
adamc@315:                             let
adamc@315:                                 fun isIrregular (e, pos) =
adamc@315:                                     case #1 e of
adamc@315:                                         ENamed n =>
adamc@315:                                         IS.member (ns, n)
adamc@315:                                         andalso
adamc@315:                                         (case #1 c of
adamc@315:                                              CRel i => i <> nargs - pos
adamc@315:                                            | _ => true)
adamc@315:                                       | ECApp (e, _) => isIrregular (e, pos + 1)
adamc@315:                                       | _ => false
adamc@315:                             in
adamc@315:                                 isIrregular (e, 1)
adamc@315:                             end
adamc@315:                           | ECAbs _ => true
adamc@315:                           | _ => false
adamc@315: 
adamc@315:                     val irregular = U.Exp.exists {kind = kind, con = con, exp = exp}
adamc@315:                 in
adamc@315:                     if List.exists (fn x => irregular (deAbs (#4 x, cargs))) vis then
adamc@315:                         (d, st)
adamc@315:                     else
adamc@315:                         (d, {funcs = foldl (fn (vi, funcs) =>
adamc@315:                                                IM.insert (funcs, #2 vi, (cargs, vis)))
adamc@315:                                            (#funcs st) vis,
adamc@315:                              decls = #decls st,
adamc@315:                              nextName = #nextName st})
adamc@315:                 end
adamc@315:         end
adamc@315: 
adamc@315:       | _ => (d, st)
adamc@315: 
adamc@315: val polyDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
adamc@315: 
adamc@315: fun unpoly file =
adamc@315:     let
adamc@315:         fun doDecl (d : decl, st : state) =
adamc@315:             let
adamc@315:                 val (d, st) = polyDecl st d
adamc@315:             in
adamc@315:                 (rev (d :: #decls st),
adamc@315:                  {funcs = #funcs st,
adamc@315:                   decls = [],
adamc@315:                   nextName = #nextName st})
adamc@315:             end
adamc@315: 
adamc@315:         val (ds, _) = ListUtil.foldlMapConcat doDecl
adamc@315:                       {funcs = IM.empty,
adamc@315:                        decls = [],
adamc@315:                        nextName = U.File.maxName file + 1} file
adamc@315:     in
adamc@315:         ds
adamc@315:     end
adamc@315: 
adamc@315: end