{-|
Module      : Idris.Parser
Description : Idris' parser.

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# LANGUAGE ConstraintKinds, FlexibleContexts, GeneralizedNewtypeDeriving,
             PatternGuards #-}
{-# OPTIONS_GHC -O0 #-}
-- FIXME: {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
{-# OPTIONS_GHC -fwarn-unused-imports #-}

module Idris.Parser(IdrisParser(..), ImportInfo(..), moduleName, addReplSyntax, clearParserWarnings,
                    decl, fixColour, loadFromIFile, loadModule, name, opChars, parseElabShellStep, parseConst, parseExpr, parseImports, parseTactic,
                    runparser, ParseError, parseErrorDoc) where

import Idris.AbsSyntax hiding (namespace, params)
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Delaborate
import Idris.Docstrings hiding (Unchecked)
import Idris.DSL
import Idris.Elab.Value
import Idris.ElabDecls
import Idris.Error
import Idris.IBC
import Idris.Imports
import Idris.Options
import Idris.Output
import Idris.Parser.Data
import Idris.Parser.Expr
import Idris.Parser.Helpers
import Idris.Parser.Ops
import Idris.Termination
import Idris.Unlit

import Util.System (readSource)

import Prelude hiding (pi)

import Control.Applicative hiding (Const)
import Control.Monad
import Control.Monad.State.Strict
import Data.Char
import Data.Foldable (asum)
import Data.Function
import Data.Generics.Uniplate.Data (descendM)
import Data.List
import qualified Data.List.NonEmpty as NonEmpty
import qualified Data.List.Split as Spl
import qualified Data.Map as M
import Data.Maybe
import Data.Ord
import qualified Data.Set as S
import qualified Data.Text as T
import qualified System.Directory as Dir (doesFileExist, getModificationTime,
                                          makeAbsolute)
import System.FilePath
import Text.Megaparsec ((<?>))
import qualified Text.Megaparsec as P
import qualified Text.PrettyPrint.ANSI.Leijen as PP

{-
@
 grammar shortcut notation:
    ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
    RULE? = optional rule (i.e. RULE or nothing)
    RULE* = repeated rule (i.e. RULE zero or more times)
    RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
    RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
    RULE{n} = rule repeated n times
@
-}

{- * Main grammar -}

{-| Parses module definition

@
      ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?;
@
-}


moduleName :: Parsing m => m Name
moduleName :: forall (m :: * -> *). Parsing m => m Name
moduleName = [Text] -> [Text] -> Name
mkName [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m [String]
moduleNamePieces where

  mkName :: [T.Text] -> [T.Text] -> Name
  mkName :: [Text] -> [Text] -> Name
mkName [Text]
ts [Text
x]    = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Text]
ts then Text -> Name
UN Text
x else Name -> [Text] -> Name
NS (Text -> Name
UN Text
x) [Text]
ts
  mkName [Text]
ts (Text
x:[Text]
xs) = [Text] -> [Text] -> Name
mkName (Text
x forall a. a -> [a] -> [a]
: [Text]
ts) [Text]
xs

moduleNamePieces :: Parsing m => m [String]
moduleNamePieces :: forall (m :: * -> *). Parsing m => m [String]
moduleNamePieces = forall a. Eq a => [a] -> [a] -> [[a]]
Spl.splitOn String
"." forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m String
identifier

moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
moduleHeader :: IdrisParser
  (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
moduleHeader =     forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do Maybe (Docstring (), [(Name, Docstring ())])
docs <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional IdrisParser (Docstring (), [(Name, Docstring ())])
docComment
                             forall {t :: * -> *} {m :: * -> *} {a} {a}.
(Foldable t, MonadFail m) =>
Maybe (a, t a) -> m ()
noArgs Maybe (Docstring (), [(Name, Docstring ())])
docs
                             forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"module"
                             ([String]
modName, FC
ifc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). Parsing m => m [String]
moduleNamePieces
                             forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option Char
';' (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
';')
                             forall (m :: * -> *) a. Monad m => a -> m a
return (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst Maybe (Docstring (), [(Name, Docstring ())])
docs,
                                     [String]
modName,
                                     [(FC
ifc, [Text] -> Maybe String -> OutputAnnotation
AnnNamespace (forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack [String]
modName) forall a. Maybe a
Nothing)]))
               forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%'; forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"unqualified"
                             forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, [], []))
               forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, [String
"Main"], [])
  where noArgs :: Maybe (a, t a) -> m ()
noArgs (Just (a
_, t a
args)) | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null t a
args) = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Modules do not take arguments"
        noArgs Maybe (a, t a)
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()

data ImportInfo = ImportInfo { ImportInfo -> Bool
import_reexport :: Bool
                             , ImportInfo -> String
import_path :: FilePath
                             , ImportInfo -> Maybe (String, FC)
import_rename :: Maybe (String, FC)
                             , ImportInfo -> [Text]
import_namespace :: [T.Text]
                             , ImportInfo -> FC
import_location :: FC
                             , ImportInfo -> FC
import_modname_location :: FC
                             }

{-| Parses an import statement

@
  Import ::= 'import' Identifier_t ';'?;
@
 -}
import_ :: IdrisParser ImportInfo
import_ :: IdrisParser ImportInfo
import_ = do FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"import"
             Bool
reexport <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option Bool
False (Bool
True forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"public")
             ([String]
ns, FC
idfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). Parsing m => m [String]
moduleNamePieces
             Maybe (String, FC)
newName <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"as"
                                     forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). Parsing m => m String
identifier)
             forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option Char
';' (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
';')
             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool
-> String -> Maybe (String, FC) -> [Text] -> FC -> FC -> ImportInfo
ImportInfo Bool
reexport ([String] -> String
toPath [String]
ns)
                        (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(String
n, FC
fc) -> ([String] -> String
toPath (forall a. Eq a => [a] -> [a] -> [[a]]
Spl.splitOn String
"." String
n), FC
fc)) Maybe (String, FC)
newName)
                        (forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack [String]
ns) FC
fc FC
idfc
          forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"import statement"
  where toPath :: [String] -> String
toPath = forall a. (a -> a -> a) -> [a] -> a
foldl1' String -> String -> String
(</>)

{-| Parses program source

@
     Prog ::= Decl* EOF;
@
 -}
prog :: SyntaxInfo -> IdrisParser [PDecl]
prog :: SyntaxInfo -> IdrisParser [PDecl]
prog SyntaxInfo
syn = do ([PDecl]
decls, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ do
                  forall (m :: * -> *). Parsing m => m ()
whiteSpace
                  [PDecl]
decls <- forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (SyntaxInfo -> IdrisParser [PDecl]
decl SyntaxInfo
syn)
                  case SyntaxInfo -> Maybe Int
maxline SyntaxInfo
syn of
                       Maybe Int
Nothing -> do StateT IState (WriterT FC (Parsec Void String)) ()
notOpenBraces; forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
                       Maybe Int
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  forall (m :: * -> *) a. Monad m => a -> m a
return [PDecl]
decls
              IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
              forall s (m :: * -> *). MonadState s m => s -> m ()
put IState
ist { idris_parsedSpan :: Maybe FC
idris_parsedSpan = forall a. a -> Maybe a
Just (String -> (Int, Int) -> (Int, Int) -> FC
FC (FC -> String
fc_fname FC
fc) (Int
0,Int
0) (FC -> (Int, Int)
fc_end FC
fc)),
                        ibc_write :: [IBCWrite]
ibc_write = FC -> IBCWrite
IBCParsedRegion FC
fc forall a. a -> [a] -> [a]
: IState -> [IBCWrite]
ibc_write IState
ist }
              forall (m :: * -> *) a. Monad m => a -> m a
return [PDecl]
decls

{-| Parses a top-level declaration

@
Decl ::=
    Decl'
  | Using
  | Params
  | Mutual
  | Namespace
  | Interface
  | Implementation
  | DSL
  | Directive
  | Provider
  | Transform
  | Import!
  | RunElabDecl
  ;
@
-}
decl :: SyntaxInfo -> IdrisParser [PDecl]
decl :: SyntaxInfo -> IdrisParser [PDecl]
decl SyntaxInfo
syn = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser [PDecl]
externalDecl SyntaxInfo
syn)
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
internalDecl SyntaxInfo
syn
           forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"declaration"

internalDecl :: SyntaxInfo -> IdrisParser [PDecl]
internalDecl :: SyntaxInfo -> IdrisParser [PDecl]
internalDecl SyntaxInfo
syn
         = do FC
fc <- forall (m :: * -> *). Parsing m => m FC
getFC
              -- if we're after maxline, stop at the next type declaration
              -- (so we get all cases of a definition to preserve totality
              -- results, in particular).
              let continue :: Bool
continue = case SyntaxInfo -> Maybe Int
maxline SyntaxInfo
syn of
                                Maybe Int
Nothing -> Bool
True
                                Just Int
l -> if forall a b. (a, b) -> a
fst (FC -> (Int, Int)
fc_end FC
fc) forall a. Ord a => a -> a -> Bool
> Int
l
                                             then SyntaxInfo -> Int
mut_nesting SyntaxInfo
syn forall a. Eq a => a -> a -> Bool
/= Int
0
                                             else Bool
True
              -- What I'd really like to do here is explicitly save the
              -- current state, then if reading ahead finds we've passed
              -- the end of the definition, reset the state. But I've lost
              -- patience with trying to find out how to do that from the
              -- trifecta docs, so this does the job instead.
              if Bool
continue then
                 do StateT IState (WriterT FC (Parsec Void String)) ()
notEndBlock
                    Bool -> IdrisParser [PDecl]
declBody Bool
continue
                else forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do StateT IState (WriterT FC (Parsec Void String)) ()
notEndBlock
                               Bool -> IdrisParser [PDecl]
declBody Bool
continue)
                     forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"End of readable input"
  where declBody :: Bool -> IdrisParser [PDecl]
        declBody :: Bool -> IdrisParser [PDecl]
declBody Bool
b =
                   forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser [PDecl]
implementation SyntaxInfo
syn)
                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser [PDecl]
openInterface SyntaxInfo
syn)
                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> IdrisParser [PDecl]
declBody' Bool
b
                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
using_ SyntaxInfo
syn
                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
params SyntaxInfo
syn
                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
mutual SyntaxInfo
syn
                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
namespace SyntaxInfo
syn
                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
interface_ SyntaxInfo
syn
                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do PDecl
d <- SyntaxInfo -> IdrisParser PDecl
dsl SyntaxInfo
syn; forall (m :: * -> *) a. Monad m => a -> m a
return [PDecl
d]
                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
directive SyntaxInfo
syn
                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
provider SyntaxInfo
syn
                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
transform SyntaxInfo
syn
                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do IdrisParser ImportInfo
import_; forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"imports must be at top of file"
                   forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"declaration"
        declBody' :: Bool -> IdrisParser [PDecl]
        declBody' :: Bool -> IdrisParser [PDecl]
declBody' Bool
cont = do PDecl
d <- SyntaxInfo -> IdrisParser PDecl
decl' SyntaxInfo
syn
                            IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
                            let d' :: PDecl
d' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SyntaxInfo -> PTerm -> PTerm
debindApp SyntaxInfo
syn forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
i)) PDecl
d
                            if forall {t}. Bool -> PDecl' t -> Bool
continue Bool
cont PDecl
d'
                               then forall (m :: * -> *) a. Monad m => a -> m a
return [PDecl
d']
                               else forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"End of readable input"

        -- Keep going while we're still parsing clauses
        continue :: Bool -> PDecl' t -> Bool
continue Bool
False (PClauses FC
_ FnOpts
_ Name
_ [PClause' t]
_) = Bool
True
        continue Bool
c PDecl' t
_ = Bool
c

{-| Parses a top-level declaration with possible syntax sugar

@
Decl' ::=
    Fixity
  | FunDecl'
  | Data
  | Record
  | SyntaxDecl
  ;
@
-}
decl' :: SyntaxInfo -> IdrisParser PDecl
decl' :: SyntaxInfo -> IdrisParser PDecl
decl' SyntaxInfo
syn =    IdrisParser PDecl
fixity
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
syntaxDecl SyntaxInfo
syn
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
fnDecl' SyntaxInfo
syn
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
data_ SyntaxInfo
syn
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
record SyntaxInfo
syn
           forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
runElabDecl SyntaxInfo
syn
           forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"declaration"

externalDecl :: SyntaxInfo -> IdrisParser [PDecl]
externalDecl :: SyntaxInfo -> IdrisParser [PDecl]
externalDecl SyntaxInfo
syn = do IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
                      StateT IState (WriterT FC (Parsec Void String)) ()
notEndBlock
                      ([PDecl]
decls, fc :: FC
fc@(FC String
fn (Int, Int)
_ (Int, Int)
_)) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]
declExtensions SyntaxInfo
syn (SyntaxRules -> [Syntax]
syntaxRulesList forall a b. (a -> b) -> a -> b
$ IState -> SyntaxRules
syntax_rules IState
i)
                      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ((FC -> FC) -> (FC -> FC) -> PDecl -> PDecl
mapPDeclFC (FC -> FC -> FC
fixFC FC
fc) (String -> FC -> FC -> FC
fixFCH String
fn FC
fc)) [PDecl]
decls
  where
    -- | Fix non-highlighting FCs to prevent spurious error location reports
    fixFC :: FC -> FC -> FC
    fixFC :: FC -> FC -> FC
fixFC FC
outer FC
inner | FC
inner FC -> FC -> Bool
`fcIn` FC
outer = FC
inner
                      | Bool
otherwise          = FC
outer
    -- | Fix highlighting FCs by obliterating them, to avoid spurious highlights
    fixFCH :: String -> FC -> FC -> FC
fixFCH String
fn FC
outer FC
inner | FC
inner FC -> FC -> Bool
`fcIn` FC
outer = FC
inner
                          | Bool
otherwise          = String -> FC
FileFC String
fn

declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]
declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]
declExtensions SyntaxInfo
syn [Syntax]
rules = SyntaxInfo
-> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser [PDecl]
declExtension SyntaxInfo
syn [] (forall a. (a -> Bool) -> [a] -> [a]
filter Syntax -> Bool
isDeclRule [Syntax]
rules)
                           forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"user-defined declaration"
   where
     isDeclRule :: Syntax -> Bool
isDeclRule (DeclRule [SSymbol]
_ [PDecl]
_) = Bool
True
     isDeclRule Syntax
_ = Bool
False

declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]
                 -> IdrisParser [PDecl]
declExtension :: SyntaxInfo
-> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser [PDecl]
declExtension SyntaxInfo
syn [Maybe (Name, SynMatch)]
ns [Syntax]
rules =
  forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> [a] -> [b]
map (forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (forall {a}. Eq a => [a] -> [a] -> Bool
ruleGroup forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Syntax -> [SSymbol]
syntaxSymbols) [Syntax]
rules) forall a b. (a -> b) -> a -> b
$ \[Syntax]
rs ->
    case forall a. [a] -> a
head [Syntax]
rs of -- can never be []
      DeclRule (SSymbol
symb:[SSymbol]
_) [PDecl]
_ -> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ do
        Maybe (Name, SynMatch)
n <- SSymbol -> IdrisParser (Maybe (Name, SynMatch))
extSymbol SSymbol
symb
        SyntaxInfo
-> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser [PDecl]
declExtension SyntaxInfo
syn (Maybe (Name, SynMatch)
n forall a. a -> [a] -> [a]
: [Maybe (Name, SynMatch)]
ns) [[SSymbol] -> [PDecl] -> Syntax
DeclRule [SSymbol]
ss [PDecl]
t | (DeclRule (SSymbol
_:[SSymbol]
ss) [PDecl]
t) <- [Syntax]
rs]
      -- If we have more than one Rule in this bucket, our grammar is
      -- nondeterministic.
      DeclRule [] [PDecl]
dec -> let r :: [PDecl]
r = forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PDecl -> PDecl
update (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall a. a -> a
id [Maybe (Name, SynMatch)]
ns)) [PDecl]
dec in
                             forall (m :: * -> *) a. Monad m => a -> m a
return [PDecl]
r

  where
    update :: [(Name, SynMatch)] -> PDecl -> PDecl
    update :: [(Name, SynMatch)] -> PDecl -> PDecl
update [(Name, SynMatch)]
ns = [(Name, SynMatch)] -> PDecl -> PDecl
updateNs [(Name, SynMatch)]
ns forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> PTerm -> PTerm
updateRefs [(Name, SynMatch)]
ns) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> PTerm -> PTerm
updateSynMatch [(Name, SynMatch)]
ns)

    updateRefs :: [(Name, SynMatch)] -> PTerm -> PTerm
updateRefs [(Name, SynMatch)]
ns = (PTerm -> PTerm) -> PTerm -> PTerm
mapPT PTerm -> PTerm
newref
      where
        newref :: PTerm -> PTerm
newref (PRef FC
fc [FC]
fcs Name
n) = FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
fcs ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
n)
        newref PTerm
t = PTerm
t

    -- Below is a lot of tedious boilerplate which updates any top level
    -- names in the declaration. It will only change names which are bound in
    -- the declaration (including method names in interfaces and field names in
    -- record declarations, not including pattern variables)
    updateB :: [(Name, SynMatch)] -> Name -> Name
    updateB :: [(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns (NS Name
n [Text]
mods) = Name -> [Text] -> Name
NS ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
n) [Text]
mods
    updateB [(Name, SynMatch)]
ns Name
n = case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, SynMatch)]
ns of
                        Just (SynBind FC
tfc Name
t) -> Name
t
                        Maybe SynMatch
_ -> Name
n

    updateNs :: [(Name, SynMatch)] -> PDecl -> PDecl
    updateNs :: [(Name, SynMatch)] -> PDecl -> PDecl
updateNs [(Name, SynMatch)]
ns (PTy Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argdoc SyntaxInfo
s FC
fc FnOpts
o Name
n FC
fc' PTerm
t)
          = forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> t
-> PDecl' t
PTy Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argdoc SyntaxInfo
s FC
fc FnOpts
o ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
n) FC
fc' PTerm
t
    updateNs [(Name, SynMatch)]
ns (PClauses FC
fc FnOpts
o Name
n [PClause' PTerm]
cs)
         = forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
o ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
n) (forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PClause' PTerm -> PClause' PTerm
updateClause [(Name, SynMatch)]
ns) [PClause' PTerm]
cs)
    updateNs [(Name, SynMatch)]
