diff --git a/compiler/dcalc/from_scopelang.ml b/compiler/dcalc/from_scopelang.ml
index bd06d614..a720c69d 100644
--- a/compiler/dcalc/from_scopelang.ml
+++ b/compiler/dcalc/from_scopelang.ml
@@ -16,7 +16,6 @@
 
 open Catala_utils
 open Shared_ast
-
 module S = Scopelang.Ast
 
 type scope_var_ctx = {
@@ -150,8 +149,8 @@ let tag_with_log_entry
 
    NOTE: the choice of the exception that will be triggered and show in the
    trace is arbitrary (but deterministic). *)
-let collapse_similar_outcomes (type m) (excepts : m S.expr list) :
-    m S.expr list =
+let collapse_similar_outcomes (type m) (excepts : m S.expr list) : m S.expr list
+    =
   let module ExprMap = Map.Make (struct
     type t = m S.expr
 
@@ -213,8 +212,7 @@ let thunk_scope_arg var_ctx e =
     Expr.make_abs [| Var.make "_" |] e [TLit TUnit, pos] pos
   | _ -> assert false
 
-let rec translate_expr (ctx : 'm ctx) (e : 'm S.expr) :
-    'm Ast.expr boxed =
+let rec translate_expr (ctx : 'm ctx) (e : 'm S.expr) : 'm Ast.expr boxed =
   let m = Mark.get e in
   match Mark.remove e with
   | EMatch { e = e1; name; cases = e_cases } ->
@@ -575,9 +573,9 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm S.expr) :
     | EIfThenElse _ | EAppOp _ ) as e ->
     Expr.map ~f:(translate_expr ctx) ~op:Operator.translate (e, m)
 
-(** The result of a rule translation is a list of assignments, with variables and
-    expressions. We also return the new translation context available after the
-    assignment to use in later rule translations. The list is actually a
+(** The result of a rule translation is a list of assignments, with variables
+    and expressions. We also return the new translation context available after
+    the assignment to use in later rule translations. The list is actually a
     continuation yielding a [Dcalc.scope_body_expr] by giving it what should
     come later in the chain of let-bindings. *)
 let translate_rule
@@ -591,12 +589,13 @@ let translate_rule
   | S.ScopeVarDefinition { var; typ; e; _ }
   | S.SubScopeVarDefinition { var; typ; e; _ } ->
     let pos_mark, _ = pos_mark_mk e in
-    let scope_let_kind, io = match rule with
-      | S.ScopeVarDefinition {io; _} -> ScopeVarDefinition, io
+    let scope_let_kind, io =
+      match rule with
+      | S.ScopeVarDefinition { io; _ } -> ScopeVarDefinition, io
       | S.SubScopeVarDefinition _ ->
         let pos = Mark.get var in
-        SubScopeVarDefinition,
-        { io_input = (NoInput, pos); io_output = (false, pos) }
+        ( SubScopeVarDefinition,
+          { io_input = NoInput, pos; io_output = false, pos } )
       | S.Assertion _ -> assert false
     in
     let a_name = ScopeVar.get_info (Mark.remove var) in
@@ -763,9 +762,11 @@ let translate_scope_decl
          or not ? *)
       Message.raise_spanned_error pos_sigma "Scope %a has no content"
         ScopeName.format scope_name
-    | (S.ScopeVarDefinition { e; _ }
+    | ( S.ScopeVarDefinition { e; _ }
       | S.SubScopeVarDefinition { e; _ }
-      | S.Assertion e) :: _ -> Mark.get e
+      | S.Assertion e )
+      :: _ ->
+      Mark.get e
   in
   let rules_with_return_expr, ctx =
     translate_rules ctx scope_name sigma.scope_decl_rules sigma_info scope_mark
diff --git a/compiler/desugared/ast.ml b/compiler/desugared/ast.ml
index 30e1b023..71be1155 100644
--- a/compiler/desugared/ast.ml
+++ b/compiler/desugared/ast.ml
@@ -27,25 +27,29 @@ module ScopeDef = struct
   module Base = struct
     type kind =
       | Var of StateName.t option
-      | SubScope of { name: ScopeName.t; var_within_origin_scope: ScopeVar.t }
+      | SubScope of { name : ScopeName.t; var_within_origin_scope : ScopeVar.t }
 
     type t = ScopeVar.t Mark.pos * kind
 
-    let equal_kind k1 k2 = match k1, k2 with
+    let equal_kind k1 k2 =
+      match k1, k2 with
       | Var s1, Var s2 -> Option.equal StateName.equal s1 s2
-      | SubScope { var_within_origin_scope = v1; _ }, SubScope { var_within_origin_scope = v2; _ } -> ScopeVar.equal v1 v2
+      | ( SubScope { var_within_origin_scope = v1; _ },
+          SubScope { var_within_origin_scope = v2; _ } ) ->
+        ScopeVar.equal v1 v2
       | (Var _ | SubScope _), _ -> false
 
     let equal (v1, k1) (v2, k2) =
-      ScopeVar.equal (Mark.remove v1) (Mark.remove v2) &&
-      equal_kind k1 k2
+      ScopeVar.equal (Mark.remove v1) (Mark.remove v2) && equal_kind k1 k2
 
-    let compare_kind k1 k2 = match k1, k2 with
-    | Var st1, Var st2 -> Option.compare StateName.compare st1 st2
-    | SubScope { var_within_origin_scope = v1; _ }, SubScope { var_within_origin_scope = v2; _ } ->
-      ScopeVar.compare v1 v2
-    | Var _, SubScope _ -> -1
-    | SubScope _, Var _ -> 1
+    let compare_kind k1 k2 =
+      match k1, k2 with
+      | Var st1, Var st2 -> Option.compare StateName.compare st1 st2
+      | ( SubScope { var_within_origin_scope = v1; _ },
+          SubScope { var_within_origin_scope = v2; _ } ) ->
+        ScopeVar.compare v1 v2
+      | Var _, SubScope _ -> -1
+      | SubScope _, Var _ -> 1
 
     let compare (v1, k1) (v2, k2) =
       match Mark.compare ScopeVar.compare v1 v2 with
@@ -57,19 +61,19 @@ module ScopeDef = struct
     let format_kind ppf = function
       | Var None -> ()
       | Var (Some st) -> Format.fprintf ppf "@%a" StateName.format st
-      | SubScope { var_within_origin_scope = v; _ } -> Format.fprintf ppf ".%a" ScopeVar.format v
+      | SubScope { var_within_origin_scope = v; _ } ->
+        Format.fprintf ppf ".%a" ScopeVar.format v
 
     let format ppf (v, k) =
       ScopeVar.format ppf (Mark.remove v);
       format_kind ppf k
 
     let hash_kind = function
-      | Var (None) -> 0
+      | Var None -> 0
       | Var (Some st) -> StateName.hash st
       | SubScope { var_within_origin_scope = v; _ } -> ScopeVar.hash v
 
-    let hash (v, k) =
-      Int.logxor (ScopeVar.hash (Mark.remove v)) (hash_kind k)
+    let hash (v, k) = Int.logxor (ScopeVar.hash (Mark.remove v)) (hash_kind k)
   end
 
   include Base
