summaryrefslogtreecommitdiff
path: root/src/reduce_local.sml
diff options
context:
space:
mode:
Diffstat (limited to 'src/reduce_local.sml')
-rw-r--r--src/reduce_local.sml179
1 files changed, 152 insertions, 27 deletions
diff --git a/src/reduce_local.sml b/src/reduce_local.sml
index 4c5ab52e..43317b9e 100644
--- a/src/reduce_local.sml
+++ b/src/reduce_local.sml
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2010, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
@@ -43,11 +43,15 @@ datatype env_item =
Unknown
| Known of exp
- | Lift of int
+ | UnknownC
+ | KnownC of con
+
+ | Lift of int * int
type env = env_item list
val deKnown = List.filter (fn Known _ => false
+ | KnownC _ => false
| _ => true)
datatype result = Yes of env | No | Maybe
@@ -120,39 +124,140 @@ fun match (env, p : pat, e : exp) =
match (env, p, e)
end
+fun con env (all as (c, loc)) =
+ ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*)
+ 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)
+ | TKFun (x, c2) => (TKFun (x, con env c2), loc)
+ | TRecord c => (TRecord (con env c), loc)
+
+ | CRel n =>
+ let
+ fun find (n', env, nudge, liftC) =
+ case env of
+ [] => raise Fail "Reduce.con: CRel"
+ | Unknown :: rest => find (n', rest, nudge, liftC)
+ | Known _ :: rest => find (n', rest, nudge, liftC)
+ | Lift (liftC', _) :: rest => find (n', rest, nudge + liftC',
+ liftC + liftC')
+ | UnknownC :: rest =>
+ if n' = 0 then
+ (CRel (n + nudge), loc)
+ else
+ find (n' - 1, rest, nudge, liftC + 1)
+ | KnownC c :: rest =>
+ if n' = 0 then
+ con (Lift (liftC, 0) :: rest) c
+ else
+ find (n' - 1, rest, nudge - 1, liftC)
+ in
+ (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
+ find (n, env, 0, 0)
+ end
+ | CNamed _ => all
+ | CFfi _ => all
+ | CApp (c1, c2) =>
+ let
+ val c1 = con env c1
+ val c2 = con env c2
+ in
+ case #1 c1 of
+ CAbs (_, _, b) =>
+ con (KnownC c2 :: deKnown env) b
+
+ | CApp ((CMap (dom, ran), _), f) =>
+ (case #1 c2 of
+ CRecord (_, []) => (CRecord (ran, []), loc)
+ | CRecord (_, (x, c) :: rest) =>
+ con (deKnown env)
+ (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc),
+ (CApp (c1, (CRecord (dom, rest), loc)), loc)), loc)
+ | _ => (CApp (c1, c2), loc))
+
+ | _ => (CApp (c1, c2), loc)
+ end
+ | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc)
+
+ | CKApp (c1, k) =>
+ let
+ val c1 = con env c1
+ in
+ case #1 c1 of
+ CKAbs (_, b) =>
+ con (deKnown env) b
+
+ | _ => (CKApp (c1, k), loc)
+ end
+ | CKAbs (x, b) => (CKAbs (x, con env b), loc)
+
+ | CName _ => all
+
+ | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc)
+ | CConcat (c1, c2) =>
+ let
+ val c1 = con env c1
+ val c2 = con env c2
+ in
+ case (#1 c1, #1 c2) of
+ (CRecord (k, xcs1), CRecord (_, xcs2)) =>
+ (CRecord (k, xcs1 @ xcs2), loc)
+ | (CRecord (_, []), _) => c2
+ | (_, CRecord (_, [])) => c1
+ | _ => (CConcat (c1, c2), loc)
+ end
+ | CMap _ => all
+
+ | CUnit => all
+
+ | CTuple cs => (CTuple (map (con env) cs), loc)
+ | CProj (c, n) =>
+ let
+ val c = con env c
+ in
+ case #1 c of
+ CTuple cs => List.nth (cs, n - 1)
+ | _ => (CProj (c, n), loc)
+ end)
+
+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}
+
fun exp env (all as (e, loc)) =
case e of
EPrim _ => all
| ERel n =>
let
- fun find (n', env, nudge, lift) =
+ fun find (n', env, nudge, liftC, liftE) =
case env of
[] => (ERel (n + nudge), loc)
- | Lift lift' :: rest => find (n', rest, nudge + lift', lift + lift')
+ | 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, lift + 1)
+ find (n' - 1, rest, nudge, liftC, liftE + 1)
| Known e :: rest =>
if n' = 0 then
((*print "SUBSTITUTING\n";*)
- exp (Lift lift :: rest) e)
+ exp (Lift (liftC, liftE) :: rest) e)
else
- find (n' - 1, rest, nudge - 1, lift)
+ find (n' - 1, rest, nudge - 1, liftC, liftE)
in
- find (n, env, 0, 0)
+ find (n, env, 0, 0, 0)
end
| ENamed _ => all
- | ECon (dk, pc, cs, eo) => (ECon (dk, pc, cs, Option.map (exp env) eo), loc)
+ | 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 ((ECApp ((ECAbs (_, _, (EAbs (_, (CRel 0, _), _,
- (ECon (dk, pc, [(CRel 0, loc)], SOME (ERel 0, _)), _)), _)), _),
- t), _), e) =>
- (ECon (dk, pc, [t], SOME (exp env e)), loc)
-
| EApp (e1, e2) =>
let
val e1 = exp env e1
@@ -163,21 +268,28 @@ fun exp env (all as (e, loc)) =
| _ => (EApp (e1, e2), loc)
end
- | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc)
+ | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (Unknown :: env) e), loc)
- | ECApp ((ECAbs (_, _, (ECon (dk, pc, [(CRel 0, loc)], NONE), _)), _), t) =>
- (ECon (dk, pc, [t], NONE), 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
- | ECApp (e, c) => (ECApp (exp env e, c), loc)
- | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc)
+ | 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) => (x, exp env e, t)) xcs), loc)
+ | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc)
| EField (e, c, others) =>
let
val e = exp env e
+ val c = con env c
fun default () = (EField (e, c, others), loc)
in
@@ -189,12 +301,16 @@ fun exp env (all as (e, loc)) =
| _ => default ()
end
- | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, c1, exp env e2, c2), loc)
- | ECut (e, c, others) => (ECut (exp env e, c, others), loc)
- | ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc)
+ | 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, others) =>
+ | ECase (e, pes, {disc = d, result = r}) =>
let
+ val others = {disc = con env d, result = con env r}
+
fun patBinds (p, _) =
case p of
PWild => 0
@@ -204,9 +320,18 @@ fun exp env (all as (e, loc)) =
| 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)
+
fun push () =
(ECase (exp env e,
- map (fn (p, e) => (p,
+ map (fn (p, e) => (pat p,
exp (List.tabulate (patBinds p,
fn _ => Unknown) @ env) e))
pes, others), loc)
@@ -226,9 +351,9 @@ fun exp env (all as (e, loc)) =
| EWrite e => (EWrite (exp env e), loc)
| EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
- | ELet (x, t, e1, e2) => (ELet (x, t, exp env e1, exp (Unknown :: env) e2), loc)
+ | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (Unknown :: env) e2), loc)
- | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, t), loc)
+ | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, con env t), loc)
fun reduce file =
let
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 20:18:57 +0000