如何在Agda中检查大型值？适配5×5 Word64表格调试

我来分享几个在Agda里处理这类大型数值表格调试的实用技巧，毕竟盯着64位二进制串看确实容易眼花😅

1. 用Agda REPL直接求值查看格式化结果 #

你已经写了view函数把表格转成字符串，那最直接的方式就是在Agda的交互式环境（REPL）里调用它：

• 先加载你的Agda文件：> :load YourFileName.agda
• 假设你的表格实例是myTable : Vec (Vec Word64 5) 5，直接输入> view myTable就能看到格式化后的输出。

如果输出被REPL截断了，可以调整输出限制：

> :set max-output-size 20000  -- 设置更大的输出长度上限

2. 优化view函数的可读性 #

默认的64位二进制串太冗长了，你可以把Word64转成十六进制字符串，这样每个值只需要16个字符，表格会紧凑很多：

open import Data.Word
open import Data.String
open import Data.Nat
open import Data.Char

-- 将Word64转换为十六进制字符串
word64ToHex : Word64 -> String
word64ToHex w = natToHex (toNat w) ""
  where
    natToHex : Nat -> String -> String
    natToHex zero s = s
    natToHex n s = natToHex (n ÷ 16) (hexDigit (n mod 16) ∷ s)
    
    hexDigit : Nat -> Char
    hexDigit d with d < 10
    ... | true = chr (48 + d)  -- 0-9
    ... | false = chr (55 + d) -- A-F

-- 优化后的view函数，每行输出5个十六进制值
view : Vec (Vec Word64 5) 5 -> String
view table = unlines (map (unwords ∘ map word64ToHex) table)

这样输出的表格会变成类似：

0000000000000000 123456789ABCDEF0 0000000000000000 ...
...

可读性提升不少。

3. 编写针对性测试用例，聚焦关键值 #

不用每次都看全表，你可以针对表格里的关键位置写等式测试，让Agda自动验证值是否符合预期：

open import Relation.Binary.PropositionalEquality
open import Data.Vec

myTable : Vec (Vec Word64 5) 5
myTable = -- 你的表格实现

-- 验证第一行第一列的值为0
test-top-left : myTable !! 0 !! 0 ≡ 0
test-top-left = refl

-- 验证第三行第四列的值为特定十六进制数
test-middle : myTable !! 2 !! 3 ≡ 0xDEADBEEFCAFEBABE
test-middle = refl

如果这些等式能被Agda顺利通过，说明对应位置的逻辑是正确的，不用浪费时间看全量输出。

4. 将输出导出到外部文件 #

如果REPL里看还是不方便，你可以用Agda的IO库把view的结果写入文件，这样能完整查看所有内容：

open import IO

-- 将表格写入指定文件
writeTableToFile : Vec (Vec Word64 5) 5 -> IO ()
writeTableToFile table = writeFile "word64-table.txt" (view table)

在REPL里运行这个IO动作：

> run (writeTableToFile myTable)

之后你就能在当前目录下的word64-table.txt里看到完整的格式化表格了。

内容的提问来源于stack exchange，提问作者MaiaVictor