diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2010-04-13 11:15:43 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2010-04-13 11:15:43 -0400 |
| commit | f865ba33dbdaa023deb71b8a68d8d0ffe3442a82 (patch) | |
| tree | 12bbf1c7df0d058382b36e01bcf0ca1899ca2ea6 /src/iflow.sml | |
| parent | 4ba4ade9e6ae86ed07aed13eafd7d71d9fadddb7 (diff) | |
Catching lame FFI applications
Diffstat (limited to 'src/iflow.sml')
| -rw-r--r-- | src/iflow.sml | 35 |
1 files changed, 19 insertions, 16 deletions
diff --git a/src/iflow.sml b/src/iflow.sml index 73ff07ea..f0dfd1f3 100644 --- a/src/iflow.sml +++ b/src/iflow.sml @@ -2023,6 +2023,22 @@ fun evalExp env (e as (_, loc), st) = 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 @@ fun evalExp env (e as (_, loc), st) = 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 @@ fun check file = | 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 () |