Support registers and option "pseudovariables"

[mrkgnao]

Currently we only support regular variables with the sigils [glsa]:, but we will need to access registers, options, and environment variables (with @, &, &[gl]:, and $).

[mrkgnao]

This looks not-unreasonably-difficult: for registers, which I'll try first, we need to add another constructor to VIM_Foreign in Vimscript.FFI, and read it out in genForeign. We also have to add another type of NameScope. Reading and setting registers is a side-effect (yay global variables!) so the corresponding Idris primops should be in IO.

[owickstrom]

Sounds very good. Agree on all the points. Is it called "sigils" in Vim lingo?

[mrkgnao]

I mean, prefixes of that sort (e.g. Perl/BASIC $) are usually called "sigils" in my experience. 🤷‍♂️

[owickstrom]

Ok :) just asked because we might change the type name "NameScope" in the AST, if so.

Den 2 dec. 2017 11:02 skrev "Soham Chowdhury" notifications@github.com:

I mean, prefixes of that sort (e.g. Perl/BASIC $) are usually called "sigils" in my experience. 🤷‍♂️

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/owickstrom/idris-vimscript/issues/3#issuecomment-348681698, or mute the thread https://github.com/notifications/unsubscribe-auth/ABZYCIMtgGmmvtELY7kRls1Pgjdf3Bnbks5s8SBJgaJpZM4QzK6u .

[mrkgnao]

I decided to try options instead; reading values of options is introduced in https://github.com/owickstrom/idris-vimscript/pull/1/commits/5532e00ae22bc8555e90c304c0dd7cd308f3f7fd.

To write values of options, we will need to modify the Let constructor: since it is currently of the form Let Name Expr, the LHS of the let is forced to be a local variable (like l:foo). We want

let &foo = bar

instead. We will either have to generalise the Let tycon to accept a general ScopedName (we will have to refactor some code in that case) or add a new tycon for "option-lets", but then we will want more when we introduce register assignment and so on. What do you recommend?

Another option is to have small RTS functions like

function setVimOption(name, value) abort
  execute "&" . a:name . "=" . a:value
endfunction

but I'd strongly prefer we not do this.

[owickstrom]

I prefer generalizing the Let constructor. 👍

[mrkgnao]

Done in https://github.com/owickstrom/idris-vimscript/pull/1/commits/a0422ac64f59743c71ab56c72c89336b528778a1. Let's proceed to actually using the generalised constructor.

[mrkgnao]

Writing values of options is now supported with https://github.com/owickstrom/idris-vimscript/pull/1/commits/ed3a9ca2d3e838e9a3dd35b2df0529848c419b45. (example here)

Extending this to registers and scoped options (&g:foo,&l:foo) is easy now :)

[mrkgnao]

@owickstrom as in https://github.com/owickstrom/idris-vimscript/issues/6, it seems generalising over register names won't work with the current approach. The crux of it is: how do you read a register whose name is passed in as a variable without using execute or some form of eval/unquoting? This is needed to, e.g. loop over registers. (Obviously, &(l:foo) doesn't work.)

We will either need to create a small RTS, or emit execute commands from the code generator itself (which is the same as the former, morally):

function! s:readRegister(a)
    execute ("l:a = &" . a:a)
    return l:a
endfunction

or specialise all our code manually:

prim__readRegister : ... -- not exported

readRegisterA = prim__readRegister "a" -- statically known argument!
readRegisterB = prim__readRegister "b"

-- ...

data Register = RA | RB | ...

readRegister : Register -> ...
readRegister RA = readRegisterA
readRegister RB = readRegisterB
...

