如何理解idris中的SDecl？

Question

我正在为 idris 编写后端，即 idris 代码（缩写）

main = putStrLn "hello"

生成了这个：

(SLet
    (Loc 1)
    (SLet
        (Loc 1)
        (SConst "hello\n")
        (SOp LWriteStr [Loc 0,Loc 1]))
    (SCon Nothing 0 MkUnit [])
    )

那里的Loc n怎么理解？这与 de brujin 指数有关吗？

Answer 1

这是 SExp，不是 TT，所以它还没有被 de Bruijn 化：

Module      : IRTS.Simplified
Description : Simplified expressions, where functions/constructors can only be applied to variables.

SLoc n 只是一个生成的标识符，因此在您的示例中，内部 SLet 确实遮蔽了外部（未使用）SLet ;它可以被糖化成

let v1 = let v1 = "hello\n" in writeStr v0 v1
in v1

或者，或者，为变量分配唯一的名称，

let v1 = let v2 = "hello\n" in writeStr v0 v2
in v1

请注意，LWriteStr 的 Loc 0 参数未绑定在此片段中；我猜那将是传递给 main 的 IO 世界令牌，因此整个 main 将是

\v0 => let v1 = let v2 = "hello\n" in writeStr v0 v2 in v1

How to understand SDecl in idris?