-- SPDX-License-Identifier: CC0-1.0
let Test = ./test.dhall ? env:DHALL_GENODE_TEST

let Genode = Test.Genode

let Prelude = Genode.Prelude

let XML = Prelude.XML

let Init = Genode.Init

let Child = Init.Child

let TextMapType = Prelude.Map.Type Text

let Children = TextMapType Child.Type

let Manifest/Type = TextMapType (TextMapType Text)

let Manifest/toRoutes =
        λ(manifest : Manifest/Type)
      → Prelude.List.map
          (Prelude.Map.Entry Text Text)
          Init.ServiceRoute.Type
          (   λ(entry : Prelude.Map.Entry Text Text)
            → { service =
                  { name = "ROM"
                  , label = Init.LabelSelector.Type.Last entry.mapKey
                  }
              , route =
                  Init.Route.Type.Child
                    { name = "store_rom"
                    , label = Some entry.mapValue
                    , diag = None Bool
                    }
              }
          )
          ( Prelude.List.concat
              (Prelude.Map.Entry Text Text)
              (Prelude.Map.values Text (Prelude.Map.Type Text Text) manifest)
          )

let parentROMs =
      Prelude.List.map
        Text
        Init.ServiceRoute.Type
        (   λ(label : Text)
          → { service =
                { name = "ROM", label = Init.LabelSelector.Type.Last label }
            , route =
                Init.Route.Type.Parent { label = Some label, diag = None Bool }
            }
        )

let wrapHarness
    : Children → Manifest/Type → Child.Type
    =   λ(children : Children)
      → λ(manifest : Manifest/Type)
      → Child.nested
          children
          Child.Attributes::{
          , binary = "sotest-harness"
          , exitPropagate = True
          , 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.parent "VM"
                , Init.ServiceRoute.child "Timer" "timer"
                , Init.ServiceRoute.child "Rtc" "rtc"
                , Init.ServiceRoute.child "File_system" "store_fs"
                ]
              # parentROMs
                  [ "ld.lib.so"
                  , "init"
                  , "platform_info"
                  , "core_log"
                  , "kernel_log"
                  , "vfs"
                  , "libvfs.so"
                  , "cached_fs_rom"
                  ]
              # Manifest/toRoutes manifest
          }

in    λ(test : Test.Type)
    → λ(storeSize : Natural)
    → λ(storeManifest : Manifest/Type)
    → λ(bootManifest : Manifest/Type)
    → Genode.Boot::{
      , config = Init::{
        , children =
          [ { mapKey = "timer"
            , mapValue =
                Child.flat
                  Child.Attributes::{
                  , binary = "timer_drv"
                  , provides = [ "Timer" ]
                  }
            }
          , { mapKey = "rtc"
            , mapValue =
                Child.flat
                  Child.Attributes::{
                  , binary = "rtc_drv"
                  , provides = [ "Rtc" ]
                  , routes = [ Init.ServiceRoute.parent "IO_PORT" ]
                  }
            }
          , { mapKey = "store_fs"
            , mapValue =
                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 = "store.tar" }
                                }
                            ]
                          }
                      ]
                    , defaultPolicy = Some Init.Config.DefaultPolicy::{
                      , attributes = toMap { root = "/", writeable = "no" }
                      }
                    }
                  , provides = [ "File_system" ]
                  }
            }
          , { mapKey = "store_rom"
            , mapValue =
                Child.flat
                  Child.Attributes::{
                  , binary = "cached_fs_rom"
                  , provides = [ "ROM" ]
                  , resources = Init.Resources::{
                    , ram = storeSize + Genode.units.MiB 1
                    }
                  , routes =
                    [ Init.ServiceRoute.child "File_system" "store_fs" ]
                  }
            }
          , { mapKey = "harness"
            , mapValue = wrapHarness test.children storeManifest
            }
          ]
        }
      , rom =
            test.rom
          # Genode.BootModules.toRomPaths
              ( Prelude.List.concat
                  (Prelude.Map.Entry Text Text)
                  ( Prelude.Map.values
                      Text
                      (Prelude.Map.Type Text Text)
                      bootManifest
                  )
              )
      }