Error when searching for type, documentation

[archaeron]

In

plusAssoc : (l, c, r : Nat) -> l `plus` (c `plus` r) = (l `plus` c) `plus` r
plusAssoc Z c r = Refl
plusAssoc (S l) c r = rewrite plusAssoc l c r in Refl

select Nat and do a typesearch.

The package will send Nat) to Idris, resulting in the type not being found.

[david-christiansen]

That's interesting. When I type search Nat) over the IDE protocol in Emacs, I get:

= Prelude.Nat.Z : Nat
Zero

< Prelude.Classes.minBound : MinBound b => b
The lower bound for the type

The internal communication is:

23:03:09 -> ((:interpret ":search Nat)")
 94)
23:03:09 <- (:output
 (:ok
  (:highlight-source
   ((((:filename "(input)")
      (:start 1 9)
      (:end 1 12))
     ((:name "Prelude.Nat.Nat")
      (:implicit :False)
      (:decor :type)
      (:doc-overview "Unary natural numbers")
      (:type "Type")
      (:namespace "Prelude.Nat"))))))
 94)
23:03:09 <- (:return
 (:ok "= Prelude.Nat.Z : Nat\nZero\n\n< Prelude.Classes.minBound : MinBound b => b\nThe lower bound for the type\n"
      ((0 1
          ((:doc-overview "Result type is isomorphic")))
       (2 13
          ((:name "Prelude.Nat.Z")
           (:implicit :False)
           (:decor :data)
           (:doc-overview "Zero")
           (:type "Nat")
           (:namespace "Prelude.Nat")))
       (18 3
           ((:name "Prelude.Nat.Nat")
            (:implicit :False)
            (:decor :type)
            (:doc-overview "Unary natural numbers")
            (:type "Type")
            (:namespace "Prelude.Nat")))
       (28 1
           ((:doc-overview "Result type is more general than searched type")))
       (30 24
           ((:name "Prelude.Classes.minBound")
            (:implicit :False)
            (:decor :function)
            (:doc-overview "The lower bound for the type")
            (:type "MinBound b => b")
            (:namespace "Prelude.Classes")))
       (57 8
           ((:name "Prelude.Classes.MinBound")
            (:implicit :False)
            (:decor :type)
            (:doc-overview "")
            (:type "Type -> Type")
            (:namespace "Prelude.Classes")))
       (66 1
           ((:name "b")
            (:decor :bound)
            (:implicit :True)))
       (71 1
           ((:name "b")
            (:decor :bound)
            (:implicit :True)))))
 94)

I would actually expect a parse error, rather than getting this back.

[jeremy-w]

Sounds like an issue with getWordUnderCursor. The getCurrentWordBufferRange() defaults to ::wordRegex, which has an option .includeNonWordCharacters that defaults to true.

Supplying a regex that would match only valid Idris words to getCurrentWordBufferRange(), rather than accepting the default, would likely fix this issue.

[archaeron]

thanks for your pointers, this is helping a lot.
apparently this is the default regex:

/^[  ]*$|[^\s\/\\\(\)"':,\.;<>~!@#\$%\^&\*\|\+=\[\]\{\}`\?\-…]+|[\/\\\(\)"':,\.;<>~!@#\$%\^&\*\|\+=\[\]\{\}`\?\-…]+/g

I just need to understand what it does and change it accordingly :D

[archaeron]

looks fixed. it might need some tweaking, but in my short tests it selected just the Nat in Nat)
and works for things with primes (e.g. abc') too.

thanks @jeremy-w