diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 30 |
1 files changed, 16 insertions, 14 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 094b0ecb..00013775 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -130,7 +130,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 +141,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 +195,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 +214,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 +223,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 -> @@ -284,7 +284,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 +324,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,21 +360,21 @@ 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 defs (name, rewriter) = let t = Profile.start () in let defs = rewriter defs in Profile.finish ("rewrite " ^ name) t; @@ -389,11 +389,13 @@ 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 defs = - try List.fold_left rewrite_step defs rewriters with - | Type_check.Type_error (l, err) -> + let total = List.length rewriters in + try snd (List.fold_left (fun (n, defs) rw -> n + 1, rewrite_step n total 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)] |