{-|
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 [] ([Text] -> Name) -> ([String] -> [Text]) -> [String] -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack ([String] -> Name) -> m [String] -> m Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [String]
forall (m :: * -> *). Parsing m => m [String]
moduleNamePieces where

  mkName :: [T.Text] -> [T.Text] -> Name
  mkName :: [Text] -> [Text] -> Name
mkName [Text]
ts [Text
x]    = if [Text] -> Bool
forall a. [a] -> Bool
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 Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
ts) [Text]
xs

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

moduleHeader :: IdrisParser (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
moduleHeader :: IdrisParser
  (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
moduleHeader =     IdrisParser
  (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
-> IdrisParser
     (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do docs <- StateT
  IState
  (WriterT FC (Parsec Void String))
  (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Maybe (Docstring (), [(Name, Docstring ())]))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional StateT
  IState
  (WriterT FC (Parsec Void String))
  (Docstring (), [(Name, Docstring ())])
docComment
                             noArgs docs
                             keyword "module"
                             (modName, ifc) <- withExtent moduleNamePieces
                             P.option ';' (lchar ';')
                             return (fmap fst docs,
                                     modName,
                                     [(ifc, AnnNamespace (map T.pack modName) Nothing)]))
               IdrisParser
  (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
-> IdrisParser
     (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
-> IdrisParser
     (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser
  (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
-> IdrisParser
     (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%'; String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"unqualified"
                             (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
-> IdrisParser
     (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Docstring ())
forall a. Maybe a
Nothing, [], []))
               IdrisParser
  (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
-> IdrisParser
     (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
-> IdrisParser
     (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
-> IdrisParser
     (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Docstring ())
forall a. Maybe a
Nothing, [String
"Main"], [])
  where noArgs :: Maybe (a, t a) -> m ()
noArgs (Just (a
_, t a
args)) | Bool -> Bool
not (t a -> Bool
forall a. t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t a
args) = String -> m ()
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Modules do not take arguments"
        noArgs Maybe (a, t a)
_ = () -> m ()
forall a. a -> m 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 <- StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) FC)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"import"
             reexport <- P.option False (True <$ keyword "public")
             (ns, idfc) <- withExtent moduleNamePieces
             newName <- optional (do keyword "as"
                                     withExtent identifier)
             P.option ';' (lchar ';')
             return $ ImportInfo reexport (toPath ns)
                        (fmap (\(String
n, FC
fc) -> ([String] -> String
toPath (String -> String -> [String]
forall a. Eq a => [a] -> [a] -> [[a]]
Spl.splitOn String
"." String
n), FC
fc)) newName)
                        (map T.pack ns) fc idfc
          IdrisParser ImportInfo -> String -> IdrisParser ImportInfo
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"import statement"
  where toPath :: [String] -> String
toPath = (String -> String -> String) -> [String] -> String
forall a. HasCallStack => (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 (decls, fc) <- IdrisParser [PDecl]
-> StateT IState (WriterT FC (Parsec Void String)) ([PDecl], FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser [PDecl]
 -> StateT IState (WriterT FC (Parsec Void String)) ([PDecl], FC))
-> IdrisParser [PDecl]
-> StateT IState (WriterT FC (Parsec Void String)) ([PDecl], FC)
forall a b. (a -> b) -> a -> b
$ do
                  StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => m ()
whiteSpace
                  decls <- [[PDecl]] -> [PDecl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[PDecl]] -> [PDecl])
-> StateT IState (WriterT FC (Parsec Void String)) [[PDecl]]
-> IdrisParser [PDecl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IdrisParser [PDecl]
-> StateT IState (WriterT FC (Parsec Void String)) [[PDecl]]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (SyntaxInfo -> IdrisParser [PDecl]
decl SyntaxInfo
syn)
                  case maxline syn of
                       Maybe Int
Nothing -> do StateT IState (WriterT FC (Parsec Void String)) ()
notOpenBraces; StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
                       Maybe Int
_ -> () -> StateT IState (WriterT FC (Parsec Void String)) ()
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  return decls
              ist <- get
              put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)),
                        ibc_write = IBCParsedRegion fc : ibc_write ist }
              return 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 = IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser [PDecl]
externalDecl SyntaxInfo
syn)
           IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
internalDecl SyntaxInfo
syn
           IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
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 <- StateT IState (WriterT FC (Parsec Void String)) 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 = case SyntaxInfo -> Maybe Int
maxline SyntaxInfo
syn of
                                Maybe Int
Nothing -> Bool
True
                                Just Int
l -> if (Int, Int) -> Int
forall a b. (a, b) -> a
fst (FC -> (Int, Int)
fc_end FC
fc) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
l
                                             then SyntaxInfo -> Int
mut_nesting SyntaxInfo
syn Int -> Int -> Bool
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 continue then
                 do notEndBlock
                    declBody continue
                else P.try (do notEndBlock
                               declBody continue)
                     <|> fail "End of readable input"
  where declBody :: Bool -> IdrisParser [PDecl]
        declBody :: Bool -> IdrisParser [PDecl]
declBody Bool
b =
                   IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser [PDecl]
implementation SyntaxInfo
syn)
                   IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser [PDecl]
openInterface SyntaxInfo
syn)
                   IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> IdrisParser [PDecl]
declBody' Bool
b
                   IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
using_ SyntaxInfo
syn
                   IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
params SyntaxInfo
syn
                   IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
mutual SyntaxInfo
syn
                   IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
namespace SyntaxInfo
syn
                   IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
interface_ SyntaxInfo
syn
                   IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do d <- SyntaxInfo -> IdrisParser PDecl
dsl SyntaxInfo
syn; return [d]
                   IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
directive SyntaxInfo
syn
                   IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
provider SyntaxInfo
syn
                   IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser [PDecl]
transform SyntaxInfo
syn
                   IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do IdrisParser ImportInfo
import_; String -> IdrisParser [PDecl]
forall a.
String -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"imports must be at top of file"
                   IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
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 d <- SyntaxInfo -> IdrisParser PDecl
decl' SyntaxInfo
syn
                            i <- get
                            let d' = (PTerm -> PTerm) -> PDecl -> PDecl
forall a b. (a -> b) -> PDecl' a -> PDecl' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SyntaxInfo -> PTerm -> PTerm
debindApp SyntaxInfo
syn (PTerm -> PTerm) -> (PTerm -> PTerm) -> PTerm -> PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
i)) PDecl
d
                            if continue cont d'
                               then return [d']
                               else fail "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
           IdrisParser PDecl -> IdrisParser PDecl -> IdrisParser PDecl
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
syntaxDecl SyntaxInfo
syn
           IdrisParser PDecl -> IdrisParser PDecl -> IdrisParser PDecl
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
fnDecl' SyntaxInfo
syn
           IdrisParser PDecl -> IdrisParser PDecl -> IdrisParser PDecl
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
data_ SyntaxInfo
syn
           IdrisParser PDecl -> IdrisParser PDecl -> IdrisParser PDecl
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
record SyntaxInfo
syn
           IdrisParser PDecl -> IdrisParser PDecl -> IdrisParser PDecl
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
runElabDecl SyntaxInfo
syn
           IdrisParser PDecl -> String -> IdrisParser PDecl
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 i <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                      notEndBlock
                      (decls, fc@(FC fn _ _)) <- withExtent $ declExtensions syn (syntaxRulesList $ syntax_rules i)
                      return $ map (mapPDeclFC (fixFC fc) (fixFCH fn fc)) 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 [] ((Syntax -> Bool) -> [Syntax] -> [Syntax]
forall a. (a -> Bool) -> [a] -> [a]
filter Syntax -> Bool
isDeclRule [Syntax]
rules)
                           IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
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 =
  [IdrisParser [PDecl]] -> IdrisParser [PDecl]
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice ([IdrisParser [PDecl]] -> IdrisParser [PDecl])
-> [IdrisParser [PDecl]] -> IdrisParser [PDecl]
forall a b. (a -> b) -> a -> b
$ (([Syntax] -> IdrisParser [PDecl])
 -> [[Syntax]] -> [IdrisParser [PDecl]])
-> [[Syntax]]
-> ([Syntax] -> IdrisParser [PDecl])
-> [IdrisParser [PDecl]]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ([Syntax] -> IdrisParser [PDecl])
-> [[Syntax]] -> [IdrisParser [PDecl]]
forall a b. (a -> b) -> [a] -> [b]
map ((Syntax -> Syntax -> Bool) -> [Syntax] -> [[Syntax]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy ([SSymbol] -> [SSymbol] -> Bool
forall {a}. Eq a => [a] -> [a] -> Bool
ruleGroup ([SSymbol] -> [SSymbol] -> Bool)
-> (Syntax -> [SSymbol]) -> Syntax -> Syntax -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Syntax -> [SSymbol]
syntaxSymbols) [Syntax]
rules) (([Syntax] -> IdrisParser [PDecl]) -> [IdrisParser [PDecl]])
-> ([Syntax] -> IdrisParser [PDecl]) -> [IdrisParser [PDecl]]
forall a b. (a -> b) -> a -> b
$ \[Syntax]
rs ->
    case [Syntax] -> Syntax
forall a. HasCallStack => [a] -> a
head [Syntax]
rs of -- can never be []
      DeclRule (SSymbol
symb:[SSymbol]
_) [PDecl]
_ -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisParser [PDecl] -> IdrisParser [PDecl])
-> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a b. (a -> b) -> a -> b
$ do
        n <- SSymbol -> IdrisParser (Maybe (Name, SynMatch))
extSymbol SSymbol
symb
        declExtension syn (n : ns) [DeclRule ss t | (DeclRule (_:ss) t) <- rs]
      -- If we have more than one Rule in this bucket, our grammar is
      -- nondeterministic.
      DeclRule [] [PDecl]
dec -> let r :: [PDecl]
r = (PDecl -> PDecl) -> [PDecl] -> [PDecl]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PDecl -> PDecl
update ((Maybe (Name, SynMatch) -> Maybe (Name, SynMatch))
-> [Maybe (Name, SynMatch)] -> [(Name, SynMatch)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Maybe (Name, SynMatch) -> Maybe (Name, SynMatch)
forall a. a -> a
id [Maybe (Name, SynMatch)]
ns)) [PDecl]
dec in
                             [PDecl] -> IdrisParser [PDecl]
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 (PDecl -> PDecl) -> (PDecl -> PDecl) -> PDecl -> PDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PTerm -> PTerm) -> PDecl -> PDecl
forall a b. (a -> b) -> PDecl' a -> PDecl' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> PTerm -> PTerm
updateRefs [(Name, SynMatch)]
ns) (PDecl -> PDecl) -> (PDecl -> PDecl) -> PDecl -> PDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PTerm -> PTerm) -> PDecl -> PDecl
forall a b. (a -> b) -> PDecl' a -> PDecl' b
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 Name -> [(Name, SynMatch)] -> Maybe SynMatch
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)
          = Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> PDecl
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)
         = FC -> FnOpts -> Name -> [PClause' PTerm] -> PDecl
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
o ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns Name
n) ((PClause' PTerm -> PClause' PTerm)
-> [PClause' PTerm] -> [PClause' PTerm]
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) = FC -> Name -> PTerm -> PDecl
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)
         = Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> DataOpts
