Remove the type sv_kind ("symbolic value kind")

8 files changed, 63 insertions, 158 deletions

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index 4ecafd31..76432faa 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -206,7 +206,7 @@ let initialize_symbolic_context_for_fun (ctx : decls_ctx) (fdef : fun_decl) :
   in
   (* Create fresh symbolic values for the inputs *)
   let input_svs =
-    List.map (fun ty -> mk_fresh_symbolic_value SynthInput ty) inst_sg.inputs
+    List.map (fun ty -> mk_fresh_symbolic_value ty) inst_sg.inputs
   in
   (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
   let call_id = fresh_fun_call_id () in
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 6a7ac095..19b9fd3b 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -444,13 +444,6 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t)
     (ctx : eval_ctx) : eval_ctx =
   (* Sanity checks *)
   assert (sv.sv_id <> nsv.sv_id && ty_is_rty proj_ty);
-  (match nsv.sv_kind with
-  | SynthInputGivenBack | SynthRetGivenBack | FunCallGivenBack | LoopGivenBack
-    ->
-      ()
-  | FunCallRet | SynthInput | Global | KindConstGeneric | LoopOutput | LoopJoin
-  | Aggregate | ConstGeneric | TraitConst ->
-      raise (Failure "Unreachable"));
   (* Store the given-back value as a meta-value for synthesis purposes *)
   let mv = nsv in
   (* Substitution function, to replace the borrow projectors over symbolic values *)
@@ -459,31 +452,20 @@ let give_back_symbolic_value (_config : config) (proj_regions : RegionId.Set.t)
     let _ = raise Utils.Unimplemented in
     (* Compute the projection over the given back value *)
     let child_proj =
