diff src/elab_util.sml @ 2010:403f0cc65b9c

New lessSafeFfi
author Adam Chlipala <adam@chlipala.net>
date Fri, 02 May 2014 19:19:09 -0400
parents 1aa9629e3a4c
children 22117edf8fd3
line wrap: on
line diff
--- a/src/elab_util.sml	Fri May 02 17:16:02 2014 -0400
+++ b/src/elab_util.sml	Fri May 02 19:19:09 2014 -0400
@@ -927,7 +927,8 @@
                                                    bind (ctx, NamedE (x, (CModProj (n, [], "css_class"), loc)))
                                                  | DTask _ => ctx
                                                  | DPolicy _ => ctx
-                                                 | DOnError _ => ctx,
+                                                 | DOnError _ => ctx
+                                                 | DFfi (x, _, _, t) => bind (ctx, NamedE (x, t)),
                                                mfd ctx d)) ctx ds,
                      fn ds' => (StrConst ds', loc))
               | StrVar _ => S.return2 strAll
@@ -1056,6 +1057,10 @@
                      fn e1' =>
                         (DPolicy e1', loc))
               | DOnError _ => S.return2 dAll
+              | DFfi (x, n, modes, t) =>
+                S.map2 (mfc ctx t,
+                        fn t' =>
+                           (DFfi (x, n, modes, t'), loc))
 
         and mfvi ctx (x, n, c, e) =
             S.bind2 (mfc ctx c,
@@ -1234,6 +1239,7 @@
       | DTask _ => 0
       | DPolicy _ => 0
       | DOnError _ => 0
+      | DFfi (_, n, _, _) => n
 and maxNameStr (str, _) =
     case str of
         StrConst ds => maxName ds