# HG changeset patch # User Adam Chlipala # Date 1214141249 14400 # Node ID 0a5c312de09af9a08a565e7bcf762e8708ee1d29 # Parent ac4c0b4111babfee251c47c19369bff4e58bfe56 Start of FFI diff -r ac4c0b4111ba -r 0a5c312de09a src/core.sml --- a/src/core.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/core.sml Sun Jun 22 09:27:29 2008 -0400 @@ -44,6 +44,7 @@ | CRel of int | CNamed of int + | CFfi of string * string | CApp of con * con | CAbs of string * kind * con @@ -58,6 +59,8 @@ EPrim of Prim.t | ERel of int | ENamed of int + | EFfi of string * string + | EFfiApp of string * string * exp list | EApp of exp * exp | EAbs of string * con * con * exp | ECApp of exp * con diff -r ac4c0b4111ba -r 0a5c312de09a src/core_print.sml --- a/src/core_print.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/core_print.sml Sun Jun 22 09:27:29 2008 -0400 @@ -90,6 +90,7 @@ else string (#1 (E.lookupCNamed env n))) handle E.UnboundNamed _ => string ("UNBOUNDN_" ^ Int.toString n)) + | CFfi (m, x) => box [string "FFI(", string m, string ".", string x, string ")"] | CApp (c1, c2) => parenIf par (box [p_con env c1, space, @@ -156,6 +157,14 @@ else string (#1 (E.lookupENamed env n))) handle E.UnboundNamed _ => string ("UNBOUNDN_" ^ Int.toString n)) + | EFfi (m, x) => box [string "FFI(", string m, string ".", string x, string ")"] + | EFfiApp (m, x, es) => box [string "FFI(", + string m, + string ".", + string x, + string "(", + p_list (p_exp env) es, + string "))"] | EApp (e1, e2) => parenIf par (box [p_exp env e1, space, p_exp' true env e2]) diff -r ac4c0b4111ba -r 0a5c312de09a src/core_util.sml --- a/src/core_util.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/core_util.sml Sun Jun 22 09:27:29 2008 -0400 @@ -109,6 +109,7 @@ | CRel _ => S.return2 cAll | CNamed _ => S.return2 cAll + | CFfi _ => S.return2 cAll | CApp (c1, c2) => S.bind2 (mfc ctx c1, fn c1' => @@ -216,6 +217,11 @@ EPrim _ => S.return2 eAll | ERel _ => S.return2 eAll | ENamed _ => S.return2 eAll + | EFfi _ => S.return2 eAll + | EFfiApp (m, x, es) => + S.map2 (ListUtil.mapfold (fn e => mfe ctx e) es, + fn es' => + (EFfiApp (m, x, es'), loc)) | EApp (e1, e2) => S.bind2 (mfe ctx e1, fn e1' => diff -r ac4c0b4111ba -r 0a5c312de09a src/corify.sml --- a/src/corify.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/corify.sml Sun Jun 22 09:27:29 2008 -0400 @@ -60,10 +60,15 @@ val enter : t -> t val leave : t -> {outer : t, inner : t} + val ffi : string -> t val bindCore : t -> string -> int -> t * int val lookupCoreById : t -> int -> int option - val lookupCoreByName : t -> string -> int + + datatype core = + Normal of int + | Ffi of string + val lookupCoreByName : t -> string -> core val bindStr : t -> string -> int -> t -> t val lookupStrById : t -> int -> t @@ -74,11 +79,11 @@ val lookupFunctorByName : string * t -> int * L.str end = struct -datatype flattening = F of { - core : int SM.map, - strs : flattening SM.map, - funs : (int * L.str) SM.map -} +datatype flattening = + FNormal of {core : int SM.map, + strs : flattening SM.map, + funs : (int * L.str) SM.map} + | FFfi of string type t = { core : int IM.map, @@ -92,22 +97,25 @@ core = IM.empty, strs = IM.empty, funs = IM.empty, - current = F { core = SM.empty, strs = SM.empty, funs = SM.empty }, + current = FNormal { core = SM.empty, strs = SM.empty, funs = SM.empty }, nested = [] } +datatype core = + Normal of int + | Ffi of string + fun bindCore {core, strs, funs, current, nested} s n = let val n' = alloc () val current = - let - val F {core, strs, funs} = current - in - F {core = SM.insert (core, s, n'), - strs = strs, - funs = funs} - end + case current of + FFfi _ => raise Fail "Binding inside FFfi" + | FNormal {core, strs, funs} => + FNormal {core = SM.insert (core, s, n'), + strs = strs, + funs = funs} in ({core = IM.insert (core, n, n'), strs = strs, @@ -119,18 +127,21 @@ fun lookupCoreById ({core, ...} : t) n = IM.find (core, n) -fun lookupCoreByName ({current = F {core, ...}, ...} : t) x = - case SM.find (core, x) of - NONE => raise Fail "Corify.St.lookupCoreByName" - | SOME n => n +fun lookupCoreByName ({current, ...} : t) x = + case current of + FFfi m => Ffi m + | FNormal {core, ...} => + case SM.find (core, x) of + NONE => raise Fail "Corify.St.lookupCoreByName" + | SOME n => Normal n fun enter {core, strs, funs, current, nested} = {core = core, strs = strs, funs = funs, - current = F {core = SM.empty, - strs = SM.empty, - funs = SM.empty}, + current = FNormal {core = SM.empty, + strs = SM.empty, + funs = SM.empty}, nested = current :: nested} fun dummy f = {core = IM.empty, @@ -148,45 +159,51 @@ inner = dummy current} | leave _ = raise Fail "Corify.St.leave" -fun bindStr ({core, strs, funs, current = F {core = mcore, strs = mstrs, funs = mfuns}, nested} : t) +fun ffi m = dummy (FFfi m) + +fun bindStr ({core, strs, funs, current = FNormal {core = mcore, strs = mstrs, funs = mfuns}, nested} : t) x n ({current = f, ...} : t) = {core = core, strs = IM.insert (strs, n, f), funs = funs, - current = F {core = mcore, + current = FNormal {core = mcore, strs = SM.insert (mstrs, x, f), funs = mfuns}, nested = nested} + | bindStr _ _ _ _ = raise Fail "Corify.St.bindStr" fun lookupStrById ({strs, ...} : t) n = case IM.find (strs, n) of NONE => raise Fail "Corify.St.lookupStrById" | SOME f => dummy f -fun lookupStrByName (m, {current = F {strs, ...}, ...} : t) = - case SM.find (strs, m) of - NONE => raise Fail "Corify.St.lookupStrByName" - | SOME f => dummy f +fun lookupStrByName (m, {current = FNormal {strs, ...}, ...} : t) = + (case SM.find (strs, m) of + NONE => raise Fail "Corify.St.lookupStrByName" + | SOME f => dummy f) + | lookupStrByName _ = raise Fail "Corify.St.lookupStrByName" -fun bindFunctor ({core, strs, funs, current = F {core = mcore, strs = mstrs, funs = mfuns}, nested} : t) +fun bindFunctor ({core, strs, funs, current = FNormal {core = mcore, strs = mstrs, funs = mfuns}, nested} : t) x n na str = {core = core, strs = strs, funs = IM.insert (funs, n, (na, str)), - current = F {core = mcore, - strs = mstrs, - funs = SM.insert (mfuns, x, (na, str))}, + current = FNormal {core = mcore, + strs = mstrs, + funs = SM.insert (mfuns, x, (na, str))}, nested = nested} + | bindFunctor _ _ _ _ _ = raise Fail "Corify.St.bindFunctor" fun lookupFunctorById ({funs, ...} : t) n = case IM.find (funs, n) of NONE => raise Fail "Corify.St.lookupFunctorById" | SOME v => v -fun lookupFunctorByName (m, {current = F {funs, ...}, ...} : t) = - case SM.find (funs, m) of - NONE => raise Fail "Corify.St.lookupFunctorByName" - | SOME v => v +fun lookupFunctorByName (m, {current = FNormal {funs, ...}, ...} : t) = + (case SM.find (funs, m) of + NONE => raise Fail "Corify.St.lookupFunctorByName" + | SOME v => v) + | lookupFunctorByName _ = raise Fail "Corify.St.lookupFunctorByName" end @@ -213,9 +230,10 @@ let val st = St.lookupStrById st m val st = foldl St.lookupStrByName st ms - val n = St.lookupCoreByName st x in - (L'.CNamed n, loc) + case St.lookupCoreByName st x of + St.Normal n => (L'.CNamed n, loc) + | St.Ffi m => (L'.CFfi (m, x), loc) end | L.CApp (c1, c2) => (L'.CApp (corifyCon st c1, corifyCon st c2), loc) @@ -239,9 +257,10 @@ let val st = St.lookupStrById st m val st = foldl St.lookupStrByName st ms - val n = St.lookupCoreByName st x in - (L'.ENamed n, loc) + case St.lookupCoreByName st x of + St.Normal n => (L'.ENamed n, loc) + | St.Ffi m => (L'.EFfi (m, x), loc) end | L.EApp (e1, e2) => (L'.EApp (corifyExp st e1, corifyExp st e2), loc) | L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon st dom, corifyCon st ran, corifyExp st e1), loc) @@ -280,6 +299,14 @@ (ds, st) end + | L.DFfiStr (x, n, _) => + let + val st = St.bindStr st x n (St.ffi x) + in + ([], st) + end + + and corifyStr ((str, _), st) = case str of L.StrConst ds => @@ -324,7 +351,8 @@ L.DCon (_, n', _, _) => Int.max (n, n') | L.DVal (_, n', _ , _) => Int.max (n, n') | L.DSgn (_, n', _) => Int.max (n, n') - | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str))) + | L.DStr (_, n', _, str) => Int.max (n, Int.max (n', maxNameStr str)) + | L.DFfiStr (_, n', _) => Int.max (n, n')) 0 ds and maxNameStr (str, _) = diff -r ac4c0b4111ba -r 0a5c312de09a src/elab.sml --- a/src/elab.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/elab.sml Sun Jun 22 09:27:29 2008 -0400 @@ -103,6 +103,7 @@ | DVal of string * int * con * exp | DSgn of string * int * sgn | DStr of string * int * sgn * str + | DFfiStr of string * int * sgn and str' = StrConst of decl list diff -r ac4c0b4111ba -r 0a5c312de09a src/elab_env.sml --- a/src/elab_env.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/elab_env.sml Sun Jun 22 09:27:29 2008 -0400 @@ -290,6 +290,7 @@ | DVal (x, n, t, _) => pushENamedAs env x n t | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn + | DFfiStr (x, n, sgn) => pushStrNamedAs env x n sgn fun sgiBinds env (sgi, _) = case sgi of diff -r ac4c0b4111ba -r 0a5c312de09a src/elab_print.sml --- a/src/elab_print.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/elab_print.sml Sun Jun 22 09:27:29 2008 -0400 @@ -379,6 +379,15 @@ string "=", space, p_str env str] + | DFfiStr (x, n, sgn) => box [string "extern", + space, + string "structure", + space, + p_named x n, + space, + string ":", + space, + p_sgn env sgn] and p_str env (str, _) = case str of diff -r ac4c0b4111ba -r 0a5c312de09a src/elaborate.sml --- a/src/elaborate.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/elaborate.sml Sun Jun 22 09:27:29 2008 -0400 @@ -1160,6 +1160,7 @@ | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc) | L'.DSgn _ => NONE | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc) + | L'.DFfiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, sgn), loc) fun subSgn env sgn1 (sgn2 as (_, loc2)) = case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of @@ -1403,6 +1404,15 @@ ((L'.DStr (x, n, sgn', str'), loc), env') end + + | L.DFfiStr (x, sgn) => + let + val sgn' = elabSgn env sgn + + val (env', n) = E.pushStrNamed env x sgn' + in + ((L'.DFfiStr (x, n, sgn'), loc), env') + end end and elabStr env (str, loc) = diff -r ac4c0b4111ba -r 0a5c312de09a src/expl.sml --- a/src/expl.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/expl.sml Sun Jun 22 09:27:29 2008 -0400 @@ -90,6 +90,7 @@ | DVal of string * int * con * exp | DSgn of string * int * sgn | DStr of string * int * sgn * str + | DFfiStr of string * int * sgn and str' = StrConst of decl list diff -r ac4c0b4111ba -r 0a5c312de09a src/expl_env.sml --- a/src/expl_env.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/expl_env.sml Sun Jun 22 09:27:29 2008 -0400 @@ -242,6 +242,7 @@ | DVal (x, n, t, _) => pushENamed env x n t | DSgn (x, n, sgn) => pushSgnNamed env x n sgn | DStr (x, n, sgn, _) => pushStrNamed env x n sgn + | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn fun sgiBinds env (sgi, _) = case sgi of diff -r ac4c0b4111ba -r 0a5c312de09a src/expl_print.sml --- a/src/expl_print.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/expl_print.sml Sun Jun 22 09:27:29 2008 -0400 @@ -361,6 +361,15 @@ string "=", space, p_str env str] + | DFfiStr (x, n, sgn) => box [string "extern", + space, + string "structure", + space, + p_named x n, + space, + string ":", + space, + p_sgn env sgn] and p_str env (str, _) = case str of diff -r ac4c0b4111ba -r 0a5c312de09a src/explify.sml --- a/src/explify.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/explify.sml Sun Jun 22 09:27:29 2008 -0400 @@ -103,6 +103,7 @@ | L.DSgn (x, n, sgn) => (L'.DSgn (x, n, explifySgn sgn), loc) | L.DStr (x, n, sgn, str) => (L'.DStr (x, n, explifySgn sgn, explifyStr str), loc) + | L.DFfiStr (x, n, sgn) => (L'.DFfiStr (x, n, explifySgn sgn), loc) and explifyStr (str, loc) = case str of diff -r ac4c0b4111ba -r 0a5c312de09a src/lacweb.grm --- a/src/lacweb.grm Thu Jun 19 18:13:33 2008 -0400 +++ b/src/lacweb.grm Sun Jun 22 09:27:29 2008 -0400 @@ -44,7 +44,7 @@ | TYPE | NAME | ARROW | LARROW | DARROW | FN | PLUSPLUS | DOLLAR - | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE + | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN %nonterm file of decl list @@ -119,6 +119,7 @@ (DStr (CSYMBOL1, NONE, (StrFun (CSYMBOL2, sgn1, SOME sgn2, str), s (FUNCTORleft, strright))), s (FUNCTORleft, strright)) + | EXTERN STRUCTURE CSYMBOL COLON sgn (DFfiStr (CSYMBOL, sgn), s (EXTERNleft, sgnright)) sgn : sgntm (sgntm) | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn diff -r ac4c0b4111ba -r 0a5c312de09a src/lacweb.lex --- a/src/lacweb.lex Thu Jun 19 18:13:33 2008 -0400 +++ b/src/lacweb.lex Sun Jun 22 09:27:29 2008 -0400 @@ -67,8 +67,8 @@ %full %s COMMENT STRING; -id = [a-z_][A-Za-z0-9_]*; -cid = [A-Z][A-Za-z0-9_]*; +id = [a-z_][A-Za-z0-9_']*; +cid = [A-Z][A-Za-z0-9_']*; ws = [\ \t\012]; intconst = [0-9]+; realconst = [0-9]+\.[0-9]*; @@ -135,6 +135,7 @@ "end" => (Tokens.END (yypos, yypos + size yytext)); "functor" => (Tokens.FUNCTOR (yypos, yypos + size yytext)); "where" => (Tokens.WHERE (yypos, yypos + size yytext)); + "extern" => (Tokens.EXTERN (yypos, yypos + size yytext)); "Type" => (Tokens.TYPE (yypos, yypos + size yytext)); "Name" => (Tokens.NAME (yypos, yypos + size yytext)); diff -r ac4c0b4111ba -r 0a5c312de09a src/monoize.sml --- a/src/monoize.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/monoize.sml Sun Jun 22 09:27:29 2008 -0400 @@ -63,6 +63,7 @@ | L.CRel _ => poly () | L.CNamed n => (L'.TNamed n, loc) + | L.CFfi _ => raise Fail "Monoize CFfi" | L.CApp _ => poly () | L.CAbs _ => poly () @@ -85,6 +86,8 @@ L.EPrim p => (L'.EPrim p, loc) | L.ERel n => (L'.ERel n, loc) | L.ENamed n => (L'.ENamed n, loc) + | L.EFfi _ => raise Fail "Monoize EFfi" + | L.EFfiApp _ => raise Fail "Monoize EFfiApp" | L.EApp (e1, e2) => (L'.EApp (monoExp env e1, monoExp env e2), loc) | L.EAbs (x, dom, ran, e) => (L'.EAbs (x, monoType env dom, monoType env ran, monoExp (Env.pushERel env x dom) e), loc) diff -r ac4c0b4111ba -r 0a5c312de09a src/source.sml --- a/src/source.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/source.sml Sun Jun 22 09:27:29 2008 -0400 @@ -97,6 +97,7 @@ | DVal of string * con option * exp | DSgn of string * sgn | DStr of string * sgn option * str + | DFfiStr of string * sgn and str' = StrConst of decl list diff -r ac4c0b4111ba -r 0a5c312de09a src/source_print.sml --- a/src/source_print.sml Thu Jun 19 18:13:33 2008 -0400 +++ b/src/source_print.sml Sun Jun 22 09:27:29 2008 -0400 @@ -335,6 +335,15 @@ string "=", space, p_str str] + | DFfiStr (x, sgn) => box [string "extern", + space, + string "structure", + space, + string x, + space, + string ":", + space, + p_sgn sgn] and p_str (str, _) = case str of diff -r ac4c0b4111ba -r 0a5c312de09a tests/ffi.lac --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/ffi.lac Sun Jun 22 09:27:29 2008 -0400 @@ -0,0 +1,12 @@ +extern structure Lib : sig + type t + val x : t +end + +type t' = Lib.t +val x' : t' = Lib.x + +structure Lib' = Lib + +type t'' = Lib'.t +val x'' : t'' = Lib'.x