Idris2: idris-generate-def on infix operator generates invalid syntax

idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.

GNU General Public License v3.0

267 stars 70 forks source link

Idris2: idris-generate-def on infix operator generates invalid syntax #572

Closed keram closed 1 year ago

keram commented 1 year ago

Generating definition for : (-) : Nat leads to:

- + Errors (1)
 `-- AddClause.idr line 13 col 0:
     Couldn't parse declaration.

     AddClause:13:1--13:2
      09 | -- Regression test for:
      10 | -- idris-add-clause doesn't send a message when cursor is on a dash
      11 | -- https://github.com/idris-community/idris2-mode/issues/16
      12 | (-) : Nat
      13 | - = 0

Current:

- = 0

Expected:

(-) = 0

output-2022-11-26-23:36:10

keram commented 1 year ago

Event log suggests that the issue is in Idris2. Will keep this for reference while fix may be done in Idris2

 -> ((:generate-def 12 "-")
 56)
<- (:return
 (:ok
  ((:show-implicits :False)
   (:show-machinenames :False)
   (:show-namespace :False)
   (:show-types :False)
   (:eval "normalise")
   (:editor "vim")))
 55)
 <- (:return
 (:ok "- = 0")
 56)

keram commented 1 year ago

It is working now as expecetd in Idris2 0.6.0-2f55a3ef8 🎉

 <- (:return (:ok "(-) = ?op_rhs") 7)