-      match nsv.sv_kind with
-      | SynthRetGivenBack ->
-          (* The given back value comes from the return value of the function
-             we are currently synthesizing (as it is given back, it means
-             we ended one of the regions appearing in the signature: we are
-             currently synthesizing one of the backward functions).
-
-             As we don't allow borrow overwrites on returned value, we can
-             (and MUST) forget the borrows *)
-          AIgnoredProjBorrows
-      | FunCallGivenBack ->
-          (* TODO: there is something wrong here.
-             Consider this:
-             {[
-               abs0 {'a} { AProjLoans (s0 : &'a mut T) [] }
-               abs1 {'b} { AProjBorrows (s0 : &'a mut T <: &'b mut T) }
-             ]}
-
-             Upon ending abs1, we give back some fresh symbolic value [s1],
-             that we reinsert where the loan for [s0] is. However, the mutable
-             borrow in the type [&'a mut T] was ended: we give back a value of
-             type [T]! We thus *mustn't* introduce a projector here.
-          *)
-          AProjBorrows (nsv, sv.sv_ty)
-      | _ -> raise (Failure "Unreachable")
+      (* TODO: there is something wrong here.
+         Consider this:
+         {[
+           abs0 {'a} { AProjLoans (s0 : &'a mut T) [] }
+           abs1 {'b} { AProjBorrows (s0 : &'a mut T <: &'b mut T) }
+         ]}
+
+         Upon ending abs1, we give back some fresh symbolic value [s1],
+         that we reinsert where the loan for [s0] is. However, the mutable
+         borrow in the type [&'a mut T] was ended: we give back a value of
+         type [T]! We thus *mustn't* introduce a projector here.
+      *)
+      (* AProjBorrows (nsv, sv.sv_ty) *)
+      raise (Failure "TODO")
     in
     AProjLoans (sv, (mv, child_proj) :: local_given_back)
   in
@@ -739,17 +721,7 @@ let reborrow_shared (original_bid : BorrowId.id) (new_bid : BorrowId.id)
  *)
 let convert_avalue_to_given_back_value (abs_kind : abs_kind) (av : typed_avalue)
     : symbolic_value =
-  let sv_kind =
-    match abs_kind with
-    | FunCall _ -> FunCallGivenBack
-    | SynthRet _ -> SynthRetGivenBack
-    | SynthInput _ -> SynthInputGivenBack
-    | Loop _ -> LoopGivenBack
-    | Identity ->
-        (* Identity abstractions give back nothing *)
-        raise (Failure "Unreachable")
-  in
-  mk_fresh_symbolic_value sv_kind av.ty
+  mk_fresh_symbolic_value av.ty
 
 (** Auxiliary function: see {!end_borrow_aux}.
 
@@ -1239,7 +1211,7 @@ and end_abstraction_borrows (config : config) (chain : borrow_or_abs_ids)
           ("end_abstraction_borrows: found aproj borrows: "
           ^ aproj_to_string ctx (AProjBorrows (sv, proj_ty))));
       (* Generate a fresh symbolic value *)
-      let nsv = mk_fresh_symbolic_value FunCallGivenBack proj_ty in
+      let nsv = mk_fresh_symbolic_value proj_ty in
       (* Replace the proj_borrows - there should be exactly one *)
       let ended_borrow = AEndedProjBorrows nsv in
       let ctx = update_aproj_borrows abs.abs_id sv ended_borrow ctx in
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index d7f5fcd5..bbf4d9d5 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -209,8 +209,8 @@ let apply_symbolic_expansion_non_borrow (config : config)
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
 let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
-    (kind : sv_kind) (def_id : TypeDeclId.id) (generics : generic_args)
-    (ctx : eval_ctx) : symbolic_expansion list =
+    (def_id : TypeDeclId.id) (generics : generic_args) (ctx : eval_ctx) :
+    symbolic_expansion list =
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
   let def = ctx_lookup_type_decl ctx def_id in
@@ -227,7 +227,7 @@ let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
   let initialize ((variant_id, field_types) : VariantId.id option * rty list) :
       symbolic_expansion =
     let field_values =
-      List.map (fun (ty : rty) -> mk_fresh_symbolic_value kind ty) field_types
+      List.map (fun (ty : rty) -> mk_fresh_symbolic_value ty) field_types
     in
     let see = SeAdt (variant_id, field_values) in
     see
@@ -235,20 +235,19 @@ let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
   (* Initialize all the expanded values of all the variants *)
   List.map initialize variants_fields_types
 
-let compute_expanded_symbolic_tuple_value (kind : sv_kind)
-    (field_types : rty list) : symbolic_expansion =
+let compute_expanded_symbolic_tuple_value (field_types : rty list) :
+    symbolic_expansion =
   (* Generate the field values *)
   let field_values =
-    List.map (fun sv_ty -> mk_fresh_symbolic_value kind sv_ty) field_types
+    List.map (fun sv_ty -> mk_fresh_symbolic_value sv_ty) field_types
   in
   let variant_id = None in
   let see = SeAdt (variant_id, field_values) in
   see
 
-let compute_expanded_symbolic_box_value (kind : sv_kind) (boxed_ty : rty) :
-    symbolic_expansion =
+let compute_expanded_symbolic_box_value (boxed_ty : rty) : symbolic_expansion =
   (* Introduce a fresh symbolic value *)
-  let boxed_value = mk_fresh_symbolic_value kind boxed_ty in
+  let boxed_value = mk_fresh_symbolic_value boxed_ty in
   let see = SeAdt (None, [ boxed_value ]) in
   see
 
@@ -262,16 +261,15 @@ let compute_expanded_symbolic_box_value (kind : sv_kind) (boxed_ty : rty) :
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
 let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
-    (kind : sv_kind) (adt_id : type_id) (generics : generic_args)
-    (ctx : eval_ctx) : symbolic_expansion list =
+    (adt_id : type_id) (generics : generic_args) (ctx : eval_ctx) :
+    symbolic_expansion list =
   match (adt_id, generics.regions, generics.types) with
   | TAdtId def_id, _, _ ->
-      compute_expanded_symbolic_non_assumed_adt_value expand_enumerations kind
-        def_id generics ctx
-  | TTuple, [], _ ->
-      [ compute_expanded_symbolic_tuple_value kind generics.types ]
+      compute_expanded_symbolic_non_assumed_adt_value expand_enumerations def_id
+        generics ctx
+  | TTuple, [], _ -> [ compute_expanded_symbolic_tuple_value generics.types ]
   | TAssumed TBox, [], [ boxed_ty ] ->
-      [ compute_expanded_symbolic_box_value kind boxed_ty ]
+      [ compute_expanded_symbolic_box_value boxed_ty ]
   | _ ->
       raise
         (Failure "compute_expanded_symbolic_adt_value: unexpected combination")
@@ -313,7 +311,7 @@ let expand_symbolic_value_shared_borrow (config : config)
     else None
   in
   (* The fresh symbolic value for the shared value *)
-  let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
+  let shared_sv = mk_fresh_symbolic_value ref_ty in
   (* Visitor to replace the projectors on borrows *)
   let obj =
     object (self)
@@ -403,7 +401,7 @@ let expand_symbolic_value_borrow (config : config)
   | RMut ->
       (* Simple case: simply create a fresh symbolic value and a fresh
        * borrow id *)
-      let sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
+      let sv = mk_fresh_symbolic_value ref_ty in
       let bid = fresh_borrow_id () in
       let see = SeMutRef (bid, sv) in
       (* Expand the symbolic values - we simply perform a substitution (and
@@ -524,8 +522,8 @@ let expand_symbolic_value_no_branching (config : config) (sv : symbolic_value)
         (* Compute the expanded value *)
         let allow_branching = false in
         let seel =
-          compute_expanded_symbolic_adt_value allow_branching sv.sv_kind adt_id
-            generics ctx
+          compute_expanded_symbolic_adt_value allow_branching adt_id generics
+            ctx
         in
         (* There should be exacly one branch *)
         let see = Collections.List.to_cons_nil seel in
@@ -581,8 +579,7 @@ let expand_symbolic_adt (config : config) (sv : symbolic_value)
       let allow_branching = true in
       (* Compute the expanded value *)
       let seel =
-        compute_expanded_symbolic_adt_value allow_branching sv.sv_kind adt_id
-          generics ctx
+        compute_expanded_symbolic_adt_value allow_branching adt_id generics ctx
       in
       (* Apply *)
       let seel = List.map (fun see -> (Some see, cf_branches)) seel in
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index af545fb9..9f117933 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -283,7 +283,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
                 List.find (fun (name, _) -> name = const_name) trait_decl.consts
               in
               (* Introduce a fresh symbolic value *)
-              let v = mk_fresh_symbolic_typed_value TraitConst ty in
+              let v = mk_fresh_symbolic_typed_value ty in
               (* Continue the evaluation *)
               let e = cf v ctx in
               (* We have to wrap the generated expression *)
@@ -315,7 +315,7 @@ let eval_operand_no_reorganize (config : config) (op : operand)
                 copy_value allow_adt_copy config ctx cv
             | SymbolicMode ->
                 (* We use the looked up value only for its type *)
-                let v = mk_fresh_symbolic_typed_value KindConstGeneric cv.ty in
+                let v = mk_fresh_symbolic_typed_value cv.ty in
                 (ctx, v)
           in
           (* Continue *)
@@ -464,9 +464,7 @@ let eval_unary_op_symbolic (config : config) (unop : unop) (op : operand)
       | Cast (CastInteger (_, tgt_ty)), _ -> TLiteral (TInteger tgt_ty)
       | _ -> raise (Failure "Invalid input for unop")
     in
-    let res_sv =
-      { sv_kind = FunCallRet; sv_id = res_sv_id; sv_ty = res_sv_ty }
-    in
+    let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
     (* Call the continuation *)
     let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in
     (* Synthesize the symbolic AST *)
@@ -603,9 +601,7 @@ let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand)
             | Ne | Eq -> raise (Failure "Unreachable"))
         | _ -> raise (Failure "Invalid inputs for binop")
     in
-    let res_sv =
-      { sv_kind = FunCallRet; sv_id = res_sv_id; sv_ty = res_sv_ty }
-    in
+    let res_sv = { sv_id = res_sv_id; sv_ty = res_sv_ty } in
     (* Call the continuattion *)
     let v = mk_typed_value_from_symbolic_value res_sv in
     let expr = cf (Ok v) ctx in
@@ -769,7 +765,7 @@ let eval_rvalue_aggregate (config : config) (aggregate_kind : aggregate_kind)
            array we introduce here might be duplicated in the generated
            code: by introducing a symbolic value we introduce a let-binding
            in the generated code. *)
