<commit_before>module Idris.REPLParser(parseCmd) where

import System.FilePath ((</>))

import Idris.Parser
import Idris.AbsSyntax
import Core.TT

import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Expr
import Text.ParserCombinators.Parsec.Language
import qualified Text.ParserCombinators.Parsec.Token as PTok

import Debug.Trace
import Data.List
import Data.List.Split(splitOn)

parseCmd i = runParser pCmd i "(input)"

cmd :: [String] -> IParser ()
cmd xs = do lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)
    where docmd [] = fail "No such command"
          docmd (x:xs) = try (discard (symbol x)) <|> docmd xs

pCmd :: IParser Command
pCmd = try (do cmd ["q", "quit"]; eof; return Quit)
   <|> try (do cmd ["h", "?", "help"]; eof; return Help)
   <|> try (do cmd ["r", "reload"]; eof; return Reload)
   <|> try (do cmd ["m", "module"]; f <- identifier; eof;
               return (ModImport (toPath f)))
   <|> try (do cmd ["e", "edit"]; eof; return Edit)
   <|> try (do cmd ["exec", "execute"]; eof; return Execute)
   <|> try (do cmd ["ttshell"]; eof; return TTShell)
   <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile ViaC f))
   <|> try (do cmd ["jc", "newcompile"]; f <- identifier; eof; return (Compile ViaJava f))
   <|> try (do cmd ["js", "javascript"]; f <- identifier; eof; return (Compile ViaJavaScript f))
   <|> try (do cmd ["m", "metavars"]; eof; return Metavars)
   <|> try (do cmd ["proofs"]; eof; return Proofs)
   <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))
   <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- pName;
                                                                 return (Just x))
                                         eof; return (AddProof n))
   <|> try (do cmd ["rmproof"]; n <- pName; eof; return (RmProof n))
   <|> try (do cmd ["showproof"]; n <- pName; eof; return (ShowProof n))
   <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))
   <|> try (do cmd ["l", "load"]; f <- getInput; return (Load f))
   <|> try (do cmd ["cd"]; f <- getInput; return (ChangeDirectory f))
   <|> try (do cmd ["spec"]; t <- pFullExpr defaultSyntax; return (Spec t))
   <|> try (do cmd ["hnf"]; t <- pFullExpr defaultSyntax; return (HNF t))
   <|> try (do cmd ["doc"]; n <- pfName; eof; return (DocStr n))
   <|> try (do cmd ["d", "def"]; many1 (char ' ') ; n <- pfName; eof; return (Defn n))
   <|> try (do cmd ["total"]; do n <- pfName; eof; return (TotCheck n))
   <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))
   <|> try (do cmd ["u", "universes"]; eof; return Universes)
   <|> try (do cmd ["di", "dbginfo"]; n <- pfName; eof; return (DebugInfo n))
   <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))
   <|> try (do cmd ["miss", "missing"]; n <- pfName; eof; return (Missing n))
   <|> try (do cmd ["dynamic"]; eof; return ListDynamic)
   <|> try (do cmd ["dynamic"]; l <- getInput; return (DynamicLink l))
   <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))
   <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))
   <|> try (do cmd ["s", "search"]; t <- pFullExpr defaultSyntax; return (Search t))
   <|> try (do cmd ["x"]; t <- pFullExpr defaultSyntax; return (ExecVal t))
   <|> try (do cmd ["patt"]; t <- pFullExpr defaultSyntax; return (Pattelab t))
   <|> do t <- pFullExpr defaultSyntax; return (Eval t)
   <|> do eof; return NOP

 where toPath n = foldl1' (</>) $ splitOn "." n

pOption :: IParser Opt
pOption = do discard (symbol "errorcontext"); return ErrContext
      <|> do discard (symbol "showimplicits"); return ShowImpl
<commit_msg>Ignore initial whitespace and comments in REPL<commit_after>module Idris.REPLParser(parseCmd) where

import System.FilePath ((</>))

import Idris.Parser
import Idris.AbsSyntax
import Core.TT

import Text.ParserCombinators.Parsec
import Text.ParserCombinators.Parsec.Expr
import Text.ParserCombinators.Parsec.Language
import qualified Text.ParserCombinators.Parsec.Token as PTok