-> PData' PTerm
-> PDecl
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 ([(Name, SynMatch)] -> PData' PTerm -> PData' PTerm
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) = FC -> [(Name, PTerm)] -> [PDecl] -> PDecl
forall t. FC -> [(Name, t)] -> [PDecl' t] -> PDecl' t
PParams FC
fc [(Name, PTerm)]
ps ((PDecl -> PDecl) -> [PDecl] -> [PDecl]
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) = String -> FC -> [PDecl] -> PDecl
forall t. String -> FC -> [PDecl' t] -> PDecl' t
PNamespace String
s FC
fc ((PDecl -> PDecl) -> [PDecl] -> [PDecl]
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)
         = Docstring (Either Err PTerm)
-> SyntaxInfo
-> FC
-> DataOpts
-> Name
-> FC
-> [(Name, FC, Plicity, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
-> Maybe (Name, FC)
-> Docstring (Either Err PTerm)
-> SyntaxInfo
-> PDecl
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
                   (((Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))
 -> (Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm))))
-> [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
-> [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)]
-> (Maybe (Name, FC), Plicity, PTerm,
    Maybe (Docstring (Either Err PTerm)))
-> (Maybe (Name, FC), Plicity, PTerm,
    Maybe (Docstring (Either Err PTerm)))
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)
                   ([(Name, SynMatch)] -> Maybe (Name, FC) -> Maybe (Name, FC)
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)
         = Docstring (Either Err PTerm)
-> SyntaxInfo
-> FC
-> [(Name, PTerm)]
-> Name
-> FC
-> [(Name, FC, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Name, FC)]
-> [PDecl]
-> Maybe (Name, FC)
-> Docstring (Either Err PTerm)
-> PDecl
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
                      ((PDecl -> PDecl) -> [PDecl] -> [PDecl]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PDecl -> PDecl
updateNs [(Name, SynMatch)]
ns) [PDecl]
ds)
                      ([(Name, SynMatch)] -> Maybe (Name, FC) -> Maybe (Name, FC)
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)
         = Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> [(Name, PTerm)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [PTerm]
-> [(Name, PTerm)]
-> PTerm
-> Maybe Name
-> [PDecl]
-> PDecl
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 ((Name -> Name) -> Maybe Name -> Maybe Name
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> Name -> Name
updateB [(Name, SynMatch)]
ns) Maybe Name
ni)
                           ((PDecl -> PDecl) -> [PDecl] -> [PDecl]
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) = FC -> [PDecl] -> PDecl
forall t. FC -> [PDecl' t] -> PDecl' t
PMutual FC
fc ((PDecl -> PDecl) -> [PDecl] -> [PDecl]
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)
        = Docstring (Either Err PTerm)
-> SyntaxInfo -> FC -> FC -> ProvideWhat' PTerm -> Name -> PDecl
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 = Maybe (Name, b)
forall a. Maybe a
Nothing
    updateRecCon [(Name, SynMatch)]
ns (Just (Name
n, b
fc)) = (Name, b) -> Maybe (Name, b)
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) = ([(Name, SynMatch)] -> Maybe (Name, b) -> Maybe (Name, b)
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)
       = FC
-> Name -> PTerm -> [PTerm] -> PTerm -> [PDecl] -> PClause' PTerm
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' ((PDecl -> PDecl) -> [PDecl] -> [PDecl]
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)
       = FC
-> Name
-> PTerm
-> [PTerm]
-> PTerm
-> Maybe (Name, FC)
-> [PDecl]
-> PClause' PTerm
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 ((PDecl -> PDecl) -> [PDecl] -> [PDecl]
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)
       = FC -> [PTerm] -> PTerm -> [PDecl] -> PClause' PTerm
forall t. FC -> [t] -> t -> [PDecl' t] -> PClause' t
PClauseR FC
fc [PTerm]
ts PTerm
t ((PDecl -> PDecl) -> [PDecl] -> [PDecl]
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)
       = FC
-> [PTerm]
-> PTerm
-> Maybe (Name, FC)
-> [PDecl]
-> PClause' PTerm
forall t.
FC -> [t] -> t -> Maybe (Name, FC) -> [PDecl' t] -> PClause' t
PWithR FC
fc [PTerm]
ts PTerm
t Maybe (Name, FC)
m ((PDecl -> PDecl) -> [PDecl] -> [PDecl]
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)
       = Name
-> FC
-> t
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]
-> PData' t
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 (((Docstring (Either Err PTerm),
  [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])
 -> (Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name]))
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]
-> [(Docstring (Either Err PTerm),
     [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)]
-> (Docstring (Either Err PTerm),
    [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])
-> (Docstring (Either Err PTerm),
    [(Name, Docstring (Either Err PTerm))], Name, FC, t, FC, [Name])
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)
       = Name -> FC -> t -> PData' 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 a -> a -> Bool
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) = Maybe (Name, SynMatch)
forall a. Maybe a
Nothing Maybe (Name, SynMatch)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser (Maybe (Name, SynMatch))
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword (Name -> String
forall a. Show a => a -> String
show Name
n)
    extSymbol (Expr Name
n) = do tm <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                            return $ Just (n, SynTm tm)
    extSymbol (SimpleExpr Name
n) = do tm <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
                                  return $ Just (n, SynTm tm)
    extSymbol (Binding Name
n) = do (b, fc) <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
                               return $ Just (n, SynBind fc b)
    extSymbol (Symbol String
s) = Maybe (Name, SynMatch)
forall a. Maybe a
Nothing Maybe (Name, SynMatch)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser (Maybe (Name, SynMatch))
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ OutputAnnotation
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (String -> StateT IState (WriterT FC (Parsec Void String)) ()
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 (s, fc) <- StateT IState (WriterT FC (Parsec Void String)) Syntax
-> StateT IState (WriterT FC (Parsec Void String)) (Syntax, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (StateT IState (WriterT FC (Parsec Void String)) Syntax
 -> StateT IState (WriterT FC (Parsec Void String)) (Syntax, FC))
-> StateT IState (WriterT FC (Parsec Void String)) Syntax
-> StateT IState (WriterT FC (Parsec Void String)) (Syntax, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo
-> StateT IState (WriterT FC (Parsec Void String)) Syntax
syntaxRule SyntaxInfo
syn
                    modify $ \IState
i -> IState
i IState -> Syntax -> IState
`addSyntax` Syntax
s
                    return (PSyntax fc 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 = updateSyntaxRules [s] rs,
                    syntax_keywords = ks ++ ns,
                    ibc_write = IBCSyntax s : map IBCKeyword ks ++ 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 = (Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Name -> String
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 = updateSyntaxRules [s] rs,
                        syntax_keywords = ks ++ ns }
  where rs :: SyntaxRules
rs = IState -> SyntaxRules
syntax_rules IState
i
        ns :: [String]
ns = IState -> [String]
syntax_keywords IState
i
        ks :: [String]
ks = (Name -> String) -> [Name] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Name -> String
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
-> StateT IState (WriterT FC (Parsec Void String)) Syntax
syntaxRule SyntaxInfo
syn
    = do sty <- StateT IState (WriterT FC (Parsec Void String)) SynContext
-> StateT IState (WriterT FC (Parsec Void String)) SynContext
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do
            StateT IState (WriterT FC (Parsec Void String)) ()
pushIndent
            sty <- SynContext
-> StateT IState (WriterT FC (Parsec Void String)) SynContext
-> StateT IState (WriterT FC (Parsec Void String)) SynContext
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option SynContext
AnySyntax
                            (SynContext
TermSyntax SynContext
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) SynContext
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"term"
                             StateT IState (WriterT FC (Parsec Void String)) SynContext
-> StateT IState (WriterT FC (Parsec Void String)) SynContext
-> StateT IState (WriterT FC (Parsec Void String)) SynContext
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SynContext
PatternSyntax SynContext
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) SynContext
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"pattern")
            keyword "syntax"
            return sty)
         syms <- some syntaxSym
         when (all isExpr syms) $ P.unexpected . P.Label . NonEmpty.fromList $ "missing keywords in syntax rule"
         let ns = (SSymbol -> Maybe Name) -> [SSymbol] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SSymbol -> Maybe Name
getName [SSymbol]
syms
         when (length ns /= length (nub ns))
            $ P.unexpected . P.Label . NonEmpty.fromList $ "repeated variable in syntax rule"
         lchar '='
         tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]
         terminator
         return (Rule (mkSimple syms) tm sty)
  StateT IState (WriterT FC (Parsec Void String)) Syntax
-> StateT IState (WriterT FC (Parsec Void String)) Syntax
-> StateT IState (WriterT FC (Parsec Void String)) Syntax
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"decl"; String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"syntax"
         syms <- StateT IState (WriterT FC (Parsec Void String)) SSymbol
-> StateT IState (WriterT FC (Parsec Void String)) [SSymbol]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some StateT IState (WriterT FC (Parsec Void String)) SSymbol
syntaxSym
         when (all isExpr syms) $ P.unexpected . P.Label . NonEmpty.fromList $ "missing keywords in syntax rule"
         let ns = (SSymbol -> Maybe Name) -> [SSymbol] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SSymbol -> Maybe Name
getName [SSymbol]
syms
         when (length ns /= length (nub ns))
            $ P.unexpected . P.Label . NonEmpty.fromList $ "repeated variable in syntax rule"
         lchar '='
         openBlock
         dec <- some (decl syn)
         closeBlock
         return (DeclRule (mkSimple syms) (concat dec))
  where
    isExpr :: SSymbol -> Bool
isExpr (Expr Name
_) = Bool
True
    isExpr SSymbol
_ = Bool
False
    getName :: SSymbol -> Maybe Name
getName (Expr Name
n) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
    getName SSymbol
_ = Maybe Name
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 SSymbol -> [SSymbol] -> [SSymbol]
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 SSymbol -> [SSymbol] -> [SSymbol]
forall a. a -> [a] -> [a]
: Name -> SSymbol
SimpleExpr Name
e1 SSymbol -> [SSymbol] -> [SSymbol]
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)
      | (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
opChars) String
ts String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"" = Name -> SSymbol
SimpleExpr Name
e SSymbol -> [SSymbol] -> [SSymbol]
forall a. a -> [a] -> [a]
: String -> SSymbol
Symbol String
s SSymbol -> [SSymbol] -> [SSymbol]
forall a. a -> [a] -> [a]
: [SSymbol] -> [SSymbol]
mkSimple' [SSymbol]
es
       where ts :: String
ts = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhileEnd Char -> Bool
isSpace (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
s
    mkSimple' (SSymbol
e : [SSymbol]
es) = SSymbol
e SSymbol -> [SSymbol] -> [SSymbol]
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' <- Name -> [(Name, Name)] -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Name)]
rens =
          PTerm -> IdrisParser PTerm
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
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' <- Name -> [(Name, Name)] -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Name)]
rens =
          PTerm -> IdrisParser PTerm
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
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 Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
userNames = (PTerm -> PTerm -> PTerm)
-> IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
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 ty' <- Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens PTerm
ty
               n' <- gensym n
               body' <- fixBind 0 ((n,n'):rens) body
               return $ PLam fc n' nfc ty' body'
        fixBind Int
