diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 64 |
1 files changed, 35 insertions, 29 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index e8bb5fc1..d2a43b4a 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -90,7 +90,13 @@ let parse_file ?loc:(l=Parse_ast.Unknown) (f : string) : Parse_ast.defs = (* Simple preprocessor features for conditional file loading *) module StringSet = Set.Make(String) -let symbols = ref StringSet.empty +let default_symbols = + List.fold_left (fun set str -> StringSet.add str set) StringSet.empty + [ "FEATURE_IMPLICITS" ] + +let symbols = ref default_symbols + +let clear_symbols () = symbols := default_symbols let cond_pragma l defs = let depth = ref 0 in @@ -130,7 +136,7 @@ let parseid_to_string (Parse_ast.Id_aux (id, _)) = 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) -> + | Parse_ast.TD_variant (union_id, typq, _, flag) -> begin match arms with | [] -> [] | arm :: arms -> @@ -141,7 +147,7 @@ let rec realise_union_anon_rec_types orig_union arms = 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 + let new_rec_def = DEF_type (TD_aux (TD_record (record_id, typq, fields, flag), Generated l)) in (Some new_rec_def, new_arm) :: (realise_union_anon_rec_types orig_union arms) end | _ -> @@ -195,7 +201,7 @@ let rec preprocess opts = function let sail_dir = try Sys.getenv "SAIL_DIR" with | Not_found -> - let share_dir = Share_directory.d in + let share_dir = Manifest.dir in if Sys.file_exists share_dir then share_dir else @@ -214,7 +220,7 @@ let rec preprocess opts = function (* realise any anonymous record arms of variants *) | Parse_ast.DEF_type (Parse_ast.TD_aux - (Parse_ast.TD_variant (id, name_scm_opt, typq, arms, flag) as union, l) + (Parse_ast.TD_variant (id, typq, arms, flag) as union, l) ) :: defs -> let records_and_arms = realise_union_anon_rec_types union arms in let rec filter_records = function [] -> [] @@ -223,7 +229,7 @@ let rec preprocess opts = function in let generated_records = filter_records (List.map fst records_and_arms) in let rewritten_arms = List.map snd records_and_arms in - let rewritten_union = Parse_ast.TD_variant (id, name_scm_opt, typq, rewritten_arms, flag) in + let rewritten_union = Parse_ast.TD_variant (id, typq, rewritten_arms, flag) in generated_records @ (Parse_ast.DEF_type (Parse_ast.TD_aux (rewritten_union, l))) :: preprocess opts defs | (Parse_ast.DEF_default (Parse_ast.DT_aux (Parse_ast.DT_order (_, Parse_ast.ATyp_aux (atyp, _)), _)) as def) :: defs -> @@ -237,12 +243,10 @@ let rec preprocess opts = function let preprocess_ast opts (Parse_ast.Defs defs) = Parse_ast.Defs (preprocess opts defs) -let convert_ast (order : Ast.order) (defs : Parse_ast.defs) : unit Ast.defs = Initial_check.process_ast order defs - -let load_file_no_check opts order f = convert_ast order (preprocess_ast opts (parse_file f)) +let load_file_no_check opts order f = Initial_check.process_ast (preprocess_ast opts (parse_file f)) let load_file opts order env f = - let ast = convert_ast order (preprocess_ast opts (parse_file f)) in + let ast = Initial_check.process_ast (preprocess_ast opts (parse_file f)) in Type_error.check env ast let opt_just_check = ref false @@ -284,7 +288,7 @@ let close_output_with_check (o, temp_file_name, opt_dir, file_name) = let generated_line f = Printf.sprintf "Generated by Sail from %s." f -let output_lem filename libs defs = +let output_lem filename libs type_env defs = let generated_line = generated_line filename in (* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *) let types_module = (filename ^ "_types") in @@ -324,7 +328,7 @@ let output_lem filename libs defs = (Pretty_print.pp_defs_lem (ot, base_imports) (o, base_imports @ (String.capitalize_ascii types_module :: libs)) - defs generated_line); + type_env defs generated_line); close_output_with_check ext_ot; close_output_with_check ext_o; let ((ol,_,_,_) as ext_ol) = @@ -360,23 +364,23 @@ let rec iterate (f : int -> unit) (n : int) : unit = if n = 0 then () else (f n; iterate f (n - 1)) -let output1 libpath out_arg filename defs = +let output1 libpath out_arg filename type_env defs = let f' = Filename.basename (Filename.chop_extension filename) in match out_arg with | Lem_out libs -> - output_lem f' libs defs + output_lem f' libs type_env defs | Coq_out libs -> output_coq !opt_coq_output_dir f' libs defs let output libpath out_arg files = List.iter - (fun (f, defs) -> - output1 libpath out_arg f defs) + (fun (f, type_env, defs) -> + output1 libpath out_arg f type_env defs) files -let rewrite_step defs (name, rewriter) = +let rewrite_step n total env defs (name, rewriter) = let t = Profile.start () in - let defs = rewriter defs in + let defs = rewriter env defs in Profile.finish ("rewrite " ^ name) t; let _ = match !(opt_ddump_rewrite_ast) with | Some (f, i) -> @@ -389,21 +393,23 @@ let rewrite_step defs (name, rewriter) = opt_ddump_rewrite_ast := Some (f, i + 1) end | _ -> () in + Util.progress "Rewrite " name n total; defs -let rewrite rewriters env defs = - try List.fold_left rewrite_step defs rewriters with - | Type_check.Type_error (l, err) -> +let rewrite env rewriters defs = + let total = List.length rewriters in + try snd (List.fold_left (fun (n, defs) rw -> n + 1, rewrite_step n total env defs rw) (1, defs) rewriters) with + | Type_check.Type_error (_, l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) -let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)] -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 +let rewrite_ast env = rewrite env [("initial", fun _ -> Rewriter.rewrite_defs)] +let rewrite_ast_lem env = rewrite env Rewrites.rewrite_defs_lem +let rewrite_ast_coq env = rewrite env Rewrites.rewrite_defs_coq +let rewrite_ast_ocaml env = rewrite env Rewrites.rewrite_defs_ocaml let rewrite_ast_c env ast = ast - |> rewrite Rewrites.rewrite_defs_c env - |> rewrite [("constant_fold", Constant_fold.rewrite_constant_function_calls env)] env + |> rewrite env Rewrites.rewrite_defs_c + |> rewrite env [("constant_fold", fun _ -> Constant_fold.rewrite_constant_function_calls env)] -let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter -let rewrite_ast_check = rewrite Rewrites.rewrite_defs_check +let rewrite_ast_interpreter env = rewrite env Rewrites.rewrite_defs_interpreter +let rewrite_ast_check env = rewrite env Rewrites.rewrite_defs_check |