Merge pull request #178 from edwinb/performance

Performance

libs/prelude/Prelude.idr

@@ -1439,6 +1439,7 @@ public export
 Functor IO where
   map f io = io_bind io (\b => io_pure (f b))
 
+%inline
 public export
 Applicative IO where
   pure x = io_pure x

src/Core/Unify.idr

@@ -1335,7 +1335,7 @@ retry mode c
                              _ => pure cs
   where
     definedN : Name -> Core Bool
-    definedN n
+    definedN n@(NS _ (MN _ _)) -- a metavar will only ever be a MN
         = do defs <- get Ctxt
              Just gdef <- lookupCtxtExact n (gamma defs)
                   | _ => pure False
@@ -1344,6 +1344,7 @@ retry mode c
                   BySearch _ _ _ => pure False
                   Guess _ _ _ => pure False
                   _ => pure True
+    definedN _ = pure True
 
 delayMeta : {vars : _} ->
             LazyReason -> Nat -> Term vars -> Term vars -> Term vars

src/Idris/Parser.idr

@@ -49,13 +49,17 @@ plhs = MkParseOpts False False
 atom : FileName -> Rule PTerm
 atom fname
     = do start <- location
-         x <- constant
-         end <- location
-         pure (PPrimVal (MkFC fname start end) x)
-  <|> do start <- location
          exactIdent "Type"
          end <- location
          pure (PType (MkFC fname start end))
+  <|> do start <- location
+         x <- name
+         end <- location
+         pure (PRef (MkFC fname start end) x)
+  <|> do start <- location
+         x <- constant
+         end <- location
+         pure (PPrimVal (MkFC fname start end) x)
   <|> do start <- location
          symbol "_"
          end <- location
@@ -80,10 +84,6 @@ atom fname
          pragma "search"
          end <- location
          pure (PSearch (MkFC fname start end) 50)
-  <|> do start <- location
-         x <- name
-         end <- location
-         pure (PRef (MkFC fname start end) x)
 
 whereBlock : FileName -> Int -> Rule (List PDecl)
 whereBlock fname col

src/Parser/Support.idr

@@ -155,23 +155,23 @@ escape' ('\\' :: 'o' :: xs)
 escape' ('\\' :: xs)
     = case span isDigit xs of
            ([], (a :: b :: c :: rest)) =>
