summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/core.sml3
-rw-r--r--src/core_print.sml9
-rw-r--r--src/core_util.sml6
-rw-r--r--src/corify.sml108
-rw-r--r--src/elab.sml1
-rw-r--r--src/elab_env.sml1
-rw-r--r--src/elab_print.sml9
-rw-r--r--src/elaborate.sml10
-rw-r--r--src/expl.sml1
-rw-r--r--src/expl_env.sml1
-rw-r--r--src/expl_print.sml9
-rw-r--r--src/explify.sml1
-rw-r--r--src/lacweb.grm3
-rw-r--r--src/lacweb.lex5
-rw-r--r--src/monoize.sml3
-rw-r--r--src/source.sml1
-rw-r--r--src/source_print.sml9
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 15:58:27 +0000