changeset 1234:e799c8df3146

Catching lame FFI applications
author Adam Chlipala <adamc@hcoop.net>
date Tue, 13 Apr 2010 11:15:43 -0400 (2010-04-13)
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
                                 ()