如何理解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 bruijn指数有关吗？

Answer 1

这是一个SExp，而不是TT所以它还没有de Bruijn-ized：

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

请注意，Loc 0的LWriteStr参数不受此片段的约束;我猜这将是传递给IO的main世界标记，因此整个main将是

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