[ fix #2202 ] Use SnocList in parser state to avoid quadratic slowdown (#2203)

Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>

src/Idris/IDEMode/Parser.idr

@@ -3,14 +3,14 @@
 ||| we can reuse the standard stuff
 module Idris.IDEMode.Parser
 
+import Core.Core
+import Core.FC
+
 import Protocol.SExp
 import Protocol.SExp.Parser
 
 import Parser.Source
 
-import Core.Core
-import Core.FC
-
 Cast SExpError Error where
   cast (LexError    err) = fromLexError      (Virtual Interactive) err
   cast (ParseErrors err) = fromParsingErrors (Virtual Interactive) err

src/Idris/Parser.idr

@@ -34,14 +34,14 @@ boundedNameDecoration fname decor bstr = ((fname, start bstr, end bstr)
 
 decorateBoundedNames : OriginDesc -> Decoration -> List (WithBounds Name) -> EmptyRule ()
 decorateBoundedNames fname decor bns
-  = act $ MkState (map (boundedNameDecoration fname decor) bns) []
+  = act $ MkState (cast (map (boundedNameDecoration fname decor) bns)) []
 
 decorateBoundedName : OriginDesc -> Decoration -> WithBounds Name -> EmptyRule ()
 decorateBoundedName fname decor bn = actD (boundedNameDecoration fname decor bn)
 
 decorateKeywords : OriginDesc -> List (WithBounds a) -> EmptyRule ()
 decorateKeywords fname xs
-  = act $ MkState (map (decorationFromBounded fname Keyword) xs) []
+  = act $ MkState (cast (map (decorationFromBounded fname Keyword) xs)) []
 
 dependentDecorate : OriginDesc -> Rule a -> (a -> Decoration) -> Rule a
 dependentDecorate fname rule decor = do
@@ -421,7 +421,7 @@ mutual
                      pure $
                        let fc = boundToFC fname (mergeBounds s b)
                            nilFC = if null xs then fc else boundToFC fname b
-                       in PList fc nilFC (map (\ t => (boundToFC fname t, t.val)) xs))
+                       in PList fc nilFC (cast (map (\ t => (boundToFC fname t, t.val)) xs)))
 
   snocListExpr : OriginDesc -> WithBounds () -> IndentInfo -> Rule PTerm
   snocListExpr fname s indents

src/Parser/Rule/Source.idr

@@ -7,29 +7,52 @@ import Core.Context
 import Core.TT
 import Core.Metadata
 import Data.List1
+import Data.SnocList
 import Data.String
 import Libraries.Data.List.Extra
 
 %default total
 
+||| This version of the Parser's state is parameterized over
+||| the container for SemanticDecorations. The parser should
+||| only work the ParsingState type below and after parsing
+||| is complete, use the regular State type.
 public export
-record State where
+record ParserState (container : Type -> Type) where
   constructor MkState
-  decorations : SemanticDecorations
+  decorations : container ASemanticDecoration
   holeNames : List String
 
-export
-Semigroup State where
-  MkState decs1 hs1 <+> MkState decs2 hs2
-    = MkState (decs1 ++ decs2) (hs1 ++ hs2)
+||| This state needs to provide efficient concatenation.
+public export
+ParsingState : Type
+ParsingState = ParserState SnocList
+
+||| This is the final state after parsing. We no longer
+||| need to support efficient concatenation.
+public export
+State : Type
+State = ParserState List
 
 export
-Monoid State where
-  neutral = MkState [] []
+toState : ParsingState -> State
+toState (MkState decs hs) = MkState (cast decs) hs
+
+-- To help prevent concatenation slow downs, we only
+-- provide Semigroup and Monoid for the efficient
+-- version of the ParserState.
+export
+Semigroup ParsingState where
+  MkState decs1 hs1 <+> MkState decs2 hs2
+    = MkState (decs1 <+> decs2) (hs1 ++ hs2)
+
+export
+Monoid ParsingState where
+  neutral = MkState [<] []
 
 public export
 BRule : Bool -> Type -> Type
-BRule = Grammar State Token
+BRule = Grammar ParsingState Token
 
 public export
 Rule : Type -> Type
@@ -41,11 +64,11 @@ EmptyRule = BRule False
 
 export
 actD : ASemanticDecoration -> EmptyRule ()
-actD s = act (MkState [s] [])
+actD s = act (MkState [<s] [])
 
 export
 actH : String -> EmptyRule ()
-actH s = act (MkState [] [s])
+actH s = act (MkState [<] [s])
 
 export
 eoi : EmptyRule ()

src/Parser/Source.idr

@@ -17,7 +17,7 @@ export
 runParserTo : {e : _} ->
               (origin : OriginDesc) ->
               Maybe LiterateStyle -> Lexer ->
-              String -> Grammar State Token e ty ->
+              String -> Grammar ParsingState Token e ty ->
               Either Error (List Warning, State, ty)
 runParserTo origin lit reject str p
     = do str        <- mapFst (fromLitError origin) $ unlit lit str
@@ -28,12 +28,14 @@ runParserTo origin lit reject str p
          let ws = ws <&> \ (mb, warn) =>
                     let mkFC = \ b => MkFC origin (startBounds b) (endBounds b)
                     in ParserWarning (maybe EmptyFC mkFC mb) warn
-         Right (ws, { decorations $= (cs ++) } decs, parsed)
+         let state : State
+             state = { decorations $= (cs++) } (toState decs)
+         pure (ws, state, parsed)
 
 export
 runParser : {e : _} ->
             (origin : OriginDesc) -> Maybe LiterateStyle -> String ->
-            Grammar State Token e ty ->
+            Grammar ParsingState Token e ty ->
             Either Error (List Warning, State, ty)
 runParser origin lit = runParserTo origin lit (pred $ const False)
 

src/Protocol/SExp/Parser.idr

@@ -86,7 +86,7 @@ data SExpError =
   | ParseErrors (List1 $ ParsingError Token)
 
 ideParser : {e : _} ->
-            String -> Grammar State Token e ty -> Either SExpError ty
+            String -> Grammar ParsingState Token e ty -> Either SExpError ty
 ideParser str p
     = do toks   <- mapFst LexError $ idelex str
          (_, _, (parsed, _)) <- mapFst ParseErrors $ parseWith p toks

tests/Main.idr

@@ -124,7 +124,8 @@ idrisTestsPerformance = MkTestPool "Performance" [] Nothing
        -- Performance: things which have been slow in the past, or which
        -- pose interesting challenges for the elaborator
       ["perf001", "perf002", "perf003", "perf004", "perf005",
-       "perf007", "perf008", "perf009", "perf010", "perf011"]
+       "perf007", "perf008", "perf009", "perf010", "perf011",
+       "perf2202"]
 
 idrisTestsRegression : TestPool
 idrisTestsRegression = MkTestPool "Various regressions" [] Nothing

tests/idris2/perf2202/expected

@@ -0,0 +1,2 @@
+1/1: Building many10000 (many10000.idr)
+1/1: Building Church (Church.idr)

tests/idris2/perf2202/run

@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --check many10000.idr
+$1 --no-color --console-width 0 --check Church.idr