summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/compiler.sig4
-rw-r--r--src/compiler.sml53
2 files changed, 37 insertions, 20 deletions
diff --git a/src/compiler.sig b/src/compiler.sig
index 2b08bff4..e34b771e 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008-2009, Adam Chlipala
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
@@ -73,6 +73,7 @@ signature COMPILER = sig
val parseUr : (string, Source.file) phase
val parseUrs : (string, Source.sgn_item list) phase
val parseUrp : (string, job) phase
+ val parseUrp' : (string, {Job : job, Libs : string list}) phase
val parse : (job, Source.file) phase
val elaborate : (Source.file, Elab.file) phase
@@ -104,6 +105,7 @@ signature COMPILER = sig
val sqlify : (Mono.file, Cjr.file) phase
val toParseJob : (string, job) transform
+ val toParseJob' : (string, {Job : job, Libs : string list}) transform
val toParse : (string, Source.file) transform
val toElaborate : (string, Elab.file) transform
val toUnnest : (string, Elab.file) transform
diff --git a/src/compiler.sml b/src/compiler.sml
index baf8ddac..95ad80ad 100644
--- a/src/compiler.sml
+++ b/src/compiler.sml
@@ -104,20 +104,6 @@ fun transform (ph : ('src, 'dst) phase) name = {
end
}
-fun op o (tr2 : ('b, 'c) transform, tr1 : ('a, 'b) transform) = {
- func = fn input => case #func tr1 input of
- NONE => NONE
- | SOME v => #func tr2 v,
- print = #print tr2,
- time = fn (input, pmap) => let
- val (ro, pmap) = #time tr1 (input, pmap)
- in
- case ro of
- NONE => (NONE, pmap)
- | SOME v => #time tr2 (v, pmap)
- end
-}
-
fun check (tr : ('src, 'dst) transform) x = (ErrorMsg.resetErrors ();
ignore (#func tr x))
@@ -284,9 +270,10 @@ structure M = BinaryMapFn(struct
val compare = String.compare
end)
-fun parseUrp' fname =
+fun parseUrp' accLibs fname =
let
val pathmap = ref (M.insert (M.empty, "", Config.libUr))
+ val bigLibs = ref []
fun pu filename =
let
@@ -431,7 +418,10 @@ fun parseUrp' fname =
dbms = mergeO #2 (#dbms old, #dbms new)
}
in
- foldr (fn (job', job) => merge (job, job')) job (!libs)
+ if accLibs then
+ foldr (fn (job', job) => merge (job, job')) job (!libs)
+ else
+ job
end
fun parsePkind s =
@@ -568,7 +558,10 @@ fun parseUrp' fname =
fkind := {action = Settings.Deny, kind = kind, pattern = pattern} :: !fkind
end
| _ => ErrorMsg.error "Bad 'deny' syntax")
- | "library" => libs := pu (relify arg) :: !libs
+ | "library" => if accLibs then
+ libs := pu (relify arg) :: !libs
+ else
+ bigLibs := relify arg :: !bigLibs
| "path" =>
(case String.fields (fn ch => ch = #"=") arg of
[n, v] => pathmap := M.insert (!pathmap, n, v)
@@ -597,15 +590,37 @@ fun parseUrp' fname =
job
end
in
- pu fname
+ {Job = pu fname, Libs = !bigLibs}
end
+fun p_job' {Job = j, Libs = _ : string list} = p_job j
+
val parseUrp = {
- func = parseUrp',
+ func = #Job o parseUrp' false,
print = p_job
}
+val parseUrp' = {
+ func = parseUrp' true,
+ print = p_job'
+}
+
val toParseJob = transform parseUrp "parseJob"
+val toParseJob' = transform parseUrp' "parseJob'"
+
+fun op o (tr2 : ('b, 'c) transform, tr1 : ('a, 'b) transform) = {
+ func = fn input => case #func tr1 input of
+ NONE => NONE
+ | SOME v => #func tr2 v,
+ print = #print tr2,
+ time = fn (input, pmap) => let
+ val (ro, pmap) = #time tr1 (input, pmap)
+ in
+ case ro of
+ NONE => (NONE, pmap)
+ | SOME v => #time tr2 (v, pmap)
+ end
+}
fun capitalize "" = ""
| capitalize s = str (Char.toUpper (String.sub (s, 0))) ^ String.extract (s, 1, NONE)