From 7441db19749fb7fb9383b6361dfbd99547e53486 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 29 Sep 2020 16:23:40 +0100 Subject: Refactor: Change AST type from a union to a struct --- src/jib/c_backend.ml | 12 ++++++------ src/jib/c_codegen.ml | 10 +++++----- src/jib/jib_compile.ml | 8 ++++---- src/jib/jib_smt.ml | 2 +- 4 files changed, 16 insertions(+), 16 deletions(-) (limited to 'src/jib') diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index a7e64fe4..2fe21d93 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -2196,10 +2196,10 @@ let sgen_finish = function Printf.sprintf " finish_%s();" (sgen_id id) | _ -> assert false -let rec get_recursive_functions (Defs defs) = +let rec get_recursive_functions defs = match defs with | DEF_internal_mutrec fundefs :: defs -> - IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions (Defs defs)) + IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions defs) | (DEF_fundef fdef as def) :: defs -> let open Rewriter in @@ -2216,11 +2216,11 @@ let rec get_recursive_functions (Defs defs) = let map_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp map_exp) } in let _ = rewrite_def map_defs def in if IdSet.mem (id_of_fundef fdef) !ids then - IdSet.add (id_of_fundef fdef) (get_recursive_functions (Defs defs)) + IdSet.add (id_of_fundef fdef) (get_recursive_functions defs) else - get_recursive_functions (Defs defs) + get_recursive_functions defs - | _ :: defs -> get_recursive_functions (Defs defs) + | _ :: defs -> get_recursive_functions defs | [] -> IdSet.empty let jib_of_ast env ast = @@ -2230,7 +2230,7 @@ let jib_of_ast env ast = let compile_ast env output_chan c_includes ast = try - let recursive_functions = Spec_analysis.top_sort_defs ast |> get_recursive_functions in + let recursive_functions = (Spec_analysis.top_sort_defs ast).defs |> get_recursive_functions in let cdefs, ctx = jib_of_ast env ast in let cdefs', _ = Jib_optimize.remove_tuples cdefs ctx in diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml index ea4afd00..b92713ff 100644 --- a/src/jib/c_codegen.ml +++ b/src/jib/c_codegen.ml @@ -1666,10 +1666,10 @@ let sgen_finish = function Printf.sprintf " finish_%s();" (sgen_id id) | _ -> assert false -let rec get_recursive_functions (Defs defs) = +let rec get_recursive_functions defs = match defs with | DEF_internal_mutrec fundefs :: defs -> - IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions (Defs defs)) + IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions defs) | (DEF_fundef fdef as def) :: defs -> let open Rewriter in @@ -1686,11 +1686,11 @@ let rec get_recursive_functions (Defs defs) = let map_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp map_exp) } in let _ = rewrite_def map_defs def in if IdSet.mem (id_of_fundef fdef) !ids then - IdSet.add (id_of_fundef fdef) (get_recursive_functions (Defs defs)) + IdSet.add (id_of_fundef fdef) (get_recursive_functions defs) else - get_recursive_functions (Defs defs) + get_recursive_functions defs - | _ :: defs -> get_recursive_functions (Defs defs) + | _ :: defs -> get_recursive_functions defs | [] -> IdSet.empty let codegen_output file_name docs = diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 4fd61a7d..cd4edd12 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -1642,7 +1642,7 @@ let sort_ctype_defs cdefs = ctype_defs @ cdefs -let compile_ast ctx (Defs defs) = +let compile_ast ctx ast = if !opt_memo_cache then (try if Sys.is_directory "_sbuild" then @@ -1653,9 +1653,9 @@ let compile_ast ctx (Defs defs) = | Sys_error _ -> Unix.mkdir "_sbuild" 0o775) else (); - let total = List.length defs in + let total = List.length ast.defs in let _, chunks, ctx = - List.fold_left (fun (n, chunks, ctx) def -> let defs, ctx = compile_def n total ctx def in n + 1, defs :: chunks, ctx) (1, [], ctx) defs + List.fold_left (fun (n, chunks, ctx) def -> let defs, ctx = compile_def n total ctx def in n + 1, defs :: chunks, ctx) (1, [], ctx) ast.defs in let cdefs = List.concat (List.rev chunks) in let cdefs, ctx = specialize_variants ctx [] cdefs in @@ -1669,4 +1669,4 @@ let add_special_functions env = let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit" in let cons_vs = Initial_check.extern_of_string (mk_id "sail_cons") "forall ('a : Type). ('a, list('a)) -> list('a)" in - snd (Type_error.check env (Defs [assert_vs; exit_vs; cons_vs])) + snd (Type_error.check_defs env [assert_vs; exit_vs; cons_vs]) diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index b03c1134..434ca8a9 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -118,7 +118,7 @@ let initial_ctx () = { tc_env = Type_check.initial_env; pragma_l = Parse_ast.Unknown; arg_stack = Stack.create (); - ast = Defs []; + ast = empty_ast; shared = Bindings.empty; preserved = IdSet.empty; events = ref EventMap.empty; -- cgit v1.2.3