@@ -249,8 +253,7 @@ type program = {
 
 let rec locations_used e : LocationSet.t =
   match e with
-  | ELocation l, m ->
-    LocationSet.singleton (l, Expr.mark_pos m)
+  | ELocation l, m -> LocationSet.singleton (l, Expr.mark_pos m)
   | e ->
     Expr.shallow_fold
       (fun e -> LocationSet.union (locations_used e))
@@ -263,8 +266,7 @@ let free_variables (def : rule RuleName.Map.t) : Pos.t ScopeDef.Map.t =
       (fun (loc, loc_pos) acc ->
         let usage =
           match loc with
-          | DesugaredScopeVar { name; state } ->
-            Some (name, ScopeDef.Var state)
+          | DesugaredScopeVar { name; state } -> Some (name, ScopeDef.Var state)
           | ToplevelVar _ -> None
         in
         match usage with
diff --git a/compiler/desugared/ast.mli b/compiler/desugared/ast.mli
index 91f396f6..308d081d 100644
--- a/compiler/desugared/ast.mli
+++ b/compiler/desugared/ast.mli
@@ -19,11 +19,12 @@
 open Catala_utils
 open Shared_ast
 
-(** Inside a scope, a definition can refer to a variable (possibly an intermediate state thereof) or an input of a subscope. *)
+(** Inside a scope, a definition can refer to a variable (possibly an
+    intermediate state thereof) or an input of a subscope. *)
 module ScopeDef : sig
   type kind =
     | Var of StateName.t option
-    | SubScope of { name: ScopeName.t; var_within_origin_scope: ScopeVar.t }
+    | SubScope of { name : ScopeName.t; var_within_origin_scope : ScopeVar.t }
 
   val equal_kind : kind -> kind -> bool
   val compare_kind : kind -> kind -> int
diff --git a/compiler/desugared/dependency.ml b/compiler/desugared/dependency.ml
index a98c96b3..fc1bf92d 100644
--- a/compiler/desugared/dependency.ml
+++ b/compiler/desugared/dependency.ml
@@ -179,7 +179,8 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
   in
   (* then add the edges *)
   let g =
-    let to_vertex (var, kind) = match kind with
+    let to_vertex (var, kind) =
+      match kind with
       | Ast.ScopeDef.Var st -> Vertex.Var (Mark.remove var, st)
       | Ast.ScopeDef.SubScope _ -> Vertex.Var (Mark.remove var, None)
     in
@@ -190,14 +191,14 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
         let fv = Ast.free_variables def in
         Ast.ScopeDef.Map.fold
           (fun fv_def fv_def_pos g ->
-             let v_used = to_vertex fv_def in
-             if Vertex.equal v_used v_defined then
-                Message.raise_spanned_error fv_def_pos
-                  "The variable %a is used in one of its definitions, but \
-                   recursion is forbidden in Catala"
-                  Ast.ScopeDef.format def_key;
-             ScopeDependencies.add_edge_e g
-               (ScopeDependencies.E.create v_used fv_def_pos v_defined))
+            let v_used = to_vertex fv_def in
+            if Vertex.equal v_used v_defined then
+              Message.raise_spanned_error fv_def_pos
+                "The variable %a is used in one of its definitions, but \
+                 recursion is forbidden in Catala"
+                Ast.ScopeDef.format def_key;
+            ScopeDependencies.add_edge_e g
+              (ScopeDependencies.E.create v_used fv_def_pos v_defined))
           fv g)
       scope.scope_defs g
   in
