diff options
| -rw-r--r-- | src/core_print.sml | 2 | ||||
| -rw-r--r-- | src/core_util.sig | 5 | ||||
| -rw-r--r-- | src/core_util.sml | 8 | ||||
| -rw-r--r-- | src/elab_print.sml | 2 | ||||
| -rw-r--r-- | src/reduce.sml | 72 | ||||
| -rw-r--r-- | src/source_print.sml | 2 | ||||
| -rw-r--r-- | tests/reduce.lac | 1 |
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"} |