adamc@0: (* Copyright (c) 2008, Adam Chlipala
adamc@0:  * All rights reserved.
adamc@0:  *
adamc@0:  * Redistribution and use in source and binary forms, with or without
adamc@0:  * modification, are permitted provided that the following conditions are met:
adamc@0:  *
adamc@0:  * - Redistributions of source code must retain the above copyright notice,
adamc@0:  *   this list of conditions and the following disclaimer.
adamc@0:  * - Redistributions in binary form must reproduce the above copyright notice,
adamc@0:  *   this list of conditions and the following disclaimer in the documentation
adamc@0:  *   and/or other materials provided with the distribution.
adamc@0:  * - The names of contributors may not be used to endorse or promote products
adamc@0:  *   derived from this software without specific prior written permission.
adamc@0:  *
adamc@0:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@0:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@0:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@0:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@0:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adamc@0:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@0:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@0:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@0:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@0:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@0:  * POSSIBILITY OF SUCH DAMAGE.
adamc@0:  *)
adamc@0: 
adamc@857: val timing = ref false
adamc@857: val sources = ref ([] : string list)
adamc@857: val demo = ref (NONE : (string * bool) option)
adamc@857: 
adamc@857: fun doArgs args =
adamc@208:     case args of
adamc@857:         [] => ()
adamc@384:       | "-demo" :: prefix :: rest =>
adamc@857:         (demo := SOME (prefix, false);
adamc@857:          doArgs rest)
adamc@501:       | "-guided-demo" :: prefix :: rest =>
adamc@857:         (demo := SOME (prefix, true);
adamc@857:          doArgs rest)
adamc@856:       | "-protocol" :: name :: rest =>
adamc@856:         (Settings.setProtocol name;
adamc@857:          doArgs rest)
adamc@857:       | "-debug" :: rest =>
adamc@857:         (Settings.setDebug true;
adamc@857:          doArgs rest)
adamc@857:       | "-timing" :: rest =>
adamc@857:         (timing := true;
adamc@857:          doArgs rest)
adamc@208:       | arg :: rest =>
adamc@857:         (if size arg > 0 andalso String.sub (arg, 0) = #"-" then
adamc@857:              raise Fail ("Unknown flag " ^ arg)
adamc@857:          else
adamc@857:              sources := arg :: !sources;
adamc@857:          doArgs rest)
adamc@208: 
adamc@857: val () = doArgs (CommandLine.arguments ())
adamc@208: 
adamc@279: val job =
adamc@857:     case !sources of
adamc@279:         [file] => file
adamc@378:       | _ => raise Fail "Zero or multiple job files specified"
adamc@279: 
adamc@208: val () =
adamc@857:     case !demo of
adamc@501:         SOME (prefix, guided) =>
adamc@501:         Demo.make {prefix = prefix, dirname = job, guided = guided}
adamc@384:       | NONE =>
adamc@857:         if !timing then
adamc@384:             Compiler.time Compiler.toCjrize job
adamc@384:         else
adamc@384:             Compiler.compile job