import Base
import ./type.bend as ND
import ./service/type.bend as Sv
import ./service/ops.bend as SvO
import ../../container/type.bend as Ct

def user(nd: ND.NixDarwin) -> String:
  match nd:
    case ND.NixDarwin{_, _, u, _, _, _, _, _, _, _, _, _, _, _}:
      u

def tailscale(nd: ND.NixDarwin) -> Bool:
  match nd:
    case ND.NixDarwin{_, _, _, _, t, _, _, _, _, _, _, _, _, _}:
      t

def services(nd: ND.NixDarwin) -> List<&2, Sv.Service>:
  match nd:
    case ND.NixDarwin{_, _, _, _, _, _, _, _, ss, _, _, _, _, _}:
      ss

def serves(nd: ND.NixDarwin) -> List<&2, ND.Serve>:
  match nd:
    case ND.NixDarwin{_, _, _, _, _, _, _, _, _, ss, _, _, _, _}:
      ss

def listeners(nd: ND.NixDarwin) -> List<&2, ND.Listening>:
  match nd:
    case ND.NixDarwin{_, _, _, _, _, _, _, _, _, _, ls, _, _, _}:
      ls

def kept(nd: ND.NixDarwin) -> List<&2, String>:
  match nd:
    case ND.NixDarwin{_, _, _, _, _, _, _, _, _, _, _, k, _, _}:
      k

def serve_container(s: ND.Serve) -> String:
  match s:
    case ND.Serve{c, _, _, _}:
      c

def serve_https(s: ND.Serve) -> U32:
  match s:
    case ND.Serve{_, h, _, _}:
      h

def serve_port(s: ND.Serve) -> U32:
  match s:
    case ND.Serve{_, _, p, _}:
      p

# What Tailscale proxies a serve to.
def serve_target(s: ND.Serve) -> String:
  match s:
    case ND.Serve{_, _, p, path}:
      "http://127.0.0.1:" ++ U32.show(p) ++ path

def listening_process(l: ND.Listening) -> String:
  match l:
    case ND.Listening{p, _}:
      p

def listening_processes(xs: List<&2, ND.Listening>) -> List<&2, String>:
  match xs:
    case []:
      []
    case l <> rest:
      listening_process(l) <> listening_processes(rest)

# ---- the nix-darwin flake: pinned inputs, the Mac's module, and one launchd job per service ----
def tailscale_line(on: Bool) -> String:
  match on:
    case True{}:
      "      services.tailscale.enable = true;\n"
    case False{}:
      ""

# `lets` are Nix bindings the jobs may use (e.g. a derivation); `config` is extra nix-darwin config lines.
def flake(nd: ND.NixDarwin) -> String:
  match nd:
    case ND.NixDarwin{host, platform, +u, +logs, t, _, _, _, ss, _, _, _, lets, config}:
      "# Generated by V from the architecture. Do not edit.\n" ++
      "{\n" ++
      "  inputs.nixpkgs.url = \"github:NixOS/nixpkgs/nixpkgs-unstable\";\n" ++
      "  inputs.nix-darwin.url = \"github:nix-darwin/nix-darwin/master\";\n" ++
      "  inputs.nix-darwin.inputs.nixpkgs.follows = \"nixpkgs\";\n" ++
      "  outputs = { nixpkgs, nix-darwin, ... }: {\n" ++
      "    darwinConfigurations." ++ host ++ " = nix-darwin.lib.darwinSystem {\n" ++
      "      system = \"" ++ platform ++ "\";\n" ++
      "      modules = [ ./mac.nix ({ pkgs, ... }: let\n" ++ lets ++
      "      in {\n" ++ config ++ tailscale_line(t) ++ SvO.jobs(ss, u, logs) ++ "      }) ];\n    };\n  };\n}"

