Move the ast defs wrapper into it's own file

This refactoring is intended to allow this type to have more than just a
list of definitions in future.

51 files changed, 136 insertions, 41 deletions

diff --git a/language/sail.ott b/language/sail.ott
index a1dbda60..93ce382d 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -875,13 +875,6 @@ def :: 'DEF_' ::=
   | $ string1 string2 l                                :: :: pragma
     {{ com compiler directive }}
 
-defs :: '' ::=
-  {{ com definition sequence }}
-  {{ auxparam 'a }}
-  | def1  .. defn                 :: :: Defs
-
-
-
 terminals :: '' ::=
   | **                                  :: :: starstar
     {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }}
diff --git a/src/ast_defs.ml b/src/ast_defs.ml
new file mode 100644
index 00000000..7d7c7ac5
--- /dev/null
+++ b/src/ast_defs.ml
@@ -0,0 +1,53 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast
+
+type 'a defs = Defs of 'a def list
diff --git a/src/ast_util.ml b/src/ast_util.ml
index 3123d447..a342fc6b 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Util
 module Big_int = Nat_big_num
 
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 6ac29123..5d740277 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -51,6 +51,7 @@
 (** Utilities and helper functions for operating on Sail ASTs *)
 
 open Ast
+open Ast_defs
 module Big_int = Nat_big_num
 
 type mut = Immutable | Mutable
diff --git a/src/bitfield.ml b/src/bitfield.ml
index 5b0a73b0..e4813e44 100644
--- a/src/bitfield.ml
+++ b/src/bitfield.ml
@@ -52,6 +52,7 @@ module Big_int = Nat_big_num
 
 open Initial_check
 open Ast
+open Ast_defs
 open Ast_util
 
 let bitvec size order =
diff --git a/src/cgen_backend.ml b/src/cgen_backend.ml
index 77029c9e..3bca3fa1 100644
--- a/src/cgen_backend.ml
+++ b/src/cgen_backend.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open PPrint
 
diff --git a/src/constant_propagation.mli b/src/constant_propagation.mli
index 9c182cb0..1312290a 100644
--- a/src/constant_propagation.mli
+++ b/src/constant_propagation.mli
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Type_check
 
diff --git a/src/constant_propagation_mutrec.ml b/src/constant_propagation_mutrec.ml
index 03d8e154..a8c26bff 100644
--- a/src/constant_propagation_mutrec.ml
+++ b/src/constant_propagation_mutrec.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Type_check
 open Rewriter
diff --git a/src/initial_check.ml b/src/initial_check.ml
index 828d1b5e..c0d956c4 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -49,8 +49,9 @@
 (**************************************************************************)
 
 open Ast
-open Util
+open Ast_defs
 open Ast_util
+open Util
 open Printf
 module Big_int = Nat_big_num
 
diff --git a/src/initial_check.mli b/src/initial_check.mli
index 5a352eee..48bdc785 100644
--- a/src/initial_check.mli
+++ b/src/initial_check.mli
@@ -51,6 +51,7 @@
 (** Initial desugaring pass over AST after parsing *)
 
 open Ast
+open Ast_defs
 open Ast_util
 
 (** {2 Options} *)
diff --git a/src/interactive.ml b/src/interactive.ml
index 93df1dc0..d5d0fca4 100644
--- a/src/interactive.ml
+++ b/src/interactive.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Printf
 
diff --git a/src/interactive.mli b/src/interactive.mli
index b0cce425..46b52022 100644
--- a/src/interactive.mli
+++ b/src/interactive.mli
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Type_check
 
 val opt_interactive : bool ref
diff --git a/src/interpreter.ml b/src/interpreter.ml
index b3e8fe31..29598993 100644
--- a/src/interpreter.ml
+++ b/src/interpreter.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Value
 
@@ -755,11 +756,11 @@ let exp_of_fundef (FD_aux (FD_function (_, _, _, funcls), annot)) value =
   let pexp_of_funcl (FCL_aux (FCL_Funcl (_, pexp), _)) = pexp in
   E_aux (E_case (exp_of_value value, List.map pexp_of_funcl funcls), annot)
 
-let rec ast_letbinds (Defs defs) =
+let rec defs_letbinds defs =
   match defs with
   | [] -> []
-  | DEF_val lb :: defs -> lb :: ast_letbinds (Defs defs)
-  | _ :: defs -> ast_letbinds (Defs defs)
+  | DEF_val lb :: defs -> lb :: defs_letbinds defs
+  | _ :: defs -> defs_letbinds defs
 
 let initial_lstate =
   { locals = Bindings.empty }
@@ -945,11 +946,11 @@ let rec run_frame frame =
 let eval_exp state exp =
   run_frame (Step (lazy "", state, return exp, []))
 
-let initial_gstate primops ast env =
+let initial_gstate primops defs env =
   { registers = Bindings.empty;
     allow_registers = true;
     primops = primops;
-    letbinds = ast_letbinds ast;
+    letbinds = defs_letbinds defs;
     fundefs = Bindings.empty;
     last_write_ea = None;
     typecheck_env = env;
@@ -972,14 +973,14 @@ let rec initialize_registers allow_registers gstate =
     | _ -> gstate
   in
   function
-  | Defs (def :: defs) ->
-     initialize_registers allow_registers (process_def def) (Defs defs)
-  | Defs [] -> gstate
+  | def :: defs ->
+     initialize_registers allow_registers (process_def def) defs
+  | [] -> gstate
 
-let initial_state ?(registers=true) ast env primops =
-  let gstate = initial_gstate primops ast env in
+let initial_state ?(registers=true) (Defs defs) env primops =
+  let gstate = initial_gstate primops defs env in
   let gstate =
-    { (initialize_registers registers gstate ast)
+    { (initialize_registers registers gstate defs)
       with allow_registers = registers }
   in
   initial_lstate, gstate
diff --git a/src/isail.ml b/src/isail.ml
index e7864751..7fcca62a 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -569,7 +569,7 @@ let handle_input' input =
            interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops;
            vs_ids := val_spec_ids !Interactive.ast
         | ":u" | ":unload" ->
-           Interactive.ast := Ast.Defs [];
+           Interactive.ast := Ast_defs.Defs [];
            Interactive.env := Type_check.initial_env;
            interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops;
            vs_ids := val_spec_ids !Interactive.ast;
@@ -693,7 +693,7 @@ let handle_input' input =
                 print_endline (emacs_error l (String.escaped msg))
            end
         | ":unload" ->
-           Interactive.ast := Ast.Defs [];
+           Interactive.ast := Ast_defs.Defs [];
            Interactive.env := Type_check.initial_env;
            interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops;
            vs_ids := val_spec_ids !Interactive.ast;
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index b2447125..a7e64fe4 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Jib
 open Jib_compile
diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli
index 2d3d3c2b..d4478c88 100644
--- a/src/jib/c_backend.mli
+++ b/src/jib/c_backend.mli
@@ -99,7 +99,7 @@ val optimize_alias : bool ref
 val optimize_fixed_int : bool ref
 val optimize_fixed_bits : bool ref
 
-val jib_of_ast : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx
-val compile_ast : Env.t -> out_channel -> string list -> tannot Ast.defs -> unit
+val jib_of_ast : Env.t -> tannot Ast_defs.defs -> cdef list * Jib_compile.ctx
+val compile_ast : Env.t -> out_channel -> string list -> tannot Ast_defs.defs -> unit
 
-val compile_ast_clib : Env.t -> tannot Ast.defs -> (Jib_compile.ctx -> cdef list -> unit) -> unit
+val compile_ast_clib : Env.t -> tannot Ast_defs.defs -> (Jib_compile.ctx -> cdef list -> unit) -> unit
diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml
index 3cf56ba4..ea4afd00 100644
--- a/src/jib/c_codegen.ml
+++ b/src/jib/c_codegen.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Jib
 open Jib_compile
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 42228cd6..4fd61a7d 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Jib
 open Jib_util
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 30f379d8..38d03d40 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -52,6 +52,7 @@
 
 open Anf
 open Ast
+open Ast_defs
 open Ast_util
 open Jib
 open Type_check
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 6cbd1b87..2e0299d9 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -50,6 +50,7 @@
 
 open Anf
 open Ast
+open Ast_defs
 open Ast_util
 open Jib
 open Jib_util
diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli
index 616877e4..421cbf2c 100644
--- a/src/jib/jib_smt.mli
+++ b/src/jib/jib_smt.mli
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Jib
 open Jib_util
diff --git a/src/latex.ml b/src/latex.ml
index be3e8748..7f9b1317 100644
--- a/src/latex.ml
+++ b/src/latex.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open PPrint
 open Printf
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 9bb47774..318cfa63 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -56,6 +56,7 @@
 
 open Parse_ast
 open Ast
+open Ast_defs
 open Ast_util
 module Big_int = Nat_big_num
 open Type_check
diff --git a/src/monomorphise.mli b/src/monomorphise.mli
index f8a17494..7db12078 100644
--- a/src/monomorphise.mli
+++ b/src/monomorphise.mli
@@ -48,6 +48,8 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+open Ast_defs
+
 type options = {
   auto : bool;                    (* Analyse ast to find splits for monomorphisation *)
   debug_analysis : int;           (* Debug output level for the automatic analysis *)
@@ -59,17 +61,17 @@ val monomorphise :
   string -> (* Target backend *)
   options ->
   ((string * int) * string) list -> (* List of splits from the command line *)
-  Type_check.tannot Ast.defs ->
-  Type_check.tannot Ast.defs
+  Type_check.tannot defs ->
+  Type_check.tannot defs
 
 (* Rewrite (combinations of) variable-sized operations into fixed-sized operations *)
-val mono_rewrites : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val mono_rewrites : Type_check.tannot defs -> Type_check.tannot defs
 
 (* Move complex nexps in function signatures into constraints *)
-val rewrite_toplevel_nexps : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_toplevel_nexps : Type_check.tannot defs -> Type_check.tannot defs
 
 (* Add casts across case splits *)
-val add_bitvector_casts : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val add_bitvector_casts : Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs
 
 (* Replace atom arguments which are fixed by a type parameter for a size with a singleton type *)
-val rewrite_atoms_to_singletons : string -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs
+val rewrite_atoms_to_singletons : string -> Type_check.tannot defs -> Type_check.tannot defs
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 98a43ebc..2f262ec3 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open PPrint
 open Type_check
diff --git a/src/optimize.ml b/src/optimize.ml
index b0d05bef..8c456a1b 100644
--- a/src/optimize.ml
+++ b/src/optimize.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Rewriter
 
diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index 5537f42c..2738e025 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Type_check
 
 (* Prints on formatter the defs as Lem Ast nodes *)
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index dbb0356d..cc5cd4da 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -50,6 +50,7 @@
 
 open Type_check
 open Ast
+open Ast_defs
 open Ast_util
 open Reporting
 open Rewriter
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index b18541a3..c3006d7a 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -50,6 +50,7 @@
 
 open Type_check
 open Ast
+open Ast_defs
 open Ast_util
 open Reporting
 open Rewriter
diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 4114920a..c306d0b6 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open PPrint
 
diff --git a/src/process_file.ml b/src/process_file.ml
index a0245c8f..2cf0325e 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -48,6 +48,7 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+open Ast_defs
 open PPrint
 open Pretty_print_common
 
@@ -263,7 +264,7 @@ let opt_ddump_tc_ast = ref false
 let opt_ddump_rewrite_ast = ref None
 let opt_dno_cast = ref false
 
-let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tannot Ast.defs * Type_check.Env.t =
+let check_ast (env : Type_check.Env.t) (defs : unit defs) : Type_check.tannot defs * Type_check.Env.t =
   let env = if !opt_dno_cast then Type_check.Env.no_casts env else env in
   let ast, env = Type_error.check env defs in
   let () = if !opt_ddump_tc_ast then Pretty_print_sail.pp_defs stdout ast else () in
diff --git a/src/process_file.mli b/src/process_file.mli
index ea00dd29..041026d5 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -48,6 +48,8 @@
 (*  SUCH DAMAGE.                                                          *)
 (**************************************************************************)
 
+open Ast_defs
+
 (** Parse a file. The optional loc argument is the location of the
    $include directive that is importing the file, if applicable. *)
 val parse_file : ?loc:Parse_ast.l -> string -> Lexer.comment list * Parse_ast.def list
@@ -57,10 +59,10 @@ val have_symbol : string -> bool
 val add_symbol : string -> unit
 
 val preprocess : (Arg.key * Arg.spec * Arg.doc) list -> Parse_ast.def list -> Parse_ast.def list
-val check_ast : Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
-val rewrite_ast_initial : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
-val rewrite_ast_target : string -> Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
-val rewrite_ast_check : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
+val check_ast : Type_check.Env.t -> unit defs -> Type_check.tannot defs * Type_check.Env.t
+val rewrite_ast_initial : Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs * Type_check.Env.t
+val rewrite_ast_target : string -> Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs * Type_check.Env.t
+val rewrite_ast_check : Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs * Type_check.Env.t
 
 val opt_file_out : string option ref
 val opt_memo_z3 : bool ref
@@ -84,7 +86,7 @@ type out_type =
 val output :
   string ->                           (* The path to the library *)
   out_type ->                         (* Backend kind *)
-  (string * Type_check.Env.t * Type_check.tannot Ast.defs) list -> (*File names paired with definitions *)
+  (string * Type_check.Env.t * Type_check.tannot Ast_defs.defs) list -> (*File names paired with definitions *)
   unit
 
 (** [always_replace_files] determines whether Sail only updates modified files.
@@ -93,6 +95,6 @@ val output :
     the output file is only updated, if its content really changes. *)
 val always_replace_files : bool ref
 
-val load_files : ?check:bool -> (Arg.key * Arg.spec * Arg.doc) list -> Type_check.Env.t -> string list -> (string * Type_check.tannot Ast.defs * Type_check.Env.t)
+val load_files : ?check:bool -> (Arg.key * Arg.spec * Arg.doc) list -> Type_check.Env.t -> string list -> (string * Type_check.tannot defs * Type_check.Env.t)
 
-val descatter : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
+val descatter : Type_check.Env.t -> Type_check.tannot defs -> Type_check.tannot defs * Type_check.Env.t
diff --git a/src/property.ml b/src/property.ml
index 83594f4f..854677c8 100644
--- a/src/property.ml
+++ b/src/property.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Parser_combinators
 
diff --git a/src/property.mli b/src/property.mli
index 66a732b9..bba1f638 100644
--- a/src/property.mli
+++ b/src/property.mli
@@ -52,6 +52,7 @@
    $counterexample pragmas. *)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Type_check
 
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 3b68f493..eb8208dd 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -50,6 +50,7 @@
 
 module Big_int = Nat_big_num
 open Ast
+open Ast_defs
 open Ast_util
 open Type_check
 
diff --git a/src/rewriter.mli b/src/rewriter.mli
index f61bcc66..9ea01096 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -52,6 +52,7 @@
 
 module Big_int = Nat_big_num
 open Ast
+open Ast_defs
 open Type_check
 
 type 'a rewriters = { rewrite_exp  : 'a rewriters -> 'a exp -> 'a exp;
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 574356d4..b1cfce86 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -50,6 +50,7 @@
 
 module Big_int = Nat_big_num
 open Ast
+open Ast_defs
 open Ast_util
 open Type_check
 open Spec_analysis
diff --git a/src/rewrites.mli b/src/rewrites.mli
index 43a2e057..4212993e 100644
--- a/src/rewrites.mli
+++ b/src/rewrites.mli
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Type_check
 
 (* Monomorphisation options *)
diff --git a/src/scattered.ml b/src/scattered.ml
index 92cb3561..b8979f31 100644
--- a/src/scattered.ml
+++ b/src/scattered.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 
 let funcl_id (FCL_aux (FCL_Funcl (id, _), _)) = id
diff --git a/src/slice.ml b/src/slice.ml
index c249fb5a..7611a54c 100644
--- a/src/slice.ml
+++ b/src/slice.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Rewriter
 
diff --git a/src/slice.mli b/src/slice.mli
index 0c15defb..58d2cf17 100644
--- a/src/slice.mli
+++ b/src/slice.mli
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 
 type node =
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 542ecaae..bb30e971 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -49,8 +49,9 @@
 (**************************************************************************)
 
 open Ast
-open Util
+open Ast_defs
 open Ast_util
+open Util
 
 module Nameset = Set.Make(String)
 
@@ -511,7 +512,7 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function
      Reporting.unreachable (id_loc id) __POS__ "Loop termination measures should be rewritten before now"
 
 
-let group_defs consider_scatter_as_one (Ast.Defs defs) =
+let group_defs consider_scatter_as_one (Defs defs) =
   List.map (fun d -> (fv_of_def false consider_scatter_as_one defs d,d)) defs
 
 
diff --git a/src/spec_analysis.mli b/src/spec_analysis.mli
index 41ab9b6c..a2ed74bf 100644
--- a/src/spec_analysis.mli
+++ b/src/spec_analysis.mli
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Util
 open Type_check
diff --git a/src/specialize.ml b/src/specialize.ml
index d705b83a..b703d27a 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Rewriter
 
diff --git a/src/specialize.mli b/src/specialize.mli
index ddfb0c67..ae71bfcb 100644
--- a/src/specialize.mli
+++ b/src/specialize.mli
@@ -51,6 +51,7 @@
 (** Rewrites for removing polymorphism from specifications *)
 
 open Ast
+open Ast_defs
 open Ast_util
 open Type_check
 
diff --git a/src/splice.ml b/src/splice.ml
index dd19e664..6198a4c7 100644
--- a/src/splice.ml
+++ b/src/splice.ml
@@ -4,6 +4,7 @@
 *)
 
 open Ast
+open Ast_defs
 open Ast_util
 
 let scan_defs (Defs defs) =
diff --git a/src/state.ml b/src/state.ml
index 8d487d3e..a598be92 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -53,6 +53,7 @@ module Big_int = Nat_big_num
 open Initial_check
 open Type_check
 open Ast
+open Ast_defs
 open Ast_util
 open PPrint
 open Pretty_print_common
diff --git a/src/toFromInterp_backend.ml b/src/toFromInterp_backend.ml
index 30b93d90..11d66ef6 100644
--- a/src/toFromInterp_backend.ml
+++ b/src/toFromInterp_backend.ml
@@ -49,6 +49,7 @@
 (**************************************************************************)
 
 open Ast
+open Ast_defs
 open Ast_util
 open PPrint
 open Type_check
diff --git a/src/type_check.ml b/src/type_check.ml
index 86bfc251..afe24bc6 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -49,8 +49,9 @@
 (**************************************************************************)
 
 open Ast
-open Util
+open Ast_defs
 open Ast_util
+open Util
 open Lazy
 
 module Big_int = Nat_big_num
diff --git a/src/type_check.mli b/src/type_check.mli
index 75c0d2a2..9c2cd236 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -51,6 +51,7 @@
 (** The type checker API *)
 
 open Ast
+open Ast_defs
 open Ast_util
 module Big_int = Nat_big_num
 
diff --git a/src/type_error.ml b/src/type_error.ml
index 1ac771bf..3ae06c31 100644
--- a/src/type_error.ml
+++ b/src/type_error.ml
@@ -50,6 +50,7 @@
 
 open Util
 open Ast
+open Ast_defs
 open Ast_util
 open Type_check