-- SPDX-License-Identifier: CC0-1.0

let Genode = env:DHALL_GENODE

let Prelude = Genode.Prelude

let Init = Genode.Init

let Child = Init.Child

let wrapHarness
    : Init.Type → Child.Type
    =   λ(init : Init.Type)
      → Child.nested
          (toMap { init = Genode.Init.toChild init Init.Attributes.default })
          Child.Attributes::{
          , binary = "sotest-harness"
          , resources = Init.Resources::{ ram = Genode.units.MiB 4 }
          , routes =
              [ Init.ServiceRoute.parentLabel
                  "LOG"
                  (Some "SOTEST")
                  (Some "unlabeled")
              , Init.ServiceRoute.parent "IO_MEM"
              , Init.ServiceRoute.parent "IO_PORT"
              , Init.ServiceRoute.parent "IRQ"
              , Init.ServiceRoute.child "Timer" "timer"
              ]
          }

let TextMapType = Prelude.Map.Type Text

in    λ(boot : Genode.Boot.Type)
    → λ(inputsManifest : TextMapType (TextMapType Text))
    →   boot
      ⫽ { config =
            Init::{
            , children =
                [ { mapKey = "timer"
                  , mapValue =
                      Child.flat
                        Child.Attributes::{
                        , binary = "timer_drv"
                        , provides = [ "Timer" ]
                        }
                  }
                , { mapKey = "harness", mapValue = wrapHarness boot.config }
                ]
            }
        , rom =
            let inputRoms =
                  Genode.BootModules.toRomPaths
                    ( Prelude.List.concat
                        (Prelude.Map.Entry Text Text)
                        ( Prelude.Map.values
                            Text
                            (Prelude.Map.Type Text Text)
                            inputsManifest
                        )
                    )
            
            in  boot.rom # inputRoms
        }