diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 42 |
1 files changed, 8 insertions, 34 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 9b5cd9da..435beb3c 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -48,7 +48,8 @@ (* SUCH DAMAGE. *) (**************************************************************************) -let opt_new_parser = ref false +let opt_lem_sequential = ref false +let opt_lem_mwords = ref false type out_type = | Lem_ast_out @@ -64,42 +65,14 @@ let get_lexbuf f = lexbuf, in_chan let parse_file (f : string) : Parse_ast.defs = - if not !opt_new_parser - then - let scanbuf, in_chan = get_lexbuf f in - let type_names = - try - Pre_parser.file Pre_lexer.token scanbuf - with - | Parsing.Parse_error -> - let pos = Lexing.lexeme_start_p scanbuf in - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "pre"))) - | Parse_ast.Parse_error_locn(l,m) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m))) - | Lexer.LexError(s,p) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) - in - close_in in_chan; - Lexer.custom_type_names := !Lexer.custom_type_names @ type_names - else (); - let lexbuf, in_chan = get_lexbuf f in try - let ast = - if !opt_new_parser - then Parser2.file Lexer2.token lexbuf - else Parser.file Lexer.token lexbuf - in + let ast = Parser.file Lexer.token lexbuf in close_in in_chan; ast with - | Parser2.Error -> + | Parser.Error -> let pos = Lexing.lexeme_start_p lexbuf in raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "no information"))) - | Parsing.Parse_error -> - let pos = Lexing.lexeme_start_p lexbuf in - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax (pos, "main"))) - | Parse_ast.Parse_error_locn(l,m) -> - raise (Reporting_basic.Fatal_error (Reporting_basic.Err_syntax_locn (l, m))) | Lexer.LexError(s,p) -> raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s))) @@ -119,7 +92,7 @@ let opt_dno_cast = ref false let check_ast (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t = let ienv = if !opt_dno_cast then Type_check.Env.no_casts Type_check.initial_env else Type_check.initial_env in let ast, env = Type_check.check ienv defs in - let () = if !opt_ddump_tc_ast then Pretty_print.pp_defs stdout ast else () in + let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_defs stdout ast else () in let () = if !opt_just_check then exit 0 else () in (ast, env) @@ -139,7 +112,7 @@ let monomorphise_ast locs type_env ast = all_split_errors = !opt_dall_split_errors } in let ast = monomorphise opts locs type_env ast in - let () = if !opt_ddump_raw_mono_ast then Pretty_print.pp_defs stdout ast else () in + let () = if !opt_ddump_raw_mono_ast then Pretty_print_sail.pp_defs stdout ast else () in let ienv = Type_check.Env.no_casts Type_check.initial_env in Type_check.check ienv ast @@ -225,7 +198,7 @@ let rewrite_step defs (name,rewriter) = let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in (* output "" Lem_ast_out [filename, defs]; *) let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted filename in - Pretty_print_sail2.pp_defs ot defs; + Pretty_print_sail.pp_defs ot defs; close_output_with_check ext_ot; opt_ddump_rewrite_ast := Some (f, i + 1) end @@ -241,5 +214,6 @@ let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)] let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !Pretty_print_lem.opt_mwords x)] let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml +let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter let rewrite_ast_sil = rewrite Rewrites.rewrite_defs_sil let rewrite_ast_check = rewrite Rewrites.rewrite_defs_check |