How to understand SDecl in idris?

Question

I am working on writing a backend for idris , the idris code (abbreviated)

main = putStrLn "hello"

generated this :

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

How to understand the Loc n there? is that related to de brujin index?

Answer 1

This is an SExp, not a TT so it's not yet de Bruijn-ized:

Module      : IRTS.Simplified
Description : Simplified expressions, where functions/constructors can only be applied to variables.

SLoc n is simply a generated identifier, so in your example, the inner SLet does shadow the outer (unused) SLet; it could be sugared into

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

or, alternatively, assigning unique names to variables, to

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

Note that the Loc 0 argument to LWriteStr is not bound in this fragment; I guess that would be the IO world token passed to main, so the whole of main would be

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