summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-26 12:59:32 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-26 12:59:32 -0500
commitc767386f0b9d6af9ac3e306f73ea0608cb521c7b (patch)
treefa3c1d9e427cf780845f8cd77a83f6b5bf826044
parent125bd1380f059c9ee3541df4cbf0e12e2b6dcc70 (diff)
Most exp rules for new Reduce
-rw-r--r--src/reduce.sml231
1 files changed, 219 insertions, 12 deletions
diff --git a/src/reduce.sml b/src/reduce.sml
index 7531e0ca..3d117fb5 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -59,6 +59,7 @@ fun conAndExp (namedC, namedE) =
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 @@ fun conAndExp (namedC, namedE) =
| 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 @@ fun conAndExp (namedC, namedE) =
| _ => (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 @@ fun reduce file =
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