let Genode = env:DHALL_GENODE

let Prelude = Genode.Prelude

let XML = Prelude.XML

let Init = Genode.Init

let Child = Init.Child

let TextMapType = Prelude.Map.Type Text

let Manifest/Type = TextMapType (TextMapType Text)

in  λ(subinit : Init.Type) →
    λ(storeName : Text) →
    λ(storeSize : Natural) →
    λ(storeRomPolicies : Prelude.Map.Type Text Text) →
    λ(bootManifest : Manifest/Type) →
      Genode.Boot::{
      , config = Init::{
        , children =
            let child = Prelude.Map.keyValue Child.Type

            in  [ child
                    "timer"
                    ( Child.flat
                        Child.Attributes::{
                        , binary = "timer_drv"
                        , provides = [ "Timer" ]
                        }
                    )
                , child
                    "rtc"
                    ( Child.flat
                        Child.Attributes::{
                        , binary = "rtc_drv"
                        , provides = [ "Rtc" ]
                        , routes = [ Init.ServiceRoute.parent "IO_PORT" ]
                        }
                    )
                , child
                    "store_fs"
                    ( Child.flat
                        Child.Attributes::{
                        , binary = "vfs"
                        , config = Init.Config::{
                          , content =
                            [ XML.element
                                { name = "vfs"
                                , attributes = XML.emptyAttributes
                                , content =
                                  [ XML.leaf
                                      { name = "tar"
                                      , attributes = toMap { name = storeName }
                                      }
                                  ]
                                }
                            ]
                          , policies =
                            [ Init.Config.Policy::{
                              , service = "File_system"
                              , label = Init.LabelSelector.suffix "nix-store"
                              , attributes = toMap { root = "/nix/store" }
                              }
                            , Init.Config.Policy::{
                              , service = "File_system"
                              , label = Init.LabelSelector.prefix "store_rom"
                              , attributes = toMap { root = "/" }
                              }
                            ]
                          }
                        , provides = [ "File_system" ]
                        }
                    )
                , child
                    "store_rom"
                    ( Child.flat
                        Child.Attributes::{
                        , binary = "cached_fs_rom"
                        , provides = [ "ROM" ]
                        , resources = Init.Resources::{
                          , ram = storeSize + Genode.units.MiB 1
                          }
                        , config = Init.Config::{
                          , policies =
                                [ Init.Config.Policy::{
                                  , service = "ROM"
                                  , label =
                                      Init.LabelSelector.prefix
                                        "nixos -> /nix/store"
                                  }
                                ]
                              # ( let Entry = Prelude.Map.Entry Text Text

                                  in  Prelude.List.concatMap
                                        Entry
                                        Init.Config.Policy.Type
                                        ( λ(e : Entry) →
                                            [ Init.Config.Policy::{
                                              , service = "ROM"
                                              , label =
                                                  Init.LabelSelector.prefix
                                                    "nixos -> ${e.mapKey}"
                                              , attributes = toMap
                                                  { directory =
                                                      "${e.mapValue}/bin"
                                                  }
                                              }
                                            , Init.Config.Policy::{
                                              , service = "ROM"
                                              , label =
                                                  Init.LabelSelector.Type.Partial
                                                    { prefix = Some
                                                        "nixos -> ${e.mapKey}"
                                                    , suffix = Some ".lib.so"
                                                    }
                                              , attributes = toMap
                                                  { directory =
                                                      "${e.mapValue}/lib"
                                                  }
                                              }
                                            ]
                                        )
                                        storeRomPolicies
                                )
                          }
                        }
                    )
                , child
                    "nixos"
                    ( Init.toChild
                        subinit
                        Init.Attributes::{
                        , exitPropagate = True
                        , resources = Init.Resources::{
                          , ram = Genode.units.MiB 4
                          }
                        , routes =
                            let parentROMs =
                                  Prelude.List.concatMap
                                    Text
                                    Init.ServiceRoute.Type
                                    ( λ(suffix : Text) →
                                        Prelude.List.map
                                          Text
                                          Init.ServiceRoute.Type
                                          ( λ(prefix : Text) →
                                              { service =
                                                { name = "ROM"
                                                , label =
                                                    Init.LabelSelector.Type.Partial
                                                      { prefix = Some prefix
                                                      , suffix = Some suffix
                                                      }
                                                }
                                              , route =
                                                  Init.Route.parent
                                                    (Some suffix)
                                              }
                                          )
                                          ( Prelude.Map.keys
                                              Text
                                              Init.Child.Type
                                              subinit.children
                                          )
                                    )

                            in    parentROMs
                                    [ "ld.lib.so"
                                    , "vfs.lib.so"
                                    , "init"
                                    , "platform_info"
                                    , "core_log"
                                    , "kernel_log"
                                    ]
                                # [ Init.ServiceRoute.parent "IO_MEM"
                                  , Init.ServiceRoute.parent "IO_PORT"
                                  , Init.ServiceRoute.parent "IRQ"
                                  , Init.ServiceRoute.parent "VM"
                                  , Init.ServiceRoute.child "Timer" "timer"
                                  , Init.ServiceRoute.child "Rtc" "rtc"
                                  ]
                        }
                    )
                ]
        }
      , rom =
          Genode.BootModules.toRomPaths
            ( Prelude.List.concat
                (Prelude.Map.Entry Text Text)
                ( Prelude.Map.values
                    Text
                    (Prelude.Map.Type Text Text)
                    bootManifest
                )
            )
      }