Mercurial > urweb
changeset 21:067029c748e9
Beta reductions for expressions
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 08 Jun 2008 16:02:26 -0400 |
| parents | 1ab48e37d0ef |
| children | d8850cc06d24 |
| files | src/core_print.sml src/core_util.sig src/core_util.sml src/elab_print.sml src/reduce.sml src/source_print.sml tests/reduce.lac |
| diffstat | 7 files changed, 88 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- 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,
--- 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
--- 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, ()),
--- 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,
--- 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