From 3f497272d327fea2638006c751d812dbbc449c78 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 1 Nov 2008 11:17:29 -0400 Subject: Elaborating 'let' --- src/elab_util.sml | 42 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) (limited to 'src/elab_util.sml') diff --git a/src/elab_util.sml b/src/elab_util.sml index 247e2b3a..28fe8f22 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -352,6 +352,48 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = | EError => S.return2 eAll | EUnif (ref (SOME e)) => mfe ctx e | EUnif _ => S.return2 eAll + + | ELet (des, e) => + let + val (des, ctx) = foldl (fn (ed, (des, ctx)) => + (S.bind2 (des, + fn des' => + S.map2 (mfed ctx ed, + fn ed' => des' @ [ed'])), + case #1 ed of + EDVal (x, t, _) => bind (ctx, RelE (x, t)) + | EDValRec vis => + foldl (fn ((x, t, _), env) => bind (ctx, RelE (x, t))) ctx vis)) + (S.return2 [], ctx) des + in + S.bind2 (des, + fn des' => + S.map2 (mfe ctx e, + fn e' => + (ELet (des', e'), loc))) + end + + and mfed ctx (dAll as (d, loc)) = + case d of + EDVal vi => + S.map2 (mfvi ctx vi, + fn vi' => + (EDVal vi', loc)) + | EDValRec vis => + let + val ctx = foldl (fn ((x, t, _), env) => bind (ctx, RelE (x, t))) ctx vis + in + S.map2 (ListUtil.mapfold (mfvi ctx) vis, + fn vis' => + (EDValRec vis', loc)) + end + + and mfvi ctx (x, c, e) = + S.bind2 (mfc ctx c, + fn c' => + S.map2 (mfe ctx e, + fn e' => + (x, c', e'))) in mfe end -- cgit v1.2.3