<commit_before>{-# LANGUAGE PatternGuards #-}

module Idris.Parser where

import Idris.AbsSyntax
import Idris.DSL
import Idris.Imports
import Idris.Error
import Idris.ElabDecls
import Idris.ElabTerm
import Idris.Coverage
import Idris.IBC
import Idris.Unlit
import Paths_idris

import Core.CoreParser
import Core.TT
import Core.Evaluate

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

import Data.List
import Control.Monad.State
import Debug.Trace
import Data.Maybe
import System.FilePath

type TokenParser a = PTok.TokenParser a

type IParser = GenParser Char IState

lexer :: TokenParser IState
lexer  = PTok.makeTokenParser idrisDef

whiteSpace= PTok.whiteSpace lexer
lexeme    = PTok.lexeme lexer
symbol    = PTok.symbol lexer
natural   = PTok.natural lexer
parens    = PTok.parens lexer
semi      = PTok.semi lexer
comma     = PTok.comma lexer
identifier= PTok.identifier lexer
reserved  = PTok.reserved lexer
operator  = PTok.operator lexer
reservedOp= PTok.reservedOp lexer
integer   = PTok.integer lexer
float     = PTok.float lexer
strlit    = PTok.stringLiteral lexer
chlit     = PTok.charLiteral lexer
lchar = lexeme.char

-- Loading modules

loadModule :: FilePath -> Idris String
loadModule f 
   = idrisCatch (do i <- getIState
                    ibcsd <- valIBCSubDir i
                    ids <- allImportDirs i
                    fp <- liftIO $ findImport ids ibcsd f
                    if (f `elem` imported i)
                       then iLOG $ "Already read " ++ f
                       else do putIState (i { imported = f : imported i })
                               case fp of
                                   IDR fn  -> loadSource False fn
                                   LIDR fn -> loadSource True  fn
                                   IBC fn src -> 
                                     idrisCatch (loadIBC fn)
                                                (\c -> do iLOG $ fn ++ " failed " ++ show c
                                                          case src of
                                                            IDR sfn -> loadSource False sfn
                                                            LIDR sfn -> loadSource True sfn)
                    let (dir, fh) = splitFileName f
                    return (dropExtension fh))
                (\e -> do let msg = show e
                          setErrLine (getErrLine msg)
                          iputStrLn msg
                          return "")

loadSource :: Bool -> FilePath -> Idris () 
loadSource lidr f 
             = do iLOG ("Reading " ++ f)
                  file_in <- liftIO $ readFile f
                  file <- if lidr then tclift $ unlit f file_in else return file_in
                  (mname, modules, rest, pos) <- parseImports f file
                  i <- getIState
                  putIState (i { default_access = Hidden })
                  mapM_ loadModule modules
                  clearIBC -- start a new .ibc file
                  mapM_ (\m -> addIBC (IBCImport m)) modules
                  ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname }) 
                                   f rest pos
                  let ds = namespaces mname ds'
                  logLvl 3 (dumpDecls ds)
                  i <- getIState
                  logLvl 10 (show (toAlist (idris_implicits i)))
                  logLvl 3 (show (idris_infixes i))
                  -- Now add all the declarations to the context
                  v <- verbose
                  when v $ iputStrLn $ "Type checking " ++ f
                  mapM_ (elabDecl toplevel) ds
                  i <- get
                  mapM_ checkDeclTotality (idris_totcheck i)
                  iLOG ("Finished " ++ f)
                  ibcsd <- valIBCSubDir i
                  let ibc = ibcPathNoFallback ibcsd f
                  iucheck
                  i <- getIState
                  addHides (hide_list i)
                  ok <- noErrors
                  when ok $
                    idrisCatch (do writeIBC f ibc; clearIBC)
                               (\c -> return ()) -- failure is harmless
                  i <- getIState
                  putIState (i { hide_list = [] })
                  return ()
  where
    namespaces []     ds = ds
    namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]