import Debug.Trace
import Data.List
import Data.List.Split(splitOn)

parseCmd i = runParser pCmd i "(input)"

cmd :: [String] -> IParser ()
cmd xs = do lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)
    where docmd [] = fail "No such command"
          docmd (x:xs) = try (discard (symbol x)) <|> docmd xs

pCmd :: IParser Command
pCmd = do spaces; try (do cmd ["q", "quit"]; eof; return Quit)
              <|> try (do cmd ["h", "?", "help"]; eof; return Help)
              <|> try (do cmd ["r", "reload"]; eof; return Reload)
              <|> try (do cmd ["m", "module"]; f <- identifier; eof;
                          return (ModImport (toPath f)))
              <|> try (do cmd ["e", "edit"]; eof; return Edit)
              <|> try (do cmd ["exec", "execute"]; eof; return Execute)
              <|> try (do cmd ["ttshell"]; eof; return TTShell)
              <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile ViaC f))
              <|> try (do cmd ["jc", "newcompile"]; f <- identifier; eof; return (Compile ViaJava f))
              <|> try (do cmd ["js", "javascript"]; f <- identifier; eof; return (Compile ViaJavaScript f))
              <|> try (do cmd ["m", "metavars"]; eof; return Metavars)
              <|> try (do cmd ["proofs"]; eof; return Proofs)
              <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))
              <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- pName;
                                                                            return (Just x))
                                                    eof; return (AddProof n))
              <|> try (do cmd ["rmproof"]; n <- pName; eof; return (RmProof n))
              <|> try (do cmd ["showproof"]; n <- pName; eof; return (ShowProof n))
              <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))
              <|> try (do cmd ["l", "load"]; f <- getInput; return (Load f))
              <|> try (do cmd ["cd"]; f <- getInput; return (ChangeDirectory f))
              <|> try (do cmd ["spec"]; whiteSpace; t <- pFullExpr defaultSyntax; return (Spec t))
              <|> try (do cmd ["hnf"]; whiteSpace; t <- pFullExpr defaultSyntax; return (HNF t))
              <|> try (do cmd ["doc"]; n <- pfName; eof; return (DocStr n))
              <|> try (do cmd ["d", "def"]; many1 (char ' ') ; n <- pfName; eof; return (Defn n))
              <|> try (do cmd ["total"]; do n <- pfName; eof; return (TotCheck n))
              <|> try (do cmd ["t", "type"]; do whiteSpace; t <- pFullExpr defaultSyntax; return (Check t))
              <|> try (do cmd ["u", "universes"]; eof; return Universes)
              <|> try (do cmd ["di", "dbginfo"]; n <- pfName; eof; return (DebugInfo n))
              <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))
              <|> try (do cmd ["miss", "missing"]; n <- pfName; eof; return (Missing n))
              <|> try (do cmd ["dynamic"]; eof; return ListDynamic)
              <|> try (do cmd ["dynamic"]; l <- getInput; return (DynamicLink l))
              <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o))
              <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))
              <|> try (do cmd ["s", "search"]; whiteSpace; t <- pFullExpr defaultSyntax; return (Search t))
              <|> try (do cmd ["x"]; whiteSpace; t <- pFullExpr defaultSyntax; return (ExecVal t))
              <|> try (do cmd ["patt"]; whiteSpace; t <- pFullExpr defaultSyntax; return (Pattelab t))
              <|> do whiteSpace; do eof; return NOP
                             <|> do t <- pFullExpr defaultSyntax; return (Eval t)

 where toPath n = foldl1' (</>) $ splitOn "." n

pOption :: IParser Opt
pOption = do discard (symbol "errorcontext"); return ErrContext
      <|> do discard (symbol "showimplicits"); return ShowImpl

{'fraction_non_alphanumeric': 0.17962870045158053, 'fraction_numerical': 0.0005017561465127947, 'mean_word_length': 2.610960144927536, 'pattern_counts': {'":': 0, '<': 141, '<?xml version=': 0, '>': 89, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 10, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4590745', 'n_tokens_mistral': 2690, 'n_tokens_neox': 2509, 'n_words': 944}