ATS mode indentation

[Andrew Knapp]

Hello all,

By cannibalizing sml.el, I have largely gotten automatic indentation working in ATS.

After a few months of sporadic use, the only problem I couldn't fix is excessive indentation after a function has ended.

This can be fixed by terminating all functions with semicolons, which is ugly, but it seems to work.

If you don't do this, you have to type "fun" and then hit tab to indent properly.

Perhaps someone with more experience with programming languages can fix this, since I have no background with parsers.

(The code is based on Emacs' SMIE, which uses operator precedence grammars.)

Here is the temporary link. Let me know what I need to do to get this upstream.

https://github.com/ajknapp/ats-mode-indent

Best,

Andrew Knapp

[Hongwei Xi]

I gave it a try last night. I encountered many cases of excessive indentation.

The syntax of ATS is rich and complex. So it makes sense to require the programmer

to manually add indentation. With the current ats-mode, you get two spaces if you hit the

tab key. So you are pretty much in control of indentation. As far as I know, a lot of programmers

want this kind of control :)

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/ad0158e6-35c0-4a98-9aff-13d9a27578a6%40googlegroups.com.

[Andrew Knapp]

Taking a closer look, there are definitely cases I didn't use that behave strangely. As I see it, there are four causes for this.

The first is an incomplete treatment of similar constructs that should be indented the same way, e.g. datatype, dataprop, dataviewtype... I thought I had gotten this working, but I didn't test every keyword.

The second is things that indent strangely at first, but indent correctly after entering calling newline-and-indent. This behavior is mildly annoying, but it is also inherited from the original SML mode and can be fixed with semicolon usage. I'm not sure SMIE is powerful enough to eradicate this behavior.

The third is flat out bugs. For example, different styles of datatype declaration break indentation (i.e. | Foo of (a,b) vs | Foo() of (a,b)).

The fourth is my preferred indentation style, which uses much longer lines than yours. I find it painful to read such short lines of code, and so I didn't test that case very much. For example, I would write

fun {n:nat} factorial(n:int(n)): [r:int] (FACTORIAL(n,r) | int(r))

Do you have any particular examples that stood out as being incorrect? I will continue working on this for my own use, at least :)

On Thursday, October 12, 2017 at 5:58:02 AM UTC-7, gmhwxi wrote:

I gave it a try last night. I encountered many cases of excessive indentation.

The syntax of ATS is rich and complex. So it makes sense to require the programmer

to manually add indentation. With the current ats-mode, you get two spaces if you hit the

tab key. So you are pretty much in control of indentation. As far as I know, a lot of programmers

want this kind of control :)

On Wed, Oct 11, 2017 at 3:43 PM, Andrew Knapp <andy.j...@gmail.com> wrote:

Hello all,

By cannibalizing sml.el, I have largely gotten automatic indentation working in ATS.

After a few months of sporadic use, the only problem I couldn't fix is excessive indentation after a function has ended.

This can be fixed by terminating all functions with semicolons, which is ugly, but it seems to work.

If you don't do this, you have to type "fun" and then hit tab to indent properly.

Perhaps someone with more experience with programming languages can fix this, since I have no background with parsers.