addHides :: [(Name, Maybe Accessibility)] -> Idris ()
addHides xs = do i <- getIState
                 let defh = default_access i
                 let (hs, as) = partition isNothing xs
                 if null as then return ()
                            else mapM_ doHide
                                    (map (\ (n, _) -> (n, defh)) hs ++
                                     map (\ (n, Just a) -> (n, a)) as)
  where isNothing (_, Nothing) = True
        isNothing _            = False

        doHide (n, a) = do setAccessibility n a
                           addIBC (IBCAccess n a)

parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"
parseTac i = runParser (do t <- pTactic defaultSyntax
                           eof
                           return t) i "(proof)"

parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
parseImports fname input 
    = do i <- get
         case (runParser (do whiteSpace
                             mname <- pHeader
                             ps <- many pImport
                             rest <- getInput
                             pos <- getPosition
                             return ((mname, ps, rest, pos), i)) i fname input) of
            Left err -> fail (show err)
            Right (x, i) -> do put i
                               return x
  where ishow err = let ln = sourceLine (errorPos err) in
                        fname ++ ":" ++ show ln ++ ":parse error"
--                            ++ show (map messageString (errorMessages err))

pHeader :: IParser [String]
pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
                  return (parseName i))
     <|> return []
  where parseName x = case span (/='.') x of
                            (x, "") -> [x]
                            (x, '.':y) -> x : parseName y

push_indent :: IParser ()
push_indent = do pos <- getPosition
                 ist <- getState
                 setState (ist { indent_stack = sourceColumn pos :
                                                indent_stack ist })

last_indent :: IParser Int
last_indent = do ist <- getState
                 case indent_stack ist of
                    (x : xs) -> return x
                    _ -> return 1

indent :: IParser Int
indent = do pos <- getPosition
            return (sourceColumn pos)

pop_indent :: IParser ()
pop_indent = do ist <- getState
                let (x : xs) = indent_stack ist
                setState (ist { indent_stack = xs })

open_block :: IParser ()
open_block = do lchar '{'
                ist <- getState
                setState (ist { brace_stack = Nothing : brace_stack ist })
         <|> do ist <- getState
                lvl <- indent
                setState (ist { brace_stack = Just lvl : brace_stack ist })

close_block :: IParser ()
close_block = do ist <- getState
                 bs <- case brace_stack ist of
                         Nothing : xs -> do lchar '}'
                                            return xs
                         Just lvl : xs -> do i <- indent
                                             inp <- getInput
--                                              trace (show (take 10 inp, i, lvl)) $
                                             if (i >= lvl && take 1 inp /= ")") 
                                                then fail "Not end of block"
                                                else return xs
                 setState (ist { brace_stack = bs })

pTerminator = do lchar ';'; pop_indent
          <|> do c <- indent; l <- last_indent
                 if (c <= l) then pop_indent
                             else fail "Not a terminator"
          <|> do i <- getInput; if (take 1 i == "}" || take 1 i == ")") then pop_indent 
                                                     else fail "Not a terminator"
          <|> lookAhead eof

pBarTerminator 
            = do lchar '|'; return ()
          <|> do c <- indent; l <- last_indent
                 if (c <= l) then return ()
                             else fail "Not a terminator"
          <|> lookAhead eof

pKeepTerminator 
            = do lchar ';'; return ()
          <|> do c <- indent; l <- last_indent
                 if (c <= l) then return ()
                             else fail "Not a terminator"
          <|> do i <- getInput; let h = take 1 i
                 if (h == "}" || h == ")" || h == "|") then return ()
                                           else fail "Not a terminator"
          <|> lookAhead eof

notEndApp = do c <- indent; l <- last_indent
               i <- getInput
               if (c <= l) then fail "Terminator"
                           else return ()

notEndBlock = do ist <- getState
                 case brace_stack ist of
                    Just lvl : xs -> do i <- indent
                                        inp <- getInput
                                        if (i < lvl || take 1 inp == ")")
                                                     then fail "End of block"
                                                     else return ()
                    _ -> return ()

pfc :: IParser FC
pfc = do s <- getPosition
         let (dir, file) = splitFileName (sourceName s)
         let f = case dir of
                    "./" -> file
                    _ -> sourceName s
         return $ FC f (sourceLine s)

