Type nat specialization

RefrStuff.hs

-- Form1: Wrapper type class

withELF1 :: FilePath -> (E.SomeElf E.Elf -> IO ()) -> IO ()
withELF1 fp k = do
  bytes <- B.readFile fp
  case E.parseElf bytes of
    E.Elf32Res [] e32 -> k $ E.Elf32 e32
    E.Elf64Res [] e64 -> k $ E.Elf64 e64


testDiscovery1 :: FilePath -> E.SomeElf E.Elf -> IO ()
testDiscovery1 fname elf =
    case elf of
      E.Elf32 e32 -> testDiscovery32 fname e32

-- Form2: Witnessing specific type via parameterized-utils testEquality

withELF2 :: FilePath -> (forall w. NatRepr w -> E.Elf w -> IO ()) -> IO ()
withELF2 fp k = do
  bytes <- B.readFile fp
  case E.parseElf bytes of
    E.Elf32Res [] e32 -> k (knownNat @32) e32
    E.Elf64Res [] e64 -> k (knownNat @64) e64

testDiscovery2 :: forall w . FilePath -> NatRepr w -> E.Elf w -> IO ()
testDiscovery2 fname sz elf =
    case testEquality sz (knownNat @32) of
      Just Refl -> testDiscovery32 fname elf
      Nothing -> error "not 32"

-- Form3: With ELF internal type class

withELF3 :: FilePath -> (forall w. E.Elf w -> IO ()) -> IO ()
withELF3 fp k = do
  bytes <- B.readFile fp
  case E.parseElf bytes of
    E.Elf32Res [] e32 -> k e32
    E.Elf64Res [] e64 -> k e64

testDiscovery3 :: forall w . FilePath -> E.Elf w -> IO ()
testDiscovery3 fname elf =
    case E.elfClass elf of
      E.ELFCLASS32 -> testDiscovery32 fname elf
      _ -> error "not 32"


-- Framework for the above:

testDiscovery32 :: FilePath -> E.Elf 32 -> IO ()
testDiscovery32 expectedFilename elf =
  withMemory MM.Addr32 elf $ \mem -> return ()

main = do withElf1 "filename.exe" (testDiscovery1 "filename.exe")
          withElf2 "filename.exe" (testDiscovery2 "filename.exe")
          withElf3 "filename.exe" (testDiscovery3 "filename.exe")