Mercurial > urweb
changeset 1234:e799c8df3146
Catching lame FFI applications
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 13 Apr 2010 11:15:43 -0400 |
| parents | 8d1d2f7163c2 |
| children | a7b773f1d053 |
| files | src/iflow.sml |
| diffstat | 1 files changed, 19 insertions(+), 16 deletions(-) [+] |
line wrap: on
line diff
--- a/src/iflow.sml Tue Apr 13 10:40:55 2010 -0400 +++ b/src/iflow.sml Tue Apr 13 11:15:43 2010 -0400 @@ -2023,6 +2023,22 @@ in St.clearPaths st end + + fun doFfi (m, s, es) = + if m = "Basis" andalso SS.member (writers, s) then + let + val (es, st) = ListUtil.foldlMap (evalExp env) st es + in + (Recd [], foldl (fn (e, st) => addSent (St.ambient st, e, st)) st es) + end + else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then + default () + else + let + val (es, st) = ListUtil.foldlMap (evalExp env) st es + in + (Func (Other (m ^ "." ^ s), es), st) + end in case #1 e of EPrim p => (Const p, st) @@ -2044,21 +2060,8 @@ end | EFfi _ => default () - | EFfiApp (m, s, es) => - if m = "Basis" andalso SS.member (writers, s) then - let - val (es, st) = ListUtil.foldlMap (evalExp env) st es - in - (Recd [], foldl (fn (e, st) => addSent (St.ambient st, e, st)) st es) - end - else if Settings.isEffectful (m, s) andalso not (Settings.isBenignEffectful (m, s)) then - default () - else - let - val (es, st) = ListUtil.foldlMap (evalExp env) st es - in - (Func (Other (m ^ "." ^ s), es), st) - end + | EFfiApp x => doFfi x + | EApp ((EFfi (m, s), _), e) => doFfi (m, s, [e]) | EApp (e1, e2) => let @@ -2560,7 +2563,7 @@ | Control Case => " (case discriminee)" | Data => " (returned data value)"), Print.p_list p_atom hyps); - Print.preface ("DB", Cc.p_database cc); + (*Print.preface ("DB", Cc.p_database cc);*) false) end handle Cc.Contradiction => true) then ()