{ config, pkgs, lib, modulesPath, ... }:

with lib;
let localPackages = pkgs.buildPackages;
in {
  options.genode = {
    core = {

      prefix = mkOption {
        type = types.str;
        example = "hw-pc-";
      };

      supportedSystems = mkOption {
        type = types.listOf types.str;
        example = [ "i686-genode" "x86_64-genode" ];
      };

      basePackages = mkOption { type = types.listOf types.package; };

    };

    boot = {

      kernel = mkOption {
        type = types.path;
        default = "${pkgs.genodePackages.bender}/bender";
      };

      initrd = mkOption {
        type = types.str;
        default = "${pkgs.genodePackages.bender}/bender";
        description = "Path to an image or a command-line arguments";
      };

      configFile = mkOption {
        type = types.path;
        description = ''
          Dhall boot configuration. See
          https://git.sr.ht/~ehmry/dhall-genode/tree/master/Boot/package.dhall
        '';
      };

      image = mkOption {
        type = types.path;
        description =
          "Boot image containing the base component binaries and configuration.";
      };

      romModules = mkOption {
        type = types.attrsOf types.path;
        description = "Attr set of initial ROM modules";
      };

    };

  };

  config = let

    addManifest = drv:
      drv // {
        manifest =
          localPackages.runCommand "${drv.name}.dhall" { inherit drv; } ''
            set -eu
            echo -n '[' >> $out
            find $drv/ -type f -printf ',{mapKey= "%f",mapValue="%p"}' >> $out
            ${if builtins.elem "lib" drv.outputs then
              ''
                find ${drv.lib}/ -type f -printf ',{mapKey= "%f",mapValue="%p"}' >> $out''
            else
              ""}
            echo -n ']' >> $out
          '';
      };

    mergeManifests = inputs:
      localPackages.writeTextFile {
        name = "manifest.dhall";
        text = with builtins;
          let
            f = head: input:
              if hasAttr "manifest" input then
                ''
                  ${head}, { mapKey = "${
                    lib.getName input
                  }", mapValue = ${input.manifest} }''
              else
                abort "${input.pname} does not have a manifest";
          in (foldl' f "[" inputs) + "]";
      };

    romDirectories = filterAttrs (_: value: value != null) (mapAttrs
      (name: value:
        if value.inputs == [ ] then
          null
        else
          pkgs.symlinkJoin {
            name = "${name}-rom";
            paths = value.inputs;
          }) config.genode.init.children);

  in {

    assertions = [{
      assertion = builtins.any (s: s == config.nixpkgs.system)
        config.genode.core.supportedSystems;
      message = "invalid Genode core for this system";
    }];

    genode.boot.configFile = let
      tarball =
        "${config.system.build.tarball}/tarball/${config.system.build.tarball.fileName}.tar";
      manifest = mergeManifests (map addManifest
        (config.genode.core.basePackages ++ [ config.system.build.tarball ]
          ++ (with pkgs.genodePackages; [
            init
            cached_fs_rom
            jitter_sponge
            report_rom
            vfs
          ])));

      storeRomPolicies = mapAttrsToList
        (name: value: '', { mapKey = "${name}", mapValue = "${value}" }'')
        romDirectories;

      extraRoutes = lib.concatStringsSep ", " (lib.lists.flatten
        (lib.mapAttrsToList (name: value:
          map (suffix: ''
            { service =
              { name = "ROM"
              , label =
                  Genode.Init.LabelSelector.Type.Partial
                    { prefix = Some "nixos -> ${name}", suffix = Some "${suffix}" }
              }
            , route = Genode.Init.Route.parent (Some "${suffix}")
            }
          '') value.coreROMs) config.genode.init.children));

    in localPackages.runCommand "boot.dhall" { } ''
      cat > $out << EOF
      let Genode = env:DHALL_GENODE in
      ${./store-wrapper.dhall}
      (${config.genode.init.configFile})
      "${config.system.build.tarball.fileName}.tar"
      $(stat --format '%s' ${tarball})
      ([${toString storeRomPolicies} ] : Genode.Prelude.Map.Type Text Text)
      ([${extraRoutes} ] : List Genode.Init.ServiceRoute.Type)
      ${manifest}
      EOF
    '';

    # Create the tarball of the store to live in core ROM
    system.build.tarball =
      pkgs.callPackage "${modulesPath}/../lib/make-system-tarball.nix" {
        contents = [ ];
        storeContents = let
          romDirs = mapAttrsToList (name: object: {
            symlink = "rom/${name}";
            inherit object;
          }) romDirectories;
          configFiles = mapAttrsToList (name: child: {
            symlink = "config/${name}.dhall";
            object = child.configFile;
          }) config.genode.init.children;
        in romDirs ++ configFiles;
        compressCommand = "cat";
        compressionExtension = "";
      };

    system.build.initXml = pkgs.buildPackages.runCommand "init.xml" {
      nativeBuildInputs = with pkgs.buildPackages; [ dhall xorg.lndir libxml2 ];
      DHALL_GENODE = "${pkgs.genodePackages.dhallGenode}/binary.dhall";
    } ''
      export XDG_CACHE_HOME=$NIX_BUILD_TOP
      lndir -silent \
        ${pkgs.genodePackages.dhallGenode}/.cache \
        $XDG_CACHE_HOME
      dhall text <<< "(env:DHALL_GENODE).Init.render (${config.genode.boot.configFile}).config" > $out
      xmllint --noout $out
    '';

  };

}