Emacs indentation for multi-line constructs

[ilyasergey]

The following snipped is not indented correctly:

match A with
| _ ->
  expr = {something ;
          something_else}

[vaivaswatha]

Committed directly to master. Closing issue.

[ilyasergey]

The issue still persists in a code with >2 lines to be indented:

transition Pong (sender: Address)
  one = 1;
  cnt <- count;
  is_game_over = builtin lt cnt one;
  match is_game_over with
  | True =>
    msg = {_tag : Main;
                     to : pingAddr;
        _amount : 0};
    msgs = one_msg msg;
    send msgs
  end
end

[vaivaswatha]

@ilyasergey can you check now (and close if it works).

[ilyasergey]

There are still some issues:

1. Tabs and spaces are used inconsistently. For instance, the file below is formatted following the automatic indentation, so the tabs are inserted. It is not visible in my editor, as the tab is the same as two-spaces, but visible here.

transition Pong (sender: Address)
  one = 1;
    cnt <- count;
  is_game_over = builtin lt cnt one;
  match is_game_over with
  | True =>
        msg = {_tag : Main;
                     to : pingAddr;
                     _amount : 0};
    msgs = one_msg msg;
    send msgs
  end
end

Can we please fix the standard indent size to be two space?

2. Even the spaces/tabs thing aside, the code around True branch is formatted without ever pressing a tab (just making new lines), and hence the multi-line message body is misaligned. Getting rid of (non-uniform) \t in favour of double-spaces would solve this issue.

3. The following fragment is formatted by pressing "enter" for the new lines:

let zero = Zero in 
    let one  = Succ zero in
        let two  = Succ one in
            let three = Succ two in
                let four = Succ three in
                    four

As customary in ML-style languages, let-bindings should not get an additional indentation when nested, hence this should be formatted as

let zero = Zero in 
let one  = Succ zero in
let two  = Succ one in
let three = Succ two in
let four = Succ three in
four

[vaivaswatha]

@ilyasergey (3) I've fixed this now. Nested "let-in" and "fun" constructs don't indent. But if one follows the other, there is an indentation. (i.e., fun => let-in .... let-in will be indented). Only consecutive ones of the same type (fun/let-in) don't indent.

The following lines specify to use only "2 spaces" for tabs. It seems to be working on mine. I do not know why it's not what is happening with your editor. For example, with the current contract.zilla of "zil-game", if I do an "od -bc" on it, I see only two '\t' characters, both unrelated to indentation (they are at the end of the line, not beginning).

;; Set to use only spaces for indentation, no tabs.                                                                           
(setq indent-tabs-mode nil)
(setq default-tab-width 2)

[vaivaswatha]

@AmritKumar @ilyasergey I must also comment that, there may be other smaller issues with indentation. It is doing a rule-based matching rather than defining a full grammar and specifying the indentation.

To me, it seems good enough to write Scilla code (which I currently am, in Emacs). We can defer attempts on perfect indentation to a later time when things are more stable.

[ilyasergey]

@vaivaswatha Thanks for the fixes. I've just tried the last one.

In fact, the two lines that fixed by \t-related issue are slightly different, but thanks for pointing this out:

(setq-default indent-tabs-mode nil)
(setq default-tab-width 2)

Unfortunately, there are still issues that make the Emacs mode somewhat difficult to use. Specifically:

(1) Here's a code fragment, written from scratch in scilla-emacs mode, without ever pressing TAB:

let x = 5 in
let g = 42 in
let y = g in
  match y with
  | _ => let z = builtin add x g in
  z
  end

Trying to play with the position of the last z gives some funny effect on the formatting of end

Expected behaviour:

let x = 5 in
let g = 42 in
let y = g in
match y with
| _ => let z = builtin add x g in
       z
end

