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

with lib;

{
  options = {

    networking.interfaces = lib.mkOption {
      type = with types;
        attrsOf (submodule ({ ... }: {
          options.genode = {

            driver = mkOption {
              type = types.enum [ "ipxe" "virtio" ];
              description = "Nic driver to use for this interface.";
            };

            stack = mkOption {
              type = with types; nullOr (enum [ "lwip" "lxip" ]);
              default = "lwip";
              description = "IP stack to use for this interface.";
            };

          };
        }));
    };

    hardware.genode.platform.policies = lib.mkOption {
      type = with types; listOf path;
      default = [ ];
      description = ''
        List of policies to append to the Genode platform driver.
        Type is Init.Config.Policy.Type.
      '';
    };

    hardware.genode = {

      ahci.enable = lib.mkEnableOption "AHCI (SATA) block driver";

      framebuffer = {
        enable = lib.mkEnableOption "framebuffer driver";
        driver = mkOption {
          type = types.enum [ "boot" "vesa" ];
          default = "vesa";
        };
      };

      usb = {

        enable = lib.mkEnableOption "USB driver";
        storage.enable = lib.mkEnableOption "USB mass storage driver";

        ehciSupport = lib.mkEnableOption "EHCI support" // { default = true; };
        ohciSupport = lib.mkEnableOption "OHCI support" // { default = true; };
        uhciSupport = lib.mkEnableOption "UHCI support" // { default = false; };
        xhciSupport = lib.mkEnableOption "XHCI support" // { default = true; };

      };

    };

  };

  config = {

    assertions = with builtins;
      let
        addrCheck = name: interface: {
          assertion = lessThan (length interface.ipv4.addresses) 2;
          message = "Genode interfaces do not support multihoming.";
        };
        routeCheck = name: interface: {
          assertion = lessThan (length interface.ipv4.routes) 2;
          message = "Genode interfaces do not support multiple routes.";
        };
        policyCheck = name: interface:
          let
            clientList = filter (x x != null) (lib.mapAttrsToList
              (childName: value:
                if any (nic: nic == name) value.routeToNics then
                  childName
                else
                  null) config.genode.init.children);
          in {
            assertion =
              trace clientList (clientList == [ ] || length clientList == 1);
            message = "Multiple routes to Nic ${name}, ${clientList}";
          };
      in lib.lists.concatMap
      (f: lib.mapAttrsToList f config.networking.interfaces) [
        addrCheck
        routeCheck
        policyCheck
      ];

    hardware.genode.ahci.enable = config.genode.boot.storeBackend == "ahci";

    hardware.genode.usb.storage.enable = config.genode.boot.storeBackend
      == "usb";

    hardware.genode.usb.enable = config.hardware.genode.usb.storage.enable;

    hardware.genode.platform.policies = lib.lists.imap0 (i: name:
      builtins.toFile (name + ".platform-policy.dhall") ''
        let Genode = env:DHALL_GENODE

        in  Genode.Init.Config.Policy::{
            , service = "Platform"
            , label = Genode.Init.LabelSelector.prefix "nixos -> ${name}.driver"
            , content =
              [ Genode.Prelude.XML.leaf
                  { name = "pci"
                  , attributes = toMap {
                    , class = "ETHERNET"
                    , index = "${toString i}"
                    }
                  }
              ]
            }
      '') (builtins.attrNames config.networking.interfaces)
      ++ (lib.optional config.hardware.genode.ahci.enable
        (builtins.toFile ("ahci.platform-policy.dhall") ''
          let Genode = env:DHALL_GENODE

          in  Genode.Init.Config.Policy::{
              , service = "Platform"
              , label = Genode.Init.LabelSelector.prefix "ahci_drv"
              , content =
                [ Genode.Prelude.XML.leaf
                    { name = "pci", attributes = toMap { class = "AHCI" } }
                ]
              }
        '')) ++ (lib.optional config.hardware.genode.framebuffer.enable
          (builtins.toFile ("framebuffer.platform-policy.dhall") ''
            let Genode = env:DHALL_GENODE

            in  Genode.Init.Config.Policy::{
                , service = "Platform"
                , label = Genode.Init.LabelSelector.prefix "fb_drv"
                , content =
                  [ Genode.Prelude.XML.leaf
                      { name = "pci", attributes = toMap { class = "VGA" } }
                  ]
                }
          '')) ++ (lib.optional config.hardware.genode.usb.enable
            (builtins.toFile ("usb.platform-policy.dhall") ''
              let Genode = env:DHALL_GENODE

              in  Genode.Init.Config.Policy::{
                  , service = "Platform"
                  , label = Genode.Init.LabelSelector.prefix "usb_drv"
                  , content =
                    [ Genode.Prelude.XML.leaf
                        { name = "pci", attributes = toMap { class = "USB" } }
                    ]
                  }
            ''));

    genode.init.children = let

      nics = mapAttrs' (name: interface:
        let name' = name + ".driver";
        in {
          name = name';
          value = let
            binary = with pkgs.genodePackages;
              {
                ipxe = ipxe_nic_drv;
                virtio = virtio_nic_drv;
              }.${interface.genode.driver};
          in {
            inputs = [ binary ];
            configFile = let
              policy = lib.mapAttrsToList (childName: value:
                if any (nic: nic == name) value.routeToNics then ''
                  Init.Config.Policy::{
                  , service = "Nic"
                  , label = Init.LabelSelector.prefix "${childName}"
                  }
                '' else
                  "") config.genode.init.children;

            in pkgs.writeText "${name'}.dhall" ''
              let Genode = env:DHALL_GENODE

              let Init = Genode.Init

              in  Init.Child.flat
                    Init.Child.Attributes::{
                    , binary = "${binary}/bin/${binary.pname}"
                    , resources = Init.Resources::{
                      , caps = 128
                      , ram = Genode.units.MiB 4
                      }
                    , routes = [
                      , Init.ServiceRoute.parent "IO_MEM"
                      , Init.ServiceRoute.parent "Platform"
                      ]
                    , config = Init.Config::{
                      , attributes = toMap { verbose = "true" }
                      , policies =
                            [ ${toString policy} ]
                          : List Init.Config.Policy.Type
                      }
                    }
            '';
          };
        }) config.networking.interfaces;

      sockets = mapAttrs' (name: interface:
        let name' = name + ".sockets";
        in {
          name = name';
          value = if interface.genode.stack == null then
            null
          else {

            inputs = with pkgs.genodePackages;
              {
                lwip = [ vfs_lwip ];
                lxip = [ vfs_lxip ];
              }.${interface.genode.stack};

            routeToNics = [ name ];

            configFile = let
              binary = "${pkgs.genodePackages.vfs}/bin/vfs";
              ram = {
                lwip = 16;
                lxip = 32;
              }.${interface.genode.stack};
              settings = with builtins;
                lib.optionals (interface.ipv4.addresses != [ ])
                (let addr = head interface.ipv4.addresses;
                in [
                  {
                    name = "ip_addr";
                    value = addr.address;
                  }
                  {
                    name = "netmask";
                    value = if addr.prefixLength == 24 then
                      "255.255.255.0"
                    else
                      throw "missing prefix to netmask conversion";
                  }
                ]) ++ lib.optional (interface.ipv4.routes != [ ])
                (let route = head interface.ipv4.routes;
                in {
                  name = "gateway";
                  value = route.address;
                }) ++ lib.optional (interface.useDHCP != null) {
                  name = "dhcp";
                  value = if interface.useDHCP then "true" else "false";
                };
              settingsMap = builtins.concatStringsSep ", " (map
                ({ name, value }:
                  ''{ mapKey = "${name}", mapValue = "${value}" }'') settings);
            in pkgs.writeText "${name'}.dhall" ''
              let Genode = env:DHALL_GENODE

              let Init = Genode.Init

              in  Init.Child.flat
                    Init.Child.Attributes::{
                    , binary = "${binary}"
                    , provides = [ "File_system" ]
                    , resources = Init.Resources::{
                      , caps = 128
                      , ram = Genode.units.MiB ${toString ram}
                      }
                    , config = Init.Config::{
                      , policies =
                        [ Init.Config.Policy::{
                          , service = "File_system"
                          , label = Init.LabelSelector.suffix "${name'}"
                          , attributes = toMap { root = "/", writeable="yes" }
                          }
                        ]
                      , content =
                          let VFS = Genode.VFS

                          in  [ VFS.vfs
                                  [ VFS.leafAttrs
                                      "${interface.genode.stack}"
                                      ([ ${settingsMap} ] : Genode.Prelude.Map.Type Text Text)
                                  ]
                              ]
                      }
                    }
            '';

          };
        }) config.networking.interfaces;

    in lib.filterAttrs (n: v: v != null) (nics // sockets);

    genode.core.children.ahci_drv = {
      inputs = [ pkgs.genodePackages.ahci_drv ];
      configFile = pkgs.writeText "ahci_drv.dhall" ''
        let Genode = env:DHALL_GENODE

        let Init = Genode.Init

        in  Init.Child.flat
              Init.Child.Attributes::{
              , binary = "ahci_drv"
              , resources = Init.Resources::{
                , caps = 400
                , ram = Genode.units.MiB 10
                , constrainPhys = True
                }
              , romReports = [ { local = "ports", route = "ahci_ports" } ]
              , routes =
                [ Init.ServiceRoute.parent "IRQ"
                , Init.ServiceRoute.parent "IO_MEM"
                , Init.ServiceRoute.parent "IO_PORT"
                ]
              , config = Init.Config::{
                , policies =
                  [ Init.Config.Policy::{
                    , service = "Block"
                    , label = Init.LabelSelector.prefix "part_block"
                    , attributes = toMap { device = "0", writeable = "yes" }
                    }
                  ]
                }
              }
      '';
    };

    genode.core.children.acpi_drv = {
      inputs = [ pkgs.genodePackages.acpi_drv ];
      configFile = pkgs.writeText "acpi_drv.dhall" ''
        let Genode = env:DHALL_GENODE

        let Init = Genode.Init

        let label = λ(_ : Text) → { local = _, route = _ }

        in  Init.Child.flat
              Init.Child.Attributes::{
              , binary = "acpi_drv"
              , resources = Init.Resources::{
                , caps = 400
                , ram = Genode.units.MiB 4
                , constrainPhys = True
                }
              , romReports = [ label "acpi", label "smbios_table" ]
              , routes =
                [ Init.ServiceRoute.parent "IRQ"
                , Init.ServiceRoute.parent "IO_MEM"
                , Init.ServiceRoute.parent "IO_PORT"
                ]
              }
      '';
    };

    genode.core.children.platform_drv = {
      inputs = [ pkgs.genodePackages.platform_drv ];
      configFile = let
        policies =
          map (policy: ", ${policy}") config.hardware.genode.platform.policies;
      in pkgs.writeText "platform_drv.dhall" ''
        let Genode = env:DHALL_GENODE

        let Init = Genode.Init

        in  Init.Child.flat
              Init.Child.Attributes::{
              , binary = "platform_drv"
              , resources = Init.Resources::{
                , caps = 800
                , ram = Genode.units.MiB 4
                , constrainPhys = True
                }
              , reportRoms = let label = "acpi" in [ { local = label, route = label } ]
              , routes =
                [ Init.ServiceRoute.parent "IRQ"
                , Init.ServiceRoute.parent "IO_MEM"
                , Init.ServiceRoute.parent "IO_PORT"
                ]
              , config = Init.Config::{
                , policies = [ ${
                  toString policies
                } ] : List Init.Config.Policy.Type
                }
              }
      '';
    };

    genode.core.children.usb_drv = let
      cfg = config.hardware.genode.usb;
      toYesNo = b: if b then "yes" else "no";
    in mkIf cfg.enable {
      inputs = [ pkgs.genodePackages.usb_drv ];
      configFile = builtins.toFile "usb_drv.dhall" ''
        let Genode = env:DHALL_GENODE

        let XML = Genode.Prelude.XML

        let Init = Genode.Init

        in  Init.Child.flat
              Init.Child.Attributes::{
              , binary = "usb_drv"
              , resources = Init.Resources::{ caps = 256, ram = Genode.units.MiB 12 }
              , romReports = let local = "devices" in [ { local, route = local } ]
              , routes = [ Init.ServiceRoute.parent "IO_MEM" ]
              , config =
                  let storagePolicy =
                        Init.Config.Policy::{
                        , service = "Usb"
                        , label = Init.LabelSelector.prefix "usb_block_drv"
                        , attributes = toMap { class = "8" }
                        , diag = Some True
                        }

                  in  Init.Config::{
                      , attributes = toMap
                          { ehci = "${toYesNo cfg.ehciSupport}"
                          , ohci = "${toYesNo cfg.ohciSupport}"
                          , uhci = "${toYesNo cfg.uhciSupport}"
                          , xhci = "${toYesNo cfg.xhciSupport}"
                          }
                      , content =
                        [ XML.element
                            { name = "raw"
                            , attributes = XML.emptyAttributes
                            , content =
                              [ XML.leaf
                                  { name = "report"
                                  , attributes = toMap { devices = "yes" }
                                  }
                              , Init.Config.Policy.toXML storagePolicy
                              ]
                            }
                        ]
                      , policies = [ storagePolicy ] : List Init.Config.Policy.Type
                      }
              }
      '';
    };

    genode.core.children.usb_block_drv =
      mkIf config.hardware.genode.usb.storage.enable {
        inputs = [ pkgs.genodePackages.usb_block_drv ];
        configFile = builtins.toFile "usb_block_drv.dhall" ''
          let Genode = env:DHALL_GENODE

          let XML = Genode.Prelude.XML

          let Init = Genode.Init

          in  Init.Child.flat
                Init.Child.Attributes::{
                , binary = "usb_block_drv"
                , resources = Init.Resources::{ caps = 256, ram = Genode.units.MiB 4 }
                , config = Init.Config::{
                  , attributes = toMap { writeable = "yes" }
                  , policies =
                    [ Init.Config.Policy::{
                      , service = "Block"
                      , label = Init.LabelSelector.prefix "part_block"
                      }
                    ]
                  }
                }
        '';
      };

    genode.core.children.fb_drv =
      mkIf config.hardware.genode.framebuffer.enable {
        inputs = with pkgs.genodePackages;
          {
            "boot" = [ boot_fb_drv ];
            "vesa" = [ vesa_drv ];
          }.${config.hardware.genode.framebuffer.driver};
        configFile = let
          binary = with pkgs.genodePackages;
            {
              "boot" = "boot_fb_drv";
              "vesa" = "vesa_fb_drv";
            }.${config.hardware.genode.framebuffer.driver};
        in builtins.toFile "fb_drv.dhall" ''
          let Genode = env:DHALL_GENODE

          let XML = Genode.Prelude.XML

          let Init = Genode.Init

          in  Init.Child.flat
                Init.Child.Attributes::{
                , binary = "${binary}"
                , resources = Init.Resources::{ caps = 256, ram = Genode.units.MiB 32 }
                , routes =
                  [ Init.ServiceRoute.parent "IO_MEM"
                  , Init.ServiceRoute.parent "IO_PORT"
                  ]
                }
        '';
      };

    virtualisation.useBootLoader = config.genode.boot.storeBackend != "tarball";

    virtualisation.qemu.options = lib.optional config.hardware.genode.usb.enable
      (lib.optional (pkgs.stdenv.isi686 || pkgs.stdenv.isx86_64) "-usb"
        ++ lib.optional (pkgs.stdenv.isAarch32 || pkgs.stdenv.isAarch64)
        "-device usb-ehci,id=usb0");

  };

}