0 [(Name, Name)]
rens (PPi Plicity
plic Name
n FC
nfc PTerm
argTy PTerm
body)
          | Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
userNames = (PTerm -> PTerm -> PTerm)
-> IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
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 ty' <- Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens PTerm
argTy
               n' <- gensym n
               body' <- fixBind 0 ((n,n'):rens) body
               return $ (PPi plic n' nfc ty' body')
        fixBind Int
0 [(Name, Name)]
rens (PLet FC
fc RigCount
rig Name
n FC
nfc PTerm
ty PTerm
val PTerm
body)
          | Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
userNames = (PTerm -> PTerm -> PTerm -> PTerm)
-> IdrisParser PTerm
-> IdrisParser PTerm
-> IdrisParser PTerm
-> IdrisParser PTerm
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 ty' <- Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind Int
0 [(Name, Name)]
rens PTerm
ty
               val' <- fixBind 0 rens val
               n' <- gensym n
               body' <- fixBind 0 ((n,n'):rens) body
               return $ PLet fc rig n' nfc ty' val' body'
        fixBind Int
0 [(Name, Name)]
rens (PMatchApp FC
fc Name
n) | Just Name
n' <- Name -> [(Name, Name)] -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Name)]
rens =
          PTerm -> IdrisParser PTerm
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
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' <- Name -> [(Name, Name)] -> Maybe Name
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n [(Name, Name)]
rens =
          PTerm -> IdrisParser PTerm
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
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) =
          (PTerm -> Maybe PTerm -> PTerm) -> Maybe PTerm -> PTerm -> PTerm
forall a b c. (a -> b -> c) -> b -> a -> c
flip PTerm -> Maybe PTerm -> PTerm
PQuasiquote Maybe PTerm
goal (PTerm -> PTerm) -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind (Int
q Int -> Int -> Int
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 (PTerm -> PTerm) -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [(Name, Name)] -> PTerm -> IdrisParser PTerm
fixBind (Int
q Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [(Name, Name)]
rens PTerm
tm

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

        gensym :: Name -> IdrisParser Name
        gensym :: Name -> StateT IState (WriterT FC (Parsec Void String)) Name
gensym Name
n = do ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                      let idx = IState -> Int
idris_name IState
ist
                      put ist { idris_name = idx + 1 }
                      return $ sMN idx (show n)

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

@
SyntaxSym ::=   '[' Name_t ']'
             |  '{' Name_t '}'
             |  Name_t
             |  StringLiteral_t
             ;
@
 -}
syntaxSym :: IdrisParser SSymbol
syntaxSym :: StateT IState (WriterT FC (Parsec Void String)) SSymbol
syntaxSym =    StateT IState (WriterT FC (Parsec Void String)) SSymbol
-> StateT IState (WriterT FC (Parsec Void String)) SSymbol
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'['; n <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name; lchar ']'
                         return (Expr n))
            StateT IState (WriterT FC (Parsec Void String)) SSymbol
-> StateT IState (WriterT FC (Parsec Void String)) SSymbol
-> StateT IState (WriterT FC (Parsec Void String)) SSymbol
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) SSymbol
-> StateT IState (WriterT FC (Parsec Void String)) SSymbol
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'{'; n <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name; lchar '}'
                          return (Binding n))
            StateT IState (WriterT FC (Parsec Void String)) SSymbol
-> StateT IState (WriterT FC (Parsec Void String)) SSymbol
-> StateT IState (WriterT FC (Parsec Void String)) SSymbol
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do n <- [String] -> StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). Parsing m => [String] -> m Name
iName []
                   return (Keyword n)
            StateT IState (WriterT FC (Parsec Void String)) SSymbol
-> StateT IState (WriterT FC (Parsec Void String)) SSymbol
-> StateT IState (WriterT FC (Parsec Void String)) SSymbol
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do sym <- StateT IState (WriterT FC (Parsec Void String)) String
forall (m :: * -> *). Parsing m => m String
stringLiteral
                   return (Symbol sym)
            StateT IState (WriterT FC (Parsec Void String)) SSymbol
-> String
-> StateT IState (WriterT FC (Parsec Void String)) SSymbol
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 = IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do StateT IState (WriterT FC (Parsec Void String)) ()
notEndBlock
                       d <- SyntaxInfo -> IdrisParser PDecl
fnDecl' SyntaxInfo
syn
                       i <- get
                       let d' = (PTerm -> PTerm) -> PDecl -> PDecl
forall a b. (a -> b) -> PDecl' a -> PDecl' b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SyntaxInfo -> PTerm -> PTerm
debindApp SyntaxInfo
syn (PTerm -> PTerm) -> (PTerm -> PTerm) -> PTerm -> PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
i) PDecl
d
                       return [d']) IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
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 (IdrisParser PDecl -> IdrisParser PDecl)
-> IdrisParser PDecl -> IdrisParser PDecl
forall a b. (a -> b) -> a -> b
$
              do (doc, argDocs, fc, opts', n, nfc, acc) <- StateT
  IState
  (WriterT FC (Parsec Void String))
  (Docstring (Either Err PTerm),
   [(Name, Docstring (Either Err PTerm))], FC, FnOpts, Name, FC,
   Accessibility)
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], FC, FnOpts, Name, FC,
      Accessibility)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do
                        StateT IState (WriterT FC (Parsec Void String)) ()
pushIndent
                        (doc, argDocs) <- SyntaxInfo
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))])
docstring SyntaxInfo
syn
                        (opts, acc) <- fnOpts
                        (n_in, nfc) <- withExtent fnName
                        let n = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n_in
                        fc <- extent $ lchar ':'
                        return (doc, argDocs, fc, opts, n, nfc, acc))
                 ty <- typeExpr (allowImp syn)
                 terminator
                 -- If it's a top level function, note the accessibility
                 -- rules
                 when (syn_toplevel syn) $ addAcc n acc
                 return (PTy doc argDocs syn fc opts' n nfc ty)
            IdrisParser PDecl -> IdrisParser PDecl -> IdrisParser PDecl
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
postulate SyntaxInfo
syn
            IdrisParser PDecl -> IdrisParser PDecl -> IdrisParser PDecl
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
caf SyntaxInfo
syn
            IdrisParser PDecl -> IdrisParser PDecl -> IdrisParser PDecl
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PDecl
pattern SyntaxInfo
syn)
            IdrisParser PDecl -> String -> IdrisParser PDecl
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
    opts <- StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpts
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many StateT IState (WriterT FC (Parsec Void String)) FnOpt
fnOpt
    acc <- accessibility
    opts' <- many fnOpt
    let allOpts = FnOpts
opts FnOpts -> FnOpts -> FnOpts
forall a. [a] -> [a] -> [a]
++ FnOpts
opts'
    let existingTotality = FnOpts
allOpts FnOpts -> FnOpts -> FnOpts
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [FnOpt
TotalFn, FnOpt
CoveringFn, FnOpt
PartialFn]
    opts'' <- addDefaultTotality (nub existingTotality) allOpts
    return (opts'', 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
          ist <- m IState
forall s (m :: * -> *). MonadState s m => m s
get
          case default_total ist of
            DefaultTotality
DefaultCheckingTotal    -> FnOpts -> m FnOpts
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (FnOpt
TotalFnFnOpt -> FnOpts -> FnOpts
forall a. a -> [a] -> [a]
:FnOpts
opts)
            DefaultTotality
DefaultCheckingCovering -> FnOpts -> m FnOpts
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (FnOpt
CoveringFnFnOpt -> FnOpts -> FnOpts
forall a. a -> [a] -> [a]
:FnOpts
opts)
            DefaultTotality
DefaultCheckingPartial  -> FnOpts -> m FnOpts
forall a. a -> m a
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 = FnOpts -> m FnOpts
forall a. a -> m a
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 =
          String -> m FnOpts
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Conflicting totality modifiers specified " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FnOpt -> String
prettyTot FnOpt
tot1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" and " String -> String -> String
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 :: StateT IState (WriterT FC (Parsec Void String)) FnOpt
fnOpt = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"total"; FnOpt -> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return FnOpt
TotalFn
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
PartialFn FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"partial"
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
CoveringFn FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"covering"
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"export"); c <- StateT IState (WriterT FC (Parsec Void String)) String
forall (m :: * -> *). Parsing m => m String
stringLiteral;
                      return $ CExport c
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
NoImplicit FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"no_implicit")
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
Inlinable FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"inline")
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
StaticFn FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"static")
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
ErrorHandler FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"error_handler")
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
ErrorReverse FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"error_reverse")
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
ErrorReduce  FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"error_reduce")
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
Reflection   FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"reflection")
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
AutoHint     FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"hint")
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
OverlappingDictionary FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"overlapping")
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%'; String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"specialise";
               Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'['; ns <- StateT IState (WriterT FC (Parsec Void String)) (Name, Maybe Int)
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT
     IState (WriterT FC (Parsec Void String)) [(Name, Maybe Int)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy StateT IState (WriterT FC (Parsec Void String)) (Name, Maybe Int)
nameTimes (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','); lchar ']';
               return $ Specialise ns
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FnOpt
Implicit FnOpt
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall a b.
a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"implicit"
        StateT IState (WriterT FC (Parsec Void String)) FnOpt
-> String -> StateT IState (WriterT FC (Parsec Void String)) FnOpt
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"function modifier"
  where nameTimes :: IdrisParser (Name, Maybe Int)
        nameTimes :: StateT IState (WriterT FC (Parsec Void String)) (Name, Maybe Int)
nameTimes = do n <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                       t <- P.option Nothing (do reds <- natural
                                                 return (Just (fromInteger reds)))
                       return (n, 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 (doc, ext)
                       <- StateT
  IState
  (WriterT FC (Parsec Void String))
  (Docstring (Either Err PTerm), Bool)
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Docstring (Either Err PTerm), Bool)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (StateT
   IState
   (WriterT FC (Parsec Void String))
   (Docstring (Either Err PTerm), Bool)
 -> StateT
      IState
      (WriterT FC (Parsec Void String))
      (Docstring (Either Err PTerm), Bool))
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Docstring (Either Err PTerm), Bool)
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Docstring (Either Err PTerm), Bool)
forall a b. (a -> b) -> a -> b
$ do (doc, _) <- SyntaxInfo
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))])
docstring SyntaxInfo
syn
                                     pushIndent
                                     ext <- ppostDecl
                                     return (doc, ext)
                   ist <- get
                   (opts, acc) <- fnOpts
                   (n_in, nfc) <- withExtent fnName
                   let n = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n_in
                   lchar ':'
                   ty <- typeExpr (allowImp syn)
                   fc <- extent $ terminator
                   addAcc n acc
                   return (PPostulate ext doc syn fc nfc opts n ty)
                 IdrisParser PDecl -> String -> IdrisParser PDecl
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 <- String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"postulate"; return False
                 StateT IState (WriterT FC (Parsec Void String)) Bool
