diff options
| -rw-r--r-- | src/elab_util.sml | 12 | ||||
| -rw-r--r-- | src/reduce_local.sml | 303 |
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 |