-        let saggregated = mk_fresh_symbolic_typed_value Aggregate ty in
+        let saggregated = mk_fresh_symbolic_typed_value ty in
         (* Call the continuation *)
         match cf saggregated ctx with
         | None -> None
diff --git a/compiler/InterpreterLoopsMatchCtxs.ml b/compiler/InterpreterLoopsMatchCtxs.ml
index c21dab71..90559c29 100644
--- a/compiler/InterpreterLoopsMatchCtxs.ml
+++ b/compiler/InterpreterLoopsMatchCtxs.ml
@@ -389,7 +389,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
 
   let match_distinct_literals (ty : ety) (_ : literal) (_ : literal) :
       typed_value =
-    mk_fresh_symbolic_typed_value_from_no_regions_ty LoopJoin ty
+    mk_fresh_symbolic_typed_value_from_no_regions_ty ty
 
   let match_distinct_adts (ty : ety) (adt0 : adt_value) (adt1 : adt_value) :
       typed_value =
@@ -418,7 +418,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
     check_loans false adt1.field_values;
 
     (* No borrows, no loans: we can introduce a symbolic value *)
-    mk_fresh_symbolic_typed_value_from_no_regions_ty LoopJoin ty
+    mk_fresh_symbolic_typed_value_from_no_regions_ty ty
 
   let match_shared_borrows _ (ty : ety) (bid0 : borrow_id) (bid1 : borrow_id) :
       borrow_id =
