如何理解idris中的SDecl?

Posted

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了如何理解idris中的SDecl?相关的知识,希望对你有一定的参考价值。

我正在为idris写一个后端,idris代码(缩写)

main = putStrLn "hello"

生成这个:

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

如何理解那里的Loc n?这与de bruijn指数有关吗?

答案

这是一个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
" in writeStr v0 v1
in v1

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

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

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

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

以上是关于如何理解idris中的SDecl?的主要内容,如果未能解决你的问题,请参考以下文章

Idris 中的复杂量词?

调用模板化成员函数:帮助我理解另一个 *** 帖子中的代码片段

Agda 和 Idris 的区别

切换片段时如何维护子视图的状态?

Idris——类似Haskell的纯函数编程语言

c_cpp 来自Idris Lightyear的实验笔记