ns (PCAF FC
fc Name
n PTerm
t) = forall t. FC -> Name -> t -> PDecl' t
PCAF FC
fc ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
n) PTerm
t
    updateNs [(Name, SynMatch)]
ns (PData Docstring (Either Err PTerm)
ds [(Name, Docstring (Either Err PTerm))]
cds SyntaxInfo
s FC
fc DataOpts
o PData' PTerm
dat)
         = forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> DataOpts
-> PData' t
-> PDecl' t
PData Docstring (Either Err PTerm)
ds [(Name, Docstring (Either Err PTerm))]
cds SyntaxInfo
s FC
fc DataOpts
o (forall {t}. [(Name, SynMatch)] -> PData' t -> PData' t
updateData [(Name, SynMatch)]
ns PData' PTerm
dat)
    updateNs [(Name, SynMatch)]
ns (PParams FC
fc [(Name, PTerm)]
ps [PDecl]
ds) = forall t. FC -> [(Name, t)] -> [PDecl' t] -> PDecl' t
PParams FC
fc [(Name, PTerm)]
ps (forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PDecl -> PDecl
updateNs [(Name, SynMatch)]
ns) [PDecl]
ds)
    updateNs [(Name, SynMatch)]
ns (PNamespace String
s FC
fc [PDecl]
ds) = forall t. String -> FC -> [PDecl' t] -> PDecl' t
PNamespace String
s FC
fc (forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PDecl -> PDecl
updateNs [(Name, SynMatch)]
ns) [PDecl]
ds)
    updateNs [(Name, SynMatch)]
ns (PRecord Docstring (Either Err PTerm)
doc SyntaxInfo
syn FC
fc DataOpts
o Name
n FC
fc' [(Name, FC, Plicity, PTerm)]
ps [(Name, Docstring (Either Err PTerm))]
pdocs [(Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))]
fields Maybe (Name, FC)
cname Docstring (Either Err PTerm)
cdoc SyntaxInfo
s)
         = forall t.
Docstring (Either Err t)
-> SyntaxInfo
-> FC
-> DataOpts
-> Name
-> FC
-> [(Name, FC, Plicity, t)]
-> [(Name, Docstring (Either Err t))]
-> [(Maybe (Name, FC), Plicity, t,
     Maybe (Docstring (Either Err t)))]
-> Maybe (Name, FC)
-> Docstring (Either Err t)
-> SyntaxInfo
-> PDecl' t
PRecord Docstring (Either Err PTerm)
doc SyntaxInfo
syn FC
fc DataOpts
o ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
n) FC
fc' [(Name, FC, Plicity, PTerm)]
ps [(Name, Docstring (Either Err PTerm))]
pdocs
                   (forall a b. (a -> b) -> [a] -> [b]
map (forall {b} {b} {c} {d}.
[(Name, SynMatch)]
-> (Maybe (Name, b), b, c, d) -> (Maybe (Name, b), b, c, d)
updateField [(Name, SynMatch)]
ns) [(Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))]
fields)
                   (forall {b}.
[(Name, SynMatch)] -> Maybe (Name, b) -> Maybe (Name, b)
updateRecCon [(Name, SynMatch)]
ns Maybe (Name, FC)
cname)
                   Docstring (Either Err PTerm)
cdoc
                   SyntaxInfo
s
    updateNs [(Name, SynMatch)]
ns (PInterface Docstring (Either Err PTerm)
docs SyntaxInfo
s FC
fc [(Name, PTerm)]
cs Name
cn FC
fc' [(Name, FC, PTerm)]
ps [(Name, Docstring (Either Err PTerm))]
pdocs [(Name, FC)]
pdets [PDecl]
ds Maybe (Name, FC)
cname Docstring (Either Err PTerm)
cdocs)
         = forall t.
Docstring (Either Err t)
-> SyntaxInfo
-> FC
-> [(Name, t)]
-> Name
-> FC
-> [(Name, FC, t)]
-> [(Name, Docstring (Either Err t))]
-> [(Name, FC)]
-> [PDecl' t]
-> Maybe (Name, FC)
-> Docstring (Either Err t)
-> PDecl' t
PInterface Docstring (Either Err PTerm)
docs SyntaxInfo
s FC
fc [(Name, PTerm)]
cs ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
cn) FC
fc' [(Name, FC, PTerm)]
ps [(Name, Docstring (Either Err PTerm))]
pdocs [(Name, FC)]
pdets
                      (forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PDecl -> PDecl
updateNs [(Name, SynMatch)]
ns) [PDecl]
ds)
                      (forall {b}.
[(Name, SynMatch)] -> Maybe (Name, b) -> Maybe (Name, b)
updateRecCon [(Name, SynMatch)]
ns Maybe (Name, FC)
cname)
                      Docstring (Either Err PTerm)
cdocs
    updateNs [(Name, SynMatch)]
ns (PImplementation Docstring (Either Err PTerm)
docs [(Name, Docstring (Either Err PTerm))]
pdocs SyntaxInfo
s FC
fc [(Name, PTerm)]
cs [Name]
pnames Accessibility
acc FnOpts
opts Name
cn FC
fc' [PTerm]
ps [(Name, PTerm)]
pextra PTerm
ity Maybe Name
ni [PDecl]
ds)
         = forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [(Name, t)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [t]
-> [(Name, t)]
-> t
-> Maybe Name
-> [PDecl' t]
-> PDecl' t
PImplementation Docstring (Either Err PTerm)
docs [(Name, Docstring (Either Err PTerm))]
pdocs SyntaxInfo
s FC
fc [(Name, PTerm)]
cs [Name]
pnames Accessibility
acc FnOpts
opts ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
cn) FC
fc'
                           [PTerm]
ps [(Name, PTerm)]
pextra PTerm
ity (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns) Maybe Name
ni)
                           (forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PDecl -> PDecl
updateNs [(Name, SynMatch)]
ns) [PDecl]
ds)
    updateNs [(Name, SynMatch)]
ns (PMutual FC
fc [PDecl]
ds) = forall t. FC -> [PDecl' t] -> PDecl' t
PMutual FC
fc (forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PDecl -> PDecl
updateNs [(Name, SynMatch)]
ns) [PDecl]
ds)
    updateNs [(Name, SynMatch)]
ns (PProvider Docstring (Either Err PTerm)
docs SyntaxInfo
s FC
fc FC
fc' ProvideWhat' PTerm
pw Name
n)
        = forall t.
Docstring (Either Err t)
-> SyntaxInfo -> FC -> FC -> ProvideWhat' t -> Name -> PDecl' t
PProvider Docstring (Either Err PTerm)
docs SyntaxInfo
s FC
fc FC
fc' ProvideWhat' PTerm
pw ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
n)
    updateNs [(Name, SynMatch)]
ns PDecl
d = PDecl
d

    updateRecCon :: [(Name, SynMatch)] -> Maybe (Name, b) -> Maybe (Name, b)
updateRecCon [(Name, SynMatch)]
ns Maybe (Name, b)
Nothing = forall a. Maybe a
Nothing
    updateRecCon [(Name, SynMatch)]
ns (Just (Name
n, b
fc)) = forall a. a -> Maybe a
Just ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
n, b
fc)

    updateField :: [(Name, SynMatch)]
-> (Maybe (Name, b), b, c, d) -> (Maybe (Name, b), b, c, d)
updateField [(Name, SynMatch)]
ns (Maybe (Name, b)
m, b
p, c
t, d
doc) = (forall {b}.
[(Name, SynMatch)] -> Maybe (Name, b) -> Maybe (Name, b)
updateRecCon [(Name, SynMatch)]
ns Maybe (Name, b)
m, b
p, c
t, d
doc)

    updateClause :: [(Name, SynMatch)] -> PClause' PTerm -> PClause' PTerm
updateClause [(Name, SynMatch)]
ns (PClause FC
fc Name
n PTerm
t [PTerm]
ts PTerm
t' [PDecl]
ds)
       = forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
n) PTerm
t [PTerm]
ts PTerm
t' (forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PDecl -> PDecl
update [(Name, SynMatch)]
ns) [PDecl]
ds)
    updateClause [(Name, SynMatch)]
ns (PWith FC
fc Name
n PTerm
t [PTerm]
ts PTerm
t' Maybe (Name, FC)
m [PDecl]
ds)
       = forall t.
FC
-> Name
-> t
-> [t]
-> t
-> Maybe (Name, FC)
-> [PDecl' t]
-> PClause' t
PWith FC
fc ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
n) PTerm
t [PTerm]
ts PTerm
t' Maybe (Name, FC)
m (forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PDecl -> PDecl
update [(Name, SynMatch)]
ns) [PDecl]
ds)
    updateClause [(Name, SynMatch)]
ns (PClauseR FC
fc [PTerm]
ts PTerm
t [PDecl]
ds)
       = forall t. FC -> [t] -> t -> [PDecl' t] -> PClause' t
PClauseR FC
fc [PTerm]
ts PTerm
t (forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PDecl -> PDecl
update [(Name, SynMatch)]
ns) [PDecl]
ds)
    updateClause [(Name, SynMatch)]
ns (PWithR FC
fc [PTerm]
ts PTerm
t Maybe (Name, FC)
m [PDecl]
ds)
       = forall t.
FC -> [t] -> t -> Maybe (Name, FC) -> [PDecl' t] -> PClause' t
PWithR FC
fc [PTerm]
ts PTerm
t Maybe (Name, FC)
m (forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PDecl -> PDecl
update [(Name, SynMatch)]
ns) [PDecl]
ds)

    updateData :: [(Name, SynMatch)] -> PData' t -> PData' t
updateData [(Name, SynMatch)]
ns (PDatadecl Name
n FC
fc t
t [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]
cs)
       = forall t.
Name
-> FC
-> t
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]
-> PData' t
PDatadecl ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
n) FC
fc t
t (forall a b. (a -> b) -> [a] -> [b]
map (forall {a} {b} {d} {e} {f} {g}.
[(Name, SynMatch)]
-> (a, b, Name, d, e, f, g) -> (a, b, Name, d, e, f, g)
updateCon [(Name, SynMatch)]
ns) [(Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]
cs)
    updateData [(Name, SynMatch)]
ns (PLaterdecl Name
n FC
fc t
t)
       = forall t. Name -> FC -> t -> PData' t
PLaterdecl ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
n) FC
fc t
t

    updateCon :: [(Name, SynMatch)]
-> (a, b, Name, d, e, f, g) -> (a, b, Name, d, e, f, g)
updateCon [(Name, SynMatch)]
ns (a
cd, b
ads, Name
cn, d
fc, e
ty, f
fc', g
fns)
       = (a
cd, b
ads, [(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
cn, d
fc, e
ty, f
fc', g
fns)

    ruleGroup :: [a] -> [a] -> Bool
ruleGroup [] [] = Bool
True
    ruleGroup (a
s1:[a]
_) (a
s2:[a]
_) = a
s1 forall a. Eq a => a -> a -> Bool
== a
s2
    ruleGroup [a]
_ [a]
_ = Bool
False

    extSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
    extSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
extSymbol (Keyword Name
n) = forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword (forall a. Show a => a -> String
show Name
n)
    extSymbol (Expr Name
n) = do PTerm
tm <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Name
n, PTerm -> SynMatch
SynTm PTerm
tm)
    extSymbol (SimpleExpr Name
n) = do PTerm
tm <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
                                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Name
n, PTerm -> SynMatch
SynTm PTerm
tm)
    extSymbol (Binding Name
n) = do (Name
b, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
                               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Name
n, FC -> Name -> SynMatch
SynBind FC
fc Name
b)
    extSymbol (Symbol String
s) = forall a. Maybe a
Nothing forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (forall (m :: * -> *). Parsing m => String -> m ()
symbol String
s)

{-| Parses a syntax extension declaration (and adds the rule to parser state)

@
  SyntaxDecl ::= SyntaxRule;
@
-}
syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
syntaxDecl SyntaxInfo
syn = do (Syntax
s, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser Syntax
syntaxRule SyntaxInfo
syn
                    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \IState
i -> IState
i IState -> Syntax -> IState
`addSyntax` Syntax
s
                    forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. FC -> Syntax -> PDecl' t
PSyntax FC
fc Syntax
s)

-- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'.
addSyntax :: IState -> Syntax -> IState
addSyntax :: IState -> Syntax -> IState
addSyntax IState
i Syntax
s = IState
i { syntax_rules :: SyntaxRules
syntax_rules = [Syntax] -> SyntaxRules -> SyntaxRules
updateSyntaxRules [Syntax
s] SyntaxRules
rs,
                    syntax_keywords :: [String]
syntax_keywords = [String]
ks forall a. [a] -> [a] -> [a]
++ [String]
ns,
                    ibc_write :: [IBCWrite]
ibc_write = Syntax -> IBCWrite
IBCSyntax Syntax
s forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map String -> IBCWrite
IBCKeyword [String]
ks forall a. [a] -> [a] -> [a]
++ [IBCWrite]
ibc }
  where rs :: SyntaxRules
rs = IState -> SyntaxRules
syntax_rules IState
i
        ns :: [String]
ns = IState -> [String]
syntax_keywords IState
i
        ibc :: [IBCWrite]
ibc = IState -> [IBCWrite]
ibc_write IState
i
        ks :: [String]
ks = forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show (Syntax -> [Name]
syntaxNames Syntax
s)

-- | Like 'addSyntax', but no effect on the IBC.
addReplSyntax :: IState -> Syntax -> IState
addReplSyntax :: IState -> Syntax -> IState
addReplSyntax IState
i Syntax
s = IState
i { syntax_rules :: SyntaxRules
syntax_rules = [Syntax] -> SyntaxRules -> SyntaxRules
updateSyntaxRules [Syntax
s] SyntaxRules
rs,
                        syntax_keywords :: [String]
syntax_keywords = [String]
ks forall a. [a] -> [a] -> [a]
++ [String]
ns }
  where rs :: SyntaxRules
rs = IState -> SyntaxRules
syntax_rules IState
i
        ns :: [String]
ns = IState -> [String]
syntax_keywords IState
i
        ks :: [String]
ks = forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show (Syntax -> [Name]
syntaxNames Syntax
s)

{-| Parses a syntax extension declaration

@
SyntaxRuleOpts ::= 'term' | 'pattern';
@

@
SyntaxRule ::=
  SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
@

@
SyntaxSym ::=   '[' Name_t ']'
             |  '{' Name_t '}'
             |  Name_t
             |  StringLiteral_t
             ;
@
-}
syntaxRule :: SyntaxInfo -> IdrisParser Syntax
syntaxRule :: SyntaxInfo -> IdrisParser Syntax
syntaxRule SyntaxInfo
syn
    = do SynContext
sty <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do
            StateT IState (WriterT FC (Parsec Void String)) ()
pushIndent
            SynContext
sty <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option SynContext
AnySyntax
                            (SynContext
TermSyntax forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"term"
                             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SynContext
PatternSyntax forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"pattern")
            forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"syntax"
            forall (m :: * -> *) a. Monad m => a -> m a
return SynContext
sty)
         [SSymbol]
syms <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
some IdrisParser SSymbol
syntaxSym
         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SSymbol -> Bool
isExpr [SSymbol]
syms) forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a.
MonadParsec e s m =>
ErrorItem (Token s) -> m a
P.unexpected forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. NonEmpty Char -> ErrorItem t
P.Label forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> NonEmpty a
NonEmpty.fromList forall a b. (a -> b) -> a -> b
$ String
"missing keywords in syntax rule"
         let ns :: [Name]
ns = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SSymbol -> Maybe Name
getName [SSymbol]
syms
         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Eq a => [a] -> [a]
nub [Name]
ns))
            forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a.
MonadParsec e s m =>
ErrorItem (Token s) -> m a
P.unexpected forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. NonEmpty Char -> ErrorItem t
P.Label forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> NonEmpty a
NonEmpty.fromList forall a b. (a -> b) -> a -> b
$ String
"repeated variable in syntax rule"
         forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'='
         PTerm
tm <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
allowImp SyntaxInfo
syn) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Name] -> PTerm -> IdrisParser PTerm
uniquifyBinders [Name
n | Binding Name
n <- [SSymbol]
syms]
         StateT IState (WriterT FC (Parsec Void String)) ()
terminator
         forall (m :: * -> *) a. Monad m => a -> m a
return ([SSymbol] -> PTerm -> SynContext -> Syntax
Rule ([SSymbol] -> [SSymbol]
mkSimple [SSymbol]
syms) PTerm
tm SynContext
sty)
  forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"decl"; forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"syntax"
         [SSymbol]
syms <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
some IdrisParser SSymbol
syntaxSym
         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SSymbol -> Bool
isExpr [SSymbol]
syms) forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a.
MonadParsec e s m =>
ErrorItem (Token s) -> m a
P.unexpected forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. NonEmpty Char -> ErrorItem t
P.Label forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> NonEmpty a
NonEmpty.fromList forall a b. (a -> b) -> a -> b
$ String
"missing keywords in syntax rule"
         let ns :: [Name]
ns = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SSymbol -> Maybe Name
getName [SSymbol]
syms
         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. Eq a => [a] -> [a]
nub [Name]
ns))
            forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a.
MonadParsec e s m =>
ErrorItem (Token s) -> m a
P.unexpected forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. NonEmpty Char -> ErrorItem t
P.Label forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> NonEmpty a
NonEmpty.fromList forall a b. (a -> b) -> a -> b
$ String
"repeated variable in syntax rule"
         forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'='
         StateT IState (WriterT FC (Parsec Void String)) ()
openBlock
         [[PDecl]]
dec <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
some (SyntaxInfo -> IdrisParser [PDecl]
decl SyntaxInfo
syn)
         StateT IState (WriterT FC (Parsec Void String)) ()
closeBlock
         forall (m :: * -> *) a. Monad m => a -> m a
return ([SSymbol] -> [PDecl] -> Syntax
DeclRule ([SSymbol] -> [SSymbol]
mkSimple [SSymbol]
syms) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PDecl]]
dec))
  where
    isExpr :: SSymbol -> Bool
isExpr (Expr Name
_) = Bool
True
    isExpr SSymbol
_ = Bool
False
    getName :: SSymbol -> Maybe Name
getName (Expr Name
n) = forall a. a -> Maybe a
Just Name
n
    getName SSymbol
