aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2014-05-02 19:19:09 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2014-05-02 19:19:09 -0400
commit0c83e8f7c345a27be3cae77eeb2d7cb8658e5e9c (patch)
treebdccc17f7ec57e17465ac689d0f02d7b8c219a8b /src/elaborate.sml
parent77b4d9b9397aefc41ae0c6465a75874c497d945c (diff)
New lessSafeFfi
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml15
1 files changed, 15 insertions, 0 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 97ac610b..d492883f 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2999,6 +2999,7 @@ and sgiOfDecl (d, loc) =
| L'.DTask _ => []
| L'.DPolicy _ => []
| L'.DOnError _ => []
+ | L'.DFfi (x, n, _, t) => [(L'.SgiVal (x, n, t), loc)]
and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) =
((*prefaces "subSgn" [("sgn1", p_sgn env sgn1),
@@ -4298,6 +4299,20 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
([(L'.DOnError (n, ms, s), loc)], (env, denv, gs))
end)
+ | L.DFfi (x, modes, t) =>
+ let
+ val () = if Settings.getLessSafeFfi () then
+ ()
+ else
+ ErrorMsg.errorAt loc "To enable 'ffi' declarations, the .urp directive 'lessSafeFfi' is mandatory."
+
+ val (t', _, gs1) = elabCon (env, denv) t
+ val t' = normClassConstraint env t'
+ val (env', n) = E.pushENamed env x t'
+ in
+ ([(L'.DFfi (x, n, modes, t'), loc)], (env', denv, enD gs1 @ gs))
+ end
+
(*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*)
in
(*prefaces "/elabDecl" [("d", SourcePrint.p_decl dAll),