-- SPDX-License-Identifier: CC0-1.0

let Genode = env:DHALL_GENODE

let Prelude = Genode.Prelude

let ChildEntry = Prelude.Map.Entry Text Genode.Init.Start.Type

let toChildEntry =
        λ(init : Genode.Init.Type)
      → let childCount = Prelude.List.length ChildEntry init.children
        
        let onlyChild = Prelude.Natural.lessThan childCount 2
        
        let child =
                    if onlyChild
              
              then  Prelude.Optional.fold
                      ChildEntry
                      (Prelude.List.head ChildEntry init.children)
                      ChildEntry
                      (λ(child : ChildEntry) → child)
                      { mapKey = ""
                      , mapValue = Genode.Init.Start::{ binary = "" }
                      }
              
              else  { mapKey = "init", mapValue = Genode.Init.toStart init }
        
        in  child

in    λ(boot : Genode.Boot.Type)
    → let child = toChildEntry boot.config
      
      in  { config =
              Genode.Init::{
              , defaultRoutes =
                    Genode.Init.default.defaultRoutes
                  # [ Genode.ServiceRoute.parent "IO_MEM"
                    , Genode.ServiceRoute.parent "IO_PORT"
                    , Genode.ServiceRoute.parent "IRQ"
                    , Genode.ServiceRoute.child "Timer" "timer"
                    ]
              , children =
                  [ { mapKey = "timer"
                    , mapValue =
                        Genode.Init.Start::{
                        , binary = "hw_timer_drv"
                        , resources = { caps = 96, ram = Genode.units.MiB 1 }
                        , provides = [ "Timer" ]
                        }
                    }
                  , { mapKey = "harness"
                    , mapValue =
                        Genode.Init.Start::{
                        , binary = "sotest-harness"
                        , exitPropagate = True
                        , resources =
                            { caps = child.mapValue.resources.caps + 128
                            , ram =
                                  child.mapValue.resources.ram
                                + Genode.units.MiB 1
                            }
                        , config =
                            Some
                              ( Prelude.XML.element
                                  { name = "config"
                                  , attributes = Prelude.XML.emptyAttributes
                                  , content =
                                      [ Genode.Init.Start.toXML
                                          child.mapKey
                                          child.mapValue
                                      ]
                                  }
                              )
                        , routes =
                            [ Genode.ServiceRoute.parentLabel
                                "LOG"
                                (Some "SOTEST")
                                (Some "unlabeled")
                            ]
                        }
                    }
                  ]
              }
          , rom =
              let manifest = env:MANIFEST
              
              in    Genode.Boot.toRomPaths
                      [ manifest.base-hw-pc.lib.ld
                      , manifest.base-hw-pc.bin.hw_timer_drv
                      , manifest.os.bin.init
                      , manifest.sotest-producer.bin.sotest-harness
                      ]
                  # boot.rom
          }