_ = forall a. Maybe a
Nothing
    -- Can't parse two full expressions (i.e. expressions with application) in a row
    -- so change them both to a simple expression
    mkSimple :: [SSymbol] -> [SSymbol]
mkSimple (Expr Name
e : [SSymbol]
es) = Name -> SSymbol
SimpleExpr Name
e forall a. a -> [a] -> [a]
: [SSymbol] -> [SSymbol]
mkSimple' [SSymbol]
es
    mkSimple [SSymbol]
xs = [SSymbol] -> [SSymbol]
mkSimple' [SSymbol]
xs

    mkSimple' :: [SSymbol] -> [SSymbol]
mkSimple' (Expr Name
e : Expr Name
e1 : [SSymbol]
es) = Name -> SSymbol
SimpleExpr Name
e forall a. a -> [a] -> [a]
: Name -> SSymbol
SimpleExpr Name
e1 forall a. a -> [a] -> [a]
:
                                           [SSymbol] -> [SSymbol]
mkSimple [SSymbol]
es
    -- Can't parse a full expression followed by operator like characters due to ambiguity
    mkSimple' (Expr Name
e : Symbol String
s : [SSymbol]
es)
      | forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
opChars) String
ts forall a. Eq a => a -> a -> Bool
/= String
"" = Name -> SSymbol
SimpleExpr Name
e forall a. a -> [a] -> [a]
: String -> SSymbol
Symbol String
s forall a. a -> [a] -> [a]
: [SSymbol] -> [SSymbol]
mkSimple' [SSymbol]
es
       where ts :: String
ts = forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
dropWhileEnd Char -> Bool
isSpace forall a b. (a -> b) -> a -> b
$ String
s
    mkSimple' (SSymbol
e : [SSymbol]
es) = SSymbol
e forall a. a -> [a] -> [a]
: [SSymbol] -> [SSymbol]
mkSimple' [SSymbol]
es
    mkSimple' [] = []

    -- Prevent syntax variable capture by making all binders under syntax unique
    -- (the ol' Common Lisp GENSYM approach)
    uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
    uniquifyBinders :: [Name] -> PTerm -> IdrisParser PTerm
uniquifyBinders [Name]
userNames = Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 []
      where
        fixBind :: Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
        fixBind :: Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens (PRef FC
fc [FC]
hls Name
n) | Just Name
n' <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Name)]
rens =
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
hls Name
n'
        fixBind Int
0 [(Name, Name)]
rens (PPatvar FC
fc Name
n) | Just Name
n' <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Name)]
rens =
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FC -> Name -> PTerm
PPatvar FC
fc Name
n'
        fixBind Int
0 [(Name, Name)]
rens (PLam FC
fc Name
n FC
nfc PTerm
ty PTerm
body)
          | Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
userNames = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n FC
nfc)
                                        (Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens PTerm
ty)
                                        (Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens PTerm
body)
          | Bool
otherwise =
            do PTerm
ty' <- Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens PTerm
ty
               Name
n' <- Name -> IdrisParser Name
gensym Name
n
               PTerm
body' <- Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 ((Name
n,Name
n')forall a. a -> [a] -> [a]
:[(Name, Name)]
rens) PTerm
body
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n' FC
nfc PTerm
ty' PTerm
body'
        fixBind Int
0 [(Name, Name)]
rens (PPi Plicity
plic Name
n FC
nfc PTerm
argTy PTerm
body)
          | Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
userNames = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
plic Name
n FC
nfc)
                                        (Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens PTerm
argTy)
                                        (Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens PTerm
body)
          | Bool
otherwise =
            do PTerm
ty' <- Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens PTerm
argTy
               Name
n' <- Name -> IdrisParser Name
gensym Name
n
               PTerm
body' <- Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 ((Name
n,Name
n')forall a. a -> [a] -> [a]
:[(Name, Name)]
rens) PTerm
body
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
plic Name
n' FC
nfc PTerm
ty' PTerm
body')
        fixBind Int
0 [(Name, Name)]
rens (PLet FC
fc RigCount
rig Name
n FC
nfc PTerm
ty PTerm
val PTerm
body)
          | Name
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
userNames = forall (m :: * -> *) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 (FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
rig Name
n FC
nfc)
                                        (Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens PTerm
ty)
                                        (Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens PTerm
val)
                                        (Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens PTerm
body)
          | Bool
otherwise =
            do PTerm
ty' <- Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens PTerm
ty
               PTerm
val' <- Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens PTerm
val
               Name
n' <- Name -> IdrisParser Name
gensym Name
n
               PTerm
body' <- Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 ((Name
n,Name
n')forall a. a -> [a] -> [a]
:[(Name, Name)]
rens) PTerm
body
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
rig Name
n' FC
nfc PTerm
ty' PTerm
val' PTerm
body'
        fixBind Int
0 [(Name, Name)]
rens (PMatchApp FC
fc Name
n) | Just Name
n' <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Name)]
rens =
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FC -> Name -> PTerm
PMatchApp FC
fc Name
n'
        -- Also rename resolved quotations, to allow syntax rules to
        -- have quoted references to their own bindings.
        fixBind Int
0 [(Name, Name)]
rens (PQuoteName Name
n Bool
True FC
fc) | Just Name
n' <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Name)]
rens =
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> Bool -> FC -> PTerm
PQuoteName Name
n' Bool
True FC
fc

        -- Don't mess with quoted terms
        fixBind Int
q [(Name, Name)]
rens (PQuasiquote PTerm
tm Maybe PTerm
goal) =
          forall a b c. (a -> b -> c) -> b -> a -> c
flip PTerm -> Maybe PTerm -> PTerm
PQuasiquote Maybe PTerm
goal forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind (Int
q forall a. Num a => a -> a -> a
+ Int
1) [(Name, Name)]
rens PTerm
tm
        fixBind Int
q [(Name, Name)]
rens (PUnquote PTerm
tm) =
          PTerm -> PTerm
PUnquote forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind (Int
q forall a. Num a => a -> a -> a
- Int
1) [(Name, Name)]
rens PTerm
tm

        fixBind Int
q [(Name, Name)]
rens PTerm
x = forall on (m :: * -> *).
(Uniplate on, Applicative m) =>
(on -> m on) -> on -> m on
descendM (Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
q [(Name, Name)]
rens) PTerm
x

        gensym :: Name -> IdrisParser Name
        gensym :: Name -> IdrisParser Name
gensym Name
n = do IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                      let idx :: Int
idx = IState -> Int
idris_name IState
ist
                      forall s (m :: * -> *). MonadState s m => s -> m ()
put IState
ist { idris_name :: Int
idris_name = Int
idx forall a. Num a => a -> a -> a
+ Int
1 }
                      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> String -> Name
sMN Int
idx (forall a. Show a => a -> String
show Name
n)

{-| Parses a syntax symbol (either binding variable, keyword or expression)

@
SyntaxSym ::=   '[' Name_t ']'
             |  '{' Name_t '}'
             |  Name_t
             |  StringLiteral_t
             ;
@
 -}
syntaxSym :: IdrisParser SSymbol
syntaxSym :: IdrisParser SSymbol
syntaxSym =    forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'['; Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name; forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
']'
                         forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> SSymbol
Expr Name
n))
            forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'{'; Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name; forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'}'
                          forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> SSymbol
Binding Name
n))
            forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Name
n <- forall (m :: * -> *). Parsing m => [String] -> m Name
iName []
                   forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> SSymbol
Keyword Name
n)
            forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String
sym <- forall (m :: * -> *). Parsing m => m String
stringLiteral
                   forall (m :: * -> *) a. Monad m => a -> m a
return (String -> SSymbol
Symbol String
sym)
            forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"syntax symbol"

{-| Parses a function declaration with possible syntax sugar

@
  FunDecl ::= FunDecl';
@
-}
fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
fnDecl SyntaxInfo
syn = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do StateT IState (WriterT FC (Parsec Void String)) ()
notEndBlock
                       PDecl
d <- SyntaxInfo -> IdrisParser PDecl
fnDecl' SyntaxInfo
syn
                       IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
                       let d' :: PDecl
d' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SyntaxInfo -> PTerm -> PTerm
debindApp SyntaxInfo
syn forall b c a. (b -> c) -> (a -> b) -> a -> c
. SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
i) PDecl
d
                       forall (m :: * -> *) a. Monad m => a -> m a
return [PDecl
d']) forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"function declaration"

{-| Parses a function declaration

@
 FunDecl' ::=
  DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
  | Postulate
  | Pattern
  | CAF
  ;
@
-}
fnDecl' :: SyntaxInfo -> IdrisParser PDecl
fnDecl' :: SyntaxInfo -> IdrisParser PDecl
fnDecl' SyntaxInfo
syn = (IdrisParser PDecl -> IdrisParser PDecl
checkDeclFixity forall a b. (a -> b) -> a -> b
$
              do (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs, FC
fc, FnOpts
opts', Name
n, FC
nfc, Accessibility
acc) <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do
                        StateT IState (WriterT FC (Parsec Void String)) ()
pushIndent
                        (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs) <- SyntaxInfo
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))])
docstring SyntaxInfo
syn
                        (FnOpts
opts, Accessibility
acc) <- IdrisParser (FnOpts, Accessibility)
fnOpts
                        (Name
n_in, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                        let n :: Name
n = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n_in
                        FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
                        forall (m :: * -> *) a. Monad m => a -> m a
return (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs, FC
fc, FnOpts
opts, Name
n, FC
nfc, Accessibility
acc))
                 PTerm
ty <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
allowImp SyntaxInfo
syn)
                 StateT IState (WriterT FC (Parsec Void String)) ()
terminator
                 -- If it's a top level function, note the accessibility
                 -- rules
                 forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SyntaxInfo -> Bool
syn_toplevel SyntaxInfo
syn) forall a b. (a -> b) -> a -> b
$ Name
-> Accessibility
-> StateT IState (WriterT FC (Parsec Void String)) ()
addAcc Name
n Accessibility
acc
                 forall (m :: * -> *) a. Monad m => a -> m a
return (forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> t
-> PDecl' t
PTy Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
syn FC
fc FnOpts
opts' Name
n FC
nfc PTerm
ty)
            forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
postulate SyntaxInfo
syn
            forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
caf SyntaxInfo
syn
            forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
pattern SyntaxInfo
syn)
            forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"function declaration"

{-| Parses a series of function and accessbility options

@
FnOpts ::= FnOpt* Accessibility FnOpt*
@
 -}
fnOpts :: IdrisParser ([FnOpt], Accessibility)
fnOpts :: IdrisParser (FnOpts, Accessibility)
fnOpts = do
    FnOpts
opts <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many IdrisParser FnOpt
fnOpt
    Accessibility
acc <- IdrisParser Accessibility
accessibility
    FnOpts
opts' <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many IdrisParser FnOpt
fnOpt
    let allOpts :: FnOpts
allOpts = FnOpts
opts forall a. [a] -> [a] -> [a]
++ FnOpts
opts'
    let existingTotality :: FnOpts
existingTotality = FnOpts
allOpts forall a. Eq a => [a] -> [a] -> [a]
`intersect` [FnOpt
TotalFn, FnOpt
CoveringFn, FnOpt
PartialFn]
    FnOpts
opts'' <- forall {m :: * -> *}.
(MonadState IState m, MonadFail m) =>
FnOpts -> FnOpts -> m FnOpts
addDefaultTotality (forall a. Eq a => [a] -> [a]
nub FnOpts
existingTotality) FnOpts
allOpts
    forall (m :: * -> *) a. Monad m => a -> m a
return (FnOpts
opts'', Accessibility
acc)
  where prettyTot :: FnOpt -> String
prettyTot FnOpt
TotalFn = String
"total"
        prettyTot FnOpt
PartialFn = String
"partial"
        prettyTot FnOpt
CoveringFn = String
"covering"
        addDefaultTotality :: FnOpts -> FnOpts -> m FnOpts
addDefaultTotality [] FnOpts
opts = do
          IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
          case IState -> DefaultTotality
default_total IState
ist of
            DefaultTotality
DefaultCheckingTotal    -> forall (m :: * -> *) a. Monad m => a -> m a
return (FnOpt
TotalFnforall a. a -> [a] -> [a]
:FnOpts
opts)
            DefaultTotality
DefaultCheckingCovering -> forall (m :: * -> *) a. Monad m => a -> m a
return (FnOpt
CoveringFnforall a. a -> [a] -> [a]
:FnOpts
opts)
            DefaultTotality
DefaultCheckingPartial  -> forall (m :: * -> *) a. Monad m => a -> m a
return FnOpts
opts -- Don't add partial so that --warn-partial still reports warnings if necessary
        addDefaultTotality [FnOpt
tot] FnOpts
opts = forall (m :: * -> *) a. Monad m => a -> m a
return FnOpts
opts
        -- Should really be a semantics error instead of a parser error
        addDefaultTotality (FnOpt
tot1:FnOpt
tot2:FnOpts
tots) FnOpts
opts =
          forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Conflicting totality modifiers specified " forall a. [a] -> [a] -> [a]
++ FnOpt -> String
prettyTot FnOpt
tot1 forall a. [a] -> [a] -> [a]
++ String
" and " forall a. [a] -> [a] -> [a]
++ FnOpt -> String
prettyTot FnOpt
tot2)


{-| Parses a function option

@
FnOpt ::= 'total'
  | 'partial'
  | 'covering'
  | 'implicit'
  | '%' 'no_implicit'
  | '%' 'assert_total'
  | '%' 'error_handler'
  | '%' 'reflection'
  | '%' 'specialise' '[' NameTimesList? ']'
  ;
@

@
NameTimes ::= FnName Natural?;
@

@
NameTimesList ::=
  NameTimes
  | NameTimes ',' NameTimesList
  ;
@
-}
fnOpt :: IdrisParser FnOpt
fnOpt :: IdrisParser FnOpt
fnOpt = do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"total"; forall (m :: * -> *) a. Monad m => a -> m a
return FnOpt
TotalFn
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
PartialFn forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"partial"
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
CoveringFn forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"covering"
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"export"); String
c <- forall (m :: * -> *). Parsing m => m String
stringLiteral;
                      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> FnOpt
CExport String
c
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
NoImplicit forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"no_implicit")
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
Inlinable forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"inline")
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
StaticFn forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"static")
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
ErrorHandler forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"error_handler")
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
ErrorReverse forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"error_reverse")
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
ErrorReduce  forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"error_reduce")
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
Reflection   forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"reflection")
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
AutoHint     forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"hint")
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
OverlappingDictionary forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"overlapping")
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%'; forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"specialise";
               forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'['; [(Name, Maybe Int)]
ns <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy IdrisParser (Name, Maybe Int)
nameTimes (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','); forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
']';
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [(Name, Maybe Int)] -> FnOpt
Specialise [(Name, Maybe Int)]
ns
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
Implicit forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"implicit"
        forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"function modifier"
  where nameTimes :: IdrisParser (Name, Maybe Int)
        nameTimes :: IdrisParser (Name, Maybe Int)
nameTimes = do Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                       Maybe Int
t <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option forall a. Maybe a
Nothing (do Integer
reds <- forall (m :: * -> *). Parsing m => m Integer
natural
                                                 forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (forall a. Num a => Integer -> a
fromInteger Integer
reds)))
                       forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, Maybe Int
t)

{-| Parses a postulate

@
Postulate ::=
  DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
  ;
@
-}
postulate :: SyntaxInfo -> IdrisParser PDecl
postulate :: SyntaxInfo -> IdrisParser PDecl
postulate SyntaxInfo
syn = do (Docstring (Either Err PTerm)
doc, Bool
ext)
                       <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try forall a b. (a -> b) -> a -> b
$ do (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
_) <- SyntaxInfo
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))])
docstring SyntaxInfo
syn
                                     StateT IState (WriterT FC (Parsec Void String)) ()
pushIndent
                                     Bool
ext <- StateT IState (WriterT FC (Parsec Void String)) Bool
ppostDecl
                                     forall (m :: * -> *) a. Monad m => a -> m a
return (Docstring (Either Err PTerm)
doc, Bool
ext)
                   IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                   (FnOpts
opts, Accessibility
acc) <- IdrisParser (FnOpts, Accessibility)
fnOpts
                   (Name
n_in, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                   let n :: Name
n = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n_in
                   forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
                   PTerm
ty <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
allowImp SyntaxInfo
syn)
                   FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ StateT IState (WriterT FC (Parsec Void String)) ()
terminator
                   Name
-> Accessibility
-> StateT IState (WriterT FC (Parsec Void String)) ()
addAcc Name
n Accessibility
acc
                   forall (m :: * -> *) a. Monad m => a -> m a
return (forall t.
Bool
-> Docstring (Either Err t)
-> SyntaxInfo
-> FC
-> FC
-> FnOpts
-> Name
-> t
-> PDecl' t
PPostulate Bool
ext Docstring (Either Err PTerm)
doc SyntaxInfo
syn FC
fc FC
nfc FnOpts
opts Name
n PTerm
ty)
                 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"postulate"
   where ppostDecl :: StateT IState (WriterT FC (Parsec Void String)) Bool
ppostDecl = do ()
fc <- forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"postulate"; forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%'; forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"extern"; forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

{-| Parses a using declaration

@
Using ::=
  'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
  ;
@
 -}
using_ :: SyntaxInfo -> IdrisParser [PDecl]
using_ :: SyntaxInfo -> IdrisParser [PDecl]
using_ SyntaxInfo
syn =
    do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"using"
       forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'('; [Using]
ns <- SyntaxInfo -> IdrisParser [Using]
usingDeclList SyntaxInfo
syn; forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'
       StateT IState (WriterT FC (Parsec Void String)) ()
openBlock
       let uvars :: [Using]
uvars = SyntaxInfo -> [Using]
using SyntaxInfo
syn
       [[PDecl]]
ds <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (SyntaxInfo -> IdrisParser [PDecl]
decl (SyntaxInfo
syn { using :: [Using]
using = [Using]
uvars forall a. [a] -> [a] -> [a]
++ [Using]
ns }))
       StateT IState (WriterT FC (Parsec Void String)) ()
closeBlock
       forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PDecl]]
ds)
    forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"using declaration"

