Move some files to the Charon project

29 files changed, 57 insertions, 3486 deletions

diff --git a/compiler/Assumed.ml b/compiler/Assumed.ml
index cb089c08..7fba3c5c 100644
--- a/compiler/Assumed.ml
+++ b/compiler/Assumed.ml
@@ -6,9 +6,9 @@
     Semantically speaking, we thus handle [Box::free] as a value drop and
     not as a function call, and thus never need its signature.
     
-    TODO: implementing the concrete evaluation functions for the assumed
-    functions is really annoying (see
-    [InterpreterStatements.eval_non_local_function_call_concrete]).
+    TODO: implementing the concrete evaluation functions for the
+    assumed functions is really annoying (see
+    {!InterpreterStatements.eval_non_local_function_call_concrete}),
     I think it should be possible, in most situations, to write bodies which
     model the behaviour of those unsafe functions. For instance, [Box::deref_mut]
     should simply be:
diff --git a/compiler/Collections.ml b/compiler/Collections.ml
index 0933b3e4..0b24004f 100644
--- a/compiler/Collections.ml
+++ b/compiler/Collections.ml
@@ -1,378 +1 @@
-(** The following file redefines several modules like Map or Set. *)
-
-module F = Format
-
-module List = struct
-  include List
-
-  (** Split a list at a given index.
-  
-      [split_at ls i] splits [ls] into two lists where the first list has
-      length [i].
-      
-      Raise [Failure] if the list is too short.
-  *)
-  let rec split_at (ls : 'a list) (i : int) =
-    if i < 0 then raise (Invalid_argument "split_at take positive integers")
-    else if i = 0 then ([], ls)
-    else
-      match ls with
-      | [] ->
-          raise
-            (Failure "The int given to split_at should be <= the list's length")
-      | x :: ls' ->
-          let ls1, ls2 = split_at ls' (i - 1) in
-          (x :: ls1, ls2)
-
-  (** Pop the last element of a list
-     
-      Raise [Failure] if the list is empty.
-   *)
-  let rec pop_last (ls : 'a list) : 'a list * 'a =
-    match ls with
-    | [] -> raise (Failure "The list is empty")
-    | [ x ] -> ([], x)
-    | x :: ls ->
-        let ls, last = pop_last ls in
-        (x :: ls, last)
-
-  (** Return the n first elements of the list *)
-  let prefix (n : int) (ls : 'a list) : 'a list = fst (split_at ls n)
-
-  (** Iter and link the iterations.
-
-      Iterate over a list, but call a function between every two elements
-      (but not before the first element, and not after the last).
-   *)
-  let iter_link (link : unit -> unit) (f : 'a -> unit) (ls : 'a list) : unit =
-    let rec iter ls =
-      match ls with
-      | [] -> ()
-      | [ x ] -> f x
-      | x :: y :: ls ->
-          f x;
-          link ();
-          iter (y :: ls)
-    in
-    iter ls
-
-  (** Fold and link the iterations.
-
-      Similar to {!iter_link} but for fold left operations.
-   *)
-  let fold_left_link (link : unit -> unit) (f : 'a -> 'b -> 'a) (init : 'a)
-      (ls : 'b list) : 'a =
-    let rec fold (acc : 'a) (ls : 'b list) : 'a =
-      match ls with
-      | [] -> acc
-      | [ x ] -> f acc x
-      | x :: y :: ls ->
-          let acc = f acc x in
-          link ();
-          fold acc (y :: ls)
-    in
-    fold init ls
-
-  let to_cons_nil (ls : 'a list) : 'a =
-    match ls with
-    | [ x ] -> x
-    | _ -> raise (Failure "The list should have length exactly one")
-
-  let pop (ls : 'a list) : 'a * 'a list =
-    match ls with
-    | x :: ls' -> (x, ls')
-    | _ -> raise (Failure "The list should have length > 0")
-end
-
-module type OrderedType = sig
-  include Map.OrderedType
-
-  val to_string : t -> string
-  val pp_t : Format.formatter -> t -> unit
-  val show_t : t -> string
-end
-
-(** Ordered string *)
-module OrderedString : OrderedType with type t = string = struct
-  include String
-
-  let to_string s = s
-  let pp_t fmt s = Format.pp_print_string fmt s
-  let show_t s = s
-end
-
-module type Map = sig
-  include Map.S
-
-  val add_list : (key * 'a) list -> 'a t -> 'a t
-  val of_list : (key * 'a) list -> 'a t
-
-  (** "Simple" pretty printing function.
-  
-      Is useful when we need to customize a bit [show_t], but without using
-      something as burdensome as [pp_t].
-  
-      [to_string (Some indent) m] prints [m] by breaking line after every binding
-      and inserting [indent].
-   *)
-  val to_string : string option -> ('a -> string) -> 'a t -> string
-
-  val pp : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
-  val show : ('a -> string) -> 'a t -> string
-end
-
-module MakeMap (Ord : OrderedType) : Map with type key = Ord.t = struct
-  module Map = Map.Make (Ord)
-  include Map
-
-  let add_list bl m = List.fold_left (fun s (key, e) -> add key e s) m bl
-  let of_list bl = add_list bl empty
-
-  let to_string indent_opt a_to_string m =
-    let indent, break =
-      match indent_opt with Some indent -> (indent, "\n") | None -> ("", " ")
-    in
-    let sep = "," ^ break in
-    let ls =
-      Map.fold
-        (fun key v ls ->
-          (indent ^ Ord.to_string key ^ " -> " ^ a_to_string v) :: ls)
-        m []
-    in
-    match ls with
-    | [] -> "{}"
-    | _ -> "{" ^ break ^ String.concat sep (List.rev ls) ^ break ^ "}"
-
-  let pp (pp_a : Format.formatter -> 'a -> unit) (fmt : Format.formatter)
-      (m : 'a t) : unit =
-    let pp_string = F.pp_print_string fmt in
-    let pp_space () = F.pp_print_space fmt () in
-    pp_string "{";
-    F.pp_open_box fmt 2;
-    Map.iter
-      (fun key x ->
-        Ord.pp_t fmt key;
-        pp_space ();
-        pp_string "->";
-        pp_space ();
-        pp_a fmt x;
-        pp_string ",";
-        F.pp_print_break fmt 1 0)
-      m;
-    F.pp_close_box fmt ();
-    F.pp_print_break fmt 0 0;
-    pp_string "}"
-
-  let show show_a m = to_string None show_a m
-end
-
-module type Set = sig
-  include Set.S
-
-  val add_list : elt list -> t -> t
-  val of_list : elt list -> t
-
-  (** "Simple" pretty printing function.
-  
-      Is useful when we need to customize a bit [show_t], but without using
-      something as burdensome as [pp_t].
-  
-      [to_string (Some indent) s] prints [s] by breaking line after every element
-      and inserting [indent].
-   *)
-  val to_string : string option -> t -> string
-
-  val pp : Format.formatter -> t -> unit
-  val show : t -> string
-  val pairwise_distinct : elt list -> bool
-end
-
-module MakeSet (Ord : OrderedType) : Set with type elt = Ord.t = struct
-  module Set = Set.Make (Ord)
-  include Set
-
-  let add_list bl s = List.fold_left (fun s e -> add e s) s bl
-  let of_list bl = add_list bl empty
-
-  let to_string indent_opt m =
-    let indent, break =
-      match indent_opt with Some indent -> (indent, "\n") | None -> ("", " ")
-    in
-    let sep = "," ^ break in
-    let ls = Set.fold (fun v ls -> (indent ^ Ord.to_string v) :: ls) m [] in
-    match ls with
-    | [] -> "{}"
-    | _ -> "{" ^ break ^ String.concat sep (List.rev ls) ^ break ^ "}"
-
-  let pp (fmt : Format.formatter) (m : t) : unit =
-    let pp_string = F.pp_print_string fmt in
-    pp_string "{";
-    F.pp_open_box fmt 2;
-    Set.iter
-      (fun x ->
-        Ord.pp_t fmt x;
-        pp_string ",";
-        F.pp_print_break fmt 1 0)
-      m;
-    F.pp_close_box fmt ();
-    F.pp_print_break fmt 0 0;
-    pp_string "}"
-
-  let show s = to_string None s
-
-  let pairwise_distinct ls =
-    let s = ref empty in
-    let rec check ls =
-      match ls with
-      | [] -> true
-      | x :: ls' ->
-          if mem x !s then false
-          else (
-            s := add x !s;
-            check ls')
-    in
-    check ls
-end
-
-(** A map where the bindings are injective (i.e., if two keys are distinct,
-    their bindings are distinct).
-    
-    This is useful for instance when generating mappings from our internal
-    identifiers to names (i.e., strings) when generating code, in order to
-    make sure that we don't have potentially dangerous collisions.
- *)
-module type InjMap = sig
-  type key
-  type elem
-  type t
-
-  val empty : t
-  val is_empty : t -> bool
-  val mem : key -> t -> bool
-  val add : key -> elem -> t -> t
-  val singleton : key -> elem -> t
-  val remove : key -> t -> t
-  val compare : (elem -> elem -> int) -> t -> t -> int
-  val equal : (elem -> elem -> bool) -> t -> t -> bool
-  val iter : (key -> elem -> unit) -> t -> unit
-  val fold : (key -> elem -> 'b -> 'b) -> t -> 'b -> 'b
-  val for_all : (key -> elem -> bool) -> t -> bool
-  val exists : (key -> elem -> bool) -> t -> bool
-  val filter : (key -> elem -> bool) -> t -> t
-  val partition : (key -> elem -> bool) -> t -> t * t
-  val cardinal : t -> int
-  val bindings : t -> (key * elem) list
-  val min_binding : t -> key * elem
-  val min_binding_opt : t -> (key * elem) option
-  val max_binding : t -> key * elem
-  val max_binding_opt : t -> (key * elem) option
-  val choose : t -> key * elem
-  val choose_opt : t -> (key * elem) option
-  val split : key -> t -> t * elem option * t
-  val find : key -> t -> elem
-  val find_opt : key -> t -> elem option
-  val find_first : (key -> bool) -> t -> key * elem
-  val find_first_opt : (key -> bool) -> t -> (key * elem) option
-  val find_last : (key -> bool) -> t -> key * elem
-  val find_last_opt : (key -> bool) -> t -> (key * elem) option
-  val to_seq : t -> (key * elem) Seq.t
-  val to_seq_from : key -> t -> (key * elem) Seq.t
-  val add_seq : (key * elem) Seq.t -> t -> t
-  val of_seq : (key * elem) Seq.t -> t
-  val add_list : (key * elem) list -> t -> t
-  val of_list : (key * elem) list -> t
-end
-
-(** See {!InjMap} *)
-module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
-  InjMap with type key = Key.t with type elem = Elem.t = struct
-  module Map = MakeMap (Key)
-  module Set = MakeSet (Elem)
-
-  type key = Key.t
-  type elem = Elem.t
-  type t = { map : elem Map.t; elems : Set.t }
-
-  let empty = { map = Map.empty; elems = Set.empty }
-  let is_empty m = Map.is_empty m.map
-  let mem k m = Map.mem k m.map
-
-  let add k e m =
-    assert (not (Set.mem e m.elems));
-    { map = Map.add k e m.map; elems = Set.add e m.elems }
-
-  let singleton k e = { map = Map.singleton k e; elems = Set.singleton e }
-
-  let remove k m =
-    match Map.find_opt k m.map with
-    | None -> m
-    | Some x -> { map = Map.remove k m.map; elems = Set.remove x m.elems }
-
-  let compare f m1 m2 = Map.compare f m1.map m2.map
-  let equal f m1 m2 = Map.equal f m1.map m2.map
-  let iter f m = Map.iter f m.map
-  let fold f m x = Map.fold f m.map x
-  let for_all f m = Map.for_all f m.map
-  let exists f m = Map.exists f m.map
-
-  (** Small helper *)
-  let bindings_to_elems_set (bls : (key * elem) list) : Set.t =
-    let elems = List.map snd bls in
-    let elems = List.fold_left (fun s e -> Set.add e s) Set.empty elems in
-    elems
-
-  (** Small helper *)
-  let map_to_elems_set (map : elem Map.t) : Set.t =
-    bindings_to_elems_set (Map.bindings map)
-
-  (** Small helper *)
-  let map_to_t (map : elem Map.t) : t =
-    let elems = map_to_elems_set map in
-    { map; elems }
-
-  let filter f m =
-    let map = Map.filter f m.map in
-    let elems = map_to_elems_set map in
-    { map; elems }
-
-  let partition f m =
-    let map1, map2 = Map.partition f m.map in
-    (map_to_t map1, map_to_t map2)
-
-  let cardinal m = Map.cardinal m.map
-  let bindings m = Map.bindings m.map
-  let min_binding m = Map.min_binding m.map
-  let min_binding_opt m = Map.min_binding_opt m.map
-  let max_binding m = Map.max_binding m.map
-  let max_binding_opt m = Map.max_binding_opt m.map
-  let choose m = Map.choose m.map
-  let choose_opt m = Map.choose_opt m.map
-
-  let split k m =
-    let l, data, r = Map.split k m.map in
-    let l = map_to_t l in
-    let r = map_to_t r in
-    (l, data, r)
-
-  let find k m = Map.find k m.map
-  let find_opt k m = Map.find_opt k m.map
-  let find_first k m = Map.find_first k m.map
-  let find_first_opt k m = Map.find_first_opt k m.map
-  let find_last k m = Map.find_last k m.map
-  let find_last_opt k m = Map.find_last_opt k m.map
-  let to_seq m = Map.to_seq m.map
-  let to_seq_from k m = Map.to_seq_from k m.map
-
-  let rec add_seq s m =
-    (* Note that it is important to check that we don't add bindings mapping
-     * to the same element *)
-    match s () with
-    | Seq.Nil -> m
-    | Seq.Cons ((k, e), s) ->
-        let m = add k e m in
-        add_seq s m
-
-  let of_seq s = add_seq s empty
-  let add_list ls m = List.fold_left (fun m (key, elem) -> add key elem m) m ls
-  let of_list ls = add_list ls empty
-end
+include Charon.Collections
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 510976f4..52815859 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -1,4 +1,5 @@
 open Types
+open Expressions
 open Values
 open LlbcAst
 module V = Values
diff --git a/compiler/Crates.ml b/compiler/Crates.ml
index eb47a8e1..81f42cea 100644
--- a/compiler/Crates.ml
+++ b/compiler/Crates.ml
@@ -1,90 +1 @@
-open Types
-open LlbcAst
-
-type 'id g_declaration_group = NonRec of 'id | Rec of 'id list
-[@@deriving show]
-
-type type_declaration_group = TypeDeclId.id g_declaration_group
-[@@deriving show]
-
-type fun_declaration_group = FunDeclId.id g_declaration_group [@@deriving show]
-
-(** Module declaration. Globals cannot be mutually recursive. *)
-type declaration_group =
-  | Type of type_declaration_group
-  | Fun of fun_declaration_group
-  | Global of GlobalDeclId.id
-[@@deriving show]
-
-(** LLBC crate *)
-type llbc_crate = {
-  name : string;
-  declarations : declaration_group list;
-  types : type_decl list;
-  functions : fun_decl list;
-  globals : global_decl list;
-}
-
-let compute_defs_maps (c : llbc_crate) :
-    type_decl TypeDeclId.Map.t
-    * fun_decl FunDeclId.Map.t
-    * global_decl GlobalDeclId.Map.t =
-  let types_map =
-    List.fold_left
-      (fun m (def : type_decl) -> TypeDeclId.Map.add def.def_id def m)
-      TypeDeclId.Map.empty c.types
-  in
-  let funs_map =
-    List.fold_left
-      (fun m (def : fun_decl) -> FunDeclId.Map.add def.def_id def m)
-      FunDeclId.Map.empty c.functions
-  in
-  let globals_map =
-    List.fold_left
-      (fun m (def : global_decl) -> GlobalDeclId.Map.add def.def_id def m)
-      GlobalDeclId.Map.empty c.globals
-  in
-  (types_map, funs_map, globals_map)
-
-(** Split a module's declarations between types, functions and globals *)
-let split_declarations (decls : declaration_group list) :
-    type_declaration_group list
-    * fun_declaration_group list
-    * GlobalDeclId.id list =
-  let rec split decls =
-    match decls with
-    | [] -> ([], [], [])
-    | d :: decls' -> (
-        let types, funs, globals = split decls' in
-        match d with
-        | Type decl -> (decl :: types, funs, globals)
-        | Fun decl -> (types, decl :: funs, globals)
-        | Global decl -> (types, funs, decl :: globals))
-  in
-  split decls
-
-(** Split a module's declarations into three maps from type/fun/global ids to
-    declaration groups.
- *)
-let split_declarations_to_group_maps (decls : declaration_group list) :
-    type_declaration_group TypeDeclId.Map.t
-    * fun_declaration_group FunDeclId.Map.t
-    * GlobalDeclId.Set.t =
-  let module G (M : Map.S) = struct
-    let add_group (map : M.key g_declaration_group M.t)
-        (group : M.key g_declaration_group) : M.key g_declaration_group M.t =
-      match group with
-      | NonRec id -> M.add id group map
-      | Rec ids -> List.fold_left (fun map id -> M.add id group map) map ids
-
-    let create_map (groups : M.key g_declaration_group list) :
-        M.key g_declaration_group M.t =
-      List.fold_left add_group M.empty groups
-  end in
-  let types, funs, globals = split_declarations decls in
-  let module TG = G (TypeDeclId.Map) in
-  let types = TG.create_map types in
-  let module FG = G (FunDeclId.Map) in
-  let funs = FG.create_map funs in
-  let globals = GlobalDeclId.Set.of_list globals in
-  (types, funs, globals)
+include Charon.Crates
diff --git a/compiler/Errors.ml b/compiler/Errors.ml
index 31a53cf4..58dd3a0b 100644
--- a/compiler/Errors.ml
+++ b/compiler/Errors.ml
@@ -1,2 +1 @@
-exception IntegerOverflow of unit
-exception Unimplemented
+include Charon.Errors
diff --git a/compiler/Expressions.ml b/compiler/Expressions.ml
index 1fca7284..06bca9e5 100644
--- a/compiler/Expressions.ml
+++ b/compiler/Expressions.ml
@@ -1,118 +1 @@
-open Types
-open Values
-
-type field_proj_kind =
-  | ProjAdt of TypeDeclId.id * VariantId.id option
-  | ProjOption of VariantId.id
-      (** Option is an assumed type, coming from the standard library *)
-  | ProjTuple of int
-[@@deriving show]
-(* arity of the tuple *)
-
-type projection_elem =
-  | Deref
-  | DerefBox
-  | Field of field_proj_kind * FieldId.id
-[@@deriving show]
-
-type projection = projection_elem list [@@deriving show]
-type place = { var_id : VarId.id; projection : projection } [@@deriving show]
-type borrow_kind = Shared | Mut | TwoPhaseMut [@@deriving show]
-
-type unop =
-  | Not
-  | Neg
-  | Cast of integer_type * integer_type
-      (** Cast an integer from a source type to a target type *)
-[@@deriving show, ord]
-
-(** A binary operation
-
-    Note that we merge checked binops and unchecked binops: we perform a
-    micro-pass on the MIR AST to remove the assertions introduced by rustc,
-    and later extract the binops which can fail (addition, substraction, etc.)
-    or have preconditions (division, remainder...) to monadic functions.
- *)
-type binop =
-  | BitXor
-  | BitAnd
-  | BitOr
-  | Eq
-  | Lt
-  | Le
-  | Ne
-  | Ge
-  | Gt
-  | Div
-  | Rem
-  | Add
-  | Sub
-  | Mul
-  | Shl
-  | Shr
-[@@deriving show, ord]
-
-let all_binops =
-  [
-    BitXor;
-    BitAnd;
-    BitOr;
-    Eq;
-    Lt;
-    Le;
-    Ne;
-    Ge;
-    Gt;
-    Div;
-    Rem;
-    Add;
-    Sub;
-    Mul;
-    Shl;
-    Shr;
-  ]
-
-type operand =
-  | Copy of place
-  | Move of place
-  | Constant of ety * primitive_value
-[@@deriving show]
-
-(** An aggregated ADT.
-
-    Note that ADTs are desaggregated at some point in MIR. For instance, if
-    we have in Rust:
-    {[
-      let ls = Cons(hd, tl);
-    ]}
-    
-    In MIR we have (yes, the discriminant update happens *at the end* for some
-    reason):
-    {[
-      (ls as Cons).0 = move hd;
-      (ls as Cons).1 = move tl;
-      discriminant(ls) = 0; // assuming [Cons] is the variant of index 0
-    ]}
-    
-    Note that in our semantics, we handle both cases (in case of desaggregated
-    initialization, [ls] is initialized to [⊥], then this [⊥] is expanded to
-    [Cons (⊥, ⊥)] upon the first assignment, at which point we can initialize
-    the field 0, etc.).
- *)
-type aggregate_kind =
-  | AggregatedTuple
-  | AggregatedOption of VariantId.id * ety
-  (* TODO: AggregatedOption should be merged with AggregatedAdt *)
-  | AggregatedAdt of
-      TypeDeclId.id * VariantId.id option * erased_region list * ety list
-[@@deriving show]
-
-(* TODO: move the aggregate kind to operands *)
-type rvalue =
-  | Use of operand
-  | Ref of place * borrow_kind
-  | UnaryOp of unop * operand
-  | BinaryOp of binop * operand * operand
-  | Discriminant of place
-  | Aggregate of aggregate_kind * operand list
-[@@deriving show]
+include Charon.Expressions
diff --git a/compiler/ExpressionsUtils.ml b/compiler/ExpressionsUtils.ml
index c3ccfb15..7dfef101 100644
--- a/compiler/ExpressionsUtils.ml
+++ b/compiler/ExpressionsUtils.ml
@@ -1,10 +1 @@
-module E = Expressions
-
-let unop_can_fail (unop : E.unop) : bool =
-  match unop with Neg | Cast _ -> true | Not -> false
-
-let binop_can_fail (binop : E.binop) : bool =
-  match binop with
-  | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt -> false
-  | Div | Rem | Add | Sub | Mul -> true
-  | Shl | Shr -> raise Errors.Unimplemented
+include Charon.ExpressionsUtils
diff --git a/compiler/Identifiers.ml b/compiler/Identifiers.ml
index b022b18d..513d0eaa 100644
--- a/compiler/Identifiers.ml
+++ b/compiler/Identifiers.ml
@@ -1,139 +1 @@
-module C = Collections
-
-(** Signature for a module describing an identifier.
-    
-    We often need identifiers (for definitions, variables, etc.) and in
-    order to make sure we don't mix them, we use a generative functor
-    (see {!IdGen}).
-*)
-module type Id = sig
-  type id
-
-  (** Id generator - simply a counter *)
-  type generator
-
-  val zero : id
-  val generator_zero : generator
-  val generator_from_incr_id : id -> generator
-  val fresh_stateful_generator : unit -> generator ref * (unit -> id)
-  val mk_stateful_generator : generator -> generator ref * (unit -> id)
-  val incr : id -> id
-
-  (* TODO: this should be stateful! - but we may want to be able to duplicate
-     contexts...
-     Maybe we could have a [fresh] and a [global_fresh]
-     TODO: change the order of the returned types
-  *)
-  val fresh : generator -> id * generator
-  val to_string : id -> string
-  val pp_id : Format.formatter -> id -> unit
-  val show_id : id -> string
-  val id_of_json : Yojson.Basic.t -> (id, string) result
-  val compare_id : id -> id -> int
-  val max : id -> id -> id
-  val min : id -> id -> id
-  val pp_generator : Format.formatter -> generator -> unit
-  val show_generator : generator -> string
-  val to_int : id -> int
-  val of_int : int -> id
-  val nth : 'a list -> id -> 'a
-  (* TODO: change the signature (invert the index and the list *)
-
-  val nth_opt : 'a list -> id -> 'a option
-
-  (** Update the nth element of the list.
-
-      Raises [Invalid_argument] if the identifier is out of range.
-   *)
-  val update_nth : 'a list -> id -> 'a -> 'a list
-
-  val mapi : (id -> 'a -> 'b) -> 'a list -> 'b list
-
-  (** Same as {!mapi}, but where the indices start with 1.
-       
-      TODO: generalize to [map_from_i]
-   *)
-  val mapi_from1 : (id -> 'a -> 'b) -> 'a list -> 'b list
-
-  val iteri : (id -> 'a -> unit) -> 'a list -> unit
-
-  module Ord : C.OrderedType with type t = id
-  module Set : C.Set with type elt = id
-  module Map : C.Map with type key = id
-end
-
-(** Generative functor for identifiers.
-
-    See {!Id}.
-*)
-module IdGen () : Id = struct
-  (* TODO: use Z.t *)
-  type id = int [@@deriving show]
-  type generator = id [@@deriving show]
-
-  let zero = 0
-  let generator_zero = 0
-
-  let incr x =
-    (* Identifiers should never overflow (because max_int is a really big
-     * value - but we really want to make sure we detect overflows if
-     * they happen *)
-    if x = max_int then raise (Errors.IntegerOverflow ()) else x + 1
-
-  let generator_from_incr_id id = incr id
-
-  let mk_stateful_generator g =
-    let g = ref g in
-    let fresh () =
-      let id = !g in
-      g := incr id;
-      id
-    in
-    (g, fresh)
-
-  let fresh_stateful_generator () = mk_stateful_generator 0
-  let fresh gen = (gen, incr gen)
-  let to_string = string_of_int
-  let to_int x = x
-  let of_int x = x
-
-  let id_of_json js =
-    (* TODO: check boundaries ? *)
-    match js with
-    | `Int i -> Ok i
-    | _ -> Error ("id_of_json: failed on " ^ Yojson.Basic.show js)
-
-  let compare_id = compare
-  let max id0 id1 = if id0 > id1 then id0 else id1
-  let min id0 id1 = if id0 < id1 then id0 else id1
-  let nth v id = List.nth v id
-  let nth_opt v id = List.nth_opt v id
-
-  let rec update_nth vec id v =
-    match (vec, id) with
-    | [], _ -> raise (Invalid_argument "Out of range")
-    | _ :: vec', 0 -> v :: vec'
-    | x :: vec', _ -> x :: update_nth vec' (id - 1) v
-
-  let mapi = List.mapi
-
-  let mapi_from1 f ls =
-    let rec aux i ls =
-      match ls with [] -> [] | x :: ls' -> f i x :: aux (i + 1) ls'
-    in
-    aux 1 ls
-
-  let iteri = List.iteri
-
-  module Ord = struct
-    type t = id
-
-    let compare = compare
-    let to_string = to_string
-    let pp_t = pp_id
-    let show_t = show_id
-  end
-
-  module Set = C.MakeSet (Ord)
-  module Map = C.MakeMap (Ord)
-end
+include Charon.Identifiers
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index f935734e..308f561c 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -315,7 +315,7 @@ let get_non_local_function_return_type (fid : A.assumed_fun_id)
 let move_return_value (config : C.config) (cf : V.typed_value -> m_fun) : m_fun
     =
  fun ctx ->
-  let ret_vid = V.VarId.zero in
+  let ret_vid = E.VarId.zero in
   let cc = eval_operand config (E.Move (mk_place_from_var_id ret_vid)) in
   cc cf ctx
 
@@ -334,7 +334,7 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
   log#ldebug (lazy ("ctx_pop_frame:\n" ^ eval_ctx_to_string ctx));
 
   (* List the local variables, but the return variable *)
-  let ret_vid = V.VarId.zero in
+  let ret_vid = E.VarId.zero in
   let rec list_locals env =
     match env with
     | [] -> raise (Failure "Inconsistent environment")
@@ -345,12 +345,12 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
         if var.index <> ret_vid then var.index :: locals else locals
     | C.Frame :: _ -> []
   in
-  let locals : V.VarId.id list = list_locals ctx.env in
+  let locals : E.VarId.id list = list_locals ctx.env in
   (* Debug *)
   log#ldebug
     (lazy
       ("ctx_pop_frame: locals in which to drop the outer loans: ["
-      ^ String.concat "," (List.map V.VarId.to_string locals)
+      ^ String.concat "," (List.map E.VarId.to_string locals)
       ^ "]"));
 
   (* Move the return value out of the return variable *)
@@ -447,7 +447,7 @@ let eval_box_new_concrete (config : C.config)
         let box_v = mk_typed_value box_ty box_v in
 
         (* Move this value to the return variable *)
-        let dest = mk_place_from_var_id V.VarId.zero in
+        let dest = mk_place_from_var_id E.VarId.zero in
         let cf_assign = assign_to_place config box_v dest in
 
         (* Continue *)
@@ -496,7 +496,7 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config)
             raise (Failure "Unreachable")
         | Ok borrowed_value ->
             (* Move and continue *)
-            let destp = mk_place_from_var_id V.VarId.zero in
+            let destp = mk_place_from_var_id E.VarId.zero in
             assign_to_place config borrowed_value destp cf
       in
 
@@ -595,7 +595,7 @@ let eval_non_local_function_call_concrete (config : C.config)
         let cc = push_frame in
 
         (* Create and push the return variable *)
-        let ret_vid = V.VarId.zero in
+        let ret_vid = E.VarId.zero in
         let ret_ty =
           get_non_local_function_return_type fid region_params type_params
         in
@@ -604,7 +604,7 @@ let eval_non_local_function_call_concrete (config : C.config)
 
         (* Create and push the input variables *)
         let input_vars =
-          V.VarId.mapi_from1
+          E.VarId.mapi_from1
             (fun id (v : V.typed_value) -> (mk_var id None v.V.ty, v))
             args_vl
         in
@@ -922,7 +922,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
   (* Compose and apply *)
   comp cc cf_eval_st cf ctx
 
-and eval_global (config : C.config) (dest : V.VarId.id)
+and eval_global (config : C.config) (dest : E.VarId.id)
     (gid : LA.GlobalDeclId.id) : st_cm_fun =
  fun cf ctx ->
   let global = C.ctx_lookup_global_decl ctx gid in
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index e6033e9e..578ee5ef 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -30,12 +30,12 @@ let statement_to_string_with_tab ctx = PA.statement_to_string ctx "  " "  "
 let same_symbolic_id (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : bool =
   sv0.V.sv_id = sv1.V.sv_id
 
-let mk_var (index : V.VarId.id) (name : string option) (var_ty : T.ety) : A.var
+let mk_var (index : E.VarId.id) (name : string option) (var_ty : T.ety) : A.var
     =
   { A.index; name; var_ty }
 
 (** Small helper - TODO: move *)
-let mk_place_from_var_id (var_id : V.VarId.id) : E.place =
+let mk_place_from_var_id (var_id : E.VarId.id) : E.place =
   { var_id; projection = [] }
 
 (** Create a fresh symbolic value *)
@@ -124,7 +124,7 @@ type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs
 (** Generic borrow content: concrete or abstract *)
 type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs
 
-type abs_or_var_id = AbsId of V.AbstractionId.id | VarId of V.VarId.id option
+type abs_or_var_id = AbsId of V.AbstractionId.id | VarId of E.VarId.id option
 
 (** Utility exception *)
 exception FoundBorrowContent of V.borrow_content
diff --git a/compiler/LlbcAst.ml b/compiler/LlbcAst.ml
index 1b08f1ea..f4d26e18 100644
--- a/compiler/LlbcAst.ml
+++ b/compiler/LlbcAst.ml
@@ -1,46 +1,6 @@
-open Names
 open Types
 open Values
-open Expressions
-open Identifiers
-module FunDeclId = IdGen ()
-module GlobalDeclId = IdGen ()
-open Meta
-
-(** A variable, as used in a function definition *)
-type var = {
-  index : VarId.id;  (** Unique variable identifier *)
-  name : string option;
-  var_ty : ety;
-      (** The variable type - erased type, because variables are not used
-       ** in function signatures: they are only used to declare the list of
-       ** variables manipulated by a function body *)
-}
-[@@deriving show]
-
-type assumed_fun_id =
-  | Replace  (** [core::mem::replace] *)
-  | BoxNew
-  | BoxDeref  (** [core::ops::deref::Deref::<alloc::boxed::Box<T>>::deref] *)
-  | BoxDerefMut
-      (** [core::ops::deref::DerefMut::<alloc::boxed::Box<T>>::deref_mut] *)
-  | BoxFree
-  | VecNew
-  | VecPush
-  | VecInsert
-  | VecLen
-  | VecIndex  (** [core::ops::index::Index::index<alloc::vec::Vec<T>, usize>] *)
-  | VecIndexMut
-      (** [core::ops::index::IndexMut::index_mut<alloc::vec::Vec<T>, usize>] *)
-[@@deriving show, ord]
-
-type fun_id = Regular of FunDeclId.id | Assumed of assumed_fun_id
-[@@deriving show, ord]
-
-type global_assignment = { dst : VarId.id; global : GlobalDeclId.id }
-[@@deriving show]
-
-type assertion = { cond : operand; expected : bool } [@@deriving show]
+include Charon.LlbcAst
 
 type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group
 [@@deriving show]
@@ -48,17 +8,6 @@ type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group
 type abs_region_groups = (AbstractionId.id, RegionId.id) g_region_groups
 [@@deriving show]
 
-(** A function signature, as used when declaring functions *)
-type fun_sig = {
-  region_params : region_var list;
-  num_early_bound_regions : int;
-  regions_hierarchy : region_var_groups;
-  type_params : type_var list;
-  inputs : sty list;
-  output : sty;
-}
-[@@deriving show]
-
 (** A function signature, after instantiation *)
 type inst_fun_sig = {
   regions_hierarchy : abs_region_groups;
@@ -66,140 +15,3 @@ type inst_fun_sig = {
   output : rty;
 }
 [@@deriving show]
-
-type call = {
-  func : fun_id;
-  region_args : erased_region list;
-  type_args : ety list;
-  args : operand list;
-  dest : place;
-}
-[@@deriving show]
-
-(** Ancestor for [typed_value] iter visitor *)
-class ['self] iter_statement_base =
-  object (_self : 'self)
-    inherit [_] VisitorsRuntime.iter
-
-    method visit_global_assignment : 'env -> global_assignment -> unit =
-      fun _ _ -> ()
-
-    method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
-    method visit_place : 'env -> place -> unit = fun _ _ -> ()
-    method visit_rvalue : 'env -> rvalue -> unit = fun _ _ -> ()
-    method visit_id : 'env -> VariantId.id -> unit = fun _ _ -> ()
-    method visit_assertion : 'env -> assertion -> unit = fun _ _ -> ()
-    method visit_operand : 'env -> operand -> unit = fun _ _ -> ()
-    method visit_call : 'env -> call -> unit = fun _ _ -> ()
-    method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
-    method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> ()
-  end
-
-(** Ancestor for [typed_value] map visitor *)
-class ['self] map_statement_base =
-  object (_self : 'self)
-    inherit [_] VisitorsRuntime.map
-
-    method visit_global_assignment
-        : 'env -> global_assignment -> global_assignment =
-      fun _ x -> x
-
-    method visit_meta : 'env -> meta -> meta = fun _ x -> x
-    method visit_place : 'env -> place -> place = fun _ x -> x
-    method visit_rvalue : 'env -> rvalue -> rvalue = fun _ x -> x
-    method visit_id : 'env -> VariantId.id -> VariantId.id = fun _ x -> x
-    method visit_assertion : 'env -> assertion -> assertion = fun _ x -> x
-    method visit_operand : 'env -> operand -> operand = fun _ x -> x
-    method visit_call : 'env -> call -> call = fun _ x -> x
-
-    method visit_integer_type : 'env -> integer_type -> integer_type =
-      fun _ x -> x
-
-    method visit_scalar_value : 'env -> scalar_value -> scalar_value =
-      fun _ x -> x
-  end
-
-type statement = {
-  meta : meta;  (** The statement meta-data *)
-  content : raw_statement;  (** The statement itself *)
-}
-
-and raw_statement =
-  | Assign of place * rvalue
-  | AssignGlobal of global_assignment
-  | FakeRead of place
-  | SetDiscriminant of place * VariantId.id
-  | Drop of place
-  | Assert of assertion
-  | Call of call
-  | Panic
-  | Return
-  | Break of int
-      (** Break to (outer) loop. The [int] identifies the loop to break to:
-          * 0: break to the first outer loop (the current loop)
-          * 1: break to the second outer loop
-          * ...
-          *)
-  | Continue of int
-      (** Continue to (outer) loop. The loop identifier works
-          the same way as for {!Break} *)
-  | Nop
-  | Sequence of statement * statement
-  | Switch of operand * switch_targets
-  | Loop of statement
-
-and switch_targets =
-  | If of statement * statement  (** Gives the "if" and "else" blocks *)
-  | SwitchInt of integer_type * (scalar_value list * statement) list * statement
-      (** The targets for a switch over an integer are:
-          - the list [(matched values, statement to execute)]
-            We need a list for the matched values in case we do something like this:
-            [switch n { 0 | 1 => ..., _ => ... }]
-          - the "otherwise" statement
-          Also note that we precise the type of the integer (uint32, int64, etc.)
-          which we switch on. *)
-[@@deriving
-  show,
-    visitors
-      {
-        name = "iter_statement";
-        variety = "iter";
-        ancestors = [ "iter_statement_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      },
-    visitors
-      {
-        name = "map_statement";
-        variety = "map";
-        ancestors = [ "map_statement_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-      }]
-
-type fun_body = {
-  meta : meta;
-  arg_count : int;
-  locals : var list;
-  body : statement;
-}
-[@@deriving show]
-
-type fun_decl = {
-  def_id : FunDeclId.id;
-  meta : meta;
-  name : fun_name;
-  signature : fun_sig;
-  body : fun_body option;
-  is_global_decl_body : bool;
-}
-[@@deriving show]
-
-type global_decl = {
-  def_id : GlobalDeclId.id;
-  meta : meta;
-  body_id : FunDeclId.id;
-  name : global_name;
-  ty : ety;
-}
-[@@deriving show]
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index 46711d0a..1111c297 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -1,25 +1,5 @@
 open LlbcAst
-open Utils
-module T = Types
-
-(** Check if a {!type:LlbcAst.statement} contains loops *)
-let statement_has_loops (st : statement) : bool =
-  let obj =
-    object
-      inherit [_] iter_statement
-      method! visit_Loop _ _ = raise Found
-    end
-  in
-  try
-    obj#visit_statement () st;
-    false
-  with Found -> true
-
-(** Check if a {!type:LlbcAst.fun_decl} contains loops *)
-let fun_decl_has_loops (fd : fun_decl) : bool =
-  match fd.body with
-  | Some body -> statement_has_loops body.body
-  | None -> false
+include Charon.LlbcAstUtils
 
 let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
     fun_sig =
@@ -32,42 +12,3 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) :
   match fun_id with
   | Regular id -> (FunDeclId.Map.find id fun_decls).name
   | Assumed aid -> Assumed.get_assumed_name aid
-
-(** Small utility: list the transitive parents of a region var group.
-    We don't do that in an efficient manner, but it doesn't matter.
-    
-    TODO: rename to "list_ancestors_..."
-
-    This list *doesn't* include the current region.
- *)
-let rec list_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) :
-    T.RegionGroupId.Set.t =
-  let rg = T.RegionGroupId.nth sg.regions_hierarchy gid in
-  let parents =
-    List.fold_left
-      (fun s gid ->
-        (* Compute the parents *)
-        let parents = list_parent_region_groups sg gid in
-        (* Parents U current region *)
-        let parents = T.RegionGroupId.Set.add gid parents in
-        (* Make the union with the accumulator *)
-        T.RegionGroupId.Set.union s parents)
-      T.RegionGroupId.Set.empty rg.parents
-  in
-  parents
-
-(** Small utility: same as {!list_parent_region_groups}, but returns an ordered list.  *)
-let list_ordered_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id)
-    : T.RegionGroupId.id list =
-  let pset = list_parent_region_groups sg gid in
-  let parents =
-    List.filter
-      (fun (rg : T.region_var_group) -> T.RegionGroupId.Set.mem rg.id pset)
-      sg.regions_hierarchy
-  in
-  let parents = List.map (fun (rg : T.region_var_group) -> rg.id) parents in
-  parents
-
-let fun_body_get_input_vars (fbody : fun_body) : var list =
-  let locals = List.tl fbody.locals in
-  Collections.List.prefix fbody.arg_count locals
diff --git a/compiler/LlbcOfJson.ml b/compiler/LlbcOfJson.ml
index ad4cd5e4..dd8692a8 100644
--- a/compiler/LlbcOfJson.ml
+++ b/compiler/LlbcOfJson.ml
@@ -1,917 +1 @@
-(** Functions to load LLBC ASTs from json.
-
-    Initially, we used [ppx_derive_yojson] to automate this.
-    However, [ppx_derive_yojson] expects formatting to be slightly
-    different from what [serde_rs] generates (because it uses [Yojson.Safe.t]
-    and not [Yojson.Basic.t]).
-
-    TODO: we should check all that the integer values are in the proper range
- *)
-
-open Yojson.Basic
-open Names
-open OfJsonBasic
-open Identifiers
-open Meta
-module T = Types
-module PV = PrimitiveValues
-module V = Values
-module S = Scalars
-module E = Expressions
-module A = LlbcAst
-module TU = TypesUtils
-module AU = LlbcAstUtils
-module LocalFileId = IdGen ()
-module VirtualFileId = IdGen ()
-
-(** The default logger *)
-let log = Logging.llbc_of_json_logger
-
-(** A file identifier *)
-type file_id = LocalId of LocalFileId.id | VirtualId of VirtualFileId.id
-[@@deriving show, ord]
-
-module OrderedIdToFile : Collections.OrderedType with type t = file_id = struct
-  type t = file_id
-
-  let compare fid0 fid1 = compare_file_id fid0 fid1
-
-  let to_string id =
-    match id with
-    | LocalId id -> "Local " ^ LocalFileId.to_string id
-    | VirtualId id -> "Virtual " ^ VirtualFileId.to_string id
-
-  let pp_t fmt x = Format.pp_print_string fmt (to_string x)
-  let show_t x = to_string x
-end
-
-module IdToFile = Collections.MakeMap (OrderedIdToFile)
-
-type id_to_file_map = file_name IdToFile.t
-
-let file_id_of_json (js : json) : (file_id, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("LocalId", id) ] ->
-        let* id = LocalFileId.id_of_json id in
-        Ok (LocalId id)
-    | `Assoc [ ("VirtualId", id) ] ->
-        let* id = VirtualFileId.id_of_json id in
-        Ok (VirtualId id)
-    | _ -> Error "")
-
-let file_name_of_json (js : json) : (file_name, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("Virtual", name) ] ->
-        let* name = string_of_json name in
-        Ok (Virtual name)
-    | `Assoc [ ("Local", name) ] ->
-        let* name = string_of_json name in
-        Ok (Local name)
-    | _ -> Error "")
-
-(** Deserialize a map from file id to file name.
-
-    In the serialized LLBC, the files in the loc spans are refered to by their
-    ids, in order to save space. In a functional language like OCaml this is
-    not necessary: we thus replace the file ids by the file name themselves in
-    the AST.
-    The "id to file" map is thus only used in the deserialization process.
-  *)
-let id_to_file_of_json (js : json) : (id_to_file_map, string) result =
-  combine_error_msgs js __FUNCTION__
-    ((* The map is stored as a list of pairs (key, value): we deserialize
-      * this list then convert it to a map *)
-     let* key_values =
-       list_of_json (pair_of_json file_id_of_json file_name_of_json) js
-     in
-     Ok (IdToFile.of_list key_values))
-
-let loc_of_json (js : json) : (loc, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("line", line); ("col", col) ] ->
-        let* line = int_of_json line in
-        let* col = int_of_json col in
-        Ok { line; col }
-    | _ -> Error "")
-
-let span_of_json (id_to_file : id_to_file_map) (js : json) :
-    (span, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("file_id", file_id); ("beg", beg_loc); ("end", end_loc) ] ->
-        let* file_id = file_id_of_json file_id in
-        let file = IdToFile.find file_id id_to_file in
-        let* beg_loc = loc_of_json beg_loc in
-        let* end_loc = loc_of_json end_loc in
-        Ok { file; beg_loc; end_loc }
-    | _ -> Error "")
-
-let meta_of_json (id_to_file : id_to_file_map) (js : json) :
-    (meta, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("span", span); ("generated_from_span", generated_from_span) ] ->
-        let* span = span_of_json id_to_file span in
-        let* generated_from_span =
-          option_of_json (span_of_json id_to_file) generated_from_span
-        in
-        Ok { span; generated_from_span }
-    | _ -> Error "")
-
-let path_elem_of_json (js : json) : (path_elem, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("Ident", name) ] ->
-        let* name = string_of_json name in
-        Ok (Ident name)
-    | `Assoc [ ("Disambiguator", d) ] ->
-        let* d = Disambiguator.id_of_json d in
-        Ok (Disambiguator d)
-    | _ -> Error "")
-
-let name_of_json (js : json) : (name, string) result =
-  combine_error_msgs js __FUNCTION__ (list_of_json path_elem_of_json js)
-
-let fun_name_of_json (js : json) : (fun_name, string) result =
-  combine_error_msgs js __FUNCTION__ (name_of_json js)
-
-let type_var_of_json (js : json) : (T.type_var, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("index", index); ("name", name) ] ->
-        let* index = T.TypeVarId.id_of_json index in
-        let* name = string_of_json name in
-        Ok { T.index; name }
-    | _ -> Error "")
-
-let region_var_of_json (js : json) : (T.region_var, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("index", index); ("name", name) ] ->
-        let* index = T.RegionVarId.id_of_json index in
-        let* name = string_option_of_json name in
-        Ok { T.index; name }
-    | _ -> Error "")
-
-let region_of_json (js : json) : (T.RegionVarId.id T.region, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `String "Static" -> Ok T.Static
-    | `Assoc [ ("Var", rid) ] ->
-        let* rid = T.RegionVarId.id_of_json rid in
-        Ok (T.Var rid)
-    | _ -> Error "")
-
-let erased_region_of_json (js : json) : (T.erased_region, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with `String "Erased" -> Ok T.Erased | _ -> Error "")
-
-let integer_type_of_json (js : json) : (T.integer_type, string) result =
-  match js with
-  | `String "Isize" -> Ok T.Isize
-  | `String "I8" -> Ok T.I8
-  | `String "I16" -> Ok T.I16
-  | `String "I32" -> Ok T.I32
-  | `String "I64" -> Ok T.I64
-  | `String "I128" -> Ok T.I128
-  | `String "Usize" -> Ok T.Usize
-  | `String "U8" -> Ok T.U8
-  | `String "U16" -> Ok T.U16
-  | `String "U32" -> Ok T.U32
-  | `String "U64" -> Ok T.U64
-  | `String "U128" -> Ok T.U128
-  | _ -> Error ("integer_type_of_json failed on: " ^ show js)
-
-let ref_kind_of_json (js : json) : (T.ref_kind, string) result =
-  match js with
-  | `String "Mut" -> Ok T.Mut
-  | `String "Shared" -> Ok T.Shared
-  | _ -> Error ("ref_kind_of_json failed on: " ^ show js)
-
-let assumed_ty_of_json (js : json) : (T.assumed_ty, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `String "Box" -> Ok T.Box
-    | `String "Vec" -> Ok T.Vec
-    | `String "Option" -> Ok T.Option
-    | _ -> Error "")
-
-let type_id_of_json (js : json) : (T.type_id, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("Adt", id) ] ->
-        let* id = T.TypeDeclId.id_of_json id in
-        Ok (T.AdtId id)
-    | `String "Tuple" -> Ok T.Tuple
-    | `Assoc [ ("Assumed", aty) ] ->
-        let* aty = assumed_ty_of_json aty in
-        Ok (T.Assumed aty)
-    | _ -> Error "")
-
-let rec ty_of_json (r_of_json : json -> ('r, string) result) (js : json) :
-    ('r T.ty, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("Adt", `List [ id; regions; types ]) ] ->
-        let* id = type_id_of_json id in
-        let* regions = list_of_json r_of_json regions in
-        let* types = list_of_json (ty_of_json r_of_json) types in
-        (* Sanity check *)
-        (match id with T.Tuple -> assert (List.length regions = 0) | _ -> ());
-        Ok (T.Adt (id, regions, types))
-    | `Assoc [ ("TypeVar", `List [ id ]) ] ->
-        let* id = T.TypeVarId.id_of_json id in
-        Ok (T.TypeVar id)
-    | `String "Bool" -> Ok Bool
-    | `String "Char" -> Ok Char
-    | `String "`Never" -> Ok Never
-    | `Assoc [ ("Integer", `List [ int_ty ]) ] ->
-        let* int_ty = integer_type_of_json int_ty in
-        Ok (T.Integer int_ty)
-    | `String "Str" -> Ok Str
-    | `Assoc [ ("Array", `List [ ty ]) ] ->
-        let* ty = ty_of_json r_of_json ty in
-        Ok (T.Array ty)
-    | `Assoc [ ("Slice", `List [ ty ]) ] ->
-        let* ty = ty_of_json r_of_json ty in
-        Ok (T.Slice ty)
-    | `Assoc [ ("Ref", `List [ region; ty; ref_kind ]) ] ->
-        let* region = r_of_json region in
-        let* ty = ty_of_json r_of_json ty in
-        let* ref_kind = ref_kind_of_json ref_kind in
-        Ok (T.Ref (region, ty, ref_kind))
-    | _ -> Error "")
-
-let sty_of_json (js : json) : (T.sty, string) result =
-  combine_error_msgs js __FUNCTION__ (ty_of_json region_of_json js)
-
-let ety_of_json (js : json) : (T.ety, string) result =
-  combine_error_msgs js __FUNCTION__ (ty_of_json erased_region_of_json js)
-
-let field_of_json (id_to_file : id_to_file_map) (js : json) :
-    (T.field, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("meta", meta); ("name", name); ("ty", ty) ] ->
-        let* meta = meta_of_json id_to_file meta in
-        let* name = option_of_json string_of_json name in
-        let* ty = sty_of_json ty in
-        Ok { T.meta; field_name = name; field_ty = ty }
-    | _ -> Error "")
-
-let variant_of_json (id_to_file : id_to_file_map) (js : json) :
-    (T.variant, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("meta", meta); ("name", name); ("fields", fields) ] ->
-        let* meta = meta_of_json id_to_file meta in
-        let* name = string_of_json name in
-        let* fields = list_of_json (field_of_json id_to_file) fields in
-        Ok { T.meta; variant_name = name; fields }
-    | _ -> Error "")
-
-let type_decl_kind_of_json (id_to_file : id_to_file_map) (js : json) :
-    (T.type_decl_kind, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("Struct", fields) ] ->
-        let* fields = list_of_json (field_of_json id_to_file) fields in
-        Ok (T.Struct fields)
-    | `Assoc [ ("Enum", variants) ] ->
-        let* variants = list_of_json (variant_of_json id_to_file) variants in
-        Ok (T.Enum variants)
-    | `String "Opaque" -> Ok T.Opaque
-    | _ -> Error "")
-
-let region_var_group_of_json (js : json) : (T.region_var_group, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("id", id); ("regions", regions); ("parents", parents) ] ->
-        let* id = T.RegionGroupId.id_of_json id in
-        let* regions = list_of_json T.RegionVarId.id_of_json regions in
-        let* parents = list_of_json T.RegionGroupId.id_of_json parents in
-        Ok { T.id; regions; parents }
-    | _ -> Error "")
-
-let region_var_groups_of_json (js : json) : (T.region_var_groups, string) result
-    =
-  combine_error_msgs js __FUNCTION__ (list_of_json region_var_group_of_json js)
-
-let type_decl_of_json (id_to_file : id_to_file_map) (js : json) :
-    (T.type_decl, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc
-        [
-          ("def_id", def_id);
-          ("meta", meta);
-          ("name", name);
-          ("region_params", region_params);
-          ("type_params", type_params);
-          ("regions_hierarchy", regions_hierarchy);
-          ("kind", kind);
-        ] ->
-        let* def_id = T.TypeDeclId.id_of_json def_id in
-        let* meta = meta_of_json id_to_file meta in
-        let* name = name_of_json name in
-        let* region_params = list_of_json region_var_of_json region_params in
-        let* type_params = list_of_json type_var_of_json type_params in
-        let* kind = type_decl_kind_of_json id_to_file kind in
-        let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in
-        Ok
-          {
-            T.def_id;
-            meta;
-            name;
-            region_params;
-            type_params;
-            kind;
-            regions_hierarchy;
-          }
-    | _ -> Error "")
-
-let var_of_json (js : json) : (A.var, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("index", index); ("name", name); ("ty", ty) ] ->
-        let* index = V.VarId.id_of_json index in
-        let* name = string_option_of_json name in
-        let* var_ty = ety_of_json ty in
-        Ok { A.index; name; var_ty }
-    | _ -> Error "")
-
-let big_int_of_json (js : json) : (V.big_int, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Int i -> Ok (Z.of_int i)
-    | `String is -> Ok (Z.of_string is)
-    | _ -> Error "")
-
-(** Deserialize a {!V.scalar_value} from JSON and **check the ranges**.
-    
-    Note that in practice we also check that the values are in range
-    in the interpreter functions. Still, it doesn't cost much to be
-    a bit conservative.
- *)
-let scalar_value_of_json (js : json) : (V.scalar_value, string) result =
-  let res =
-    combine_error_msgs js __FUNCTION__
-      (match js with
-      | `Assoc [ ("Isize", `List [ bi ]) ] ->
-          let* bi = big_int_of_json bi in
-          Ok { PV.value = bi; int_ty = Isize }
-      | `Assoc [ ("I8", `List [ bi ]) ] ->
-          let* bi = big_int_of_json bi in
-          Ok { PV.value = bi; int_ty = I8 }
-      | `Assoc [ ("I16", `List [ bi ]) ] ->
-          let* bi = big_int_of_json bi in
-          Ok { PV.value = bi; int_ty = I16 }
-      | `Assoc [ ("I32", `List [ bi ]) ] ->
-          let* bi = big_int_of_json bi in
-          Ok { PV.value = bi; int_ty = I32 }
-      | `Assoc [ ("I64", `List [ bi ]) ] ->
-          let* bi = big_int_of_json bi in
-          Ok { PV.value = bi; int_ty = I64 }
-      | `Assoc [ ("I128", `List [ bi ]) ] ->
-          let* bi = big_int_of_json bi in
-          Ok { PV.value = bi; int_ty = I128 }
-      | `Assoc [ ("Usize", `List [ bi ]) ] ->
-          let* bi = big_int_of_json bi in
-          Ok { PV.value = bi; int_ty = Usize }
-      | `Assoc [ ("U8", `List [ bi ]) ] ->
-          let* bi = big_int_of_json bi in
-          Ok { PV.value = bi; int_ty = U8 }
-      | `Assoc [ ("U16", `List [ bi ]) ] ->
-          let* bi = big_int_of_json bi in
-          Ok { PV.value = bi; int_ty = U16 }
-      | `Assoc [ ("U32", `List [ bi ]) ] ->
-          let* bi = big_int_of_json bi in
-          Ok { PV.value = bi; int_ty = U32 }
-      | `Assoc [ ("U64", `List [ bi ]) ] ->
-          let* bi = big_int_of_json bi in
-          Ok { PV.value = bi; int_ty = U64 }
-      | `Assoc [ ("U128", `List [ bi ]) ] ->
-          let* bi = big_int_of_json bi in
-          Ok { PV.value = bi; int_ty = U128 }
-      | _ -> Error "")
-  in
-  match res with
-  | Error _ -> res
-  | Ok sv ->
-      if not (S.check_scalar_value_in_range sv) then (
-        log#serror ("Scalar value not in range: " ^ PV.show_scalar_value sv);
-        raise
-          (Failure ("Scalar value not in range: " ^ PV.show_scalar_value sv)));
-      res
-
-let field_proj_kind_of_json (js : json) : (E.field_proj_kind, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("ProjAdt", `List [ def_id; opt_variant_id ]) ] ->
-        let* def_id = T.TypeDeclId.id_of_json def_id in
-        let* opt_variant_id =
-          option_of_json T.VariantId.id_of_json opt_variant_id
-        in
-        Ok (E.ProjAdt (def_id, opt_variant_id))
-    | `Assoc [ ("ProjTuple", i) ] ->
-        let* i = int_of_json i in
-        Ok (E.ProjTuple i)
-    | `Assoc [ ("ProjOption", variant_id) ] ->
-        let* variant_id = T.VariantId.id_of_json variant_id in
-        Ok (E.ProjOption variant_id)
-    | _ -> Error "")
-
-let projection_elem_of_json (js : json) : (E.projection_elem, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `String "Deref" -> Ok E.Deref
-    | `String "DerefBox" -> Ok E.DerefBox
-    | `Assoc [ ("Field", `List [ proj_kind; field_id ]) ] ->
-        let* proj_kind = field_proj_kind_of_json proj_kind in
-        let* field_id = T.FieldId.id_of_json field_id in
-        Ok (E.Field (proj_kind, field_id))
-    | _ -> Error ("projection_elem_of_json failed on:" ^ show js))
-
-let projection_of_json (js : json) : (E.projection, string) result =
-  combine_error_msgs js __FUNCTION__ (list_of_json projection_elem_of_json js)
-
-let place_of_json (js : json) : (E.place, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("var_id", var_id); ("projection", projection) ] ->
-        let* var_id = V.VarId.id_of_json var_id in
-        let* projection = projection_of_json projection in
-        Ok { E.var_id; projection }
-    | _ -> Error "")
-
-let borrow_kind_of_json (js : json) : (E.borrow_kind, string) result =
-  match js with
-  | `String "Shared" -> Ok E.Shared
-  | `String "Mut" -> Ok E.Mut
-  | `String "TwoPhaseMut" -> Ok E.TwoPhaseMut
-  | _ -> Error ("borrow_kind_of_json failed on:" ^ show js)
-
-let unop_of_json (js : json) : (E.unop, string) result =
-  match js with
-  | `String "Not" -> Ok E.Not
-  | `String "Neg" -> Ok E.Neg
-  | `Assoc [ ("Cast", `List [ src_ty; tgt_ty ]) ] ->
-      let* src_ty = integer_type_of_json src_ty in
-      let* tgt_ty = integer_type_of_json tgt_ty in
-      Ok (E.Cast (src_ty, tgt_ty))
-  | _ -> Error ("unop_of_json failed on:" ^ show js)
-
-let binop_of_json (js : json) : (E.binop, string) result =
-  match js with
-  | `String "BitXor" -> Ok E.BitXor
-  | `String "BitAnd" -> Ok E.BitAnd
-  | `String "BitOr" -> Ok E.BitOr
-  | `String "Eq" -> Ok E.Eq
-  | `String "Lt" -> Ok E.Lt
-  | `String "Le" -> Ok E.Le
-  | `String "Ne" -> Ok E.Ne
-  | `String "Ge" -> Ok E.Ge
-  | `String "Gt" -> Ok E.Gt
-  | `String "Div" -> Ok E.Div
-  | `String "Rem" -> Ok E.Rem
-  | `String "Add" -> Ok E.Add
-  | `String "Sub" -> Ok E.Sub
-  | `String "Mul" -> Ok E.Mul
-  | `String "Shl" -> Ok E.Shl
-  | `String "Shr" -> Ok E.Shr
-  | _ -> Error ("binop_of_json failed on:" ^ show js)
-
-let primitive_value_of_json (js : json) : (V.primitive_value, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("Scalar", scalar_value) ] ->
-        let* scalar_value = scalar_value_of_json scalar_value in
-        Ok (PV.Scalar scalar_value)
-    | `Assoc [ ("Bool", v) ] ->
-        let* v = bool_of_json v in
-        Ok (PV.Bool v)
-    | `Assoc [ ("Char", v) ] ->
-        let* v = char_of_json v in
-        Ok (PV.Char v)
-    | `Assoc [ ("String", v) ] ->
-        let* v = string_of_json v in
-        Ok (PV.String v)
-    | _ -> Error "")
-
-let operand_of_json (js : json) : (E.operand, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("Copy", place) ] ->
-        let* place = place_of_json place in
-        Ok (E.Copy place)
-    | `Assoc [ ("Move", place) ] ->
-        let* place = place_of_json place in
-        Ok (E.Move place)
-    | `Assoc [ ("Const", `List [ ty; cv ]) ] ->
-        let* ty = ety_of_json ty in
-        let* cv = primitive_value_of_json cv in
-        Ok (E.Constant (ty, cv))
-    | _ -> Error "")
-
-let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `String "AggregatedTuple" -> Ok E.AggregatedTuple
-    | `Assoc [ ("AggregatedOption", `List [ variant_id; ty ]) ] ->
-        let* variant_id = T.VariantId.id_of_json variant_id in
-        let* ty = ety_of_json ty in
-        Ok (E.AggregatedOption (variant_id, ty))
-    | `Assoc [ ("AggregatedAdt", `List [ id; opt_variant_id; regions; tys ]) ]
-      ->
-        let* id = T.TypeDeclId.id_of_json id in
-        let* opt_variant_id =
-          option_of_json T.VariantId.id_of_json opt_variant_id
-        in
-        let* regions = list_of_json erased_region_of_json regions in
-        let* tys = list_of_json ety_of_json tys in
-        Ok (E.AggregatedAdt (id, opt_variant_id, regions, tys))
-    | _ -> Error "")
-
-let rvalue_of_json (js : json) : (E.rvalue, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("Use", op) ] ->
-        let* op = operand_of_json op in
-        Ok (E.Use op)
-    | `Assoc [ ("Ref", `List [ place; borrow_kind ]) ] ->
-        let* place = place_of_json place in
-        let* borrow_kind = borrow_kind_of_json borrow_kind in
-        Ok (E.Ref (place, borrow_kind))
-    | `Assoc [ ("UnaryOp", `List [ unop; op ]) ] ->
-        let* unop = unop_of_json unop in
-        let* op = operand_of_json op in
-        Ok (E.UnaryOp (unop, op))
-    | `Assoc [ ("BinaryOp", `List [ binop; op1; op2 ]) ] ->
-        let* binop = binop_of_json binop in
-        let* op1 = operand_of_json op1 in
-        let* op2 = operand_of_json op2 in
-        Ok (E.BinaryOp (binop, op1, op2))
-    | `Assoc [ ("Discriminant", place) ] ->
-        let* place = place_of_json place in
-        Ok (E.Discriminant place)
-    | `Assoc [ ("Aggregate", `List [ aggregate_kind; ops ]) ] ->
-        let* aggregate_kind = aggregate_kind_of_json aggregate_kind in
-        let* ops = list_of_json operand_of_json ops in
-        Ok (E.Aggregate (aggregate_kind, ops))
-    | _ -> Error "")
-
-let assumed_fun_id_of_json (js : json) : (A.assumed_fun_id, string) result =
-  match js with
-  | `String "Replace" -> Ok A.Replace
-  | `String "BoxNew" -> Ok A.BoxNew
-  | `String "BoxDeref" -> Ok A.BoxDeref
-  | `String "BoxDerefMut" -> Ok A.BoxDerefMut
-  | `String "BoxFree" -> Ok A.BoxFree
-  | `String "VecNew" -> Ok A.VecNew
-  | `String "VecPush" -> Ok A.VecPush
-  | `String "VecInsert" -> Ok A.VecInsert
-  | `String "VecLen" -> Ok A.VecLen
-  | `String "VecIndex" -> Ok A.VecIndex
-  | `String "VecIndexMut" -> Ok A.VecIndexMut
-  | _ -> Error ("assumed_fun_id_of_json failed on:" ^ show js)
-
-let fun_id_of_json (js : json) : (A.fun_id, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("Regular", id) ] ->
-        let* id = A.FunDeclId.id_of_json id in
-        Ok (A.Regular id)
-    | `Assoc [ ("Assumed", fid) ] ->
-        let* fid = assumed_fun_id_of_json fid in
-        Ok (A.Assumed fid)
-    | _ -> Error "")
-
-let assertion_of_json (js : json) : (A.assertion, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("cond", cond); ("expected", expected) ] ->
-        let* cond = operand_of_json cond in
-        let* expected = bool_of_json expected in
-        Ok { A.cond; expected }
-    | _ -> Error "")
-
-let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc
-        [
-          ("region_params", region_params);
-          ("num_early_bound_regions", num_early_bound_regions);
-          ("regions_hierarchy", regions_hierarchy);
-          ("type_params", type_params);
-          ("inputs", inputs);
-          ("output", output);
-        ] ->
-        let* region_params = list_of_json region_var_of_json region_params in
-        let* num_early_bound_regions = int_of_json num_early_bound_regions in
-        let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in
-        let* type_params = list_of_json type_var_of_json type_params in
-        let* inputs = list_of_json sty_of_json inputs in
-        let* output = sty_of_json output in
-        Ok
-          {
-            A.region_params;
-            num_early_bound_regions;
-            regions_hierarchy;
-            type_params;
-            inputs;
-            output;
-          }
-    | _ -> Error "")
-
-let call_of_json (js : json) : (A.call, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc
-        [
-          ("func", func);
-          ("region_args", region_args);
-          ("type_args", type_args);
-          ("args", args);
-          ("dest", dest);
-        ] ->
-        let* func = fun_id_of_json func in
-        let* region_args = list_of_json erased_region_of_json region_args in
-        let* type_args = list_of_json ety_of_json type_args in
-        let* args = list_of_json operand_of_json args in
-        let* dest = place_of_json dest in
-        Ok { A.func; region_args; type_args; args; dest }
-    | _ -> Error "")
-
-let rec statement_of_json (id_to_file : id_to_file_map) (js : json) :
-    (A.statement, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("meta", meta); ("content", content) ] ->
-        let* meta = meta_of_json id_to_file meta in
-        let* content = raw_statement_of_json id_to_file content in
-        Ok { A.meta; content }
-    | _ -> Error "")
-
-and raw_statement_of_json (id_to_file : id_to_file_map) (js : json) :
-    (A.raw_statement, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("Assign", `List [ place; rvalue ]) ] ->
-        let* place = place_of_json place in
-        let* rvalue = rvalue_of_json rvalue in
-        Ok (A.Assign (place, rvalue))
-    | `Assoc [ ("AssignGlobal", `List [ dst; global ]) ] ->
-        let* dst = V.VarId.id_of_json dst in
-        let* global = A.GlobalDeclId.id_of_json global in
-        Ok (A.AssignGlobal { dst; global })
-    | `Assoc [ ("FakeRead", place) ] ->
-        let* place = place_of_json place in
-        Ok (A.FakeRead place)
-    | `Assoc [ ("SetDiscriminant", `List [ place; variant_id ]) ] ->
-        let* place = place_of_json place in
-        let* variant_id = T.VariantId.id_of_json variant_id in
-        Ok (A.SetDiscriminant (place, variant_id))
-    | `Assoc [ ("Drop", place) ] ->
-        let* place = place_of_json place in
-        Ok (A.Drop place)
-    | `Assoc [ ("Assert", assertion) ] ->
-        let* assertion = assertion_of_json assertion in
-        Ok (A.Assert assertion)
-    | `Assoc [ ("Call", call) ] ->
-        let* call = call_of_json call in
-        Ok (A.Call call)
-    | `String "Panic" -> Ok A.Panic
-    | `String "Return" -> Ok A.Return
-    | `Assoc [ ("Break", i) ] ->
-        let* i = int_of_json i in
-        Ok (A.Break i)
-    | `Assoc [ ("Continue", i) ] ->
-        let* i = int_of_json i in
-        Ok (A.Continue i)
-    | `String "Nop" -> Ok A.Nop
-    | `Assoc [ ("Sequence", `List [ st1; st2 ]) ] ->
-        let* st1 = statement_of_json id_to_file st1 in
-        let* st2 = statement_of_json id_to_file st2 in
-        Ok (A.Sequence (st1, st2))
-    | `Assoc [ ("Switch", `List [ op; tgt ]) ] ->
-        let* op = operand_of_json op in
-        let* tgt = switch_targets_of_json id_to_file tgt in
-        Ok (A.Switch (op, tgt))
-    | `Assoc [ ("Loop", st) ] ->
-        let* st = statement_of_json id_to_file st in
-        Ok (A.Loop st)
-    | _ -> Error "")
-
-and switch_targets_of_json (id_to_file : id_to_file_map) (js : json) :
-    (A.switch_targets, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("If", `List [ st1; st2 ]) ] ->
-        let* st1 = statement_of_json id_to_file st1 in
-        let* st2 = statement_of_json id_to_file st2 in
-        Ok (A.If (st1, st2))
-    | `Assoc [ ("SwitchInt", `List [ int_ty; tgts; otherwise ]) ] ->
-        let* int_ty = integer_type_of_json int_ty in
-        let* tgts =
-          list_of_json
-            (pair_of_json
-               (list_of_json scalar_value_of_json)
-               (statement_of_json id_to_file))
-            tgts
-        in
-        let* otherwise = statement_of_json id_to_file otherwise in
-        Ok (A.SwitchInt (int_ty, tgts, otherwise))
-    | _ -> Error "")
-
-let fun_body_of_json (id_to_file : id_to_file_map) (js : json) :
-    (A.fun_body, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc
-        [
-          ("meta", meta);
-          ("arg_count", arg_count);
-          ("locals", locals);
-          ("body", body);
-        ] ->
-        let* meta = meta_of_json id_to_file meta in
-        let* arg_count = int_of_json arg_count in
-        let* locals = list_of_json var_of_json locals in
-        let* body = statement_of_json id_to_file body in
-        Ok { A.meta; arg_count; locals; body }
-    | _ -> Error "")
-
-let fun_decl_of_json (id_to_file : id_to_file_map) (js : json) :
-    (A.fun_decl, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc
-        [
-          ("def_id", def_id);
-          ("meta", meta);
-          ("name", name);
-          ("signature", signature);
-          ("body", body);
-        ] ->
-        let* def_id = A.FunDeclId.id_of_json def_id in
-        let* meta = meta_of_json id_to_file meta in
-        let* name = fun_name_of_json name in
-        let* signature = fun_sig_of_json signature in
-        let* body = option_of_json (fun_body_of_json id_to_file) body in
-        Ok
-          { A.def_id; meta; name; signature; body; is_global_decl_body = false }
-    | _ -> Error "")
-
-(* Strict type for the number of function declarations (see {!global_to_fun_id} below) *)
-type global_id_converter = { fun_count : int } [@@deriving show]
-
-(** Converts a global id to its corresponding function id.
-    To do so, it adds the global id to the number of function declarations :
-    We have the bijection [global_fun_id <=> global_id + fun_id_count].
-*)
-let global_to_fun_id (conv : global_id_converter) (gid : A.GlobalDeclId.id) :
-    A.FunDeclId.id =
-  A.FunDeclId.of_int (A.GlobalDeclId.to_int gid + conv.fun_count)
-
-(* Converts a global declaration to a function declaration.
- *)
-let global_decl_of_json (id_to_file : id_to_file_map) (js : json)
-    (gid_conv : global_id_converter) :
-    (A.global_decl * A.fun_decl, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc
-        [
-          ("def_id", def_id);
-          ("meta", meta);
-          ("name", name);
-          ("ty", ty);
-          ("body", body);
-        ] ->
-        let* global_id = A.GlobalDeclId.id_of_json def_id in
-        let fun_id = global_to_fun_id gid_conv global_id in
-        let* meta = meta_of_json id_to_file meta in
-        let* name = fun_name_of_json name in
-        let* ty = ety_of_json ty in
-        let* body = option_of_json (fun_body_of_json id_to_file) body in
-        let signature : A.fun_sig =
-          {
-            region_params = [];
-            num_early_bound_regions = 0;
-            regions_hierarchy = [];
-            type_params = [];
-            inputs = [];
-            output = TU.ety_no_regions_to_sty ty;
-          }
-        in
-        Ok
-          ( { A.def_id = global_id; meta; body_id = fun_id; name; ty },
-            {
-              A.def_id = fun_id;
-              meta;
-              name;
-              signature;
-              body;
-              is_global_decl_body = true;
-            } )
-    | _ -> Error "")
-
-let g_declaration_group_of_json (id_of_json : json -> ('id, string) result)
-    (js : json) : ('id Crates.g_declaration_group, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("NonRec", `List [ id ]) ] ->
-        let* id = id_of_json id in
-        Ok (Crates.NonRec id)
-    | `Assoc [ ("Rec", `List [ ids ]) ] ->
-        let* ids = list_of_json id_of_json ids in
-        Ok (Crates.Rec ids)
-    | _ -> Error "")
-
-let type_declaration_group_of_json (js : json) :
-    (Crates.type_declaration_group, string) result =
-  combine_error_msgs js __FUNCTION__
-    (g_declaration_group_of_json T.TypeDeclId.id_of_json js)
-
-let fun_declaration_group_of_json (js : json) :
-    (Crates.fun_declaration_group, string) result =
-  combine_error_msgs js __FUNCTION__
-    (g_declaration_group_of_json A.FunDeclId.id_of_json js)
-
-let global_declaration_group_of_json (js : json) :
-    (A.GlobalDeclId.id, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("NonRec", `List [ id ]) ] ->
-        let* id = A.GlobalDeclId.id_of_json id in
-        Ok id
-    | `Assoc [ ("Rec", `List [ _ ]) ] -> Error "got mutually dependent globals"
-    | _ -> Error "")
-
-let declaration_group_of_json (js : json) :
-    (Crates.declaration_group, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc [ ("Type", `List [ decl ]) ] ->
-        let* decl = type_declaration_group_of_json decl in
-        Ok (Crates.Type decl)
-    | `Assoc [ ("Fun", `List [ decl ]) ] ->
-        let* decl = fun_declaration_group_of_json decl in
-        Ok (Crates.Fun decl)
-    | `Assoc [ ("Global", `List [ decl ]) ] ->
-        let* id = global_declaration_group_of_json decl in
-        Ok (Crates.Global id)
-    | _ -> Error "")
-
-let length_of_json_list (js : json) : (int, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `List jsl -> Ok (List.length jsl)
-    | _ -> Error ("not a list: " ^ show js))
-
-let llbc_crate_of_json (js : json) : (Crates.llbc_crate, string) result =
-  combine_error_msgs js __FUNCTION__
-    (match js with
-    | `Assoc
-        [
-          ("name", name);
-          ("id_to_file", id_to_file);
-          ("declarations", declarations);
-          ("types", types);
-          ("functions", functions);
-          ("globals", globals);
-        ] ->
-        (* We first deserialize the declaration groups (which simply contain ids)
-         * and all the declarations *butù* the globals *)
-        let* name = string_of_json name in
-        let* id_to_file = id_to_file_of_json id_to_file in
-        let* declarations =
-          list_of_json declaration_group_of_json declarations
-        in
-        let* types = list_of_json (type_decl_of_json id_to_file) types in
-        let* functions = list_of_json (fun_decl_of_json id_to_file) functions in
-        (* When deserializing the globals, we split the global declarations
-         * between the globals themselves and their bodies, which are simply
-         * functions with no arguments. We add the global bodies to the list
-         * of function declarations: the (fresh) ids we use for those bodies
-         * are simply given by: [num_functions + global_id] *)
-        let gid_conv = { fun_count = List.length functions } in
-        let* globals =
-          list_of_json
-            (fun js -> global_decl_of_json id_to_file js gid_conv)
-            globals
-        in
-        let globals, global_bodies = List.split globals in
-        Ok
-          {
-            Crates.name;
-            declarations;
-            types;
-            functions = functions @ global_bodies;
-            globals;
-          }
-    | _ -> Error "")
+include Charon.LlbcOfJson
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index e83f25f8..7b95f41d 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -1,17 +1,8 @@
-module H = Easy_logging.Handlers
-module L = Easy_logging.Logging
-
-let _ = L.make_logger "MainLogger" Debug [ Cli Debug ]
-
-(** The main logger *)
-let main_log = L.get_logger "MainLogger"
+include Charon.Logging
 
 (** Below, we create subgloggers for various submodules, so that we can precisely
     toggle logging on/off, depending on which information we need *)
 