@@ -435,9 +435,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
 
       (* Generate a fresh symbolic value for the shared value *)
       let _, bv_ty, kind = ty_as_ref ty in
-      let sv =
-        mk_fresh_symbolic_typed_value_from_no_regions_ty LoopJoin bv_ty
-      in
+      let sv = mk_fresh_symbolic_typed_value_from_no_regions_ty bv_ty in
 
       let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
 
@@ -582,9 +580,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
 
       (* Generate a fresh symbolic value for the borrowed value *)
       let _, bv_ty, kind = ty_as_ref ty in
-      let sv =
-        mk_fresh_symbolic_typed_value_from_no_regions_ty LoopJoin bv_ty
-      in
+      let sv = mk_fresh_symbolic_typed_value_from_no_regions_ty bv_ty in
 
       let borrow_ty = mk_ref_ty (RFVar rid) bv_ty kind in
 
@@ -664,7 +660,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
          borrows *)
       assert (not (ty_has_borrows S.ctx.type_context.type_infos sv0.sv_ty));
       (* We simply introduce a fresh symbolic value *)
-      mk_fresh_symbolic_value LoopJoin sv0.sv_ty)
+      mk_fresh_symbolic_value sv0.sv_ty)
 
   let match_symbolic_with_other (left : bool) (sv : symbolic_value)
       (v : typed_value) : typed_value =
@@ -685,7 +681,7 @@ module MakeJoinMatcher (S : MatchJoinState) : PrimMatcher = struct
         if value_is_left then raise (ValueMatchFailure (LoanInLeft id))
         else raise (ValueMatchFailure (LoanInRight id)));
     (* Return a fresh symbolic value *)