{-| Parses a parameters declaration

@
Params ::=
  'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
  ;
@
-}
params :: SyntaxInfo -> IdrisParser [PDecl]
params :: SyntaxInfo -> IdrisParser [PDecl]
params SyntaxInfo
syn =
    do ([(RigCount, Name, FC, PTerm)]
ns, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ do
          forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"parameters"
          forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'(' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [(RigCount, Name, FC, PTerm)]
typeDeclList SyntaxInfo
syn forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'
       let ns' :: [(Name, PTerm)]
ns' = [(Name
n, PTerm
ty) | (RigCount
_, Name
n, FC
_, PTerm
ty) <- [(RigCount, Name, FC, PTerm)]
ns]
       StateT IState (WriterT FC (Parsec Void String)) ()
openBlock
       let pvars :: [(Name, PTerm)]
pvars = SyntaxInfo -> [(Name, PTerm)]
syn_params SyntaxInfo
syn
       [[PDecl]]
ds <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (SyntaxInfo -> IdrisParser [PDecl]
decl SyntaxInfo
syn { syn_params :: [(Name, PTerm)]
syn_params = [(Name, PTerm)]
pvars forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)]
ns' })
       StateT IState (WriterT FC (Parsec Void String)) ()
closeBlock
       forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. FC -> [(Name, t)] -> [PDecl' t] -> PDecl' t
PParams FC
fc [(Name, PTerm)]
ns' (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PDecl]]
ds)]
    forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"parameters declaration"

-- | Parses an open block
openInterface :: SyntaxInfo -> IdrisParser [PDecl]
openInterface :: SyntaxInfo -> IdrisParser [PDecl]
openInterface SyntaxInfo
syn =
    do ([(Name, FC)]
ns, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ do
         forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"using"
         forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"implementation"
         forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')

       StateT IState (WriterT FC (Parsec Void String)) ()
openBlock
       [[PDecl]]
ds <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (SyntaxInfo -> IdrisParser [PDecl]
decl SyntaxInfo
syn)
       StateT IState (WriterT FC (Parsec Void String)) ()
closeBlock
       forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. FC -> [Name] -> [PDecl' t] -> PDecl' t
POpenInterfaces FC
fc (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, FC)]
ns) (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PDecl]]
ds)]
    forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"open interface declaration"





{-| Parses a mutual declaration (for mutually recursive functions)

@
Mutual ::=
  'mutual' OpenBlock Decl* CloseBlock
  ;
@
-}
mutual :: SyntaxInfo -> IdrisParser [PDecl]
mutual :: SyntaxInfo -> IdrisParser [PDecl]
mutual SyntaxInfo
syn =
    do FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"mutual"
       StateT IState (WriterT FC (Parsec Void String)) ()
openBlock
       [[PDecl]]
ds <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (SyntaxInfo -> IdrisParser [PDecl]
decl (SyntaxInfo
syn { mut_nesting :: Int
mut_nesting = SyntaxInfo -> Int
mut_nesting SyntaxInfo
syn forall a. Num a => a -> a -> a
+ Int
1 } ))
       StateT IState (WriterT FC (Parsec Void String)) ()
closeBlock
       forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. FC -> [PDecl' t] -> PDecl' t
PMutual FC
fc (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PDecl]]
ds)]
    forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"mutual block"

{-| Parses a namespace declaration

@
Namespace ::=
  'namespace' identifier OpenBlock Decl+ CloseBlock
  ;
@
-}
namespace :: SyntaxInfo -> IdrisParser [PDecl]
namespace :: SyntaxInfo -> IdrisParser [PDecl]
namespace SyntaxInfo
syn =
    do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"namespace"
       (String
n, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). Parsing m => m String
identifier
       StateT IState (WriterT FC (Parsec Void String)) ()
openBlock
       [[PDecl]]
ds <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
some (SyntaxInfo -> IdrisParser [PDecl]
decl SyntaxInfo
syn { syn_namespace :: [String]
syn_namespace = String
n forall a. a -> [a] -> [a]
: SyntaxInfo -> [String]
syn_namespace SyntaxInfo
syn })
       StateT IState (WriterT FC (Parsec Void String)) ()
closeBlock
       forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. String -> FC -> [PDecl' t] -> PDecl' t
PNamespace String
n FC
nfc (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PDecl]]
ds)]
     forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"namespace declaration"

{-| Parses a methods block (for implementations)

@
  ImplementationBlock ::= 'where' OpenBlock FnDecl* CloseBlock
@
-}
implementationBlock :: SyntaxInfo -> IdrisParser [PDecl]
implementationBlock :: SyntaxInfo -> IdrisParser [PDecl]
implementationBlock SyntaxInfo
syn = do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"where"
                             StateT IState (WriterT FC (Parsec Void String)) ()
openBlock
                             [[PDecl]]
ds <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (SyntaxInfo -> IdrisParser [PDecl]
fnDecl SyntaxInfo
syn)
                             StateT IState (WriterT FC (Parsec Void String)) ()
closeBlock
                             forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PDecl]]
ds)
                          forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"implementation block"

{-| Parses a methods and implementations block (for interfaces)

@
MethodOrImplementation ::=
   FnDecl
   | Implementation
   ;
@

@
InterfaceBlock ::=
  'where' OpenBlock Constructor? MethodOrImplementation* CloseBlock
  ;
@
-}
interfaceBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
interfaceBlock :: SyntaxInfo
-> IdrisParser
     (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
interfaceBlock SyntaxInfo
syn = do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"where"
                        StateT IState (WriterT FC (Parsec Void String)) ()
openBlock
                        (Maybe (Name, FC)
cn, Docstring ()
cd) <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (forall a. Maybe a
Nothing, forall a. Docstring a
emptyDocstring) forall a b. (a -> b) -> a -> b
$
                                    forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (Docstring ()
doc, [(Name, Docstring ())]
_) <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option forall a. (Docstring a, [(Name, Docstring a)])
noDocs IdrisParser (Docstring (), [(Name, Docstring ())])
docComment
                                              (Name, FC)
n <- IdrisParser (Name, FC)
constructor
                                              forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (Name, FC)
n, Docstring ()
doc))
                        IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                        let cd' :: Docstring (Either Err PTerm)
cd' = SyntaxInfo
-> IState -> Docstring () -> Docstring (Either Err PTerm)
annotate SyntaxInfo
syn IState
ist Docstring ()
cd

                        [[PDecl]]
ds <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (StateT IState (WriterT FC (Parsec Void String)) ()
notEndBlock forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser [PDecl]
implementation SyntaxInfo
syn)
                                                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do PDecl
x <- SyntaxInfo -> IdrisParser PDecl
data_ SyntaxInfo
syn
                                                          forall (m :: * -> *) a. Monad m => a -> m a
return [PDecl
x]
                                                   forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
fnDecl SyntaxInfo
syn)
                        StateT IState (WriterT FC (Parsec Void String)) ()
closeBlock
                        forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Name, FC)
cn, Docstring (Either Err PTerm)
cd', forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PDecl]]
ds)
                     forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"interface block"
  where
    constructor :: IdrisParser (Name, FC)
    constructor :: IdrisParser (Name, FC)
constructor = forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"constructor" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName

    annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
    annotate :: SyntaxInfo
-> IState -> Docstring () -> Docstring (Either Err PTerm)
annotate SyntaxInfo
syn IState
ist = forall a b. (String -> b) -> Docstring a -> Docstring b
annotCode forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IState -> String -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist

{-| Parses an interface declaration

@
InterfaceArgument ::=
   Name
   | '(' Name ':' Expr ')'
   ;
@

@
Interface ::=
  DocComment_t? Accessibility? 'interface' ConstraintList? Name InterfaceArgument* InterfaceBlock?
  ;
@
-}
interface_ :: SyntaxInfo -> IdrisParser [PDecl]
interface_ :: SyntaxInfo -> IdrisParser [PDecl]
interface_ SyntaxInfo
syn = do (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs, Accessibility
acc)
                      <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs) <- SyntaxInfo
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))])
docstring SyntaxInfo
syn
                                   Accessibility
acc <- IdrisParser Accessibility
accessibility
                                   StateT IState (WriterT FC (Parsec Void String)) ()
interfaceKeyword
                                   forall (m :: * -> *) a. Monad m => a -> m a
return (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs, Accessibility
acc))
                    (([(Name, PTerm)]
cons', Name
n, FC
nfc, [(Name, FC, PTerm)]
cs, [(Name, FC)]
fds), FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ do
                        [(RigCount, Name, FC, PTerm)]
cons <- SyntaxInfo
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [(RigCount, Name, FC, PTerm)]
constraintList SyntaxInfo
syn
                        let cons' :: [(Name, PTerm)]
cons' = [(Name
c, PTerm
ty) | (RigCount
_, Name
c, FC
_, PTerm
ty) <- [(RigCount, Name, FC, PTerm)]
cons]
                        (Name
n_in, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                        let n :: Name
n = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n_in
                        [(Name, FC, PTerm)]
cs <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many IdrisParser (Name, FC, PTerm)
carg
                        [(Name, FC)]
fds <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option [(Name
cn, FC
NoFC) | (Name
cn, FC
_, PTerm
_) <- [(Name, FC, PTerm)]
cs] StateT IState (WriterT FC (Parsec Void String)) [(Name, FC)]
fundeps
                        forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, PTerm)]
cons', Name
n, FC
nfc, [(Name, FC, PTerm)]
cs, [(Name, FC)]
fds)

                    (Maybe (Name, FC)
cn, Docstring (Either Err PTerm)
cd, [PDecl]
ds) <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (forall a. Maybe a
Nothing, forall a b. (a, b) -> a
fst forall a. (Docstring a, [(Name, Docstring a)])
noDocs, []) (SyntaxInfo
-> IdrisParser
     (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
interfaceBlock SyntaxInfo
syn)
                    Accessibility
-> Name
-> [Name]
-> StateT IState (WriterT FC (Parsec Void String)) ()
accData Accessibility
acc Name
n (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl -> [Name]
declared [PDecl]
ds)
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t.
Docstring (Either Err t)
-> SyntaxInfo
-> FC
-> [(Name, t)]
-> Name
-> FC
-> [(Name, FC, t)]
-> [(Name, Docstring (Either Err t))]
-> [(Name, FC)]
-> [PDecl' t]
-> Maybe (Name, FC)
-> Docstring (Either Err t)
-> PDecl' t
PInterface Docstring (Either Err PTerm)
doc SyntaxInfo
syn FC
fc [(Name, PTerm)]
cons' Name
n FC
nfc [(Name, FC, PTerm)]
cs [(Name, Docstring (Either Err PTerm))]
argDocs [(Name, FC)]
fds [PDecl]
ds Maybe (Name, FC)
cn Docstring (Either Err PTerm)
cd]
                 forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"interface declaration"
  where
    fundeps :: IdrisParser [(Name, FC)]
    fundeps :: StateT IState (WriterT FC (Parsec Void String)) [(Name, FC)]
fundeps = do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|'; forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy (forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')

    classWarning :: String
    classWarning :: String
classWarning = String
"Use of a fragile keyword `class`. " forall a. [a] -> [a] -> [a]
++
                   String
"`class` is provided for those coming from Haskell. " forall a. [a] -> [a] -> [a]
++
                   String
"Please use `interface` instead, which is equivalent."

    interfaceKeyword :: IdrisParser ()
    interfaceKeyword :: StateT IState (WriterT FC (Parsec Void String)) ()
interfaceKeyword = forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"interface"
               forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"class"
                      FC
-> Maybe Opt
-> Err
-> StateT IState (WriterT FC (Parsec Void String)) ()
parserWarning FC
fc forall a. Maybe a
Nothing (forall t. String -> Err' t
Msg String
classWarning)

    carg :: IdrisParser (Name, FC, PTerm)
    carg :: IdrisParser (Name, FC, PTerm)
carg = do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'('; (Name
i, FC
ifc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name; forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'; PTerm
ty <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn; forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'
              forall (m :: * -> *) a. Monad m => a -> m a
return (Name
i, FC
ifc, PTerm
ty)
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do (Name
i, FC
ifc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
              forall (m :: * -> *) a. Monad m => a -> m a
return (Name
i, FC
ifc, FC -> PTerm
PType FC
ifc)

{-| Parses an interface implementation declaration

@
  Implementation ::=
    DocComment_t? 'implementation' ImplementationName? ConstraintList? Name SimpleExpr* ImplementationBlock?
    ;
@

@
ImplementationName ::= '[' Name ']';
@
-}
implementation :: SyntaxInfo -> IdrisParser [PDecl]
implementation :: SyntaxInfo -> IdrisParser [PDecl]
implementation SyntaxInfo
syn = do (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
argDocs) <- SyntaxInfo
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))])
docstring SyntaxInfo
syn
                        (FnOpts
opts, Accessibility
acc) <- IdrisParser (FnOpts, Accessibility)
fnOpts
                        forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional StateT IState (WriterT FC (Parsec Void String)) ()
implementationKeyword

                        ((Maybe Name
en, [(RigCount, Name, FC, PTerm)]
cs, [(Name, PTerm)]
cs', Name
cn, FC
cnfc, [PTerm]
args, [Name]
pnames), FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ do
                            Maybe Name
en <- forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional IdrisParser Name
implementationName
                            [(RigCount, Name, FC, PTerm)]
cs <- SyntaxInfo
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [(RigCount, Name, FC, PTerm)]
constraintList SyntaxInfo
syn
                            let cs' :: [(Name, PTerm)]
cs' = [(Name
c, PTerm
ty) | (RigCount
_, Name
c, FC
_, PTerm
ty) <- [(RigCount, Name, FC, PTerm)]
cs]
                            (Name
cn, FC
cnfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                            [PTerm]
args <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn)
                            [Name]
pnames <- IdrisParser [Name]
implementationUsing
                            forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Name
en, [(RigCount, Name, FC, PTerm)]
cs, [(Name, PTerm)]
cs', Name
cn, FC
cnfc, [PTerm]
args, [Name]
pnames)

                        let sc :: PTerm
sc = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
cnfc [FC
cnfc] Name
cn) (forall a b. (a -> b) -> [a] -> [b]
map forall {t}. t -> PArg' t
pexp [PTerm]
args)
                        let t :: PTerm
t = (RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm)
-> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList (\RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
constraint { pcount :: RigCount
pcount = RigCount
r }) [(RigCount, Name, FC, PTerm)]
cs PTerm
sc

                        [PDecl]
ds <- SyntaxInfo -> IdrisParser [PDecl]
implementationBlock SyntaxInfo
syn
                        forall (m :: * -> *) a. Monad m => a -> m a
return [forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [(Name, t)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [t]
-> [(Name, t)]
-> t
-> Maybe Name
-> [PDecl' t]
-> PDecl' t
PImplementation Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
syn FC
fc [(Name, PTerm)]
cs' [Name]
pnames Accessibility
acc FnOpts
opts Name
cn FC
cnfc [PTerm]
args [] PTerm
t Maybe Name
en [PDecl]
ds]
                      forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"implementation declaration"
  where implementationName :: IdrisParser Name
        implementationName :: IdrisParser Name
implementationName = do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'['; Name
n_in <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName; forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
']'
                                let n :: Name
n = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n_in
                                forall (m :: * -> *) a. Monad m => a -> m a
return Name
n
                             forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"implementation name"

        instanceWarning :: String
        instanceWarning :: String
instanceWarning = String
"Use of fragile keyword `instance`. " forall a. [a] -> [a] -> [a]
++
                          String
"`instance` is provided for those coming from Haskell. " forall a. [a] -> [a] -> [a]
++
                          String
"Please use `implementation` (which is equivalent) instead, or omit it."

        implementationKeyword :: IdrisParser ()
        implementationKeyword :: StateT IState (WriterT FC (Parsec Void String)) ()
implementationKeyword = forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"implementation"
                         forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"instance"
                                FC
-> Maybe Opt
-> Err
-> StateT IState (WriterT FC (Parsec Void String)) ()
parserWarning FC
fc forall a. Maybe a
Nothing (forall t. String -> Err' t
Msg String
instanceWarning)

        implementationUsing :: IdrisParser [Name]
        implementationUsing :: IdrisParser [Name]
implementationUsing = do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"using"
                                 [(Name, FC)]
ns <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                                 forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Name, FC)]
ns)
                              forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. Monad m => a -> m a
return []

-- | Parse a docstring
docstring :: SyntaxInfo
          -> IdrisParser (Docstring (Either Err PTerm),
                          [(Name,Docstring (Either Err PTerm))])
docstring :: SyntaxInfo
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))])
docstring SyntaxInfo
syn = do (Docstring ()
doc, [(Name, Docstring ())]
argDocs) <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option forall a. (Docstring a, [(Name, Docstring a)])
noDocs IdrisParser (Docstring (), [(Name, Docstring ())])
docComment
                   IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                   let doc' :: Docstring (Either Err PTerm)
doc' = forall a b. (String -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> String -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
doc
                       argDocs' :: [(Name, Docstring (Either Err PTerm))]
argDocs' = [ (Name
n, forall a b. (String -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> String -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
d)
                                  | (Name
n, Docstring ()
d) <- [(Name, Docstring ())]
argDocs ]
                   forall (m :: * -> *) a. Monad m => a -> m a
return (Docstring (Either Err PTerm)
doc', [(Name, Docstring (Either Err PTerm))]
argDocs')


{-| Parses a using declaration list

@
UsingDeclList ::=
  UsingDeclList'
  | NameList TypeSig
  ;
@

@
UsingDeclList' ::=
  UsingDecl
  | UsingDecl ',' UsingDeclList'
  ;
@

@
NameList ::=
  Name
  | Name ',' NameList
  ;
@
-}
usingDeclList :: SyntaxInfo -> IdrisParser [Using]
usingDeclList :: SyntaxInfo -> IdrisParser [Using]
usingDeclList SyntaxInfo
syn
               = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser Using
usingDecl SyntaxInfo
syn) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','))
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do [Name]
ns <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                    forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
                    PTerm
t <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map (\Name
x -> Name -> PTerm -> Using
UImplicit Name
x PTerm
t) [Name]
ns)
             forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"using declaration list"

{-| Parses a using declaration

@
UsingDecl ::=
  FnName TypeSig
  | FnName FnName+
  ;
@
-}
usingDecl :: SyntaxInfo -> IdrisParser Using
usingDecl :: SyntaxInfo -> IdrisParser Using
usingDecl SyntaxInfo
syn = forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do Name
x <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                          forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'
                          PTerm