pImport :: IParser String
pImport = do reserved "import"
             f <- identifier
             option ';' (lchar ';')
             return (map dot f)
  where dot '.' = '/'
        dot c = c

parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]
parseProg syn fname input pos
    = do i <- get
         case (runParser (do setPosition pos
                             whiteSpace
                             ps <- many (pDecl syn)
                             eof
                             i' <- getState
                             return (concat ps, i')) i fname input) of
            Left err -> fail (ishow err)
            Right (x, i) -> do put i
                               return (collect x)
  where ishow err = let ln = sourceLine (errorPos err) in
                        fname ++ ":" ++ show ln ++ ":parse error"
                              ++ " at column " ++ show (sourceColumn (errorPos err))
--                           show (map messageString (errorMessages err))

-- Collect PClauses with the same function name

collect :: [PDecl] -> [PDecl]
collect (c@(PClauses _ o _ _) : ds) 
    = clauses (cname c) [] (c : ds)
  where clauses n acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
           | n == n' = clauses n (PClause fc' n' l ws r (collect w) : acc) ds
        clauses n acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)
           | n == n' = clauses n (PWith fc' n' l ws r (collect w) : acc) ds
        clauses n acc xs = PClauses (getfc c) o n (reverse acc) : collect xs

        cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = n
        cname (PClauses fc _ _ [PWith   _ n _ _ _ _]) = n
        getfc (PClauses fc _ _ _) = fc

collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'
collect (PInstance f s cs n ps t en ds : ds') 
    = PInstance f s cs n ps t en (collect ds) : collect ds'
collect (d : ds) = d : collect ds
collect [] = []

pFullExpr :: SyntaxInfo -> IParser PTerm
pFullExpr syn 
          = do x <- pExpr syn; eof;
               i <- getState
               return $ desugar syn i x

pDecl :: SyntaxInfo -> IParser [PDecl]
pDecl syn = do notEndBlock
               pDeclBody where
  pDeclBody
      = do d <- pDecl' syn
           i <- getState
           let d' = fmap (desugar syn i) d
           return [d']
    <|> pUsing syn
    <|> pParams syn
    <|> pNamespace syn
    <|> pClass syn
    <|> pInstance syn
    <|> do d <- pDSL syn; return [d]
    <|> pDirective
    <|> try (do reserved "import"
                fp <- identifier
                fail "imports must be at the top of file") 

pFunDecl :: SyntaxInfo -> IParser [PDecl]
pFunDecl syn
      = try (do notEndBlock
                d <- pFunDecl' syn
                i <- getState
                let d' = fmap (desugar syn i) d
                return [d'])

--------- Top Level Declarations ---------

pDecl' :: SyntaxInfo -> IParser PDecl
pDecl' syn
       = try pFixity
     <|> pFunDecl' syn
     <|> try (pData syn)
     <|> try (pRecord syn)
     <|> pSyntaxDecl syn

pSyntaxDecl :: SyntaxInfo -> IParser PDecl
pSyntaxDecl syn
    = do s <- pSyntaxRule syn
         i <- getState
         let rs = syntax_rules i
         let ns = syntax_keywords i
         let ibc = ibc_write i
         let ks = map show (names s)
         setState (i { syntax_rules = s : rs,
                       syntax_keywords = ks ++ ns,
                       ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc
                     })
         fc <- pfc
         return (PSyntax fc s)
  where
    names (Rule syms _ _) = mapMaybe ename syms
    ename (Keyword n) = Just n
    ename _ = Nothing

pSyntaxRule :: SyntaxInfo -> IParser Syntax
pSyntaxRule syn 
    = do push_indent
         sty <- option AnySyntax (do reserved "term"; return TermSyntax
                                  <|> do reserved "pattern"; return PatternSyntax)
         reserved "syntax"
         syms <- many1 pSynSym
         when (all expr syms) $ fail "No keywords in syntax rule"
         let ns = mapMaybe name syms
         when (length ns /= length (nub ns)) 
            $ fail "Repeated variable in syntax rule"
         lchar '='
         tm <- pExpr (impOK syn)
         pTerminator
         return (Rule (mkSimple syms) tm sty)
  where
    expr (Expr _) = True
    expr _ = False
    name (Expr n) = Just n
    name _ = Nothing

    -- Can't parse two full expressions (i.e. expressions with application) in a row
    -- so change the first to a simple expression

    mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
    mkSimple xs = mkSimple' xs

    mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : mkSimple' (Expr e1 : es)
    mkSimple' (e : es) = e : mkSimple' es
    mkSimple' [] = []

pSynSym :: IParser SSymbol
pSynSym = try (do lchar '['; n <- pName; lchar ']'
                  return (Expr n))
      <|> try (do lchar '{'; n <- pName; lchar '}'
                  return (Binding n))
      <|> do n <- iName []
             return (Keyword n)
      <|> do sym <- strlit
             return (Symbol sym)

pFunDecl' :: SyntaxInfo -> IParser PDecl
pFunDecl' syn = try (do push_indent
                        opts <- pFnOpts
                        acc <- pAccessibility
                        opts' <- pFnOpts
                        n_in <- pfName
                        let n = expandNS syn n_in
                        ty <- pTSig (impOK syn)
                        fc <- pfc
                        pTerminator 
--                         ty' <- implicit syn n ty
                        addAcc n acc
                        return (PTy syn fc (opts ++ opts') n ty))
            <|> try (pPattern syn)

pUsing :: SyntaxInfo -> IParser [PDecl]
pUsing syn = 
    do reserved "using"; 
       lchar '('
       ns <- tyDeclList syn
       lchar ')'
       open_block
       let uvars = using syn
       ds <- many1 (pDecl (syn { using = uvars ++ ns }))
       close_block
       return (concat ds)

pParams :: SyntaxInfo -> IParser [PDecl]
pParams syn = 
    do reserved "params"; 
       lchar '('
       ns <- tyDeclList syn
       lchar ')'
       lchar '{'
       let pvars = syn_params syn
       ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
       lchar '}'
       fc <- pfc
       return [PParams fc ns (concat ds)]

pNamespace :: SyntaxInfo -> IParser [PDecl]
pNamespace syn =
    do reserved "namespace";
       n <- identifier
       open_block 
       ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
       close_block
       return [PNamespace n (concat ds)] 

--------- Fixity ---------

pFixity :: IParser PDecl
pFixity = do push_indent
             f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
             pTerminator 
             let prec = fromInteger i
             istate <- getState
             let fs = map (Fix (f prec)) ops
             setState (istate { 
                idris_infixes = nub $ sort (fs ++ idris_infixes istate),
                ibc_write = map IBCFix fs ++ ibc_write istate })
             fc <- pfc
             return (PFix fc (f prec) ops)

fixity :: IParser (Int -> Fixity) 
fixity = try (do reserved "infixl"; return Infixl)
     <|> try (do reserved "infixr"; return Infixr)
     <|> try (do reserved "infix";  return InfixN)
     <|> try (do reserved "prefix"; return PrefixN)

--------- Tyoe classes ---------

pClass :: SyntaxInfo -> IParser [PDecl]
pClass syn = do acc <- pAccessibility
                reserved "class"
                fc <- pfc
                cons <- pConstList syn
                n_in <- pName; let n = expandNS syn n_in
                cs <- many1 carg
                reserved "where"; open_block 
                ds <- many $ pFunDecl syn
                close_block
                let allDs = concat ds
                accData acc n (concatMap declared allDs)
                return [PClass syn fc cons n cs allDs]
  where
    carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
              return (i, ty)
       <|> do i <- pName;
              return (i, PSet)

pInstance :: SyntaxInfo -> IParser [PDecl]
pInstance syn = do reserved "instance"
                   fc <- pfc
                   en <- option Nothing
                            (do lchar '['; n_in <- pfName; lchar ']'
                                let n = expandNS syn n_in
                                return (Just n))<commit_msg>tiny tiny tiny typo fix<commit_after>{-# LANGUAGE PatternGuards #-}

module Idris.Parser where

import Idris.AbsSyntax
import Idris.DSL
import Idris.Imports
import Idris.Error
import Idris.ElabDecls
import Idris.ElabTerm
import Idris.Coverage
import Idris.IBC
import Idris.Unlit
import Paths_idris

import Core.CoreParser
import Core.TT
import Core.Evaluate

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

import Data.List
import Control.Monad.State
import Debug.Trace
import Data.Maybe
import System.FilePath

type TokenParser a = PTok.TokenParser a

type IParser = GenParser Char IState

lexer :: TokenParser IState
lexer  = PTok.makeTokenParser idrisDef

whiteSpace= PTok.whiteSpace lexer
lexeme    = PTok.lexeme lexer
symbol    = PTok.symbol lexer
natural   = PTok.natural lexer
parens    = PTok.parens lexer
semi      = PTok.semi lexer
comma     = PTok.comma lexer
identifier= PTok.identifier lexer
reserved  = PTok.reserved lexer
operator  = PTok.operator lexer
reservedOp= PTok.reservedOp lexer
integer   = PTok.integer lexer
float     = PTok.float lexer
strlit    = PTok.stringLiteral lexer
chlit     = PTok.charLiteral lexer
lchar = lexeme.char

-- Loading modules

loadModule :: FilePath -> Idris String
loadModule f 
   = idrisCatch (do i <- getIState
                    ibcsd <- valIBCSubDir i
                    ids <- allImportDirs i
                    fp <- liftIO $ findImport ids ibcsd f
                    if (f `elem` imported i)
                       then iLOG $ "Already read " ++ f
                       else do putIState (i { imported = f : imported i })
                               case fp of
                                   IDR fn  -> loadSource False fn
                                   LIDR fn -> loadSource True  fn
                                   IBC fn src -> 
                                     idrisCatch (loadIBC fn)
                                                (\c -> do iLOG $ fn ++ " failed " ++ show c
                                                          case src of
                                                            IDR sfn -> loadSource False sfn
                                                            LIDR sfn -> loadSource True sfn)
                    let (dir, fh) = splitFileName f
                    return (dropExtension fh))
                (\e -> do let msg = show e
                          setErrLine (getErrLine msg)
                          iputStrLn msg
                          return "")

loadSource :: Bool -> FilePath -> Idris () 
loadSource lidr f 
             = do iLOG ("Reading " ++ f)
                  file_in <- liftIO $ readFile f
                  file <- if lidr then tclift $ unlit f file_in else return file_in
                  (mname, modules, rest, pos) <- parseImports f file
                  i <- getIState
                  putIState (i { default_access = Hidden })
                  mapM_ loadModule modules
                  clearIBC -- start a new .ibc file
                  mapM_ (\m -> addIBC (IBCImport m)) modules
                  ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname }) 
                                   f rest pos
                  let ds = namespaces mname ds'
                  logLvl 3 (dumpDecls ds)
                  i <- getIState
                  logLvl 10 (show (toAlist (idris_implicits i)))
                  logLvl 3 (show (idris_infixes i))
                  -- Now add all the declarations to the context
                  v <- verbose
                  when v $ iputStrLn $ "Type checking " ++ f
                  mapM_ (elabDecl toplevel) ds
                  i <- get
                  mapM_ checkDeclTotality (idris_totcheck i)
                  iLOG ("Finished " ++ f)
                  ibcsd <- valIBCSubDir i
                  let ibc = ibcPathNoFallback ibcsd f
                  iucheck
                  i <- getIState
                  addHides (hide_list i)
                  ok <- noErrors
                  when ok $
                    idrisCatch (do writeIBC f ibc; clearIBC)
                               (\c -> return ()) -- failure is harmless
                  i <- getIState
                  putIState (i { hide_list = [] })
                  return ()
  where
    namespaces []     ds = ds
    namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]

addHides :: [(Name, Maybe Accessibility)] -> Idris ()
addHides xs = do i <- getIState
                 let defh = default_access i
                 let (hs, as) = partition isNothing xs
                 if null as then return ()
                            else mapM_ doHide
                                    (map (\ (n, _) -> (n, defh)) hs ++
                                     map (\ (n, Just a) -> (n, a)) as)
  where isNothing (_, Nothing) = True
        isNothing _            = False

        doHide (n, a) = do setAccessibility n a
                           addIBC (IBCAccess n a)

parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"
parseTac i = runParser (do t <- pTactic defaultSyntax
                           eof
                           return t) i "(proof)"

parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)
parseImports fname input 
    = do i <- get
         case (runParser (do whiteSpace
                             mname <- pHeader
                             ps <- many pImport
                             rest <- getInput
                             pos <- getPosition
                             return ((mname, ps, rest, pos), i)) i fname input) of
            Left err -> fail (show err)
            Right (x, i) -> do put i
                               return x
  where ishow err = let ln = sourceLine (errorPos err) in
                        fname ++ ":" ++ show ln ++ ":parse error"
--                            ++ show (map messageString (errorMessages err))

pHeader :: IParser [String]
pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')
                  return (parseName i))
     <|> return []
  where parseName x = case span (/='.') x of
                            (x, "") -> [x]
                            (x, '.':y) -> x : parseName y

push_indent :: IParser ()
push_indent = do pos <- getPosition
                 ist <- getState
                 setState (ist { indent_stack = sourceColumn pos :
                                                indent_stack ist })

last_indent :: IParser Int
last_indent = do ist <- getState
                 case indent_stack ist of
                    (x : xs) -> return x
                    _ -> return 1

indent :: IParser Int
indent = do pos <- getPosition
            return (sourceColumn pos)

pop_indent :: IParser ()
pop_indent = do ist <- getState
                let (x : xs) = indent_stack ist
                setState (ist { indent_stack = xs })

open_block :: IParser ()
open_block = do lchar '{'
                ist <- getState
                setState (ist { brace_stack = Nothing : brace_stack ist })
         <|> do ist <- getState
                lvl <- indent
                setState (ist { brace_stack = Just lvl : brace_stack ist })

close_block :: IParser ()
close_block = do ist <- getState
                 bs <- case brace_stack ist of
                         Nothing : xs -> do lchar '}'
                                            return xs
                         Just lvl : xs -> do i <- indent
                                             inp <- getInput
--                                              trace (show (take 10 inp, i, lvl)) $
                                             if (i >= lvl && take 1 inp /= ")") 
                                                then fail "Not end of block"
                                                else return xs
                 setState (ist { brace_stack = bs })

pTerminator = do lchar ';'; pop_indent
          <|> do c <- indent; l <- last_indent
                 if (c <= l) then pop_indent
                             else fail "Not a terminator"
          <|> do i <- getInput; if (take 1 i == "}" || take 1 i == ")") then pop_indent 
                                                     else fail "Not a terminator"
          <|> lookAhead eof

pBarTerminator 
            = do lchar '|'; return ()
          <|> do c <- indent; l <- last_indent
                 if (c <= l) then return ()
                             else fail "Not a terminator"
          <|> lookAhead eof

pKeepTerminator 
            = do lchar ';'; return ()
          <|> do c <- indent; l <- last_indent
                 if (c <= l) then return ()
                             else fail "Not a terminator"
          <|> do i <- getInput; let h = take 1 i
                 if (h == "}" || h == ")" || h == "|") then return ()
                                           else fail "Not a terminator"
          <|> lookAhead eof

notEndApp = do c <- indent; l <- last_indent
               i <- getInput
               if (c <= l) then fail "Terminator"
                           else return ()

notEndBlock = do ist <- getState
                 case brace_stack ist of
                    Just lvl : xs -> do i <- indent
                                        inp <- getInput
                                        if (i < lvl || take 1 inp == ")")
                                                     then fail "End of block"
                                                     else return ()
                    _ -> return ()

pfc :: IParser FC
pfc = do s <- getPosition
         let (dir, file) = splitFileName (sourceName s)
         let f = case dir of
                    "./" -> file
                    _ -> sourceName s
         return $ FC f (sourceLine s)

pImport :: IParser String
pImport = do reserved "import"
             f <- identifier
             option ';' (lchar ';')
             return (map dot f)
  where dot '.' = '/'
        dot c = c

parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> Idris [PDecl]
parseProg syn fname input pos
    = do i <- get
         case (runParser (do setPosition pos
                             whiteSpace
                             ps <- many (pDecl syn)
                             eof
                             i' <- getState
                             return (concat ps, i')) i fname input) of
            Left err -> fail (ishow err)
            Right (x, i) -> do put i
                               return (collect x)
  where ishow err = let ln = sourceLine (errorPos err) in
                        fname ++ ":" ++ show ln ++ ":parse error"
                              ++ " at column " ++ show (sourceColumn (errorPos err))
--                           show (map messageString (errorMessages err))

-- Collect PClauses with the same function name

collect :: [PDecl] -> [PDecl]
collect (c@(PClauses _ o _ _) : ds) 
    = clauses (cname c) [] (c : ds)
  where clauses n acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
           | n == n' = clauses n (PClause fc' n' l ws r (collect w) : acc) ds
        clauses n acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)
           | n == n' = clauses n (PWith fc' n' l ws r (collect w) : acc) ds
        clauses n acc xs = PClauses (getfc c) o n (reverse acc) : collect xs

        cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = n
        cname (PClauses fc _ _ [PWith   _ n _ _ _ _]) = n
        getfc (PClauses fc _ _ _) = fc

collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'
collect (PInstance f s cs n ps t en ds : ds') 
    = PInstance f s cs n ps t en (collect ds) : collect ds'
collect (d : ds) = d : collect ds
collect [] = []

pFullExpr :: SyntaxInfo -> IParser PTerm
pFullExpr syn 
          = do x <- pExpr syn; eof;
               i <- getState
               return $ desugar syn i x

pDecl :: SyntaxInfo -> IParser [PDecl]
pDecl syn = do notEndBlock
               pDeclBody where
  pDeclBody
      = do d <- pDecl' syn
           i <- getState
           let d' = fmap (desugar syn i) d
           return [d']
    <|> pUsing syn
    <|> pParams syn
    <|> pNamespace syn
    <|> pClass syn
    <|> pInstance syn
    <|> do d <- pDSL syn; return [d]
    <|> pDirective
    <|> try (do reserved "import"
                fp <- identifier
                fail "imports must be at the top of file") 

pFunDecl :: SyntaxInfo -> IParser [PDecl]
pFunDecl syn
      = try (do notEndBlock
                d <- pFunDecl' syn
                i <- getState
                let d' = fmap (desugar syn i) d
                return [d'])

--------- Top Level Declarations ---------

pDecl' :: SyntaxInfo -> IParser PDecl
pDecl' syn
       = try pFixity
     <|> pFunDecl' syn
     <|> try (pData syn)
     <|> try (pRecord syn)
     <|> pSyntaxDecl syn

pSyntaxDecl :: SyntaxInfo -> IParser PDecl
pSyntaxDecl syn
    = do s <- pSyntaxRule syn
         i <- getState
         let rs = syntax_rules i
         let ns = syntax_keywords i
         let ibc = ibc_write i
         let ks = map show (names s)
         setState (i { syntax_rules = s : rs,
                       syntax_keywords = ks ++ ns,
                       ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc
                     })
         fc <- pfc
         return (PSyntax fc s)
  where
    names (Rule syms _ _) = mapMaybe ename syms
    ename (Keyword n) = Just n
    ename _ = Nothing

pSyntaxRule :: SyntaxInfo -> IParser Syntax
pSyntaxRule syn 
    = do push_indent
         sty <- option AnySyntax (do reserved "term"; return TermSyntax
                                  <|> do reserved "pattern"; return PatternSyntax)
         reserved "syntax"
         syms <- many1 pSynSym
         when (all expr syms) $ fail "No keywords in syntax rule"
         let ns = mapMaybe name syms
         when (length ns /= length (nub ns)) 
            $ fail "Repeated variable in syntax rule"
         lchar '='
         tm <- pExpr (impOK syn)
         pTerminator
         return (Rule (mkSimple syms) tm sty)
  where
    expr (Expr _) = True
    expr _ = False
    name (Expr n) = Just n
    name _ = Nothing

    -- Can't parse two full expressions (i.e. expressions with application) in a row
    -- so change the first to a simple expression

    mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
    mkSimple xs = mkSimple' xs

    mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : mkSimple' (Expr e1 : es)
    mkSimple' (e : es) = e : mkSimple' es
    mkSimple' [] = []

pSynSym :: IParser SSymbol
pSynSym = try (do lchar '['; n <- pName; lchar ']'
                  return (Expr n))
      <|> try (do lchar '{'; n <- pName; lchar '}'
                  return (Binding n))
      <|> do n <- iName []
             return (Keyword n)
      <|> do sym <- strlit
             return (Symbol sym)

pFunDecl' :: SyntaxInfo -> IParser PDecl
pFunDecl' syn = try (do push_indent
                        opts <- pFnOpts
                        acc <- pAccessibility
                        opts' <- pFnOpts
                        n_in <- pfName
                        let n = expandNS syn n_in
                        ty <- pTSig (impOK syn)
                        fc <- pfc
                        pTerminator 
--                         ty' <- implicit syn n ty
                        addAcc n acc
                        return (PTy syn fc (opts ++ opts') n ty))
            <|> try (pPattern syn)

pUsing :: SyntaxInfo -> IParser [PDecl]
pUsing syn = 
    do reserved "using"; 
       lchar '('
       ns <- tyDeclList syn
       lchar ')'
       open_block
       let uvars = using syn
       ds <- many1 (pDecl (syn { using = uvars ++ ns }))
       close_block
       return (concat ds)

pParams :: SyntaxInfo -> IParser [PDecl]
pParams syn = 
    do reserved "params"; 
       lchar '('
       ns <- tyDeclList syn
       lchar ')'
       lchar '{'
       let pvars = syn_params syn
       ds <- many1 (pDecl syn { syn_params = pvars ++ ns })
       lchar '}'
       fc <- pfc
       return [PParams fc ns (concat ds)]

pNamespace :: SyntaxInfo -> IParser [PDecl]
pNamespace syn =
    do reserved "namespace";
       n <- identifier
       open_block 
       ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })
       close_block
       return [PNamespace n (concat ds)] 

--------- Fixity ---------

pFixity :: IParser PDecl
pFixity = do push_indent
             f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')
             pTerminator 
             let prec = fromInteger i
             istate <- getState
             let fs = map (Fix (f prec)) ops
             setState (istate { 
                idris_infixes = nub $ sort (fs ++ idris_infixes istate),
                ibc_write = map IBCFix fs ++ ibc_write istate })
             fc <- pfc
             return (PFix fc (f prec) ops)

fixity :: IParser (Int -> Fixity) 
fixity = try (do reserved "infixl"; return Infixl)
     <|> try (do reserved "infixr"; return Infixr)
     <|> try (do reserved "infix";  return InfixN)
     <|> try (do reserved "prefix"; return PrefixN)

--------- Type classes ---------

pClass :: SyntaxInfo -> IParser [PDecl]
pClass syn = do acc <- pAccessibility
                reserved "class"
                fc <- pfc
                cons <- pConstList syn
                n_in <- pName; let n = expandNS syn n_in
                cs <- many1 carg
                reserved "where"; open_block 
                ds <- many $ pFunDecl syn
                close_block
                let allDs = concat ds
                accData acc n (concatMap declared allDs)
                return [PClass syn fc cons n cs allDs]
  where
    carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'
              return (i, ty)
       <|> do i <- pName;
              return (i, PSet)

pInstance :: SyntaxInfo -> IParser [PDecl]
pInstance syn = do reserved "instance"
                   fc <- pfc
                   en <- option Nothing
                            (do lchar '['; n_in <- pfName; lchar ']'
                                let n = expandNS syn n_in
                                return (Just n))
{'fraction_non_alphanumeric': 0.09184888504005195, 'fraction_numerical': 0.001082485386447283, 'mean_word_length': 1.2688647387486953, 'pattern_counts': {'":': 8, '<': 283, '<?xml version=': 0, '>': 165, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 108, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5481845', 'n_tokens_mistral': 10677, 'n_tokens_neox': 9928, 'n_words': 3599}