changeset 509:140c68046598

Most exp rules for new Reduce
author Adam Chlipala <adamc@hcoop.net>
date Wed, 26 Nov 2008 12:59:32 -0500
parents 04053089878a
children c644ec94866d
files src/reduce.sml
diffstat 1 files changed, 219 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/src/reduce.sml	Wed Nov 26 12:13:00 2008 -0500
+++ b/src/reduce.sml	Wed Nov 26 12:59:32 2008 -0500
@@ -59,6 +59,7 @@
                             case env of
                                 UnknownC :: _ => (CRel (n + lift), loc)
                               | KnownC c :: _ => con (Lift (lift, 0) :: env) c
+                              | Lift (lift', _) :: rest => find (0, rest, lift + lift')
                               | _ => raise Fail "Reduce.con: CRel [1]"
                         else
                             case env of
@@ -66,7 +67,7 @@
                               | KnownC _ :: rest => find (n' - 1, rest, lift)
                               | UnknownE :: rest => find (n' - 1, rest, lift)
                               | KnownE _ :: rest => find (n' - 1, rest, lift)
-                              | Lift (lift', _) :: rest => find (n' - 1, rest, lift + lift')
+                              | Lift (lift', _) :: rest => find (n', rest, lift + lift')
                               | [] => raise Fail "Reduce.con: CRel [2]"
                 in
                     find (n, env, 0)
@@ -125,13 +126,215 @@
                       | _ => (CProj (c, n), loc)
                 end
 
-        fun exp env e = e
+        fun patCon pc =
+            case pc of
+                PConVar _ => pc
+              | PConFfi {mod = m, datatyp, params, con = c, arg, kind} =>
+                PConFfi {mod = m, datatyp = datatyp, params = params, con = c,
+                         arg = Option.map (con (map (fn _ => UnknownC) params)) arg,
+                         kind = kind}
+
+
+        val k = (KType, ErrorMsg.dummySpan)
+        fun doPart e (this as (x, t), rest) =
+            ((x, (EField (e, x, {field = t, rest = (CRecord (k, rest), #2 t)}), #2 t), t),
+             this :: rest)
+
+        fun exp env (all as (e, loc)) =
+            case e of
+                EPrim _ => all
+              | ERel n =>
+                let
+                    fun find (n', env, liftC, liftE) =
+                        if n' = 0 then
+                            case env of
+                                UnknownE :: _ => (ERel (n + liftE), loc)
+                              | KnownE e :: _ => exp (Lift (liftC, liftE) :: env) e
+                              | Lift (liftC', liftE') :: rest => find (0, rest, liftC + liftC', liftE + liftE')
+                              | _ => raise Fail "Reduce.exp: ERel [1]"
+                        else
+                            case env of
+                                UnknownC :: rest => find (n' - 1, rest, liftC + 1, liftE)
+                              | KnownC _ :: rest => find (n' - 1, rest, liftC, liftE)
+                              | UnknownE :: rest => find (n' - 1, rest, liftC, liftE + 1)
+                              | KnownE _ :: rest => find (n' - 1, rest, liftC, liftE)
+                              | Lift (liftC', liftE') :: rest => find (n', rest, liftC + liftC', liftE + liftE')
+                              | [] => raise Fail "Reduce.exp: ERel [2]"
+                in
+                    find (n, env, 0, 0)
+                end
+              | ENamed n =>
+                (case IM.find (namedE, n) of
+                     NONE => all
+                   | SOME e => e)
+              | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc,
+                                                map (con env) cs, Option.map (exp env) eo), loc)
+              | EFfi _ => all
+              | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
+
+              | EApp (e1, e2) =>
+                let
+                    val e1 = exp env e1
+                    val e2 = exp env e2
+                in
+                    case #1 e1 of
+                        EAbs (_, _, _, b) => exp (KnownE e2 :: env) b
+                      | _ => (EApp (e1, e2), loc)
+                end
+
+              | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc)
+
+              | ECApp (e, c) =>
+                let
+                    val e = exp env e
+                    val c = con env c
+                in
+                    case #1 e of
+                        ECAbs (_, _, b) => exp (KnownC c :: env) b
+                      | _ => (ECApp (e, c), loc)
+                end
+
+              | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc)
+
+              | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc)
+              | EField (e, c, {field, rest}) =>
+                let
+                    val e = exp env e
+                    val c = con env c
+
+                    fun default () = (EField (e, c, {field = con env field, rest = con env rest}), loc)
+                in
+                    case (#1 e, #1 c) of
+                        (ERecord xcs, CName x) =>
+                        (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of
+                             NONE => default ()
+                           | SOME (_, e, _) => e)
+                      | _ => default ()
+                end
+
+              | EConcat (e1, c1, e2, c2) =>
+                let
+                    val e1 = exp env e1
+                    val e2 = exp env e2
+                in
+                    case (#1 e1, #1 e2) of
+                        (ERecord xes1, ERecord xes2) => (ERecord (xes1 @ xes2), loc)
+                      | _ =>
+                        let
+                            val c1 = con env c1
+                            val c2 = con env c2
+                        in
+                            case (#1 c1, #1 c2) of
+                                (CRecord (k, xcs1), CRecord (_, xcs2)) =>
+                                let
+                                    val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1
+                                    val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2
+                                in
+                                    exp env (ERecord (xes1 @ xes2), loc)
+                                end
+                              | _ => (EConcat (e1, c1, e2, c2), loc)
+                        end
+                end
+
+              | ECut (e, c, {field, rest}) =>
+                let
+                    val e = exp env e
+                    val c = con env c
+
+                    fun default () =
+                        let
+                            val rest = con env rest
+                        in
+                            case #1 rest of
+                                CRecord (k, xcs) =>
+                                let
+                                    val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
+                                in
+                                    exp env (ERecord xes, loc)
+                                end
+                              | _ => (ECut (e, c, {field = con env field, rest = rest}), loc)
+                        end
+                in
+                    case (#1 e, #1 c) of
+                        (ERecord xes, CName x) =>
+                        if List.all (fn ((CName _, _), _, _) => true | _ => false) xes then
+                            (ERecord (List.filter (fn ((CName x', _), _, _) => x' <> x
+                                                    | _ => raise Fail "Reduce: ECut") xes), loc)
+                        else
+                            default ()
+                      | _ => default ()
+                end
+
+              | ECutMulti (e, c, {rest}) =>
+                let
+                    val e = exp env e
+                    val c = con env c
+
+                    fun default () =
+                        let
+                            val rest = con env rest
+                        in
+                            case #1 rest of
+                                CRecord (k, xcs) =>
+                                let
+                                    val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
+                                in
+                                    exp env (ERecord xes, loc)
+                                end
+                              | _ => (ECutMulti (e, c, {rest = rest}), loc)
+                        end
+                in
+                    case (#1 e, #1 c) of
+                        (ERecord xes, CRecord (_, xcs)) =>
+                        if List.all (fn ((CName _, _), _, _) => true | _ => false) xes
+                           andalso List.all (fn ((CName _, _), _) => true | _ => false) xcs then
+                            (ERecord (List.filter (fn ((CName x', _), _, _) =>
+                                                      List.all (fn ((CName x, _), _) => x' <> x
+                                                                 | _ => raise Fail "Reduce: ECutMulti [1]") xcs
+                                                    | _ => raise Fail "Reduce: ECutMulti [2]") xes), loc)
+                        else
+                            default ()
+                      | _ => default ()
+                end
+
+              | EFold _ => all
+
+              | ECase (e, pes, {disc, result}) =>
+                let
+                    fun patBinds (p, _) =
+                        case p of
+                            PWild => 0
+                          | PVar _ => 1
+                          | PPrim _ => 0
+                          | PCon (_, _, _, NONE) => 0
+                          | PCon (_, _, _, SOME p) => patBinds p
+                          | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
+
+                    fun pat (all as (p, loc)) =
+                        case p of
+                            PWild => all
+                          | PVar (x, t) => (PVar (x, con env t), loc)
+                          | PPrim _ => all
+                          | PCon (dk, pc, cs, po) =>
+                            (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc)
+                          | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc)
+                in
+                    (ECase (exp env e,
+                            map (fn (p, e) => (pat p,
+                                               exp (List.tabulate (patBinds p, fn _ => UnknownE) @ env) e))
+                                pes, {disc = con env disc, result = con env result}), loc)
+                end
+
+              | EWrite e => (EWrite (exp env e), loc)
+              | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
+
+              | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc)
     in
         {con = con, exp = exp}
     end
 
-fun con namedC c = #con (conAndExp (namedC, IM.empty)) [] c
-fun exp (namedC, namedE) e = #exp (conAndExp (namedC, namedE)) [] e
+fun con namedC env c = #con (conAndExp (namedC, IM.empty)) env c
+fun exp (namedC, namedE) env e = #exp (conAndExp (namedC, namedE)) env e
 
 fun reduce file =
     let
@@ -139,30 +342,34 @@
             case #1 d of
                 DCon (x, n, k, c) =>
                 let
-                    val c = con namedC c
+                    val c = con namedC [] c
                 in
                     ((DCon (x, n, k, c), loc),
                      (IM.insert (namedC, n, c), namedE))
                 end
               | DDatatype (x, n, ps, cs) =>
-                ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC) co)) cs), loc),
-                 st)
+                let
+                    val env = map (fn _ => UnknownC) ps
+                in
+                    ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC env) co)) cs), loc),
+                     st)
+                end
               | DVal (x, n, t, e, s) =>
                 let
-                    val t = con namedC t
-                    val e = exp (namedC, namedE) e
+                    val t = con namedC [] t
+                    val e = exp (namedC, namedE) [] e
                 in
                     ((DVal (x, n, t, e, s), loc),
                      (namedC, IM.insert (namedE, n, e)))
                 end
               | DValRec vis =>
-                ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC t, exp (namedC, namedE) e, s)) vis), loc),
+                ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC [] t, exp (namedC, namedE) [] e, s)) vis), loc),
                  st)
               | DExport _ => (d, st)
-              | DTable (s, n, c, s') => ((DTable (s, n, con namedC c, s'), loc), st)
+              | DTable (s, n, c, s') => ((DTable (s, n, con namedC [] c, s'), loc), st)
               | DSequence _ => (d, st)
               | DDatabase _ => (d, st)
-              | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC c, s'), loc), st)
+              | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC [] c, s'), loc), st)
 
         val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty) file
     in