Beta reductions for expressions

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"}