summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/elab_util.sml12
-rw-r--r--src/reduce_local.sml303
2 files changed, 164 insertions, 151 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 0cdb9cc1..aa5bc6a4 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -541,11 +541,13 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
and mfed ctx (dAll as (d, loc)) =
case d of
EDVal (p, t, e) =>
- S.bind2 (mfc ctx t,
- fn t' =>
- S.map2 (mfe ctx e,
- fn e' =>
- (EDVal (p, t', e'), loc)))
+ S.bind2 (mfp ctx p,
+ fn p' =>
+ S.bind2 (mfc ctx t,
+ fn t' =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (EDVal (p', t', e'), loc))))
| EDValRec vis =>
let
val ctx = foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis
diff --git a/src/reduce_local.sml b/src/reduce_local.sml
index 06f49fef..aee8e7a9 100644
--- a/src/reduce_local.sml
+++ b/src/reduce_local.sml
@@ -54,6 +54,14 @@ val deKnown = List.filter (fn Known _ => false
| KnownC _ => false
| _ => true)
+fun p_env_item ei =
+ Print.PD.string (case ei of
+ Unknown => "?"
+ | Known _ => "K"
+ | UnknownC => "C?"
+ | KnownC _ => "CK"
+ | Lift _ => "^")
+
datatype result = Yes of env | No | Maybe
fun match (env, p : pat, e : exp) =
@@ -124,7 +132,8 @@ fun match (env, p : pat, e : exp) =
end
fun con env (all as (c, loc)) =
- ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*)
+ ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all),
+ ("env", Print.p_list p_env_item env)];*)
case c of
TFun (c1, c2) => (TFun (con env c1, con env c2), loc)
| TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc)
@@ -139,7 +148,7 @@ fun con env (all as (c, loc)) =
| Unknown :: rest => find (n', rest, nudge, liftC)
| Known _ :: rest => find (n', rest, nudge, liftC)
| Lift (liftC', _) :: rest => find (n', rest, nudge + liftC',
- liftC + liftC')
+ liftC + liftC')
| UnknownC :: rest =>
if n' = 0 then
(CRel (n + nudge), loc)
@@ -228,154 +237,156 @@ fun patCon pc =
kind = kind}
fun exp env (all as (e, loc)) =
- case e of
- EPrim _ => all
- | ERel n =>
- let
- fun find (n', env, nudge, liftC, liftE) =
- case env of
- [] => (ERel (n + nudge), loc)
- | Lift (liftC', liftE') :: rest => find (n', rest, nudge + liftE', liftC + liftC', liftE + liftE')
- | UnknownC :: rest => find (n', rest, nudge, liftC + 1, liftE)
- | KnownC _ :: rest => find (n', rest, nudge, liftC, liftE)
- | Unknown :: rest =>
- if n' = 0 then
- (ERel (n + nudge), loc)
- else
- find (n' - 1, rest, nudge, liftC, liftE + 1)
- | Known e :: rest =>
- if n' = 0 then
- ((*print "SUBSTITUTING\n";*)
- exp (Lift (liftC, liftE) :: rest) e)
- else
- find (n' - 1, rest, nudge - 1, liftC, liftE)
- in
- find (n, env, 0, 0, 0)
- end
- | ENamed _ => all
- | 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 (fn (e, t) => (exp env e, con env t)) es), loc)
-
- | EApp (e1, e2) =>
- let
- val e1 = exp env e1
- val e2 = exp env e2
- in
- case #1 e1 of
- EAbs (_, _, _, b) => exp (Known e2 :: deKnown env) b
- | _ => (EApp (e1, e2), loc)
- end
-
- | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (Unknown :: 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 :: deKnown env) b
- | _ => (ECApp (e, c), loc)
- end
-
- | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc)
-
- | EKApp (e, k) => (EKApp (exp env e, k), loc)
- | EKAbs (x, e) => (EKAbs (x, exp 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 = f, rest = r}) =>
- let
- val e = exp env e
- val c = con env c
-
- fun default () = (EField (e, c, {field = con env f, rest = con env r}), 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) => (EConcat (exp env e1, con env c1, exp env e2, con env c2), loc)
- | ECut (e, c, {field = f, rest = r}) => (ECut (exp env e,
- con env c,
- {field = con env f, rest = con env r}), loc)
- | ECutMulti (e, c, {rest = r}) => (ECutMulti (exp env e, con env c, {rest = con env r}), loc)
-
- | ECase (e, pes, {disc = d, result = r}) =>
- let
- val others = {disc = con env d, result = con env r}
-
- fun patBinds (p, _) =
- case p of
- 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
- 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)
-
- fun push () =
- (ECase (exp env e,
- map (fn (p, e) => (pat p,
- exp (List.tabulate (patBinds p,
- fn _ => Unknown) @ env) e))
- pes, others), loc)
-
- fun search pes =
- case pes of
- [] => push ()
- | (p, body) :: pes =>
- case match (env, p, e) of
- No => search pes
- | Maybe => push ()
- | Yes env' => exp env' body
- in
- search pes
- 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 (Unknown :: env) e2), loc)
-
- | EServerCall (n, es, t, fm) => (EServerCall (n, map (exp env) es, con env t, fm), loc)
+ ((*Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all)];*)
+ case e of
+ EPrim _ => all
+ | ERel n =>
+ let
+ fun find (n', env, nudge, liftC, liftE) =
+ case env of
+ [] => (ERel (n + nudge), loc)
+ | Lift (liftC', liftE') :: rest => find (n', rest, nudge + liftE', liftC + liftC', liftE + liftE')
+ | UnknownC :: rest => find (n', rest, nudge, liftC + 1, liftE)
+ | KnownC _ :: rest => find (n', rest, nudge, liftC, liftE)
+ | Unknown :: rest =>
+ if n' = 0 then
+ (ERel (n + nudge), loc)
+ else
+ find (n' - 1, rest, nudge, liftC, liftE + 1)
+ | Known e :: rest =>
+ if n' = 0 then
+ ((*print "SUBSTITUTING\n";*)
+ exp (Lift (liftC, liftE) :: rest) e)
+ else
+ find (n' - 1, rest, nudge - 1, liftC, liftE)
+ in
+ find (n, env, 0, 0, 0)
+ end
+ | ENamed _ => all
+ | 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 (fn (e, t) => (exp env e, con env t)) es), loc)
+
+ | EApp (e1, e2) =>
+ let
+ val e1 = exp env e1
+ val e2 = exp env e2
+ in
+ case #1 e1 of
+ EAbs (_, _, _, b) => exp (Known e2 :: deKnown env) b
+ | _ => (EApp (e1, e2), loc)
+ end
+
+ | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (Unknown :: 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 :: deKnown env) b
+ | _ => (ECApp (e, c), loc)
+ end
+
+ | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc)
+
+ | EKApp (e, k) => (EKApp (exp env e, k), loc)
+ | EKAbs (x, e) => (EKAbs (x, exp 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 = f, rest = r}) =>
+ let
+ val e = exp env e
+ val c = con env c
+
+ fun default () = (EField (e, c, {field = con env f, rest = con env r}), 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) => (EConcat (exp env e1, con env c1, exp env e2, con env c2), loc)
+ | ECut (e, c, {field = f, rest = r}) => (ECut (exp env e,
+ con env c,
+ {field = con env f, rest = con env r}), loc)
+ | ECutMulti (e, c, {rest = r}) => (ECutMulti (exp env e, con env c, {rest = con env r}), loc)
+
+ | ECase (e, pes, {disc = d, result = r}) =>
+ let
+ val others = {disc = con env d, result = con env r}
+
+ fun patBinds (p, _) =
+ case p of
+ 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
+ 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)
+
+ fun push () =
+ (ECase (exp env e,
+ map (fn (p, e) => (pat p,
+ exp (List.tabulate (patBinds p,
+ fn _ => Unknown) @ env) e))
+ pes, others), loc)
+
+ fun search pes =
+ case pes of
+ [] => push ()
+ | (p, body) :: pes =>
+ case match (env, p, e) of
+ No => search pes
+ | Maybe => push ()
+ | Yes env' => exp env' body
+ in
+ search pes
+ 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 (Unknown :: env) e2), loc)
+
+ | EServerCall (n, es, t, fm) => (EServerCall (n, map (exp env) es, con env t, fm), loc))
fun reduce file =
let
fun doDecl (d as (_, loc)) =
- case #1 d of
- DCon _ => d
- | DDatatype _ => d
- | DVal (x, n, t, e, s) =>
- let
- val e = exp [] e
- in
- (DVal (x, n, t, e, s), loc)
- end
- | DValRec vis =>
- (DValRec (map (fn (x, n, t, e, s) => (x, n, t, exp [] e, s)) vis), loc)
- | DExport _ => d
- | DTable _ => d
- | DSequence _ => d
- | DView _ => d
- | DDatabase _ => d
- | DCookie _ => d
- | DStyle _ => d
- | DTask (e1, e2) => (DTask (exp [] e1, exp [] e2), loc)
- | DPolicy e1 => (DPolicy (exp [] e1), loc)
- | DOnError _ => d
+ ((*Print.prefaces "decl" [("d", CorePrint.p_decl CoreEnv.empty d)];*)
+ case #1 d of
+ DCon _ => d
+ | DDatatype _ => d
+ | DVal (x, n, t, e, s) =>
+ let
+ val e = exp [] e
+ in
+ (DVal (x, n, t, e, s), loc)
+ end
+ | DValRec vis =>
+ (DValRec (map (fn (x, n, t, e, s) => (x, n, t, exp [] e, s)) vis), loc)
+ | DExport _ => d
+ | DTable _ => d
+ | DSequence _ => d
+ | DView _ => d
+ | DDatabase _ => d
+ | DCookie _ => d
+ | DStyle _ => d
+ | DTask (e1, e2) => (DTask (exp [] e1, exp [] e2), loc)
+ | DPolicy e1 => (DPolicy (exp [] e1), loc)
+ | DOnError _ => d)
in
map doDecl file
end