These seem like the only ways that the codegen will get statically known (per this document's language) arguments passed to the builtins.

I'm leaning towards the latter, since the execute-based ones will make inlining and optimisation really, really hard. (Unless we extend our Expr and Stmt types to have explicit knowledge of the "execute " ++ targetRegName ++ " = " ++ whatever idiom instead of representing it as BinOpApply Concat, but this extension of core data types will again complicate analysis and increase complexity a lot.)

[mrkgnao]

Also, I think this is why the C backend has separate primops for 8-, 16-, 32-, and 64-bit operations.

https://github.com/idris-lang/Idris-dev/blob/3f7bb1ce6d3974a39035ca9294f84ba128615a14/libs/prelude/Builtins.idr#L217

[owickstrom]

I'm also very much for the latter, but I think we can simplify as this:

-- adding this to VIM_Foreign:
  ...
  | VIM_ReadRegister String
  ...

-- in Builtins.idr:
public export
data Register : String -> Type where
  RA : Register "a"
  RB : Register "b"

%inline
public export
readRegister : Register r -> VIM_IO String
readRegister {r} _ = foreign FFI_VIM (VIM_ReadRegister r) (VIM_IO String)

-- in CodegenVim.hs:
...
genForeign ret (FApp (showCG -> "VIM_ReadRegister") [FStr reg]) _ = do
  stmt <- ret (Vim.WhateverWeNeedHere (T.pack reg))
  pure [stmt]

Then usage is:

main = readRegister RA

[mrkgnao]

I'm not sure whether that leaves open the same problem as the existing code when you try map readRegister [RA, RB]. The ffi_fn f argument essentially has to be monomorphised at compile-time.

That's why I went to all that trouble: note that, at the definition sites of all those functions, we are creating a "fixed" call to prim__readRegister.

(I considered a minor variation on yours before, actually, but then I decided it wouldn't work. I would love to find that I was mistaken, for obvious reasons! :D)

[owickstrom]

Oh, not sure about that. We can try it later.

Den 3 dec. 2017 15:55 skrev "Soham Chowdhury" notifications@github.com:

I'm not sure whether that leaves open the same problem as the existing code when you try map readRegister [RA, RB]. (I considered a minor variation on this but decided it wouldn't work. Maybe I was wrong?)

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/owickstrom/idris-vimscript/issues/3#issuecomment-348778790, or mute the thread https://github.com/notifications/unsubscribe-auth/ABZYCPl-5sI8Dv6muKtIiV4RYisMyQl9ks5s8rZtgaJpZM4QzK6u .

[mrkgnao]

Another option: if we do go the specialisation route, we should look at "Template Idris", aka elaborator reflection, to do the work for us.

[owickstrom]

Tried a bit more, and as you say, the mapping example can't do the static specialization.

I guess this comes down to what you want to optimize for when writing plugins with Idris, i.e. if you do find yourself mapping over registers, or if you're usually working with a fixed set directly.

If we don't support mapping, like in your example, I think the GADT approach is nicer than a whole bunch of writeRegister<R>. You can't put your [R0, R1, ...] in a list and map over them, you get a type error, but that supports our decision nicely, IMO.

If we do want dynamic mapping over them, I think we can live with an RTS function or an inlined call to execute.

Thoughts?

[owickstrom]

And as with specialized writeRegisterA etc, you could do zipWith ($) [writeRegister X, writeRegister Y] ["foo", "bar"], or whatever... 😃

[mrkgnao]

I'd just prefer to not have code that typechecks, successfully elaborates, and then fails at the codegen step because of something we can design around. And with the GADT, you can break that guarantee: wrap it in an existential and map over lists of these existentialised things with a function of type forall r. Register r -> foo, kinda like the exists package lets you do in Haskell. Even if it's a bit of a stretch, it's not something like unsafePerformIO where you can say "all bets are off if you use that".

(I'm really strongly leaning towards figuring out the elaborator reflection idea. What do you say? 😉)

[owickstrom]

If you have time to try it, then go for it, and we'll see later what works best. 😃

[mrkgnao]

There's some work on this branch:

https://github.com/mrkgnao/idris-vimscript/commits/elabrefl-registers