-> StateT IState (WriterT FC (Parsec Void String)) Bool
-> StateT IState (WriterT FC (Parsec Void String)) Bool
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%'; String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"extern"; Bool -> StateT IState (WriterT FC (Parsec Void String)) Bool
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"using"
       Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'('; ns <- SyntaxInfo -> IdrisParser [Using]
usingDeclList SyntaxInfo
syn; lchar ')'
       openBlock
       let uvars = SyntaxInfo -> [Using]
using SyntaxInfo
syn
       ds <- many (decl (syn { using = uvars ++ ns }))
       closeBlock
       return (concat ds)
    IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
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 (ns, fc) <- StateT
  IState
  (WriterT FC (Parsec Void String))
  [(RigCount, Name, FC, PTerm)]
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     ([(RigCount, Name, FC, PTerm)], FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (StateT
   IState
   (WriterT FC (Parsec Void String))
   [(RigCount, Name, FC, PTerm)]
 -> StateT
      IState
      (WriterT FC (Parsec Void String))
      ([(RigCount, Name, FC, PTerm)], FC))
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [(RigCount, Name, FC, PTerm)]
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     ([(RigCount, Name, FC, PTerm)], FC)
forall a b. (a -> b) -> a -> b
$ do
          String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"parameters"
          Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'(' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [(RigCount, Name, FC, PTerm)]
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [(RigCount, Name, FC, PTerm)]
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
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 StateT
  IState
  (WriterT FC (Parsec Void String))
  [(RigCount, Name, FC, PTerm)]
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     [(RigCount, Name, FC, PTerm)]
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
')'
       let ns' = [(Name
n, PTerm
ty) | (RigCount
_, Name
n, FC
_, PTerm
ty) <- [(RigCount, Name, FC, PTerm)]
ns]
       openBlock
       let pvars = SyntaxInfo -> [(Name, PTerm)]
syn_params SyntaxInfo
syn
       ds <- many (decl syn { syn_params = pvars ++ ns' })
       closeBlock
       return [PParams fc ns' (concat ds)]
    IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
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 (ns, fc) <- StateT IState (WriterT FC (Parsec Void String)) [(Name, FC)]
-> StateT
     IState (WriterT FC (Parsec Void String)) ([(Name, FC)], FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (StateT IState (WriterT FC (Parsec Void String)) [(Name, FC)]
 -> StateT
      IState (WriterT FC (Parsec Void String)) ([(Name, FC)], FC))
-> StateT IState (WriterT FC (Parsec Void String)) [(Name, FC)]
-> StateT
     IState (WriterT FC (Parsec Void String)) ([(Name, FC)], FC)
forall a b. (a -> b) -> a -> b
$ do
         String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"using"
         String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"implementation"
         StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) [(Name, FC)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName) (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')

       openBlock
       ds <- many (decl syn)
       closeBlock
       return [POpenInterfaces fc (map fst ns) (concat ds)]
    IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
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 <- StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) FC)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"mutual"
       openBlock
       ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))
       closeBlock
       return [PMutual fc (concat ds)]
    IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
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 String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"namespace"
       (n, nfc) <- StateT IState (WriterT FC (Parsec Void String)) String
-> StateT IState (WriterT FC (Parsec Void String)) (String, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) String
forall (m :: * -> *). Parsing m => m String
identifier
       openBlock
       ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
       closeBlock
       return [PNamespace n nfc (concat ds)]
     IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
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 String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"where"
                             StateT IState (WriterT FC (Parsec Void String)) ()
openBlock
                             ds <- IdrisParser [PDecl]
-> StateT IState (WriterT FC (Parsec Void String)) [[PDecl]]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (SyntaxInfo -> IdrisParser [PDecl]
fnDecl SyntaxInfo
syn)
                             closeBlock
                             return (concat ds)
                          IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
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 String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"where"
                        StateT IState (WriterT FC (Parsec Void String)) ()
openBlock
                        (cn, cd) <- (Maybe (Name, FC), Docstring ())
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Maybe (Name, FC), Docstring ())
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Maybe (Name, FC), Docstring ())
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Maybe (Name, FC)
forall a. Maybe a
Nothing, Docstring ()
forall a. Docstring a
emptyDocstring) (StateT
   IState
   (WriterT FC (Parsec Void String))
   (Maybe (Name, FC), Docstring ())
 -> StateT
      IState
      (WriterT FC (Parsec Void String))
      (Maybe (Name, FC), Docstring ()))
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Maybe (Name, FC), Docstring ())
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Maybe (Name, FC), Docstring ())
forall a b. (a -> b) -> a -> b
$
                                    StateT
  IState
  (WriterT FC (Parsec Void String))
  (Maybe (Name, FC), Docstring ())
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Maybe (Name, FC), Docstring ())
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (doc, _) <- (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Docstring (), [(Name, Docstring ())])
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (), [(Name, Docstring ())])
forall a. (Docstring a, [(Name, Docstring a)])
noDocs StateT
  IState
  (WriterT FC (Parsec Void String))
  (Docstring (), [(Name, Docstring ())])
docComment
                                              n <- constructor
                                              return (Just n, doc))
                        ist <- get
                        let cd' = SyntaxInfo
-> IState -> Docstring () -> Docstring (Either Err PTerm)
annotate SyntaxInfo
syn IState
ist Docstring ()
cd

                        ds <- many (notEndBlock >> P.try (implementation syn)
                                                   <|> do x <- data_ syn
                                                          return [x]
                                                   <|> fnDecl syn)
                        closeBlock
                        return (cn, cd', concat ds)
                     IdrisParser
  (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
-> String
-> IdrisParser
     (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"interface block"
  where
    constructor :: IdrisParser (Name, FC)
    constructor :: StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
constructor = String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"constructor" StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
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 = (String -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
forall a b. (String -> b) -> Docstring a -> Docstring b
annotCode ((String -> Either Err PTerm)
 -> Docstring () -> Docstring (Either Err PTerm))
-> (String -> Either Err PTerm)
-> Docstring ()
-> Docstring (Either Err PTerm)
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 (doc, argDocs, acc)
                      <- StateT
  IState
  (WriterT FC (Parsec Void String))
  (Docstring (Either Err PTerm),
   [(Name, Docstring (Either Err PTerm))], Accessibility)
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))], Accessibility)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (doc, argDocs) <- SyntaxInfo
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))])
docstring SyntaxInfo
syn
                                   acc <- accessibility
                                   interfaceKeyword
                                   return (doc, argDocs, acc))
                    ((cons', n, nfc, cs, fds), fc) <- withExtent $ do
                        cons <- constraintList syn
                        let cons' = [(Name
c, PTerm
ty) | (RigCount
_, Name
c, FC
_, PTerm
ty) <- [(RigCount, Name, FC, PTerm)]
cons]
                        (n_in, nfc) <- withExtent fnName
                        let n = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n_in
                        cs <- many carg
                        fds <- P.option [(cn, NoFC) | (cn, _, _) <- cs] fundeps
                        return (cons', n, nfc, cs, fds)

                    (cn, cd, ds) <- P.option (Nothing, fst noDocs, []) (interfaceBlock syn)
                    accData acc n (concatMap declared ds)
                    return [PInterface doc syn fc cons' n nfc cs argDocs fds ds cn cd]
                 IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
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 Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|'; StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) [(Name, FC)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy (StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name) (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')

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

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

    carg :: IdrisParser (Name, FC, PTerm)
    carg :: StateT IState (WriterT FC (Parsec Void String)) (Name, FC, PTerm)
carg = do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'('; (i, ifc) <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name; lchar ':'; ty <- expr syn; lchar ')'
              return (i, ifc, ty)
       StateT IState (WriterT FC (Parsec Void String)) (Name, FC, PTerm)
-> StateT
     IState (WriterT FC (Parsec Void String)) (Name, FC, PTerm)
-> StateT
     IState (WriterT FC (Parsec Void String)) (Name, FC, PTerm)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do (i, ifc) <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
              return (i, ifc, PType 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 (doc, argDocs) <- SyntaxInfo
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))])
docstring SyntaxInfo
syn
                        (opts, acc) <- fnOpts
                        optional implementationKeyword

                        ((en, cs, cs', cn, cnfc, args, pnames), fc) <- withExtent $ do
                            en <- optional implementationName
                            cs <- constraintList syn
                            let cs' = [(Name
c, PTerm
ty) | (RigCount
_, Name
c, FC
_, PTerm
ty) <- [(RigCount, Name, FC, PTerm)]
cs]
                            (cn, cnfc) <- withExtent fnName
                            args <- many (simpleExpr syn)
                            pnames <- implementationUsing
                            return (en, cs, cs', cn, cnfc, args, pnames)

                        let sc = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
cnfc [FC
cnfc] Name
cn) ((PTerm -> PArg) -> [PTerm] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map PTerm -> PArg
forall {t}. t -> PArg' t
pexp [PTerm]
args)
                        let 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 = r }) [(RigCount, Name, FC, PTerm)]
cs PTerm
sc

                        ds <- implementationBlock syn
                        return [PImplementation doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]
                      IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"implementation declaration"
  where implementationName :: IdrisParser Name
        implementationName :: StateT IState (WriterT FC (Parsec Void String)) Name
implementationName = do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'['; n_in <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName; lchar ']'
                                let n = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn Name
n_in
                                return n
                             StateT IState (WriterT FC (Parsec Void String)) Name
