Start of FFI

17 files changed, 137 insertions, 43 deletions

diff --git a/src/core.sml b/src/core.sml
index fa06f56a..613e0c41 100644
--- a/src/core.sml
+++ b/src/core.sml
@@ -44,6 +44,7 @@ datatype con' =
 
        | CRel of int
        | CNamed of int
+       | CFfi of string * string
        | CApp of con * con
        | CAbs of string * kind * con
 
@@ -58,6 +59,8 @@ datatype exp' =
          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 --git a/src/core_print.sml b/src/core_print.sml
index 3bcb982e..a3fde909 100644
--- a/src/core_print.sml
+++ b/src/core_print.sml
@@ -90,6 +90,7 @@ fun p_con' par env (c, _) =
           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 @@ fun p_exp' par env (e, _) =
           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 --git a/src/core_util.sml b/src/core_util.sml
index 8d9a6529..b3e266af 100644
--- a/src/core_util.sml
+++ b/src/core_util.sml
@@ -109,6 +109,7 @@ fun mapfoldB {kind = fk, con = fc, bind} =
 
               | 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
                 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 --git a/src/corify.sml b/src/corify.sml
index e3ea791e..6a80881a 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -60,10 +60,15 @@ structure St : sig
 
     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 @@ structure St : sig
     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 @@ val empty = {
     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 bindCore {core, strs, funs, current, nested} s n =
 
 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 @@ fun leave {core, strs, funs, current, nested = m1 :: rest} =
          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 @@ fun corifyCon st (c, loc) =
         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 @@ fun corifyExp st (e, loc) =
         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 @@ fun corifyDecl ((d, loc : EM.span), st) =
             (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 @@ fun maxName ds = foldl (fn ((d, _), n) =>
                                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 --git a/src/elab.sml b/src/elab.sml
index e675144d..99468146 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -103,6 +103,7 @@ datatype decl' =
        | 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 --git a/src/elab_env.sml b/src/elab_env.sml
index 6f20733a..db9faa22 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -290,6 +290,7 @@ fun declBinds env (d, _) =
       | 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 --git a/src/elab_print.sml b/src/elab_print.sml
index cdbb652d..85271a89 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -379,6 +379,15 @@ fun p_decl env ((d, _) : decl) =
                                       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 --git a/src/elaborate.sml b/src/elaborate.sml
index d87fadd1..06e13237 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1160,6 +1160,7 @@ fun sgiOfDecl (d, loc) =
       | 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 @@ fun elabDecl ((d, loc), env) =
 
                 ((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 --git a/src/expl.sml b/src/expl.sml
index 295aa9b2..49633d27 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -90,6 +90,7 @@ datatype decl' =
        | 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 --git a/src/expl_env.sml b/src/expl_env.sml
index 27f02b73..2ae167b2 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -242,6 +242,7 @@ fun declBinds env (d, _) =
       | 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 --git a/src/expl_print.sml b/src/expl_print.sml
index 0e7f66eb..900a4063 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -361,6 +361,15 @@ fun p_decl env ((d, _) : decl) =
                                       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 --git a/src/explify.sml b/src/explify.sml
index 2d52083a..00d58fcf 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -103,6 +103,7 @@ fun explifyDecl (d, loc : EM.span) =
 
       | 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 --git a/src/lacweb.grm b/src/lacweb.grm
index 85a58eb8..17bc31cc 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -44,7 +44,7 @@ val s = ErrorMsg.spanOf
  | 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 @@ decl   : CON SYMBOL EQ cexp             (DCon (SYMBOL, NONE, cexp), s (CONleft,
                                         (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 --git a/src/lacweb.lex b/src/lacweb.lex
index 337da093..76cf26c0 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -67,8 +67,8 @@ val strStart = ref 0
 %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 @@ realconst = [0-9]+\.[0-9]*;
 <INITIAL> "end"       => (Tokens.END (yypos, yypos + size yytext));
 <INITIAL> "functor"   => (Tokens.FUNCTOR (yypos, yypos + size yytext));
 <INITIAL> "where"     => (Tokens.WHERE (yypos, yypos + size yytext));
+<INITIAL> "extern"    => (Tokens.EXTERN (yypos, yypos + size yytext));
 
 <INITIAL> "Type"      => (Tokens.TYPE (yypos, yypos + size yytext));
 <INITIAL> "Name"      => (Tokens.NAME (yypos, yypos + size yytext));
diff --git a/src/monoize.sml b/src/monoize.sml
index c3e9e806..1dbbf211 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -63,6 +63,7 @@ fun monoType env (all as (c, loc)) =
 
           | 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 @@ fun monoExp env (all as (e, loc)) =
             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 --git a/src/source.sml b/src/source.sml
index b8aa33aa..6397bd71 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -97,6 +97,7 @@ datatype decl' =
        | 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 --git a/src/source_print.sml b/src/source_print.sml
index 1522e6da..1ea2b837 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -335,6 +335,15 @@ fun p_decl ((d, _) : decl) =
                                         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