adamc@1276: (* Copyright (c) 2008-2010, Adam Chlipala
adamc@193:  * All rights reserved.
adamc@193:  *
adamc@193:  * Redistribution and use in source and binary forms, with or without
adamc@193:  * modification, are permitted provided that the following conditions are met:
adamc@193:  *
adamc@193:  * - Redistributions of source code must retain the above copyright notice,
adamc@193:  *   this list of conditions and the following disclaimer.
adamc@193:  * - Redistributions in binary form must reproduce the above copyright notice,
adamc@193:  *   this list of conditions and the following disclaimer in the documentation
adamc@193:  *   and/or other materials provided with the distribution.
adamc@193:  * - The names of contributors may not be used to endorse or promote products
adamc@193:  *   derived from this software without specific prior written permission.
adamc@193:  *
adamc@193:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@193:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@193:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@193:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@193:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adamc@193:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@193:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@193:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@193:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@193:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@193:  * POSSIBILITY OF SUCH DAMAGE.
adamc@193:  *)
adamc@193: 
adamc@315: (* Simplify a Core program by repeating polymorphic definitions of datatypes *)
adamc@193: 
adamc@193: structure Specialize :> SPECIALIZE = struct
adamc@193: 
adamc@193: open Core
adamc@193: 
adamc@193: structure E = CoreEnv
adamc@193: structure U = CoreUtil
adamc@193: 
adamc@193: val liftConInCon = E.liftConInCon
adamc@193: val subConInCon = E.subConInCon
adamc@193: 
adamc@193: structure CK = struct
adamc@193: type ord_key = con list
adamc@193: val compare = Order.joinL U.Con.compare
adamc@193: end
adamc@193: 
adamc@193: structure CM = BinaryMapFn(CK)
adamc@193: structure IM = IntBinaryMap
adamc@193: 
adamc@193: type datatyp' = {
adamc@193:      name : int,
adamc@193:      constructors : int IM.map
adamc@193: }
adamc@193: 
adamc@193: type datatyp = {
adamc@193:      name : string,
adamc@193:      params : int,
adamc@193:      constructors : (string * int * con option) list,
adamc@193:      specializations : datatyp' CM.map
adamc@193: }
adamc@193: 
adamc@193: type state = {
adamc@193:      count : int,
adamc@193:      datatypes : datatyp IM.map,
adamc@193:      constructors : int IM.map,
adamc@846:      decls : (string * int * string list * (string * int * con option) list) list     
adamc@193: }
adamc@193: 
adamc@193: fun kind (k, st) = (k, st)
adamc@193: 
adamc@193: val isOpen = U.Con.exists {kind = fn _ => false,
adamc@193:                            con = fn c =>
adamc@193:                                     case c of
adamc@193:                                         CRel _ => true
adamc@193:                                       | _ => false}
adamc@193: 
adamc@193: fun considerSpecialization (st : state, n, args, dt : datatyp) =
adamc@1276:     let
adamc@1276:         val args = map ReduceLocal.reduceCon args
adamc@1276:     in
adamc@1276:         case CM.find (#specializations dt, args) of
adamc@1276:             SOME dt' => (#name dt', #constructors dt', st)
adamc@1276:           | NONE =>
adamc@1276:             let
adamc@1276:                 (*val () = Print.prefaces "Args" [("n", Print.PD.string (Int.toString n)),
adamc@1276:                                                 ("args", Print.p_list (CorePrint.p_con CoreEnv.empty) args)]*)
adamc@194: 
adamc@1276:                 val n' = #count st
adamc@193: 
adamc@1276:                 val nxs = length args - 1
adamc@1276:                 fun sub t = ListUtil.foldli (fn (i, arg, t) =>
adamc@1276:                                                 subConInCon (nxs - i, arg) t) t args
adamc@193: 
adamc@1276:                 val (cons, (count, cmap)) =
adamc@1276:                     ListUtil.foldlMap (fn ((x, n, to), (count, cmap)) =>
adamc@1276:                                           let
adamc@1276:                                               val to = Option.map sub to
adamc@1276:                                           in
adamc@1276:                                               ((x, count, to),
adamc@1276:                                                (count + 1,
adamc@1276:                                                 IM.insert (cmap, n, count)))
adamc@1276:                                           end) (n' + 1, IM.empty) (#constructors dt)
adamc@193: 
adamc@1276:                 val st = {count = count,
adamc@1276:                           datatypes = IM.insert (#datatypes st, n,
adamc@1276:                                                  {name = #name dt,
adamc@1276:                                                   params = #params dt,
adamc@1276:                                                   constructors = #constructors dt,
adamc@1276:                                                   specializations = CM.insert (#specializations dt,
adamc@1276:                                                                                args,
adamc@1276:                                                                                {name = n',
adamc@1276:                                                                                 constructors = cmap})}),
adamc@1276:                           constructors = #constructors st,
adamc@1276:                           decls = #decls st}
adamc@193: 
adamc@1276:                 val (cons, st) = ListUtil.foldlMap (fn ((x, n, NONE), st) => ((x, n, NONE), st)
adamc@1276:                                                      | ((x, n, SOME t), st) =>
adamc@1276:                                                        let
adamc@1276:                                                            val (t, st) = specCon st t
adamc@1276:                                                        in
adamc@1276:                                                            ((x, n, SOME t), st)
adamc@1276:                                                        end) st cons
adamc@193: 
adamc@1276:                 val dt = (#name dt ^ "_s",
adamc@1276:                           n',
adamc@1276:                           [],
adamc@1276:                           cons)
adamc@1276:             in
adamc@1276:                 (n', cmap, {count = #count st,
adamc@1276:                             datatypes = #datatypes st,
adamc@1276:                             constructors = #constructors st,
adamc@1276:                             decls = dt :: #decls st})
adamc@1276:             end
adamc@1276:     end
adamc@193: 
adamc@193: and con (c, st : state) =
adamc@193:     let
adamc@193:         fun findApp (c, args) =
adamc@193:             case c of
adamc@193:                 CApp ((c', _), arg) => findApp (c', arg :: args)
adamc@193:               | CNamed n => SOME (n, args)
adamc@193:               | _ => NONE
adamc@193:     in
adamc@193:         case findApp (c, []) of
adamc@193:             SOME (n, args as (_ :: _)) =>
adamc@193:             if List.exists isOpen args then
adamc@193:                 (c, st)
adamc@193:             else
adamc@193:                 (case IM.find (#datatypes st, n) of
adamc@193:                      NONE => (c, st)
adamc@193:                    | SOME dt =>
adamc@193:                      if length args <> #params dt then
adamc@193:                          (c, st)
adamc@193:                      else
adamc@193:                          let
adamc@193:                              val (n, _, st) = considerSpecialization (st, n, args, dt)
adamc@193:                          in
adamc@193:                              (CNamed n, st)
adamc@193:                          end)
adamc@193:           | _ => (c, st)
adamc@193:     end
adamc@193: 
adamc@193: and specCon st = U.Con.foldMap {kind = kind, con = con} st
adamc@193: 
adamc@193: fun pat (p, st) =
adamc@193:     case #1 p of
adamc@193:         PWild => (p, st)
adamc@193:       | PVar _ => (p, st)
adamc@193:       | PPrim _ => (p, st)
adamc@193:       | PCon (dk, PConVar pn, args as (_ :: _), po) =>
adamc@193:         let
adamc@193:             val (po, st) =
adamc@193:                 case po of
adamc@193:                     NONE => (NONE, st)
adamc@193:                   | SOME p =>
adamc@193:                     let
adamc@193:                         val (p, st) = pat (p, st)
adamc@193:                     in
adamc@193:                         (SOME p, st)
adamc@193:                     end
adamc@193:             val p = (PCon (dk, PConVar pn, args, po), #2 p)
adamc@193:         in
adamc@193:             if List.exists isOpen args then
adamc@193:                 (p, st)
adamc@193:             else
adamc@193:                 case IM.find (#constructors st, pn) of
adamc@193:                     NONE => (p, st)
adamc@193:                   | SOME n =>
adamc@193:                     case IM.find (#datatypes st, n) of
adamc@193:                         NONE => (p, st)
adamc@193:                       | SOME dt =>
adamc@193:                         let
adamc@193:                             val (n, cmap, st) = considerSpecialization (st, n, args, dt)
adamc@193:                         in
adamc@193:                             case IM.find (cmap, pn) of
adamc@193:                                 NONE => raise Fail "Specialize: Missing datatype constructor (pat)"
adamc@193:                               | SOME pn' => ((PCon (dk, PConVar pn', [], po), #2 p), st)
adamc@193:                         end
adamc@193:         end
adamc@851:       | PCon (dk, pc, args, SOME p') =>
adamc@851:         let
adamc@851:             val (p', st) = pat (p', st)
adamc@851:         in
adamc@851:             ((PCon (dk, pc, args, SOME p'), #2 p), st)
adamc@851:         end
adamc@193:       | PCon _ => (p, st)
adamc@193:       | PRecord xps =>
adamc@193:         let
adamc@193:             val (xps, st) = ListUtil.foldlMap (fn ((x, p, t), st) =>
adamc@193:                                                   let
adamc@193:                                                       val (p, st) = pat (p, st)
adamc@193:                                                   in
adamc@193:                                                       ((x, p, t), st)
adamc@193:                                                   end)
adamc@193:                             st xps
adamc@193:         in
adamc@193:             ((PRecord xps, #2 p), st)
adamc@193:         end
adamc@193: 
adamc@193: fun exp (e, st) =
adamc@193:     case e of
adamc@193:         ECon (dk, PConVar pn, args as (_ :: _), eo) =>
adamc@193:         if List.exists isOpen args then
adamc@193:             (e, st)
adamc@193:         else
adamc@193:             (case IM.find (#constructors st, pn) of
adamc@193:                  NONE => (e, st)
adamc@193:                | SOME n =>
adamc@193:                  case IM.find (#datatypes st, n) of
adamc@193:                      NONE => (e, st)
adamc@193:                    | SOME dt =>
adamc@193:                      let
adamc@193:                          val (n, cmap, st) = considerSpecialization (st, n, args, dt)
adamc@193:                      in
adamc@193:                          case IM.find (cmap, pn) of
adamc@193:                              NONE => raise Fail "Specialize: Missing datatype constructor"
adamc@193:                            | SOME pn' => (ECon (dk, PConVar pn', [], eo), st)
adamc@193:                      end)
adamc@193:       | ECase (e, pes, r) =>
adamc@193:         let
adamc@193:             val (pes, st) = ListUtil.foldlMap (fn ((p, e), st) =>
adamc@193:                                                   let
adamc@193:                                                       val (p, st) = pat (p, st)
adamc@193:                                                   in
adamc@193:                                                       ((p, e), st)
adamc@193:                                                   end) st pes
adamc@193:         in
adamc@193:             (ECase (e, pes, r), st)
adamc@193:         end
adamc@193:       | _ => (e, st)
adamc@193: 
adamc@193: fun decl (d, st) = (d, st)
adamc@193: 
adamc@193: val specDecl = U.Decl.foldMap {kind = kind, con = con, exp = exp, decl = decl}
adamc@193: 
adamc@193: fun specialize file =
adamc@193:     let
adamc@792:         fun doDecl (d, st) =
adamc@194:             let
adamc@194:                 (*val () = Print.preface ("decl:", CorePrint.p_decl CoreEnv.empty all)*)
adamc@792:                 val (d, st) = specDecl st d
adamc@194:             in
adamc@792:                 case #1 d of
adamc@846:                     DDatatype dts =>
adamc@847:                     ((case #decls st of
adamc@847:                           [] => [d]
adamc@847:                         | dts' => [(DDatatype (dts' @ dts), #2 d)]),
adamc@792:                      {count = #count st,
adamc@846:                       datatypes = foldl (fn ((x, n, xs, xnts), dts) =>
adamc@846:                                             IM.insert (dts, n,
adamc@846:                                                        {name = x,
adamc@846:                                                         params = length xs,
adamc@846:                                                         constructors = xnts,
adamc@846:                                                         specializations = CM.empty}))
adamc@846:                                         (#datatypes st) dts,
adamc@846:                       constructors = foldl (fn ((x, n, xs, xnts), cs) =>
adamc@846:                                                foldl (fn ((_, n', _), constructors) =>
adamc@846:                                                          IM.insert (constructors, n', n))
adamc@846:                                                      cs xnts)
adamc@846:                                            (#constructors st) dts,
adamc@792:                       decls = []})
adamc@194:                   | _ =>
adamc@847:                     (case #decls st of
adamc@847:                           [] => [d]
adamc@847:                         | dts => [(DDatatype dts, #2 d), d],
adamc@792:                      {count = #count st,
adamc@792:                       datatypes = #datatypes st,
adamc@792:                       constructors = #constructors st,
adamc@792:                       decls = []})
adamc@194:             end
adamc@193: 
adamc@193:         val (ds, _) = ListUtil.foldlMapConcat doDecl
adamc@193:                       {count = U.File.maxName file + 1,
adamc@193:                        datatypes = IM.empty,
adamc@193:                        constructors = IM.empty,
adamc@193:                        decls = []} file
adamc@193:     in
adamc@193:         ds
adamc@193:     end
adamc@193: 
adamc@193: end