-> String -> StateT IState (WriterT FC (Parsec Void String)) Name
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`. " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                          String
"`instance` is provided for those coming from Haskell. " String -> String -> String
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 = String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"implementation"
                         StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do fc <- StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) FC)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"instance"
                                parserWarning fc Nothing (Msg instanceWarning)

        implementationUsing :: IdrisParser [Name]
        implementationUsing :: IdrisParser [Name]
implementationUsing = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"using"
                                 ns <- StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) [(Name, FC)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName) (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                                 return (map fst ns)
                              IdrisParser [Name] -> IdrisParser [Name] -> IdrisParser [Name]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Name] -> IdrisParser [Name]
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) 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 (doc, argDocs) <- (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Docstring (), [(Name, Docstring ())])
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Docstring (), [(Name, Docstring ())])
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (Docstring (), [(Name, Docstring ())])
forall a. (Docstring a, [(Name, Docstring a)])
noDocs StateT
  IState
  (WriterT FC (Parsec Void String))
  (Docstring (), [(Name, Docstring ())])
docComment
                   ist <- get
                   let doc' = (String -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
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
n, (String -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
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 ]
                   return (doc', 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
               = IdrisParser [Using] -> IdrisParser [Using]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (StateT IState (WriterT FC (Parsec Void String)) Using
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [Using]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) Using
usingDecl SyntaxInfo
syn) (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
','))
             IdrisParser [Using] -> IdrisParser [Using] -> IdrisParser [Using]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do ns <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [Name]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                    lchar ':'
                    t <- typeExpr (disallowImp syn)
                    return (map (\Name
x -> Name -> PTerm -> Using
UImplicit Name
x PTerm
t) ns)
             IdrisParser [Using] -> String -> IdrisParser [Using]
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 -> StateT IState (WriterT FC (Parsec Void String)) Using
usingDecl SyntaxInfo
syn = StateT IState (WriterT FC (Parsec Void String)) Using
-> StateT IState (WriterT FC (Parsec Void String)) Using
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do x <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                          lchar ':'
                          t <- typeExpr (disallowImp syn)
                          return (UImplicit x t))
            StateT IState (WriterT FC (Parsec Void String)) Using
-> StateT IState (WriterT FC (Parsec Void String)) Using
-> StateT IState (WriterT FC (Parsec Void String)) Using
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do c <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                   xs <- many fnName
                   return (UConstraint c xs)
            StateT IState (WriterT FC (Parsec Void String)) Using
-> String -> StateT IState (WriterT FC (Parsec Void String)) Using
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 (clause, fc) <- StateT IState (WriterT FC (Parsec Void String)) (PClause' PTerm)
-> StateT
     IState (WriterT FC (Parsec Void String)) (PClause' PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (SyntaxInfo
-> StateT IState (WriterT FC (Parsec Void String)) (PClause' PTerm)
clause SyntaxInfo
syn)
                 return (PClauses fc [] (sMN 2 "_") [clause]) -- collect together later
              IdrisParser PDecl -> String -> IdrisParser PDecl
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 String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"let"
             (n, fc) <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn (Name -> Name)
-> StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName)
             pushIndent
             lchar '='
             t <- indented $ expr syn
             terminator
             return (PCAF fc n t)
           IdrisParser PDecl -> String -> IdrisParser PDecl
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 = True } in
                  IdrisParser PTerm -> IdrisParser PTerm
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser PTerm
hsimpleExpr SyntaxInfo
syn') IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
simpleExternalExpr SyntaxInfo
syn'
              IdrisParser PTerm -> String -> IdrisParser PTerm
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 Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'='
               StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt
               IdrisParser PTerm -> IdrisParser (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm -> IdrisParser (PTerm, FC))
-> IdrisParser PTerm -> IdrisParser (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
        IdrisParser (PTerm, FC)
-> IdrisParser (PTerm, FC) -> IdrisParser (PTerm, FC)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol String
"?=";
               (name, fc) <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (StateT IState (WriterT FC (Parsec Void String)) Name
 -> StateT IState (WriterT FC (Parsec Void String)) (Name, FC))
-> StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall a b. (a -> b) -> a -> b
$ Name
-> StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option Name
n' (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol String
"{" StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) Name
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) Name
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol String
"}")
               r <- expr syn
               return (addLet fc name r, fc)
        IdrisParser (PTerm, FC)
-> IdrisParser (PTerm, FC) -> IdrisParser (PTerm, FC)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser PTerm -> IdrisParser (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent IdrisParser PTerm
impossible
        IdrisParser (PTerm, FC) -> String -> IdrisParser (PTerm, FC)
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
xString -> String -> String
forall 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 (((PTerm, PTerm) -> (PTerm, PTerm))
-> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm, PTerm) -> (PTerm, PTerm)
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
-> StateT IState (WriterT FC (Parsec Void String)) (PClause' PTerm)
clause SyntaxInfo
syn
           -- unnamed with or function clause (inside a with)
         = do wargs <- StateT IState (WriterT FC (Parsec Void String)) [PTerm]
-> StateT IState (WriterT FC (Parsec Void String)) [PTerm]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do StateT IState (WriterT FC (Parsec Void String)) ()
pushIndent; IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) [PTerm]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some (SyntaxInfo -> IdrisParser PTerm
wExpr SyntaxInfo
syn))
              ist <- get
              n <- case lastParse ist of
                        Just Name
t -> Name -> StateT IState (WriterT FC (Parsec Void String)) Name
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
t
                        Maybe Name
Nothing -> String -> StateT IState (WriterT FC (Parsec Void String)) Name
forall a.
String -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Invalid clause"
              (do (r, fc) <- rhs syn n
                  let wsyn = SyntaxInfo
syn { syn_namespace = [], syn_toplevel = False }
                  (wheres, nmap) <-     whereBlock n wsyn <* popIndent
                                    <|> ([], []) <$ terminator
                  return $ PClauseR fc wargs r wheres) <|> (do
                  popIndent
                  ((wval, pn), fc) <- withExtent $ do
                      keyword "with"
                      wval <- bracketed syn
                      pn <- optProof
                      return (wval, pn)
                  openBlock
                  ds <- some $ fnDecl syn
                  let withs = [[PDecl]] -> [PDecl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PDecl]]
ds
                  closeBlock
                  return $ PWithR fc wargs wval pn withs)
           -- <==
       StateT IState (WriterT FC (Parsec Void String)) (PClause' PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) (PClause' PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) (PClause' PTerm)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do ty <- IdrisParser PTerm -> IdrisParser PTerm
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do StateT IState (WriterT FC (Parsec Void String)) ()
pushIndent
                              ty <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
                              symbol "<=="
                              return ty)
              (n, fc) <- withExtent (expandNS syn <$> fnName)
              (r, _) <- rhs syn n
              let wsyn = SyntaxInfo
syn { syn_namespace = [] }
              (wheres, nmap) <-   whereBlock n wsyn <* popIndent
                                <|> ([], []) <$ terminator
              let 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"))
              ist <- get
              put (ist { lastParse = Just n })
              return $ PClause fc n capp [] r wheres
           -- lhs application "with" clause or function clause
       StateT IState (WriterT FC (Parsec Void String)) (PClause' PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) (PClause' PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) (PClause' PTerm)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
pushIndent
              (n, nfc, capp, wargs) <- IdrisParser (Name, FC, PTerm, [PTerm])
lhs
              modify $ \IState
ist -> IState
ist { lastParse = Just n }
              (do (rs, fc) <- rhs syn n
                  let wsyn = SyntaxInfo
syn { syn_namespace = [] }
                  (wheres, nmap) <-     whereBlock n wsyn <* popIndent
                                    <|> ([], []) <$ terminator
                  return $ PClause fc n capp wargs rs wheres) <|> (do
                   popIndent
                   ((wval, pn), fc) <- withExtent $ do
                       keyword "with"
                       wval <- bracketed syn
                       pn <- optProof
                       return (wval, pn)
                   openBlock
                   ds <- some $ fnDecl syn
                   closeBlock
                   let withs = (PDecl -> PDecl) -> [PDecl] -> [PDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> PTerm -> [PTerm] -> PDecl -> PDecl
fillLHSD Name
n PTerm
capp [PTerm]
wargs) ([PDecl] -> [PDecl]) -> [PDecl] -> [PDecl]
forall a b. (a -> b) -> a -> b
$ [[PDecl]] -> [PDecl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PDecl]]
ds
                   return $ PWith fc n capp wargs wval pn withs)
      StateT IState (WriterT FC (Parsec Void String)) (PClause' PTerm)
-> String
-> StateT IState (WriterT FC (Parsec Void String)) (PClause' PTerm)
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 l <- SyntaxInfo -> IdrisParser PTerm
argExpr SyntaxInfo
syn
                     (op, nfc) <- withExtent symbolicOperator
                     when (op == "=" || op == "?=" ) $
                          fail "infix clause definition with \"=\" and \"?=\" not supported "
                     let n = SyntaxInfo -> Name -> Name
expandNS SyntaxInfo
syn (String -> Name
sUN String
op)
                     r <- argExpr syn
                     wargs <- many (wExpr syn)
                     return (n, nfc, [pexp l, pexp r], wargs)

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

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

    optProof :: StateT IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
optProof = Maybe (Name, FC)
-> StateT
     IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
-> StateT
     IState (WriterT FC (Parsec Void String)) (Maybe (Name, FC))
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option Maybe (Name, FC)
forall a. Maybe a
Nothing (do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"proof"
                                    n <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                                    return (Just 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)
       = FC
-> Name -> PTerm -> [PTerm] -> PTerm -> [PDecl] -> PClause' PTerm
forall t. FC -> Name -> t -> [t] -> t -> [PDecl' t] -> PClause' t
PClause FC
fc Name
n PTerm
capp ([PTerm]
owargs [PTerm] -> [PTerm] -> [PTerm]
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)
       = FC
-> Name
-> PTerm
-> [PTerm]
-> PTerm
-> Maybe (Name, FC)
-> [PDecl]
-> PClause' PTerm
forall t.
FC
-> Name
-> t
-> [t]
-> t
-> Maybe (Name, FC)
-> [PDecl' t]
-> PClause' t
PWith FC
fc Name
n PTerm
capp ([PTerm]
owargs [PTerm] -> [PTerm] -> [PTerm]
forall a. [a] -> [a] -> [a]
++ [PTerm]
wargs) PTerm
v Maybe (Name, FC)
pn
            ((PDecl -> PDecl) -> [PDecl] -> [PDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> PTerm -> [PTerm] -> PDecl -> PDecl
fillLHSD Name
n PTerm
capp ([PTerm]
owargs [PTerm] -> [PTerm] -> [PTerm]
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) = FC -> FnOpts -> Name -> [PClause' PTerm] -> PDecl
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses FC
fc FnOpts
o Name
fn ((PClause' PTerm -> PClause' PTerm)
-> [PClause' PTerm] -> [PClause' PTerm]
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 Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'|'
               SyntaxInfo -> IdrisParser PTerm
expr' (SyntaxInfo
syn { inPattern = True })
            IdrisParser PTerm -> String -> IdrisParser PTerm
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 -> IdrisParser ([PDecl], [(Name, Name)])
whereBlock Name
n SyntaxInfo
syn
    = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"where"
         ds <- IdrisParser [PDecl]
-> StateT IState (WriterT FC (Parsec Void String)) [[PDecl]]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
indentedBlock1 (SyntaxInfo -> IdrisParser [PDecl]
decl SyntaxInfo
syn)
         let dns = ([PDecl] -> [Name]) -> [[PDecl]] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((PDecl -> [Name]) -> [PDecl] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl -> [Name]
declared) [[PDecl]]
ds
         return (concat ds, map (\Name
x -> (Name
x, SyntaxInfo -> Name -> Name
decoration SyntaxInfo
syn Name
x)) dns)
      IdrisParser ([PDecl], [(Name, Name)])
-> String -> IdrisParser ([PDecl], [(Name, Name)])
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 n <- StateT IState (WriterT FC (Parsec Void String)) String
forall (m :: * -> *). Parsing m => m String
identifier
              return (Via IBCFormat (map toLower n))
       IdrisParser Codegen -> IdrisParser Codegen -> IdrisParser Codegen
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"Bytecode"; Codegen -> IdrisParser Codegen
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Codegen
Bytecode
       IdrisParser Codegen -> String -> IdrisParser Codegen
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 StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"lib")
                   cgn <- IdrisParser Codegen
codegen_
                   lib <- stringLiteral
                   return [PDirective (DLib cgn lib)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"link")
                    cgn <- IdrisParser Codegen
codegen_; obj <- stringLiteral
                    return [PDirective (DLink cgn obj)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"flag")
                    cgn <- IdrisParser Codegen
codegen_; flag <- stringLiteral
                    return [PDirective (DFlag cgn flag)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"include")
                    cgn <- IdrisParser Codegen
codegen_
                    hdr <- stringLiteral
                    return [PDirective (DInclude cgn hdr)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"hide"); n <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                    return [PDirective (DHide n)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"freeze"); n <- [String] -> StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). Parsing m => [String] -> m Name
iName []
                    return [PDirective (DFreeze n)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"thaw"); n <- [String] -> StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). Parsing m => [String] -> m Name
iName []
                    return [PDirective (DThaw n)]
             -- injectivity assertins are intended for debugging purposes
             -- only, and won't be documented/could be removed at any point
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"assert_injective"); n <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                    return [PDirective (DInjective 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)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"access")
                    acc <- IdrisParser Accessibility
accessibility
                    ist <- get
                    put ist { default_access = acc }
                    return [PDirective (DAccess acc)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"default"); tot <- IdrisParser DefaultTotality
totality
                    i <- get
                    put (i { default_total = tot } )
                    return [PDirective (DDefault tot)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"logging")
                    i <- StateT IState (WriterT FC (Parsec Void String)) Integer
forall (m :: * -> *). Parsing m => m Integer
natural
                    return [PDirective (DLogging i)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"dynamic")
                    libs <- StateT IState (WriterT FC (Parsec Void String)) String
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) [String]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 StateT IState (WriterT FC (Parsec Void String)) String
forall (m :: * -> *). Parsing m => m String
stringLiteral (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
',')
                    return [PDirective (DDynamicLibs libs)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"name")
                    (ty, tyFC) <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                    ns <- P.sepBy1 (withExtent name) (lchar ',')
                    return [PDirective (DNameHint ty tyFC ns)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"error_handlers")
                    (fn, nfc) <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                    (arg, afc) <- withExtent fnName
                    ns <- P.sepBy1 (withExtent name) (lchar ',')
                    return [PDirective (DErrorHandlers fn nfc arg afc ns) ]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"language"); ext <- IdrisParser LanguageExt
pLangExt;
                    return [PDirective (DLanguage ext)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"deprecate")
                    n <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                    alt <- P.option "" stringLiteral
                    return [PDirective (DDeprecate n alt)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"fragile")
                    n <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
                    alt <- P.option "" stringLiteral
                    return [PDirective (DFragile n alt)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do fc <- StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) FC)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall a b. (a -> b) -> a -> b
$ StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"used")
                    fn <- fnName
                    arg <- iName []
                    return [PDirective (DUsed fc fn arg)]
             IdrisParser [PDecl] -> IdrisParser [PDecl] -> IdrisParser [PDecl]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"auto_implicits")
                    b <- StateT IState (WriterT FC (Parsec Void String)) Bool
on_off
                    return [PDirective (DAutoImplicits b)]
             IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
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 String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"on"; Bool -> StateT IState (WriterT FC (Parsec Void String)) Bool
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
             StateT IState (WriterT FC (Parsec Void String)) Bool
-> StateT IState (WriterT FC (Parsec Void String)) Bool
-> StateT IState (WriterT FC (Parsec Void String)) Bool
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"off"; Bool -> StateT IState (WriterT FC (Parsec Void String)) Bool
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

pLangExt :: IdrisParser LanguageExt
pLangExt :: IdrisParser LanguageExt
pLangExt = (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"TypeProviders" StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser LanguageExt -> IdrisParser LanguageExt
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LanguageExt -> IdrisParser LanguageExt
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return LanguageExt
TypeProviders)
       IdrisParser LanguageExt
-> IdrisParser LanguageExt -> IdrisParser LanguageExt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"ErrorReflection" StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser LanguageExt -> IdrisParser LanguageExt
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LanguageExt -> IdrisParser LanguageExt
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return LanguageExt
ErrorReflection)
       IdrisParser LanguageExt
-> IdrisParser LanguageExt -> IdrisParser LanguageExt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"UniquenessTypes" StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser LanguageExt -> IdrisParser LanguageExt
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LanguageExt -> IdrisParser LanguageExt
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return LanguageExt
UniquenessTypes)
       IdrisParser LanguageExt
-> IdrisParser LanguageExt -> IdrisParser LanguageExt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"LinearTypes" StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser LanguageExt -> IdrisParser LanguageExt
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LanguageExt -> IdrisParser LanguageExt
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return LanguageExt
LinearTypes)
       IdrisParser LanguageExt
-> IdrisParser LanguageExt -> IdrisParser LanguageExt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"DSLNotation" StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser LanguageExt -> IdrisParser LanguageExt
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LanguageExt -> IdrisParser LanguageExt
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return LanguageExt
DSLNotation)
       IdrisParser LanguageExt
-> IdrisParser LanguageExt -> IdrisParser LanguageExt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"ElabReflection" StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser LanguageExt -> IdrisParser LanguageExt
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LanguageExt -> IdrisParser LanguageExt
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return LanguageExt
ElabReflection)
       IdrisParser LanguageExt
-> IdrisParser LanguageExt -> IdrisParser LanguageExt
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"FirstClassReflection" StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser LanguageExt -> IdrisParser LanguageExt
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LanguageExt -> IdrisParser LanguageExt
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"total";   DefaultTotality -> IdrisParser DefaultTotality
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return DefaultTotality
DefaultCheckingTotal
      IdrisParser DefaultTotality
-> IdrisParser DefaultTotality -> IdrisParser DefaultTotality
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"partial"; DefaultTotality -> IdrisParser DefaultTotality
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (m :: * -> *) a. Monad m => a -> m a
return DefaultTotality
DefaultCheckingPartial
      IdrisParser DefaultTotality
-> IdrisParser DefaultTotality -> IdrisParser DefaultTotality
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"covering"; DefaultTotality -> IdrisParser DefaultTotality
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 doc <- StateT
  IState
  (WriterT FC (Parsec Void String))
  (Docstring (Either Err PTerm))
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Docstring (Either Err PTerm))
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (doc, _) <- SyntaxInfo
-> IdrisParser
     (Docstring (Either Err PTerm),
      [(Name, Docstring (Either Err PTerm))])
docstring SyntaxInfo
syn
                                   highlight AnnKeyword $ lchar '%' *> reserved "provide"
                                   return doc)
                  provideTerm doc <|> providePostulate doc
               IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
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 Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'('; (n, nfc) <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName; lchar ':'; t <- typeExpr syn; lchar ')'
             keyword "with"
             (e, fc) <- withExtent (expr syn) <?> "provider expression"
             return  [PProvider doc syn fc nfc (ProvTerm t e) n]
        providePostulate :: Docstring (Either Err PTerm) -> IdrisParser [PDecl]
providePostulate Docstring (Either Err PTerm)
doc =
          do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword String
"postulate"
             (n, nfc) <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
             keyword "with"
             (e, fc) <- withExtent (expr syn) <?> "provider expression"
             return [PProvider doc syn fc nfc (ProvPostulate e) n]

{-| Parses a transform

@
Transform ::= '%' 'transform' Expr '==>' Expr
@
-}
transform :: SyntaxInfo -> IdrisParser [PDecl]
transform :: SyntaxInfo -> IdrisParser [PDecl]
transform SyntaxInfo
syn = do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
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)
                   l <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                   fc <- extent $ symbol "==>"
                   r <- expr syn
                   return [PTransform fc False l r]
                IdrisParser [PDecl] -> String -> IdrisParser [PDecl]
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 kwFC <- StateT IState (WriterT FC (Parsec Void String)) FC
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (OutputAnnotation
-> StateT IState (WriterT FC (Parsec Void String)) FC
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnKeyword (StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) FC)
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall a b. (a -> b) -> a -> b
$ Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar Char
'%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"runElab"))
     script <- expr syn <?> "elaborator script"
     return $ PRunElabDecl kwFC script (syn_namespace syn)
  IdrisParser PDecl -> String -> IdrisParser PDecl
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 = IdrisParser PTerm
-> IState -> String -> String -> Either ParseError PTerm
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 = Parser IState Const
-> IState -> String -> String -> Either ParseError Const
forall st res.
Parser st res -> st -> String -> String -> Either ParseError res
runparser Parser IState Const
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 = Parser IState PTactic
-> IState -> String -> String -> Either ParseError PTactic
forall st res.
Parser st res -> st -> String -> String -> Either ParseError res
runparser (SyntaxInfo -> Parser IState 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 = Parser IState (Either ElabShellCmd PDo)
-> IState
-> String
-> String
-> Either ParseError (Either ElabShellCmd PDo)
forall st res.
Parser st res -> st -> String -> String -> Either ParseError res
runparser (PDo -> Either ElabShellCmd PDo
forall a b. b -> Either a b
Right (PDo -> Either ElabShellCmd PDo)
-> StateT IState (WriterT FC (Parsec Void String)) PDo
-> Parser IState (Either ElabShellCmd PDo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PDo
do_ SyntaxInfo
defaultSyntax Parser IState (Either ElabShellCmd PDo)
-> Parser IState (Either ElabShellCmd PDo)
-> Parser IState (Either ElabShellCmd PDo)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ElabShellCmd -> Either ElabShellCmd PDo
forall a b. a -> Either a b
Left (ElabShellCmd -> Either ElabShellCmd PDo)
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> Parser IState (Either ElabShellCmd PDo)
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 = Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
char Char
':' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                       (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"qed"     StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ElabShellCmd
EQED       ) StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"abandon" StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ElabShellCmd
EAbandon   ) StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"undo"    StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ElabShellCmd
EUndo      ) StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"state"   StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ElabShellCmd
EProofState) StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"term"    StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ElabShellCmd
EProofTerm ) StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       ([String]
-> (PTerm -> ElabShellCmd)
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall {b}.
[String]
-> (PTerm -> b)
-> StateT IState (WriterT FC (Parsec Void String)) b
expressionTactic [String
"e", String
"eval"] PTerm -> ElabShellCmd
EEval ) StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       ([String]
-> (PTerm -> ElabShellCmd)
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall {b}.
[String]
-> (PTerm -> b)
-> StateT IState (WriterT FC (Parsec Void String)) b
expressionTactic [String
"t", String
"type"] PTerm -> ElabShellCmd
ECheck) StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       ([String]
-> (PTerm -> ElabShellCmd)
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall {b}.
[String]
-> (PTerm -> b)
-> StateT IState (WriterT FC (Parsec Void String)) b
expressionTactic [String
"search"] PTerm -> ElabShellCmd
ESearch   ) StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                       (do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
"doc"
                           doc <- (Const -> Either Name Const
forall a b. b -> Either a b
Right (Const -> Either Name Const)
-> Parser IState Const
-> StateT
     IState (WriterT FC (Parsec Void String)) (Either Name Const)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser IState Const
forall (m :: * -> *). Parsing m => m Const
constant) StateT IState (WriterT FC (Parsec Void String)) (Either Name Const)
-> StateT
     IState (WriterT FC (Parsec Void String)) (Either Name Const)
-> StateT
     IState (WriterT FC (Parsec Void String)) (Either Name Const)
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Name -> Either Name Const
forall a b. a -> Either a b
Left (Name -> Either Name Const)
-> StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT
     IState (WriterT FC (Parsec Void String)) (Either Name Const)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName)
                           P.eof
                           return (EDocStr doc))
                       StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
-> String
-> StateT IState (WriterT FC (Parsec Void String)) ElabShellCmd
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 [StateT IState (WriterT FC (Parsec Void String)) ()]
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
asum ((String -> StateT IState (WriterT FC (Parsec Void String)) ())
-> [String] -> [StateT IState (WriterT FC (Parsec Void String)) ()]
forall a b. (a -> b) -> [a] -> [b]
map String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved [String]
cmds)
              t <- IdrisParser PTerm -> IdrisParser PTerm
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)
              i <- get
              return $ tactic (desugar defaultSyntax i t)
        spaced :: f b -> f b
spaced f b
parser = f ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt f () -> f b -> f b
forall a b. f a -> f b -> f b
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 i <- Idris IState
getIState
         case runparser imports i fname input of
              Left ParseError
err -> ParseError -> Idris OutputDoc
forall w. Message w => w -> Idris OutputDoc
formatMessage ParseError
err Idris OutputDoc
-> (OutputDoc
    -> Idris
         (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark))
-> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark)
forall a b.
StateT IState (ExceptT Err IO) a
-> (a -> StateT IState (ExceptT Err IO) b)
-> StateT IState (ExceptT Err IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String
-> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark)
forall a. String -> Idris a
ifail (String
 -> Idris
      (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark))
-> (OutputDoc -> String)
-> OutputDoc
-> Idris (Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutputDoc -> String
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
                   fname' <- IO String -> Idris String
forall a. IO a -> Idris a
runIO (IO String -> Idris String) -> IO String -> Idris String
forall a b. (a -> b) -> a -> b
$ String -> IO String
Dir.makeAbsolute String
fname
                   sendHighlighting $ S.fromList $ addPath annots fname'
                   return x
  where imports :: IdrisParser ((Maybe (Docstring ()), [String],
                                 [ImportInfo],
                                 Maybe Mark),
                                [(FC, OutputAnnotation)], IState)
        imports :: Parser
  IState
  ((Maybe (Docstring ()), [String], [ImportInfo], Maybe Mark),
   [(FC, OutputAnnotation)], IState)
imports = do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe ())
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional StateT IState (WriterT FC (Parsec Void String)) ()
shebang
                     StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => m ()
whiteSpace
                     (mdoc, mname, annots) <- IdrisParser
  (Maybe (Docstring ()), [String], [(FC, OutputAnnotation)])
moduleHeader
                     ps_exp        <- many import_
                     mrk           <- mark
                     isEof         <- lookAheadMatches P.eof
                     let mrk' = if Bool
isEof
                                   then Maybe Mark
forall a. Maybe a
Nothing
                                   else Mark -> Maybe Mark
forall a. a -> Maybe a
Just Mark
mrk
                     i     <- get
                     -- add Builtins and Prelude, unless options say
                     -- not to
                     let ps = [ImportInfo]
ps_exp -- imp "Builtins" : imp "Prelude" : ps_exp
                     return ((mdoc, mname, ps, mrk'), annots, 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 (String -> Maybe String
forall a. a -> Maybe a
Just String
path)) (FC', OutputAnnotation)
-> [(FC', OutputAnnotation)] -> [(FC', OutputAnnotation)]
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) (FC', OutputAnnotation)
-> [(FC', OutputAnnotation)] -> [(FC', OutputAnnotation)]
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 = String -> StateT IState (WriterT FC (Parsec Void String)) String
forall (m :: * -> *). Parsing m => String -> m String
string String
"#!" StateT IState (WriterT FC (Parsec Void String)) String
-> StateT IState (WriterT FC (Parsec Void String)) [Token String]
-> StateT IState (WriterT FC (Parsec Void String)) [Token String]
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT IState (WriterT FC (Parsec Void String)) (Token String)
-> StateT IState (WriterT FC (Parsec Void String)) [Token String]
forall a.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ((Token String -> Bool)
-> StateT IState (WriterT FC (Parsec Void String)) (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
P.satisfy ((Token String -> Bool)
 -> StateT IState (WriterT FC (Parsec Void String)) (Token String))
-> (Token String -> Bool)
-> StateT IState (WriterT FC (Parsec Void String)) (Token String)
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isEol) StateT IState (WriterT FC (Parsec Void String)) [Token String]
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => m ()
eol StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b.
StateT IState (WriterT FC (Parsec Void String)) a
-> StateT IState (WriterT FC (Parsec Void String)) b
-> StateT IState (WriterT FC (Parsec Void String)) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> StateT IState (WriterT FC (Parsec Void String)) ()
forall a. a -> StateT IState (WriterT FC (Parsec Void String)) a
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 i <- Idris IState
getIState
         case runparser mainProg i fname input of
            Left ParseError
err -> do ParseError -> Idris ()
forall w. Message w => w -> Idris ()
emitWarning ParseError
err
                           i <- Idris IState
getIState
                           putIState (i { errSpan = Just (messageExtent err) })
                           return []
            Right ([PDecl]
x, IState
i)  -> do IState -> Idris ()
putIState IState
i
                                Idris ()
reportParserWarnings
                                [PDecl] -> Idris [PDecl]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([PDecl] -> Idris [PDecl]) -> [PDecl] -> Idris [PDecl]
forall a b. (a -> b) -> a -> b
$ [PDecl] -> [PDecl]
collect [PDecl]
x
  where mainProg :: IdrisParser ([PDecl], IState)
        mainProg :: Parser IState ([PDecl], IState)
mainProg = case Maybe Mark
mrk of
                        Maybe Mark
Nothing -> do i <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get; return ([], i)
                        Just Mark
mrk -> do
                          Mark -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => Mark -> m ()
restore Mark
mrk
                          ds <- SyntaxInfo -> IdrisParser [PDecl]
prog SyntaxInfo
syn
                          i' <- get
                          return (ds, 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 PDecl -> [PDecl] -> [PDecl]
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' = Maybe Name -> [PClause' PTerm] -> [PDecl] -> [PDecl]
clauses Maybe Name
j (FC
-> Name -> PTerm -> [PTerm] -> PTerm -> [PDecl] -> PClause' PTerm
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) PClause' PTerm -> [PClause' PTerm] -> [PClause' PTerm]
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 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n' = Maybe Name -> [PClause' PTerm] -> [PDecl] -> [PDecl]
clauses Maybe Name
j (FC
-> Name
-> PTerm
-> [PTerm]
-> PTerm
-> Maybe (Name, FC)
-> [PDecl]
-> PClause' PTerm
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) PClause' PTerm -> [PClause' PTerm] -> [PClause' PTerm]
forall a. a -> [a] -> [a]
: [PClause' PTerm]
acc) [PDecl]
ds
        clauses (Just Name
n) [PClause' PTerm]
acc [PDecl]
xs = FC -> FnOpts -> Name -> [PClause' PTerm] -> PDecl
forall t. FC -> FnOpts -> Name -> [PClause' t] -> PDecl' t
PClauses (PDecl -> FC
fcOf PDecl
c) FnOpts
o Name
n ([PClause' PTerm] -> [PClause' PTerm]
forall a. [a] -> [a]
reverse [PClause' PTerm]
acc) PDecl -> [PDecl] -> [PDecl]
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]
_]) = Name -> Maybe Name
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]
_]) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
n
        cname (PClauses FC
fc FnOpts
_ Name
_ [PClauseR FC
_ [PTerm]
_ PTerm
_ [PDecl]
_]) = Maybe Name
forall a. Maybe a
Nothing
        cname (PClauses FC
fc FnOpts
_ Name
_ [PWithR FC
_ [PTerm]
_ PTerm
_ Maybe (Name, FC)
_ [PDecl]
_]) = Maybe Name
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) = FC -> [(Name, PTerm)] -> [PDecl] -> PDecl
forall t. FC -> [(Name, t)] -> [PDecl' t] -> PDecl' t
PParams FC
f [(Name, PTerm)]
ns ([PDecl] -> [PDecl]
collect [PDecl]
ps) PDecl -> [PDecl] -> [PDecl]
forall a. a -> [a] -> [a]
: [PDecl] -> [PDecl]
collect [PDecl]
ds
collect (POpenInterfaces FC
f [Name]
ns [PDecl]
ps : [PDecl]
ds) = FC -> [Name] -> [PDecl] -> PDecl
forall t. FC -> [Name] -> [PDecl' t] -> PDecl' t
POpenInterfaces FC
f [Name]
ns ([PDecl] -> [PDecl]
collect [PDecl]
ps) PDecl -> [PDecl] -> [PDecl]
forall a. a -> [a] -> [a]
: [PDecl] -> [PDecl]
collect [PDecl]
ds
collect (PMutual FC
f [PDecl]
ms : [PDecl]
ds) = FC -> [PDecl] -> PDecl
forall t. FC -> [PDecl' t] -> PDecl' t
PMutual FC
f ([PDecl] -> [PDecl]
collect [PDecl]
ms) PDecl -> [PDecl] -> [PDecl]
forall a. a -> [a] -> [a]
: [PDecl] -> [PDecl]
collect [PDecl]
ds
collect (PNamespace String
ns FC
fc [PDecl]
ps : [PDecl]
ds) = String -> FC -> [PDecl] -> PDecl
forall t. String -> FC -> [PDecl' t] -> PDecl' t
PNamespace String
ns FC
fc ([PDecl] -> [PDecl]
collect [PDecl]
ps) PDecl -> [PDecl] -> [PDecl]
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')
    = Docstring (Either Err PTerm)
-> SyntaxInfo
-> FC
-> [(Name, PTerm)]
-> Name
-> FC
-> [(Name, FC, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Name, FC)]
-> [PDecl]
-> Maybe (Name, FC)
-> Docstring (Either Err PTerm)
-> PDecl
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 PDecl -> [PDecl] -> [PDecl]
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')
    = Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> SyntaxInfo
-> FC
-> [(Name, PTerm)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [PTerm]
-> [(Name, PTerm)]
-> PTerm
-> Maybe Name
-> [PDecl]
-> PDecl
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) PDecl -> [PDecl] -> [PDecl]
forall a. a -> [a] -> [a]
: [PDecl] -> [PDecl]
collect [PDecl]
ds'
collect (PDecl
d : [PDecl]
ds) = PDecl
d PDecl -> [PDecl] -> [PDecl]
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
   = Idris (Maybe String)
-> (Err -> Idris (Maybe String)) -> Idris (Maybe String)
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)
                          ist <- Idris IState
getIState
                          iWarn (getErrSpan e) $ pprintErr ist e
                          return Nothing)

{-| Load idris module -}
loadModule' :: FilePath -> IBCPhase -> Idris (Maybe String)
loadModule' :: String -> IBCPhase -> Idris (Maybe String)
loadModule' String
f IBCPhase
phase
   = do i <- Idris IState
getIState
        let file = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
' ') String
f
        ibcsd <- valIBCSubDir i
        ids <- rankedImportDirs file
        fp <- findImport ids ibcsd file
        if file `elem` imported i
          then do logParser 1 $ "Already read " ++ file
                  return Nothing
          else do putIState (i { imported = file : imported i })
                  case fp of
                    IDR String
fn  -> Bool -> String -> Maybe Int -> Idris ()
loadSource Bool
False String
fn Maybe Int
forall a. Maybe a
Nothing
                    LIDR String
fn -> Bool -> String -> Maybe Int -> Idris ()
loadSource Bool
True  String
fn Maybe Int
forall a. Maybe a
Nothing
                    IBC String
fn IFileType
src ->
                      Idris () -> (Err -> Idris ()) -> Idris ()
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 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
fn String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" failed " String -> String -> String
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 Maybe Int
forall a. Maybe a
Nothing
                                             LIDR String
sfn -> Bool -> String -> Maybe Int -> Idris ()
loadSource Bool
True String
sfn Maybe Int
forall a. Maybe a
Nothing)
                  return $ Just 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 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Skipping " String -> String -> String
forall a. [a] -> [a] -> [a]
++ IFileType -> String
getSrcFile IFileType
i
        Int -> String -> Idris ()
logParser Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"loadFromIFile i" String -> String -> String
forall a. [a] -> [a] -> [a]
++ IFileType -> String
forall a. Show a => a -> String
show IFileType
i
        Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (Bool -> IBCPhase -> String -> Idris ()
loadIBC Bool
reexp IBCPhase
phase String
fn)
                (\Err
err -> Err -> Idris ()
forall a. Err -> Idris a
ierror (Err -> Idris ()) -> Err -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> Err -> Err
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
   = Idris () -> (Err -> Idris ()) -> Idris ()
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)
                          ist <- Idris IState
getIState
                          case 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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f)
          Int -> String -> Idris ()
iReport   Int
2 (String
"Reading " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f)
          i <- Idris IState
getIState
          let def_total = IState -> DefaultTotality
default_total IState
i
          file_in <- runIO $ readSource f
          file <- if lidr then tclift $ unlit f file_in else return file_in
          (mdocs, mname, imports_in, pos) <- parseImports f file
          ai <- getAutoImports
          let imports = (String -> ImportInfo) -> [String] -> [ImportInfo]
forall a b. (a -> b) -> [a] -> [b]
map (\String
n -> Bool
-> String -> Maybe (String, FC) -> [Text] -> FC -> FC -> ImportInfo
ImportInfo Bool
True String
n Maybe (String, FC)
forall a. Maybe a
Nothing [] FC
NoFC FC
NoFC) [String]
ai [ImportInfo] -> [ImportInfo] -> [ImportInfo]
forall a. [a] -> [a] -> [a]
++ [ImportInfo]
imports_in
          ids <- rankedImportDirs f
          ibcsd <- valIBCSubDir i
          let ibc = String -> String -> String
ibcPathNoFallback String
ibcsd String
f
          impHashes <- idrisCatch (getImportHashes ibc)
                                  (\Err
err -> [(String, Int)] -> Idris [(String, Int)]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [])
          newHashes <- mapM (\ (Bool
_, String
f, [Text]
_, FC
_) ->
                         do fp <- [String] -> String -> String -> Idris IFileType
findImport [String]
ids String
ibcsd String
f
                            case fp of
                                 IBC String
fn IFileType
src ->
                                   StateT IState (ExceptT Err IO) (Maybe (String, Int))
-> (Err -> StateT IState (ExceptT Err IO) (Maybe (String, Int)))
-> StateT IState (ExceptT Err IO) (Maybe (String, Int))
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (do hash <- String -> Idris Int
getIBCHash String
fn
                                                  return (Just (fn, hash)))
                                              (\Err
err -> Maybe (String, Int)
-> StateT IState (ExceptT Err IO) (Maybe (String, Int))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (String, Int)
forall a. Maybe a
Nothing)
                                 IFileType
_ -> Maybe (String, Int)
-> StateT IState (ExceptT Err IO) (Maybe (String, Int))
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (String, Int)
forall a. Maybe a
Nothing)
                [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]

          fmod <- liftIO $ Dir.getModificationTime f
          ibcexists <- liftIO $ Dir.doesFileExist ibc
          ibcmod <- if ibcexists
                       then liftIO $ Dir.getModificationTime ibc
                       else return fmod

          logParser 10 $ ibc ++ " " ++ show ibcmod
          logParser 10 $ f ++ " " ++ show fmod
          logParser 10 $ show impHashes ++ "\n" ++ show 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 = (UTCTime
ibcmod UTCTime -> UTCTime -> Bool
forall a. Ord a => a -> a -> Bool
<= UTCTime
fmod) Bool -> Bool -> Bool
||
                         ([(String, Int)] -> [(String, Int)]
forall a. Ord a => [a] -> [a]
sort [(String, Int)]
impHashes [(String, Int)] -> [(String, Int)] -> Bool
forall a. Eq a => a -> a -> Bool
/= [(String, Int)] -> [(String, Int)]
forall a. Ord a => [a] -> [a]
sort ((Maybe (String, Int) -> Maybe (String, Int))
-> [Maybe (String, Int)] -> [(String, Int)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Maybe (String, Int) -> Maybe (String, Int)
forall a. a -> a
id [Maybe (String, Int)]
newHashes))

          if not needLoad
             then pure ()
             else do
              iReport 1 $ "Type checking " ++ f
              mapM_ (\ (Bool
re, String
f, [Text]
ns, FC
nfc) ->
                           do fp <- [String] -> String -> String -> Idris IFileType
findImport [String]
ids String
ibcsd String
f
                              case fp of
                                  LIDR String
fn -> String -> Idris ()
forall a. String -> Idris a
ifail (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"No ibc for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f
                                  IDR String
fn -> String -> Idris ()
forall a. String -> Idris a
ifail (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"No ibc for " String -> String -> String
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 -> String -> Maybe String
forall a. a -> Maybe a
Just String
fn
                                                     LIDR String
fn -> String -> Maybe String
forall a. a -> Maybe a
Just String
fn
                                                     IFileType
_ -> Maybe String
forall a. Maybe a
Nothing
                                       srcFnAbs <- case Maybe String
srcFn of
                                                     Just String
fn -> (String -> Maybe String) -> Idris String -> Idris (Maybe String)
forall a b.
(a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Maybe String
forall a. a -> Maybe a
Just (IO String -> Idris String
forall a. IO a -> Idris a
runIO (IO String -> Idris String) -> IO String -> Idris String
forall a b. (a -> b) -> a -> b
$ String -> IO String
Dir.makeAbsolute String
fn)
                                                     Maybe String
Nothing -> Maybe String -> Idris (Maybe String)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing
                                       sendHighlighting $ S.fromList [(FC' nfc, AnnNamespace ns srcFnAbs)])
                    [(re, fn, ns, nfc) | ImportInfo re fn _ ns _ nfc <- imports]
              reportParserWarnings
              sendParserHighlighting

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

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

              case (ds', 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 ist <- Idris IState
getIState
                     putIState ist { idris_parsedSpan = oldSpan
                                   , ibc_write = IBCParsedRegion fc :
                                                 ibc_write ist
                                   }
                ([PDecl], Maybe FC)
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              sendParserHighlighting

              -- Parsing done, now process declarations

              let ds = [String] -> [PDecl] -> [PDecl]
namespaces [String]
mname [PDecl]
ds'
              logParser 3 (show $ showDecls verbosePPOption ds)
              i <- getIState
              logLvl 10 (show (toAlist (idris_implicits i)))
              logLvl 3 (show (idris_infixes 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
              elabDecls (toplevelWith f) (map toMutual ds)
              i <- getIState
              -- simplify every definition do give the totality checker
              -- a better chance
              mapM_ (\Name
n -> do Int -> String -> Idris ()
logLvl Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Simplifying " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
                              ctxt' <-
                                do ctxt <- Idris Context
getContext
                                   tclift $ simplifyCasedef n [] [] (getErasureInfo i) ctxt
                              setContext ctxt')
                       (map snd (idris_totcheck i))
              -- build size change graph from simplified definitions
              iReport 3 $ "Totality checking " ++ f
              logLvl 1 $ "Totality checking " ++ f
              i <- getIState
              mapM_ buildSCG (idris_totcheck i)
              mapM_ checkDeclTotality (idris_totcheck i)
              mapM_ verifyTotality (idris_totcheck i)

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

              logLvl 1 ("Finished " ++ f)
              ibcsd <- valIBCSubDir i
              logLvl  1 $ "Universe checking " ++ f
              iReport 3 $ "Universe checking " ++ f
              iucheck
              i <- getIState
              addHides (hide_list i)

              -- Save module documentation if applicable
              i <- getIState
              case mdocs of
                Maybe (Docstring ())
Nothing   -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
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
              ok <- noErrors
              when ok $
                do idrisCatch (do writeIBC f ibc; clearIBC)
                              (\Err
c -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) -- failure is harmless
                   hl <- getDumpHighlighting
                   when hl $
                     idrisCatch (writeHighlights f)
                                (const $ return ()) -- failure is harmless
              clearHighlights
              i <- getIState
              putIState (i { default_total = def_total,
                             hide_list = emptyContext })
              return ()
  where
    namespaces :: [String] -> [PDecl] -> [PDecl]
    namespaces :: [String] -> [PDecl] -> [PDecl]
namespaces []     [PDecl]
ds = [PDecl]
ds
    namespaces (String
x:[String]
xs) [PDecl]
ds = [String -> FC -> [PDecl] -> PDecl
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) = String -> FC -> [PDecl] -> PDecl
forall t. String -> FC -> [PDecl' t] -> PDecl' t
PNamespace String
x FC
fc ((PDecl -> PDecl) -> [PDecl] -> [PDecl]
forall a b. (a -> b) -> [a] -> [b]
map PDecl -> PDecl
toMutual [PDecl]
ds)
    toMutual (POpenInterfaces FC
f [Name]
ns [PDecl]
ds) = FC -> [Name] -> [PDecl] -> PDecl
forall t. FC -> [Name] -> [PDecl' t] -> PDecl' t
POpenInterfaces FC
f [Name]
ns ((PDecl -> PDecl) -> [PDecl] -> [PDecl]
forall a b. (a -> b) -> [a] -> [b]
map PDecl -> PDecl
toMutual [PDecl]
ds)
    toMutual PDecl
x = let r :: PDecl
r = FC -> [PDecl] -> PDecl
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 ist <- Idris IState
getIState
         docs' <- elabDocTerms (toplevelWith f) (parsedDocs ist)
         let modDocs' = Name
-> Docstring DocTerm
-> Ctxt (Docstring DocTerm)
-> Ctxt (Docstring DocTerm)
forall a. Name -> a -> Ctxt a -> Ctxt a
addDef Name
docName Docstring DocTerm
docs' (IState -> Ctxt (Docstring DocTerm)
idris_moduledocs IState
ist)
         putIState ist { idris_moduledocs = modDocs' }
         addIBC (IBCModDocs docName)
      where
        docName :: Name
docName = Name -> [Text] -> Name
NS Name
modDocName ((String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack ([String] -> [String]
forall a. [a] -> [a]
reverse [String]
mname))
        parsedDocs :: IState -> Docstring (Either Err PTerm)
parsedDocs IState
ist = (String -> Either Err PTerm)
-> Docstring () -> Docstring (Either Err PTerm)
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 = ((Name, Accessibility) -> Idris ())
-> [(Name, Accessibility)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Name, Accessibility) -> Idris ()
doHide (Ctxt Accessibility -> [(Name, Accessibility)]
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)