t <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                          forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> PTerm -> Using
UImplicit Name
x PTerm
t))
            forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Name
c <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                   [Name]
xs <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                   forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> [Name] -> Using
UConstraint Name
c [Name]
xs)
            forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"using declaration"

{-| Parse a clause with patterns

@
Pattern ::= Clause;
@
-}
pattern :: SyntaxInfo -> IdrisParser PDecl
pattern :: SyntaxInfo -> IdrisParser PDecl
pattern SyntaxInfo
syn = do (PClause' PTerm
clause, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (SyntaxInfo -> IdrisParser (PClause' PTerm)
clause SyntaxInfo
syn)
                 forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc [] (Int -> String -> Name
sMN Int
2 String
"_") [PClause' PTerm
clause]) -- collect together later
              forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"pattern"

{-| Parse a constant applicative form declaration

@
CAF ::= 'let' FnName '=' Expr Terminator;
@
-}
caf :: SyntaxInfo -> IdrisParser PDecl
caf :: SyntaxInfo -> IdrisParser PDecl
caf SyntaxInfo
syn = do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"let"
             (Name
n, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName)
             StateT IState (WriterT FC (Parsec Void String)) ()
pushIndent
             forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'='
             PTerm
t <- forall a. IdrisParser a -> IdrisParser a
indented forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
             StateT IState (WriterT FC (Parsec Void String)) ()
terminator
             forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. FC -> Name -> t -> PDecl' t
PCAF FC
fc Name
n PTerm
t)
           forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"constant applicative form declaration"

{-| Parse an argument expression

@
ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
@
-}
argExpr :: SyntaxInfo -> IdrisParser PTerm
argExpr :: SyntaxInfo -> IdrisParser PTerm
argExpr SyntaxInfo
syn = let syn' :: SyntaxInfo
syn' = SyntaxInfo
syn { inPattern :: Bool
inPattern = Bool
True } in
                  forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser PTerm
hsimpleExpr SyntaxInfo
syn') forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
simpleExternalExpr SyntaxInfo
syn'
              forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"argument expression"

{-| Parse a right hand side of a function

@
RHS ::= '='            Expr
     |  '?='  RHSName? Expr
     |  Impossible
     ;
@

@
RHSName ::= '{' FnName '}';
@
-}
rhs :: SyntaxInfo -> Name -> IdrisParser (PTerm, FC)
rhs :: SyntaxInfo -> Name -> IdrisParser (PTerm, FC)
rhs SyntaxInfo
syn Name
n = do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'='
               forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt
               forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => String -> m ()
symbol String
"?=";
               (Name
name, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option Name
n' (forall (m :: * -> *). Parsing m => String -> m ()
symbol String
"{" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (m :: * -> *). Parsing m => String -> m ()
symbol String
"}")
               PTerm
r <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
               forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Name -> PTerm -> PTerm
addLet FC
fc Name
name PTerm
r, FC
fc)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent IdrisParser PTerm
impossible
        forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"function right hand side"
  where mkN :: Name -> Name
        mkN :: Name -> Name
mkN (UN Text
x)   = if (Text -> Bool
tnull Text
x Bool -> Bool -> Bool
|| Bool -> Bool
not (Char -> Bool
isAlpha (Text -> Char
thead Text
x)))
                         then String -> Name
sUN String
"infix_op_lemma_1"
                         else String -> Name
sUN (Text -> String
str Text
xforall a. [a] -> [a] -> [a]
++String
"_lemma_1")
        mkN (NS Name
x [Text]
n) = Name -> [Text] -> Name
NS (Name -> Name
mkN Name
x) [Text]
n
        n' :: Name
        n' :: Name
n' = Name -> Name
mkN Name
n
        addLet :: FC -> Name -> PTerm -> PTerm
        addLet :: FC -> Name -> PTerm -> PTerm
addLet FC
fc Name
nm (PLet FC
fc' RigCount
rig Name
n FC
nfc PTerm
ty PTerm
val PTerm
r) = FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc' RigCount
rig Name
n FC
nfc PTerm
ty PTerm
val (FC -> Name -> PTerm -> PTerm
addLet FC
fc Name
nm PTerm
r)
        addLet FC
fc Name
nm (PCase FC
fc' PTerm
t [(PTerm, PTerm)]
cs) = FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc' PTerm
t (forall a b. (a -> b) -> [a] -> [b]
map forall {a}. (a, PTerm) -> (a, PTerm)
addLetC [(PTerm, PTerm)]
cs)
          where addLetC :: (a, PTerm) -> (a, PTerm)
addLetC (a
l, PTerm
r) = (a
l, FC -> Name -> PTerm -> PTerm
addLet FC
fc Name
nm PTerm
r)
        addLet FC
fc Name
nm PTerm
r = (FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
RigW (String -> Name
sUN String
"value") FC
NoFC PTerm
Placeholder PTerm
r (FC -> Name -> PTerm
PMetavar FC
NoFC Name
nm))

{-|Parses a function clause

@
RHSOrWithBlock ::= RHS WhereOrTerminator
               | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
               ;
@

@
Clause ::=                                                               WExpr+ RHSOrWithBlock
       |   SimpleExpr '<=='  FnName                                             RHS WhereOrTerminator
       |   ArgExpr Operator ArgExpr                                      WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
       |                     FnName ConstraintArg* ImplicitOrArgExpr*    WExpr* RHSOrWithBlock
       ;
@

@
ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
@

@
WhereOrTerminator ::= WhereBlock | Terminator;
@
-}
clause :: SyntaxInfo -> IdrisParser PClause
clause :: SyntaxInfo -> IdrisParser (PClause' PTerm)
clause SyntaxInfo
syn
           -- unnamed with or function clause (inside a with)
         = do [PTerm]
wargs <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do StateT IState (WriterT FC (Parsec Void String)) ()
pushIndent; forall (f :: * -> *) a. Alternative f => f a -> f [a]
some (SyntaxInfo -> IdrisParser PTerm
wExpr SyntaxInfo
syn))
              IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
              Name
n <- case IState -> Maybe Name
lastParse IState
ist of
                        Just Name
t -> forall (m :: * -> *) a. Monad m => a -> m a
return Name
t
                        Maybe Name
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Invalid clause"
              (do (PTerm
r, FC
fc) <- SyntaxInfo -> Name -> IdrisParser (PTerm, FC)
rhs SyntaxInfo
syn Name
n
                  let wsyn :: SyntaxInfo
wsyn = SyntaxInfo
syn { syn_namespace :: [String]
syn_namespace = [], syn_toplevel :: Bool
syn_toplevel = Bool
False }
                  ([PDecl]
wheres, [(Name, Name)]
nmap) <-     Name
-> SyntaxInfo
-> StateT
     IState (WriterT FC (Parsec Void String)) ([PDecl], [(Name, Name)])
whereBlock Name
n SyntaxInfo
wsyn forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* StateT IState (WriterT FC (Parsec Void String)) ()
popIndent
                                    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([], []) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT IState (WriterT FC (Parsec Void String)) ()
terminator
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. FC -> [t] -> t -> [PDecl' t] -> PClause' t
PClauseR FC
fc [PTerm]
wargs PTerm
r [PDecl]
wheres) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do
                  StateT IState (WriterT FC (Parsec Void String)) ()
popIndent
                  ((PTerm
wval, Maybe (Name, FC)
pn), FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ do
                      forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"with"
                      PTerm
wval <- SyntaxInfo -> IdrisParser PTerm
bracketed SyntaxInfo
syn
                      Maybe (Name, FC)
pn <- StateT IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
optProof
                      forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
wval, Maybe (Name, FC)
pn)
                  StateT IState (WriterT FC (Parsec Void String)) ()
openBlock
                  [[PDecl]]
ds <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
some forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser [PDecl]
fnDecl SyntaxInfo
syn
                  let withs :: [PDecl]
withs = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PDecl]]
ds
                  StateT IState (WriterT FC (Parsec Void String)) ()
closeBlock
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t.
FC -> [t] -> t -> Maybe (Name, FC) -> [PDecl' t] -> PClause' t
PWithR FC
fc [PTerm]
wargs PTerm
wval Maybe (Name, FC)
pn [PDecl]
withs)
           -- <==
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do PTerm
ty <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do StateT IState (WriterT FC (Parsec Void String)) ()
pushIndent
                              PTerm
ty <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
                              forall (m :: * -> *). Parsing m => String -> m ()
symbol String
"<=="
                              forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
ty)
              (Name
n, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName)
              (PTerm
r, FC
_) <- SyntaxInfo -> Name -> IdrisParser (PTerm, FC)
rhs SyntaxInfo
syn Name
n
              let wsyn :: SyntaxInfo
wsyn = SyntaxInfo
syn { syn_namespace :: [String]
syn_namespace = [] }
              ([PDecl]
wheres, [(Name, Name)]
nmap) <-   Name
-> SyntaxInfo
-> StateT
     IState (WriterT FC (Parsec Void String)) ([PDecl], [(Name, Name)])
whereBlock Name
n SyntaxInfo
wsyn forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* StateT IState (WriterT FC (Parsec Void String)) ()
popIndent
                                forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([], []) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT IState (WriterT FC (Parsec Void String)) ()
terminator
              let capp :: PTerm
capp = FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
RigW (Int -> String -> Name
sMN Int
0 String
"match") FC
NoFC
                              PTerm
ty
                              (FC -> Name -> PTerm
PMatchApp FC
fc Name
n)
                              (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> String -> Name
sMN Int
0 String
"match"))
              IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
              forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
ist { lastParse :: Maybe Name
lastParse = forall a. a -> Maybe a
Just Name
n })
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
n PTerm
capp [] PTerm
r [PDecl]
wheres
           -- lhs application "with" clause or function clause
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
pushIndent
              (Name
n, FC
nfc, PTerm
capp, [PTerm]
wargs) <- IdrisParser (Name, FC, PTerm, [PTerm])
lhs
              forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \IState
ist -> IState
ist { lastParse :: Maybe Name
lastParse = forall a. a -> Maybe a
Just Name
n }
              (do (PTerm
rs, FC
fc) <- SyntaxInfo -> Name -> IdrisParser (PTerm, FC)
rhs SyntaxInfo
syn Name
n
                  let wsyn :: SyntaxInfo
wsyn = SyntaxInfo
syn { syn_namespace :: [String]
syn_namespace = [] }
                  ([PDecl]
wheres, [(Name, Name)]
nmap) <-     Name
-> SyntaxInfo
-> StateT
     IState (WriterT FC (Parsec Void String)) ([PDecl], [(Name, Name)])
whereBlock Name
n SyntaxInfo
wsyn forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* StateT IState (WriterT FC (Parsec Void String)) ()
popIndent
                                    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([], []) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT IState (WriterT FC (Parsec Void String)) ()
terminator
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
n PTerm
capp [PTerm]
wargs PTerm
rs [PDecl]
wheres) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do
                   StateT IState (WriterT FC (Parsec Void String)) ()
popIndent
                   ((PTerm
wval, Maybe (Name, FC)
pn), FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall a b. (a -> b) -> a -> b
$ do
                       forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"with"
                       PTerm
wval <- SyntaxInfo -> IdrisParser PTerm
bracketed SyntaxInfo
syn
                       Maybe (Name, FC)
pn <- StateT IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
optProof
                       forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
wval, Maybe (Name, FC)
pn)
                   StateT IState (WriterT FC (Parsec Void String)) ()
openBlock
                   [[PDecl]]
ds <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
some forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser [PDecl]
fnDecl SyntaxInfo
syn
                   StateT IState (WriterT FC (Parsec Void String)) ()
closeBlock
                   let withs :: [PDecl]
withs = forall a b. (a -> b) -> [a] -> [b]
map (Name -> PTerm -> [PTerm] -> PDecl -> PDecl
fillLHSD Name
n PTerm
capp [PTerm]
wargs) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PDecl]]
ds
                   forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t.
FC
-> Name
-> t
-> [t]
-> t
-> Maybe (Name, FC)
-> [PDecl' t]
-> PClause' t
PWith FC
fc Name
n PTerm
capp [PTerm]
wargs PTerm
wval Maybe (Name, FC)
pn [PDecl]
withs)
      forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"function clause"
  where
    lhsInfixApp :: IdrisParser (Name, FC, [PArg], [PTerm])
    lhsInfixApp :: IdrisParser (Name, FC, [PArg], [PTerm])
lhsInfixApp = do PTerm
l <- SyntaxInfo -> IdrisParser PTerm
argExpr SyntaxInfo
syn
                     (String
op, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). Parsing m => m String
symbolicOperator
                     forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
op forall a. Eq a => a -> a -> Bool
== String
"=" Bool -> Bool -> Bool
|| String
op forall a. Eq a => a -> a -> Bool
== String
"?=" ) forall a b. (a -> b) -> a -> b
$
                          forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"infix clause definition with \"=\" and \"?=\" not supported "
                     let n :: Name
n = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn (String -> Name
sUN String
op)
                     PTerm
r <- SyntaxInfo -> IdrisParser PTerm
argExpr SyntaxInfo
syn
                     [PTerm]
wargs <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (SyntaxInfo -> IdrisParser PTerm
wExpr SyntaxInfo
syn)
                     forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, FC
nfc, [forall {t}. t -> PArg' t
pexp PTerm
l, forall {t}. t -> PArg' t
pexp PTerm
r], [PTerm]
wargs)

    lhsPrefixApp :: IdrisParser (Name, FC, [PArg], [PTerm])
    lhsPrefixApp :: IdrisParser (Name, FC, [PArg], [PTerm])
lhsPrefixApp = do (Name
n, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName)
                      [PArg]
args <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PArg
implicitArg (SyntaxInfo
syn { inPattern :: Bool
inPattern = Bool
True } ))
                                    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PArg
constraintArg (SyntaxInfo
syn { inPattern :: Bool
inPattern = Bool
True }))
                                    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {t}. t -> PArg' t
pexp (SyntaxInfo -> IdrisParser PTerm
argExpr SyntaxInfo
syn)))
                      [PTerm]
wargs <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (SyntaxInfo -> IdrisParser PTerm
wExpr SyntaxInfo
syn)
                      forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, FC
nfc, [PArg]
args, [PTerm]
wargs)

    lhs :: IdrisParser (Name, FC, PTerm, [PTerm])
    lhs :: IdrisParser (Name, FC, PTerm, [PTerm])
lhs = do ((Name
n, FC
nfc, [PArg]
args, [PTerm]
wargs), FC
lhs_fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try IdrisParser (Name, FC, [PArg], [PTerm])
lhsInfixApp forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser (Name, FC, [PArg], [PTerm])
lhsPrefixApp)
             let capp :: PTerm
capp = FC -> PTerm -> [PArg] -> PTerm
PApp FC
lhs_fc (FC -> [FC] -> Name -> PTerm
PRef FC
nfc [FC
nfc] Name
n) [PArg]
args
             forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, FC
nfc, PTerm
capp, [PTerm]
wargs)

    optProof :: StateT IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
optProof = forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option forall a. Maybe a
Nothing (do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"proof"
                                    (Name, FC)
n <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                                    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (Name, FC)
n))

    fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
    fillLHS :: Name -> PTerm -> [PTerm] -> PClause' PTerm -> PClause' PTerm
fillLHS Name
n PTerm
capp [PTerm]
owargs (PClauseR FC
fc [PTerm]
wargs PTerm
v [PDecl]
ws)
       = forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
n PTerm
capp ([PTerm]
owargs forall a. [a] -> [a] -> [a]
++ [PTerm]
wargs) PTerm
v [PDecl]
ws
    fillLHS Name
n PTerm
capp [PTerm]
owargs (PWithR FC
fc [PTerm]
wargs PTerm
v Maybe (Name, FC)
pn [PDecl]
ws)
       = forall t.
FC
-> Name
-> t
-> [t]
-> t
-> Maybe (Name, FC)
-> [PDecl' t]
-> PClause' t
PWith FC
fc Name
n PTerm
capp ([PTerm]
owargs forall a. [a] -> [a] -> [a]
++ [PTerm]
wargs) PTerm
v Maybe (Name, FC)
pn
            (forall a b. (a -> b) -> [a] -> [b]
map (Name -> PTerm -> [PTerm] -> PDecl -> PDecl
fillLHSD Name
n PTerm
capp ([PTerm]
owargs forall a. [a] -> [a] -> [a]
++ [PTerm]
wargs)) [PDecl]
ws)
    fillLHS Name
_ PTerm
_ [PTerm]
_ PClause' PTerm
c = PClause' PTerm
c

    fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
    fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
fillLHSD Name
n PTerm
c [PTerm]
a (PClauses FC
fc FnOpts
o Name
fn [PClause' PTerm]
cs) = forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
o Name
fn (forall a b. (a -> b) -> [a] -> [b]
map (Name -> PTerm -> [PTerm] -> PClause' PTerm -> PClause' PTerm
fillLHS Name
n PTerm
c [PTerm]
a) [PClause' PTerm]
cs)
    fillLHSD Name
n PTerm
c [PTerm]
a PDecl
x = PDecl
x

{-| Parses with pattern

@
WExpr ::= '|' Expr';
@
-}
wExpr :: SyntaxInfo -> IdrisParser PTerm
wExpr :: SyntaxInfo -> IdrisParser PTerm
wExpr SyntaxInfo
syn = do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|'
               SyntaxInfo -> IdrisParser PTerm
expr' (SyntaxInfo
syn { inPattern :: Bool
inPattern = Bool
True })
            forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"with pattern"

{-| Parses a where block

@
WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
@
-}
whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
whereBlock :: Name
-> SyntaxInfo
-> StateT
     IState (WriterT FC (Parsec Void String)) ([PDecl], [(Name, Name)])
whereBlock Name
n SyntaxInfo
syn
    = do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"where"
         [[PDecl]]
ds <- forall a. IdrisParser a -> IdrisParser [a]
indentedBlock1 (SyntaxInfo -> IdrisParser [PDecl]
decl SyntaxInfo
syn)
         let dns :: [Name]
dns = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl -> [Name]
declared) [[PDecl]]
ds
         forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PDecl]]
ds, forall a b. (a -> b) -> [a] -> [b]
map (\Name
x -> (Name
x, SyntaxInfo -> Name -> Name
decoration SyntaxInfo
syn Name
x)) [Name]
dns)
      forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"where block"