-               case getEsc (pack (the (List _) [a, b, c])) of
+               case getEsc (fastPack (the (List _) [a, b, c])) of
                    Just v => Just (v :: !(assert_total (escape' rest)))
-                   Nothing => case getEsc (pack (the (List _) [a, b])) of
+                   Nothing => case getEsc (fastPack (the (List _) [a, b])) of
                                    Just v => Just (v :: !(assert_total (escape' (c :: rest))))
                                    Nothing => escape' xs
            ([], (a :: b :: [])) =>
-               case getEsc (pack (the (List _) [a, b])) of
+               case getEsc (fastPack (the (List _) [a, b])) of
                    Just v => Just (v :: [])
                    Nothing => escape' xs
            ([], rest) => assert_total (escape' rest)
-           (ds, rest) => Just $ cast (cast {to=Int} (pack ds)) ::
+           (ds, rest) => Just $ cast (cast {to=Int} (fastPack ds)) ::
                                  !(assert_total (escape' rest))
 escape' (x :: xs) = Just $ x :: !(escape' xs)
 
 export
 escape : String -> Maybe String
-escape x = pure $ pack !(escape' (unpack x))
+escape x = pure $ fastPack !(escape' (unpack x))
 
 export
 getCharLit : String -> Maybe Char

src/Text/Lexer/Core.idr

@@ -168,23 +168,11 @@ tokenise pred line col acc tmap str
     getFirstToken [] str = Nothing
     getFirstToken ((lex, fn) :: ts) str
         = case scan lex [] str of
-               Just (tok, rest) => Just (MkToken line col (fn (pack (reverse tok))),
+               Just (tok, rest) => Just (MkToken line col (fn (fastPack (reverse tok))),
                                          line + cast (countNLs tok),
                                          getCols tok col, rest)
                Nothing => getFirstToken ts str
 
--- faster than the prelude version since there's no intermediate StrM
-funpack' : String -> List Char -> List Char
-funpack' "" acc = reverse acc
-funpack' str acc
-    = assert_total $
-        let x = prim__strHead str
-            xs = prim__strTail str in
-            funpack' xs (x :: acc)
-
-funpack : String -> List Char
-funpack str = funpack' str []
-
 ||| Given a mapping from lexers to token generating functions (the
 ||| TokenMap a) and an input string, return a list of recognised tokens,
 ||| and the line, column, and remainder of the input at the first point in the
@@ -193,11 +181,11 @@ export
 lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
 lex tmap str
     = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (unpack str) in
-          (ts, (l, c, pack str'))
+          (ts, (l, c, fastPack str'))
 
 export
 lexTo : (TokenData a -> Bool) ->
         TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
 lexTo pred tmap str
     = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (unpack str) in
-          (ts, (l, c, pack str'))
+          (ts, (l, c, fastPack str'))

src/Text/Parser/Core.idr

@@ -38,7 +38,7 @@ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
 ||| guaranteed to consume some input. If the first one consumes input, the
 ||| second is allowed to be recursive (because it means some input has been
 ||| consumed and therefore the input is smaller)
-export -- %inline
+export %inline
 (>>=) : {c1, c2 : Bool} ->
         Grammar tok c1 a ->
         inf c1 (a -> Grammar tok c2 b) ->
@@ -49,7 +49,7 @@ export -- %inline
 ||| Sequence two grammars. If either consumes some input, the sequence is
 ||| guaranteed to consume input. This is an explicitly non-infinite version
 ||| of `>>=`.
-export
+export %inline
 seq : {c1,c2 : Bool} ->
       Grammar tok c1 a ->
       (a -> Grammar tok c2 b) ->
@@ -57,7 +57,7 @@ seq : {c1,c2 : Bool} ->
 seq = SeqEmpty
 
 ||| Sequence a grammar followed by the grammar it returns.
-export
+export %inline
 join : {c1,c2 : Bool} ->
        Grammar tok c1 (Grammar tok c2 a) ->
        Grammar tok (c1 || c2) a
@@ -66,7 +66,7 @@ join {c1 = True} p = SeqEat p id
 
 ||| Give two alternative grammars. If both consume, the combination is
 ||| guaranteed to consume.
-export
+export %inline
 (<|>) : {c1,c2 : Bool} -> 
         Grammar tok c1 ty ->
         Lazy (Grammar tok c2 ty) ->
@@ -94,7 +94,7 @@ Functor (Grammar tok c) where
 ||| with value type `a`. If both succeed, apply the function
 ||| from the first grammar to the value from the second grammar.
 ||| Guaranteed to consume if either grammar consumes.
-export
+export %inline
 (<*>) : {c1, c2 : Bool} ->
         Grammar tok c1 (a -> b) ->
         Grammar tok c2 a ->
@@ -103,7 +103,7 @@ export
 
 ||| Sequence two grammars. If both succeed, use the value of the first one.
 ||| Guaranteed to consume if either grammar consumes.
-export
+export %inline
 (<*) : {c1,c2 : Bool} ->
        Grammar tok c1 a ->
        Grammar tok c2 b ->
@@ -112,7 +112,7 @@ export
 
 ||| Sequence two grammars. If both succeed, use the value of the second one.
 ||| Guaranteed to consume if either grammar consumes.
-export
+export %inline
 (*>) : {c1,c2 : Bool} ->
        Grammar tok c1 a ->
        Grammar tok c2 b ->
@@ -135,82 +135,66 @@ mapToken f (SeqEmpty act next) = SeqEmpty (mapToken f act) (\x => mapToken f (ne
 mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y)
 
 ||| Always succeed with the given value.
-export
+export %inline
 pure : (val : ty) -> Grammar tok False ty
 pure = Empty
 
 ||| Check whether the next token satisfies a predicate
-export
+export %inline
 nextIs : String -> (tok -> Bool) -> Grammar tok False tok
 nextIs = NextIs
 
 ||| Look at the next token in the input
-export
+export %inline
 peek : Grammar tok False tok
 peek = nextIs "Unrecognised token" (const True)
 
 ||| Succeeds if running the predicate on the next token returns Just x,
 ||| returning x. Otherwise fails.
-export
+export %inline
 terminal : String -> (tok -> Maybe a) -> Grammar tok True a
 terminal = Terminal
 
 ||| Always fail with a message
-export
+export %inline
 fail : String -> Grammar tok c ty
 fail = Fail False
 
-export
+export %inline
 fatalError : String -> Grammar tok c ty
 fatalError = Fail True
 
 ||| Succeed if the input is empty
-export
+export %inline
 eof : Grammar tok False ()
 eof = EOF
 
 ||| Commit to an alternative; if the current branch of an alternative
 ||| fails to parse, no more branches will be tried
-export
+export %inline
 commit : Grammar tok False ()
 commit = Commit
 
 ||| If the parser fails, treat it as a fatal error
-export
+export %inline
 mustWork : {c : Bool} -> Grammar tok c ty -> Grammar tok c ty
 mustWork = MustWork
 
-data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
+data ParseResult : Type -> Type -> Type where
-     Failure : {xs : List tok} ->
+     Failure : (committed : Bool) -> (fatal : Bool) ->
-               (committed : Bool) -> (fatal : Bool) ->
+               (err : String) -> (rest : List tok) -> ParseResult tok ty
-               (err : String) -> (rest : List tok) -> ParseResult xs c ty
+     Res : (committed : Bool) ->
-     EmptyRes : (committed : Bool) ->
+           (val : ty) -> (more : List tok) -> ParseResult tok ty
-                (val : ty) -> (more : List tok) -> ParseResult more False ty
-     NonEmptyRes : {xs : List tok} ->
-                   (committed : Bool) ->
-                   (val : ty) -> (more : List tok) ->
-                   ParseResult (x :: xs ++ more) c ty
-
--- Take the result of an alternative branch, reset the commit flag to
--- the commit flag from the outer alternative, and weaken the 'consumes'
--- flag to take both alternatives into account
-weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
-            (com' : Bool) ->
-						ParseResult xs c ty -> ParseResult xs (whatever && c) ty
-weakenRes com' (Failure com fatal msg ts) = Failure com' fatal msg ts
-weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs
-weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs
-weakenRes com' (NonEmptyRes com val more) = NonEmptyRes com' val more
 
 mutual
   doParse : (commit : Bool) -> 
             (act : Grammar tok c ty) ->
             (xs : List tok) -> 
-            ParseResult xs c ty
+            ParseResult tok ty
-  doParse com (Empty val) xs = EmptyRes com val xs
+  doParse com (Empty val) xs = Res com val xs
   doParse com (Fail fatal str) [] = Failure com fatal str []
   doParse com (Fail fatal str) (x :: xs) = Failure com fatal str (x :: xs)
-  doParse com Commit xs = EmptyRes True () xs
+  doParse com Commit xs = Res True () xs
   doParse com (MustWork g) xs =
       let p' = assert_total (doParse com g xs) in
         case p' of
@@ -220,14 +204,14 @@ mutual
   doParse com (Terminal err f) (x :: xs)
         = case f x of
                Nothing => Failure com False err (x :: xs)
-               Just a => NonEmptyRes com {xs=[]} a xs
+               Just a => Res com a xs
-  doParse com EOF [] = EmptyRes com () []
+  doParse com EOF [] = Res com () []
   doParse com EOF (x :: xs)
         = Failure com False "Expected end of input" (x :: xs)
   doParse com (NextIs err f) [] = Failure com False "End of input" []
   doParse com (NextIs err f) (x :: xs)
         = if f x
-             then EmptyRes com x (x :: xs)
+             then Res com x (x :: xs)
              else Failure com False err (x :: xs)
   doParse com (Alt {c1} {c2} x y) xs
       = case doParse False x xs of
@@ -236,40 +220,23 @@ mutual
                           -- If the alternative had committed, don't try the
                           -- other branch (and reset commit flag)
                      then Failure com fatal msg ts
-                     else weakenRes {whatever = c1} com (assert_total (doParse False y xs))
+                     else assert_total (doParse False y xs)
 -- Successfully parsed the first option, so use the outer commit flag
-             EmptyRes _ val xs => EmptyRes com val xs
+             Res _ val xs => Res com val xs
-             NonEmptyRes {xs=xs'} _ val more => NonEmptyRes {xs=xs'} com val more
+  doParse com (SeqEmpty act next) xs
-  doParse com (SeqEmpty {c1} {c2} act next) xs
+      = case assert_total (doParse com act xs) of
-      = case assert_total (doParse {c=c1} com act xs) of
              Failure com fatal msg ts => Failure com fatal msg ts
-             EmptyRes com val xs =>
+             Res com val xs =>
                    case assert_total (doParse com (next val) xs) of
                         Failure com' fatal msg ts => Failure com' fatal msg ts
-                        EmptyRes com' val xs => EmptyRes com' val xs
+                        Res com' val xs => Res com' val xs
-                        NonEmptyRes {xs=xs'} com' val more =>
+  doParse com (SeqEat act next) xs
-                                         NonEmptyRes {xs=xs'} com' val more
+      = case assert_total (doParse com act xs) of
-             NonEmptyRes {x} {xs=ys} com val more =>
+             Failure com fatal msg ts => Failure com fatal msg ts
-                   case assert_total (doParse com (next val) more) of
+             Res com val xs =>
+                   case assert_total (doParse com (next val) xs) of
                         Failure com' fatal msg ts => Failure com' fatal msg ts
-                        EmptyRes com' val _ => NonEmptyRes {xs=ys} com' val more
+                        Res com' val xs => Res com' val xs
-                        NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
-                             rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
-                                     NonEmptyRes {xs = ys ++ (x1 :: xs1)} com' val more'
-  doParse com (SeqEat act next) xs with (doParse com act xs)
-    doParse com (SeqEat act next) xs | Failure com' fatal msg ts
-         = Failure com' fatal msg ts
-    doParse com (SeqEat act next) (x :: (ys ++ more)) | (NonEmptyRes {xs=ys} com' val more)
-         = let p' = assert_total (doParse com' (next val) more) in
-               case p' of -- doParse com' (next val) more of
-                Failure com' fatal msg ts => Failure com' fatal msg ts
-                EmptyRes com' val _ => NonEmptyRes {xs=ys} com' val more
-                NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
-                     rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
-                             NonEmptyRes {xs = ys ++ (x1 :: xs1)} com' val more'
-  -- This next line is not strictly necessary, but it stops the coverage
-  -- checker taking a really long time and eating lots of memory...
-  -- doParse _ _ _ = Failure True True "Help the coverage checker!" []
 
 public export
 data ParsingError tok = Error String (List tok)
@@ -283,5 +250,4 @@ parse : {c : Bool} -> (act : Grammar tok c ty) -> (xs : List tok) ->
 parse act xs
     = case doParse False act xs of
            Failure _ _ msg ts => Left (Error msg ts)
-           EmptyRes _ val rest => pure (val, rest)
+           Res _ val rest => pure (val, rest)
-           NonEmptyRes _ val rest => pure (val, rest)