-(** Logger for LlbcOfJson *)
-let llbc_of_json_logger = L.get_logger "MainLogger.LlbcOfJson"
-
 (** Logger for PrePasses *)
 let pre_passes_log = L.get_logger "MainLogger.PrePasses"
 
@@ -50,130 +41,3 @@ let borrows_log = L.get_logger "MainLogger.Interpreter.Borrows"
 
 (** Logger for Invariants *)
 let invariants_log = L.get_logger "MainLogger.Interpreter.Invariants"
-
-(** Terminal colors - TODO: comes from easy_logging (did not manage to reuse the module directly) *)
-type color =
-  | Default
-  | Black
-  | Red
-  | Green
-  | Yellow
-  | Blue
-  | Magenta
-  | Cyan
-  | Gray
-  | White
-  | LRed
-  | LGreen
-  | LYellow
-  | LBlue
-  | LMagenta
-  | LCyan
-  | LGray
-
-(** Terminal styles - TODO: comes from easy_logging (did not manage to reuse the module directly) *)
-type format = Bold | Underline | Invert | Fg of color | Bg of color
-
-(** TODO: comes from easy_logging (did not manage to reuse the module directly) *)
-let to_fg_code c =
-  match c with
-  | Default -> 39
-  | Black -> 30
-  | Red -> 31
-  | Green -> 32
-  | Yellow -> 33
-  | Blue -> 34
-  | Magenta -> 35
-  | Cyan -> 36
-  | Gray -> 90
-  | White -> 97
-  | LRed -> 91
-  | LGreen -> 92
-  | LYellow -> 93
-  | LBlue -> 94
-  | LMagenta -> 95
-  | LCyan -> 96
-  | LGray -> 37
-
-(** TODO: comes from easy_logging (did not manage to reuse the module directly) *)
-let to_bg_code c =
-  match c with
-  | Default -> 49
-  | Black -> 40
-  | Red -> 41
-  | Green -> 42
-  | Yellow -> 43
-  | Blue -> 44
-  | Magenta -> 45
-  | Cyan -> 46
-  | Gray -> 100
-  | White -> 107
-  | LRed -> 101
-  | LGreen -> 102
-  | LYellow -> 103
-  | LBlue -> 104
-  | LMagenta -> 105
-  | LCyan -> 106
-  | LGray -> 47
-
-(** TODO: comes from easy_logging (did not manage to reuse the module directly) *)
-let style_to_codes s =
-  match s with
-  | Bold -> (1, 21)
-  | Underline -> (4, 24)
-  | Invert -> (7, 27)
-  | Fg c -> (to_fg_code c, to_fg_code Default)
-  | Bg c -> (to_bg_code c, to_bg_code Default)
-
-(** TODO: comes from easy_logging (did not manage to reuse the module directly)
-    I made a minor modifications, though. *)
-let level_to_color (lvl : L.level) =
-  match lvl with
-  | L.Flash -> LMagenta
-  | Error -> LRed
-  | Warning -> LYellow
-  | Info -> LGreen
-  | Trace -> Cyan
-  | Debug -> LBlue
-  | NoLevel -> Default
-
-(** [format styles str] formats [str] to the given [styles] -
-    TODO: comes from {{: http://ocamlverse.net/content/documentation_guidelines.html}[easy_logging]}
-    (did not manage to reuse the module directly)
-*)
-let rec format styles str =
-  match styles with
-  | (_ as s) :: styles' ->
-      let set, reset = style_to_codes s in
-      Printf.sprintf "\027[%dm%s\027[%dm" set (format styles' str) reset
-  | [] -> str
-
-(** TODO: comes from {{: http://ocamlverse.net/content/documentation_guidelines.html}[easy_logging]}
-    (did not manage to reuse the module directly) *)
-let format_tags (tags : string list) =
-  match tags with
-  | [] -> ""
-  | _ ->
-      let elems_str = String.concat " | " tags in
-      "[" ^ elems_str ^ "] "
-
-(* Change the formatters *)
-let main_logger_handler =
-  (* TODO: comes from easy_logging *)
-  let formatter (item : L.log_item) : string =
-    let item_level_fmt =
-      format [ Fg (level_to_color item.level) ] (L.show_level item.level)
-    and item_msg_fmt =
-      match item.level with
-      | Flash -> format [ Fg Black; Bg LMagenta ] item.msg
-      | _ -> item.msg
-    in
-
-    Format.pp_set_max_indent Format.str_formatter 200;
-    Format.sprintf "@[[%-15s] %s%s@]" item_level_fmt (format_tags item.tags)
-      item_msg_fmt
-  in
-  (* There should be exactly one handler *)
-  let handlers = main_log#get_handlers in
-  List.iter (fun h -> H.set_formatter h formatter) handlers;
-  match handlers with [ handler ] -> handler | _ -> failwith "Unexpected"
diff --git a/compiler/Meta.ml b/compiler/Meta.ml
index f0e4ca04..b8a3d1e0 100644
--- a/compiler/Meta.ml
+++ b/compiler/Meta.ml
@@ -1,44 +1 @@
-(** Meta data like code spans *)
-
-(** A line location *)
-type loc = {
-  line : int;  (** The (1-based) line number. *)
-  col : int;  (** The (0-based) column offset. *)
-}
-[@@deriving show]
-
-type file_name =
-  | Virtual of string  (** A remapped path (namely paths into stdlib) *)
-  | Local of string
-      (** A local path (a file coming from the current crate for instance) *)
-[@@deriving show]
-
-(** Span data *)
-type span = { file : file_name; beg_loc : loc; end_loc : loc } [@@deriving show]
-
-type meta = {
-  span : span;
-      (** The source code span.
-
-          If this meta information is for a statement/terminator coming from a macro
-          expansion/inlining/etc., this span is (in case of macros) for the macro
-          before expansion (i.e., the location the code where the user wrote the call
-          to the macro).
-
-          Ex:
-          {[
-            // Below, we consider the spans for the statements inside `test`
-
-            //   the statement we consider, which gets inlined in `test`
-                                     VV
-            macro_rules! macro { ... st ... } // `generated_from_span` refers to this location
-
-            fn test() {
-                macro!(); // <-- `span` refers to this location
-            }
-          ]}
-       *)
-  generated_from_span : span option;
-      (** Where the code actually comes from, in case of macro expansion/inlining/etc. *)
-}
-[@@deriving show]
+include Charon.Meta
diff --git a/compiler/Names.ml b/compiler/Names.ml
index a27db161..97dbc180 100644
--- a/compiler/Names.ml
+++ b/compiler/Names.ml
@@ -1,80 +1 @@
-open Identifiers
-module Disambiguator = IdGen ()
-
-(** See the comments for [Name] *)
-type path_elem = Ident of string | Disambiguator of Disambiguator.id
-[@@deriving show, ord]
-
-(** A name such as: [std::collections::vector] (which would be represented as
-    [[Ident "std"; Ident "collections"; Ident "vector"]])
-
-
-    A name really is a list of strings. However, we sometimes need to
-    introduce unique indices to disambiguate. This mostly happens because
-    of "impl" blocks in Rust:
-    {[
-      impl<T> List<T> {
-        ...
-      }
-    ]}
-   
-    A type in Rust can have several "impl" blocks, and those blocks can
-    contain items with similar names. For this reason, we need to disambiguate
-    them with unique indices. Rustc calls those "disambiguators". In rustc, this
-    gives names like this:
-    - [betree_main::betree::NodeIdCounter{impl#0}::new]
-    - note that impl blocks can be nested, and macros sometimes generate
-      weird names (which require disambiguation):
-      [betree_main::betree_utils::_#1::{impl#0}::deserialize::{impl#0}]
-   
-    Finally, the paths used by rustc are a lot more precise and explicit than
-    those we expose in LLBC: for instance, every identifier belongs to a specific
-    namespace (value namespace, type namespace, etc.), and is coupled with a
-    disambiguator.
-   
-    On our side, we want to stay high-level and simple: we use string identifiers
-    as much as possible, insert disambiguators only when necessary (whenever
-    we find an "impl" block, typically) and check that the disambiguator is useless
-    in the other situations (i.e., the disambiguator is always equal to 0).
-   
-    Moreover, the items are uniquely disambiguated by their (integer) ids
-    ([TypeDeclId.id], etc.), and when extracting the code we have to deal with
-    name clashes anyway. Still, we might want to be more precise in the future.
-   
-    Also note that the first path element in the name is always the crate name.
- *)
-type name = path_elem list [@@deriving show, ord]
-
-let to_name (ls : string list) : name = List.map (fun s -> Ident s) ls
-
-type module_name = name [@@deriving show, ord]
-type type_name = name [@@deriving show, ord]
-type fun_name = name [@@deriving show, ord]
-type global_name = name [@@deriving show, ord]
-
-(** Filter the disambiguators equal to 0 in a name *)
-let filter_disambiguators_zero (n : name) : name =
-  let pred (pe : path_elem) : bool =
-    match pe with Ident _ -> true | Disambiguator d -> d <> Disambiguator.zero
-  in
-  List.filter pred n
-
-(** Filter the disambiguators in a name *)
-let filter_disambiguators (n : name) : name =
-  let pred (pe : path_elem) : bool =
-    match pe with Ident _ -> true | Disambiguator _ -> false
-  in
-  List.filter pred n
-
-let as_ident (pe : path_elem) : string =
-  match pe with
-  | Ident s -> s
-  | Disambiguator _ -> raise (Failure "Improper variant")
-
-let path_elem_to_string (pe : path_elem) : string =
-  match pe with
-  | Ident s -> s
-  | Disambiguator d -> "{" ^ Disambiguator.to_string d ^ "}"
-
-let name_to_string (name : name) : string =
-  String.concat "::" (List.map path_elem_to_string name)
+include Charon.Names
diff --git a/compiler/OfJsonBasic.ml b/compiler/OfJsonBasic.ml
deleted file mode 100644
index 07daf03d..00000000
--- a/compiler/OfJsonBasic.ml
+++ /dev/null
@@ -1,75 +0,0 @@
-(** This module defines various basic utilities for json deserialization.
-   
- *)
-
-open Yojson.Basic
-
-type json = t
-
-let ( let* ) o f = match o with Error e -> Error e | Ok x -> f x
-
-let combine_error_msgs js msg res : ('a, string) result =
-  match res with
-  | Ok x -> Ok x
-  | Error e -> Error ("[" ^ msg ^ "]" ^ " failed on: " ^ show js ^ "\n\n" ^ e)
-
-let bool_of_json (js : json) : (bool, string) result =
-  match js with
-  | `Bool b -> Ok b
-  | _ -> Error ("bool_of_json: not a bool: " ^ show js)
-
-let int_of_json (js : json) : (int, string) result =
-  match js with
-  | `Int i -> Ok i
-  | _ -> Error ("int_of_json: not an int: " ^ show js)
-
-let char_of_json (js : json) : (char, string) result =
-  match js with
-  | `String c ->
-      if String.length c = 1 then Ok c.[0]
-      else Error ("char_of_json: stricly more than one character in: " ^ show js)
-  | _ -> Error ("char_of_json: not a char: " ^ show js)
-
-let rec of_json_list (a_of_json : json -> ('a, string) result) (jsl : json list)
-    : ('a list, string) result =
-  match jsl with
-  | [] -> Ok []
-  | x :: jsl' ->
-      let* x = a_of_json x in
-      let* jsl' = of_json_list a_of_json jsl' in
-      Ok (x :: jsl')
-
-let pair_of_json (a_of_json : json -> ('a, string) result)
-    (b_of_json : json -> ('b, string) result) (js : json) :
-    ('a * 'b, string) result =
-  match js with
-  | `List [ a; b ] ->
-      let* a = a_of_json a in
-      let* b = b_of_json b in
-      Ok (a, b)
-  | _ -> Error ("pair_of_json failed on: " ^ show js)
-
-let list_of_json (a_of_json : json -> ('a, string) result) (js : json) :
-    ('a list, string) result =
-  combine_error_msgs js "list_of_json"
-    (match js with
-    | `List jsl -> of_json_list a_of_json jsl
-    | _ -> Error ("not a list: " ^ show js))
-
-let string_of_json (js : json) : (string, string) result =
-  match js with
-  | `String str -> Ok str
-  | _ -> Error ("string_of_json: not a string: " ^ show js)
-
-let option_of_json (a_of_json : json -> ('a, string) result) (js : json) :
-    ('a option, string) result =
-  combine_error_msgs js "option_of_json"
-    (match js with
-    | `Null -> Ok None
-    | _ ->
-        let* x = a_of_json js in
-        Ok (Some x))
-
-let string_option_of_json (js : json) : (string option, string) result =
-  combine_error_msgs js "string_option_of_json"
-    (option_of_json string_of_json js)
diff --git a/compiler/PrimitiveValues.ml b/compiler/PrimitiveValues.ml
index 0bf37256..0eacca9e 100644
--- a/compiler/PrimitiveValues.ml
+++ b/compiler/PrimitiveValues.ml
@@ -1,41 +1 @@
-(** The primitive values. *)
-
-open Types
-
-(** We use big integers to store the integer values (this way we don't have
-    to think about the bounds, nor architecture issues - Rust allows to
-    manipulate 128-bit integers for instance).
- *)
-type big_int = Z.t
-
-let big_int_of_yojson (json : Yojson.Safe.t) : (big_int, string) result =
-  match json with
-  | `Int i -> Ok (Z.of_int i)
-  | `Intlit is -> Ok (Z.of_string is)
-  | _ -> Error "not an integer or an integer literal"
-
-let big_int_to_yojson (i : big_int) = `Intlit (Z.to_string i)
-
-let pp_big_int (fmt : Format.formatter) (bi : big_int) : unit =
-  Format.pp_print_string fmt (Z.to_string bi)
-
-let show_big_int (bi : big_int) : string = Z.to_string bi
-
-(** A scalar value
-
-    Note that we use unbounded integers everywhere.
-    We then harcode the boundaries for the different types.
- *)
-type scalar_value = { value : big_int; int_ty : integer_type } [@@deriving show]
-
-(** A primitive value.
-
-    Can be used by operands (in which case it represents a constant) or by
-    the interpreter to represent a concrete, primitive value.
- *)
-type primitive_value =
-  | Scalar of scalar_value
-  | Bool of bool
-  | Char of char
-  | String of string
-[@@deriving show]
+include Charon.PrimitiveValues
diff --git a/compiler/Print.ml b/compiler/Print.ml
index cc25c780..3f15bd32 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -1,226 +1,8 @@
-open Names
-module T = Types
-module TU = TypesUtils
+include Charon.Print
 module V = Values
 module VU = ValuesUtils
-module E = Expressions
-module A = LlbcAst
 module C = Contexts
 
-let option_to_string (to_string : 'a -> string) (x : 'a option) : string =
-  match x with Some x -> "Some (" ^ to_string x ^ ")" | None -> "None"
-
-let name_to_string (name : name) : string = Names.name_to_string name
-let fun_name_to_string (name : fun_name) : string = name_to_string name
-let global_name_to_string (name : global_name) : string = name_to_string name
-
-(** Pretty-printing for types *)
-module Types = struct
-  let type_var_to_string (tv : T.type_var) : string = tv.name
-
-  let region_var_to_string (rv : T.region_var) : string =
-    match rv.name with
-    | Some name -> name
-    | None -> T.RegionVarId.to_string rv.index
-
-  let region_var_id_to_string (rid : T.RegionVarId.id) : string =
-    "rv@" ^ T.RegionVarId.to_string rid
-
-  let region_id_to_string (rid : T.RegionId.id) : string =
-    "r@" ^ T.RegionId.to_string rid
-
-  let region_to_string (rid_to_string : 'rid -> string) (r : 'rid T.region) :
-      string =
-    match r with Static -> "'static" | Var rid -> rid_to_string rid
-
-  let erased_region_to_string (_ : T.erased_region) : string = "'_"
-
-  let ref_kind_to_string (rk : T.ref_kind) : string =
-    match rk with Mut -> "Mut" | Shared -> "Shared"
-
-  let assumed_ty_to_string (_ : T.assumed_ty) : string = "Box"
-
-  type 'r type_formatter = {
-    r_to_string : 'r -> string;
-    type_var_id_to_string : T.TypeVarId.id -> string;
-    type_decl_id_to_string : T.TypeDeclId.id -> string;
-  }
-
-  type stype_formatter = T.RegionVarId.id T.region type_formatter
-  type rtype_formatter = T.RegionId.id T.region type_formatter
-  type etype_formatter = T.erased_region type_formatter
-
-  let integer_type_to_string = function
-    | T.Isize -> "isize"
-    | T.I8 -> "i8"
-    | T.I16 -> "i16"
-    | T.I32 -> "i32"
-    | T.I64 -> "i64"
-    | T.I128 -> "i128"
-    | T.Usize -> "usize"
-    | T.U8 -> "u8"
-    | T.U16 -> "u16"
-    | T.U32 -> "u32"
-    | T.U64 -> "u64"
-    | T.U128 -> "u128"
-
-  let type_id_to_string (fmt : 'r type_formatter) (id : T.type_id) : string =
-    match id with
-    | T.AdtId id -> fmt.type_decl_id_to_string id
-    | T.Tuple -> ""
-    | T.Assumed aty -> (
-        match aty with
-        | Box -> "alloc::boxed::Box"
-        | Vec -> "alloc::vec::Vec"
-        | Option -> "core::option::Option")
-
-  let rec ty_to_string (fmt : 'r type_formatter) (ty : 'r T.ty) : string =
-    match ty with
-    | T.Adt (id, regions, tys) ->
-        let is_tuple = match id with T.Tuple -> true | _ -> false in
-        let params = params_to_string fmt is_tuple regions tys in
-        type_id_to_string fmt id ^ params
-    | T.TypeVar tv -> fmt.type_var_id_to_string tv
-    | T.Bool -> "bool"
-    | T.Char -> "char"
-    | T.Never -> "⊥"
-    | T.Integer int_ty -> integer_type_to_string int_ty
-    | T.Str -> "str"
-    | T.Array aty -> "[" ^ ty_to_string fmt aty ^ "; ?]"
-    | T.Slice sty -> "[" ^ ty_to_string fmt sty ^ "]"
-    | T.Ref (r, rty, ref_kind) -> (
-        match ref_kind with
-        | T.Mut ->
-            "&" ^ fmt.r_to_string r ^ " mut (" ^ ty_to_string fmt rty ^ ")"
-        | T.Shared ->
-            "&" ^ fmt.r_to_string r ^ " (" ^ ty_to_string fmt rty ^ ")")
-
-  and params_to_string (fmt : 'r type_formatter) (is_tuple : bool)
-      (regions : 'r list) (types : 'r T.ty list) : string =
-    let regions = List.map fmt.r_to_string regions in
-    let types = List.map (ty_to_string fmt) types in
-    let params = String.concat ", " (List.append regions types) in
-    if is_tuple then "(" ^ params ^ ")"
-    else if List.length regions + List.length types > 0 then "<" ^ params ^ ">"
-    else ""
-
-  let sty_to_string (fmt : stype_formatter) (ty : T.sty) : string =
-    ty_to_string fmt ty
-
-  let rty_to_string (fmt : rtype_formatter) (ty : T.rty) : string =
-    ty_to_string fmt ty
-
-  let ety_to_string (fmt : etype_formatter) (ty : T.ety) : string =
-    ty_to_string fmt ty
-
-  let field_to_string fmt (f : T.field) : string =
-    match f.field_name with
-    | Some field_name -> field_name ^ " : " ^ ty_to_string fmt f.field_ty
-    | None -> ty_to_string fmt f.field_ty
-
-  let variant_to_string fmt (v : T.variant) : string =
-    v.variant_name ^ "("
-    ^ String.concat ", " (List.map (field_to_string fmt) v.fields)
-    ^ ")"
-
-  let type_decl_to_string (type_decl_id_to_string : T.TypeDeclId.id -> string)
-      (def : T.type_decl) : string =
-    let regions = def.region_params in
-    let types = def.type_params in
-    let rid_to_string rid =
-      match List.find_opt (fun rv -> rv.T.index = rid) regions with
-      | Some rv -> region_var_to_string rv
-      | None -> failwith "Unreachable"
-    in
-    let r_to_string = region_to_string rid_to_string in
-    let type_var_id_to_string id =
-      match List.find_opt (fun tv -> tv.T.index = id) types with
-      | Some tv -> type_var_to_string tv
-      | None -> failwith "Unreachable"
-    in
-    let fmt = { r_to_string; type_var_id_to_string; type_decl_id_to_string } in
-    let name = name_to_string def.name in
-    let params =
-      if List.length regions + List.length types > 0 then
-        let regions = List.map region_var_to_string regions in
-        let types = List.map type_var_to_string types in
-        let params = String.concat ", " (List.append regions types) in
-        "<" ^ params ^ ">"
-      else ""
-    in
-    match def.kind with
-    | T.Struct fields ->
-        if List.length fields > 0 then
-          let fields =
-            String.concat ","
-              (List.map (fun f -> "\n  " ^ field_to_string fmt f) fields)
-          in
-          "struct " ^ name ^ params ^ "{" ^ fields ^ "}"
-        else "struct " ^ name ^ params ^ "{}"
-    | T.Enum variants ->
-        let variants =
-          List.map (fun v -> "|  " ^ variant_to_string fmt v) variants
-        in
-        let variants = String.concat "\n" variants in
-        "enum " ^ name ^ params ^ " =\n" ^ variants
-    | T.Opaque -> "opaque type " ^ name ^ params
-
-  let type_ctx_to_adt_variant_to_string_fun
-      (ctx : T.type_decl T.TypeDeclId.Map.t) :
-      T.TypeDeclId.id -> T.VariantId.id -> string =
-   fun def_id variant_id ->
-    let def = T.TypeDeclId.Map.find def_id ctx in
-    match def.kind with
-    | Struct _ | Opaque -> failwith "Unreachable"
-    | Enum variants ->
-        let variant = T.VariantId.nth variants variant_id in
-        name_to_string def.name ^ "::" ^ variant.variant_name
-
-  let type_ctx_to_adt_field_names_fun (ctx : T.type_decl T.TypeDeclId.Map.t) :
-      T.TypeDeclId.id -> T.VariantId.id option -> string list option =
-   fun def_id opt_variant_id ->
-    let def = T.TypeDeclId.Map.find def_id ctx in
-    let fields = TU.type_decl_get_fields def opt_variant_id in
-    (* There are two cases: either all the fields have names, or none of them
-     * has names *)
-    let has_names =
-      List.exists (fun f -> Option.is_some f.T.field_name) fields
-    in
-    if has_names then
-      let fields = List.map (fun f -> Option.get f.T.field_name) fields in
-      Some fields
-    else None
-
-  let type_ctx_to_adt_field_to_string_fun (ctx : T.type_decl T.TypeDeclId.Map.t)
-      :
-      T.TypeDeclId.id -> T.VariantId.id option -> T.FieldId.id -> string option
-      =
-   fun def_id opt_variant_id field_id ->
-    let def = T.TypeDeclId.Map.find def_id ctx in
-    let fields = TU.type_decl_get_fields def opt_variant_id in
-    let field = T.FieldId.nth fields field_id in
-    field.T.field_name
-end
-
-module PT = Types (* local module *)
-
-(** Pretty-printing for primitive values *)
-module PrimitiveValues = struct
-  let big_int_to_string (bi : V.big_int) : string = Z.to_string bi
-
-  let scalar_value_to_string (sv : V.scalar_value) : string =
-    big_int_to_string sv.value ^ ": " ^ PT.integer_type_to_string sv.int_ty
-
-  let primitive_value_to_string (cv : V.primitive_value) : string =
-    match cv with
-    | Scalar sv -> scalar_value_to_string sv
-    | Bool b -> Bool.to_string b
-    | Char c -> String.make 1 c
-    | String s -> s
-end
-
-module PPV = PrimitiveValues (* local module *)
-
 (** Pretty-printing for values *)
 module Values = struct
   type value_formatter = {
@@ -229,7 +11,7 @@ module Values = struct
     type_var_id_to_string : T.TypeVarId.id -> string;
     type_decl_id_to_string : T.TypeDeclId.id -> string;
     adt_variant_to_string : T.TypeDeclId.id -> T.VariantId.id -> string;
-    var_id_to_string : V.VarId.id -> string;
+    var_id_to_string : E.VarId.id -> string;
     adt_field_names :
       T.TypeDeclId.id -> T.VariantId.id option -> string list option;
   }
@@ -255,8 +37,8 @@ module Values = struct
       PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
     }
 
-  let var_id_to_string (id : V.VarId.id) : string =
-    "var@" ^ V.VarId.to_string id
+  let var_id_to_string (id : E.VarId.id) : string =
+    "var@" ^ E.VarId.to_string id
 
   let symbolic_value_id_to_string (id : V.SymbolicValueId.id) : string =
     "s@" ^ V.SymbolicValueId.to_string id
@@ -522,413 +304,6 @@ end
 
 module PV = Values (* local module *)
 
-(** Pretty-printing for LLBC AST (generic functions) *)
-module LlbcAst = struct
-  let var_to_string (var : A.var) : string =
-    match var.name with
-    | None -> V.VarId.to_string var.index
-    | Some name -> name
-
-  type ast_formatter = {
-    rvar_to_string : T.RegionVarId.id -> string;
-    r_to_string : T.RegionId.id -> string;
-    type_var_id_to_string : T.TypeVarId.id -> string;
-    type_decl_id_to_string : T.TypeDeclId.id -> string;
-    adt_variant_to_string : T.TypeDeclId.id -> T.VariantId.id -> string;
-    adt_field_to_string :
-      T.TypeDeclId.id -> T.VariantId.id option -> T.FieldId.id -> string option;
-    var_id_to_string : V.VarId.id -> string;
-    adt_field_names :
-      T.TypeDeclId.id -> T.VariantId.id option -> string list option;
-    fun_decl_id_to_string : A.FunDeclId.id -> string;
-    global_decl_id_to_string : A.GlobalDeclId.id -> string;
-  }
-
-  let ast_to_etype_formatter (fmt : ast_formatter) : PT.etype_formatter =
-    {
-      PT.r_to_string = PT.erased_region_to_string;
-      PT.type_var_id_to_string = fmt.type_var_id_to_string;
-      PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
-    }
-
-  let ast_to_rtype_formatter (fmt : ast_formatter) : PT.rtype_formatter =
-    {
-      PT.r_to_string = PT.region_to_string fmt.r_to_string;
-      PT.type_var_id_to_string = fmt.type_var_id_to_string;
-      PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
-    }
-
-  let ast_to_stype_formatter (fmt : ast_formatter) : PT.stype_formatter =
-    {
-      PT.r_to_string = PT.region_to_string fmt.rvar_to_string;
-      PT.type_var_id_to_string = fmt.type_var_id_to_string;
-      PT.type_decl_id_to_string = fmt.type_decl_id_to_string;
-    }
-
-  let fun_decl_to_ast_formatter (type_decls : T.type_decl T.TypeDeclId.Map.t)
-      (fun_decls : A.fun_decl A.FunDeclId.Map.t)
-      (global_decls : A.global_decl A.GlobalDeclId.Map.t) (fdef : A.fun_decl) :
-      ast_formatter =
-    let rvar_to_string r =
-      let rvar = T.RegionVarId.nth fdef.signature.region_params r in
-      PT.region_var_to_string rvar
-    in
-    let r_to_string r = PT.region_id_to_string r in
-
-    let type_var_id_to_string vid =
-      let var = T.TypeVarId.nth fdef.signature.type_params vid in
-      PT.type_var_to_string var
-    in
-    let type_decl_id_to_string def_id =
-      let def = T.TypeDeclId.Map.find def_id type_decls in
-      name_to_string def.name
-    in
-    let adt_variant_to_string =
-      PT.type_ctx_to_adt_variant_to_string_fun type_decls
-    in
-    let var_id_to_string vid =
-      let var = V.VarId.nth (Option.get fdef.body).locals vid in
-      var_to_string var
-    in
-    let adt_field_names = PT.type_ctx_to_adt_field_names_fun type_decls in
-    let adt_field_to_string =
-      PT.type_ctx_to_adt_field_to_string_fun type_decls
-    in
-    let fun_decl_id_to_string def_id =
-      let def = A.FunDeclId.Map.find def_id fun_decls in
-      fun_name_to_string def.name
-    in
-    let global_decl_id_to_string def_id =
-      let def = A.GlobalDeclId.Map.find def_id global_decls in
-      global_name_to_string def.name
-    in
-    {
-      rvar_to_string;
-      r_to_string;
-      type_var_id_to_string;
-      type_decl_id_to_string;
-      adt_variant_to_string;
-      var_id_to_string;
-      adt_field_names;
-      adt_field_to_string;
-      fun_decl_id_to_string;
-      global_decl_id_to_string;
-    }
-
-  let rec projection_to_string (fmt : ast_formatter) (inside : string)
-      (p : E.projection) : string =
-    match p with
-    | [] -> inside
-    | pe :: p' -> (
-        let s = projection_to_string fmt inside p' in
-        match pe with
-        | E.Deref -> "*(" ^ s ^ ")"
-        | E.DerefBox -> "deref_box(" ^ s ^ ")"
-        | E.Field (E.ProjOption variant_id, fid) ->
-            assert (variant_id = T.option_some_id);
-            assert (fid = T.FieldId.zero);
-            "(" ^ s ^ " as Option::Some)." ^ T.FieldId.to_string fid
-        | E.Field (E.ProjTuple _, fid) ->
-            "(" ^ s ^ ")." ^ T.FieldId.to_string fid
-        | E.Field (E.ProjAdt (adt_id, opt_variant_id), fid) -> (
-            let field_name =
-              match fmt.adt_field_to_string adt_id opt_variant_id fid with
-              | Some field_name -> field_name
-              | None -> T.FieldId.to_string fid
-            in
-            match opt_variant_id with
-            | None -> "(" ^ s ^ ")." ^ field_name
-            | Some variant_id ->
-                let variant_name =
-                  fmt.adt_variant_to_string adt_id variant_id
-                in
-                "(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name))
-
-  let place_to_string (fmt : ast_formatter) (p : E.place) : string =
-    let var = fmt.var_id_to_string p.E.var_id in
-    projection_to_string fmt var p.E.projection
-
-  let unop_to_string (unop : E.unop) : string =
-    match unop with
-    | E.Not -> "¬"
-    | E.Neg -> "-"
-    | E.Cast (src, tgt) ->
-        "cast<"
-        ^ PT.integer_type_to_string src
-        ^ ","
-        ^ PT.integer_type_to_string tgt
-        ^ ">"
-
-  let binop_to_string (binop : E.binop) : string =
-    match binop with
-    | E.BitXor -> "^"
-    | E.BitAnd -> "&"
-    | E.BitOr -> "|"
-    | E.Eq -> "=="
-    | E.Lt -> "<"
-    | E.Le -> "<="
-    | E.Ne -> "!="
-    | E.Ge -> ">="
-    | E.Gt -> ">"
-    | E.Div -> "/"
-    | E.Rem -> "%"
-    | E.Add -> "+"
-    | E.Sub -> "-"
-    | E.Mul -> "*"
-    | E.Shl -> "<<"
-    | E.Shr -> ">>"
-
-  let operand_to_string (fmt : ast_formatter) (op : E.operand) : string =
-    match op with
-    | E.Copy p -> "copy " ^ place_to_string fmt p
-    | E.Move p -> "move " ^ place_to_string fmt p
-    | E.Constant (ty, cv) ->
-        "("
-        ^ PPV.primitive_value_to_string cv
-        ^ " : "
-        ^ PT.ety_to_string (ast_to_etype_formatter fmt) ty
-        ^ ")"
-
-  let rvalue_to_string (fmt : ast_formatter) (rv : E.rvalue) : string =
-    match rv with
-    | E.Use op -> operand_to_string fmt op
-    | E.Ref (p, bk) -> (
-        let p = place_to_string fmt p in
-        match bk with
-        | E.Shared -> "&" ^ p
-        | E.Mut -> "&mut " ^ p
-        | E.TwoPhaseMut -> "&two-phase " ^ p)
-    | E.UnaryOp (unop, op) ->
-        unop_to_string unop ^ " " ^ operand_to_string fmt op
-    | E.BinaryOp (binop, op1, op2) ->
-        operand_to_string fmt op1 ^ " " ^ binop_to_string binop ^ " "
-        ^ operand_to_string fmt op2
-    | E.Discriminant p -> "discriminant(" ^ place_to_string fmt p ^ ")"
-    | E.Aggregate (akind, ops) -> (
-        let ops = List.map (operand_to_string fmt) ops in
-        match akind with
-        | E.AggregatedTuple -> "(" ^ String.concat ", " ops ^ ")"
-        | E.AggregatedOption (variant_id, _ty) ->
-            if variant_id == T.option_none_id then (
-              assert (ops == []);
-              "@Option::None")
-            else if variant_id == T.option_some_id then (
-              assert (List.length ops == 1);
-              let op = List.hd ops in
-              "@Option::Some(" ^ op ^ ")")
-            else raise (Failure "Unreachable")
-        | E.AggregatedAdt (def_id, opt_variant_id, _regions, _types) ->
-            let adt_name = fmt.type_decl_id_to_string def_id in
-            let variant_name =
-              match opt_variant_id with
-              | None -> adt_name
-              | Some variant_id ->
-                  adt_name ^ "::" ^ fmt.adt_variant_to_string def_id variant_id
-            in
-            let fields =
-              match fmt.adt_field_names def_id opt_variant_id with
-              | None -> "(" ^ String.concat ", " ops ^ ")"
-              | Some field_names ->
-                  let fields = List.combine field_names ops in
-                  let fields =
-                    List.map
-                      (fun (field, value) -> field ^ " = " ^ value ^ ";")
-                      fields
-                  in
-                  let fields = String.concat " " fields in
-                  "{ " ^ fields ^ " }"
-            in
-            variant_name ^ " " ^ fields)
-
-  let rec statement_to_string (fmt : ast_formatter) (indent : string)
-      (indent_incr : string) (st : A.statement) : string =
-    raw_statement_to_string fmt indent indent_incr st.content
-
-  and raw_statement_to_string (fmt : ast_formatter) (indent : string)
-      (indent_incr : string) (st : A.raw_statement) : string =
-    match st with
-    | A.Assign (p, rv) ->
-        indent ^ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv
-    | A.AssignGlobal { dst; global } ->
-        indent ^ fmt.var_id_to_string dst ^ " := global "
-        ^ fmt.global_decl_id_to_string global
-    | A.FakeRead p -> indent ^ "fake_read " ^ place_to_string fmt p
-    | A.SetDiscriminant (p, variant_id) ->
-        (* TODO: improve this to lookup the variant name by using the def id *)
-        indent ^ "set_discriminant(" ^ place_to_string fmt p ^ ", "
-        ^ T.VariantId.to_string variant_id
-        ^ ")"
-    | A.Drop p -> indent ^ "drop " ^ place_to_string fmt p
-    | A.Assert a ->
-        let cond = operand_to_string fmt a.A.cond in
-        if a.A.expected then indent ^ "assert(" ^ cond ^ ")"
-        else indent ^ "assert(¬" ^ cond ^ ")"
-    | A.Call call ->
-        let ty_fmt = ast_to_etype_formatter fmt in
-        let t_params =
-          if List.length call.A.type_args > 0 then
-            "<"
-            ^ String.concat ","
-                (List.map (PT.ty_to_string ty_fmt) call.A.type_args)
-            ^ ">"
-          else ""
-        in
-        let args = List.map (operand_to_string fmt) call.A.args in
-        let args = "(" ^ String.concat ", " args ^ ")" in
-        let name_args =
-          match call.A.func with
-          | A.Regular fid -> fmt.fun_decl_id_to_string fid ^ t_params
-          | A.Assumed fid -> (
-              match fid with
-              | A.Replace -> "core::mem::replace" ^ t_params
-              | A.BoxNew -> "alloc::boxed::Box" ^ t_params ^ "::new"
-              | A.BoxDeref ->
-                  "core::ops::deref::Deref<Box" ^ t_params ^ ">::deref"
-              | A.BoxDerefMut ->
-                  "core::ops::deref::DerefMut" ^ t_params ^ "::deref_mut"
-              | A.BoxFree -> "alloc::alloc::box_free" ^ t_params
-              | A.VecNew -> "alloc::vec::Vec" ^ t_params ^ "::new"
-              | A.VecPush -> "alloc::vec::Vec" ^ t_params ^ "::push"
-              | A.VecInsert -> "alloc::vec::Vec" ^ t_params ^ "::insert"
-              | A.VecLen -> "alloc::vec::Vec" ^ t_params ^ "::len"
-              | A.VecIndex ->
-                  "core::ops::index::Index<alloc::vec::Vec" ^ t_params
-                  ^ ">::index"
-              | A.VecIndexMut ->
-                  "core::ops::index::IndexMut<alloc::vec::Vec" ^ t_params
-                  ^ ">::index_mut")
-        in
-        let dest = place_to_string fmt call.A.dest in
-        indent ^ dest ^ " := move " ^ name_args ^ args
-    | A.Panic -> indent ^ "panic"
-    | A.Return -> indent ^ "return"
-    | A.Break i -> indent ^ "break " ^ string_of_int i
-    | A.Continue i -> indent ^ "continue " ^ string_of_int i
-    | A.Nop -> indent ^ "nop"
-    | A.Sequence (st1, st2) ->
-        statement_to_string fmt indent indent_incr st1
-        ^ ";\n"
-        ^ statement_to_string fmt indent indent_incr st2
-    | A.Switch (op, tgts) -> (
-        let op = operand_to_string fmt op in
-        match tgts with
-        | A.If (true_st, false_st) ->
-            let inner_indent = indent ^ indent_incr in
-            let inner_to_string =
-              statement_to_string fmt inner_indent indent_incr
-            in
-            let true_st = inner_to_string true_st in
-            let false_st = inner_to_string false_st in
-            indent ^ "if (" ^ op ^ ") {\n" ^ true_st ^ "\n" ^ indent ^ "}\n"
-            ^ indent ^ "else {\n" ^ false_st ^ "\n" ^ indent ^ "}"
-        | A.SwitchInt (_ty, branches, otherwise) ->
-            let indent1 = indent ^ indent_incr in
-            let indent2 = indent1 ^ indent_incr in
-            let inner_to_string2 =
-              statement_to_string fmt indent2 indent_incr
-            in
-            let branches =
-              List.map
-                (fun (svl, be) ->
-                  let svl =
-                    List.map
-                      (fun sv -> "| " ^ PPV.scalar_value_to_string sv)
-                      svl
-                  in
-                  let svl = String.concat " " svl in
-                  indent1 ^ svl ^ " => {\n" ^ inner_to_string2 be ^ "\n"
-                  ^ indent1 ^ "}")
-                branches
-            in
-            let branches = String.concat "\n" branches in
-            let branches =
-              branches ^ "\n" ^ indent1 ^ "_ => {\n"
-              ^ inner_to_string2 otherwise ^ "\n" ^ indent1 ^ "}"
-            in
-            indent ^ "switch (" ^ op ^ ") {\n" ^ branches ^ "\n" ^ indent ^ "}")
-    | A.Loop loop_st ->
-        indent ^ "loop {\n"
-        ^ statement_to_string fmt (indent ^ indent_incr) indent_incr loop_st
-        ^ "\n" ^ indent ^ "}"
-
-  let var_to_string (v : A.var) : string =
-    match v.name with None -> PV.var_id_to_string v.index | Some name -> name
-
-  let fun_decl_to_string (fmt : ast_formatter) (indent : string)
-      (indent_incr : string) (def : A.fun_decl) : string =
-    let sty_fmt = ast_to_stype_formatter fmt in
-    let sty_to_string = PT.sty_to_string sty_fmt in
-    let ety_fmt = ast_to_etype_formatter fmt in
-    let ety_to_string = PT.ety_to_string ety_fmt in
-    let sg = def.signature in
-
-    (* Function name *)
-    let name = fun_name_to_string def.A.name in
-
-    (* Region/type parameters *)
-    let regions = sg.region_params in
-    let types = sg.type_params in
-    let params =
-      if List.length regions + List.length types = 0 then ""
-      else
-        let regions = List.map PT.region_var_to_string regions in
-        let types = List.map PT.type_var_to_string types in
-        "<" ^ String.concat "," (List.append regions types) ^ ">"
-    in
-
-    (* Return type *)
-    let ret_ty = sg.output in
-    let ret_ty =
-      if TU.ty_is_unit ret_ty then "" else " -> " ^ sty_to_string ret_ty
-    in
-
-    (* We print the declaration differently if it is opaque (no body) or transparent
-     * (we have access to a body) *)
-    match def.body with
-    | None ->
-        (* Arguments *)
-        let input_tys = sg.inputs in
-        let args = List.map sty_to_string input_tys in
-        let args = String.concat ", " args in
-
-        (* Put everything together *)
-        indent ^ "opaque fn " ^ name ^ params ^ "(" ^ args ^ ")" ^ ret_ty
-    | Some body ->
-        (* Arguments *)
-        let inputs = List.tl body.locals in
-        let inputs, _aux_locals =
-          Collections.List.split_at inputs body.arg_count
-        in
-        let args = List.combine inputs sg.inputs in
-        let args =
-          List.map
-            (fun (var, rty) -> var_to_string var ^ " : " ^ sty_to_string rty)
-            args
-        in
-        let args = String.concat ", " args in
-
-        (* All the locals (with erased regions) *)
-        let locals =
-          List.map
-            (fun var ->
-              indent ^ indent_incr ^ var_to_string var ^ " : "
-              ^ ety_to_string var.var_ty ^ ";")
-            body.locals
-        in
-        let locals = String.concat "\n" locals in
-
-        (* Body *)
-        let body =
-          statement_to_string fmt (indent ^ indent_incr) indent_incr body.body
-        in
-
-        (* Put everything together *)
-        indent ^ "fn " ^ name ^ params ^ "(" ^ args ^ ")" ^ ret_ty ^ " {\n"
-        ^ locals ^ "\n\n" ^ body ^ "\n" ^ indent ^ "}"
-end
-
-module PA = LlbcAst (* local module *)
-
 (** Pretty-printing for contexts *)
 module Contexts = struct
   let binder_to_string (bv : C.binder) : string =
@@ -1129,105 +504,6 @@ end
 
 module PC = Contexts (* local module *)
 
-(** Pretty-printing for ASTs (functions based on a definition context) *)
-module Module = struct
-  (** This function pretty-prints a type definition by using a definition
-      context *)
-  let type_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t)
-      (def : T.type_decl) : string =
-    let type_decl_id_to_string (id : T.TypeDeclId.id) : string =
-      let def = T.TypeDeclId.Map.find id type_context in
-      name_to_string def.name
-    in
-    PT.type_decl_to_string type_decl_id_to_string def
-
-  (** Generate an [ast_formatter] by using a definition context in combination
-      with the variables local to a function's definition *)
-  let def_ctx_to_ast_formatter (type_context : T.type_decl T.TypeDeclId.Map.t)
-      (fun_context : A.fun_decl A.FunDeclId.Map.t)
-      (global_context : A.global_decl A.GlobalDeclId.Map.t) (def : A.fun_decl) :
-      PA.ast_formatter =
-    let rvar_to_string vid =
-      let var = T.RegionVarId.nth def.signature.region_params vid in
-      PT.region_var_to_string var
-    in
-    let r_to_string vid =
-      (* TODO: we might want something more informative *)
-      PT.region_id_to_string vid
-    in
-    let type_var_id_to_string vid =
-      let var = T.TypeVarId.nth def.signature.type_params vid in
-      PT.type_var_to_string var
-    in
-    let type_decl_id_to_string def_id =
-      let def = T.TypeDeclId.Map.find def_id type_context in
-      name_to_string def.name
-    in
-    let fun_decl_id_to_string def_id =
-      let def = A.FunDeclId.Map.find def_id fun_context in
-      fun_name_to_string def.name
-    in
-    let global_decl_id_to_string def_id =
-      let def = A.GlobalDeclId.Map.find def_id global_context in
-      global_name_to_string def.name
-    in
-    let var_id_to_string vid =
-      let var = V.VarId.nth (Option.get def.body).locals vid in
-      PA.var_to_string var
-    in
-    let adt_variant_to_string =
-      PT.type_ctx_to_adt_variant_to_string_fun type_context
-    in
-    let adt_field_to_string =
-      PT.type_ctx_to_adt_field_to_string_fun type_context
-    in
-    let adt_field_names = PT.type_ctx_to_adt_field_names_fun type_context in
-    {
-      rvar_to_string;
-      r_to_string;
-      type_var_id_to_string;
-      type_decl_id_to_string;
-      adt_variant_to_string;
-      adt_field_to_string;
-      var_id_to_string;
-      adt_field_names;
-      fun_decl_id_to_string;
-      global_decl_id_to_string;
-    }
-
-  (** This function pretty-prints a function definition by using a definition
-      context *)
-  let fun_decl_to_string (type_context : T.type_decl T.TypeDeclId.Map.t)
-      (fun_context : A.fun_decl A.FunDeclId.Map.t)
-      (global_context : A.global_decl A.GlobalDeclId.Map.t) (def : A.fun_decl) :
-      string =
-    let fmt =
-      def_ctx_to_ast_formatter type_context fun_context global_context def
-    in
-    PA.fun_decl_to_string fmt "" "  " def
-
-  let module_to_string (m : Crates.llbc_crate) : string =
-    let types_defs_map, funs_defs_map, globals_defs_map =
-      Crates.compute_defs_maps m
-    in
-
-    (* The types *)
-    let type_decls =
-      List.map (type_decl_to_string types_defs_map) m.Crates.types
-    in
-
-    (* The functions *)
-    let fun_decls =
-      List.map
-        (fun_decl_to_string types_defs_map funs_defs_map globals_defs_map)
-        m.Crates.functions
-    in
-
-    (* Put everything together *)
-    let all_defs = List.append type_decls fun_decls in
-    String.concat "\n\n" all_defs
-end
-
 (** Pretty-printing for LLBC ASTs (functions based on an evaluation context) *)
 module EvalCtxLlbcAst = struct
   let ety_to_string (ctx : C.eval_ctx) (t : T.ety) : string =
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 67353547..0b2e3a62 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -223,7 +223,7 @@ let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =
    * use indices of the variables in the original LLBC program, while
    * regular places use indices for the pure variables: we want to make
    * this explicit, otherwise it is confusing. *)
-  let name = name ^ "^" ^ V.VarId.to_string p.var_id ^ "llbc" in
+  let name = name ^ "^" ^ E.VarId.to_string p.var_id ^ "llbc" in
   mprojection_to_string fmt name p.projection
 
 let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index ae4cba22..f9c693c6 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -1,7 +1,7 @@
 open Identifiers
 open Names
-module T = Types
 module PV = PrimitiveValues
+module T = Types
 module V = Values
 module E = Expressions
 module A = LlbcAst
@@ -18,7 +18,7 @@ module GlobalDeclId = A.GlobalDeclId
     for group of regions 0, etc.) *)
 module SynthPhaseId = IdGen ()
 
-(** Pay attention to the fact that we also define a {!Values.VarId} module in Values *)
+(** Pay attention to the fact that we also define a {!E.VarId} module in Values *)
 module VarId = IdGen ()
 
 type integer_type = T.integer_type [@@deriving show, ord]
@@ -156,7 +156,7 @@ type mprojection = mprojection_elem list [@@deriving show]
     we introduce.
  *)
 type mplace = {
-  var_id : V.VarId.id;
+  var_id : E.VarId.id;
   name : string option;
   projection : mprojection;
 }
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 5da07e55..81879883 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -104,7 +104,7 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator =
 type pn_ctx = {
   pure_vars : string VarId.Map.t;
       (** Information about the pure variables used in the synthesized program *)
-  llbc_vars : string V.VarId.Map.t;
+  llbc_vars : string E.VarId.Map.t;
       (** Information about the LLBC variables used in the original program *)
 }
 
@@ -237,14 +237,14 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
         ctx0.pure_vars ctx1.pure_vars
     in
     let llbc_vars =
-      V.VarId.Map.fold
-        (fun id name ctx -> V.VarId.Map.add id name ctx)
+      E.VarId.Map.fold
+        (fun id name ctx -> E.VarId.Map.add id name ctx)
         ctx0.llbc_vars ctx1.llbc_vars
     in
     { pure_vars; llbc_vars }
   in
   let empty_ctx =
-    { pure_vars = VarId.Map.empty; llbc_vars = V.VarId.Map.empty }
+    { pure_vars = VarId.Map.empty; llbc_vars = E.VarId.Map.empty }
   in
   let merge_ctxs_ls (ctxs : pn_ctx list) : pn_ctx =
     List.fold_left (fun ctx0 ctx1 -> merge_ctxs ctx0 ctx1) empty_ctx ctxs
@@ -281,7 +281,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
         | None ->
             if Option.is_some mp then
               match
-                V.VarId.Map.find_opt (Option.get mp).var_id ctx.llbc_vars
+                E.VarId.Map.find_opt (Option.get mp).var_id ctx.llbc_vars
               with
               | None -> v
               | Some basename -> { v with basename = Some basename }
@@ -300,9 +300,9 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
 
   (* Register an mplace the first time we find one *)
   let register_mplace (mp : mplace) (ctx : pn_ctx) : pn_ctx =
-    match (V.VarId.Map.find_opt mp.var_id ctx.llbc_vars, mp.name) with
+    match (E.VarId.Map.find_opt mp.var_id ctx.llbc_vars, mp.name) with
     | None, Some name ->
-        let llbc_vars = V.VarId.Map.add mp.var_id name ctx.llbc_vars in
+        let llbc_vars = E.VarId.Map.add mp.var_id name ctx.llbc_vars in
         { ctx with llbc_vars }
     | _ -> ctx
   in
@@ -318,11 +318,11 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     { ctx with pure_vars }
   in
   (* Similar to [add_pure_var_constraint], but for LLBC variables *)
-  let add_llbc_var_constraint (var_id : V.VarId.id) (name : string)
+  let add_llbc_var_constraint (var_id : E.VarId.id) (name : string)
       (ctx : pn_ctx) : pn_ctx =
     let llbc_vars =
-      if V.VarId.Map.mem var_id ctx.llbc_vars then ctx.llbc_vars
-      else V.VarId.Map.add var_id name ctx.llbc_vars
+      if E.VarId.Map.mem var_id ctx.llbc_vars then ctx.llbc_vars
+      else E.VarId.Map.add var_id name ctx.llbc_vars
     in
     { ctx with llbc_vars }
   in
@@ -399,7 +399,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
             | Some { var_id; name; projection = [] } -> (
                 if Option.is_some name then add (Option.get name) ctx
                 else
-                  match V.VarId.Map.find_opt var_id ctx.llbc_vars with
+                  match E.VarId.Map.find_opt var_id ctx.llbc_vars with
                   | None -> ctx
                   | Some name -> add name ctx)
             | _ -> ctx
@@ -500,7 +500,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
                 let name =
                   match name with
                   | Some name -> Some name
-                  | None -> V.VarId.Map.find_opt var_id ctx.llbc_vars
+                  | None -> E.VarId.Map.find_opt var_id ctx.llbc_vars
                 in
                 match name with
                 | None -> ctx
@@ -530,7 +530,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
         let ctx =
           {
             pure_vars = VarId.Map.of_list input_names;
-            llbc_vars = V.VarId.Map.empty;
+            llbc_vars = E.VarId.Map.empty;
           }
         in
         let _, body_exp = update_texpression body.body ctx in
diff --git a/compiler/Scalars.ml b/compiler/Scalars.ml
index 03ca506c..8a1e981b 100644
--- a/compiler/Scalars.ml
+++ b/compiler/Scalars.ml
@@ -1,59 +1 @@
-open Types
-open Values
-
-(** The minimum/maximum values an integer type can have depending on its type *)
-
-let i8_min = Z.of_string "-128"
-let i8_max = Z.of_string "127"
-let i16_min = Z.of_string "-32768"
-let i16_max = Z.of_string "32767"
-let i32_min = Z.of_string "-2147483648"
-let i32_max = Z.of_string "2147483647"
-let i64_min = Z.of_string "-9223372036854775808"
-let i64_max = Z.of_string "9223372036854775807"
-let i128_min = Z.of_string "-170141183460469231731687303715884105728"
-let i128_max = Z.of_string "170141183460469231731687303715884105727"
-let u8_min = Z.of_string "0"
-let u8_max = Z.of_string "255"
-let u16_min = Z.of_string "0"
-let u16_max = Z.of_string "65535"
-let u32_min = Z.of_string "0"
-let u32_max = Z.of_string "4294967295"
-let u64_min = Z.of_string "0"
-let u64_max = Z.of_string "18446744073709551615"
-let u128_min = Z.of_string "0"
-let u128_max = Z.of_string "340282366920938463463374607431768211455"
-
-(** Being a bit conservative about isize/usize: depending on the system,
-    the values are encoded as 32-bit values or 64-bit values - we may
-    want to take that into account in the future *)
-
-let isize_min = i32_min
-let isize_max = i32_max
-let usize_min = u32_min
-let usize_max = u32_max
-
-(** Check that an integer value is in range *)
-let check_int_in_range (int_ty : integer_type) (i : big_int) : bool =
-  match int_ty with
-  | Isize -> Z.leq isize_min i && Z.leq i isize_max
-  | I8 -> Z.leq i8_min i && Z.leq i i8_max
-  | I16 -> Z.leq i16_min i && Z.leq i i16_max
-  | I32 -> Z.leq i32_min i && Z.leq i i32_max
-  | I64 -> Z.leq i64_min i && Z.leq i i64_max
-  | I128 -> Z.leq i128_min i && Z.leq i i128_max
-  | Usize -> Z.leq usize_min i && Z.leq i usize_max
-  | U8 -> Z.leq u8_min i && Z.leq i u8_max
-  | U16 -> Z.leq u16_min i && Z.leq i u16_max
-  | U32 -> Z.leq u32_min i && Z.leq i u32_max
-  | U64 -> Z.leq u64_min i && Z.leq i u64_max
-  | U128 -> Z.leq u128_min i && Z.leq i u128_max
-
-(** Check that a scalar value is correct (the integer value it contains is in range) *)
-let check_scalar_value_in_range (v : scalar_value) : bool =
-  check_int_in_range v.int_ty v.value
-
-(** Make a scalar value, while checking the value is in range *)
-let mk_scalar (int_ty : integer_type) (i : big_int) :
-    (scalar_value, unit) result =
-  if check_int_in_range int_ty i then Ok { value = i; int_ty } else Error ()
+include Charon.Scalars
diff --git a/compiler/Types.ml b/compiler/Types.ml
index 326ef76f..c76b6ffa 100644
--- a/compiler/Types.ml
+++ b/compiler/Types.ml
@@ -1,208 +1 @@
-open Identifiers
-open Names
-open Meta
-module TypeVarId = IdGen ()
-module TypeDeclId = IdGen ()
-module VariantId = IdGen ()
-module FieldId = IdGen ()
-
-(** Region variable ids. Used in function signatures. *)
-module RegionVarId = IdGen ()
-
-(** Region ids. Used for symbolic executions. *)
-module RegionId = IdGen ()
-
-module RegionGroupId = IdGen ()
-
-type ('id, 'name) indexed_var = {
-  index : 'id;  (** Unique index identifying the variable *)
-  name : 'name;  (** Variable name *)
-}
-[@@deriving show]
-
-type type_var = (TypeVarId.id, string) indexed_var [@@deriving show]
-type region_var = (RegionVarId.id, string option) indexed_var [@@deriving show]
-
-(** A region.
-    
-    Regions are used in function signatures (in which case we use region variable
-    ids) and in symbolic variables and projections (in which case we use region
-    ids).
- *)
-type 'rid region =
-  | Static  (** Static region *)
-  | Var of 'rid  (** Non-static region *)
-[@@deriving show, ord]
-
-(** The type of erased regions.
-    
-    We could use unit, but having a dedicated type makes things more explicit.
- *)
-type erased_region = Erased [@@deriving show, ord]
-
-(** A group of regions.
-
-    Results from a lifetime analysis: we group the regions with the same
-    lifetime together, and compute the hierarchy between the regions.
-    This is necessary to introduce the proper abstraction with the
-    proper constraints, when evaluating a function call in symbolic mode.
-*)
-type ('id, 'r) g_region_group = {
-  id : 'id;
-  regions : 'r list;
-  parents : 'id list;
-}
-[@@deriving show]
-
-type ('r, 'id) g_region_groups = ('r, 'id) g_region_group list [@@deriving show]
-
-type region_var_group = (RegionGroupId.id, RegionVarId.id) g_region_group
-[@@deriving show]
-
-type region_var_groups = (RegionGroupId.id, RegionVarId.id) g_region_groups
-[@@deriving show]
-
-type integer_type =
-  | Isize
-  | I8
-  | I16
-  | I32
-  | I64
-  | I128
-  | Usize
-  | U8
-  | U16
-  | U32
-  | U64
-  | U128
-[@@deriving show, ord]
-
-let all_signed_int_types = [ Isize; I8; I16; I32; I64; I128 ]
-let all_unsigned_int_types = [ Usize; U8; U16; U32; U64; U128 ]
-let all_int_types = List.append all_signed_int_types all_unsigned_int_types
-
-type ref_kind = Mut | Shared [@@deriving show, ord]
-type assumed_ty = Box | Vec | Option [@@deriving show, ord]
-
-(** The variant id for [Option::None] *)
-let option_none_id = VariantId.of_int 0
-
-(** The variant id for [Option::Some] *)
-let option_some_id = VariantId.of_int 1
-
-(** Type identifier for ADTs.
-
-    ADTs are very general in our encoding: they account for "regular" ADTs,
-    tuples and also assumed types.
-*)
-type type_id = AdtId of TypeDeclId.id | Tuple | Assumed of assumed_ty
-[@@deriving show, ord]
-
-(** Ancestor for iter visitor for [ty] *)
-class ['self] iter_ty_base =
-  object (_self : 'self)
-    inherit [_] VisitorsRuntime.iter
-    method visit_'r : 'env -> 'r -> unit = fun _ _ -> ()
-    method visit_id : 'env -> TypeVarId.id -> unit = fun _ _ -> ()
-    method visit_type_id : 'env -> type_id -> unit = fun _ _ -> ()
-    method visit_integer_type : 'env -> integer_type -> unit = fun _ _ -> ()
-    method visit_ref_kind : 'env -> ref_kind -> unit = fun _ _ -> ()
-  end
-
-(** Ancestor for map visitor for [ty] *)
-class ['self] map_ty_base =
-  object (_self : 'self)
-    inherit [_] VisitorsRuntime.map
-    method visit_'r : 'env -> 'r -> 'r = fun _ r -> r
-    method visit_id : 'env -> TypeVarId.id -> TypeVarId.id = fun _ id -> id
-    method visit_type_id : 'env -> type_id -> type_id = fun _ id -> id
-
-    method visit_integer_type : 'env -> integer_type -> integer_type =
-      fun _ ity -> ity
-
-    method visit_ref_kind : 'env -> ref_kind -> ref_kind = fun _ rk -> rk
-  end
-
-type 'r ty =
-  | Adt of type_id * 'r list * 'r ty list
-      (** {!Adt} encodes ADTs, tuples and assumed types *)
-  | TypeVar of TypeVarId.id
-  | Bool
-  | Char
-  | Never
-  | Integer of integer_type
-  | Str
-  | Array of 'r ty (* TODO: there should be a constant with the array *)
-  | Slice of 'r ty
-  | Ref of 'r * 'r ty * ref_kind
-[@@deriving
-  show,
-    ord,
-    visitors
-      {
-        name = "iter_ty";
-        variety = "iter";
-        ancestors = [ "iter_ty_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-        polymorphic = false;
-      },
-    visitors
-      {
-        name = "map_ty";
-        variety = "map";
-        ancestors = [ "map_ty_base" ];
-        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
-        concrete = true;
-        polymorphic = false;
-      }]
-(* TODO: group Bool, Char, etc. in Constant *)
-
-(** Generic type with regions *)
-type 'r gr_ty = 'r region ty [@@deriving show, ord]
-
-(** *S*ignature types.
-
-    Used in function signatures and type definitions.
- *)
-type sty = RegionVarId.id gr_ty [@@deriving show, ord]
-
-(** Type with *R*egions.
-
-    Used to project borrows/loans inside of abstractions, during symbolic
-    execution.
- *)
-type rty = RegionId.id gr_ty [@@deriving show, ord]
-
-(** Type with *E*rased regions.
-    
-    Used in function bodies, "regular" value types, etc.
- *)
-type ety = erased_region ty [@@deriving show, ord]
-
-type field = { meta : meta; field_name : string option; field_ty : sty }
-[@@deriving show]
-
-type variant = { meta : meta; variant_name : string; fields : field list }
-[@@deriving show]
-
-type type_decl_kind =
-  | Struct of field list
-  | Enum of variant list
-  | Opaque
-      (** An opaque type: either a local type marked as opaque, or an external type *)
-[@@deriving show]
-
-type type_decl = {
-  def_id : TypeDeclId.id;
-  meta : meta;
-  name : type_name;
-  region_params : region_var list;
-  type_params : type_var list;
-  kind : type_decl_kind;
-  regions_hierarchy : region_var_groups;
-      (** Stores the hierarchy between the regions (which regions have the
-          same lifetime, which lifetime should end before which other lifetime,
-          etc.) *)
-}
-[@@deriving show]
+include Charon.Types
diff --git a/compiler/TypesUtils.ml b/compiler/TypesUtils.ml
index 7531dd8b..c7f0fbc3 100644
--- a/compiler/TypesUtils.ml
+++ b/compiler/TypesUtils.ml
@@ -1,130 +1,7 @@
 open Types
-open Utils
+include Charon.TypesUtils
 module TA = TypesAnalysis
 
-let type_decl_is_opaque (d : type_decl) : bool =
-  match d.kind with Struct _ | Enum _ -> false | Opaque -> true
-
-(** Retrieve the list of fields for the given variant of a {!Types.type_decl}.
-
-    Raises [Invalid_argument] if the arguments are incorrect.
- *)
-let type_decl_get_fields (def : type_decl)
-    (opt_variant_id : VariantId.id option) : field list =
-  match (def.kind, opt_variant_id) with
-  | Enum variants, Some variant_id -> (VariantId.nth variants variant_id).fields
-  | Struct fields, None -> fields
-  | _ ->
-      let opt_variant_id =
-        match opt_variant_id with None -> "None" | Some _ -> "Some"
-      in
-      raise
-        (Invalid_argument
-           ("The variant id should be [Some] if and only if the definition is \
-             an enumeration:\n\
-             - def: " ^ show_type_decl def ^ "\n- opt_variant_id: "
-          ^ opt_variant_id))
-
-(** Return [true] if a {!Types.ty} is actually [unit] *)
-let ty_is_unit (ty : 'r ty) : bool =
-  match ty with Adt (Tuple, [], []) -> true | _ -> false
-
-let ty_is_adt (ty : 'r ty) : bool =
-  match ty with Adt (_, _, _) -> true | _ -> false
-
-let ty_as_adt (ty : 'r ty) : type_id * 'r list * 'r ty list =
-  match ty with
-  | Adt (id, regions, tys) -> (id, regions, tys)
-  | _ -> failwith "Unreachable"
-
-let ty_is_custom_adt (ty : 'r ty) : bool =
-  match ty with Adt (AdtId _, _, _) -> true | _ -> false
-
-let ty_as_custom_adt (ty : 'r ty) : TypeDeclId.id * 'r list * 'r ty list =
-  match ty with
-  | Adt (AdtId id, regions, tys) -> (id, regions, tys)
-  | _ -> failwith "Unreachable"
-
-(** The unit type *)
-let mk_unit_ty : 'r ty = Adt (Tuple, [], [])
-
-(** The usize type *)
-let mk_usize_ty : 'r ty = Integer Usize
-
-(** Deconstruct a type of the form [Box<T>] to retrieve the [T] inside *)
-let ty_get_box (box_ty : ety) : ety =
-  match box_ty with
-  | Adt (Assumed Box, [], [ boxed_ty ]) -> boxed_ty
-  | _ -> failwith "Not a boxed type"
-
-(** Deconstruct a type of the form [&T] or [&mut T] to retrieve the [T] (and
-    the borrow kind, etc.)
- *)
-let ty_get_ref (ty : 'r ty) : 'r * 'r ty * ref_kind =
-  match ty with
-  | Ref (r, ty, ref_kind) -> (r, ty, ref_kind)
-  | _ -> failwith "Not a ref type"
-
-let mk_ref_ty (r : 'r) (ty : 'r ty) (ref_kind : ref_kind) : 'r ty =
-  Ref (r, ty, ref_kind)
-
-(** Make a box type *)
-let mk_box_ty (ty : 'r ty) : 'r ty = Adt (Assumed Box, [], [ ty ])
-
-(** Make a vec type *)
-let mk_vec_ty (ty : 'r ty) : 'r ty = Adt (Assumed Vec, [], [ ty ])
-
-(** Check if a region is in a set of regions *)
-let region_in_set (r : RegionId.id region) (rset : RegionId.Set.t) : bool =
-  match r with Static -> false | Var id -> RegionId.Set.mem id rset
-
-(** Return the set of regions in an rty *)
-let rty_regions (ty : rty) : RegionId.Set.t =
-  let s = ref RegionId.Set.empty in
-  let add_region (r : RegionId.id region) =
-    match r with Static -> () | Var rid -> s := RegionId.Set.add rid !s
-  in
-  let obj =
-    object
-      inherit [_] iter_ty
-      method! visit_'r _env r = add_region r
-    end
-  in
-  (* Explore the type *)
-  obj#visit_ty () ty;
-  (* Return the set of accumulated regions *)
-  !s
-
-let rty_regions_intersect (ty : rty) (regions : RegionId.Set.t) : bool =
-  let ty_regions = rty_regions ty in
-  not (RegionId.Set.disjoint ty_regions regions)
-
-(** Convert an {!Types.ety}, containing no region variables, to an {!Types.rty}
-    or an {!Types.sty}.
-
-    In practice, it is the identity.
- *)
-let rec ety_no_regions_to_gr_ty (ty : ety) : 'a gr_ty =
-  match ty with
-  | Adt (type_id, regions, tys) ->
-      assert (regions = []);
-      Adt (type_id, [], List.map ety_no_regions_to_gr_ty tys)
-  | TypeVar v -> TypeVar v
-  | Bool -> Bool
-  | Char -> Char
-  | Never -> Never
-  | Integer int_ty -> Integer int_ty
-  | Str -> Str
-  | Array ty -> Array (ety_no_regions_to_gr_ty ty)
-  | Slice ty -> Slice (ety_no_regions_to_gr_ty ty)
-  | Ref (_, _, _) ->
-      failwith
-        "Can't convert a ref with erased regions to a ref with non-erased \
-         regions"
-
-let ety_no_regions_to_rty (ty : ety) : rty = ety_no_regions_to_gr_ty ty
-let ety_no_regions_to_sty (ty : ety) : sty = ety_no_regions_to_gr_ty ty
-
 (** Retuns true if the type contains borrows.
 
     Note that we can't simply explore the type and look for regions: sometimes
@@ -149,42 +26,3 @@ let ty_has_nested_borrows (infos : TA.type_infos) (ty : 'r ty) : bool =
 let ty_has_borrow_under_mut (infos : TA.type_infos) (ty : 'r ty) : bool =
   let info = TA.analyze_ty infos ty in
   info.TA.contains_borrow_under_mut
-
-(** Check if a {!Types.ty} contains regions from a given set *)
-let ty_has_regions_in_set (rset : RegionId.Set.t) (ty : rty) : bool =
-  let obj =
-    object
-      inherit [_] iter_ty as super
-
-      method! visit_Adt env type_id regions tys =
-        List.iter (fun r -> if region_in_set r rset then raise Found) regions;
-        super#visit_Adt env type_id regions tys
-
-      method! visit_Ref env r ty rkind =
-        if region_in_set r rset then raise Found
-        else super#visit_Ref env r ty rkind
-    end
-  in
-  try
-    obj#visit_ty () ty;
-    false
-  with Found -> true
-
-(** Return true if a type is "primitively copyable".
-  *
-  * "primitively copyable" means that copying instances of this type doesn't
-  * require calling dedicated functions defined through the Copy trait. It
-  * is the case for types like integers, shared borrows, etc.
-  *
-  * Generally, ADTs are not copyable. However, some of the primitive ADTs are
-  * like `Option`.
-  *)
-let rec ty_is_primitively_copyable (ty : 'r ty) : bool =
-  match ty with
-  | Adt (Assumed Option, _, tys) -> List.for_all ty_is_primitively_copyable tys
-  | Adt ((AdtId _ | Assumed (Box | Vec)), _, _) -> false
-  | Adt (Tuple, _, tys) -> List.for_all ty_is_primitively_copyable tys
-  | TypeVar _ | Never | Str | Array _ | Slice _ -> false
-  | Bool | Char | Integer _ -> true
-  | Ref (_, _, Mut) -> false
-  | Ref (_, _, Shared) -> true
diff --git a/compiler/Utils.ml b/compiler/Utils.ml
index 9a79eb55..987ac317 100644
--- a/compiler/Utils.ml
+++ b/compiler/Utils.ml
@@ -1,6 +1 @@
-(** Utility exception
-
-    When looking for something while exploring a term, it can be easier to
-    just throw an exception to signal we found what we were looking for.
- *)
-exception Found
+include Charon.Utils
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 7d6623aa..6245608d 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -1,11 +1,11 @@
 open Identifiers
 open Types
+module PrimitiveValues = PrimitiveValues
 
 (* TODO(SH): I often write "abstract" (value, borrow content, etc.) while I should
  * write "abstraction" (because those values are not abstract, they simply are
  * inside abstractions) *)
 
-module VarId = IdGen ()
 module BorrowId = IdGen ()
 module SymbolicValueId = IdGen ()
 module AbstractionId = IdGen ()
diff --git a/compiler/dune b/compiler/dune
index f0fd2102..d3f5eaec 100644
--- a/compiler/dune
+++ b/compiler/dune
@@ -1,12 +1,8 @@
-;; core: for Core.Unix.mkdir_p
-
 (executable
  (name driver)
  (public_name aeneas_driver)
  (package aeneas)
- (preprocess
-  (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
- (libraries ppx_deriving yojson zarith easy_logging core_unix aeneas)
+ (libraries aeneas)
  (modules Driver))
 
 (library
@@ -14,7 +10,7 @@
  (public_name aeneas) ;; The name as revealed to the projects importing this library
  (preprocess
   (pps ppx_deriving.show ppx_deriving.ord visitors.ppx))
- (libraries ppx_deriving yojson zarith easy_logging core_unix)
+ (libraries charon core_unix)
  (modules
   Assumed
   Collections
@@ -44,7 +40,6 @@
   Logging
   Meta
   Names
-  OfJsonBasic
   PrePasses
   Print
   PrintPure
diff --git a/compiler/dune-project b/compiler/dune-project
index f8b418f2..650eeec0 100644
--- a/compiler/dune-project
+++ b/compiler/dune-project
@@ -6,8 +6,6 @@
 
 (generate_opam_files true)
 
-(formatting)
-
 (source
  (uri git+https://github.com/AeneasVerif/aeneas.git))