adamc@20: (* Copyright (c) 2008, Adam Chlipala
adamc@20:  * All rights reserved.
adamc@20:  *
adamc@20:  * Redistribution and use in source and binary forms, with or without
adamc@20:  * modification, are permitted provided that the following conditions are met:
adamc@20:  *
adamc@20:  * - Redistributions of source code must retain the above copyright notice,
adamc@20:  *   this list of conditions and the following disclaimer.
adamc@20:  * - Redistributions in binary form must reproduce the above copyright notice,
adamc@20:  *   this list of conditions and the following disclaimer in the documentation
adamc@20:  *   and/or other materials provided with the distribution.
adamc@20:  * - The names of contributors may not be used to endorse or promote products
adamc@20:  *   derived from this software without specific prior written permission.
adamc@20:  *
adamc@20:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@20:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@20:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@20:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@20:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adamc@20:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@20:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@20:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@20:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@20:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@20:  * POSSIBILITY OF SUCH DAMAGE.
adamc@20:  *)
adamc@20: 
adamc@20: (* Simplify a Core program algebraically *)
adamc@20: 
adamc@20: structure Reduce :> REDUCE = struct
adamc@20: 
adamc@20: open Core
adamc@20: 
adamc@508: structure IM = IntBinaryMap
adamc@20: 
adamc@508: datatype env_item =
adamc@508:          UnknownC
adamc@508:        | KnownC of con
adamc@21: 
adamc@508:        | UnknownE
adamc@508:        | KnownE of exp
adamc@20: 
adamc@508:        | Lift of int * int
adamc@20: 
adamc@508: type env = env_item list
adamc@20: 
adamc@508: fun conAndExp (namedC, namedE) =
adamc@508:     let
adamc@508:         fun con env (all as (c, loc)) =
adamc@508:             case c of
adamc@508:                 TFun (c1, c2) => (TFun (con env c1, con env c2), loc)
adamc@508:               | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc)
adamc@508:               | TRecord c => (TRecord (con env c), loc)
adamc@215: 
adamc@508:               | CRel n =>
adamc@508:                 let
adamc@508:                     fun find (n', env, lift) =
adamc@508:                         if n' = 0 then
adamc@508:                             case env of
adamc@508:                                 UnknownC :: _ => (CRel (n + lift), loc)
adamc@508:                               | KnownC c :: _ => con (Lift (lift, 0) :: env) c
adamc@508:                               | _ => raise Fail "Reduce.con: CRel [1]"
adamc@508:                         else
adamc@508:                             case env of
adamc@508:                                 UnknownC :: rest => find (n' - 1, rest, lift + 1)
adamc@508:                               | KnownC _ :: rest => find (n' - 1, rest, lift)
adamc@508:                               | UnknownE :: rest => find (n' - 1, rest, lift)
adamc@508:                               | KnownE _ :: rest => find (n' - 1, rest, lift)
adamc@508:                               | Lift (lift', _) :: rest => find (n' - 1, rest, lift + lift')
adamc@508:                               | [] => raise Fail "Reduce.con: CRel [2]"
adamc@508:                 in
adamc@508:                     find (n, env, 0)
adamc@508:                 end
adamc@508:               | CNamed n =>
adamc@508:                 (case IM.find (namedC, n) of
adamc@508:                      NONE => all
adamc@508:                    | SOME c => c)
adamc@508:               | CFfi _ => all
adamc@508:               | CApp (c1, c2) =>
adamc@508:                 let
adamc@508:                     val c1 = con env c1
adamc@508:                     val c2 = con env c2
adamc@508:                 in
adamc@508:                     case #1 c1 of
adamc@508:                         CAbs (_, _, b) =>
adamc@508:                         con (KnownC c2 :: env) b
adamc@215: 
adamc@508:                       | CApp ((CApp (fold as (CFold _, _), f), _), i) =>
adamc@508:                         (case #1 c2 of
adamc@508:                              CRecord (_, []) => i
adamc@508:                            | CRecord (k, (x, c) :: rest) =>
adamc@508:                              con env (CApp ((CApp ((CApp (f, x), loc), c), loc),
adamc@508:                                             (CApp ((CApp ((CApp (fold, f), loc), i), loc),
adamc@508:                                                    (CRecord (k, rest), loc)), loc)), loc)
adamc@508:                            | _ => (CApp (c1, c2), loc))                           
adamc@20: 
adamc@508:                       | _ => (CApp (c1, c2), loc)
adamc@508:                 end
adamc@508:               | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc)
adamc@20: 
adamc@508:               | CName _ => all
adamc@21: 
adamc@508:               | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc)
adamc@508:               | CConcat (c1, c2) =>
adamc@508:                 let
adamc@508:                     val c1 = con env c1
adamc@508:                     val c2 = con env c2
adamc@508:                 in
adamc@508:                     case (#1 c1, #1 c2) of
adamc@508:                         (CRecord (k, xcs1), CRecord (_, xcs2)) =>
adamc@508:                         (CRecord (k, xcs1 @ xcs2), loc)
adamc@508:                       | _ => (CConcat (c1, c2), loc)
adamc@508:                 end
adamc@508:               | CFold _ => all
adamc@74: 
adamc@508:               | CUnit => all
adamc@21: 
adamc@508:               | CTuple cs => (CTuple (map (con env) cs), loc)
adamc@508:               | CProj (c, n) =>
adamc@508:                 let
adamc@508:                     val c = con env c
adamc@508:                 in
adamc@508:                     case #1 c of
adamc@508:                         CTuple cs => List.nth (cs, n - 1)
adamc@508:                       | _ => (CProj (c, n), loc)
adamc@508:                 end
adamc@22: 
adamc@508:         fun exp env e = e
adamc@417:     in
adamc@508:         {con = con, exp = exp}
adamc@417:     end
adamc@21: 
adamc@508: fun con namedC c = #con (conAndExp (namedC, IM.empty)) [] c
adamc@508: fun exp (namedC, namedE) e = #exp (conAndExp (namedC, namedE)) [] e
adamc@20: 
adamc@508: fun reduce file =
adamc@508:     let
adamc@508:         fun doDecl (d as (_, loc), st as (namedC, namedE)) =
adamc@508:             case #1 d of
adamc@508:                 DCon (x, n, k, c) =>
adamc@508:                 let
adamc@508:                     val c = con namedC c
adamc@508:                 in
adamc@508:                     ((DCon (x, n, k, c), loc),
adamc@508:                      (IM.insert (namedC, n, c), namedE))
adamc@508:                 end
adamc@508:               | DDatatype (x, n, ps, cs) =>
adamc@508:                 ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC) co)) cs), loc),
adamc@508:                  st)
adamc@508:               | DVal (x, n, t, e, s) =>
adamc@508:                 let
adamc@508:                     val t = con namedC t
adamc@508:                     val e = exp (namedC, namedE) e
adamc@508:                 in
adamc@508:                     ((DVal (x, n, t, e, s), loc),
adamc@508:                      (namedC, IM.insert (namedE, n, e)))
adamc@508:                 end
adamc@508:               | DValRec vis =>
adamc@508:                 ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC t, exp (namedC, namedE) e, s)) vis), loc),
adamc@508:                  st)
adamc@508:               | DExport _ => (d, st)
adamc@508:               | DTable (s, n, c, s') => ((DTable (s, n, con namedC c, s'), loc), st)
adamc@508:               | DSequence _ => (d, st)
adamc@508:               | DDatabase _ => (d, st)
adamc@508:               | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC c, s'), loc), st)
adamc@20: 
adamc@508:         val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty) file
adamc@508:     in
adamc@508:         file
adamc@508:     end
adamc@20: 
adamc@20: end