# The Tailscale CLI: Nix's when Nix runs Tailscale, else the app's.
def tailscale_command(nd: ND.NixDarwin) -> String:
  Bool.pick(String, tailscale(nd), "/run/current-system/sw/bin/tailscale", "/Applications/Tailscale.app/Contents/MacOS/Tailscale")

# ---- laws of a system with this node ----
# 0 is not a port.
def fresh(+p: U32, ps: List<&2, U32>) -> Bool:
  U32.is_eq(p, 0) || Bool.not(List.contains(~U32, ~U32.is_eq, ps, p))

def distinct(ps: List<&2, U32>) -> Bool:
  match ps:
    case []:
      True{}
    case +p <> +rest:
      fresh(p, rest) && distinct(rest)

def https_ports(xs: List<&2, ND.Serve>) -> List<&2, U32>:
  match xs:
    case []:
      []
    case s <> rest:
      serve_https(s) <> https_ports(rest)

# No two serves share a tailnet HTTPS port.
def serve_ports_distinct(nd: ND.NixDarwin) -> Bool:
  distinct(https_ports(serves(nd)))

def belongs(l: ND.Listening, +keys: List<&2, String>) -> Bool:
  match l:
    case ND.Listening{_, +o}:
      String.eq(o, "macos") || List.contains(~String, ~String.eq, keys, o)

def all_belong(xs: List<&2, ND.Listening>, +keys: List<&2, String>) -> Bool:
  match xs:
    case []:
      True{}
    case l <> rest:
      belongs(l, keys) && all_belong(rest, keys)

# Every allowed listener belongs to macOS or to one of `keys` (the system's containers and nodes).
def listeners_belong(nd: ND.NixDarwin, +keys: List<&2, String>) -> Bool:
  all_belong(listeners(nd), keys)

def services_among(xs: List<&2, Sv.Service>, +instances: List<&2, String>) -> Bool:
  match xs:
    case []:
      True{}
    case s <> rest:
      List.contains(~String, ~String.eq, instances, SvO.container(s)) && services_among(rest, instances)

def serves_among(xs: List<&2, ND.Serve>, +instances: List<&2, String>) -> Bool:
  match xs:
    case []:
      True{}
    case s <> rest:
      List.contains(~String, ~String.eq, instances, serve_container(s)) && serves_among(rest, instances)

# Services and serves run only containers this node runs.
def services_on(+nd: ND.NixDarwin, +instances: List<&2, String>) -> Bool:
  services_among(services(nd), instances) && serves_among(serves(nd), instances)

def served(+k: String, xs: List<&2, ND.Serve>) -> Bool:
  match xs:
    case []:
      False{}
    case s <> rest:
      String.eq(k, serve_container(s)) || served(k, rest)

def is_tailnet(e: Ct.Exposure) -> Bool:
  match e:
    case Ct.Tailnet{}:
      True{}
    case _:
      False{}

def honest(c: Ct.Container, +ss: List<&2, ND.Serve>, +instances: List<&2, String>) -> Bool:
  match c:
    case Ct.Container{+k, _, _, _, _, e, _, _, _, _, _, _, _, _, _}:
      Bool.not(List.contains(~String, ~String.eq, instances, k)) || Bool.not(Bool.xor(is_tailnet(e), served(k, ss)))

def all_honest(cs: List<&2, Ct.Container>, +ss: List<&2, ND.Serve>, +instances: List<&2, String>) -> Bool:
  match cs:
    case []:
      True{}
    case c <> rest:
      honest(c, ss, instances) && all_honest(rest, ss, instances)

# A container on this node is on the tailnet exactly when a serve names it.
def exposure_honest(nd: ND.NixDarwin, +cs: List<&2, Ct.Container>, +instances: List<&2, String>) -> Bool:
  all_honest(cs, serves(nd), instances)

# Services that start at login need the Mac to log its user in by itself.
def survives_reboot(+nd: ND.NixDarwin, auto_login_user: String) -> Bool:
  Bool.not(SvO.needs_login(services(nd))) || String.eq(auto_login_user, user(nd))