diff --git a/compiler/desugared/disambiguate.ml b/compiler/desugared/disambiguate.ml
index 17e43383..ebc52aff 100644
--- a/compiler/desugared/disambiguate.ml
+++ b/compiler/desugared/disambiguate.ml
@@ -84,10 +84,10 @@ let program prg =
         let vars =
           ScopeDef.Map.fold
             (fun (v, kind) def vars ->
-                 match kind with
-                 | ScopeDef.Var _ -> ScopeVar.Map.add (Mark.remove v) def.scope_def_typ vars
-                 | ScopeDef.SubScope _ -> vars
-            )
+              match kind with
+              | ScopeDef.Var _ ->
+                ScopeVar.Map.add (Mark.remove v) def.scope_def_typ vars
+              | ScopeDef.SubScope _ -> vars)
             scope.scope_defs ScopeVar.Map.empty
         in
         (* at this stage, rule resolution and the corresponding encapsulation
diff --git a/compiler/desugared/from_surface.ml b/compiler/desugared/from_surface.ml
index 71861f4f..e6981dca 100644
--- a/compiler/desugared/from_surface.ml
+++ b/compiler/desugared/from_surface.ml
@@ -482,8 +482,8 @@ let rec translate_expr
       | mod_id :: path ->
         get_str (Name_resolution.get_module_ctx ctxt mod_id) path
     in
-    Expr.edstructaccess ~e ~field:(Mark.remove x)
-      ~name_opt:(get_str ctxt path) emark
+    Expr.edstructaccess ~e ~field:(Mark.remove x) ~name_opt:(get_str ctxt path)
+      emark
   | FunCall ((Builtin b, _), [arg]) ->
     let op, ty =
       match b with
@@ -1510,20 +1510,25 @@ let init_scope_defs
   (* Initializing the definitions of all scopes and subscope vars, with no rules
      yet inside *)
   let add_def _ v scope_def_map =
-    let pos = match v with ScopeVar v | SubScope (v, _, _) -> Mark.get (ScopeVar.get_info v) in
-    let new_def v_sig io = {
-      Ast.scope_def_rules = RuleName.Map.empty;
-      Ast.scope_def_typ = v_sig.Name_resolution.var_sig_typ;
-      Ast.scope_def_is_condition = v_sig.var_sig_is_condition;
-      Ast.scope_def_parameters = v_sig.var_sig_parameters;
-      Ast.scope_def_io = io;
-    } in
+    let pos =
+      match v with
+      | ScopeVar v | SubScope (v, _, _) -> Mark.get (ScopeVar.get_info v)
+    in
+    let new_def v_sig io =
+      {
+        Ast.scope_def_rules = RuleName.Map.empty;
+        Ast.scope_def_typ = v_sig.Name_resolution.var_sig_typ;
+        Ast.scope_def_is_condition = v_sig.var_sig_is_condition;
+        Ast.scope_def_parameters = v_sig.var_sig_parameters;
+        Ast.scope_def_io = io;
+      }
+    in
     match v with
     | ScopeVar v -> (
       let v_sig = ScopeVar.Map.find v ctxt.Name_resolution.var_typs in
       match v_sig.var_sig_states_list with
       | [] ->
-        let def_key = ((v, pos), Ast.ScopeDef.Var None) in
+        let def_key = (v, pos), Ast.ScopeDef.Var None in
         Ast.ScopeDef.Map.add def_key
           (new_def v_sig (attribute_to_io v_sig.var_sig_io))
           scope_def_map
@@ -1535,9 +1540,9 @@ let init_scope_defs
               let def_key = (v, pos), Ast.ScopeDef.Var (Some state) in
               let original_io = attribute_to_io v_sig.var_sig_io in
               (* The first state should have the input I/O of the original
-                 variable, and the last state should have the output I/O
-                 of the original variable. All intermediate states shall
-                 have "internal" I/O.*)
+                 variable, and the last state should have the output I/O of the
+                 original variable. All intermediate states shall have
+                 "internal" I/O.*)
               let io_input =
                 if i = 0 then original_io.io_input
                 else NoInput, Mark.get (StateName.get_info state)
@@ -1563,32 +1568,41 @@ let init_scope_defs
           ctxt
           (ScopeName.path subscope_uid)
       in
-      let var_def = {
-        Ast.scope_def_rules = RuleName.Map.empty;
-        Ast.scope_def_typ = TStruct sub_scope_def.scope_out_struct, Mark.get (ScopeVar.get_info v0);
-        Ast.scope_def_is_condition = false;
-        Ast.scope_def_parameters = None;
-        Ast.scope_def_io = { io_input = NoInput, Mark.get forward_out; io_output = forward_out };
-      } in
+      let var_def =
+        {
+          Ast.scope_def_rules = RuleName.Map.empty;
+          Ast.scope_def_typ =
+            ( TStruct sub_scope_def.scope_out_struct,
+              Mark.get (ScopeVar.get_info v0) );
+          Ast.scope_def_is_condition = false;
+          Ast.scope_def_parameters = None;
+          Ast.scope_def_io =
+            {
+              io_input = NoInput, Mark.get forward_out;
+              io_output = forward_out;
+            };
+        }
+      in
       let scope_def_map =
-        Ast.ScopeDef.Map.add ((v0, pos), Ast.ScopeDef.Var None) var_def scope_def_map
+        Ast.ScopeDef.Map.add
+          ((v0, pos), Ast.ScopeDef.Var None)
+          var_def scope_def_map
       in
       Ident.Map.fold
         (fun _ v scope_def_map ->
           match v with
           | SubScope _ ->
-            (* TODO: if we consider "input subscopes" at some point their inputs will need to be forwarded here *)
+            (* TODO: if we consider "input subscopes" at some point their inputs
+               will need to be forwarded here *)
             scope_def_map
           | ScopeVar v ->
             (* TODO: shouldn't we ignore internal variables too at this point
                ? *)
             let v_sig = ScopeVar.Map.find v ctxt.Name_resolution.var_typs in
             let def_key =
-              (v0, Mark.get (ScopeVar.get_info v)),
-              Ast.ScopeDef.SubScope {
-                name = subscope_uid;
-                var_within_origin_scope = v;
-              }
+              ( (v0, Mark.get (ScopeVar.get_info v)),
+                Ast.ScopeDef.SubScope
+                  { name = subscope_uid; var_within_origin_scope = v } )
             in
             Ast.ScopeDef.Map.add def_key
               {
diff --git a/compiler/desugared/linting.ml b/compiler/desugared/linting.ml
index 9f3d2a86..fd589eb5 100644
--- a/compiler/desugared/linting.ml
+++ b/compiler/desugared/linting.ml
@@ -27,8 +27,11 @@ let detect_empty_definitions (p : program) : unit =
           if
             (match scope_def_key with _, ScopeDef.Var _ -> true | _ -> false)
             && RuleName.Map.is_empty scope_def.scope_def_rules
-            && not scope_def.scope_def_is_condition
-            && not (ScopeVar.Map.mem (Mark.remove (fst scope_def_key)) scope.scope_sub_scopes)
+            && (not scope_def.scope_def_is_condition)
+            && (not
+                  (ScopeVar.Map.mem
+                     (Mark.remove (fst scope_def_key))
+                     scope.scope_sub_scopes))
             &&
             match Mark.remove scope_def.scope_def_io.io_input with
             | NoInput -> true
@@ -254,7 +257,9 @@ let detect_dead_code (p : program) : unit =
         | Assertion _ -> true
         | Var (var, state) ->
           let scope_def =
-            ScopeDef.Map.find ((var, Pos.no_pos), ScopeDef.Var state) scope.scope_defs
+            ScopeDef.Map.find
+              ((var, Pos.no_pos), ScopeDef.Var state)
+              scope.scope_defs
           in
           Mark.remove scope_def.scope_def_io.io_output
         (* A variable is initially alive if it is an output*)
@@ -263,14 +268,15 @@ let detect_dead_code (p : program) : unit =
       let emit_unused_warning vx =
         Message.emit_spanned_warning
           (Mark.get (Dependency.Vertex.info vx))
-          "Unused varible: %a does not contribute to computing \
-           any of scope %a outputs. Did you forget something?"
-          Dependency.Vertex.format vx
-          ScopeName.format scope_name
+          "Unused varible: %a does not contribute to computing any of scope %a \
+           outputs. Did you forget something?"
+          Dependency.Vertex.format vx ScopeName.format scope_name
       in
-      Dependency.ScopeDependencies.iter_vertex (fun vx ->
-          if not (is_alive vx) &&
-             Dependency.ScopeDependencies.succ scope_dependencies vx = []
+      Dependency.ScopeDependencies.iter_vertex
+        (fun vx ->
+          if
+            (not (is_alive vx))
+            && Dependency.ScopeDependencies.succ scope_dependencies vx = []
           then emit_unused_warning vx)
         scope_dependencies)
     p.program_root.module_scopes
diff --git a/compiler/desugared/name_resolution.ml b/compiler/desugared/name_resolution.ml
index 5daeed7e..19ff5007 100644
--- a/compiler/desugared/name_resolution.ml
+++ b/compiler/desugared/name_resolution.ml
@@ -163,10 +163,11 @@ let belongs_to (ctxt : context) (uid : ScopeVar.t) (scope_uid : ScopeName.t) :
       | _ -> false)
     scope.var_idmap
 
-let get_var_def (def: Ast.ScopeDef.t) : ScopeVar.t =
+let get_var_def (def : Ast.ScopeDef.t) : ScopeVar.t =
   match def with
-  | ((v, _), Ast.ScopeDef.Var _)
-  | (_, Ast.ScopeDef.SubScope { var_within_origin_scope = v; _ }) -> v
+  | (v, _), Ast.ScopeDef.Var _
+  | _, Ast.ScopeDef.SubScope { var_within_origin_scope = v; _ } ->
+    v
 
 (** Retrieves the type of a scope definition from the context *)
 let get_params (ctxt : context) (def : Ast.ScopeDef.t) :
@@ -255,7 +256,10 @@ let process_subscope_decl
     (ctxt : context)
     (decl : Surface.Ast.scope_decl_context_scope) : context =
   let name, name_pos = decl.scope_decl_context_scope_name in
-  let forward_output = decl.Surface.Ast.scope_decl_context_scope_attribute.scope_decl_context_io_output in
+  let forward_output =
+    decl.Surface.Ast.scope_decl_context_scope_attribute
+      .scope_decl_context_io_output
+  in
   let (path, subscope), s_pos = decl.scope_decl_context_scope_sub_scope in
   let scope_ctxt = get_scope_context ctxt scope in
   match Ident.Map.find_opt (Mark.remove subscope) scope_ctxt.var_idmap with
@@ -567,16 +571,18 @@ let process_scope_decl (ctxt : context) (decl : Surface.Ast.scope_decl) :
                 data.scope_decl_context_item_typ;
             }
           :: acc
-        | Surface.Ast.ContextScope {
-            scope_decl_context_scope_name = var;
-            scope_decl_context_scope_sub_scope = ((path, scope), pos);
-            scope_decl_context_scope_attribute = { scope_decl_context_io_output = true, _; _ };
-          } ->
+        | Surface.Ast.ContextScope
+            {
+              scope_decl_context_scope_name = var;
+              scope_decl_context_scope_sub_scope = (path, scope), pos;
+              scope_decl_context_scope_attribute =
+                { scope_decl_context_io_output = true, _; _ };
+            } ->
           Mark.add (Mark.get item)
             {
               Surface.Ast.struct_decl_field_name = var;
               Surface.Ast.struct_decl_field_typ =
-                (Base (Data (Primitive (Named (path, scope))))), pos;
+                Base (Data (Primitive (Named (path, scope)))), pos;
             }
           :: acc
         | _ -> acc)
@@ -765,9 +771,9 @@ let get_def_key
   | [x] ->
     let x_uid = get_var_uid scope_uid ctxt x in
     let var_sig = ScopeVar.Map.find x_uid ctxt.var_typs in
