Refactor: Change AST type from a union to a struct

4 files changed, 16 insertions, 16 deletions

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;