如何理解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 0
的LWriteStr
参数不受此片段的约束;我猜这将是传递给IO
的main
世界标记,因此整个main
将是
v0 => let v1 = let v2 = "hello
" in writeStr v0 v2 in v1
以上是关于如何理解idris中的SDecl?的主要内容,如果未能解决你的问题,请参考以下文章