# HG changeset patch # User Adam Chlipala # Date 1271171743 14400 # Node ID e799c8df3146ea3fdbcd96d443e238bd2700181e # Parent 8d1d2f7163c250fb818fad5c4686799224047a6e Catching lame FFI applications diff -r 8d1d2f7163c2 -r e799c8df3146 src/iflow.sml --- 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 ()