Merge branch 'sail2' into rmem_interpreter

1 files changed, 30 insertions, 24 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index 344c7921..87acd83a 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -65,7 +65,7 @@ let get_lexbuf f =
   lexbuf, in_chan
 
 let parse_file ?loc:(l=Parse_ast.Unknown) (f : string) : Parse_ast.defs =
-  let open Reporting_basic in
+  let open Reporting in
   try
     let lexbuf, in_chan = get_lexbuf f in
     begin
@@ -75,7 +75,8 @@ let parse_file ?loc:(l=Parse_ast.Unknown) (f : string) : Parse_ast.defs =
       with
       | Parser.Error ->
          let pos = Lexing.lexeme_start_p lexbuf in
-         raise (Fatal_error (Err_syntax (pos, "no information")))
+         let tok = Lexing.lexeme lexbuf in
+         raise (Fatal_error (Err_syntax (pos, "current token: " ^ tok)))
       | Lexer.LexError(s,p) ->
          raise (Fatal_error (Err_lex (p, s)))
     end
@@ -111,7 +112,7 @@ let cond_pragma l defs =
        decr depth; push_def def; scan defs
     | def :: defs ->
        push_def def; scan defs
-    | [] -> raise (Reporting_basic.err_general l "$ifdef or $ifndef never ended by $endif")
+    | [] -> raise (Reporting.err_general l "$ifdef or $ifndef never ended by $endif")
   in
   scan defs
 
@@ -123,19 +124,24 @@ let parseid_to_string (Parse_ast.Id_aux (id, _)) =
   match id with
   | Parse_ast.Id x | Parse_ast.DeIid x -> x
 
-let rec realise_union_anon_rec_types (Parse_ast.TD_variant (union_id, name_scm_opt, typq, _, flag) as orig_union) arms =
-  match arms with
-  | [] -> []
-  | arm :: arms ->
-     match arm with
-     | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_id _), _)) -> (None, arm) :: realise_union_anon_rec_types orig_union arms
-     | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_anon_rec (fields, id)), l)) ->
-        let open Parse_ast in
-        let record_str = "_" ^ parseid_to_string union_id ^ "_" ^ parseid_to_string id ^ "_record" in
-        let record_id = Id_aux (Id record_str, Generated l) in
-        let new_arm = Tu_aux ((Tu_ty_id ((ATyp_aux (ATyp_id record_id, Generated l)), id)), Generated l) in
-        let new_rec_def = DEF_type (TD_aux (TD_record (record_id, name_scm_opt, typq, fields, flag), Generated l)) in
-        (Some new_rec_def, new_arm) :: (realise_union_anon_rec_types orig_union arms)
+let rec realise_union_anon_rec_types orig_union arms =
+  match orig_union with
+  | Parse_ast.TD_variant (union_id, name_scm_opt, typq, _, flag) ->
+     begin match arms with
+     | [] -> []
+     | arm :: arms ->
+        match arm with
+        | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_id _), _)) -> (None, arm) :: realise_union_anon_rec_types orig_union arms
+        | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_anon_rec (fields, id)), l)) ->
+           let open Parse_ast in
+           let record_str = "_" ^ parseid_to_string union_id ^ "_" ^ parseid_to_string id ^ "_record" in
+           let record_id = Id_aux (Id record_str, Generated l) in
+           let new_arm = Tu_aux ((Tu_ty_id ((ATyp_aux (ATyp_id record_id, Generated l)), id)), Generated l) in
+           let new_rec_def = DEF_type (TD_aux (TD_record (record_id, name_scm_opt, typq, fields, flag), Generated l)) in
+           (Some new_rec_def, new_arm) :: (realise_union_anon_rec_types orig_union arms)
+     end
+  | _ ->
+     raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Non union type-definition passed to realise_union_anon_rec_typs")
 
 let rec preprocess opts = function
   | [] -> []
@@ -149,11 +155,10 @@ let rec preprocess opts = function
          let args = Str.split (Str.regexp " +") command in
          Arg.parse_argv ~current:(ref 0) (Array.of_list ("sail" :: args)) opts (fun _ -> ()) "";
        with
-       | Arg.Bad message | Arg.Help message -> raise (Reporting_basic.err_general l message)
+       | Arg.Bad message | Arg.Help message -> raise (Reporting.err_general l message)
      end;
      preprocess opts defs
 
-
   | Parse_ast.DEF_pragma ("ifndef", symbol, l) :: defs ->
      let then_defs, else_defs, defs = cond_pragma l defs in
      if not (StringSet.mem symbol !symbols) then
@@ -200,8 +205,8 @@ let rec preprocess opts = function
        let help = "Make sure the filename is surrounded by quotes or angle brackets" in
        (Util.warn ("Skipping bad $include " ^ file ^ ". " ^ help); preprocess opts defs)
 
-  | Parse_ast.DEF_pragma (p, arg, _) :: defs ->
-     (Util.warn ("Bad pragma $" ^ p ^ " " ^ arg); preprocess opts defs)
+  | Parse_ast.DEF_pragma (p, arg, l) :: defs ->
+     Parse_ast.DEF_pragma (p, arg, l) :: preprocess opts defs
 
   (* realise any anonymous record arms of variants *)
   | Parse_ast.DEF_type (Parse_ast.TD_aux
@@ -309,7 +314,7 @@ let output_lem filename libs defs =
     open_output_with_check_unformatted (filename ^ ".lem") in
   (Pretty_print.pp_defs_lem
      (ot, base_imports)
-     (o, base_imports @ (String.capitalize types_module :: libs))
+     (o, base_imports @ (String.capitalize_ascii types_module :: libs))
      defs generated_line);
   close_output_with_check ext_ot;
   close_output_with_check ext_o;
@@ -360,8 +365,10 @@ let output libpath out_arg files =
       output1 libpath out_arg f defs)
     files
 
-let rewrite_step defs (name,rewriter) =
+let rewrite_step defs (name, rewriter) =
+  let t = Profile.start () in
   let defs = rewriter defs in
+  Profile.finish ("rewrite " ^ name) t;
   let _ = match !(opt_ddump_rewrite_ast) with
     | Some (f, i) ->
       begin
@@ -378,10 +385,9 @@ let rewrite_step defs (name,rewriter) =
 let rewrite rewriters env defs =
   try List.fold_left rewrite_step defs rewriters with
   | Type_check.Type_error (l, err) ->
-     raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err))
+     raise (Reporting.err_typ l (Type_error.string_of_type_error err))
 
 let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
-let rewrite_undefined bitvectors = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined bitvectors x)]
 let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem
 let rewrite_ast_coq = rewrite Rewrites.rewrite_defs_coq
 let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml