如何理解idris中的SDecl?

问题描述 投票:0回答:1

我正在为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指数有关吗?

compilation functional-programming idris
1个回答
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 0LWriteStr参数不受此片段的约束;我猜这将是传递给IOmain世界标记,因此整个main将是

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

推荐问答