{-|Parses a code generation target language name

@
Codegen ::= 'C'
        |   'Java'
        |   'JavaScript'
        |   'Node'
        |   'LLVM'
        |   'Bytecode'
        ;
@
-}
codegen_ :: IdrisParser Codegen
codegen_ :: IdrisParser Codegen
codegen_ = do String
n <- forall (m :: * -> *). Parsing m => m String
identifier
              forall (m :: * -> *) a. Monad m => a -> m a
return (IRFormat -> String -> Codegen
Via IRFormat
IBCFormat (forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
n))
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"Bytecode"; forall (m :: * -> *) a. Monad m => a -> m a
return Codegen
Bytecode
       forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"code generation language"

{-|Parses a compiler directive
@
StringList ::=
  String
  | String ',' StringList
  ;
@

@
Directive ::= '%' Directive';
@

@
Directive' ::= 'lib'            CodeGen String_t
           |   'link'           CodeGen String_t
           |   'flag'           CodeGen String_t
           |   'include'        CodeGen String_t
           |   'hide'           Name
           |   'freeze'         Name
           |   'thaw'           Name
           |   'access'         Accessibility
           |   'default'        Totality
           |   'logging'        Natural
           |   'dynamic'        StringList
           |   'name'           Name NameList
           |   'error_handlers' Name NameList
           |   'language'       'TypeProviders'
           |   'language'       'ErrorReflection'
           |   'deprecated' Name String
           |   'fragile'    Name Reason
           ;
@
-}
directive :: SyntaxInfo -> IdrisParser [PDecl]
directive :: SyntaxInfo -> IdrisParser [PDecl]
directive SyntaxInfo
syn = do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"lib")
                   Codegen
cgn <- IdrisParser Codegen
codegen_
                   String
lib <- forall (m :: * -> *). Parsing m => m String
stringLiteral
                   forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Codegen -> String -> Directive
DLib Codegen
cgn String
lib)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"link")
                    Codegen
cgn <- IdrisParser Codegen
codegen_; String
obj <- forall (m :: * -> *). Parsing m => m String
stringLiteral
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Codegen -> String -> Directive
DLink Codegen
cgn String
obj)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"flag")
                    Codegen
cgn <- IdrisParser Codegen
codegen_; String
flag <- forall (m :: * -> *). Parsing m => m String
stringLiteral
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Codegen -> String -> Directive
DFlag Codegen
cgn String
flag)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"include")
                    Codegen
cgn <- IdrisParser Codegen
codegen_
                    String
hdr <- forall (m :: * -> *). Parsing m => m String
stringLiteral
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Codegen -> String -> Directive
DInclude Codegen
cgn String
hdr)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"hide"); Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Name -> Directive
DHide Name
n)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"freeze"); Name
n <- forall (m :: * -> *). Parsing m => [String] -> m Name
iName []
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Name -> Directive
DFreeze Name
n)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"thaw"); Name
n <- forall (m :: * -> *). Parsing m => [String] -> m Name
iName []
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Name -> Directive
DThaw Name
n)]
             -- injectivity assertins are intended for debugging purposes
             -- only, and won't be documented/could be removed at any point
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"assert_injective"); Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Name -> Directive
DInjective Name
n)]
             -- Assert totality of something after definition. This is
             -- here as a debugging aid, so commented out...
--              <|> do P.try (lchar '%' *> reserved "assert_set_total"); n <- fst <$> fnName
--                     return [PDirective (DSetTotal n)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"access")
                    Accessibility
acc <- IdrisParser Accessibility
accessibility
                    IState
ist <- forall s (m :: * -> *). MonadState s m => m s
get
                    forall s (m :: * -> *). MonadState s m => s -> m ()
put IState
ist { default_access :: Accessibility
default_access = Accessibility
acc }
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Accessibility -> Directive
DAccess Accessibility
acc)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"default"); DefaultTotality
tot <- IdrisParser DefaultTotality
totality
                    IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
                    forall s (m :: * -> *). MonadState s m => s -> m ()
put (IState
i { default_total :: DefaultTotality
default_total = DefaultTotality
tot } )
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (DefaultTotality -> Directive
DDefault DefaultTotality
tot)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"logging")
                    Integer
i <- forall (m :: * -> *). Parsing m => m Integer
natural
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Integer -> Directive
DLogging Integer
i)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"dynamic")
                    [String]
libs <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 forall (m :: * -> *). Parsing m => m String
stringLiteral (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective ([String] -> Directive
DDynamicLibs [String]
libs)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"name")
                    (Name
ty, FC
tyFC) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                    [(Name, FC)]
ns <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Name -> FC -> [(Name, FC)] -> Directive
DNameHint Name
ty FC
tyFC [(Name, FC)]
ns)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"error_handlers")
                    (Name
fn, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                    (Name
arg, FC
afc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                    [(Name, FC)]
ns <- forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name) (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Name -> FC -> Name -> FC -> [(Name, FC)] -> Directive
DErrorHandlers Name
fn FC
nfc Name
arg FC
afc [(Name, FC)]
ns) ]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"language"); LanguageExt
ext <- IdrisParser LanguageExt
pLangExt;
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (LanguageExt -> Directive
DLanguage LanguageExt
ext)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"deprecate")
                    Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                    String
alt <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option String
"" forall (m :: * -> *). Parsing m => m String
stringLiteral
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Name -> String -> Directive
DDeprecate Name
n String
alt)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"fragile")
                    Name
n <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                    String
alt <- forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option String
"" forall (m :: * -> *). Parsing m => m String
stringLiteral
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Name -> String -> Directive
DFragile Name
n String
alt)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"used")
                    Name
fn <- forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                    Name
arg <- forall (m :: * -> *). Parsing m => [String] -> m Name
iName []
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (FC -> Name -> Name -> Directive
DUsed FC
fc Name
fn Name
arg)]
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"auto_implicits")
                    Bool
b <- StateT IState (WriterT FC (Parsec Void String)) Bool
on_off
                    forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. Directive -> PDecl' t
PDirective (Bool -> Directive
DAutoImplicits Bool
b)]
             forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"directive"
  where on_off :: StateT IState (WriterT FC (Parsec Void String)) Bool
on_off = do forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"on"; forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
             forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"off"; forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

pLangExt :: IdrisParser LanguageExt
pLangExt :: IdrisParser LanguageExt
pLangExt = (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"TypeProviders" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return LanguageExt
TypeProviders)
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"ErrorReflection" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return LanguageExt
ErrorReflection)
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"UniquenessTypes" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return LanguageExt
UniquenessTypes)
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"LinearTypes" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return LanguageExt
LinearTypes)
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"DSLNotation" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return LanguageExt
DSLNotation)
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"ElabReflection" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return LanguageExt
ElabReflection)
       forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"FirstClassReflection" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return LanguageExt
FCReflection)

{-| Parses a totality

@
Totality ::= 'partial' | 'total' | 'covering'
@

-}
totality :: IdrisParser DefaultTotality
totality :: IdrisParser DefaultTotality
totality
        = do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"total";   forall (m :: * -> *) a. Monad m => a -> m a
return DefaultTotality
DefaultCheckingTotal
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"partial"; forall (m :: * -> *) a. Monad m => a -> m a
return DefaultTotality
DefaultCheckingPartial
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"covering"; forall (m :: * -> *) a. Monad m => a -> m a
return DefaultTotality
DefaultCheckingCovering

{-| Parses a type provider

@
Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;
ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'
@
 -}
provider :: SyntaxInfo -> IdrisParser [PDecl]
provider :: SyntaxInfo -> IdrisParser [PDecl]
provider SyntaxInfo
syn = do Docstring (Either Err PTerm)
doc <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (Docstring (Either Err PTerm)
doc, [(Name, Docstring (Either Err PTerm))]
_) <- SyntaxInfo
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))])
docstring SyntaxInfo
syn
                                   forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"provide"
                                   forall (m :: * -> *) a. Monad m => a -> m a
return Docstring (Either Err PTerm)
doc)
                  Docstring (Either Err PTerm) -> IdrisParser [PDecl]
provideTerm Docstring (Either Err PTerm)
doc forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Docstring (Either Err PTerm) -> IdrisParser [PDecl]
providePostulate Docstring (Either Err PTerm)
doc
               forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"type provider"
  where provideTerm :: Docstring (Either Err PTerm) -> IdrisParser [PDecl]
provideTerm Docstring (Either Err PTerm)
doc =
          do forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'('; (Name
n, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName; forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
':'; PTerm
t <- SyntaxInfo -> IdrisParser PTerm
typeExpr SyntaxInfo
syn; forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'
             forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"with"
             (PTerm
e, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn) forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"provider expression"
             forall (m :: * -> *) a. Monad m => a -> m a
return  [forall t.
Docstring (Either Err t)
-> SyntaxInfo -> FC -> FC -> ProvideWhat' t -> Name -> PDecl' t
PProvider Docstring (Either Err PTerm)
doc SyntaxInfo
syn FC
fc FC
nfc (forall t. t -> t -> ProvideWhat' t
ProvTerm PTerm
t PTerm
e) Name
n]
        providePostulate :: Docstring (Either Err PTerm) -> IdrisParser [PDecl]
providePostulate Docstring (Either Err PTerm)
doc =
          do forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"postulate"
             (Name
n, FC
nfc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
             forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"with"
             (PTerm
e, FC
fc) <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn) forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"provider expression"
             forall (m :: * -> *) a. Monad m => a -> m a
return [forall t.
Docstring (Either Err t)
-> SyntaxInfo -> FC -> FC -> ProvideWhat' t -> Name -> PDecl' t
PProvider Docstring (Either Err PTerm)
doc SyntaxInfo
syn FC
fc FC
nfc (forall t. t -> ProvideWhat' t
ProvPostulate PTerm
e) Name
n]

{-| Parses a transform

@
Transform ::= '%' 'transform' Expr '==>' Expr
@
-}
transform :: SyntaxInfo -> IdrisParser [PDecl]
transform :: SyntaxInfo -> IdrisParser [PDecl]
transform SyntaxInfo
syn = do forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"transform")
                    -- leave it unchecked, until we work out what this should
                    -- actually mean...
--                     safety <- option True (do reserved "unsafe"
--                                               return False)
                   PTerm
l <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                   FC
fc <- forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => String -> m ()
symbol String
"==>"
                   PTerm
r <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                   forall (m :: * -> *) a. Monad m => a -> m a
return [forall t. FC -> Bool -> t -> t -> PDecl' t
PTransform FC
fc Bool
False PTerm
l PTerm
r]
                forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"transform"

{-| Parses a top-level reflected elaborator script

@
RunElabDecl ::= '%' 'runElab' Expr
@
-}
runElabDecl :: SyntaxInfo -> IdrisParser PDecl
runElabDecl :: SyntaxInfo -> IdrisParser PDecl
runElabDecl SyntaxInfo
syn =
  do FC
kwFC <- forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"runElab"))
     PTerm
script <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"elaborator script"
     forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall t. FC -> t -> [String] -> PDecl' t
PRunElabDecl FC
kwFC PTerm
script (SyntaxInfo -> [String]
syn_namespace SyntaxInfo
syn)
  forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"top-level elaborator script"

{- * Loading and parsing -}
{-| Parses an expression from input -}
parseExpr :: IState -> String -> Either ParseError PTerm
parseExpr :: IState -> String -> Either ParseError PTerm
parseExpr IState
st = forall st res.
Parser st res -> st -> String -> String -> Either ParseError res
runparser (SyntaxInfo -> IdrisParser PTerm
fullExpr SyntaxInfo
defaultSyntax) IState
st String
"(input)"

{-| Parses a constant form input -}
parseConst :: IState -> String -> Either ParseError Const
parseConst :: IState -> String -> Either ParseError Const
parseConst IState
st = forall st res.
Parser st res -> st -> String -> String -> Either ParseError res
runparser forall (m :: * -> *). Parsing m => m Const
constant IState
st String
"(input)"

{-| Parses a tactic from input -}
parseTactic :: IState -> String -> Either ParseError PTactic
parseTactic :: IState -> String -> Either ParseError PTactic
parseTactic IState
st = forall st res.
Parser st res -> st -> String -> String -> Either ParseError res
runparser (SyntaxInfo -> IdrisParser PTactic
fullTactic SyntaxInfo
defaultSyntax) IState
st String
"(input)"

{-| Parses a do-step from input (used in the elab shell) -}
parseElabShellStep :: IState -> String -> Either ParseError (Either ElabShellCmd PDo)
parseElabShellStep :: IState -> String -> Either ParseError (Either ElabShellCmd PDo)
parseElabShellStep IState
ist = forall st res.
Parser st res -> st -> String -> String -> Either ParseError res
runparser (forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SyntaxInfo -> IdrisParser PDo
do_ SyntaxInfo
defaultSyntax forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
elabShellCmd) IState
ist String
"(input)"
  where elabShellCmd :: StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
elabShellCmd = forall (m :: * -> *). Parsing m => Char -> m Char
char Char
':' forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                       (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"qed"     forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure ElabShellCmd
EQED       ) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"abandon" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure ElabShellCmd
EAbandon   ) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"undo"    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure ElabShellCmd
EUndo      ) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"state"   forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure ElabShellCmd
EProofState) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       (forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"term"    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure ElabShellCmd
EProofTerm ) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       (forall {b}.
[String]
-> (PTerm -> b)
-> StateT IState (WriterT FC (Parsec Void String)) b
expressionTactic [String
"e", String
"eval"] PTerm -> ElabShellCmd
EEval ) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       (forall {b}.
[String]
-> (PTerm -> b)
-> StateT IState (WriterT FC (Parsec Void String)) b
expressionTactic [String
"t", String
"type"] PTerm -> ElabShellCmd
ECheck) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       (forall {b}.
[String]
-> (PTerm -> b)
-> StateT IState (WriterT FC (Parsec Void String)) b
expressionTactic [String
"search"] PTerm -> ElabShellCmd
ESearch   ) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       (do forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"doc"
                           Either Name Const
doc <- (forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Parsing m => m Const
constant) forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName)
                           forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
                           forall (m :: * -> *) a. Monad m => a -> m a
return (Either Name Const -> ElabShellCmd
EDocStr Either Name Const
doc))
                       forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"elab command"
        expressionTactic :: [String]
-> (PTerm -> b)
-> StateT IState (WriterT FC (Parsec Void String)) b
expressionTactic [String]
cmds PTerm -> b
tactic =
           do forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
asum (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *). Parsing m => String -> m ()
reserved [String]
cmds)
              PTerm
t <- forall {f :: * -> *} {b}.
(MonadFail f, MonadParsec Void String f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced (SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
defaultSyntax)
              IState
i <- forall s (m :: * -> *). MonadState s m => m s
get
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ PTerm -> b
tactic (SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
defaultSyntax IState
i PTerm
t)
        spaced :: f b -> f b
spaced f b
parser = forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> f b
parser

-- | Parse module header and imports
parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark)
parseImports :: String
-> String
-> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark)
parseImports String
fname String
input
    = do IState
i <- Idris IState
getIState
         case forall st res.
Parser st res -> st -> String -> String -> Either ParseError res
runparser IdrisParser
  ((Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark),
   [(FC, OutputAnnotation)], IState)
imports IState
i String
fname String
input of
              Left ParseError
err -> forall w. Message w => w -> Idris OutputDoc
formatMessage ParseError
err forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. String -> Idris a
ifail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show
              Right ((Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark)
x, [(FC, OutputAnnotation)]
annots, IState
i) ->
                do IState -> Idris ()
putIState IState
i
                   String