-    (x_uid, pos),
-    Ast.ScopeDef.Var
-      ( match state with
+    ( (x_uid, pos),
+      Ast.ScopeDef.Var
+        (match state with
         | Some state -> (
           try
             Some
@@ -790,22 +796,21 @@ let get_def_key
               "This definition does not indicate which state has to be \
                considered for variable %a."
               ScopeVar.format x_uid
-          else None )
+          else None) )
   | [y; x] ->
     let (subscope_var, name) : ScopeVar.t * ScopeName.t =
       match Ident.Map.find_opt (Mark.remove y) scope_ctxt.var_idmap with
       | Some (SubScope (v, u, _)) -> v, u
       | Some _ ->
         Message.raise_spanned_error pos
-          "Invalid definition, %a is not a subscope"
-          Print.lit_style (Mark.remove y)
+          "Invalid definition, %a is not a subscope" Print.lit_style
+          (Mark.remove y)
       | None ->
         Message.raise_spanned_error pos "No definition found for subscope %a"
           Print.lit_style (Mark.remove y)
     in
     let var_within_origin_scope = get_var_uid name ctxt x in
-    (subscope_var, pos),
-    Ast.ScopeDef.SubScope { name; var_within_origin_scope }
+    (subscope_var, pos), Ast.ScopeDef.SubScope { name; var_within_origin_scope }
   | _ ->
     Message.raise_spanned_error pos
       "This line is defining a quantity that is neither a scope variable nor a \
diff --git a/compiler/desugared/name_resolution.mli b/compiler/desugared/name_resolution.mli
index d0494ec8..ce54061d 100644
--- a/compiler/desugared/name_resolution.mli
+++ b/compiler/desugared/name_resolution.mli
@@ -132,8 +132,7 @@ val get_scope_context : context -> ScopeName.t -> scope_context
 val get_var_uid : ScopeName.t -> context -> Ident.t Mark.pos -> ScopeVar.t
 (** Get the variable uid inside the scope given in argument *)
 
-val get_subscope_uid :
-  ScopeName.t -> context -> Ident.t Mark.pos -> ScopeVar.t
+val get_subscope_uid : ScopeName.t -> context -> Ident.t Mark.pos -> ScopeVar.t
 (** Get the subscope uid inside the scope given in argument *)
 
 val is_subscope_uid : ScopeName.t -> context -> Ident.t -> bool
diff --git a/compiler/driver.ml b/compiler/driver.ml
index 266db1fa..afb519fb 100644
--- a/compiler/driver.ml
+++ b/compiler/driver.ml
@@ -339,7 +339,7 @@ module Commands = struct
   let get_variable_uid
       (ctxt : Desugared.Name_resolution.context)
       (scope_uid : ScopeName.t)
-      (variable : string): Desugared.Ast.ScopeDef.t =
+      (variable : string) : Desugared.Ast.ScopeDef.t =
     (* Sometimes the variable selected is of the form [a.b] *)
     let first_part, second_part =
       match String.index_opt variable '.' with
@@ -358,18 +358,19 @@ module Commands = struct
         variable ScopeName.format scope_uid
     | Some (ScopeVar v | SubScope (v, _, _)) ->
       let state =
-        second_part |> Option.map @@ fun id ->
-        let var_sig = ScopeVar.Map.find v ctxt.var_typs in
-        match Ident.Map.find_opt id var_sig.var_sig_states_idmap with
-        | Some state -> state
-        | None ->
-          Message.raise_error
-            "State @{<yellow>\"%s\"@} is not found for variable \
-             @{<yellow>\"%s\"@} of scope @{<yellow>\"%a\"@}"
-            id first_part ScopeName.format scope_uid
+        second_part
+        |> Option.map
+           @@ fun id ->
+           let var_sig = ScopeVar.Map.find v ctxt.var_typs in
+           match Ident.Map.find_opt id var_sig.var_sig_states_idmap with
+           | Some state -> state
+           | None ->
+             Message.raise_error
+               "State @{<yellow>\"%s\"@} is not found for variable \
+                @{<yellow>\"%s\"@} of scope @{<yellow>\"%a\"@}"
+               id first_part ScopeName.format scope_uid
       in
-      ( (v, Pos.no_pos),
-        Desugared.Ast.ScopeDef.Var state )
+      (v, Pos.no_pos), Desugared.Ast.ScopeDef.Var state
 
   let get_output ?ext options output_file =
     let output_file = Option.map options.Global.path_rewrite output_file in
diff --git a/compiler/scopelang/ast.ml b/compiler/scopelang/ast.ml
index cdf5663c..100cfc10 100644
--- a/compiler/scopelang/ast.ml
+++ b/compiler/scopelang/ast.ml
@@ -40,16 +40,16 @@ let rec locations_used (e : 'm expr) : LocationSet.t =
 
 type 'm rule =
   | ScopeVarDefinition of {
-      var: ScopeVar.t Mark.pos;
-      typ: typ;
-      io: Desugared.Ast.io;
-      e: 'm expr
+      var : ScopeVar.t Mark.pos;
+      typ : typ;
+      io : Desugared.Ast.io;
+      e : 'm expr;
     }
   | SubScopeVarDefinition of {
-      var: ScopeVar.t Mark.pos;
-      var_within_origin_scope: ScopeVar.t;
-      typ: typ;
-      e: 'm expr
+      var : ScopeVar.t Mark.pos;
+      var_within_origin_scope : ScopeVar.t;
+      typ : typ;
+      e : 'm expr;
     }
   | Assertion of 'm expr
 
@@ -78,7 +78,7 @@ type 'm program = {
 let type_rule decl_ctx env = function
   | ScopeVarDefinition ({ typ; e; _ } as def) ->
     let e = Typing.expr decl_ctx ~env ~typ e in
-    ScopeVarDefinition {def with e = Expr.unbox e}
+    ScopeVarDefinition { def with e = Expr.unbox e }
   | SubScopeVarDefinition ({ typ; e; _ } as def) ->
     let e = Typing.expr decl_ctx ~env ~typ e in
     SubScopeVarDefinition { def with e = Expr.unbox e }
diff --git a/compiler/scopelang/ast.mli b/compiler/scopelang/ast.mli
index c93f9cd5..c47d1336 100644
--- a/compiler/scopelang/ast.mli
+++ b/compiler/scopelang/ast.mli
@@ -33,19 +33,19 @@ val locations_used : 'm expr -> LocationSet.t
 
 type 'm rule =
   | ScopeVarDefinition of {
-      var: ScopeVar.t Mark.pos;
-      typ: typ;
-      io: Desugared.Ast.io;
-      e: 'm expr
+      var : ScopeVar.t Mark.pos;
+      typ : typ;
+      io : Desugared.Ast.io;
+      e : 'm expr;
     }
   | SubScopeVarDefinition of {
-      var: ScopeVar.t Mark.pos; (** Variable within the current scope *)
+      var : ScopeVar.t Mark.pos;  (** Variable within the current scope *)
       (* scope: ScopeVar.t Mark.pos; (\** Variable pointing to the *\) *)
       (* origin_var: ScopeVar.t Mark.pos;
        * reentrant: bool; *)
-      var_within_origin_scope: ScopeVar.t;
-      typ: typ; (* non-thunked at this point for reentrant vars *)
-      e: 'm expr
+      var_within_origin_scope : ScopeVar.t;
+      typ : typ; (* non-thunked at this point for reentrant vars *)
+      e : 'm expr;
     }
   | Assertion of 'm expr
 
diff --git a/compiler/scopelang/dependency.ml b/compiler/scopelang/dependency.ml
index b5b5b9cc..8644ae0d 100644
--- a/compiler/scopelang/dependency.ml
+++ b/compiler/scopelang/dependency.ml
@@ -94,7 +94,9 @@ let rec expr_used_defs e =
   | e -> recurse_subterms e
 
 let rule_used_defs = function
-  | Ast.Assertion e | Ast.ScopeVarDefinition { e; _} | Ast.SubScopeVarDefinition { e; _ } ->
+  | Ast.Assertion e
+  | Ast.ScopeVarDefinition { e; _ }
+  | Ast.SubScopeVarDefinition { e; _ } ->
     (* TODO: maybe this info could be passed on from previous passes without
        walking through all exprs again *)
     expr_used_defs e
diff --git a/compiler/scopelang/from_desugared.ml b/compiler/scopelang/from_desugared.ml
index 9f7c7b2f..6b9ca0cb 100644
--- a/compiler/scopelang/from_desugared.ml
+++ b/compiler/scopelang/from_desugared.ml
@@ -195,80 +195,77 @@ let rule_to_exception_graph (scope : D.scope) = function
     (* Before calling the sub_scope, we need to include all the re-definitions
        of subscope parameters*)
     D.ScopeDef.Map.fold
-      (fun (sscope, kind as def_key) scope_def exc_graphs ->
-         match kind with
-         | D.ScopeDef.Var _ -> exc_graphs
-         | D.ScopeDef.SubScope _
-           when
-             not (ScopeVar.equal var (Mark.remove sscope))
-             ||
-             Mark.remove scope_def.D.scope_def_io.io_input = NoInput
-             && RuleName.Map.is_empty scope_def.scope_def_rules
-           ->
-           (* We exclude subscope variables that have 0 re-definitions and are
-              not visible in the input of the subscope *)
-           exc_graphs
-         | D.ScopeDef.SubScope { var_within_origin_scope; _ } ->
-           (* This definition redefines a variable of the correct subscope. But
-              we have to check that this redefinition is allowed with respect
-              to the io parameters of that subscope variable. *)
-           let def = scope_def.D.scope_def_rules in
-           let is_cond = scope_def.scope_def_is_condition in
-           let () = match Mark.remove scope_def.D.scope_def_io.io_input with
-             | NoInput ->
-               Message.raise_multispanned_error
-                 (( Some "Incriminated subscope:",
-                    Mark.get (ScopeVar.get_info (Mark.remove sscope)) )
-                  :: ( Some "Incriminated variable:",
-                       Mark.get (ScopeVar.get_info var_within_origin_scope) )
-                  :: List.map
-                    (fun rule ->
+      (fun ((sscope, kind) as def_key) scope_def exc_graphs ->
+        match kind with
+        | D.ScopeDef.Var _ -> exc_graphs
+        | D.ScopeDef.SubScope _
+          when (not (ScopeVar.equal var (Mark.remove sscope)))
+               || Mark.remove scope_def.D.scope_def_io.io_input = NoInput
+                  && RuleName.Map.is_empty scope_def.scope_def_rules ->
+          (* We exclude subscope variables that have 0 re-definitions and are
+             not visible in the input of the subscope *)
+          exc_graphs
+        | D.ScopeDef.SubScope { var_within_origin_scope; _ } ->
+          (* This definition redefines a variable of the correct subscope. But
+             we have to check that this redefinition is allowed with respect to
+             the io parameters of that subscope variable. *)
+          let def = scope_def.D.scope_def_rules in
+          let is_cond = scope_def.scope_def_is_condition in
+          let () =
+            match Mark.remove scope_def.D.scope_def_io.io_input with
+            | NoInput ->
+              Message.raise_multispanned_error
+                (( Some "Incriminated subscope:",
+                   Mark.get (ScopeVar.get_info (Mark.remove sscope)) )
+                :: ( Some "Incriminated variable:",
+                     Mark.get (ScopeVar.get_info var_within_origin_scope) )
+                :: List.map
+                     (fun rule ->
                        ( Some "Incriminated subscope variable definition:",
                          Mark.get (RuleName.get_info rule) ))
-                    (RuleName.Map.keys def))
-                 "Invalid assignment to a subscope variable that is \
-                  not tagged as input or context."
-             | OnlyInput when RuleName.Map.is_empty def && not is_cond ->
-               (* If the subscope variable is tagged as input, then it shall be
-                  defined. *)
-               Message.raise_multispanned_error
-                 [
-                   ( Some "Incriminated subscope:",
-                     Mark.get (ScopeVar.get_info (Mark.remove sscope)) );
-                   Some "Incriminated variable:", Mark.get sscope;
-                 ]
-                 "This subscope variable is a mandatory input but no definition \
-                  was provided."
-             | _ -> ()
-           in
-           let new_exc_graph = def_to_exception_graph def_key def in
-           D.ScopeDef.Map.add def_key new_exc_graph exc_graphs)
-      scope.scope_defs
-      D.ScopeDef.Map.empty
-  | Desugared.Dependency.Vertex.Var (var, state) ->
-      (let pos = Mark.get (ScopeVar.get_info var) in
-       let scope_def =
-         D.ScopeDef.Map.find ((var, pos), D.ScopeDef.Var state) scope.scope_defs
-       in
-       let var_def = scope_def.D.scope_def_rules in
-       match Mark.remove scope_def.D.scope_def_io.io_input with
-       | OnlyInput when not (RuleName.Map.is_empty var_def) ->
-         (* If the variable is tagged as input, then it shall not be redefined. *)
-         Message.raise_multispanned_error
-           ((Some "Incriminated variable:", Mark.get (ScopeVar.get_info var))
-            :: List.map
-              (fun rule ->
-                 ( Some "Incriminated variable definition:",
-                   Mark.get (RuleName.get_info rule) ))
-              (RuleName.Map.keys var_def))
-           "It is impossible to give a definition to a scope variable tagged as \
-            input."
-       | OnlyInput -> D.ScopeDef.Map.empty
-       (* we do not provide any definition for an input-only variable *)
-       | _ ->
-         D.ScopeDef.Map.singleton
-           ((var, pos), (D.ScopeDef.Var state))
-           (def_to_exception_graph ((var, pos), D.ScopeDef.Var state) var_def))
+                     (RuleName.Map.keys def))
+                "Invalid assignment to a subscope variable that is not tagged \
+                 as input or context."
+            | OnlyInput when RuleName.Map.is_empty def && not is_cond ->
+              (* If the subscope variable is tagged as input, then it shall be
+                 defined. *)
+              Message.raise_multispanned_error
+                [
+                  ( Some "Incriminated subscope:",
+                    Mark.get (ScopeVar.get_info (Mark.remove sscope)) );
+                  Some "Incriminated variable:", Mark.get sscope;
+                ]
+                "This subscope variable is a mandatory input but no definition \
+                 was provided."
+            | _ -> ()
+          in
+          let new_exc_graph = def_to_exception_graph def_key def in
+          D.ScopeDef.Map.add def_key new_exc_graph exc_graphs)
+      scope.scope_defs D.ScopeDef.Map.empty
+  | Desugared.Dependency.Vertex.Var (var, state) -> (
+    let pos = Mark.get (ScopeVar.get_info var) in
+    let scope_def =
+      D.ScopeDef.Map.find ((var, pos), D.ScopeDef.Var state) scope.scope_defs
+    in
+    let var_def = scope_def.D.scope_def_rules in
+    match Mark.remove scope_def.D.scope_def_io.io_input with
+    | OnlyInput when not (RuleName.Map.is_empty var_def) ->
+      (* If the variable is tagged as input, then it shall not be redefined. *)
+      Message.raise_multispanned_error
+        ((Some "Incriminated variable:", Mark.get (ScopeVar.get_info var))
+        :: List.map
+             (fun rule ->
+               ( Some "Incriminated variable definition:",
+                 Mark.get (RuleName.get_info rule) ))
+             (RuleName.Map.keys var_def))
+        "It is impossible to give a definition to a scope variable tagged as \
+         input."
+    | OnlyInput -> D.ScopeDef.Map.empty
+    (* we do not provide any definition for an input-only variable *)
+    | _ ->
+      D.ScopeDef.Map.singleton
+        ((var, pos), D.ScopeDef.Var state)
+        (def_to_exception_graph ((var, pos), D.ScopeDef.Var state) var_def))
   | Assertion _ -> D.ScopeDef.Map.empty (* no exceptions for assertions *)
 
 let scope_to_exception_graphs (scope : D.scope) :
@@ -553,17 +550,18 @@ let translate_rule
     ctx
     (scope : D.scope)
     (exc_graphs :
-      Desugared.Dependency.ExceptionsDependencies.t D.ScopeDef.Map.t)
-    = function
-  | Desugared.Dependency.Vertex.Var (var, state) ->
+      Desugared.Dependency.ExceptionsDependencies.t D.ScopeDef.Map.t) = function
+  | Desugared.Dependency.Vertex.Var (var, state) -> (
     let pos = Mark.get (ScopeVar.get_info var) in
-    (* TODO: this may point to the place where the variable was declared instead of the binding in the definition being explored. Needs double-checking and maybe adding more position information *)
+    (* TODO: this may point to the place where the variable was declared instead
+       of the binding in the definition being explored. Needs double-checking
+       and maybe adding more position information *)
     let scope_def =
       D.ScopeDef.Map.find ((var, pos), D.ScopeDef.Var state) scope.scope_defs
     in
-    (match ScopeVar.Map.find_opt var scope.scope_sub_scopes with
-    | None ->
-      (let var_def = scope_def.D.scope_def_rules in
+    match ScopeVar.Map.find_opt var scope.scope_sub_scopes with
+    | None -> (
+      let var_def = scope_def.D.scope_def_rules in
       let var_params = scope_def.D.scope_def_parameters in
       let var_typ = scope_def.D.scope_def_typ in
       let is_cond = scope_def.D.scope_def_is_condition in
@@ -587,86 +585,98 @@ let translate_rule
           | _ -> assert false
         in
         [
-          Ast.ScopeVarDefinition {
-            var = scope_var, pos;
-            typ = var_typ;
-            io = scope_def.D.scope_def_io;
-            e = Expr.unbox expr_def;
-          }
+          Ast.ScopeVarDefinition
+            {
+              var = scope_var, pos;
+              typ = var_typ;
+              io = scope_def.D.scope_def_io;
+              e = Expr.unbox expr_def;
+            };
         ])
-      | Some subscope ->
-    (* Before calling the subscope, we need to include all the re-definitions
-       of subscope parameters *)
-    let subscope_params =
-      D.ScopeDef.Map.fold (fun def_key scope_def acc ->
-          match def_key with
-          | _, D.ScopeDef.Var _ -> acc
-          | (v, _), D.ScopeDef.SubScope _
-            when
-              not (ScopeVar.equal var v)
-              ||
-              Mark.remove scope_def.D.scope_def_io.io_input = NoInput
-              && RuleName.Map.is_empty scope_def.scope_def_rules
-            -> acc
-          | v, D.ScopeDef.SubScope { var_within_origin_scope; _ } ->
-            let pos = Mark.get v in
-            let def = scope_def.D.scope_def_rules in
-            let def_typ = scope_def.scope_def_typ in
-            let is_cond = scope_def.scope_def_is_condition in
-            assert (* an error should have been already raised *)
-              (match scope_def.D.scope_def_io.io_input with
-               | NoInput, _ -> false
-               | OnlyInput, _ -> is_cond || not (RuleName.Map.is_empty def)
-               | _ -> true);
-            let var_within_origin_scope =
-              match ScopeVar.Map.find var_within_origin_scope ctx.scope_var_mapping with
-              | WholeVar v -> v
-              | States ((_, v) :: _) -> v
-              | States [] -> assert false
-            in
-            let def_var =
-              Var.make
-                (String.concat "."
-                   [Mark.remove (ScopeVar.get_info (Mark.remove v));
-                    Mark.remove (ScopeVar.get_info var_within_origin_scope)])
-            in
-            let typ =
-              Scope.input_type def_typ scope_def.D.scope_def_io.D.io_input
-            in
-            let expr_def =
-              translate_def ctx def_key def scope_def.D.scope_def_parameters
-                def_typ scope_def.D.scope_def_io
-                (D.ScopeDef.Map.find def_key exc_graphs)
-                ~is_cond ~is_subscope_var:true
-            in
-            ScopeVar.Map.add var_within_origin_scope (def_var, pos, typ, expr_def) acc)
-        scope.scope_defs ScopeVar.Map.empty
-    in
-    let subscope_param_map =
-      ScopeVar.Map.map (fun (_, _, _, expr) -> expr)
-        subscope_params
-    in
-    let subscope_call_expr =
-      Expr.escopecall ~scope:subscope ~args:subscope_param_map (Untyped { pos })
-    in
-    let subscope_expr = subscope_call_expr in
-    assert (RuleName.Map.is_empty scope_def.D.scope_def_rules);
-    (* The subscope will be defined by its inputs, it's not supposed to have direct rules yet *)
-    let scope_info = ScopeName.Map.find subscope ctx.decl_ctx.ctx_scopes in
-    let subscope_var_dcalc =
-      match ScopeVar.Map.find var ctx.scope_var_mapping with
-      | WholeVar v -> v
-      | _ -> assert false
-    in
-    let subscope_def =
-      Ast.ScopeVarDefinition {
-        var = subscope_var_dcalc, pos;
-        typ = TStruct scope_info.out_struct_name, Mark.get (ScopeVar.get_info var);
-        io = scope_def.D.scope_def_io;
-        e = Expr.unbox_closed subscope_expr;
-      }
-    in
-    [ subscope_def ])
+    | Some subscope ->
+      (* Before calling the subscope, we need to include all the re-definitions
+         of subscope parameters *)
+      let subscope_params =
+        D.ScopeDef.Map.fold
+          (fun def_key scope_def acc ->
+            match def_key with
+            | _, D.ScopeDef.Var _ -> acc
+            | (v, _), D.ScopeDef.SubScope _
+              when (not (ScopeVar.equal var v))
+                   || Mark.remove scope_def.D.scope_def_io.io_input = NoInput
+                      && RuleName.Map.is_empty scope_def.scope_def_rules ->
+              acc
+            | v, D.ScopeDef.SubScope { var_within_origin_scope; _ } ->
+              let pos = Mark.get v in
+              let def = scope_def.D.scope_def_rules in
+              let def_typ = scope_def.scope_def_typ in
+              let is_cond = scope_def.scope_def_is_condition in
+              assert (
+                (* an error should have been already raised *)
+                match scope_def.D.scope_def_io.io_input with
+                | NoInput, _ -> false
+                | OnlyInput, _ -> is_cond || not (RuleName.Map.is_empty def)
+                | _ -> true);
+              let var_within_origin_scope =
+                match
+                  ScopeVar.Map.find var_within_origin_scope
+                    ctx.scope_var_mapping
+                with
+                | WholeVar v -> v
+                | States ((_, v) :: _) -> v
+                | States [] -> assert false
+              in
+              let def_var =
+                Var.make
+                  (String.concat "."
+                     [
+                       Mark.remove (ScopeVar.get_info (Mark.remove v));
+                       Mark.remove (ScopeVar.get_info var_within_origin_scope);
+                     ])
+              in
+              let typ =
+                Scope.input_type def_typ scope_def.D.scope_def_io.D.io_input
+              in
+              let expr_def =
+                translate_def ctx def_key def scope_def.D.scope_def_parameters
+                  def_typ scope_def.D.scope_def_io
+                  (D.ScopeDef.Map.find def_key exc_graphs)
+                  ~is_cond ~is_subscope_var:true
+              in
+              ScopeVar.Map.add var_within_origin_scope
+                (def_var, pos, typ, expr_def)
+                acc)
+          scope.scope_defs ScopeVar.Map.empty
+      in
+      let subscope_param_map =
+        ScopeVar.Map.map (fun (_, _, _, expr) -> expr) subscope_params
+      in
+      let subscope_call_expr =
+        Expr.escopecall ~scope:subscope ~args:subscope_param_map
+          (Untyped { pos })
+      in
+      let subscope_expr = subscope_call_expr in
+      assert (RuleName.Map.is_empty scope_def.D.scope_def_rules);
+      (* The subscope will be defined by its inputs, it's not supposed to have
+         direct rules yet *)
+      let scope_info = ScopeName.Map.find subscope ctx.decl_ctx.ctx_scopes in
+      let subscope_var_dcalc =
+        match ScopeVar.Map.find var ctx.scope_var_mapping with
+        | WholeVar v -> v
+        | _ -> assert false
+      in
+      let subscope_def =
+        Ast.ScopeVarDefinition
+          {
+            var = subscope_var_dcalc, pos;
+            typ =
+              ( TStruct scope_info.out_struct_name,
+                Mark.get (ScopeVar.get_info var) );
+            io = scope_def.D.scope_def_io;
+            e = Expr.unbox_closed subscope_expr;
+          }
+      in
+      [subscope_def])
   | Assertion a_name ->
     let assertion_expr =
       D.AssertionName.Map.find a_name scope.scope_assertions
@@ -688,13 +698,16 @@ let translate_scope_interface ctx scope =
       svar_io = scope_def.scope_def_io;
     }
   in
-  let scope_sig = (* Add the definitions of standard scope vars *)
+  let scope_sig =
+    (* Add the definitions of standard scope vars *)
     ScopeVar.Map.fold
       (fun var (states : D.var_or_states) acc ->
         match states with
         | WholeVar ->
           let scope_def =
-            D.ScopeDef.Map.find ((var, Pos.no_pos), D.ScopeDef.Var None) scope.D.scope_defs
+            D.ScopeDef.Map.find
+              ((var, Pos.no_pos), D.ScopeDef.Var None)
+              scope.D.scope_defs
           in
           ScopeVar.Map.add
             (match ScopeVar.Map.find var ctx.scope_var_mapping with
@@ -720,15 +733,20 @@ let translate_scope_interface ctx scope =
             acc states)
       scope.scope_vars ScopeVar.Map.empty
   in
-  let scope_sig = (* Add the definition of vars corresponding to subscope calls, and their parameters (subscope vars) *)
-    ScopeVar.Map.fold (fun var _scope_name acc ->
+  let scope_sig =
+    (* Add the definition of vars corresponding to subscope calls, and their
+       parameters (subscope vars) *)
+    ScopeVar.Map.fold
+      (fun var _scope_name acc ->
         let scope_def =
-          D.ScopeDef.Map.find ((var, Pos.no_pos), D.ScopeDef.Var None) scope.D.scope_defs
+          D.ScopeDef.Map.find
+            ((var, Pos.no_pos), D.ScopeDef.Var None)
+            scope.D.scope_defs
         in
         ScopeVar.Map.add
           (match ScopeVar.Map.find var ctx.scope_var_mapping with
-           | WholeVar v -> v
-           | States _ -> assert false)
+          | WholeVar v -> v
+          | States _ -> assert false)
           (get_svar scope_def) acc)
       scope.D.scope_sub_scopes scope_sig
   in
@@ -786,69 +804,71 @@ let translate_program
     let add_scope_mappings modul ctx =
       ScopeName.Map.fold
         (fun _ scdef ctx ->
-           let ctx =
-             (* Add normal scope vars to the env *)
-             ScopeVar.Map.fold
-               (fun scope_var (states : D.var_or_states) ctx ->
-                  let var_name, var_pos = ScopeVar.get_info scope_var in
-                  let new_var =
-                    match states with
-                    | D.WholeVar -> WholeVar (ScopeVar.fresh (var_name, var_pos))
-                    | States states ->
-                      let var_prefix = var_name ^ "_" in
-                      let state_var state =
-                        ScopeVar.fresh
-                          (Mark.map (( ^ ) var_prefix) (StateName.get_info state))
-                      in
-                      States (List.map (fun state -> state, state_var state) states)
-                  in
-                  let reentrant =
-                    let state =
-                      match states with
-                      | D.WholeVar -> None
-                      | States (s :: _) -> Some s
-                      | States [] -> assert false
+          let ctx =
+            (* Add normal scope vars to the env *)
+            ScopeVar.Map.fold
+              (fun scope_var (states : D.var_or_states) ctx ->
+                let var_name, var_pos = ScopeVar.get_info scope_var in
+                let new_var =
+                  match states with
+                  | D.WholeVar -> WholeVar (ScopeVar.fresh (var_name, var_pos))
+                  | States states ->
+                    let var_prefix = var_name ^ "_" in
+                    let state_var state =
+                      ScopeVar.fresh
+                        (Mark.map (( ^ ) var_prefix) (StateName.get_info state))
                     in
-                    match
-                      D.ScopeDef.Map.find_opt
-                        ((scope_var, Pos.no_pos), Var state)
-                        scdef.D.scope_defs
-                    with
-                    | Some
-                        {
-                          scope_def_io = { io_input = Runtime.Reentrant, _; _ };
-                          scope_def_typ;
-                          _;
-                        } ->
-                      Some scope_def_typ
-                    | _ -> None
+                    States
+                      (List.map (fun state -> state, state_var state) states)
+                in
+                let reentrant =
+                  let state =
+                    match states with
+                    | D.WholeVar -> None
+                    | States (s :: _) -> Some s
+                    | States [] -> assert false
                   in
-                  {
-                    ctx with
-                    scope_var_mapping =
-                      ScopeVar.Map.add scope_var new_var ctx.scope_var_mapping;
-                    reentrant_vars =
-                      Option.fold reentrant
-                        ~some:(fun ty ->
-                            ScopeVar.Map.add scope_var ty ctx.reentrant_vars)
-                        ~none:ctx.reentrant_vars;
-                  })
-               scdef.D.scope_vars ctx
-           in
-           let ctx =
-             (* Add scope vars pointing to subscope executions to the env
-                (their definitions are introduced during the processing of the rules above) *)
-             ScopeVar.Map.fold (fun var _ ctx ->
-                 let var_name, var_pos = ScopeVar.get_info var in
-                 let scope_var_mapping =
-                   let new_var = WholeVar (ScopeVar.fresh (var_name, var_pos)) in
-                   ScopeVar.Map.add var new_var ctx.scope_var_mapping
-                 in
-                 { ctx with scope_var_mapping }
-               )
-               scdef.D.scope_sub_scopes ctx
-           in
-           ctx)
+                  match
+                    D.ScopeDef.Map.find_opt
+                      ((scope_var, Pos.no_pos), Var state)
+                      scdef.D.scope_defs
+                  with
+                  | Some
+                      {
+                        scope_def_io = { io_input = Runtime.Reentrant, _; _ };
+                        scope_def_typ;
+                        _;
+                      } ->
+                    Some scope_def_typ
+                  | _ -> None
+                in
+                {
+                  ctx with
+                  scope_var_mapping =
+                    ScopeVar.Map.add scope_var new_var ctx.scope_var_mapping;
+                  reentrant_vars =
+                    Option.fold reentrant
+                      ~some:(fun ty ->
+                        ScopeVar.Map.add scope_var ty ctx.reentrant_vars)
+                      ~none:ctx.reentrant_vars;
+                })
+              scdef.D.scope_vars ctx
+          in
+          let ctx =
+            (* Add scope vars pointing to subscope executions to the env (their
+               definitions are introduced during the processing of the rules
+               above) *)
+            ScopeVar.Map.fold
+              (fun var _ ctx ->
+                let var_name, var_pos = ScopeVar.get_info var in
+                let scope_var_mapping =
+                  let new_var = WholeVar (ScopeVar.fresh (var_name, var_pos)) in
+                  ScopeVar.Map.add var new_var ctx.scope_var_mapping
+                in
+                { ctx with scope_var_mapping })
+              scdef.D.scope_sub_scopes ctx
+          in
+          ctx)
         modul.D.module_scopes ctx
     in
     (* Todo: since we rename all scope vars at this point, it would be better to
diff --git a/compiler/scopelang/print.ml b/compiler/scopelang/print.ml
index 1ee0a48a..713d2ac8 100644
--- a/compiler/scopelang/print.ml
+++ b/compiler/scopelang/print.ml
@@ -72,26 +72,21 @@ let scope ?debug ctx fmt (name, (decl, _pos)) =
        ~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " Print.punctuation ";")
        (fun fmt rule ->
          match rule with
-         | ScopeVarDefinition { var; typ; io; e; } ->
-           Format.fprintf fmt "@[<hov 2>%a %a %a %a %a@ %t%a@]"
-             Print.keyword "let"
-             ScopeVar.format (Mark.remove var)
-             Print.punctuation ":"
+         | ScopeVarDefinition { var; typ; io; e } ->
+           Format.fprintf fmt "@[<hov 2>%a %a %a %a %a@ %t%a@]" Print.keyword
+             "let" ScopeVar.format (Mark.remove var) Print.punctuation ":"
              (Print.typ ctx) typ Print.punctuation "="
-             (fun fmt -> match Mark.remove io.io_input with
-                | Reentrant ->
-                  Print.op_style fmt "reentrant or by default";
-                  Format.pp_print_space fmt ()
-                | _ -> ())
+             (fun fmt ->
+               match Mark.remove io.io_input with
+               | Reentrant ->
+                 Print.op_style fmt "reentrant or by default";
+                 Format.pp_print_space fmt ()
+               | _ -> ())
              (Print.expr ?debug ()) e
          | SubScopeVarDefinition { var; typ; e; _ } ->
-           Format.fprintf fmt "@[<hov 2>%a %a %a %a %a@ %a@]"
-             Print.keyword "let"
-             ScopeVar.format (Mark.remove var)
-             Print.punctuation ":"
-             (Print.typ ctx) typ
-             Print.punctuation "="
-             (Print.expr ?debug ()) e
+           Format.fprintf fmt "@[<hov 2>%a %a %a %a %a@ %a@]" Print.keyword
+             "let" ScopeVar.format (Mark.remove var) Print.punctuation ":"
+             (Print.typ ctx) typ Print.punctuation "=" (Print.expr ?debug ()) e
          | Assertion e ->
            Format.fprintf fmt "%a %a" Print.keyword "assert"
              (Print.expr ?debug ()) e))
diff --git a/compiler/shared_ast/definitions.ml b/compiler/shared_ast/definitions.ml
index 0c8fb727..0c75a84b 100644
--- a/compiler/shared_ast/definitions.ml
+++ b/compiler/shared_ast/definitions.ml
@@ -98,7 +98,7 @@ module ScopeVar =
 type scope_var_or_subscope =
   | ScopeVar of ScopeVar.t
   | SubScope of ScopeVar.t * ScopeName.t * bool Mark.pos
-                (* The bool is true if the output of the subscope is to be forwarded *)
+(* The bool is true if the output of the subscope is to be forwarded *)
 
 module StateName =
   Uid.Gen
diff --git a/compiler/shared_ast/expr.ml b/compiler/shared_ast/expr.ml
index 8b7cab32..d59f2108 100644
--- a/compiler/shared_ast/expr.ml
+++ b/compiler/shared_ast/expr.ml
@@ -538,10 +538,10 @@ let compare_location
     (y : a glocation Mark.pos) =
   match Mark.remove x, Mark.remove y with
   | ( DesugaredScopeVar { name = vx; state = sx },
-      DesugaredScopeVar { name = vy; state = sy } ) ->
-    (match Mark.compare ScopeVar.compare vx vy with
-     | 0 -> Option.compare StateName.compare sx sy
-     | n -> n)
+      DesugaredScopeVar { name = vy; state = sy } ) -> (
+    match Mark.compare ScopeVar.compare vx vy with
+    | 0 -> Option.compare StateName.compare sx sy
+    | n -> n)
   | ScopelangScopeVar { name = vx, _ }, ScopelangScopeVar { name = vy, _ } ->
     ScopeVar.compare vx vy
   | ToplevelVar { name = vx, _ }, ToplevelVar { name = vy, _ } ->
diff --git a/compiler/shared_ast/typing.ml b/compiler/shared_ast/typing.ml
index ce2b8bca..9b88cf51 100644
--- a/compiler/shared_ast/typing.ml
+++ b/compiler/shared_ast/typing.ml
@@ -405,7 +405,6 @@ module Env = struct
   let get t v = Var.Map.find_opt v t.vars
   let get_scope_var t sv = A.ScopeVar.Map.find_opt sv t.scope_vars
   let get_toplevel_var t v = A.TopdefName.Map.find_opt v t.toplevel_vars
-
   let add v tau t = { t with vars = Var.Map.add v tau t.vars }
   let add_var v typ t = add v (ast_to_typ typ) t
 
@@ -558,9 +557,7 @@ and typecheck_expr_top_down :
       | Some name -> unionfind (TStruct name)
       | None -> unionfind (TAny (Any.fresh ()))
     in
-    let e_struct' =
-      typecheck_expr_top_down ctx env t_struct e_struct
-    in
+    let e_struct' = typecheck_expr_top_down ctx env t_struct e_struct in
     let name =
       match UnionFind.get (ty e_struct') with
       | TStruct name, _ -> name
@@ -569,8 +566,8 @@ and typecheck_expr_top_down :
           "Disambiguation failed before reaching field %s" field
       | _ ->
         Message.raise_spanned_error (Expr.pos e)
-          "This is not a structure, cannot access field %s (found type: %a)" field
-          (format_typ ctx) (ty e_struct')
+          "This is not a structure, cannot access field %s (found type: %a)"
+          field (format_typ ctx) (ty e_struct')
     in
     let str =
       try A.StructName.Map.find name env.structs
@@ -581,30 +578,43 @@ and typecheck_expr_top_down :
     let field =
       let candidate_structs =
         try A.Ident.Map.find field ctx.ctx_struct_fields
-        with A.Ident.Map.Not_found _ ->
+        with A.Ident.Map.Not_found _ -> (
           match
-            A.ScopeName.Map.choose_opt @@
-            A.ScopeName.Map.filter
-              (fun _ { A.out_struct_name; _ } -> A.StructName.equal out_struct_name name)
-              ctx.ctx_scopes
+            A.ScopeName.Map.choose_opt
+            @@ A.ScopeName.Map.filter
+                 (fun _ { A.out_struct_name; _ } ->
+                   A.StructName.equal out_struct_name name)
+                 ctx.ctx_scopes
           with
           | Some (scope_out, _) ->
             Message.raise_multispanned_error_full
-              [Some (fun ppf -> Format.fprintf ppf "@{<yellow>%s@} is used here as an output" field),
-               Expr.mark_pos context_mark;
-               Some (fun ppf -> Format.fprintf ppf "Scope %a is declared here" A.ScopeName.format scope_out),
-               Mark.get (A.StructName.get_info name)]
+              [
+                ( Some
+                    (fun ppf ->
+                      Format.fprintf ppf
+                        "@{<yellow>%s@} is used here as an output" field),
+                  Expr.mark_pos context_mark );
+                ( Some
+                    (fun ppf ->
+                      Format.fprintf ppf "Scope %a is declared here"
+                        A.ScopeName.format scope_out),
+                  Mark.get (A.StructName.get_info name) );
+              ]
               "Variable @{<yellow>%s@} is not a declared output of scope %a."
               field A.ScopeName.format scope_out
-              ~suggestion:(List.map A.StructField.to_string (A.StructField.Map.keys str))
+              ~suggestion:
+                (List.map A.StructField.to_string (A.StructField.Map.keys str))
           | None ->
             Message.raise_multispanned_error
-              [None, Expr.mark_pos context_mark;
-               Some "Structure definition", Mark.get (A.StructName.get_info name)]
+              [
+                None, Expr.mark_pos context_mark;
+                ( Some "Structure definition",
+                  Mark.get (A.StructName.get_info name) );
+              ]
               "Field @{<yellow>\"%s\"@} does not belong to structure \
                @{<yellow>\"%a\"@}."
               field A.StructName.format name
-              ~suggestion:(A.Ident.Map.keys ctx.ctx_struct_fields)
+              ~suggestion:(A.Ident.Map.keys ctx.ctx_struct_fields))
       in
       try A.StructName.Map.find name candidate_structs
       with A.StructName.Map.Not_found _ ->