Commit cdf1a6e8 authored by Armaël Guéneau's avatar Armaël Guéneau

Clean up whitespace

parent c38fc2fa
......@@ -8,7 +8,7 @@ open Mytools
let is_tracing = ref false
let trace s =
if !is_tracing
if !is_tracing
then (print_string s; print_newline())
let ppf = Format.std_formatter
......@@ -30,7 +30,7 @@ let (^/) = Filename.concat
let spec =
Arg.align [
("-I", Arg.String (fun i -> Clflags.include_dirs := i::!Clflags.include_dirs),
("-I", Arg.String (fun i -> Clflags.include_dirs := i::!Clflags.include_dirs),
" includes a directory where to look for interface files");
("-rectypes", Arg.Set Clflags.recursive_types, " activates recursive types");
("-left2right", Arg.Set Mytools.use_left_to_right_order, " use the left-to-right evaluation order for sub-expressions, instead of OCaml order");
......@@ -57,7 +57,7 @@ let _ =
(*---------------------------------------------------*)
trace "1) parsing of command line";
let files = ref [] in
Arg.parse
Arg.parse
spec
(fun f -> files := f::!files)
("usage: [-I dir] [..other options..] file.ml");
......@@ -77,11 +77,11 @@ let _ =
if List.length !files <> 1 then
failwith "Expects one argument: the filename of the ML source file";
let sourcefile = List.hd !files in
if !Clflags.nopervasives
if !Clflags.nopervasives
&& Filename.basename sourcefile <> "Pervasives.ml" then
failwith "Option -nopervasives may only be used to compile file Pervasives";
(* this defensive check is needed for the correctness of normalization
of special operators such as "mod" or "&&";
(* this defensive check is needed for the correctness of normalization
of special operators such as "mod" or "&&";
see also function [add_pervasives_prefix_if_needed] *)
if not (Filename.check_suffix sourcefile ".ml") then
......@@ -101,7 +101,7 @@ let _ =
let cmd = Printf.sprintf "mkdir -p %s" debugdir in
begin try ignore (Sys.command cmd)
with _ -> Printf.printf "Could not create debug directory\n" end;
(*---------------------------------------------------*)
trace "2) reading and typing source file";
......@@ -111,7 +111,7 @@ let _ =
| None -> failwith "Could not read and typecheck input file"
| Some (parsetree1, (typedtree1,_)) -> parsetree1
in
file_put_contents (debugdirBase ^ "_original.ml") (Print_past.string_of_structure parsetree1);
file_put_contents (debugdirBase ^ "_original.ml") (Print_past.string_of_structure parsetree1);
if !only_cmj then begin
trace "3) exiting since -only_cmj";
......@@ -121,19 +121,19 @@ let _ =
(*---------------------------------------------------*)
trace "3) normalizing source code";
let parsetree2 : Parsetree.structure = normalize_structure parsetree1 in
file_put_contents (debugdirBase ^ "_normalized.ml") (Print_past.string_of_structure parsetree2);
file_put_contents (debugdirBase ^ "_normalized.ml") (Print_past.string_of_structure parsetree2);
(*---------------------------------------------------*)
trace "4) typing normalized code";
let (typedtree2, _ : Typedtree.structure * Typedtree.module_coercion) =
let fail () =
let (typedtree2, _ : Typedtree.structure * Typedtree.module_coercion) =
let fail () =
failwith (Printf.sprintf "Could not typecheck the normalized source code\nCheck out the file %s_normalized.ml." debugdirBase) in
try
try
match typecheck_implementation_file ppf sourcefile parsetree2 with
| None -> fail() (* TODO: useful?*)
| Some typedtree2 -> typedtree2
with Typetexp.Error(loc, err) -> fail()
in
in
(*---------------------------------------------------*)
trace "5) dumping normalized file";
......@@ -148,9 +148,9 @@ let _ =
(*---------------------------------------------------*)
trace "5) constructing caracteristic formula ast";
let cftops =
try Characteristic.cfg_file typedtree2
with
let cftops =
try Characteristic.cfg_file typedtree2
with
| Typetexp.Error(_, _) -> assert false
| Characteristic.Not_in_normal_form (loc, s) ->
Location.print_error Format.std_formatter loc;
......@@ -165,11 +165,11 @@ let _ =
(*---------------------------------------------------*)
trace "7) dumping debug formula file";
let result = Print_coq.tops coqtops in
file_put_contents (debugdirBase ^ "_formulae.v") result;
file_put_contents (debugdirBase ^ "_formulae.v") result;
(*---------------------------------------------------*)
trace "8) dumping .v file";
file_put_contents outputfile result;
file_put_contents outputfile result;
(*---------------------------------------------------*)
trace "9) characteristic formulae successfully generated\n"
......
......@@ -21,8 +21,8 @@ let _ =
(*---------------------------------------------------*)
let files = ref [] in
Arg.parse
[ ("-I", Arg.String (fun i -> Clflags.include_dirs := i::!Clflags.include_dirs),
Arg.parse
[ ("-I", Arg.String (fun i -> Clflags.include_dirs := i::!Clflags.include_dirs),
"includes a directory where to look for interface files");
("-rectypes", Arg.Set Clflags.recursive_types, "activates recursive types");
("-nostdlib", Arg.Set no_mystd_include, "do not include standard library");
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment