# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1212955346 14400
# Node ID 067029c748e94e92a37deed5f2765542352016ac
# Parent  1ab48e37d0eff1fff090605d5495fb657b9bdd3f
Beta reductions for expressions

diff -r 1ab48e37d0ef -r 067029c748e9 src/core_print.sml
--- a/src/core_print.sml	Sun Jun 08 15:47:44 2008 -0400
+++ b/src/core_print.sml	Sun Jun 08 16:02:26 2008 -0400
@@ -185,7 +185,7 @@
 
       | ERecord xes => box [string "{",
                             p_list (fn (x, e) =>
-                                       box [p_con env x,
+                                       box [p_name env x,
                                             space,
                                             string "=",
                                             space,
diff -r 1ab48e37d0ef -r 067029c748e9 src/core_util.sig
--- a/src/core_util.sig	Sun Jun 08 15:47:44 2008 -0400
+++ b/src/core_util.sig	Sun Jun 08 16:02:26 2008 -0400
@@ -80,6 +80,11 @@
                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 -r 1ab48e37d0ef -r 067029c748e9 src/core_util.sml
--- a/src/core_util.sml	Sun Jun 08 15:47:44 2008 -0400
+++ b/src/core_util.sml	Sun Jun 08 16:02:26 2008 -0400
@@ -266,6 +266,14 @@
               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 -r 1ab48e37d0ef -r 067029c748e9 src/elab_print.sml
--- a/src/elab_print.sml	Sun Jun 08 15:47:44 2008 -0400
+++ b/src/elab_print.sml	Sun Jun 08 16:02:26 2008 -0400
@@ -200,7 +200,7 @@
 
       | ERecord xes => box [string "{",
                             p_list (fn (x, e) =>
-                                       box [p_con env x,
+                                       box [p_name env x,
                                             space,
                                             string "=",
                                             space,
diff -r 1ab48e37d0ef -r 067029c748e9 src/reduce.sml
--- a/src/reduce.sml	Sun Jun 08 15:47:44 2008 -0400
+++ b/src/reduce.sml	Sun Jun 08 16:02:26 2008 -0400
@@ -49,6 +49,62 @@
                 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 @@
 
 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 -r 1ab48e37d0ef -r 067029c748e9 src/source_print.sml
--- a/src/source_print.sml	Sun Jun 08 15:47:44 2008 -0400
+++ b/src/source_print.sml	Sun Jun 08 16:02:26 2008 -0400
@@ -184,7 +184,7 @@
 
       | ERecord xes => box [string "{",
                             p_list (fn (x, e) =>
-                                       box [p_con x,
+                                       box [p_name x,
                                             space,
                                             string "=",
                                             space,
diff -r 1ab48e37d0ef -r 067029c748e9 tests/reduce.lac
--- a/tests/reduce.lac	Sun Jun 08 15:47:44 2008 -0400
+++ b/tests/reduce.lac	Sun Jun 08 16:02:26 2008 -0400
@@ -17,3 +17,4 @@
 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"}