-    mk_fresh_symbolic_typed_value LoopJoin sv.sv_ty
+    mk_fresh_symbolic_typed_value sv.sv_ty
 
   let match_bottom_with_other (left : bool) (v : typed_value) : typed_value =
     (* If there are outer loans in the non-bottom value, raise an exception.
@@ -834,7 +830,7 @@ struct
 
   let match_distinct_literals (ty : ety) (_ : literal) (_ : literal) :
       typed_value =
-    mk_fresh_symbolic_typed_value_from_no_regions_ty LoopJoin ty
+    mk_fresh_symbolic_typed_value_from_no_regions_ty ty
 
   let match_distinct_adts (_ty : ety) (_adt0 : adt_value) (_adt1 : adt_value) :
       typed_value =
@@ -904,11 +900,7 @@ struct
         GetSetSid.match_e "match_symbolic_values: ids: " S.sid_map id0 id1
       in
       let sv_ty = match_rtys sv0.sv_ty sv1.sv_ty in
-      let sv_kind =
-        if sv0.sv_kind = sv1.sv_kind then sv0.sv_kind
-        else raise (Distinct "match_symbolic_values: sv_kind")
-      in
-      let sv = { sv_id; sv_ty; sv_kind } in
+      let sv = { sv_id; sv_ty } in
       sv
     else (
       (* Check: fixed values are fixed *)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 437b358a..66b8492a 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1008,7 +1008,7 @@ and eval_global (config : config) (dest : place) (gid : GlobalDeclId.id) :
       (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
        * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
       assert (ty_no_regions global.ty);
-      let sval = mk_fresh_symbolic_value Global global.ty in
+      let sval = mk_fresh_symbolic_value global.ty in
       let cc =
         assign_to_place config (mk_typed_value_from_symbolic_value sval) dest
       in
@@ -1312,7 +1312,7 @@ and eval_function_call_symbolic_from_inst_sig (config : config)
 
   (* Generate a fresh symbolic value for the return value *)
   let ret_sv_ty = inst_sg.output in
-  let ret_spc = mk_fresh_symbolic_value FunCallRet ret_sv_ty in
+  let ret_spc = mk_fresh_symbolic_value ret_sv_ty in
   let ret_value = mk_typed_value_from_symbolic_value ret_spc in
   let ret_av regions =
     mk_aproj_loans_value_from_symbolic_value regions ret_spc
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index d3f8f4fa..e04a6b90 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -74,31 +74,29 @@ let mk_place_from_var_id (var_id : VarId.id) : place =
   { var_id; projection = [] }
 
 (** Create a fresh symbolic value *)
-let mk_fresh_symbolic_value (sv_kind : sv_kind) (ty : ty) : symbolic_value =
+let mk_fresh_symbolic_value (ty : ty) : symbolic_value =
   (* Sanity check *)
   assert (ty_is_rty ty);
   let sv_id = fresh_symbolic_value_id () in
-  let svalue = { sv_kind; sv_id; sv_ty = ty } in
+  let svalue = { sv_id; sv_ty = ty } in
   svalue
 
-let mk_fresh_symbolic_value_from_no_regions_ty (sv_kind : sv_kind) (ty : ty) :
-    symbolic_value =
+let mk_fresh_symbolic_value_from_no_regions_ty (ty : ty) : symbolic_value =
   assert (ty_no_regions ty);
-  mk_fresh_symbolic_value sv_kind ty
+  mk_fresh_symbolic_value ty
 
 (** Create a fresh symbolic value *)
-let mk_fresh_symbolic_typed_value (sv_kind : sv_kind) (rty : ty) : typed_value =
+let mk_fresh_symbolic_typed_value (rty : ty) : typed_value =
   assert (ty_is_rty rty);
   let ty = Substitute.erase_regions rty in
   (* Generate the fresh a symbolic value *)
-  let value = mk_fresh_symbolic_value sv_kind rty in
+  let value = mk_fresh_symbolic_value rty in
   let value = VSymbolic value in
   { value; ty }
 
-let mk_fresh_symbolic_typed_value_from_no_regions_ty (sv_kind : sv_kind)
-    (ty : ty) : typed_value =
+let mk_fresh_symbolic_typed_value_from_no_regions_ty (ty : ty) : typed_value =
   assert (ty_no_regions ty);
-  mk_fresh_symbolic_typed_value sv_kind ty
+  mk_fresh_symbolic_typed_value ty
 
 (** Create a typed value from a symbolic value. *)
 let mk_typed_value_from_symbolic_value (svalue : symbolic_value) : typed_value =
@@ -267,15 +265,9 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : eval_ctx)
       inherit [_] iter_typed_value
 
       method! visit_symbolic_value _ s =
-        match s.sv_kind with
-        | FunCallRet | LoopOutput | LoopJoin ->
-            if ty_has_borrow_under_mut ctx.type_context.type_infos s.sv_ty then
-              raise Found
-            else ()
-        | SynthInput | SynthInputGivenBack | FunCallGivenBack
-        | SynthRetGivenBack | Global | KindConstGeneric | LoopGivenBack
-        | Aggregate | ConstGeneric | TraitConst ->
-            ()
+        if ty_has_borrow_under_mut ctx.type_context.type_infos s.sv_ty then
+          raise Found
+        else ()
     end
   in
   (* We use exceptions *)
@@ -430,7 +422,7 @@ let initialize_eval_context (ctx : decls_ctx)
       (List.map
          (fun (cg : const_generic_var) ->
            let ty = TLiteral cg.ty in
-           let cv = mk_fresh_symbolic_typed_value ConstGeneric ty in
+           let cv = mk_fresh_symbolic_typed_value ty in
            (cg.index, cv))
          const_generic_vars)
   in
diff --git a/compiler/Values.ml b/compiler/Values.ml
index 60cbcc8b..5473ce3e 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -15,47 +15,6 @@ module LoopId = IdGen ()
 type symbolic_value_id = SymbolicValueId.id [@@deriving show, ord]
 type symbolic_value_id_set = SymbolicValueId.Set.t [@@deriving show, ord]
 type loop_id = LoopId.id [@@deriving show, ord]
-
-(** The kind of a symbolic value, which precises how the value was generated.
-
-    TODO: remove? This is not useful anymore.
-  *)
-type sv_kind =
-  | FunCallRet  (** The value is the return value of a function call *)
-  | FunCallGivenBack
-      (** The value is a borrowed value given back by an abstraction
-          (happens when giving a borrow to a function: when the abstraction
-          introduced to model the function call ends we reintroduce a symbolic
-          value in the context for the value modified by the abstraction through
-          the borrow).
-       *)
-  | SynthInput
-      (** The value is an input value of the function whose body we are
-          currently synthesizing.
-       *)
-  | SynthRetGivenBack
-      (** The value is a borrowed value that the function whose body we are
-          synthesizing returned, and which was given back because we ended
-          one of the lifetimes of this function (we do this to synthesize
-          the backward functions).
-       *)
-  | SynthInputGivenBack
-      (** The value was given back upon ending one of the input abstractions *)
-  | Global  (** The value is a global *)
-  | KindConstGeneric  (** The value is a const generic *)
-  | LoopOutput  (** The output of a loop (seen as a forward computation) *)
-  | LoopGivenBack
-      (** A value given back by a loop (when ending abstractions while going backwards) *)
-  | LoopJoin
-      (** The result of a loop join (when computing loop fixed points) *)
-  | Aggregate
-      (** A symbolic value we introduce in place of an aggregate value *)
-  | ConstGeneric
-      (** A symbolic value we introduce when using a const generic as a value *)
-  | TraitConst
-      (** A symbolic value we introduce when evaluating a trait associated constant *)
-[@@deriving show, ord]
-
 type borrow_id = BorrowId.id [@@deriving show, ord]
 type borrow_id_set = BorrowId.Set.t [@@deriving show, ord]
 type loan_id = BorrowId.id [@@deriving show, ord]
@@ -65,7 +24,6 @@ type loan_id_set = BorrowId.Set.t [@@deriving show, ord]
 class ['self] iter_typed_value_base =
   object (self : 'self)
     inherit [_] iter_ty
-    method visit_sv_kind : 'env -> sv_kind -> unit = fun _ _ -> ()
 
     method visit_symbolic_value_id : 'env -> symbolic_value_id -> unit =
       fun _ _ -> ()
@@ -85,7 +43,6 @@ class ['self] iter_typed_value_base =
 class ['self] map_typed_value_base =
   object (self : 'self)
     inherit [_] map_ty
-    method visit_sv_kind : 'env -> sv_kind -> sv_kind = fun _ x -> x
 
     method visit_symbolic_value_id
         : 'env -> symbolic_value_id -> symbolic_value_id =
@@ -104,7 +61,6 @@ class ['self] map_typed_value_base =
 
 (** A symbolic value *)
 type symbolic_value = {
-  sv_kind : sv_kind;
   sv_id : symbolic_value_id;
   sv_ty : ty;  (** This should be a type with regions *)
 }