adam@1848: (* Copyright (c) 2008-2011, 2013, 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@1016: structure IS = IntBinarySet adamc@508: structure IM = IntBinaryMap adamc@20: adamc@908: structure E = CoreEnv adamc@908: adam@1544: fun multiLiftConInCon n c = adam@1544: if n = 0 then adam@1544: c adam@1544: else adam@1544: multiLiftConInCon (n - 1) (E.liftConInCon 0 c) adam@1544: adamc@908: fun multiLiftExpInExp n e = adamc@908: if n = 0 then adamc@908: e adamc@908: else adamc@908: multiLiftExpInExp (n - 1) (E.liftExpInExp 0 e) adamc@908: adamc@1179: val count = CoreUtil.Exp.foldB {kind = fn (_, _, c) => c, adamc@1179: con = fn (_, _, c) => c, adamc@1179: exp = fn (x, e, c) => adamc@1179: case e of adamc@1179: ERel x' => if x = x' then c + 1 else c adamc@1179: | _ => c, adamc@1179: bind = fn (x, b) => adamc@1179: case b of adamc@1179: CoreUtil.Exp.RelE _ => x+1 adamc@1179: | _ => x} 0 0 adamc@1179: adamc@909: val dangling = adamc@909: CoreUtil.Exp.existsB {kind = fn _ => false, adamc@909: con = fn _ => false, adamc@909: exp = fn (n, e) => adamc@909: case e of adamc@909: ERel n' => n' >= n adamc@909: | _ => false, adamc@909: bind = fn (n, b) => adamc@909: case b of adamc@909: CoreUtil.Exp.RelE _ => n + 1 adamc@909: | _ => n} adamc@909: adamc@1272: val cdangling = adamc@1272: CoreUtil.Exp.existsB {kind = fn _ => false, adamc@1272: con = fn (n, c) => adamc@1272: case c of adamc@1272: CRel n' => n' >= n adamc@1272: | _ => false, adamc@1272: exp = fn _ => false, adamc@1272: bind = fn (n, b) => adamc@1272: case b of adamc@1272: CoreUtil.Exp.RelC _ => n + 1 adamc@1272: | _ => n} adamc@1272: adamc@508: datatype env_item = adamc@626: UnknownK adamc@626: | KnownK of kind adamc@626: adamc@626: | UnknownC adamc@508: | KnownC of con adamc@21: adamc@508: | UnknownE adamc@508: | KnownE of exp adamc@20: adamc@626: | Lift of int * int * int adamc@20: adamc@909: val edepth = foldl (fn (UnknownE, n) => n + 1 adamc@909: | (KnownE _, n) => n + 1 adamc@909: | (_, n) => n) 0 adamc@909: adamc@909: val edepth' = foldl (fn (UnknownE, n) => n + 1 adamc@909: | (KnownE _, n) => n + 1 adamc@909: | (Lift (_, _, n'), n) => n + n' adamc@909: | (_, n) => n) 0 adamc@909: adamc@1272: val cdepth = foldl (fn (UnknownC, n) => n + 1 adamc@1272: | (KnownC _, n) => n + 1 adamc@1272: | (_, n) => n) 0 adamc@1272: adamc@1272: val cdepth' = foldl (fn (UnknownC, n) => n + 1 adamc@1272: | (KnownC _, n) => n + 1 adamc@1272: | (Lift (_, n', _), n) => n + n' adamc@1272: | (_, n) => n) 0 adamc@1272: adamc@508: type env = env_item list adamc@20: adamc@510: fun ei2s ei = adamc@510: case ei of adamc@626: UnknownK => "UK" adamc@626: | KnownK _ => "KK" adamc@626: | UnknownC => "UC" adamc@510: | KnownC _ => "KC" adamc@510: | UnknownE => "UE" adamc@510: | KnownE _ => "KE" adamc@626: | Lift (_, n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")" adamc@510: adamc@510: fun e2s env = String.concatWith " " (map ei2s env) adamc@510: adamc@909: (*val deKnown = List.filter (fn KnownC _ => false adamc@510: | KnownE _ => false adamc@626: | KnownK _ => false adamc@909: | _ => true)*) adamc@909: adamc@909: val deKnown = ListUtil.mapConcat (fn KnownC _ => [] adamc@909: | KnownE _ => [] adamc@909: | KnownK _ => [] adamc@909: | Lift (nk, nc, ne) => List.tabulate (nk, fn _ => UnknownK) adamc@909: @ List.tabulate (nc, fn _ => UnknownC) adamc@909: @ List.tabulate (ne, fn _ => UnknownE) adamc@909: | x => [x]) adamc@510: adamc@930: datatype result = Yes of env | No | Maybe adamc@930: adamc@930: fun match (env, p : pat, e : exp) = adamc@942: let adamc@942: val baseline = length env adamc@930: adamc@942: fun match (env, p, e) = adamc@942: case (#1 p, #1 e) of adamc@942: (PWild, _) => Yes env adamc@942: | (PVar (x, t), _) => Yes (KnownE (multiLiftExpInExp (length env - baseline) e) :: env) adamc@930: adamc@942: | (PPrim p, EPrim p') => adamc@942: if Prim.equal (p, p') then adamc@942: Yes env adamc@942: else adamc@942: No adamc@930: adamc@942: | (PCon (_, PConVar n1, _, NONE), ECon (_, PConVar n2, _, NONE)) => adamc@942: if n1 = n2 then adamc@942: Yes env adamc@942: else adamc@942: No adamc@930: adamc@942: | (PCon (_, PConVar n1, _, SOME p), ECon (_, PConVar n2, _, SOME e)) => adamc@942: if n1 = n2 then adamc@942: match (env, p, e) adamc@942: else adamc@942: No adamc@930: adamc@942: | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, NONE), adamc@942: ECon (_, PConFfi {mod = m2, con = con2, ...}, _, NONE)) => adamc@942: if m1 = m2 andalso con1 = con2 then adamc@942: Yes env adamc@942: else adamc@942: No adamc@930: adamc@942: | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, SOME ep), adamc@942: ECon (_, PConFfi {mod = m2, con = con2, ...}, _, SOME e)) => adamc@942: if m1 = m2 andalso con1 = con2 then adamc@942: match (env, p, e) adamc@942: else adamc@942: No adamc@930: adamc@942: | (PRecord xps, ERecord xes) => adamc@942: if List.exists (fn ((CName _, _), _, _) => false adamc@942: | _ => true) xes then adamc@942: Maybe adamc@942: else adamc@942: let adamc@942: fun consider (xps, env) = adamc@942: case xps of adamc@942: [] => Yes env adamc@942: | (x, p, _) :: rest => adamc@942: case List.find (fn ((CName x', _), _, _) => x' = x adamc@942: | _ => false) xes of adamc@942: NONE => No adamc@942: | SOME (_, e, _) => adamc@942: case match (env, p, e) of adamc@942: No => No adamc@942: | Maybe => Maybe adamc@942: | Yes env => consider (rest, env) adamc@942: in adamc@942: consider (xps, env) adamc@942: end adamc@942: adamc@942: | _ => Maybe adamc@942: in adamc@942: match (env, p, e) adamc@942: end adamc@930: adam@1544: fun returnType m loc = adam@1544: (TCFun ("a", (KType, loc), adam@1544: (TFun ((CRel 0, loc), adam@1544: (CApp (multiLiftConInCon 1 m, (CRel 0, loc)), loc)), loc)), loc) adam@1544: adam@1544: fun bindType m loc = adam@1544: (TCFun ("a", (KType, loc), adam@1544: (TCFun ("b", (KType, loc), adam@1544: (TFun ((CApp (multiLiftConInCon 2 m, (CRel 1, loc)), loc), adam@1544: (TFun ((TFun ((CRel 1, loc), adam@1544: (CApp (multiLiftConInCon 2 m, (CRel 0, loc)), loc)), adam@1544: loc), adam@1544: (CApp (multiLiftConInCon 2 m, (CRel 0, loc)), loc)), loc)), adam@1544: loc)), loc)), loc) adam@1544: adam@1544: fun monadRecord m loc = adam@1544: (TRecord (CRecord ((KType, loc), adam@1544: [((CName "Return", loc), adam@1544: returnType m loc), adam@1544: ((CName "Bind", loc), adam@1544: bindType m loc)]), loc), loc) adam@1544: adam@1817: fun passive (e : exp) = adam@1817: case #1 e of adam@1817: EPrim _ => true adam@1817: | ERel _ => true adam@1817: | ENamed _ => true adam@1817: | ECon (_, _, _, NONE) => true adam@1817: | ECon (_, _, _, SOME e) => passive e adam@1817: | EFfi _ => true adam@1817: | EAbs _ => true adam@1817: | ECAbs _ => true adam@1817: | EKAbs _ => true adam@1817: | ERecord xes => List.all (passive o #2) xes adam@1817: | EField (e, _, _) => passive e adam@1817: | _ => false adam@1817: adam@1824: fun notFfi (t : con) = adam@1824: case #1 t of adam@1824: CFfi _ => false adam@1824: | _ => true adam@1824: adamc@626: fun kindConAndExp (namedC, namedE) = adamc@508: let adamc@626: fun kind env (all as (k, loc)) = adamc@626: case k of adamc@626: KType => all adamc@626: | KArrow (k1, k2) => (KArrow (kind env k1, kind env k2), loc) adamc@626: | KName => all adamc@626: | KRecord k => (KRecord (kind env k), loc) adamc@626: | KUnit => all adamc@626: | KTuple ks => (KTuple (map (kind env) ks), loc) adamc@626: adamc@626: | KRel n => adamc@626: let adamc@626: fun find (n', env, nudge, lift) = adamc@626: case env of adamc@626: [] => raise Fail "Reduce.kind: KRel" adamc@626: | UnknownC :: rest => find (n', rest, nudge, lift) adamc@626: | KnownC _ :: rest => find (n', rest, nudge, lift) adamc@626: | UnknownE :: rest => find (n', rest, nudge, lift) adamc@626: | KnownE _ :: rest => find (n', rest, nudge, lift) adamc@626: | Lift (lift', _, _) :: rest => find (n', rest, nudge + lift', lift + lift') adamc@626: | UnknownK :: rest => adamc@626: if n' = 0 then adamc@626: (KRel (n + nudge), loc) adamc@626: else adamc@626: find (n' - 1, rest, nudge, lift + 1) adamc@626: | KnownK k :: rest => adamc@626: if n' = 0 then adamc@626: kind (Lift (lift, 0, 0) :: rest) k adamc@626: else adamc@626: find (n' - 1, rest, nudge - 1, lift) adamc@626: in adamc@626: find (n, env, 0, 0) adamc@626: end adamc@626: | KFun (x, k) => (KFun (x, kind (UnknownK :: env) k), loc) adamc@626: adamc@508: fun con env (all as (c, loc)) = adamc@510: ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*) adamc@508: case c of adamc@508: TFun (c1, c2) => (TFun (con env c1, con env c2), loc) adamc@626: | TCFun (x, k, c2) => (TCFun (x, kind env k, con (UnknownC :: env) c2), loc) adamc@626: | TKFun (x, c2) => (TKFun (x, con (UnknownK :: env) c2), loc) adamc@508: | TRecord c => (TRecord (con env c), loc) adamc@215: adamc@508: | CRel n => adamc@508: let adamc@626: fun find (n', env, nudge, liftK, liftC) = adamc@510: case env of adamc@510: [] => raise Fail "Reduce.con: CRel" adamc@626: | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC) adamc@626: | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC) adamc@626: | UnknownE :: rest => find (n', rest, nudge, liftK, liftC) adamc@626: | KnownE _ :: rest => find (n', rest, nudge, liftK, liftC) adamc@626: | Lift (liftK', liftC', _) :: rest => find (n', rest, nudge + liftC', adamc@626: liftK + liftK', liftC + liftC') adamc@510: | UnknownC :: rest => adamc@510: if n' = 0 then adamc@510: (CRel (n + nudge), loc) adamc@510: else adamc@626: find (n' - 1, rest, nudge, liftK, liftC + 1) adamc@510: | KnownC c :: rest => adamc@510: if n' = 0 then adamc@626: con (Lift (liftK, liftC, 0) :: rest) c adamc@510: else adamc@626: find (n' - 1, rest, nudge - 1, liftK, liftC) adamc@508: in adamc@510: (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) adamc@626: find (n, env, 0, 0, 0) adamc@508: end adam@1544: adamc@508: | CNamed n => adamc@508: (case IM.find (namedC, n) of adamc@508: NONE => all adamc@508: | SOME c => c) adam@1544: adam@1544: | CFfi ("Basis", "monad") => (CAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc), monadRecord (CRel 0, loc) loc), loc) adam@1544: 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@510: con (KnownC c2 :: deKnown env) b adamc@215: adamc@621: | CApp ((CMap (dom, ran), _), f) => adamc@508: (case #1 c2 of adamc@626: CRecord (_, []) => (CRecord (kind env ran, []), loc) adamc@621: | CRecord (_, (x, c) :: rest) => adamc@510: con (deKnown env) adamc@621: (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc), adamc@626: (CApp (c1, (CRecord (kind env dom, rest), loc)), loc)), loc) adamc@508: | _ => (CApp (c1, c2), loc)) adamc@20: adamc@508: | _ => (CApp (c1, c2), loc) adamc@508: end adamc@626: | CAbs (x, k, b) => (CAbs (x, kind env k, con (UnknownC :: env) b), loc) adamc@626: adamc@626: | CKApp (c1, k) => adamc@626: let adamc@626: val c1 = con env c1 adamc@626: in adamc@626: case #1 c1 of adamc@626: CKAbs (_, b) => adamc@626: con (KnownK k :: deKnown env) b adamc@626: adamc@626: | _ => (CKApp (c1, kind env k), loc) adamc@626: end adamc@626: | CKAbs (x, b) => (CKAbs (x, con (UnknownK :: env) b), loc) adamc@20: adamc@508: | CName _ => all adamc@21: adamc@626: | CRecord (k, xcs) => (CRecord (kind env 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@626: (CRecord (kind env k, xcs1 @ xcs2), loc) adamc@1122: | (CRecord (_, []), _) => c2 adamc@1122: | (_, CRecord (_, [])) => c1 adamc@508: | _ => (CConcat (c1, c2), loc) adamc@508: end adamc@626: | CMap (dom, ran) => (CMap (kind env dom, kind env ran), loc) 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@510: end) adamc@22: adamc@509: fun patCon pc = adamc@509: case pc of adamc@509: PConVar _ => pc adamc@509: | PConFfi {mod = m, datatyp, params, con = c, arg, kind} => adamc@509: PConFfi {mod = m, datatyp = datatyp, params = params, con = c, adamc@509: arg = Option.map (con (map (fn _ => UnknownC) params)) arg, adamc@509: kind = kind} adamc@509: adamc@509: adamc@509: val k = (KType, ErrorMsg.dummySpan) adamc@509: fun doPart e (this as (x, t), rest) = adamc@509: ((x, (EField (e, x, {field = t, rest = (CRecord (k, rest), #2 t)}), #2 t), t), adamc@509: this :: rest) adamc@509: adamc@509: fun exp env (all as (e, loc)) = adamc@909: let adamc@909: (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), adamc@909: ("env", Print.PD.string (e2s env))]*) adamc@1176: (*val () = if dangling (edepth env) all then adamc@909: (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), adamc@909: ("env", Print.PD.string (e2s env))]; adamc@909: raise Fail "!") adamc@909: else adamc@1176: ()*) adamc@1272: (*val () = if cdangling (cdepth env) all then adamc@1272: Print.prefaces "Bad exp" [("e", CorePrint.p_exp CoreEnv.empty all), adamc@1272: ("env", Print.PD.string (e2s env))] adamc@1272: else adamc@1272: ()*) adamc@509: kkallio@1533: fun patBinds (p, _) = kkallio@1533: case p of kkallio@1533: PWild => 0 kkallio@1533: | PVar _ => 1 kkallio@1533: | PPrim _ => 0 kkallio@1533: | PCon (_, _, _, NONE) => 0 kkallio@1533: | PCon (_, _, _, SOME p) => patBinds p kkallio@1533: | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts kkallio@1533: adamc@909: val r = case e of adamc@909: EPrim _ => all adamc@909: | ERel n => adamc@909: let adamc@909: fun find (n', env, nudge, liftK, liftC, liftE) = adamc@909: case env of adamc@909: [] => raise Fail ("Reduce.exp: ERel (" ^ ErrorMsg.spanToString loc ^ ")") adamc@909: | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC, liftE) adamc@909: | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC, liftE) adamc@909: | UnknownC :: rest => find (n', rest, nudge, liftK, liftC + 1, liftE) adamc@909: | KnownC _ :: rest => find (n', rest, nudge, liftK, liftC, liftE) adamc@909: | Lift (liftK', liftC', liftE') :: rest => adamc@909: find (n', rest, nudge + liftE', adamc@909: liftK + liftK', liftC + liftC', liftE + liftE') adamc@909: | UnknownE :: rest => adamc@909: if n' = 0 then adamc@909: (ERel (n + nudge), loc) adamc@909: else adamc@909: find (n' - 1, rest, nudge, liftK, liftC, liftE + 1) adamc@909: | KnownE e :: rest => adamc@909: if n' = 0 then adamc@909: ((*print "SUBSTITUTING\n";*) adamc@909: exp (Lift (liftK, liftC, liftE) :: rest) e) adamc@909: else adamc@909: find (n' - 1, rest, nudge - 1, liftK, liftC, liftE) adamc@909: in adamc@909: (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) adamc@909: find (n, env, 0, 0, 0, 0) adamc@909: end adamc@909: | ENamed n => adamc@909: (case IM.find (namedE, n) of adamc@909: NONE => all adamc@909: | SOME e => e) adamc@909: | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc, adamc@909: map (con env) cs, Option.map (exp env) eo), loc) adam@1544: adam@1544: | EFfi ("Basis", "return") => adam@1544: (ECAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc), adam@1544: (ECAbs ("a", (KType, loc), adam@1544: (EAbs ("m", monadRecord (CRel 1, loc) loc, returnType (CRel 1, loc) loc, adam@1544: (ECApp ((EField ((ERel 0, loc), (CName "Return", loc), adam@1544: {field = returnType (CRel 1, loc) loc, adam@1544: rest = (CRecord ((KType, loc), adam@1544: [((CName "Bind", loc), bindType (CRel 1, loc) loc)]), adam@1544: loc)}), loc), (CRel 0, loc)), loc)), loc)), loc)), loc) adam@1544: adam@1544: | EFfi ("Basis", "bind") => adam@1544: (ECAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc), adam@1544: (ECAbs ("a", (KType, loc), adam@1544: (ECAbs ("b", (KType, loc), adam@1544: (EAbs ("m", monadRecord (CRel 2, loc) loc, bindType (CRel 2, loc) loc, adam@1544: (ECApp ((ECApp ((EField ((ERel 0, loc), (CName "Bind", loc), adam@1544: {field = bindType (CRel 2, loc) loc, adam@1544: rest = (CRecord ((KType, loc), adam@1544: [((CName "Return", loc), adam@1544: returnType (CRel 2, loc) loc)]), adam@1544: loc)}), loc), (CRel 1, loc)), loc), adam@1544: (CRel 0, loc)), loc)), loc)), loc)), loc)), loc) adam@1544: adam@1544: | EFfi ("Basis", "mkMonad") => adam@1544: (ECAbs ("m", (KArrow ((KType, loc), (KType, loc)), loc), adam@1544: (EAbs ("m", monadRecord (CRel 0, loc) loc, monadRecord (CRel 0, loc) loc, adam@1544: (ERel 0, loc)), loc)), loc) adam@1544: adam@1544: | EFfi ("Basis", "transaction_monad") => adam@1544: (ERecord [((CName "Return", loc), adam@1544: (EFfi ("Basis", "transaction_return"), loc), adam@1544: returnType (CFfi ("Basis", "transaction"), loc) loc), adam@1544: ((CName "Bind", loc), adam@1544: (EFfi ("Basis", "transaction_bind"), loc), adam@1544: bindType (CFfi ("Basis", "transaction"), loc) loc)], loc) adam@1544: adam@1544: | EFfi ("Basis", "signal_monad") => adam@1544: (ERecord [((CName "Return", loc), adam@1544: (EFfi ("Basis", "signal_return"), loc), adam@1544: returnType (CFfi ("Basis", "signal"), loc) loc), adam@1544: ((CName "Bind", loc), adam@1544: (EFfi ("Basis", "signal_bind"), loc), adam@1544: bindType (CFfi ("Basis", "signal"), loc) loc)], loc) adam@1544: adamc@909: | EFfi _ => all adam@1663: | EFfiApp (m, f, es) => (EFfiApp (m, f, map (fn (e, t) => (exp env e, con env t)) es), loc) adamc@908: adamc@909: (*| EApp ( adamc@909: (EApp adamc@909: ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _), adamc@909: (EFfi ("Basis", "transaction_monad"), _)), _), adamc@909: (ECase (ed, pes, {disc, ...}), _)), _), adamc@909: trans2) => adamc@909: let adamc@909: val e' = (EFfi ("Basis", "bind"), loc) adamc@909: val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc) adamc@909: val e' = (ECApp (e', t1), loc) adamc@909: val e' = (ECApp (e', t2), loc) adamc@909: val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc) adamc@908: adamc@909: val pes = map (fn (p, e) => adamc@909: let adamc@909: val e' = (EApp (e', e), loc) adamc@909: val e' = (EApp (e', adamc@909: multiLiftExpInExp (E.patBindsN p) adamc@909: trans2), loc) adamc@909: val e' = exp env e' adamc@909: in adamc@909: (p, e') adamc@909: end) pes adamc@909: in adamc@909: (ECase (exp env ed, adamc@909: pes, adamc@909: {disc = con env disc, adamc@909: result = (CApp ((CFfi ("Basis", "transaction"), loc), con env t2), loc)}), adamc@909: loc) adamc@909: end*) adamc@908: adamc@909: | EApp (e1, e2) => adamc@909: let adamc@910: val env' = deKnown env adamc@910: adamc@909: val e1 = exp env e1 adamc@909: val e2 = exp env e2 adamc@909: in adamc@1179: case #1 e1 of adam@1817: ELet (x, t, e1', e2') => adam@1817: (ELet (x, t, e1', exp (UnknownE :: env') (EApp (e2', E.liftExpInExp 0 e2), loc)), loc) adam@1817: adam@1817: | EAbs (x, dom, _, b) => adam@1863: if count b <= 1 orelse passive e2 orelse ESpecialize.functionInside IS.empty dom then adam@1817: let adam@1817: val r = exp (KnownE e2 :: env') b adam@1817: in adam@1817: (*Print.prefaces "eapp" [("b", CorePrint.p_exp CoreEnv.empty b), adam@1817: ("env", Print.PD.string (e2s env')), adam@1817: ("e2", CorePrint.p_exp CoreEnv.empty e2), adam@1817: ("r", CorePrint.p_exp CoreEnv.empty r)];*) adam@1817: r adam@1817: end adam@1817: else adam@1817: let adam@1817: val dom = con env' dom adam@1817: val r = exp (UnknownE :: env') b adam@1817: in adam@1817: (*Print.prefaces "El skippo" [("x", Print.PD.string x), adam@1817: ("e2", CorePrint.p_exp CoreEnv.empty e2)];*) adam@1817: (ELet (x, dom, e2, r), loc) adam@1817: end adam@1817: kkallio@1533: | ECase (e, pes, cc as {disc, result = res as (TFun (_, c2), _)}) => kkallio@1533: let kkallio@1533: val pes' = map (fn (p, body) => kkallio@1533: let adam@1534: val env' = List.tabulate (patBinds p, fn _ => UnknownE) @ deKnown env kkallio@1533: val body' = exp env' (EApp (body, multiLiftExpInExp (patBinds p) e2), #2 body) kkallio@1533: in kkallio@1533: (p, body') kkallio@1533: end) pes kkallio@1533: kkallio@1533: val cc' = {disc = disc, result = c2} kkallio@1533: in kkallio@1533: (ECase (e, pes', cc'), loc) kkallio@1533: end adamc@1179: | _ => (EApp (e1, e2), loc) adamc@909: end adamc@509: adamc@909: | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc) adamc@509: adamc@909: | ECApp (e, c) => adamc@909: let adamc@909: val e = exp env e adamc@909: val c = con env c adamc@909: in adamc@909: case #1 e of adamc@1181: ECAbs (_, _, b) => adamc@1181: let adamc@1181: val r = exp (KnownC c :: deKnown env) b adamc@1181: in adamc@1181: (*Print.prefaces "csub" [("l", Print.PD.string (ErrorMsg.spanToString loc)), adamc@1181: ("env", Print.PD.string (e2s (deKnown env))), adamc@1181: ("b", CorePrint.p_exp CoreEnv.empty b), adamc@1181: ("c", CorePrint.p_con CoreEnv.empty c), adamc@1181: ("r", CorePrint.p_exp CoreEnv.empty r)];*) adamc@1181: r adamc@1181: end kkallio@1533: | ECase (e, pes, cc as {disc, result = res as (TCFun (_, _, c'), _)}) => kkallio@1533: let kkallio@1533: val pes' = map (fn (p, body) => kkallio@1533: let adam@1534: val env' = List.tabulate (patBinds p, fn _ => UnknownE) @ deKnown env kkallio@1533: kkallio@1533: val body' = exp env' (ECApp (body, c), #2 body) kkallio@1533: in kkallio@1533: (p, body') kkallio@1533: end) pes kkallio@1533: kkallio@1533: val c' = E.subConInCon (0, c) c' kkallio@1533: val cc' = {disc = disc, result = c'} kkallio@1533: in kkallio@1533: (ECase (e, pes', cc'), loc) kkallio@1533: end adamc@909: | _ => (ECApp (e, c), loc) adamc@909: end adamc@626: adamc@909: | ECAbs (x, k, e) => (ECAbs (x, kind env k, exp (UnknownC :: env) e), loc) adamc@626: adamc@909: | EKApp (e, k) => adamc@909: let adamc@909: val e = exp env e adamc@909: in adamc@909: case #1 e of adamc@1181: EKAbs (_, b) => adamc@1181: let adamc@1181: val r = exp (KnownK k :: deKnown env) b adamc@1181: in adamc@1181: (*Print.prefaces "ksub" [("l", Print.PD.string (ErrorMsg.spanToString loc)), adamc@1181: ("b", CorePrint.p_exp CoreEnv.empty b), adamc@1181: ("k", CorePrint.p_kind CoreEnv.empty k), adamc@1181: ("r", CorePrint.p_exp CoreEnv.empty r)];*) adamc@1181: r adamc@1181: end adamc@909: | _ => (EKApp (e, kind env k), loc) adamc@909: end adamc@509: adamc@909: | EKAbs (x, e) => (EKAbs (x, exp (UnknownK :: env) e), loc) adamc@509: adamc@909: | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc) adamc@909: | EField (e, c, {field, rest}) => adamc@909: let adamc@909: val e = exp env e adamc@909: val c = con env c adamc@509: adamc@909: fun default () = (EField (e, c, {field = con env field, rest = con env rest}), loc) adamc@909: in adamc@909: case (#1 e, #1 c) of adamc@909: (ERecord xcs, CName x) => adamc@909: (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of adamc@909: NONE => default () adamc@909: | SOME (_, e, _) => e) adamc@909: | _ => default () adamc@909: end adamc@509: adamc@909: | EConcat (e1, c1, e2, c2) => adamc@909: let adamc@909: val e1 = exp env e1 adamc@909: val e2 = exp env e2 adamc@909: in adamc@909: case (#1 e1, #1 e2) of adamc@909: (ERecord xes1, ERecord xes2) => (ERecord (xes1 @ xes2), loc) adamc@909: | _ => adamc@909: let adamc@909: val c1 = con env c1 adamc@909: val c2 = con env c2 adamc@909: in adamc@909: case (#1 c1, #1 c2) of adamc@909: (CRecord (k, xcs1), CRecord (_, xcs2)) => adamc@909: let adamc@909: val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1 adamc@909: val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2 adamc@909: in adamc@909: exp (deKnown env) (ERecord (xes1 @ xes2), loc) adamc@909: end adamc@909: | _ => (EConcat (e1, c1, e2, c2), loc) adamc@909: end adamc@909: end adamc@509: adamc@909: | ECut (e, c, {field, rest}) => adamc@909: let adamc@909: val e = exp env e adamc@909: val c = con env c adamc@509: adamc@909: fun default () = adamc@909: let adamc@909: val rest = con env rest adamc@909: in adamc@909: case #1 rest of adamc@909: CRecord (k, xcs) => adamc@909: let adamc@909: val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs adamc@909: in adamc@909: exp (deKnown env) (ERecord xes, loc) adamc@909: end adamc@909: | _ => (ECut (e, c, {field = con env field, rest = rest}), loc) adamc@909: end adamc@909: in adamc@909: case (#1 e, #1 c) of adamc@909: (ERecord xes, CName x) => adamc@909: if List.all (fn ((CName _, _), _, _) => true | _ => false) xes then adamc@909: (ERecord (List.filter (fn ((CName x', _), _, _) => x' <> x adamc@909: | _ => raise Fail "Reduce: ECut") xes), loc) adamc@909: else adamc@909: default () adamc@909: | _ => default () adamc@909: end adamc@509: adamc@909: | ECutMulti (e, c, {rest}) => adamc@909: let adamc@909: val e = exp env e adamc@909: val c = con env c adamc@509: adamc@909: fun default () = adamc@909: let adamc@909: val rest = con env rest adamc@909: in adamc@909: case #1 rest of adamc@909: CRecord (k, xcs) => adamc@909: let adamc@909: val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs adamc@909: in adamc@909: exp (deKnown env) (ERecord xes, loc) adamc@909: end adamc@909: | _ => (ECutMulti (e, c, {rest = rest}), loc) adamc@909: end adamc@909: in adamc@909: case (#1 e, #1 c) of adamc@909: (ERecord xes, CRecord (_, xcs)) => adamc@909: if List.all (fn ((CName _, _), _, _) => true | _ => false) xes adamc@909: andalso List.all (fn ((CName _, _), _) => true | _ => false) xcs then adamc@909: (ERecord (List.filter (fn ((CName x', _), _, _) => adamc@909: List.all (fn ((CName x, _), _) => x' <> x adamc@909: | _ => raise Fail "Reduce: ECutMulti [1]") xcs adamc@909: | _ => raise Fail "Reduce: ECutMulti [2]") xes), loc) adamc@909: else adamc@909: default () adamc@909: | _ => default () adamc@909: end adamc@823: adamc@909: | ECase (_, [((PRecord [], _), e)], _) => exp env e adamc@909: | ECase (_, [((PWild, _), e)], _) => exp env e adamc@509: adamc@909: | ECase (e, pes, {disc, result}) => adamc@909: let adamc@909: fun pat (all as (p, loc)) = adamc@909: case p of adamc@909: PWild => all adamc@909: | PVar (x, t) => (PVar (x, con env t), loc) adamc@909: | PPrim _ => all adamc@909: | PCon (dk, pc, cs, po) => adamc@909: (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc) adamc@909: | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc) adamc@930: adamc@930: fun push () = adamc@930: (ECase (exp env e, adamc@930: map (fn (p, e) => (pat p, adamc@930: exp (List.tabulate (patBinds p, adamc@930: fn _ => UnknownE) @ env) e)) adamc@930: pes, {disc = con env disc, result = con env result}), loc) adamc@930: adamc@930: fun search pes = adamc@930: case pes of adamc@930: [] => push () adamc@930: | (p, body) :: pes => adamc@930: case match (env, p, e) of adamc@930: No => search pes adamc@930: | Maybe => push () adamc@930: | Yes env' => exp env' body adamc@909: in adamc@930: search pes adamc@909: end adamc@509: adamc@909: | EWrite e => (EWrite (exp env e), loc) adamc@909: | EClosure (n, es) => (EClosure (n, map (exp env) es), loc) adamc@607: adamc@910: | ELet (x, t, e1, e2) => adam@1289: let adam@1817: val e1' = exp env e1 adam@1817: adam@1289: val t = con env t adam@1289: in adam@1863: if notFfi t andalso (passive e1' orelse count e2 <= 1 orelse ESpecialize.functionInside IS.empty t) then adam@1289: exp (KnownE e1 :: env) e2 adam@1289: else adam@1817: (ELet (x, t, e1', exp (UnknownE :: env) e2), loc) adam@1289: end adamc@909: adam@1848: | EServerCall (n, es, t, fm) => (EServerCall (n, map (exp env) es, con env t, fm), loc) adamc@909: in adamc@909: (*if dangling (edepth' (deKnown env)) r then adamc@909: (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), adamc@909: ("r", CorePrint.p_exp CoreEnv.empty r)]; adamc@909: raise Fail "!!") adamc@909: else adamc@909: ();*) adamc@1272: (*if cdangling (cdepth' (deKnown env)) r then adamc@1272: (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), adamc@1272: ("r", CorePrint.p_exp CoreEnv.empty r)]; adamc@1272: raise Fail "!!") adamc@1272: else adamc@1272: ();*) adamc@909: r adamc@909: end adamc@417: in adamc@626: {kind = kind, con = con, exp = exp} adamc@417: end adamc@21: adamc@626: fun kind namedC env k = #kind (kindConAndExp (namedC, IM.empty)) env k adamc@626: fun con namedC env c = #con (kindConAndExp (namedC, IM.empty)) env c adamc@626: fun exp (namedC, namedE) env e = #exp (kindConAndExp (namedC, namedE)) env e adamc@20: adamc@508: fun reduce file = adamc@508: let adamc@1016: val uses = CoreUtil.File.fold {kind = fn (_, m) => m, adamc@1016: con = fn (_, m) => m, adamc@1016: exp = fn (e, m) => adamc@1016: case e of adamc@1016: ENamed n => IM.insert (m, n, 1 + Option.getOpt (IM.find (m, n), 0)) adamc@1016: | _ => m, adamc@1016: decl = fn (_, m) => m} adamc@1016: IM.empty file adamc@1016: adamc@1016: fun isPoly names = CoreUtil.Con.exists {kind = fn _ => false, adamc@1016: con = fn TCFun _ => true adamc@1016: | TKFun _ => true adamc@1016: | CNamed n => IS.member (names, n) adamc@1016: | _ => false} adamc@1016: adamc@1016: val size = CoreUtil.Exp.fold {kind = fn (_, n) => n, adamc@1016: con = fn (_, n) => n, adamc@1016: exp = fn (_, n) => n + 1} 0 adamc@1016: adam@1969: fun mayInline (polyC, n, t, e, s) = adamc@1240: let adamc@1240: fun isPolicy t = adamc@1240: case #1 t of adamc@1240: CFfi ("Basis", "sql_policy") => true adamc@1240: | TFun (_, t) => isPolicy t adamc@1240: | _ => false adamc@1240: in adam@1969: not (Settings.checkNeverInline s) andalso adamc@1240: case IM.find (uses, n) of adamc@1240: NONE => false adamc@1240: | SOME count => count <= 1 adamc@1240: orelse (case #1 e of adamc@1240: ERecord _ => true adamc@1240: | _ => false) adamc@1240: orelse isPolicy t adamc@1240: orelse isPoly polyC t adamc@1240: orelse size e <= Settings.getCoreInline () adamc@1240: end adamc@1016: adamc@1016: fun doDecl (d as (_, loc), st as (polyC, namedC, namedE)) = adamc@508: case #1 d of adamc@508: DCon (x, n, k, c) => adamc@508: let adamc@626: val k = kind namedC [] k adamc@509: val c = con namedC [] c adamc@508: in adamc@508: ((DCon (x, n, k, c), loc), adamc@1016: (if isPoly polyC c then adamc@1016: IS.add (polyC, n) adamc@1016: else adamc@1016: polyC, adamc@1016: IM.insert (namedC, n, c), adamc@1016: namedE)) adamc@508: end adamc@807: | DDatatype dts => adamc@807: ((DDatatype (map (fn (x, n, ps, cs) => adamc@807: let adamc@807: val env = map (fn _ => UnknownC) ps adamc@807: in adamc@807: (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC env) co)) cs) adamc@807: end) dts), loc), adamc@1016: (if List.exists (fn (_, _, _, cs) => List.exists (fn (_, _, co) => case co of adamc@1016: NONE => false adamc@1016: | SOME c => isPoly polyC c) cs) adamc@1016: dts then adamc@1016: foldl (fn ((_, n, _, _), polyC) => IS.add (polyC, n)) polyC dts adamc@1016: else adamc@1016: polyC, adamc@1016: namedC, adamc@1016: namedE)) adamc@508: | DVal (x, n, t, e, s) => adamc@508: let adamc@509: val t = con namedC [] t adamc@509: val e = exp (namedC, namedE) [] e adamc@508: in adamc@508: ((DVal (x, n, t, e, s), loc), adamc@1016: (polyC, adamc@1016: namedC, adam@1969: if mayInline (polyC, n, t, e, s) then adamc@1016: IM.insert (namedE, n, e) adamc@1016: else adamc@1016: namedE)) adamc@508: end adamc@508: | DValRec vis => adamc@910: ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC [] t, adamc@910: exp (namedC, namedE) [] e, s)) vis), loc), adamc@508: st) adamc@508: | DExport _ => (d, st) adamc@707: | DTable (s, n, c, s', pe, pc, ce, cc) => ((DTable (s, n, con namedC [] c, s', adamc@707: exp (namedC, namedE) [] pe, adamc@707: con namedC [] pc, adamc@707: exp (namedC, namedE) [] ce, adamc@707: con namedC [] cc), loc), st) adamc@508: | DSequence _ => (d, st) adamc@754: | DView (s, n, s', e, c) => ((DView (s, n, s', exp (namedC, namedE) [] e, con namedC [] c), loc), st) adamc@508: | DDatabase _ => (d, st) adamc@509: | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC [] c, s'), loc), st) adamc@720: | DStyle (s, n, s') => ((DStyle (s, n, s'), loc), st) adamc@1075: | DTask (e1, e2) => adamc@1073: let adamc@1075: val e1 = exp (namedC, namedE) [] e1 adamc@1075: val e2 = exp (namedC, namedE) [] e2 adamc@1073: in adamc@1075: ((DTask (e1, e2), loc), adamc@1073: (polyC, adamc@1073: namedC, adamc@1073: namedE)) adamc@1073: end adamc@1199: | DPolicy e1 => adamc@1199: let adamc@1199: val e1 = exp (namedC, namedE) [] e1 adamc@1199: in adamc@1199: ((DPolicy e1, loc), adamc@1199: (polyC, adamc@1199: namedC, adamc@1199: namedE)) adamc@1199: end adam@1294: | DOnError _ => (d, st) adamc@20: adamc@1016: val (file, _) = ListUtil.foldlMap doDecl (IS.empty, IM.empty, IM.empty) file adamc@508: in adamc@508: file adamc@508: end adamc@20: adamc@20: end