val apply_introduced_initializer (init: initializer_t) (mem: Armada.Memory.t) : GTot Armada.Memory.t
val apply_introduced_initializer (init: initializer_t) (mem: Armada.Memory.t) : GTot Armada.Memory.t
let apply_introduced_initializer
  (init: initializer_t)
  (mem: Armada.Memory.t)
  : GTot Armada.Memory.t =
  match init.iv with
  | InitializerSpecific value ->
      (match value with
       | ObjectValuePrimitive _
       | ObjectValueAbstract _ _ ->
           let root_id = RootIdGlobal init.var_id in
           let storage = object_value_to_storage value in
           let root = RootGlobal storage in
           Spec.Map.upd mem root_id root
       | _ -> mem)
  | _ -> mem
module Strategies.VarIntro.Initialization

open Armada.Base
open Armada.Init
open Armada.Memory
open Armada.Type
open Spec.List
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.GlobalVars
open Strategies.GlobalVars.Types
open Strategies.VarIntro.Defs
/
Strategies.VarIntro.Defs.fst.checked Strategies.GlobalVars.Types.fst.checked Strategies.GlobalVars.fst.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Base.fst.checked
Strategies.VarIntro.Initialization.fsti
init: Armada.Init.initializer_t -> mem: Armada.Memory.t -> Prims.GTot Armada.Memory.t
Armada.Init.initializer_t Armada.Memory.t Armada.Init.__proj__Mkinitializer_t__item__iv Armada.Type.object_value_t Armada.Type.primitive_box_t Spec.Map.upd Armada.Base.root_id_t Armada.Memory.root_t Armada.Memory.RootGlobal Armada.Memory.object_storage_t Armada.Memory.object_value_to_storage Armada.Base.RootIdGlobal Armada.Init.__proj__Mkinitializer_t__item__var_id Armada.Init.initializer_value_t
let apply_introduced_initializer (init: initializer_t) (mem: Armada.Memory.t) : GTot Armada.Memory.t =
  
match init.iv with
| InitializerSpecific value ->
  (match value with
    | ObjectValuePrimitive _
    | ObjectValueAbstract _ _ ->
      let root_id = RootIdGlobal init.var_id in
      let storage = object_value_to_storage value in
      let root = RootGlobal storage in
      Spec.Map.upd mem root_id root
    | _ -> mem)
| _ -> mem