(* a simple main program for ppl project *) (* $Id: ppl.ml,v 1.45 2000/10/03 08:55:04 selinger Exp $ *) (* ---------------------------------------------------------------------- *) type inputmethod = Unknownin | Inputfile of string | Term of string | Stdin type outputmethod = Unknownout | Stdout | Outputfile of string type action = Compile | Reduce | Step | Parse (* a pretty-printer for input methods: this is useful to print the "filename" in error messages of the form "filename: c1-5: syntax error" *) let pp_inputmethod = function | Unknownin -> "(unknown)" | Stdin -> "(stdin)" | Inputfile s -> s | Term s -> "(input)" type commandline = { mutable input: inputmethod; mutable action: action; mutable typecheck: bool; mutable optimize: bool; mutable output: outputmethod; mutable typeinfomode: string; } (* print usage information and exit. *) (* status > 0 if there was an error, else status = 0 *) let usage status = prerr_endline "Usage: ppl [options] [outputmethod] inputmethod. Try --help for details."; exit(status) (* print help information and exit. *) (* status > 0 if there was an error, else status = 0 *) let help status = let p = print_endline in p "Usage: ppl [options] [outputmethod] inputmethod\n"; p "Inputmethods:"; p " filename | --input filename: read from file"; p " --term term: read from command line"; p " - | --stdin: read from standard input\n"; p "Outputmethods:"; p " -o filename | --output filename: write to file"; p " --stdout: write to stdout\n"; p "Options:"; p " -h | --help: print this message and exit"; p " -v | --version: print version information and exit"; p " -u | --untyped: omit type inference"; p " -t | --typed: do type inference"; p " -c | --compile: output pseudo assembly code"; p " -r | --reduce: reduce term to cbn normal form"; p " -s | --step: print cbn reduction sequence"; p " -p | --parse: parse and typecheck only"; p " -z | --optimize: optimize program before compilation"; p " -i mode | --typeinfo mode: mode for reporting intermediate types:"; p " mode = none, all, top, let, or an integer"; exit(status) (* print version information and exit. *) (* status > 0 if there was an error, else status = 0 *) let print_version status = print_endline ("PPL Version 0.1 copyright Ari Lamstein and "^ "Peter Selinger 2000."); exit(status) (* parse an argument vector and return a commandline record *) let read_commandline argv = let cmd = { input = Unknownin; action = Compile; typecheck = true; optimize = false; output = Unknownout; typeinfomode = "none"; } in let argc = Array.length argv in let rec read_from n = if n=argc then cmd else try match argv.(n) with "-h" | "--help" -> help 0; | "-v" | "--version" -> print_version 0; | "-u" | "--untyped" -> cmd.typecheck<-false; read_from (n+1) | "-t" | "--typed" -> cmd.typecheck<-true; read_from (n+1) | "-c" | "--compile" -> cmd.action<-Compile; read_from (n+1) | "-r" | "--reduce" -> cmd.action<-Reduce; read_from (n+1) | "-s" | "--step" -> cmd.action<-Step; read_from (n+1) | "-p" | "--parse" -> cmd.action<-Parse; read_from (n+1) | "-i" | "--typeinfo" -> cmd.typeinfomode <- argv.(n+1); read_from (n+2) | "-z" | "--optimize" -> cmd.optimize <- true; read_from (n+1) | "--term" -> cmd.input<-Term(argv.(n+1)); read_from (n+2) | "--output" | "-o" -> cmd.output<-Outputfile(argv.(n+1)); read_from (n+2) | "--input" -> cmd.input<-Inputfile(argv.(n+1)); read_from (n+2) | "--stdin" | "-" -> cmd.input<-Stdin; read_from (n+1) | "--stdout" -> cmd.output<-Stdout; read_from (n+1) | other -> if (String.length other) > 0 && ((String.get other 0) = '-') then begin prerr_endline ("ppl: unknown option: "^other); usage 1 end else (* if it is not an option, it is a file name *) begin cmd.input<-Inputfile(other); read_from (n+1) end with Invalid_argument "Array.get" -> prerr_endline ("ppl: invalid command line"); usage 1 in read_from 1 (* get a Lambda.lambdaterm from the appropriate input source *) let get_term input_method = match input_method with Inputfile(filename) -> let infile = open_in filename in (* read and parse the \-term *) let term = (Frontend.parse_channel infile) in close_in infile; term | Term(term) -> let term' = (Frontend.parse_string term) in term' | Stdin -> Frontend.parse_channel stdin | Unknownin -> prerr_endline ("ppl: no filename given"); usage 1 (* perform the appropriate action on a Lambda.lambdaterm, return a string *) let do_action action term = match (action) with Compile -> let code=Compiler.compile term in Pseudo.string_of_program code | Reduce -> begin try let nf=Cbn.reduce_cbn term in Lambda.string_of_lambdaterm nf with Exn.Runtimeerror(s,_) -> "Runtime error: "^s end | Step -> let rec continually_reduce term = let str = Lambda.string_of_lambdaterm term in try str ^"\n"^ (continually_reduce (Cbn.reduce_cbn_step term)) with Cbn.NormalForm -> str | Exn.Runtimeerror(s,_) -> str ^"\n"^ "Runtime error: "^s in continually_reduce term | Parse -> Lambda.string_of_lambdaterm term (* calculate the most general type of a lambdaterm and print it to stdout *) let do_typeinference term typeinfomode = let most_general_type = Typing.most_general_type term in print_string (Typing.string_of_typeinfo typeinfomode); print_endline ("Most general type is: "^ Types.string_of_typeexp most_general_type) (* output a string to the appropriate outputmethod *) let do_output outmethod str = match outmethod with Unknownout -> prerr_endline "ppl: no output file given" | Outputfile(filename) -> let file = open_out filename in let v = output_string file str in close_out file | Stdout -> print_endline str (* add a suffix to a filename, deleting the old suffix, if any *) let appendsuffix str suf = try let r = String.rindex str '.' in String.sub str 0 r ^ suf with Not_found -> str ^ suf (* guess the most appropriate default outputmethod, based on inputmethod and action *) let guess_outputmethod inmethod action = match inmethod with Unknownin -> Unknownout | Term(t) -> Stdout | Stdin -> Stdout | Inputfile(filename) -> match action with Compile -> Outputfile(appendsuffix filename ".c") | Reduce -> Stdout | Step -> Stdout | Parse -> Stdout (* main program *) let ppl = let cmd = read_commandline Sys.argv in if cmd.output = Unknownout then cmd.output <- guess_outputmethod cmd.input cmd.action; let infilename = pp_inputmethod cmd.input in let ppl_warning s = prerr_endline ("Warning: "^ infilename ^": "^ s) in Compiler.warning := ppl_warning; try let term=get_term cmd.input in if (cmd.typecheck=true) then do_typeinference term cmd.typeinfomode; let term' = if (cmd.optimize=true && cmd.action=Compile) then Opt.reduce_to_nf term else term in let outstr = do_action cmd.action term' in do_output cmd.output outstr; with Sys_error(message) -> prerr_endline message; exit 1 | Exn.Syntax_error(startchar,endchar) -> prerr_endline (infilename ^":c."^ (string_of_int startchar) ^"-"^ (string_of_int endchar) ^": syntax error"); exit 1 | Exn.Illegal_character(badchar,startchar,endchar) -> prerr_endline (infilename ^":c."^ (string_of_int startchar) ^"-"^ (string_of_int endchar) ^ ": illegal character '"^ badchar ^"'"); exit 1 | Exn.Unbound_variable(var) -> let var_string = (Lambda.string_of_variable var) in prerr_endline (infilename ^": undeclared variable "^ var_string); exit 1 | Exn.Can't_unify(a,b) -> prerr_endline (infilename ^": type error; cannot unify "^ (Types.string_of_typeexp a) ^" and "^ (Types.string_of_typeexp b)); prerr_endline ("\ntypeinference until failure:"); prerr_string (Typing.string_of_typeinfo cmd.typeinfomode); exit 1 | Exn.Illegal_range(badnum,startchar,endchar) -> prerr_endline (infilename ^":c."^ (string_of_int startchar) ^"-"^ (string_of_int endchar) ^ ": integer out of range '"^ badnum ^"'"); | Exn.Compiler_exception(location) -> prerr_endline ("ppl: fatal error: internal bug encountered at "^ location ^"\nPlease send a bug report to "^ "selinger@umich.edu"); | Exn.Illegal_projection(badproj,startchar,endchar) -> prerr_endline (infilename ^":c."^ (string_of_int startchar) ^"-"^ (string_of_int endchar) ^ ": illegal projection '"^ badproj ^"'") | Exn.Illegal_injection(badinj,startchar,endchar) -> prerr_endline (infilename ^":c."^ (string_of_int startchar) ^"-"^ (string_of_int endchar) ^ ": illegal injection '"^ badinj ^"'") | Exn.Illegal_casedist(badcasedist) -> prerr_endline (infilename ^": illegal case distinction: "^ (Library.string_of_list (Lambda.string_of_injpattern) " | " badcasedist))