(The code is based on Emacs' SMIE, which uses operator precedence grammars.)

Here is the temporary link. Let me know what I need to do to get this upstream.

https://github.com/ajknapp/ats-mode-indent

Best,

Andrew Knapp

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.

[aditya siram]

Huge thanks for working on this. It's difficult and tedious but sorely needed.

Here's some bad indentation cases I found:

      sortdef even = { i:int | i mod 2 == 0  }
                       sortdef agz = {l:addr | l > null}

implement main0 () =
          let
            ...
          in
            ...
          end

[Andrew Knapp]

Both of those test cases should work now, as well as a lot of others. Some of the weird starting errors have been fixed, especially at the top level, but it won't be possible in the general case.

Supposing you've typed

let
  val foo = 3

there is no way for the indentation engine to know whether you will next type

let
  val foo = 3
  val bar = 4

or

let
  val foo = 3
                 +baz()

The best we can hope for is indentation that is correct after the fact.

Here's the output of running indent-region on the following code. More test cases are welcome :)

#include "share/atspre_staload.hats"

#include "share/atspre_define.hats"

extern fun imul2

  {i,j:int}(i:int i,j:int j):<>

  [ij:int] (MUL(i,j,ij)|int ij) = "mac#imul2"

                                    

extern fun atoi(!strptr): int = "mac#atoi"

                                  

fun test(a:int): int = a+1

                           

typedef qwerty = int

typedef dvorak = double

                   

dataprop FACTORIAL(n:int,r:int) =

  | FACTORIAL_BAS(0,1) of ()

  | {n:nat}{r,r1:int} FACTORIAL_IND(n,r) of

    (FACTORIAL(n-1,r1), MUL(n,r1,r))

fun factorial

  {n:nat} .<>. (n:int(n)):<>

  [r:int] (FACTORIAL(n,r) | int(r)) =

let

  fun loop

  {i:nat|i <= n}

  {r:int}

  .<n-i>.

  (

    pf: FACTORIAL(i,r) |

    n:int n, i: int i, r: int r

  ):<>

  [r:int] (FACTORIAL(n,r) | int r) =

  if n-i>0 then

  let

    val (pfmul | r1) = imul2(i+1,r)

  in

    loop(FACTORIAL_IND(pf,pfmul) | n, i+1, r1)

  end

  else (pf | r)

in

  loop(FACTORIAL_BAS() | n, 0, 1)

end

fun foo(): int =

let

  fun bar(): int =

  let

    fun baz(): int =

    let

      val x = 3

      val y = 4

    in

      if x > 3 then

        x

      else

        y

    end

  in

    baz()

  end

in

  bar()

end

implement main0() = let

  val x = 3

  val (pf | res) = factorial(5)

in

  print_list($list{int}(1,2,3,4,5));

  println!(5);

  println!(res);

end

dataprop food =

  | MILK of ()

  | EGGS of ()

sortdef x = {i:int | i >= 0}

sortdef y = {i:int | i mod 2 == 0}

              

fun bar(a:int):int =

let

  val x = 3

  val y = 4

  val z = 7

in

  x*y+z

end

fun foo(): int =

let

  val x = 3

  val y = 4

  fun loop(a:int):int =

  let

    val y = 4

    val z = 7

  in

    x+3

  end

in

  if x > 3 then 5 else 8

end

[gmhwxi]

This looks good.

Could you post a video on youtube to show potential users
how to set up and then use the mode?

I will be happy to recommend it to my class.

Thanks!

[Artyom Shalkhakov]

This is awesome! I'll try it on the weekend. Thank you!

14 окт. 2017 г. 1:24 AM пользователь "Andrew Knapp" <andy.j...@gmail.com> написал:

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.

Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3aa42d9a-a59e-411a-ae7d-a7b7505fd13b%40googlegroups.com.

[aditya siram]

As a side note is there a subset of ATS syntax where indentation is unambiguous? For example a `let` with braces and semicolons:

let  {
  val x = ....;
  val y = ....;
}
in {
  ...
}

I've found languages with unambiguous indentation are really great for some spotting some kinds of bugs. Bad indentation gives you faster and better feedback than a parse error.

Thanks!

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3aa42d9a-a59e-411a-ae7d-a7b7505fd13b%40googlegroups.com.

[Andrew Knapp]

What level of knowledge should the video assume? I'm guessing these are pretty new students without much emacs experience.

I should have time to write a real README and do a brief video this weekend.

[gmhwxi]

Targeting someone with little emacs knowledge seems to be a good idea.

Basically, a few steps on installing the mode (e.g., a few lines that are needed
in the .emacs file).

In the video, you could go through the cycle of editing/compiling/fixing a short
ATS program.

Thanks!

[Andrew Knapp]

Unfortunately (or fortunately) I've discovered a few more bugs I should fix before doing the video.