diff options
author | Adam Chlipala <adam@chlipala.net> | 2014-05-02 19:19:09 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2014-05-02 19:19:09 -0400 |
commit | a67b10880366304b1004dedcbf616ba70c1e196d (patch) | |
tree | bdccc17f7ec57e17465ac689d0f02d7b8c219a8b /src/elaborate.sml | |
parent | 8184fe8f3af43f4b614b79c411fc3b5578645983 (diff) |
New lessSafeFfi
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r-- | src/elaborate.sml | 15 |
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), |