Mercurial > urweb

changeset 48:0a5c312de09a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of FFI
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Jun 2008 09:27:29 -0400
parents ac4c0b4111ba
children 874e877d2c51
files src/core.sml src/core_print.sml src/core_util.sml src/corify.sml src/elab.sml src/elab_env.sml src/elab_print.sml src/elaborate.sml src/expl.sml src/expl_env.sml src/expl_print.sml src/explify.sml src/lacweb.grm src/lacweb.lex src/monoize.sml src/source.sml src/source_print.sml tests/ffi.lac
diffstat 18 files changed, 149 insertions(+), 43 deletions(-) [+]
line wrap: on
line diff
--- 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
--- 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])
--- 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' =>
--- 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, _) =
--- 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
--- 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
--- 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
--- 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) =
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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 @@
 <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));
--- 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)
--- 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
--- 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
--- /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