diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-03-28 13:59:03 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-03-28 13:59:03 -0400 |
commit | 8c7878bfb0622f9aa99b404e3793c5aa17443966 (patch) | |
tree | c065fade680b997035a01c27601f4a1838f3b1ac /src/elab_util.sml | |
parent | 1469fd94659b3562ea7e3c180e0366194717a287 (diff) |
Start of elaborating expressions
Diffstat (limited to 'src/elab_util.sml')
-rw-r--r-- | src/elab_util.sml | 66 |
1 files changed, 66 insertions, 0 deletions
diff --git a/src/elab_util.sml b/src/elab_util.sml index ef0e740f..c07ff667 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -162,6 +162,72 @@ fun exists {kind, con} k = end +structure Exp = struct + +fun mapfold {kind = fk, con = fc, exp = fe} = + let + val mfk = Kind.mapfold fk + val mfc = Con.mapfold {kind = fk, con = fc} + + fun mfe e acc = + S.bindP (mfe' e acc, fe) + + and mfe' (eAll as (e, loc)) = + case e of + ERel _ => S.return2 eAll + | ENamed _ => S.return2 eAll + | EApp (e1, e2) => + S.bind2 (mfe e1, + fn e1' => + S.map2 (mfe e2, + fn e2' => + (EApp (e1', e2'), loc))) + | EAbs (x, t, e) => + S.bind2 (mfc t, + fn t' => + S.map2 (mfe e, + fn e' => + (EAbs (x, t', e'), loc))) + + | ECApp (e, c) => + S.bind2 (mfe e, + fn e' => + S.map2 (mfc c, + fn c' => + (ECApp (e', c'), loc))) + | ECAbs (expl, x, k, e) => + S.bind2 (mfk k, + fn k' => + S.map2 (mfe e, + fn e' => + (ECAbs (expl, x, k', e'), loc))) + + | EError => S.return2 eAll + in + mfe + end + +fun exists {kind, con, exp} k = + case mapfold {kind = fn k => fn () => + if kind k then + S.Return () + else + S.Continue (k, ()), + con = fn c => fn () => + if con c then + S.Return () + else + S.Continue (c, ()), + exp = fn e => fn () => + if exp e then + S.Return () + else + S.Continue (e, ())} k () of + S.Return _ => true + | S.Continue _ => false + +end + structure E = ElabEnv fun declBinds env (d, _) = |