summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-08 16:02:26 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-08 16:02:26 -0400
commit813e9aa4d196962f47c784aeedeaf1cddf54dc4f (patch)
treead51ff72c12a5e8287bee29501a6c7953879fdd9
parente18863bcabc5d185b7fe1fc750bdf0bbdb5a4f78 (diff)
Beta reductions for expressions
-rw-r--r--src/core_print.sml2
-rw-r--r--src/core_util.sig5
-rw-r--r--src/core_util.sml8
-rw-r--r--src/elab_print.sml2
-rw-r--r--src/reduce.sml72
-rw-r--r--src/source_print.sml2
-rw-r--r--tests/reduce.lac1
7 files changed, 88 insertions, 4 deletions
diff --git a/src/core_print.sml b/src/core_print.sml
index c035ceef..02aeba69 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -185,7 +185,7 @@ fun p_exp' par env (e, _) =
| ERecord xes => box [string "{",
p_list (fn (x, e) =>
- box [p_con env x,
+ box [p_name env x,
space,
string "=",
space,
diff --git a/src/core_util.sig b/src/core_util.sig
index 07350798..45ee7dfd 100644
--- a/src/core_util.sig
+++ b/src/core_util.sig
@@ -80,6 +80,11 @@ structure Exp : sig
con : Core.con' -> Core.con',
exp : Core.exp' -> Core.exp'}
-> Core.exp -> Core.exp
+ val mapB : {kind : Core.kind' -> Core.kind',
+ con : 'context -> Core.con' -> Core.con',
+ exp : 'context -> Core.exp' -> Core.exp',
+ bind : 'context * binder -> 'context}
+ -> 'context -> (Core.exp -> Core.exp)
val exists : {kind : Core.kind' -> bool,
con : Core.con' -> bool,
exp : Core.exp' -> bool} -> Core.exp -> bool
diff --git a/src/core_util.sml b/src/core_util.sml
index c3e8250b..4f0de447 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -266,6 +266,14 @@ fun mapfold {kind = fk, con = fc, exp = fe} =
exp = fn () => fe,
bind = fn ((), _) => ()} ()
+fun mapB {kind, con, exp, bind} ctx e =
+ case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
+ con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
+ exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
+ bind = bind} ctx e () of
+ S.Continue (e, ()) => e
+ | S.Return _ => raise Fail "CoreUtil.Exp.mapB: Impossible"
+
fun map {kind, con, exp} e =
case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
con = fn c => fn () => S.Continue (con c, ()),
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 6f1c0148..c8e37e48 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -200,7 +200,7 @@ fun p_exp' par env (e, _) =
| ERecord xes => box [string "{",
p_list (fn (x, e) =>
- box [p_con env x,
+ box [p_name env x,
space,
string "=",
space,
diff --git a/src/reduce.sml b/src/reduce.sml
index a558778c..7a5b7367 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -49,6 +49,62 @@ val subConInCon =
bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
| (ctx, _) => ctx}
+val liftExpInExp =
+ U.Exp.mapB {kind = fn k => k,
+ con = fn _ => fn c => c,
+ exp = fn bound => fn e =>
+ case e of
+ ERel xn =>
+ if xn < bound then
+ e
+ else
+ ERel (xn + 1)
+ | _ => e,
+ bind = fn (bound, U.Exp.RelE _) => bound + 1
+ | (bound, _) => bound}
+
+val subExpInExp =
+ U.Exp.mapB {kind = fn k => k,
+ con = fn _ => fn c => c,
+ exp = fn (xn, rep) => fn e =>
+ case e of
+ ERel xn' =>
+ if xn = xn' then
+ #1 rep
+ else
+ e
+ | _ => e,
+ bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
+ | (ctx, _) => ctx}
+
+val liftConInExp =
+ U.Exp.mapB {kind = fn k => k,
+ con = fn bound => fn c =>
+ case c of
+ CRel xn =>
+ if xn < bound then
+ c
+ else
+ CRel (xn + 1)
+ | _ => c,
+ exp = fn _ => fn e => e,
+ bind = fn (bound, U.Exp.RelC _) => bound + 1
+ | (bound, _) => bound}
+
+val subConInExp =
+ U.Exp.mapB {kind = fn k => k,
+ con = fn (xn, rep) => fn c =>
+ case c of
+ CRel xn' =>
+ if xn = xn' then
+ #1 rep
+ else
+ c
+ | _ => c,
+ exp = fn _ => fn e => e,
+ bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep)
+ | (ctx, _) => ctx}
+
fun bindC (env, b) =
case b of
U.Con.Rel (x, k) => E.pushCRel env x k
@@ -76,7 +132,21 @@ fun con env c =
and reduceCon env = U.Con.mapB {kind = kind, con = con, bind = bindC} env
-fun exp env e = e
+fun exp env e =
+ case e of
+ ENamed n =>
+ (case E.lookupENamed env n of
+ (_, _, SOME e') => #1 e'
+ | _ => e)
+
+ | EApp ((EAbs (_, _, e1), loc), e2) =>
+ #1 (reduceExp env (subExpInExp (0, e2) e1))
+ | ECApp ((ECAbs (_, _, e1), loc), c) =>
+ #1 (reduceExp env (subConInExp (0, c) e1))
+
+ | _ => e
+
+and reduceExp env = U.Exp.mapB {kind = kind, con = con, exp = exp, bind = bind} env
fun decl env d = d
diff --git a/src/source_print.sml b/src/source_print.sml
index 9c3b870b..28146f1f 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -184,7 +184,7 @@ fun p_exp' par (e, _) =
| ERecord xes => box [string "{",
p_list (fn (x, e) =>
- box [p_con x,
+ box [p_name x,
space,
string "=",
space,
diff --git a/tests/reduce.lac b/tests/reduce.lac
index a6fa1e94..2585862d 100644
--- a/tests/reduce.lac
+++ b/tests/reduce.lac
@@ -17,3 +17,4 @@ con c7 = apply (fst int) string
val grab = fn n :: Name => fn t :: Type => fn fs :: {Type} =>
fn x : $([n = t] ++ fs) => x
val grabA = grab[#A][int][[B = string]]
+val test_grabA = grabA {A = 6, B = "13"}