Moved parser, lexer and pretty printer to correct locations.

10 files changed, 16 insertions, 22 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 52ed1da1..4e466596 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -956,11 +956,11 @@ let initial_kind_env =
   ]
 
 let exp_of_string order str =
-  let exp = Parser2.exp_eof Lexer2.token (Lexing.from_string str) in
+  let exp = Parser.exp_eof Lexer.token (Lexing.from_string str) in
   to_ast_exp initial_kind_env order exp
 
 let typschm_of_string order str =
-  let typschm = Parser2.typschm_eof Lexer2.token (Lexing.from_string str) in
+  let typschm = Parser.typschm_eof Lexer.token (Lexing.from_string str) in
   let (typschm, _, _) = to_ast_typschm initial_kind_env order typschm in
   typschm
 
@@ -1098,5 +1098,5 @@ let process_ast order defs =
     end
 
 let ast_of_def_string order str =
-  let def = Parser2.def_eof Lexer2.token (Lexing.from_string str) in
+  let def = Parser.def_eof Lexer.token (Lexing.from_string str) in
   process_ast order (Defs [def])
diff --git a/src/interpreter.ml b/src/interpreter.ml
index 7e84f5c7..7a4b6b33 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -510,7 +510,7 @@ let rec eval_frame ast = function
         print_endline ("Returning value: " ^ string_of_value (value_of_exp v) |> Util.cyan |> Util.clear);
         Step (stack_string head, (stack_state head, snd state), stack_cont head (value_of_exp v), stack')
      | Pure exp', _ ->
-        let out' = Pretty_print_sail2.to_string (Pretty_print_sail2.doc_exp exp') in
+        let out' = Pretty_print_sail.to_string (Pretty_print_sail.doc_exp exp') in
         Step (out', state, step exp', stack)
      | Yield (Call(id, vals, cont)), _ ->
         print_endline ("Calling " ^ string_of_id id |> Util.cyan |> Util.clear);
diff --git a/src/isail.ml b/src/isail.ml
index c56fc69f..5452b7a9 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -53,7 +53,7 @@ open Sail
 open Ast
 open Ast_util
 open Interpreter
-open Pretty_print_sail2
+open Pretty_print_sail
 
 type mode =
   | Evaluation of frame
diff --git a/src/lexer2.mll b/src/lexer.mll
index 3a1f7066..ccbe12a5 100644
--- a/src/lexer2.mll
+++ b/src/lexer.mll
@@ -49,7 +49,7 @@
 (**************************************************************************)
 
 {
-open Parser2
+open Parser
 module Big_int = Nat_big_num
 open Parse_ast
 module M = Map.Make(String)
diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml
index d912c965..1babc1c9 100644
--- a/src/myocamlbuild.ml
+++ b/src/myocamlbuild.ml
@@ -109,11 +109,5 @@ dispatch begin function
         mv (basename (env "%.lem")) (dirname (env "%.lem"))
       ]);
 
-    rule "old parser"
-    ~insert:(`top)
-    ~prods: ["parser.ml"; "parser.mli"]
-    ~dep: "parser.mly"
-    (fun env builder -> Cmd(S[V"OCAMLYACC"; T(tags_of_pathname "parser.mly"++"ocaml"++"parser"++"ocamlyacc"); Px "parser.mly"]));
-
 | _ -> ()
 end ;;
diff --git a/src/parser2.mly b/src/parser.mly
index 7af70687..7af70687 100644
--- a/src/parser2.mly
+++ b/src/parser.mly
diff --git a/src/pretty_print_sail2.ml b/src/pretty_print_sail.ml
index 930da39c..930da39c 100644
--- a/src/pretty_print_sail2.ml
+++ b/src/pretty_print_sail.ml
diff --git a/src/process_file.ml b/src/process_file.ml
index 116eeb0b..7a4f71e3 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -67,13 +67,13 @@ let get_lexbuf f =
 let parse_file (f : string) : Parse_ast.defs =
   let lexbuf, in_chan = get_lexbuf f in
     try
-      let ast = Parser2.file Lexer2.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")))
-    | Lexer2.LexError(s,p) ->
+    | Lexer.LexError(s,p) ->
        raise (Reporting_basic.Fatal_error (Reporting_basic.Err_lex (p, s)))
 
 let convert_ast (order : Ast.order) (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast order defs
@@ -92,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_sail2.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)
 
@@ -103,7 +103,7 @@ let opt_auto_mono = ref false
 let monomorphise_ast locs type_env ast =
   let ast = Monomorphise.monomorphise (!opt_lem_mwords) (!opt_auto_mono) (!opt_dmono_analysis)
     locs type_env ast in
-  let () = if !opt_ddump_raw_mono_ast then Pretty_print_sail2.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
 
@@ -191,7 +191,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
diff --git a/src/sail.ml b/src/sail.ml
index fdcaa15c..974885c6 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -186,7 +186,7 @@ let main() =
     let ast = convert_ast Ast_util.inc_ord ast in
 
     if !opt_convert
-    then (Pretty_print_sail2.pp_defs stdout ast; exit 0)
+    then (Pretty_print_sail.pp_defs stdout ast; exit 0)
     else ();
 
     let (ast, type_envs) = check_ast ast in
@@ -221,7 +221,7 @@ let main() =
          ()
        else ());
       (if !(opt_print_verbose)
-       then ((Pretty_print_sail2.pp_defs stdout) ast)
+       then ((Pretty_print_sail.pp_defs stdout) ast)
        else ());
       (if !(opt_print_lem_ast)
        then output "" Lem_ast_out [out_name,ast]
@@ -229,7 +229,7 @@ let main() =
       (if !(opt_print_sil)
        then
          let ast = rewrite_ast_sil ast in
-         Pretty_print_sail2.pp_defs stdout ast
+         Pretty_print_sail.pp_defs stdout ast
        else ());
       (if !(opt_print_ocaml)
        then
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 3d3b13e3..96f6e546 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -625,7 +625,7 @@ let merge_mutrecs defs =
       | DEF_fundef fundef -> fundef :: fundefs
       | DEF_internal_mutrec fundefs' -> fundefs' @ fundefs
       | _ ->
-        (* let _ = Pretty_print_sail2.pp_defs stderr (Defs [def]) in *)
+        (* let _ = Pretty_print_sail.pp_defs stderr (Defs [def]) in *)
         raise (Reporting_basic.err_unreachable (def_loc def)
           "Trying to merge non-function definition with mutually recursive functions") in
     (* let _ = Printf.eprintf " - Merging %s (using %s)\n" (set_to_string binds') (set_to_string uses') in *)