时间戳

首页 > 解决方案 > 如何理解 idris 中的 SDecl？

compilation - 如何理解 idris 中的 SDecl？

问题描述

我正在为 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？这与德布鲁金指数有关吗？

标签： compilationfunctional-programmingidris

解决方案

这是 a SExp，不是 aTT所以它还没有被 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

请注意，此片段中未绑定Loc 0to 的参数；LWriteStr我想这将是IO传递给的世界令牌main，所以整个main将是

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

推荐阅读