From 1abc7fd02cd1a8183241ff9b3574ea6f3388ebcb Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 22 Jun 2008 14:23:05 -0400 Subject: Separate compilation and automatic basis importation --- lib/basis.lig | 3 + src/cjr_env.sig | 1 - src/cjr_env.sml | 11 ---- src/cloconv.sml | 2 +- src/compiler.sig | 48 ++++++++------- src/compiler.sml | 176 +++++++++++++++++++++++++++++++++++------------------- src/core_env.sig | 1 - src/core_env.sml | 13 ---- src/elab_env.sig | 1 - src/elab_env.sml | 10 ---- src/elaborate.sig | 2 +- src/elaborate.sml | 64 +++++++++++++++----- src/expl_env.sig | 1 - src/expl_env.sml | 14 ----- src/flat_env.sig | 1 - src/flat_env.sml | 11 ---- src/mono_env.sig | 1 - src/mono_env.sml | 11 ---- src/reduce.sml | 2 +- tests/split2.lac | 1 + 20 files changed, 195 insertions(+), 179 deletions(-) create mode 100644 lib/basis.lig create mode 100644 tests/split2.lac 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 -- cgit v1.2.3