(1') Moving the last let-in to the new line and pressing tabs to reformat gives the following:

let x = 5 in
let g = 5 in
  match g with
  | _ =>
    let z = g in
      z
      end

Expected result:

let x = 5 in
let g = 5 in
match g with
| _ =>
  let z = g in
  z
end

(2) If I type the following text without pressing tab, I get it formatted as follows:

let x = 5 in
  let g = 42 in g<caret position>

The second line only "moved left" if I start a new line after the last g. This is confusing and inconvenient.

Expected behaviour:

let x = 5 in
let g = 42 in g<caret position>

(3) Furthermore, with the same fragment, if I first type (without using TAB):

let x = 5 in
  let g<caret position>

and then press TAB (in a hope that the formatting will go right), it will result in

let x = 5 in
<caret position>let g

I.e., the caret position is now somehow before the second let, not after g.

Expected behaviour (after TAB):

let x = 5 in
let g<caret position>

Could you please, fix all of these? As a rule of thumb, I suggest to follow the principles that, in the series of chained let-in bindings, the indentation is the same as for the first one. A let-in binding within a pattern matching branch or a function body starts a new chain, providing the new base offset.

[vaivaswatha]

(1) has the problem because it only understands if the => is at the end of the line. So "match" should be put on a new line. (1') This is a bug and I am not sure if there's an easy fix. As I said, this is a lot of pattern matching and not based on a grammar. (2) This is expected. When you press "enter" after typing the first line, it doesn't yet know that you're typing in a nested "let", so it indents forward. Only after you type a "let" (and press tab/enter) does it know that this is an nested "let" and indents back. (3) I've fixed the caret position bug now. It remains where it was after indentation takes place, but taking the indentation into consideration. If the position happens to be a leading whitespace, it moves to the first character (this is common behaviour, but if you prefer, can be changed).

[ilyasergey]

(1) has the problem because it only understands if the => is at the end of the line. So "match" should be put on a new line.

I'm not sure I understand what the described issue has to do with =>. The match is on the new line in my example, yet it still isn't aligned correctly. It should be aligned with the preceding lets.

(1') This is a bug and I am not sure if there's an easy fix. As I said, this is a lot of pattern matching and not based on a grammar.

Please, implement the grammar then, as the "pattern matching" doesn't seem to cut it.

(2) This is expected. When you press "enter" after typing the first line, it doesn't yet know that you're typing in a nested "let", so it indents forward. Only after you type a "let" (and press tab/enter) does it know that this is an nested "let" and indents back.

This should not be an "expected" behaviour. The next let takes place in the body of the previous let (since it comes after in), there is no ambiguity here, so it would be given an extra indent. Please, fix it.

(3) I've fixed the caret position bug now. It remains where it was after indentation takes place, but taking the indentation into consideration. If the position happens to be a leading whitespace, it moves to the first character (this is common behaviour, but if you prefer, can be changed).

Here's a weird behaviour I get now:

let x = 5 in
<caret position>  let g = 

after pressing the TAB:

let x = 5 i<caret position>n
let g = 

[vaivaswatha]

The next let takes place in the body of the previous let (since it comes after in), there is no ambiguity here, so it would be given an extra indent

Nested lets shouldn't have indents right?

[vaivaswatha]

Here's a weird behaviour I get now:

I've fixed this now.

The "end" problem is also fixed. Please have a look.

Please, implement the grammar then,

This is non-trivial and might take a couple of days (at least, maybe more, I don't know) of dedicated effort.

[ilyasergey]

Nested lets shouldn't have indents right?

Correct. Neither should commands tgat go in the body of the last let, like that ‘match’.

[vaivaswatha]

Neither should commands tgat go in the body of the last let, like that ‘match’.

I assumed that the command that goes after the last "let" should indent. That was the disconnect. This should now be fixed though.

[ilyasergey]

Thanks, this looks better now. Here's another couple of minor issues:

1. Input:

fun (a : Int) =>
  fun (z: Int) => z<caret>

After pressing TAB:

fun (a : Int) =>
fun (z: Int) => z

<caret>

2. Nested functions should be aligned in the same way as one types. I.e., this is what I see now if I type without using TAB:

fun (x : Int) =>
  fun (g : Int) => x

Should be:

fun (x : Int) =>
fun (g : Int) => x

[vaivaswatha]

How should this be indented?

fun (x : Int) =>
  match ...

If above is correct, then the behaviour you report in (2) is normal (because, until you press tab it doesn't know that the line is a nested fun).

If on the other hand, it should be

fun (x : Int) =>
match ...

Then I will fix both.

[ilyasergey]

Hmm, okay. Let's keep (2) the way it is.

[ilyasergey]

4. Here's another formatting issue (obtained after repeatedly pressing tab in one of the test contracts):

library CrowdFundingInvoke

let one_msg = 
  fun (msg : Message) => 
    let nil_msg = Nil {Message} in
    Cons {Message} msg nil_msg

    (***************************************************)
    (*             The contract definition             *)
    (***************************************************)
    contract CrowdFundingInvoke

    (*  Parameters *)
    (cfaddr     : Address) (* address of the crowdfunding contract *)
...

Seems like the first function messes up the rest of the scope.

5. In a transition body, the following fragment:

transition Blah(_sender: Address)
  bal <-
  balance;
  s =
  sender;
donate_s = "Donate";

should be formatted as

transition Blah(_sender: Address)
  bal <-
    balance;
  s =
    sender;
  donate_s = "Donate";

[ilyasergey]

As I can see 4 is now fixed. Thanks.

[vaivaswatha]

The right way to solve this is to write a separate scilla-format tool that can canonical print Scilla, and this tool callable from Emacs.

Such a tool is an interesting project in itself: https://beza1e1.tuxen.de/articles/formatting_code.html

[anton-trunov]

Related issue: #788