summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/basis.lig3
-rw-r--r--src/cjr_env.sig1
-rw-r--r--src/cjr_env.sml11
-rw-r--r--src/cloconv.sml2
-rw-r--r--src/compiler.sig48
-rw-r--r--src/compiler.sml176
-rw-r--r--src/core_env.sig1
-rw-r--r--src/core_env.sml13
-rw-r--r--src/elab_env.sig1
-rw-r--r--src/elab_env.sml10
-rw-r--r--src/elaborate.sig2
-rw-r--r--src/elaborate.sml64
-rw-r--r--src/expl_env.sig1
-rw-r--r--src/expl_env.sml14
-rw-r--r--src/flat_env.sig1
-rw-r--r--src/flat_env.sml11
-rw-r--r--src/mono_env.sig1
-rw-r--r--src/mono_env.sml11
-rw-r--r--src/reduce.sml2
-rw-r--r--tests/split2.lac1
20 files changed, 195 insertions, 179 deletions
diff --git a/lib/basis.lig b/lib/basis.lig
new file mode 100644
index 00000000..83aa9dc6
--- /dev/null
+++ b/lib/basis.lig
@@ -0,0 +1,3 @@
+type int
+type float
+type string
diff --git a/src/cjr_env.sig b/src/cjr_env.sig
index a3e666d7..6a9b0e71 100644
--- a/src/cjr_env.sig
+++ b/src/cjr_env.sig
@@ -30,7 +30,6 @@ signature CJR_ENV = sig
type env
val empty : env
- val basis : env
exception UnboundRel of int
exception UnboundNamed of int
diff --git a/src/cjr_env.sml b/src/cjr_env.sml
index 44dad97a..9431b956 100644
--- a/src/cjr_env.sml
+++ b/src/cjr_env.sml
@@ -121,15 +121,4 @@ fun declBinds env (d, _) =
| DFun (n, x, dom, ran, _) => pushF env n x dom ran
| DStruct _ => env
-fun bbind env x =
- case ElabEnv.lookupC ElabEnv.basis x of
- ElabEnv.NotBound => raise Fail "CjrEnv.bbind: Not bound"
- | ElabEnv.Rel _ => raise Fail "CjrEnv.bbind: Rel"
- | ElabEnv.Named (n, _) => pushTNamed env x n NONE
-
-val basis = empty
-val basis = bbind basis "int"
-val basis = bbind basis "float"
-val basis = bbind basis "string"
-
end
diff --git a/src/cloconv.sml b/src/cloconv.sml
index 98f86e5b..8e962f17 100644
--- a/src/cloconv.sml
+++ b/src/cloconv.sml
@@ -190,7 +190,7 @@ fun ccDecl ((d, loc), D) =
L.DVal (x, n, t, e) =>
let
val t = ccTyp t
- val (e, D) = ccExp E.basis (e, D)
+ val (e, D) = ccExp E.empty (e, D)
in
Ds.exp D (x, n, t, e)
end
diff --git a/src/compiler.sig b/src/compiler.sig
index 872ae0fc..5a421db7 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -29,31 +29,35 @@
signature COMPILER = sig
- val compile : string -> unit
+ type job = string list
+ val compile : job -> unit
val parseLig : string -> Source.sgn_item list option
val testLig : string -> unit
- val parse : string -> Source.file option
- val elaborate : ElabEnv.env -> string -> (Elab.file * ElabEnv.env) option
- val explify : ElabEnv.env -> string -> Expl.file option
- val corify : ElabEnv.env -> string -> Core.file option
- val shake' : ElabEnv.env -> string -> Core.file option
- val reduce : ElabEnv.env -> string -> Core.file option
- val shake : ElabEnv.env -> string -> Core.file option
- val monoize : ElabEnv.env -> CoreEnv.env -> string -> Mono.file option
- val cloconv : ElabEnv.env -> CoreEnv.env -> string -> Flat.file option
- val cjrize : ElabEnv.env -> CoreEnv.env -> string -> Cjr.file option
-
- val testParse : string -> unit
- val testElaborate : string -> unit
- val testExplify : string -> unit
- val testCorify : string -> unit
- val testShake' : string -> unit
- val testReduce : string -> unit
- val testShake : string -> unit
- val testMonoize : string -> unit
- val testCloconv : string -> unit
- val testCjrize : string -> unit
+ val parseLac : string -> Source.file option
+ val testLac : string -> unit
+
+ val parse : job -> Source.file option
+ val elaborate : job -> Elab.file option
+ val explify : job -> Expl.file option
+ val corify : job -> Core.file option
+ val shake' : job -> Core.file option
+ val reduce : job -> Core.file option
+ val shake : job -> Core.file option
+ val monoize : job -> Mono.file option
+ val cloconv : job -> Flat.file option
+ val cjrize : job -> Cjr.file option
+
+ val testParse : job -> unit
+ val testElaborate : job -> unit
+ val testExplify : job -> unit
+ val testCorify : job -> unit
+ val testShake' : job -> unit
+ val testReduce : job -> unit
+ val testShake : job -> unit
+ val testMonoize : job -> unit
+ val testCloconv : job -> unit
+ val testCjrize : job -> unit
end
diff --git a/src/compiler.sml b/src/compiler.sml
index ddfa122a..1b97e874 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -76,7 +76,7 @@ fun testLig fname =
print "\n")) sgis
(* The main parsing routine *)
-fun parse filename =
+fun parseLac filename =
let
val () = (ErrorMsg.resetErrors ();
ErrorMsg.resetPositioning filename)
@@ -98,30 +98,80 @@ fun parse filename =
end
handle LrParser.ParseError => NONE
-fun elaborate env filename =
- case parse filename of
+fun testLac fname =
+ case parseLac fname of
+ NONE => ()
+ | SOME file => (Print.print (SourcePrint.p_file file);
+ print "\n")
+
+type job = string list
+
+fun capitalize "" = ""
+ | capitalize s = str (Char.toUpper (String.sub (s, 0))) ^ String.extract (s, 1, NONE)
+
+fun parse fnames =
+ let
+ fun parseOne fname =
+ let
+ val mname = capitalize (OS.Path.file fname)
+ val lac = OS.Path.joinBaseExt {base = fname, ext = SOME "lac"}
+ val lig = OS.Path.joinBaseExt {base = fname, ext = SOME "lig"}
+
+ val sgnO =
+ if Posix.FileSys.access (lig, []) then
+ case parseLig lig of
+ NONE => NONE
+ | SOME sgis => SOME (Source.SgnConst sgis, {file = lig,
+ first = ErrorMsg.dummyPos,
+ last = ErrorMsg.dummyPos})
+ else
+ NONE
+
+ val loc = {file = lac,
+ first = ErrorMsg.dummyPos,
+ last = ErrorMsg.dummyPos}
+ in
+ case parseLac lac of
+ NONE => NONE
+ | SOME ds =>
+ SOME (Source.DStr (mname, sgnO, (Source.StrConst ds, loc)), loc)
+ end
+
+ val ds = List.mapPartial parseOne fnames
+ in
+ if ErrorMsg.anyErrors () then
+ NONE
+ else
+ SOME ds
+ end
+
+fun elaborate job =
+ case parseLig "lib/basis.lig" of
NONE => NONE
- | SOME file =>
- let
- val out = Elaborate.elabFile env file
- in
- if ErrorMsg.anyErrors () then
- NONE
- else
- SOME out
- end
+ | SOME empty =>
+ case parse job of
+ NONE => NONE
+ | SOME file =>
+ let
+ val out = Elaborate.elabFile empty ElabEnv.empty file
+ in
+ if ErrorMsg.anyErrors () then
+ NONE
+ else
+ SOME out
+ end
-fun explify eenv filename =
- case elaborate eenv filename of
+fun explify job =
+ case elaborate job of
NONE => NONE
- | SOME (file, _) =>
+ | SOME file =>
if ErrorMsg.anyErrors () then
NONE
else
SOME (Explify.explify file)
-fun corify eenv filename =
- case explify eenv filename of
+fun corify job =
+ case explify job of
NONE => NONE
| SOME file =>
if ErrorMsg.anyErrors () then
@@ -129,8 +179,8 @@ fun corify eenv filename =
else
SOME (Corify.corify file)
-fun shake' eenv filename =
- case corify eenv filename of
+fun shake' job =
+ case corify job of
NONE => NONE
| SOME file =>
if ErrorMsg.anyErrors () then
@@ -138,8 +188,8 @@ fun shake' eenv filename =
else
SOME (Shake.shake file)
-fun reduce eenv filename =
- case corify eenv filename of
+fun reduce job =
+ case corify job of
NONE => NONE
| SOME file =>
if ErrorMsg.anyErrors () then
@@ -147,8 +197,8 @@ fun reduce eenv filename =
else
SOME (Reduce.reduce (Shake.shake file))
-fun shake eenv filename =
- case reduce eenv filename of
+fun shake job =
+ case reduce job of
NONE => NONE
| SOME file =>
if ErrorMsg.anyErrors () then
@@ -156,17 +206,17 @@ fun shake eenv filename =
else
SOME (Shake.shake file)
-fun monoize eenv cenv filename =
- case shake eenv filename of
+fun monoize job =
+ case shake job of
NONE => NONE
| SOME file =>
if ErrorMsg.anyErrors () then
NONE
else
- SOME (Monoize.monoize cenv file)
+ SOME (Monoize.monoize CoreEnv.empty file)
-fun cloconv eenv cenv filename =
- case monoize eenv cenv filename of
+fun cloconv job =
+ case monoize job of
NONE => NONE
| SOME file =>
if ErrorMsg.anyErrors () then
@@ -174,8 +224,8 @@ fun cloconv eenv cenv filename =
else
SOME (Cloconv.cloconv file)
-fun cjrize eenv cenv filename =
- case cloconv eenv cenv filename of
+fun cjrize job =
+ case cloconv job of
NONE => NONE
| SOME file =>
if ErrorMsg.anyErrors () then
@@ -183,104 +233,104 @@ fun cjrize eenv cenv filename =
else
SOME (Cjrize.cjrize file)
-fun testParse filename =
- case parse filename of
+fun testParse job =
+ case parse job of
NONE => print "Failed\n"
| SOME file =>
(Print.print (SourcePrint.p_file file);
print "\n")
-fun testElaborate filename =
- (case elaborate ElabEnv.basis filename of
+fun testElaborate job =
+ (case elaborate job of
NONE => print "Failed\n"
- | SOME (file, _) =>
+ | SOME file =>
(print "Succeeded\n";
- Print.print (ElabPrint.p_file ElabEnv.basis file);
+ Print.print (ElabPrint.p_file ElabEnv.empty file);
print "\n"))
handle ElabEnv.UnboundNamed n =>
print ("Unbound named " ^ Int.toString n ^ "\n")
-fun testExplify filename =
- (case explify ElabEnv.basis filename of
+fun testExplify job =
+ (case explify job of
NONE => print "Failed\n"
| SOME file =>
- (Print.print (ExplPrint.p_file ExplEnv.basis file);
+ (Print.print (ExplPrint.p_file ExplEnv.empty file);
print "\n"))
handle ExplEnv.UnboundNamed n =>
print ("Unbound named " ^ Int.toString n ^ "\n")
-fun testCorify filename =
- (case corify ElabEnv.basis filename of
+fun testCorify job =
+ (case corify job of
NONE => print "Failed\n"
| SOME file =>
- (Print.print (CorePrint.p_file CoreEnv.basis file);
+ (Print.print (CorePrint.p_file CoreEnv.empty file);
print "\n"))
handle CoreEnv.UnboundNamed n =>
print ("Unbound named " ^ Int.toString n ^ "\n")
-fun testShake' filename =
- (case shake' ElabEnv.basis filename of
+fun testShake' job =
+ (case shake' job of
NONE => print "Failed\n"
| SOME file =>
- (Print.print (CorePrint.p_file CoreEnv.basis file);
+ (Print.print (CorePrint.p_file CoreEnv.empty file);
print "\n"))
handle CoreEnv.UnboundNamed n =>
print ("Unbound named " ^ Int.toString n ^ "\n")
-fun testReduce filename =
- (case reduce ElabEnv.basis filename of
+fun testReduce job =
+ (case reduce job of
NONE => print "Failed\n"
| SOME file =>
- (Print.print (CorePrint.p_file CoreEnv.basis file);
+ (Print.print (CorePrint.p_file CoreEnv.empty file);
print "\n"))
handle CoreEnv.UnboundNamed n =>
print ("Unbound named " ^ Int.toString n ^ "\n")
-fun testShake filename =
- (case shake ElabEnv.basis filename of
+fun testShake job =
+ (case shake job of
NONE => print "Failed\n"
| SOME file =>
- (Print.print (CorePrint.p_file CoreEnv.basis file);
+ (Print.print (CorePrint.p_file CoreEnv.empty file);
print "\n"))
handle CoreEnv.UnboundNamed n =>
print ("Unbound named " ^ Int.toString n ^ "\n")
-fun testMonoize filename =
- (case monoize ElabEnv.basis CoreEnv.basis filename of
+fun testMonoize job =
+ (case monoize job of
NONE => print "Failed\n"
| SOME file =>
- (Print.print (MonoPrint.p_file MonoEnv.basis file);
+ (Print.print (MonoPrint.p_file MonoEnv.empty file);
print "\n"))
handle MonoEnv.UnboundNamed n =>
print ("Unbound named " ^ Int.toString n ^ "\n")
-fun testCloconv filename =
- (case cloconv ElabEnv.basis CoreEnv.basis filename of
+fun testCloconv job =
+ (case cloconv job of
NONE => print "Failed\n"
| SOME file =>
- (Print.print (FlatPrint.p_file FlatEnv.basis file);
+ (Print.print (FlatPrint.p_file FlatEnv.empty file);
print "\n"))
handle FlatEnv.UnboundNamed n =>
print ("Unbound named " ^ Int.toString n ^ "\n")
-fun testCjrize filename =
- (case cjrize ElabEnv.basis CoreEnv.basis filename of
+fun testCjrize job =
+ (case cjrize job of
NONE => print "Failed\n"
| SOME file =>
- (Print.print (CjrPrint.p_file CjrEnv.basis file);
+ (Print.print (CjrPrint.p_file CjrEnv.empty file);
print "\n"))
handle CjrEnv.UnboundNamed n =>
print ("Unbound named " ^ Int.toString n ^ "\n")
-fun compile filename =
- case cjrize ElabEnv.basis CoreEnv.basis filename of
+fun compile job =
+ case cjrize job of
NONE => ()
| SOME file =>
let
val outf = TextIO.openOut "/tmp/lacweb.c"
val s = TextIOPP.openOut {dst = outf, wid = 80}
in
- Print.fprint s (CjrPrint.p_file CjrEnv.basis file);
+ Print.fprint s (CjrPrint.p_file CjrEnv.empty file);
TextIO.closeOut outf
end
diff --git a/src/core_env.sig b/src/core_env.sig
index 1766b3d1..56945972 100644
--- a/src/core_env.sig
+++ b/src/core_env.sig
@@ -32,7 +32,6 @@ signature CORE_ENV = sig
type env
val empty : env
- val basis : env
exception UnboundRel of int
exception UnboundNamed of int
diff --git a/src/core_env.sml b/src/core_env.sml
index 904c71f5..1ea687dc 100644
--- a/src/core_env.sml
+++ b/src/core_env.sml
@@ -124,17 +124,4 @@ fun declBinds env (d, _) =
DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
| DVal (x, n, t, e) => pushENamed env x n t (SOME e)
-val ktype = (KType, ErrorMsg.dummySpan)
-
-fun bbind env x =
- case ElabEnv.lookupC ElabEnv.basis x of
- ElabEnv.NotBound => raise Fail "CoreEnv.bbind: Not bound"
- | ElabEnv.Rel _ => raise Fail "CoreEnv.bbind: Rel"
- | ElabEnv.Named (n, _) => pushCNamed env x n ktype NONE
-
-val basis = empty
-val basis = bbind basis "int"
-val basis = bbind basis "float"
-val basis = bbind basis "string"
-
end
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 511497c4..ec97ebbf 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -33,7 +33,6 @@ signature ELAB_ENV = sig
type env
val empty : env
- val basis : env
exception UnboundRel of int
exception UnboundNamed of int
diff --git a/src/elab_env.sml b/src/elab_env.sml
index db9faa22..a673c523 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -418,14 +418,4 @@ fun projectStr env {sgn, str, field} =
| SgnError => SOME (SgnError, ErrorMsg.dummySpan)
| _ => NONE
-
-val ktype = (KType, ErrorMsg.dummySpan)
-
-fun bbind env x = #1 (pushCNamed env x ktype NONE)
-
-val basis = empty
-val basis = bbind basis "int"
-val basis = bbind basis "float"
-val basis = bbind basis "string"
-
end
diff --git a/src/elaborate.sig b/src/elaborate.sig
index 1d388122..0a7a6bbc 100644
--- a/src/elaborate.sig
+++ b/src/elaborate.sig
@@ -27,6 +27,6 @@
signature ELABORATE = sig
- val elabFile : ElabEnv.env -> Source.file -> Elab.file * ElabEnv.env
+ val elabFile : Source.sgn_item list -> ElabEnv.env -> Source.file -> Elab.file
end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 06e13237..2417ce6f 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -141,6 +141,10 @@ val eerror = (L'.EError, dummy)
val sgnerror = (L'.SgnError, dummy)
val strerror = (L'.StrError, dummy)
+val int = ref cerror
+val float = ref cerror
+val string = ref cerror
+
local
val count = ref 0
in
@@ -750,22 +754,14 @@ fun checkCon env e c1 c2 =
expError env (Unify (e, c1, c2, err))
fun primType env p =
- let
- val s = case p of
- P.Int _ => "int"
- | P.Float _ => "float"
- | P.String _ => "string"
- in
- case E.lookupC env s of
- E.NotBound => raise Fail ("Primitive type " ^ s ^ " unbound")
- | E.Rel _ => raise Fail ("Primitive type " ^ s ^ " bound as relative")
- | E.Named (n, (L'.KType, _)) => L'.CNamed n
- | E.Named _ => raise Fail ("Primitive type " ^ s ^ " bound at non-Type kind")
- end
+ case p of
+ P.Int _ => !int
+ | P.Float _ => !float
+ | P.String _ => !string
fun typeof env (e, loc) =
case e of
- L'.EPrim p => (primType env p, loc)
+ L'.EPrim p => primType env p
| L'.ERel n => #2 (E.lookupERel env n)
| L'.ENamed n => #2 (E.lookupENamed env n)
| L'.EModProj (n, ms, x) =>
@@ -825,7 +821,7 @@ fun elabExp env (e, loc) =
(e', t')
end
- | L.EPrim p => ((L'.EPrim p, loc), (primType env p, loc))
+ | L.EPrim p => ((L'.EPrim p, loc), primType env p)
| L.EVar ([], s) =>
(case E.lookupE env s of
E.NotBound =>
@@ -1478,6 +1474,44 @@ and elabStr env (str, loc) =
(strerror, sgnerror))
end
-val elabFile = ListUtil.foldlMap elabDecl
+fun elabFile basis env file =
+ let
+ val sgn = elabSgn env (L.SgnConst basis, ErrorMsg.dummySpan)
+ val (env', basis_n) = E.pushStrNamed env "Basis" sgn
+
+ val (ds, env') =
+ case #1 (hnormSgn env' sgn) of
+ L'.SgnConst sgis =>
+ ListUtil.foldlMap (fn ((sgi, loc), env') =>
+ case sgi of
+ L'.SgiConAbs (x, n, k) =>
+ ((L'.DCon (x, n, k, (L'.CModProj (basis_n, [], x), loc)), loc),
+ E.pushCNamedAs env' x n k NONE)
+ | L'.SgiCon (x, n, k, c) =>
+ ((L'.DCon (x, n, k, (L'.CModProj (basis_n, [], x), loc)), loc),
+ E.pushCNamedAs env' x n k (SOME c))
+ | L'.SgiVal (x, n, t) =>
+ ((L'.DVal (x, n, t, (L'.EModProj (basis_n, [], x), loc)), loc),
+ E.pushENamedAs env' x n t)
+ | L'.SgiStr (x, n, sgn) =>
+ ((L'.DStr (x, n, sgn, (L'.StrProj ((L'.StrVar basis_n, loc), x), loc)), loc),
+ E.pushStrNamedAs env' x n sgn))
+ env' sgis
+ | _ => raise Fail "Non-constant Basis signature"
+
+ fun discoverC r x =
+ case E.lookupC env' x of
+ E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis")
+ | E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis")
+ | E.Named (n, (_, loc)) => r := (L'.CNamed n, loc)
+
+ val () = discoverC int "int"
+ val () = discoverC float "float"
+ val () = discoverC string "string"
+
+ val (file, _) = ListUtil.foldlMap elabDecl env' file
+ in
+ (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
+ end
end
diff --git a/src/expl_env.sig b/src/expl_env.sig
index 7cb48095..00179e45 100644
--- a/src/expl_env.sig
+++ b/src/expl_env.sig
@@ -33,7 +33,6 @@ signature EXPL_ENV = sig
type env
val empty : env
- val basis : env
exception UnboundRel of int
exception UnboundNamed of int
diff --git a/src/expl_env.sml b/src/expl_env.sml
index 2ae167b2..b1bea90b 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -251,18 +251,4 @@ fun sgiBinds env (sgi, _) =
| SgiVal (x, n, t) => pushENamed env x n t
| SgiStr (x, n, sgn) => pushStrNamed env x n sgn
-
-val ktype = (KType, ErrorMsg.dummySpan)
-
-fun bbind env x =
- case ElabEnv.lookupC ElabEnv.basis x of
- ElabEnv.NotBound => raise Fail "CoreEnv.bbind: Not bound"
- | ElabEnv.Rel _ => raise Fail "CoreEnv.bbind: Rel"
- | ElabEnv.Named (n, _) => pushCNamed env x n ktype NONE
-
-val basis = empty
-val basis = bbind basis "int"
-val basis = bbind basis "float"
-val basis = bbind basis "string"
-
end
diff --git a/src/flat_env.sig b/src/flat_env.sig
index 30349c5b..9fc1fc57 100644
--- a/src/flat_env.sig
+++ b/src/flat_env.sig
@@ -30,7 +30,6 @@ signature FLAT_ENV = sig
type env
val empty : env
- val basis : env
exception UnboundRel of int
exception UnboundNamed of int
diff --git a/src/flat_env.sml b/src/flat_env.sml
index d09f0623..9c88a233 100644
--- a/src/flat_env.sml
+++ b/src/flat_env.sml
@@ -112,15 +112,4 @@ fun declBinds env (d, _) =
DVal (x, n, t, _) => pushENamed env x n t
| DFun (n, x, dom, ran, _) => pushF env n x dom ran
-fun bbind env x =
- case ElabEnv.lookupC ElabEnv.basis x of
- ElabEnv.NotBound => raise Fail "FlatEnv.bbind: Not bound"
- | ElabEnv.Rel _ => raise Fail "FlatEnv.bbind: Rel"
- | ElabEnv.Named (n, _) => pushTNamed env x n NONE
-
-val basis = empty
-val basis = bbind basis "int"
-val basis = bbind basis "float"
-val basis = bbind basis "string"
-
end
diff --git a/src/mono_env.sig b/src/mono_env.sig
index f3936998..f0d0b0a6 100644
--- a/src/mono_env.sig
+++ b/src/mono_env.sig
@@ -30,7 +30,6 @@ signature MONO_ENV = sig
type env
val empty : env
- val basis : env
exception UnboundRel of int
exception UnboundNamed of int
diff --git a/src/mono_env.sml b/src/mono_env.sml
index 60c6f609..66396264 100644
--- a/src/mono_env.sml
+++ b/src/mono_env.sml
@@ -85,15 +85,4 @@ fun declBinds env (d, _) =
case d of
DVal (x, n, t, e) => pushENamed env x n t (SOME e)
-fun bbind env x =
- case ElabEnv.lookupC ElabEnv.basis x of
- ElabEnv.NotBound => raise Fail "MonoEnv.bbind: Not bound"
- | ElabEnv.Rel _ => raise Fail "MonoEnv.bbind: Rel"
- | ElabEnv.Named (n, _) => pushTNamed env x n NONE
-
-val basis = empty
-val basis = bbind basis "int"
-val basis = bbind basis "float"
-val basis = bbind basis "string"
-
end
diff --git a/src/reduce.sml b/src/reduce.sml
index c4397743..4c36268c 100644
--- a/src/reduce.sml
+++ b/src/reduce.sml
@@ -156,6 +156,6 @@ and reduceExp env = U.Exp.mapB {kind = kind, con = con, exp = exp, bind = bind}
fun decl env d = d
-val reduce = U.File.mapB {kind = kind, con = con, exp = exp, decl = decl, bind = bind} CoreEnv.basis
+val reduce = U.File.mapB {kind = kind, con = con, exp = exp, decl = decl, bind = bind} CoreEnv.empty
end
diff --git a/tests/split2.lac b/tests/split2.lac
new file mode 100644
index 00000000..fb66e528
--- /dev/null
+++ b/tests/split2.lac
@@ -0,0 +1 @@
+val main = Split.x
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-31 23:34:37 +0000