fname' <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO String
Dir.makeAbsolute String
fname
                   Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ [(FC, OutputAnnotation)] -> String -> [(FC', OutputAnnotation)]
addPath [(FC, OutputAnnotation)]
annots String
fname'
                   forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark)
x
  where imports :: IdrisParser ((Maybe (Docstring ()), [String],
                                 [ImportInfo],
                                 Maybe Mark),
                                [(FC, OutputAnnotation)], IState)
        imports :: IdrisParser
  ((Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark),
   [(FC, OutputAnnotation)], IState)
imports = do forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional StateT IState (WriterT FC (Parsec Void String)) ()
shebang
                     forall (m :: * -> *). Parsing m => m ()
whiteSpace
                     (Maybe (Docstring ())
mdoc, [String]
mname, [(FC, OutputAnnotation)]
annots) <- IdrisParser
  (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
moduleHeader
                     [ImportInfo]
ps_exp        <- forall (f :: * -> *) a. Alternative f => f a -> f [a]
many IdrisParser ImportInfo
import_
                     Mark
mrk           <- forall (m :: * -> *). Parsing m => m Mark
mark
                     Bool
isEof         <- forall (m :: * -> *) a. Parsing m => m a -> m Bool
lookAheadMatches forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
                     let mrk' :: Maybe Mark
mrk' = if Bool
isEof
                                   then forall a. Maybe a
Nothing
                                   else forall a. a -> Maybe a
Just Mark
mrk
                     IState
i     <- forall s (m :: * -> *). MonadState s m => m s
get
                     -- add Builtins and Prelude, unless options say
                     -- not to
                     let ps :: [ImportInfo]
ps = [ImportInfo]
ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp
                     forall (m :: * -> *) a. Monad m => a -> m a
return ((Maybe (Docstring ())
mdoc, [String]
mname, [ImportInfo]
ps, Maybe Mark
mrk'), [(FC, OutputAnnotation)]
annots, IState
i)

        addPath :: [(FC, OutputAnnotation)] -> FilePath -> [(FC', OutputAnnotation)]
        addPath :: [(FC, OutputAnnotation)] -> String -> [(FC', OutputAnnotation)]
addPath [] String
_ = []
        addPath ((FC
fc, AnnNamespace [Text]
ns Maybe String
Nothing) : [(FC, OutputAnnotation)]
annots) String
path =
           (FC -> FC'
FC' FC
fc, [Text] -> Maybe String -> OutputAnnotation
AnnNamespace [Text]
ns (forall a. a -> Maybe a
Just String
path)) forall a. a -> [a] -> [a]
: [(FC, OutputAnnotation)] -> String -> [(FC', OutputAnnotation)]
addPath [(FC, OutputAnnotation)]
annots String
path
        addPath ((FC
fc,OutputAnnotation
annot):[(FC, OutputAnnotation)]
annots) String
path = (FC -> FC'
FC' FC
fc, OutputAnnotation
annot) forall a. a -> [a] -> [a]
: [(FC, OutputAnnotation)] -> String -> [(FC', OutputAnnotation)]
addPath [(FC, OutputAnnotation)]
annots String
path

        shebang :: IdrisParser ()
        shebang :: StateT IState (WriterT FC (Parsec Void String)) ()
shebang = forall (m :: * -> *). Parsing m => String -> m String
string String
"#!" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isEol) forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *). Parsing m => m ()
eol forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Check if the coloring matches the options and corrects if necessary
fixColour :: Bool -> PP.Doc -> PP.Doc
fixColour :: Bool -> Doc -> Doc
fixColour Bool
False Doc
doc = Doc -> Doc
PP.plain Doc
doc
fixColour Bool
True Doc
doc  = Doc
doc

-- | A program is a list of declarations, possibly with associated
-- documentation strings.
parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Mark -> Idris [PDecl]
parseProg :: SyntaxInfo -> String -> String -> Maybe Mark -> Idris [PDecl]
parseProg SyntaxInfo
syn String
fname String
input Maybe Mark
mrk
    = do IState
i <- Idris IState
getIState
         case forall st res.
Parser st res -> st -> String -> String -> Either ParseError res
runparser IdrisParser ([PDecl], IState)
mainProg IState
i String
fname String
input of
            Left ParseError
err -> do forall w. Message w => w -> Idris ()
emitWarning ParseError
err
                           IState
i <- Idris IState
getIState
                           IState -> Idris ()
putIState (IState
i { errSpan :: Maybe FC
errSpan = forall a. a -> Maybe a
Just (forall a. Message a => a -> FC
messageExtent ParseError
err) })
                           forall (m :: * -> *) a. Monad m => a -> m a
return []
            Right ([PDecl]
x, IState
i)  -> do IState -> Idris ()
putIState IState
i
                                Idris ()
reportParserWarnings
                                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [PDecl] -> [PDecl]
collect [PDecl]
x
  where mainProg :: IdrisParser ([PDecl], IState)
        mainProg :: IdrisParser ([PDecl], IState)
mainProg = case Maybe Mark
mrk of
                        Maybe Mark
Nothing -> do IState
i <- forall s (m :: * -> *). MonadState s m => m s
get; forall (m :: * -> *) a. Monad m => a -> m a
return ([], IState
i)
                        Just Mark
mrk -> do
                          forall (m :: * -> *). Parsing m => Mark -> m ()
restore Mark
mrk
                          [PDecl]
ds <- SyntaxInfo -> IdrisParser [PDecl]
prog SyntaxInfo
syn
                          IState
i' <- forall s (m :: * -> *). MonadState s m => m s
get
                          forall (m :: * -> *) a. Monad m => a -> m a
return ([PDecl]
ds, IState
i')

-- | Collect 'PClauses' with the same function name
collect :: [PDecl] -> [PDecl]
collect :: [PDecl] -> [PDecl]
collect (c :: PDecl
c@(PClauses FC
_ FnOpts
o Name
_ [PClause' PTerm]
_) : [PDecl]
ds)
    = Maybe Name -> [PClause' PTerm] -> [PDecl] -> [PDecl]
clauses (PDecl -> Maybe Name
cname PDecl
c) [] (PDecl
c forall a. a -> [a] -> [a]
: [PDecl]
ds)
  where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]
        clauses :: Maybe Name -> [PClause' PTerm] -> [PDecl] -> [PDecl]
clauses j :: Maybe Name
j@(Just Name
n) [PClause' PTerm]
acc (PClauses FC
fc FnOpts
_ Name
_ [PClause FC
fc' Name
n' PTerm
l [PTerm]
ws PTerm
r [PDecl]
w] : [PDecl]
ds)
           | Name
n forall a. Eq a => a -> a -> Bool
== Name
n' = Maybe Name -> [PClause' PTerm] -> [PDecl] -> [PDecl]
clauses Maybe Name
j (forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc' Name
n' PTerm
l [PTerm]
ws PTerm
r ([PDecl] -> [PDecl]
collect [PDecl]
w) forall a. a -> [a] -> [a]
: [PClause' PTerm]
acc) [PDecl]
ds
        clauses j :: Maybe Name
j@(Just Name
n) [PClause' PTerm]
acc (PClauses FC
fc FnOpts
_ Name
_ [PWith FC
fc' Name
n' PTerm
l [PTerm]
ws PTerm
r Maybe (Name, FC)
pn [PDecl]
w] : [PDecl]
ds)
           | Name
n forall a. Eq a => a -> a -> Bool
== Name
n' = Maybe Name -> [PClause' PTerm] -> [PDecl] -> [PDecl]
clauses Maybe Name
j (forall t.
FC
-> Name
-> t
-> [t]
-> t
-> Maybe (Name, FC)
-> [PDecl' t]
-> PClause' t
PWith FC
fc' Name
n' PTerm
l [PTerm]
ws PTerm
r Maybe (Name, FC)
pn ([PDecl] -> [PDecl]
collect [PDecl]
w) forall a. a -> [a] -> [a]
: [PClause' PTerm]
acc) [PDecl]
ds
        clauses (Just Name
n) [PClause' PTerm]
acc [PDecl]
xs = forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses (PDecl -> FC
fcOf PDecl
c) FnOpts
o Name
n (forall a. [a] -> [a]
reverse [PClause' PTerm]
acc) forall a. a -> [a] -> [a]
: [PDecl] -> [PDecl]
collect [PDecl]
xs
        clauses Maybe Name
Nothing [PClause' PTerm]
acc (PDecl
x:[PDecl]
xs) = [PDecl] -> [PDecl]
collect [PDecl]
xs
        clauses Maybe Name
Nothing [PClause' PTerm]
acc [] = []

        cname :: PDecl -> Maybe Name
        cname :: PDecl -> Maybe Name
cname (PClauses FC
fc FnOpts
_ Name
_ [PClause FC
_ Name
n PTerm
_ [PTerm]
_ PTerm
_ [PDecl]
_]) = forall a. a -> Maybe a
Just Name
n
        cname (PClauses FC
fc FnOpts
_ Name
_ [PWith   FC
_ Name
n PTerm
_ [PTerm]
_ PTerm
_ Maybe (Name, FC)
_ [PDecl]
_]) = forall a. a -> Maybe a
Just Name
n
        cname (PClauses FC
fc FnOpts
_ Name
_ [PClauseR FC
_ [PTerm]
_ PTerm
_ [PDecl]
_]) = forall a. Maybe a
Nothing
        cname (PClauses FC
fc FnOpts
_ Name
_ [PWithR FC
_ [PTerm]
_ PTerm
_ Maybe (Name, FC)
_ [PDecl]
_]) = forall a. Maybe a
Nothing
        fcOf :: PDecl -> FC
        fcOf :: PDecl -> FC
fcOf (PClauses FC
fc FnOpts
_ Name
_ [PClause' PTerm]
_) = FC
fc
collect (PParams FC
f [(Name, PTerm)]
ns [PDecl]
ps : [PDecl]
ds) = forall t. FC -> [(Name, t)] -> [PDecl' t] -> PDecl' t
PParams FC
f [(Name, PTerm)]
ns ([PDecl] -> [PDecl]
collect [PDecl]
ps) forall a. a -> [a] -> [a]
: [PDecl] -> [PDecl]
collect [PDecl]
ds
collect (POpenInterfaces FC
f [Name]
ns [PDecl]
ps : [PDecl]
ds) = forall t. FC -> [Name] -> [PDecl' t] -> PDecl' t
POpenInterfaces FC
f [Name]
ns ([PDecl] -> [PDecl]
collect [PDecl]
ps) forall a. a -> [a] -> [a]
: [PDecl] -> [PDecl]
collect [PDecl]
ds
collect (PMutual FC
f [PDecl]
ms : [PDecl]
ds) = forall t. FC -> [PDecl' t] -> PDecl' t
PMutual FC
f ([PDecl] -> [PDecl]
collect [PDecl]
ms) forall a. a -> [a] -> [a]
: [PDecl] -> [PDecl]
collect [PDecl]
ds
collect (PNamespace String
ns FC
fc [PDecl]
ps : [PDecl]
ds) = forall t. String -> FC -> [PDecl' t] -> PDecl' t
PNamespace String
ns FC
fc ([PDecl] -> [PDecl]
collect [PDecl]
ps) forall a. a -> [a] -> [a]
: [PDecl] -> [PDecl]
collect [PDecl]
ds
collect (PInterface Docstring (Either Err PTerm)
doc SyntaxInfo
f FC
s [(Name, PTerm)]
cs Name
n FC
nfc [(Name, FC, PTerm)]
ps [(Name, Docstring (Either Err PTerm))]
pdocs [(Name, FC)]
fds [PDecl]
ds Maybe (Name, FC)
cn Docstring (Either Err PTerm)
cd : [PDecl]
ds')
    = forall t.
Docstring (Either Err t)
-> SyntaxInfo
-> FC
-> [(Name, t)]
-> Name
-> FC
-> [(Name, FC, t)]
-> [(Name, Docstring (Either Err t))]
-> [(Name, FC)]
-> [PDecl' t]
-> Maybe (Name, FC)
-> Docstring (Either Err t)
-> PDecl' t
PInterface Docstring (Either Err PTerm)
doc SyntaxInfo
f FC
s [(Name, PTerm)]
cs Name
n FC
nfc [(Name, FC, PTerm)]
ps [(Name, Docstring (Either Err PTerm))]
pdocs [(Name, FC)]
fds ([PDecl] -> [PDecl]
collect [PDecl]
ds) Maybe (Name, FC)
cn Docstring (Either Err PTerm)
cd forall a. a -> [a] -> [a]
: [PDecl] -> [PDecl]
collect [PDecl]
ds'
collect (PImplementation Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
f FC
s [(Name, PTerm)]
cs [Name]
pnames Accessibility
acc FnOpts
opts Name
n FC
nfc [PTerm]
ps [(Name, PTerm)]
pextra PTerm
t Maybe Name
en [PDecl]
ds : [PDecl]
ds')
    = forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> [(Name, t)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [t]
-> [(Name, t)]
-> t
-> Maybe Name
-> [PDecl' t]
-> PDecl' t
PImplementation Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
f FC
s [(Name, PTerm)]
cs [Name]
pnames Accessibility
acc FnOpts
opts Name
n FC
nfc [PTerm]
ps [(Name, PTerm)]
pextra PTerm
t Maybe Name
en ([PDecl] -> [PDecl]
collect [PDecl]
ds) forall a. a -> [a] -> [a]
: [PDecl] -> [PDecl]
collect [PDecl]
ds'
collect (PDecl
d : [PDecl]
ds) = PDecl
d forall a. a -> [a] -> [a]
: [PDecl] -> [PDecl]
collect [PDecl]
ds
collect [] = []

{-| Load idris module and show error if something wrong happens -}
loadModule :: FilePath -> IBCPhase -> Idris (Maybe String)
loadModule :: String -> IBCPhase -> Idris (Maybe String)
loadModule String
f IBCPhase
phase
   = forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (String -> IBCPhase -> Idris (Maybe String)
loadModule' String
f IBCPhase
phase)
                (\Err
e -> do FC -> Idris ()
setErrSpan (Err -> FC
getErrSpan Err
e)
                          IState
ist <- Idris IState
getIState
                          FC -> OutputDoc -> Idris ()
iWarn (Err -> FC
getErrSpan Err
e) forall a b. (a -> b) -> a -> b
$ IState -> Err -> OutputDoc
pprintErr IState
ist Err
e
                          forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)

{-| Load idris module -}
loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)
loadModule' :: String -> IBCPhase -> Idris (Maybe String)
loadModule' String
f IBCPhase
phase
   = do IState
i <- Idris IState
getIState
        let file :: String
file = forall a. (a -> Bool) -> [a] -> [a]
takeWhile (forall a. Eq a => a -> a -> Bool
/= Char
' ') String
f
        String
ibcsd <- IState -> Idris String
valIBCSubDir IState
i
        [String]
ids <- String -> Idris [String]
rankedImportDirs String
file
        IFileType
fp <- [String] -> String -> String -> Idris IFileType
findImport [String]
ids String
ibcsd String
file
        if String
file forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` IState -> [String]
imported IState
i
          then do Int -> String -> Idris ()
logParser Int
1 forall a b. (a -> b) -> a -> b
$ String
"Already read " forall a. [a] -> [a] -> [a]
++ String
file
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
          else do IState -> Idris ()
putIState (IState
i { imported :: [String]
imported = String
file forall a. a -> [a] -> [a]
: IState -> [String]
imported IState
i })
                  case IFileType
fp of
                    IDR String
fn  -> Bool -> String -> Maybe Int -> Idris ()
loadSource Bool
False String
fn forall a. Maybe a
Nothing
                    LIDR String
fn -> Bool -> String -> Maybe Int -> Idris ()
loadSource Bool
True  String
fn forall a. Maybe a
Nothing
                    IBC String
fn IFileType
src ->
                      forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (Bool -> IBCPhase -> String -> Idris ()
loadIBC Bool
True IBCPhase
phase String
fn)
                                 (\Err
c -> do Int -> String -> Idris ()
logParser Int
1 forall a b. (a -> b) -> a -> b
$ String
fn forall a. [a] -> [a] -> [a]
++ String
" failed " forall a. [a] -> [a] -> [a]
++ IState -> Err -> String
pshow IState
i Err
c
                                           case IFileType
src of
                                             IDR String
sfn -> Bool -> String -> Maybe Int -> Idris ()
loadSource Bool
False String
sfn forall a. Maybe a
Nothing
                                             LIDR String
sfn -> Bool -> String -> Maybe Int -> Idris ()
loadSource Bool
True String
sfn forall a. Maybe a
Nothing)
                  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just String
file

{-| Load idris code from file -}
loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()
loadFromIFile :: Bool -> IBCPhase -> IFileType -> Maybe Int -> Idris ()
loadFromIFile Bool
reexp IBCPhase
phase i :: IFileType
i@(IBC String
fn IFileType
src) Maybe Int
maxline
   = do Int -> String -> Idris ()
logParser Int
1 forall a b. (a -> b) -> a -> b
$ String
"Skipping " forall a. [a] -> [a] -> [a]
++ IFileType -> String
getSrcFile IFileType
i
        Int -> String -> Idris ()
logParser Int
3 forall a b. (a -> b) -> a -> b
$ String
"loadFromIFile i" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show IFileType
i
        forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (Bool -> IBCPhase -> String -> Idris ()
loadIBC Bool
reexp IBCPhase
phase String
fn)
                (\Err
err -> forall a. Err -> Idris a
ierror forall a b. (a -> b) -> a -> b
$ forall t. String -> Err' t -> Err' t
LoadingFailed String
fn Err
err)
  where
    getSrcFile :: IFileType -> String
getSrcFile (IDR String
fn) = String
fn
    getSrcFile (LIDR String
fn) = String
fn
    getSrcFile (IBC String
f IFileType
src) = IFileType -> String
getSrcFile IFileType
src

loadFromIFile Bool
_ IBCPhase
_ (IDR String
fn) Maybe Int
maxline = Bool -> String -> Maybe Int -> Idris ()
loadSource' Bool
False String
fn Maybe Int
maxline
loadFromIFile Bool
_ IBCPhase
_ (LIDR String
fn) Maybe Int
maxline = Bool -> String -> Maybe Int -> Idris ()
loadSource' Bool
True String
fn Maybe Int
maxline

{-| Load idris source code and show error if something wrong happens -}
loadSource' :: Bool -> FilePath -> Maybe Int -> Idris ()
loadSource' :: Bool -> String -> Maybe Int -> Idris ()
loadSource' Bool
lidr String
r Maybe Int
maxline
   = forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (Bool -> String -> Maybe Int -> Idris ()
loadSource Bool
lidr String
r Maybe Int
maxline)
                (\Err
e -> do FC -> Idris ()
setErrSpan (Err -> FC
getErrSpan Err
e)
                          IState
ist <- Idris IState
getIState
                          case Err
e of
                            At FC
f Err
e' -> FC -> OutputDoc -> Idris ()
iWarn FC
f (IState -> Err -> OutputDoc
pprintErr IState
ist Err
e')
                            Err
_ -> FC -> OutputDoc -> Idris ()
iWarn (Err -> FC
getErrSpan Err
e) (IState -> Err -> OutputDoc
pprintErr IState
ist Err
e))

{-| Load Idris source code-}
loadSource :: Bool -> FilePath -> Maybe Int -> Idris ()
loadSource :: Bool -> String -> Maybe Int -> Idris ()
loadSource Bool
lidr String
f Maybe Int
toline
     = do Int -> String -> Idris ()
logParser Int
1 (String
"Reading " forall a. [a] -> [a] -> [a]
++ String
f)
          Int -> String -> Idris ()
iReport   Int
2 (String
"Reading " forall a. [a] -> [a] -> [a]
++ String
f)
          IState
i <- Idris IState
getIState
          let def_total :: DefaultTotality
def_total = IState -> DefaultTotality
default_total IState
i
          String
file_in <- forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO String
readSource String
f
          String
file <- if Bool
lidr then forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ String -> String -> TC String
unlit String
f String
file_in else forall (m :: * -> *) a. Monad m => a -> m a
return String
file_in
          (Maybe (Docstring ())
mdocs, [String]
mname, [ImportInfo]
imports_in, Maybe Mark
pos) <- String
-> String
-> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark)
parseImports String
f String
file
          [String]
ai <- Idris [String]
getAutoImports
          let imports :: [ImportInfo]
imports = forall a b. (a -> b) -> [a] -> [b]
map (\String
n -> Bool
-> String -> Maybe (String, FC) -> [Text] -> FC -> FC -> ImportInfo
ImportInfo Bool
True String
n forall a. Maybe a
Nothing [] FC
NoFC FC
NoFC) [String]
ai forall a. [a] -> [a] -> [a]
++ [ImportInfo]
imports_in
          [String]
ids <- String -> Idris [String]
rankedImportDirs String
f
          String
ibcsd <- IState -> Idris String
valIBCSubDir IState
i
          let ibc :: String
ibc = String -> String -> String
ibcPathNoFallback String
ibcsd String
f
          [(String, Int)]
impHashes <- forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (String -> Idris [(String, Int)]
getImportHashes String
ibc)
                                  (\Err
err -> forall (m :: * -> *) a. Monad m => a -> m a
return [])
          [Maybe (String, Int)]
newHashes <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (Bool
_, String
f, [Text]
_, FC
_) ->
                         do IFileType
fp <- [String] -> String -> String -> Idris IFileType
findImport [String]
ids String
ibcsd String
f
                            case IFileType
fp of
                                 IBC String
fn IFileType
src ->
                                   forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do Int
hash <- String -> Idris Int
getIBCHash String
fn
                                                  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (String
fn, Int
hash)))
                                              (\Err
err -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)
                                 IFileType
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)
                [(Bool
re, String
fn, [Text]
ns, FC
nfc) | ImportInfo Bool
re String
fn Maybe (String, FC)
_ [Text]
ns FC
_ FC
nfc <- [ImportInfo]
imports]

          UTCTime
fmod <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO UTCTime
Dir.getModificationTime String
f
          Bool
ibcexists <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO Bool
Dir.doesFileExist String
ibc
          UTCTime
ibcmod <- if Bool
ibcexists
                       then forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO UTCTime
Dir.getModificationTime String
ibc
                       else forall (m :: * -> *) a. Monad m => a -> m a
return UTCTime
fmod

          Int -> String -> Idris ()
logParser Int
10 forall a b. (a -> b) -> a -> b
$ String
ibc forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show UTCTime
ibcmod
          Int -> String -> Idris ()
logParser Int
10 forall a b. (a -> b) -> a -> b
$ String
f forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show UTCTime
fmod
          Int -> String -> Idris ()
logParser Int
10 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show [(String, Int)]
impHashes forall a. [a] -> [a] -> [a]
++ String
"\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Maybe (String, Int)]
newHashes

          -- If the ibc is newer than the source, and the old import
          -- hashes are the same as the ones we've just read,
          -- quit and just load the IBC

          let needLoad :: Bool
needLoad = (UTCTime
ibcmod forall a. Ord a => a -> a -> Bool
<= UTCTime
fmod) Bool -> Bool -> Bool
||
                         (forall a. Ord a => [a] -> [a]
sort [(String, Int)]
impHashes forall a. Eq a => a -> a -> Bool
/= forall a. Ord a => [a] -> [a]
sort (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall a. a -> a
id [Maybe (String, Int)]
newHashes))

          if Bool -> Bool
not Bool
needLoad
             then forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
             else do
              Int -> String -> Idris ()
iReport Int
1 forall a b. (a -> b) -> a -> b
$ String
"Type checking " forall a. [a] -> [a] -> [a]
++ String
f
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (Bool
re, String
f, [Text]
ns, FC
nfc) ->
                           do IFileType
fp <- [String] -> String -> String -> Idris IFileType
findImport [String]
ids String
ibcsd String
f
                              case IFileType
fp of
                                  LIDR String
fn -> forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ String
"No ibc for " forall a. [a] -> [a] -> [a]
++ String
f
                                  IDR String
fn -> forall a. String -> Idris a
ifail forall a b. (a -> b) -> a -> b
$ String
"No ibc for " forall a. [a] -> [a] -> [a]
++ String
f
                                  IBC String
fn IFileType
src ->
                                    do Bool -> IBCPhase -> String -> Idris ()
loadIBC Bool
True IBCPhase
IBC_Building String
fn
                                       let srcFn :: Maybe String
srcFn = case IFileType
src of
                                                     IDR String
fn -> forall a. a -> Maybe a
Just String
fn
                                                     LIDR String
fn -> forall a. a -> Maybe a
Just String
fn
                                                     IFileType
_ -> forall a. Maybe a
Nothing
                                       Maybe String
srcFnAbs <- case Maybe String
srcFn of
                                                     Just String
fn -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just (forall a. IO a -> Idris a
runIO forall a b. (a -> b) -> a -> b
$ String -> IO String
Dir.makeAbsolute String
fn)
                                                     Maybe String
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
                                       Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
S.fromList [(FC -> FC'
FC' FC
nfc, [Text] -> Maybe String -> OutputAnnotation
AnnNamespace [Text]
ns Maybe String
srcFnAbs)])
                    [(Bool
re, String
fn, [Text]
ns, FC
nfc) | ImportInfo Bool
re String
fn Maybe (String, FC)
_ [Text]
ns FC
_ FC
nfc <- [ImportInfo]
imports]
              Idris ()
reportParserWarnings
              Idris ()
sendParserHighlighting

              -- process and check module aliases
              let modAliases :: Map [Text] [Text]
modAliases = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
                    [ (String -> [Text]
prep String
alias, String -> [Text]
prep String
realName)
                    | ImportInfo { import_reexport :: ImportInfo -> Bool
import_reexport = Bool
reexport
                                 , import_path :: ImportInfo -> String
import_path = String
realName
                                 , import_rename :: ImportInfo -> Maybe (String, FC)
import_rename = Just (String
alias, FC
_)
                                 , import_location :: ImportInfo -> FC
import_location = FC
fc } <- [ImportInfo]
imports
                    ]
                  prep :: String -> [Text]
prep = forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [a] -> [a] -> [[a]]
Spl.splitOn [Char
pathSeparator]
                  aliasNames :: [(String, FC)]
aliasNames = [ (String
alias, FC
fc)
                               | ImportInfo { import_rename :: ImportInfo -> Maybe (String, FC)
import_rename = Just (String
alias, FC
fc)
                                            } <- [ImportInfo]
imports
                               ]
                  histogram :: [[(String, FC)]]
histogram = forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ [(String, FC)]
aliasNames
              case forall a b. (a -> b) -> [a] -> [b]
map forall a. [a] -> a
head forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
/= Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length) forall a b. (a -> b) -> a -> b
$ [[(String, FC)]]
histogram of
                []       -> Int -> String -> Idris ()
logParser Int
3 forall a b. (a -> b) -> a -> b
$ String
"Module aliases: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall k a. Map k a -> [(k, a)]
M.toList Map [Text] [Text]
modAliases)
                (String
n,FC
fc):[(String, FC)]
_ -> forall a. Err -> Idris a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. FC -> Err' t -> Err' t
At FC
fc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ String
"import alias not unique: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
n

              IState
i <- Idris IState
getIState
              IState -> Idris ()
putIState (IState
i { default_access :: Accessibility
default_access = Accessibility
Private, module_aliases :: Map [Text] [Text]
module_aliases = Map [Text] [Text]
modAliases })
              Idris ()
clearIBC -- start a new .ibc file
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ IBCWrite -> Idris ()
addIBC (forall a b. (a -> b) -> [a] -> [b]
map (\ (String
f, Int
h) -> String -> Int -> IBCWrite
IBCImportHash String
f Int
h)
                                (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall a. a -> a
id [Maybe (String, Int)]
newHashes))
              -- record package info in .ibc
              [String]
imps <- Idris [String]
allImportDirs
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ IBCWrite -> Idris ()
addIBC (forall a b. (a -> b) -> [a] -> [b]
map String -> IBCWrite
IBCImportDir [String]
imps)
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IBCWrite -> Idris ()
addIBC forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, String) -> IBCWrite
IBCImport)
                [ (Bool
reexport, String
realName)
                | ImportInfo { import_reexport :: ImportInfo -> Bool
import_reexport = Bool
reexport
                             , import_path :: ImportInfo -> String
import_path = String
realName
                             } <- [ImportInfo]
imports
                ]
              let syntax :: SyntaxInfo
syntax = SyntaxInfo
defaultSyntax{ syn_namespace :: [String]
syn_namespace = forall a. [a] -> [a]
reverse [String]
mname,
                                          maxline :: Maybe Int
maxline = Maybe Int
toline }
              IState
ist <- Idris IState
getIState
              -- Save the span from parsing the module header, because
              -- an empty program parse might obliterate it.
              let oldSpan :: Maybe FC
oldSpan = IState -> Maybe FC
idris_parsedSpan IState
ist
              [PDecl]
ds' <- SyntaxInfo -> String -> String -> Maybe Mark -> Idris [PDecl]
parseProg SyntaxInfo
syntax String
f String
file Maybe Mark
pos

              case ([PDecl]
ds', Maybe FC
oldSpan) of
                ([], Just FC
fc) ->
                  -- If no program elements were parsed, we dind't
                  -- get a loaded region in the IBC file. That
                  -- means we need to add it back.
                  do IState
ist <- Idris IState
getIState
                     IState -> Idris ()
putIState IState
ist { idris_parsedSpan :: Maybe FC
idris_parsedSpan = Maybe FC
oldSpan
                                   , ibc_write :: [IBCWrite]
ibc_write = FC -> IBCWrite
IBCParsedRegion FC
fc forall a. a -> [a] -> [a]
:
                                                 IState -> [IBCWrite]
ibc_write IState
ist
                                   }
                ([PDecl], Maybe FC)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Idris ()
sendParserHighlighting

              -- Parsing done, now process declarations

              let ds :: [PDecl]
ds = [String] -> [PDecl] -> [PDecl]
namespaces [String]
mname [PDecl]
ds'
              Int -> String -> Idris ()
logParser Int
3 (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ PPOption -> [PDecl] -> OutputDoc
showDecls PPOption
verbosePPOption [PDecl]
ds)
              IState
i <- Idris IState
getIState
              Int -> String -> Idris ()
logLvl Int
10 (forall a. Show a => a -> String
show (forall a. Ctxt a -> [(Name, a)]
toAlist (IState -> Ctxt [PArg]
idris_implicits IState
i)))
              Int -> String -> Idris ()
logLvl Int
3 (forall a. Show a => a -> String
show (IState -> [FixDecl]
idris_infixes IState
i))
              -- Now add all the declarations to the context
              -- we totality check after every Mutual block, so if
              -- anything is a single definition, wrap it in a
              -- mutual block on its own
              ElabInfo -> [PDecl] -> Idris ()
elabDecls (String -> ElabInfo
toplevelWith String
f) (forall a b. (a -> b) -> [a] -> [b]
map PDecl -> PDecl
toMutual [PDecl]
ds)
              IState
i <- Idris IState
getIState
              -- simplify every definition do give the totality checker
              -- a better chance
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Name
n -> do Int -> String -> Idris ()
logLvl Int
5 forall a b. (a -> b) -> a -> b
$ String
"Simplifying " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n
                              Context
ctxt' <-
                                do Context
ctxt <- StateT IState (ExceptT Err IO) Context
getContext
                                   forall a. TC a -> Idris a
tclift forall a b. (a -> b) -> a -> b
$ Name -> [Name] -> [[Name]] -> ErasureInfo -> Context -> TC Context
simplifyCasedef Name
n [] [] (IState -> ErasureInfo
getErasureInfo IState
i) Context
ctxt
                              Context -> Idris ()
setContext Context
ctxt')
                       (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd (IState -> [(FC, Name)]
idris_totcheck IState
i))
              -- build size change graph from simplified definitions
              Int -> String -> Idris ()
iReport Int
3 forall a b. (a -> b) -> a -> b
$ String
"Totality checking " forall a. [a] -> [a] -> [a]
++ String
f
              Int -> String -> Idris ()
logLvl Int
1 forall a b. (a -> b) -> a -> b
$ String
"Totality checking " forall a. [a] -> [a] -> [a]
++ String
f
              IState
i <- Idris IState
getIState
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris ()
buildSCG (IState -> [(FC, Name)]
idris_totcheck IState
i)
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris Totality
checkDeclTotality (IState -> [(FC, Name)]
idris_totcheck IState
i)
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris ()
verifyTotality (IState -> [(FC, Name)]
idris_totcheck IState
i)

              -- Redo totality check for deferred names
              let deftots :: [(FC, Name)]
deftots = IState -> [(FC, Name)]
idris_defertotcheck IState
i
              Int -> String -> Idris ()
logLvl Int
2 forall a b. (a -> b) -> a -> b
$ String
"Totality checking " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(FC, Name)]
deftots
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Name
x -> do Totality
tot <- Name -> Idris Totality
getTotality Name
x
                              case Totality
tot of
                                   Total [Int]
_ ->
                                     do let opts :: FnOpts
opts = case forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
x (IState -> Ctxt FnOpts
idris_flags IState
i) of
                                                      Just FnOpts
os -> FnOpts
os
                                                      Maybe FnOpts
Nothing -> []
                                        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FnOpt
AssertTotal forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` FnOpts
opts) forall a b. (a -> b) -> a -> b
$
                                            Name -> Totality -> Idris ()
setTotality Name
x Totality
Unchecked
                                   Totality
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(FC, Name)]
deftots)
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris ()
buildSCG [(FC, Name)]
deftots
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris Totality
checkDeclTotality [(FC, Name)]
deftots

              Int -> String -> Idris ()
logLvl Int
1 (String
"Finished " forall a. [a] -> [a] -> [a]
++ String
f)
              String
ibcsd <- IState -> Idris String
valIBCSubDir IState
i
              Int -> String -> Idris ()
logLvl  Int
1 forall a b. (a -> b) -> a -> b
$ String
"Universe checking " forall a. [a] -> [a] -> [a]
++ String
f
              Int -> String -> Idris ()
iReport Int
3 forall a b. (a -> b) -> a -> b
$ String
"Universe checking " forall a. [a] -> [a] -> [a]
++ String
f
              Idris ()
iucheck
              IState
i <- Idris IState
getIState
              Ctxt Accessibility -> Idris ()
addHides (IState -> Ctxt Accessibility
hide_list IState
i)

              -- Save module documentation if applicable
              IState
i <- Idris IState
getIState
              case Maybe (Docstring ())
mdocs of
                Maybe (Docstring ())
Nothing   -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
                Just Docstring ()
docs -> SyntaxInfo -> [String] -> Docstring () -> Idris ()
addModDoc SyntaxInfo
syntax [String]
mname Docstring ()
docs


              -- Finally, write an ibc and highlights if checking was successful
              Bool
ok <- StateT IState (ExceptT Err IO) Bool
noErrors
              forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
ok forall a b. (a -> b) -> a -> b
$
                do forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do String -> String -> Idris ()
writeIBC String
f String
ibc; Idris ()
clearIBC)
                              (\Err
c -> forall (m :: * -> *) a. Monad m => a -> m a
return ()) -- failure is harmless
                   Bool
hl <- StateT IState (ExceptT Err IO) Bool
getDumpHighlighting
                   forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
hl forall a b. (a -> b) -> a -> b
$
                     forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (String -> Idris ()
writeHighlights String
f)
                                (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()) -- failure is harmless
              Idris ()
clearHighlights
              IState
i <- Idris IState
getIState
              IState -> Idris ()
putIState (IState
i { default_total :: DefaultTotality
default_total = DefaultTotality
def_total,
                             hide_list :: Ctxt Accessibility
hide_list = forall {k} {a}. Map k a
emptyContext })
              forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    namespaces :: [String] -> [PDecl] -> [PDecl]
    namespaces :: [String] -> [PDecl] -> [PDecl]
namespaces []     [PDecl]
ds = [PDecl]
ds
    namespaces (String
x:[String]
xs) [PDecl]
ds = [forall t. String -> FC -> [PDecl' t] -> PDecl' t
PNamespace String
x FC
NoFC ([String] -> [PDecl] -> [PDecl]
namespaces [String]
xs [PDecl]
ds)]

    toMutual :: PDecl -> PDecl
    toMutual :: PDecl -> PDecl
toMutual m :: PDecl
m@(PMutual FC
_ [PDecl]
d) = PDecl
m
    toMutual (PNamespace String
x FC
fc [PDecl]
ds) = forall t. String -> FC -> [PDecl' t] -> PDecl' t
PNamespace String
x FC
fc (forall a b. (a -> b) -> [a] -> [b]
map PDecl -> PDecl
toMutual [PDecl]
ds)
    toMutual (POpenInterfaces FC
f [Name]
ns [PDecl]
ds) = forall t. FC -> [Name] -> [PDecl' t] -> PDecl' t
POpenInterfaces FC
f [Name]
ns (forall a b. (a -> b) -> [a] -> [b]
map PDecl -> PDecl
toMutual [PDecl]
ds)
    toMutual PDecl
x = let r :: PDecl
r = forall t. FC -> [PDecl' t] -> PDecl' t
PMutual (String -> FC
fileFC String
"single mutual") [PDecl
x] in
                 case PDecl
x of
                   PClauses{} -> PDecl
r
                   PInterface{} -> PDecl
r
                   PData{} -> PDecl
r
                   PImplementation{} -> PDecl
r
                   PDecl
_ -> PDecl
x

    addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
    addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()
addModDoc SyntaxInfo
syn [String]
mname Docstring ()
docs =
      do IState
ist <- Idris IState
getIState
         Docstring DocTerm
docs' <- ElabInfo
-> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)
elabDocTerms (String -> ElabInfo
toplevelWith String
f) (IState -> Docstring (Either Err PTerm)
parsedDocs IState
ist)
         let modDocs' :: Ctxt (Docstring DocTerm)
modDocs' = forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
docName Docstring DocTerm
docs' (IState -> Ctxt (Docstring DocTerm)
idris_moduledocs IState
ist)
         IState -> Idris ()
putIState IState
ist { idris_moduledocs :: Ctxt (Docstring DocTerm)
idris_moduledocs = Ctxt (Docstring DocTerm)
modDocs' }
         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCModDocs Name
docName)
      where
        docName :: Name
docName = Name -> [Text] -> Name
NS Name
modDocName (forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack (forall a. [a] -> [a]
reverse [String]
mname))
        parsedDocs :: IState -> Docstring (Either Err PTerm)
parsedDocs IState
ist = forall a b. (String -> b) -> Docstring a -> Docstring b
annotCode (SyntaxInfo -> IState -> String -> Either Err PTerm
tryFullExpr SyntaxInfo
syn IState
ist) Docstring ()
docs

{-| Adds names to hide list -}
addHides :: Ctxt Accessibility -> Idris ()
addHides :: Ctxt Accessibility -> Idris ()
addHides Ctxt Accessibility
xs = forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Name, Accessibility) -> Idris ()
doHide (forall a. Ctxt a -> [(Name, a)]
toAlist Ctxt Accessibility
xs)
  where doHide :: (Name, Accessibility) -> Idris ()
doHide (Name
n, Accessibility
a) = do Name -> Accessibility -> Idris ()
setAccessibility Name
n Accessibility
a
                           IBCWrite -> Idris ()
addIBC (Name -> Accessibility -> IBCWrite
IBCAccess Name
n Accessibility
a)