Invalid lexing of self-closing multiline comments of the form `{------}`

[Matthew-Mosior]

Preface

Please see this repo for full, complete code (an .ipkg-based project):

https://github.com/Matthew-Mosior/Pac-Man-Clone

Problem

When trying to use the exported top-level constant, topborder, from the src/Map/TopBorder.idr file, in src/Main.idr, it cannot be found (undefined name).

Steps to Reproduce

Clone https://github.com/ECburx/Idris2GL and install following direction in the README.

Clone https://github.com/Matthew-Mosior/Pac-Man-Clone.

You may also refer to the following minified code snippets below:

src/Map/TopBorder.idr

module Map.TopBorder

import IdrisGL

{-Define top border bitmap.-}

export
borderSize : Int
borderSize = 8

export
borderStartingCoor : (Int,Int)
                   -> Rect
borderStartingCoor(x,y) = MkRect x
                                 y
                                 borderSize
                                 borderSize

export
topBorder : (Int,Int)
          -> Picture
topBorder pos = Bitmap "assets/wall.bmp"
                       (borderStartingCoor pos)

{---------------------------}

{-Define top border lines.-}

export %inline 
topborder : Picture
topborder = Pictures [ topBorder (80,120)
                     , topBorder (88,120)
                     , topBorder (96,120)
                     , topBorder (104,120)
                     , topBorder (112,120)
                     , topBorder (120,120)
                     , topBorder (128,120)
                     , topBorder (136,120)
                     , topBorder (144,120)
                     , topBorder (152,120)
                     , topBorder (160,120)
                     , topBorder (168,120)
                     , topBorder (176,120)
                     , topBorder (184,120)
                     , topBorder (192,120)
                     , topBorder (200,120)
                     , topBorder (208,120)
                     , topBorder (216,120)
                     , topBorder (224,120)
                     , topBorder (232,120)
                     , topBorder (240,120)
                     , topBorder (248,120)
                     , topBorder (256,120)
                     , topBorder (264,120)
                     , topBorder (272,120)
                     , topBorder (280,120)
                     , topBorder (288,120)
                     , topBorder (296,120)
                     , topBorder (304,120)
                     , topBorder (312,120)
                     , topBorder (320,120)
                     , topBorder (328,120)
                     , topBorder (336,120)
                     ]

{--------------------------}

src/Main.idr

module Main

import Map.Pacman
import Map.TopBorder

import IdrisGL
import IdrisGL.Color as Color

main : IO ()
main = do
  let window : Display
      window = InWindow "Pac-Man Clone" (MkRect 0 0 (224*5) (288*5))
  let initmap : Picture
      initmap = Pictures [ initialpacman
                         , topborder
                         ]
  display window Color.black initmap

Expected Behavior

The program type checks and compiles using idris2 --build pacman-clone.ipkg

Observed Behavior

$ idris2 --build pacman-clone.ipkg 
2/3: Building Map.TopBorder (src/Map/TopBorder.idr)
3/3: Building Main (src/Main.idr)
Error: While processing right hand side of main. While processing right hand side
of main,haha. Undefined name topborder. 

Main:16:14--16:23
 12 | main = do
 13 |   let window : Display
 14 |       window = InWindow "Pac-Man Clone" (MkRect 0 0 (224*5) (288*5))
 15 |   let initmap : Pictture
 16 |        initmap = [ initialpacman
                       , topborder
                         ^^^^^^^^^
Did you mean: topBorder?

Fix

This code can be made to work, (big thanks to @stefan-hoeck for helping) by removing the multi-line comments in src/Map/TopBorder.idr.

[Matthew-Mosior]

@gallais

I'm still very new to understanding the internals, but I took a crack at it (could be completely off base with this) and looks like a contributing piece of this issue stems from blockComment:

blockComment : Lexer
blockComment = is '{' <+> is '-' <+> many (is '-') <+> (eof <|> toEndComment 1)

and the fact that it calls (eof <|> toEndComment 1)

given

||| `toEndComment` is the default state and it will munch through
||| the input until we detect a special character (a dash, an
||| opening brace, or a double quote) and then switch to the
||| appropriate state.
toEndComment : (k : Nat) -> Recognise (k /= 0)
toEndComment Z = empty
toEndComment (S k)
             = some (pred (\c => c /= '-' && c /= '{' && c /= '"'))
                      <+> (eof <|> toEndComment (S k))
           <|> is '{' <+> singleBrace k
           <|> is '-' <+> singleDash k
           <|> stringLit <+> toEndComment (S k)

where toEndComment will munch until it detects a special character, of which } is not one of them?

Please see https://github.com/idris-lang/Idris2/blob/main/src/Parser/Lexer/Source.idr for these functions.

[Matthew-Mosior]

Also,

 ||| After reading a single brace, we may either finish reading an
 ||| opening delimiter or ignore it (e.g. it could be an implicit
 ||| binder).
 singleBrace : (k : Nat) -> Lexer
 singleBrace k
    =  is '-' <+> many (is '-')              -- opening delimiter
              <+> (eof <|> singleDash (S k)) -- `singleDash` handles the {----} special case
                                             -- `eof` handles the file ending with {---
   <|> toEndComment (S k)                    -- not a valid comment

states singleDash handles the {----} special case

but

||| After reading a single dash, we may either find another one,
||| meaning we may have started reading a line comment, or find
||| a closing brace meaning we have found a closing delimiter.
singleDash : (k : Nat) -> Lexer
singleDash k
   =  is '-' <+> doubleDash k    -- comment or closing delimiter
  <|> is '}' <+> toEndComment k  -- closing delimiter
  <|> toEndComment (S k)         -- not a valid comment

doesn't cover non - characters?

[Matthew-Mosior]

After trying to allow for characters other than - within a self-closing multiline comment (i.e. {-abcd-}), I found a test that shows an example of named arguments that take on this form:

-- When binding arguments on LHS or listing arguments to
-- a function on RHS
-- unnamed arguments always take priority over named,
-- i.e they are bound/applied first,
-- regardless of their relative positions to named ones
testOrder1 : (a : String) -> (a : String) -> String
testOrder1 {a = a2} {-snd-} a1 {-fst-} = a1 ++ a2

Namely, {-snd-} and {-fst-}.

Thus, this feature may not be feasible to implement.

This code can be found in tests/idris2/basic049/Fld.idr.

[gallais]

Isn't the main problem that many (is '-') eats up all the dashes and then we're only seeing } instead -}? Of course we can't just fix that in the toplevel blockComment, we also need to handle it appropriately once it's nested inside an existing {- ... -} block.

[Matthew-Mosior]

@gallais I meant to look into this awhile ago, it appears now that this is no longer an issue.