Mercurial > urweb
changeset 56:d3cc191cb25f
Separate compilation and automatic basis importation
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 22 Jun 2008 14:23:05 -0400 |
parents | 5c97b7cd912b |
children | 618b7054f931 |
files | lib/basis.lig src/cjr_env.sig src/cjr_env.sml src/cloconv.sml src/compiler.sig src/compiler.sml src/core_env.sig src/core_env.sml src/elab_env.sig src/elab_env.sml src/elaborate.sig src/elaborate.sml src/expl_env.sig src/expl_env.sml src/flat_env.sig src/flat_env.sml src/mono_env.sig src/mono_env.sml src/reduce.sml tests/split2.lac |
diffstat | 20 files changed, 195 insertions(+), 179 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/basis.lig Sun Jun 22 14:23:05 2008 -0400 @@ -0,0 +1,3 @@ +type int +type float +type string
--- a/src/cjr_env.sig Sun Jun 22 11:04:10 2008 -0400 +++ b/src/cjr_env.sig Sun Jun 22 14:23:05 2008 -0400 @@ -30,7 +30,6 @@ type env val empty : env - val basis : env exception UnboundRel of int exception UnboundNamed of int
--- a/src/cjr_env.sml Sun Jun 22 11:04:10 2008 -0400 +++ b/src/cjr_env.sml Sun Jun 22 14:23:05 2008 -0400 @@ -121,15 +121,4 @@ | 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
--- a/src/cloconv.sml Sun Jun 22 11:04:10 2008 -0400 +++ b/src/cloconv.sml Sun Jun 22 14:23:05 2008 -0400 @@ -190,7 +190,7 @@ 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
--- a/src/compiler.sig Sun Jun 22 11:04:10 2008 -0400 +++ b/src/compiler.sig Sun Jun 22 14:23:05 2008 -0400 @@ -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 parseLac : string -> Source.file option + val testLac : string -> unit - 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 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
--- a/src/compiler.sml Sun Jun 22 11:04:10 2008 -0400 +++ b/src/compiler.sml Sun Jun 22 14:23:05 2008 -0400 @@ -76,7 +76,7 @@ print "\n")) sgis (* The main parsing routine *) -fun parse filename = +fun parseLac filename = let val () = (ErrorMsg.resetErrors (); ErrorMsg.resetPositioning filename) @@ -98,30 +98,80 @@ 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 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 job = + case elaborate job of NONE => NONE | SOME file => - let - val out = Elaborate.elabFile env file - in - if ErrorMsg.anyErrors () then - NONE - else - SOME out - end - -fun explify eenv filename = - case elaborate eenv filename of - NONE => NONE - | 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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
--- a/src/core_env.sig Sun Jun 22 11:04:10 2008 -0400 +++ b/src/core_env.sig Sun Jun 22 14:23:05 2008 -0400 @@ -32,7 +32,6 @@ type env val empty : env - val basis : env exception UnboundRel of int exception UnboundNamed of int
--- a/src/core_env.sml Sun Jun 22 11:04:10 2008 -0400 +++ b/src/core_env.sml Sun Jun 22 14:23:05 2008 -0400 @@ -124,17 +124,4 @@ 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
--- a/src/elab_env.sig Sun Jun 22 11:04:10 2008 -0400 +++ b/src/elab_env.sig Sun Jun 22 14:23:05 2008 -0400 @@ -33,7 +33,6 @@ type env val empty : env - val basis : env exception UnboundRel of int exception UnboundNamed of int
--- a/src/elab_env.sml Sun Jun 22 11:04:10 2008 -0400 +++ b/src/elab_env.sml Sun Jun 22 14:23:05 2008 -0400 @@ -418,14 +418,4 @@ | 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
--- a/src/elaborate.sig Sun Jun 22 11:04:10 2008 -0400 +++ b/src/elaborate.sig Sun Jun 22 14:23:05 2008 -0400 @@ -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
--- a/src/elaborate.sml Sun Jun 22 11:04:10 2008 -0400 +++ b/src/elaborate.sml Sun Jun 22 14:23:05 2008 -0400 @@ -141,6 +141,10 @@ 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 @@ 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 @@ (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 @@ (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
--- a/src/expl_env.sig Sun Jun 22 11:04:10 2008 -0400 +++ b/src/expl_env.sig Sun Jun 22 14:23:05 2008 -0400 @@ -33,7 +33,6 @@ type env val empty : env - val basis : env exception UnboundRel of int exception UnboundNamed of int
--- a/src/expl_env.sml Sun Jun 22 11:04:10 2008 -0400 +++ b/src/expl_env.sml Sun Jun 22 14:23:05 2008 -0400 @@ -251,18 +251,4 @@ | 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
--- a/src/flat_env.sig Sun Jun 22 11:04:10 2008 -0400 +++ b/src/flat_env.sig Sun Jun 22 14:23:05 2008 -0400 @@ -30,7 +30,6 @@ type env val empty : env - val basis : env exception UnboundRel of int exception UnboundNamed of int
--- a/src/flat_env.sml Sun Jun 22 11:04:10 2008 -0400 +++ b/src/flat_env.sml Sun Jun 22 14:23:05 2008 -0400 @@ -112,15 +112,4 @@ 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
--- a/src/mono_env.sig Sun Jun 22 11:04:10 2008 -0400 +++ b/src/mono_env.sig Sun Jun 22 14:23:05 2008 -0400 @@ -30,7 +30,6 @@ type env val empty : env - val basis : env exception UnboundRel of int exception UnboundNamed of int
--- a/src/mono_env.sml Sun Jun 22 11:04:10 2008 -0400 +++ b/src/mono_env.sml Sun Jun 22 14:23:05 2008 -0400 @@ -85,15 +85,4 @@ 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
--- a/src/reduce.sml Sun Jun 22 11:04:10 2008 -0400 +++ b/src/reduce.sml Sun Jun 22 14:23:05 2008 -0400 @@ -156,6 +156,6 @@ 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