diff options
| -rw-r--r-- | src/compiler.sig | 4 | ||||
| -rw-r--r-- | src/compiler.sml | 53 |
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) |