{-|
Module      : Idris.Parser.Expr
Description : Parse Expressions.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE FlexibleContexts, TupleSections #-}
module Idris.Parser.Expr where

import Idris.AbsSyntax
import Idris.Core.TT
import Idris.DSL
import Idris.Options
import Idris.Parser.Helpers
import Idris.Parser.Ops

import Prelude hiding (pi)

import Control.Applicative
import Control.Arrow (left)
import Control.Monad
import qualified Control.Monad.Combinators.Expr as P
import Control.Monad.State.Strict
import Data.Function (on)
import Data.List
import Data.Maybe
import Text.Megaparsec ((<?>))
import qualified Text.Megaparsec as P
import qualified Text.Megaparsec.Char as P

-- | Allow implicit type declarations
allowImp :: SyntaxInfo -> SyntaxInfo
allowImp :: SyntaxInfo -> SyntaxInfo
allowImp syn :: SyntaxInfo
syn = SyntaxInfo
syn { implicitAllowed :: Bool
implicitAllowed = Bool
True,
                     constraintAllowed :: Bool
constraintAllowed = Bool
False }

-- | Disallow implicit type declarations
disallowImp :: SyntaxInfo -> SyntaxInfo
disallowImp :: SyntaxInfo -> SyntaxInfo
disallowImp = SyntaxInfo -> SyntaxInfo
scopedImp

-- | Implicits hare are scoped rather than top level
scopedImp :: SyntaxInfo -> SyntaxInfo
scopedImp :: SyntaxInfo -> SyntaxInfo
scopedImp syn :: SyntaxInfo
syn = SyntaxInfo
syn { implicitAllowed :: Bool
implicitAllowed = Bool
False,
                      constraintAllowed :: Bool
constraintAllowed = Bool
False }

-- | Allow scoped constraint arguments
allowConstr :: SyntaxInfo -> SyntaxInfo
allowConstr :: SyntaxInfo -> SyntaxInfo
allowConstr syn :: SyntaxInfo
syn = SyntaxInfo
syn { constraintAllowed :: Bool
constraintAllowed = Bool
True }

{-| Parses an expression as a whole
@
  FullExpr ::= Expr EOF_t;
@
 -}
fullExpr :: SyntaxInfo -> IdrisParser PTerm
fullExpr :: SyntaxInfo -> IdrisParser PTerm
fullExpr syn :: SyntaxInfo
syn = do PTerm
x <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                  StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
                  IState
i <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                  PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> PTerm -> PTerm
debindApp SyntaxInfo
syn (SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
i PTerm
x)

tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm
tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm
tryFullExpr syn :: SyntaxInfo
syn st :: IState
st = (ParseError -> Err) -> Either ParseError PTerm -> Either Err PTerm
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left (String -> Err
forall t. String -> Err' t
Msg (String -> Err) -> (ParseError -> String) -> ParseError -> Err
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (ParseError -> Doc) -> ParseError -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> Doc
parseErrorDoc) (Either ParseError PTerm -> Either Err PTerm)
-> (String -> Either ParseError PTerm)
-> String
-> Either Err PTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
syn) IState
st ""

{- | Parses an expression
@
  Expr ::= Pi
@
 -}
expr :: SyntaxInfo -> IdrisParser PTerm
expr :: SyntaxInfo -> IdrisParser PTerm
expr = SyntaxInfo -> IdrisParser PTerm
pi

{- | Parses an expression with possible operator applied
@
  OpExpr ::= {- Expression Parser with Operators based on Expr' -};
@
-}
opExpr :: SyntaxInfo -> IdrisParser PTerm
opExpr :: SyntaxInfo -> IdrisParser PTerm
opExpr syn :: SyntaxInfo
syn = do IState
i <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                IdrisParser PTerm
-> [[Operator
       (StateT IState (WriterT FC (Parsec Void String))) PTerm]]
-> IdrisParser PTerm
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
P.makeExprParser (SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn) ([FixDecl]
-> [[Operator
       (StateT IState (WriterT FC (Parsec Void String))) PTerm]]
table (IState -> [FixDecl]
idris_infixes IState
i))

{- | Parses either an internally defined expression or
    a user-defined one
@
Expr' ::=  "External (User-defined) Syntax"
      |   InternalExpr;
@
 -}
expr' :: SyntaxInfo -> IdrisParser PTerm
expr' :: SyntaxInfo -> IdrisParser PTerm
expr' syn :: SyntaxInfo
syn = IdrisParser PTerm -> IdrisParser PTerm
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser PTerm
externalExpr SyntaxInfo
syn)
            IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
internalExpr SyntaxInfo
syn
            IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "expression"

{- | Parses a user-defined expression -}
externalExpr :: SyntaxInfo -> IdrisParser PTerm
externalExpr :: SyntaxInfo -> IdrisParser PTerm
externalExpr syn :: SyntaxInfo
syn = do IState
i <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                      (expr :: PTerm
expr, outerFC :: FC
outerFC@(FC fn :: String
fn _ _)) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> [Syntax] -> IdrisParser PTerm
extensions SyntaxInfo
syn (SyntaxRules -> [Syntax]
syntaxRulesList (SyntaxRules -> [Syntax]) -> SyntaxRules -> [Syntax]
forall a b. (a -> b) -> a -> b
$ IState -> SyntaxRules
syntax_rules IState
i)
                      PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return ((FC -> FC) -> (FC -> FC) -> PTerm -> PTerm
mapPTermFC (FC -> FC -> FC
fixFC FC
outerFC) (String -> FC -> FC -> FC
fixFCH String
fn FC
outerFC) PTerm
expr)
                   IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "user-defined expression"
  where -- Fix non-highlighting FCs by approximating with the span of the syntax application
        fixFC :: FC -> FC -> FC
fixFC outer :: FC
outer inner :: FC
inner | FC
inner FC -> FC -> Bool
`fcIn` FC
outer = FC
inner
                          | Bool
otherwise          = FC
outer
        -- Fix highlighting FCs by making them useless, to avoid spurious highlights
        fixFCH :: String -> FC -> FC -> FC
fixFCH fn :: String
fn outer :: FC
outer inner :: FC
inner | FC
inner FC -> FC -> Bool
`fcIn` FC
outer = FC
inner
                              | Bool
otherwise          = String -> FC
FileFC String
fn

{- | Parses a simple user-defined expression -}
simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
simpleExternalExpr syn :: SyntaxInfo
syn = do IState
i <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                            SyntaxInfo -> [Syntax] -> IdrisParser PTerm
extensions SyntaxInfo
syn ((Syntax -> Bool) -> [Syntax] -> [Syntax]
forall a. (a -> Bool) -> [a] -> [a]
filter Syntax -> Bool
isSimple (SyntaxRules -> [Syntax]
syntaxRulesList (SyntaxRules -> [Syntax]) -> SyntaxRules -> [Syntax]
forall a b. (a -> b) -> a -> b
$ IState -> SyntaxRules
syntax_rules IState
i))
  where
    isSimple :: Syntax -> Bool
isSimple (Rule (Expr x :: Name
x:xs :: [SSymbol]
xs) _ _) = Bool
False
    isSimple (Rule (SimpleExpr x :: Name
x:xs :: [SSymbol]
xs) _ _) = Bool
False
    isSimple (Rule [Keyword _] _ _) = Bool
True
    isSimple (Rule [Symbol _]  _ _) = Bool
True
    isSimple (Rule (_:xs :: [SSymbol]
xs) _ _) = case [SSymbol] -> SSymbol
forall a. [a] -> a
last [SSymbol]
xs of
        Keyword _ -> Bool
True
        Symbol _  -> Bool
True
        _ -> Bool
False
    isSimple _ = Bool
False

{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
extensions syn :: SyntaxInfo
syn rules :: [Syntax]
rules = SyntaxInfo
-> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm
extension SyntaxInfo
syn [] ((Syntax -> Bool) -> [Syntax] -> [Syntax]
forall a. (a -> Bool) -> [a] -> [a]
filter Syntax -> Bool
isValid [Syntax]
rules)
                       IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "user-defined expression"
  where
    isValid :: Syntax -> Bool
    isValid :: Syntax -> Bool
isValid (Rule _ _ AnySyntax) = Bool
True
    isValid (Rule _ _ PatternSyntax) = SyntaxInfo -> Bool
inPattern SyntaxInfo
syn
    isValid (Rule _ _ TermSyntax) = Bool -> Bool
not (SyntaxInfo -> Bool
inPattern SyntaxInfo
syn)
    isValid (DeclRule _ _) = Bool
False

data SynMatch = SynTm PTerm | SynBind FC Name -- ^ the FC is for highlighting information
  deriving Int -> SynMatch -> ShowS
[SynMatch] -> ShowS
SynMatch -> String
(Int -> SynMatch -> ShowS)
-> (SynMatch -> String) -> ([SynMatch] -> ShowS) -> Show SynMatch
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SynMatch] -> ShowS
$cshowList :: [SynMatch] -> ShowS
show :: SynMatch -> String
$cshow :: SynMatch -> String
showsPrec :: Int -> SynMatch -> ShowS
$cshowsPrec :: Int -> SynMatch -> ShowS
Show

extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm
extension :: SyntaxInfo
-> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm
extension syn :: SyntaxInfo
syn ns :: [Maybe (Name, SynMatch)]
ns rules :: [Syntax]
rules =
  [IdrisParser PTerm] -> IdrisParser PTerm
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice ([IdrisParser PTerm] -> IdrisParser PTerm)
-> [IdrisParser PTerm] -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ (([Syntax] -> IdrisParser PTerm)
 -> [[Syntax]] -> [IdrisParser PTerm])
-> [[Syntax]]
-> ([Syntax] -> IdrisParser PTerm)
-> [IdrisParser PTerm]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ([Syntax] -> IdrisParser PTerm)
-> [[Syntax]] -> [IdrisParser PTerm]
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 PTerm) -> [IdrisParser PTerm])
-> ([Syntax] -> IdrisParser PTerm) -> [IdrisParser PTerm]
forall a b. (a -> b) -> a -> b
$ \rs :: [Syntax]
rs ->
    case [Syntax] -> Syntax
forall a. [a] -> a
head [Syntax]
rs of -- can never be []
      Rule (symb :: SSymbol
symb:_) _ _ -> IdrisParser PTerm -> IdrisParser PTerm
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisParser PTerm -> IdrisParser PTerm)
-> IdrisParser PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
        Maybe (Name, SynMatch)
n <- SSymbol -> IdrisParser (Maybe (Name, SynMatch))
extensionSymbol SSymbol
symb
        SyntaxInfo
-> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm
extension SyntaxInfo
syn (Maybe (Name, SynMatch)
n Maybe (Name, SynMatch)
-> [Maybe (Name, SynMatch)] -> [Maybe (Name, SynMatch)]
forall a. a -> [a] -> [a]
: [Maybe (Name, SynMatch)]
ns) [[SSymbol] -> PTerm -> SynContext -> Syntax
Rule [SSymbol]
ss PTerm
t SynContext
ctx | (Rule (_:ss :: [SSymbol]
ss) t :: PTerm
t ctx :: SynContext
ctx) <- [Syntax]
rs]
      -- If we have more than one Rule in this bucket, our grammar is
      -- nondeterministic.
      Rule [] ptm :: PTerm
ptm _ -> PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> PTerm
flatten ([(Name, SynMatch)] -> PTerm -> PTerm
updateSynMatch ((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) PTerm
ptm))
  where
    ruleGroup :: [a] -> [a] -> Bool
ruleGroup [] [] = Bool
True
    ruleGroup (s1 :: a
s1:_) (s2 :: a
s2:_) = a
s1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
s2
    ruleGroup _ _ = Bool
False

    extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
    extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
extensionSymbol (Keyword n :: 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 (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)
    extensionSymbol (Expr n :: Name
n)       = do PTerm
tm <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                                        Maybe (Name, SynMatch) -> IdrisParser (Maybe (Name, SynMatch))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Name, SynMatch) -> IdrisParser (Maybe (Name, SynMatch)))
-> Maybe (Name, SynMatch) -> IdrisParser (Maybe (Name, SynMatch))
forall a b. (a -> b) -> a -> b
$ (Name, SynMatch) -> Maybe (Name, SynMatch)
forall a. a -> Maybe a
Just (Name
n, PTerm -> SynMatch
SynTm PTerm
tm)
    extensionSymbol (SimpleExpr n :: Name
n) = do PTerm
tm <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
                                        Maybe (Name, SynMatch) -> IdrisParser (Maybe (Name, SynMatch))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Name, SynMatch) -> IdrisParser (Maybe (Name, SynMatch)))
-> Maybe (Name, SynMatch) -> IdrisParser (Maybe (Name, SynMatch))
forall a b. (a -> b) -> a -> b
$ (Name, SynMatch) -> Maybe (Name, SynMatch)
forall a. a -> Maybe a
Just (Name
n, PTerm -> SynMatch
SynTm PTerm
tm)
    extensionSymbol (Binding n :: Name
n)    = do (b :: Name
b, fc :: FC
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
                                        Maybe (Name, SynMatch) -> IdrisParser (Maybe (Name, SynMatch))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Name, SynMatch) -> IdrisParser (Maybe (Name, SynMatch)))
-> Maybe (Name, SynMatch) -> IdrisParser (Maybe (Name, SynMatch))
forall a b. (a -> b) -> a -> b
$ (Name, SynMatch) -> Maybe (Name, SynMatch)
forall a. a -> Maybe a
Just (Name
n, FC -> Name -> SynMatch
SynBind FC
fc Name
b)
    extensionSymbol (Symbol s :: 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 (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)

    flatten :: PTerm -> PTerm -- flatten application
    flatten :: PTerm -> PTerm
flatten (PApp fc :: FC
fc (PApp _ f :: PTerm
f as :: [PArg]
as) bs :: [PArg]
bs) = PTerm -> PTerm
flatten (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f ([PArg]
as [PArg] -> [PArg] -> [PArg]
forall a. [a] -> [a] -> [a]
++ [PArg]
bs))
    flatten t :: PTerm
t = PTerm
t

updateSynMatch :: [(Name, SynMatch)] -> PTerm -> PTerm
updateSynMatch = [(Name, SynMatch)] -> PTerm -> PTerm
update
  where
    updateB :: [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
    updateB :: [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB ns :: [(Name, SynMatch)]
ns (n :: Name
n, fc :: FC
fc) = 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 tfc :: FC
tfc t :: Name
t) -> (Name
t, FC
tfc)
                           _ -> (Name
n, FC
fc)

    update :: [(Name, SynMatch)] -> PTerm -> PTerm
    update :: [(Name, SynMatch)] -> PTerm -> PTerm
update ns :: [(Name, SynMatch)]
ns (PRef fc :: FC
fc hls :: [FC]
hls n :: 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 (SynTm t :: PTerm
t) -> PTerm
t
                                  _ -> FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC]
hls Name
n
    update ns :: [(Name, SynMatch)]
ns (PPatvar fc :: FC
fc n :: Name
n) = (Name -> FC -> PTerm) -> (Name, FC) -> PTerm
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((FC -> Name -> PTerm) -> Name -> FC -> PTerm
forall a b c. (a -> b -> c) -> b -> a -> c
flip FC -> Name -> PTerm
PPatvar) ((Name, FC) -> PTerm) -> (Name, FC) -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
fc)
    update ns :: [(Name, SynMatch)]
ns (PLam fc :: FC
fc n :: Name
n nfc :: FC
nfc ty :: PTerm
ty sc :: PTerm
sc)
      = let (n' :: Name
n', nfc' :: FC
nfc') = [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
nfc)
        in FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc Name
n' FC
nfc' ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
ty) ([(Name, SynMatch)] -> PTerm -> PTerm
update (Name -> [(Name, SynMatch)] -> [(Name, SynMatch)]
forall a. Name -> [(Name, a)] -> [(Name, a)]
dropn Name
n [(Name, SynMatch)]
ns) PTerm
sc)
    update ns :: [(Name, SynMatch)]
ns (PPi p :: Plicity
p n :: Name
n fc :: FC
fc ty :: PTerm
ty sc :: PTerm
sc)
      = let (n' :: Name
n', nfc' :: FC
nfc') = [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
fc)
        in Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([(Name, SynMatch)] -> Plicity -> Plicity
updTacImp [(Name, SynMatch)]
ns Plicity
p) Name
n' FC
nfc'
               ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
ty) ([(Name, SynMatch)] -> PTerm -> PTerm
update (Name -> [(Name, SynMatch)] -> [(Name, SynMatch)]
forall a. Name -> [(Name, a)] -> [(Name, a)]
dropn Name
n [(Name, SynMatch)]
ns) PTerm
sc)
    update ns :: [(Name, SynMatch)]
ns (PLet fc :: FC
fc rc :: RigCount
rc n :: Name
n nfc :: FC
nfc ty :: PTerm
ty val :: PTerm
val sc :: PTerm
sc)
      = let (n' :: Name
n', nfc' :: FC
nfc') = [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
nfc)
        in FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
rc Name
n' FC
nfc' ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
ty)
                ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
val) ([(Name, SynMatch)] -> PTerm -> PTerm
update (Name -> [(Name, SynMatch)] -> [(Name, SynMatch)]
forall a. Name -> [(Name, a)] -> [(Name, a)]
dropn Name
n [(Name, SynMatch)]
ns) PTerm
sc)
    update ns :: [(Name, SynMatch)]
ns (PApp fc :: FC
fc t :: PTerm
t args :: [PArg]
args)
      = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t) ((PArg -> PArg) -> [PArg] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PArg -> PArg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns)) [PArg]
args)
    update ns :: [(Name, SynMatch)]
ns (PAppBind fc :: FC
fc t :: PTerm
t args :: [PArg]
args)
      = FC -> PTerm -> [PArg] -> PTerm
PAppBind FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t) ((PArg -> PArg) -> [PArg] -> [PArg]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> PArg -> PArg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns)) [PArg]
args)
    update ns :: [(Name, SynMatch)]
ns (PMatchApp fc :: FC
fc n :: Name
n) = let (n' :: Name
n', nfc' :: FC
nfc') = [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
fc)
                                 in FC -> Name -> PTerm
PMatchApp FC
nfc' Name
n'
    update ns :: [(Name, SynMatch)]
ns (PIfThenElse fc :: FC
fc c :: PTerm
c t :: PTerm
t f :: PTerm
f)
      = FC -> PTerm -> PTerm -> PTerm -> PTerm
PIfThenElse FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
c) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
f)
    update ns :: [(Name, SynMatch)]
ns (PCase fc :: FC
fc c :: PTerm
c opts :: [(PTerm, PTerm)]
opts)
      = FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
c) (((PTerm, PTerm) -> (PTerm, PTerm))
-> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall a b. (a -> b) -> [a] -> [b]
map ((PTerm -> PTerm) -> (PTerm, PTerm) -> (PTerm, PTerm)
forall t b. (t -> b) -> (t, t) -> (b, b)
pmap ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns)) [(PTerm, PTerm)]
opts)
    update ns :: [(Name, SynMatch)]
ns (PRewrite fc :: FC
fc by :: Maybe Name
by eq :: PTerm
eq tm :: PTerm
tm mty :: Maybe PTerm
mty)
      = FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> PTerm
PRewrite FC
fc Maybe Name
by ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
eq) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
tm) ((PTerm -> PTerm) -> Maybe PTerm -> Maybe PTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns) Maybe PTerm
mty)
    update ns :: [(Name, SynMatch)]
ns (PPair fc :: FC
fc hls :: [FC]
hls p :: PunInfo
p l :: PTerm
l r :: PTerm
r) = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
fc [FC]
hls PunInfo
p ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
l) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
r)
    update ns :: [(Name, SynMatch)]
ns (PDPair fc :: FC
fc hls :: [FC]
hls p :: PunInfo
p l :: PTerm
l t :: PTerm
t r :: PTerm
r)
      = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
fc [FC]
hls PunInfo
p ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
l) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
r)
    update ns :: [(Name, SynMatch)]
ns (PAs fc :: FC
fc n :: Name
n t :: PTerm
t) = FC -> Name -> PTerm -> PTerm
PAs FC
fc ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name, FC) -> Name
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC)) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
    update ns :: [(Name, SynMatch)]
ns (PAlternative ms :: [(Name, Name)]
ms a :: PAltType
a as :: [PTerm]
as) = [(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [(Name, Name)]
ms PAltType
a ((PTerm -> PTerm) -> [PTerm] -> [PTerm]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns) [PTerm]
as)
    update ns :: [(Name, SynMatch)]
ns (PHidden t :: PTerm
t) = PTerm -> PTerm
PHidden ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
    update ns :: [(Name, SynMatch)]
ns (PGoal fc :: FC
fc r :: PTerm
r n :: Name
n sc :: PTerm
sc) = FC -> PTerm -> Name -> PTerm -> PTerm
PGoal FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
r) Name
n ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
sc)
    update ns :: [(Name, SynMatch)]
ns (PDoBlock ds :: [PDo]
ds) = [PDo] -> PTerm
PDoBlock ([PDo] -> PTerm) -> [PDo] -> PTerm
forall a b. (a -> b) -> a -> b
$ (PDo -> PDo) -> [PDo] -> [PDo]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PDo -> PDo
upd [(Name, SynMatch)]
ns) [PDo]
ds
      where upd :: [(Name, SynMatch)] -> PDo -> PDo
            upd :: [(Name, SynMatch)] -> PDo -> PDo
upd ns :: [(Name, SynMatch)]
ns (DoExp fc :: FC
fc t :: PTerm
t) = FC -> PTerm -> PDo
forall t. FC -> t -> PDo' t
DoExp FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
            upd ns :: [(Name, SynMatch)]
ns (DoBind fc :: FC
fc n :: Name
n nfc :: FC
nfc t :: PTerm
t) = FC -> Name -> FC -> PTerm -> PDo
forall t. FC -> Name -> FC -> t -> PDo' t
DoBind FC
fc Name
n FC
nfc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
            upd ns :: [(Name, SynMatch)]
ns (DoLet fc :: FC
fc rc :: RigCount
rc n :: Name
n nfc :: FC
nfc ty :: PTerm
ty t :: PTerm
t) = FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PDo
forall t. FC -> RigCount -> Name -> FC -> t -> t -> PDo' t
DoLet FC
fc RigCount
rc Name
n FC
nfc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
ty) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
            upd ns :: [(Name, SynMatch)]
ns (DoBindP fc :: FC
fc i :: PTerm
i t :: PTerm
t ts :: [(PTerm, PTerm)]
ts)
                    = FC -> PTerm -> PTerm -> [(PTerm, PTerm)] -> PDo
forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoBindP FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
i) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
                                 (((PTerm, PTerm) -> (PTerm, PTerm))
-> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall a b. (a -> b) -> [a] -> [b]
map (\(l :: PTerm
l,r :: PTerm
r) -> ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
l, [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
r)) [(PTerm, PTerm)]
ts)
            upd ns :: [(Name, SynMatch)]
ns (DoLetP fc :: FC
fc i :: PTerm
i t :: PTerm
t ts :: [(PTerm, PTerm)]
ts)
                    = FC -> PTerm -> PTerm -> [(PTerm, PTerm)] -> PDo
forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoLetP FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
i) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
                                (((PTerm, PTerm) -> (PTerm, PTerm))
-> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall a b. (a -> b) -> [a] -> [b]
map (\(l :: PTerm
l,r :: PTerm
r) -> ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
l, [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
r)) [(PTerm, PTerm)]
ts)
            upd ns :: [(Name, SynMatch)]
ns (DoRewrite fc :: FC
fc h :: PTerm
h) = FC -> PTerm -> PDo
forall t. FC -> t -> PDo' t
DoRewrite FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
h)
    update ns :: [(Name, SynMatch)]
ns (PIdiom fc :: FC
fc t :: PTerm
t) = FC -> PTerm -> PTerm
PIdiom FC
fc (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t
    update ns :: [(Name, SynMatch)]
ns (PMetavar fc :: FC
fc n :: Name
n) = (Name -> FC -> PTerm) -> (Name, FC) -> PTerm
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((FC -> Name -> PTerm) -> Name -> FC -> PTerm
forall a b c. (a -> b -> c) -> b -> a -> c
flip FC -> Name -> PTerm
PMetavar) ((Name, FC) -> PTerm) -> (Name, FC) -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
fc)
    update ns :: [(Name, SynMatch)]
ns (PProof tacs :: [PTactic]
tacs) = [PTactic] -> PTerm
PProof ([PTactic] -> PTerm) -> [PTactic] -> PTerm
forall a b. (a -> b) -> a -> b
$ (PTactic -> PTactic) -> [PTactic] -> [PTactic]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns) [PTactic]
tacs
    update ns :: [(Name, SynMatch)]
ns (PTactics tacs :: [PTactic]
tacs) = [PTactic] -> PTerm
PTactics ([PTactic] -> PTerm) -> [PTactic] -> PTerm
forall a b. (a -> b) -> a -> b
$ (PTactic -> PTactic) -> [PTactic] -> [PTactic]
forall a b. (a -> b) -> [a] -> [b]
map ([(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns) [PTactic]
tacs
    update ns :: [(Name, SynMatch)]
ns (PDisamb nsps :: [[Text]]
nsps t :: PTerm
t) = [[Text]] -> PTerm -> PTerm
PDisamb [[Text]]
nsps (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t
    update ns :: [(Name, SynMatch)]
ns (PUnifyLog t :: PTerm
t) = PTerm -> PTerm
PUnifyLog (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t
    update ns :: [(Name, SynMatch)]
ns (PNoImplicits t :: PTerm
t) = PTerm -> PTerm
PNoImplicits (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t
    update ns :: [(Name, SynMatch)]
ns (PQuasiquote tm :: PTerm
tm mty :: Maybe PTerm
mty) = PTerm -> Maybe PTerm -> PTerm
PQuasiquote ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
tm) ((PTerm -> PTerm) -> Maybe PTerm -> Maybe PTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns) Maybe PTerm
mty)
    update ns :: [(Name, SynMatch)]
ns (PUnquote t :: PTerm
t) = PTerm -> PTerm
PUnquote (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t
    update ns :: [(Name, SynMatch)]
ns (PQuoteName n :: Name
n res :: Bool
res fc :: FC
fc) = let (n' :: Name
n', fc' :: FC
fc') = ([(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
fc))
                                      in Name -> Bool -> FC -> PTerm
PQuoteName Name
n' Bool
res FC
fc'
    update ns :: [(Name, SynMatch)]
ns (PRunElab fc :: FC
fc t :: PTerm
t nsp :: [String]
nsp) = FC -> PTerm -> [String] -> PTerm
PRunElab FC
fc ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t) [String]
nsp
    update ns :: [(Name, SynMatch)]
ns (PConstSugar fc :: FC
fc t :: PTerm
t) = FC -> PTerm -> PTerm
PConstSugar FC
fc (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t
    -- PConstSugar probably can't contain anything substitutable, but it's hard to track
    update ns :: [(Name, SynMatch)]
ns t :: PTerm
t = PTerm
t

    updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic
    -- handle all the ones with Names explicitly, then use fmap for the rest with PTerms
    updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic
updTactic ns :: [(Name, SynMatch)]
ns (Intro ns' :: [Name]
ns') = [Name] -> PTactic
forall t. [Name] -> PTactic' t
Intro ([Name] -> PTactic) -> [Name] -> PTactic
forall a b. (a -> b) -> a -> b
$ (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name -> (Name, FC)) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns ((Name, FC) -> (Name, FC))
-> (Name -> (Name, FC)) -> Name -> (Name, FC)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, FC
NoFC)) [Name]
ns'
    updTactic ns :: [(Name, SynMatch)]
ns (Focus n :: Name
n) = Name -> PTactic
forall t. Name -> PTactic' t
Focus (Name -> PTactic) -> ((Name, FC) -> Name) -> (Name, FC) -> PTactic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> PTactic) -> (Name, FC) -> PTactic
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC)
    updTactic ns :: [(Name, SynMatch)]
ns (Refine n :: Name
n bs :: [Bool]
bs) = Name -> [Bool] -> PTactic
forall t. Name -> [Bool] -> PTactic' t
Refine ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name, FC) -> Name
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC)) [Bool]
bs
    updTactic ns :: [(Name, SynMatch)]
ns (Claim n :: Name
n t :: PTerm
t) = Name -> PTerm -> PTactic
forall t. Name -> t -> PTactic' t
Claim ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name, FC) -> Name
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC)) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
    updTactic ns :: [(Name, SynMatch)]
ns (MatchRefine n :: Name
n) = Name -> PTactic
forall t. Name -> PTactic' t
MatchRefine ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name, FC) -> Name
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC))
    updTactic ns :: [(Name, SynMatch)]
ns (LetTac n :: Name
n t :: PTerm
t) = Name -> PTerm -> PTactic
forall t. Name -> t -> PTactic' t
LetTac ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name, FC) -> Name
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC)) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
t)
    updTactic ns :: [(Name, SynMatch)]
ns (LetTacTy n :: Name
n ty :: PTerm
ty tm :: PTerm
tm) = Name -> PTerm -> PTerm -> PTactic
forall t. Name -> t -> t -> PTactic' t
LetTacTy ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name, FC) -> Name
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC)) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
ty) ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
tm)
    updTactic ns :: [(Name, SynMatch)]
ns (ProofSearch rec :: Bool
rec prover :: Bool
prover depth :: Int
depth top :: Maybe Name
top psns :: [Name]
psns hints :: [Name]
hints) = Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic
forall t.
Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic' t
ProofSearch Bool
rec Bool
prover Int
depth
      ((Name -> Name) -> Maybe Name -> Maybe Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name -> (Name, FC)) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns ((Name, FC) -> (Name, FC))
-> (Name -> (Name, FC)) -> Name -> (Name, FC)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, FC
NoFC)) Maybe Name
top) ((Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name -> (Name, FC)) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns ((Name, FC) -> (Name, FC))
-> (Name -> (Name, FC)) -> Name -> (Name, FC)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, FC
NoFC)) [Name]
psns) ((Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> Name) -> (Name -> (Name, FC)) -> Name -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns ((Name, FC) -> (Name, FC))
-> (Name -> (Name, FC)) -> Name -> (Name, FC)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (, FC
NoFC)) [Name]
hints)
    updTactic ns :: [(Name, SynMatch)]
ns (Try l :: PTactic
l r :: PTactic
r) = PTactic -> PTactic -> PTactic
forall t. PTactic' t -> PTactic' t -> PTactic' t
Try ([(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns PTactic
l) ([(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns PTactic
r)
    updTactic ns :: [(Name, SynMatch)]
ns (TSeq l :: PTactic
l r :: PTactic
r) = PTactic -> PTactic -> PTactic
forall t. PTactic' t -> PTactic' t -> PTactic' t
TSeq ([(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns PTactic
l) ([(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns PTactic
r)
    updTactic ns :: [(Name, SynMatch)]
ns (GoalType s :: String
s tac :: PTactic
tac) = String -> PTactic -> PTactic
forall t. String -> PTactic' t -> PTactic' t
GoalType String
s (PTactic -> PTactic) -> PTactic -> PTactic
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> PTactic -> PTactic
updTactic [(Name, SynMatch)]
ns PTactic
tac
    updTactic ns :: [(Name, SynMatch)]
ns (TDocStr (Left n :: Name
n)) = Either Name Const -> PTactic
forall t. Either Name Const -> PTactic' t
TDocStr (Either Name Const -> PTactic)
-> ((Name, FC) -> Either Name Const) -> (Name, FC) -> PTactic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Either Name Const
forall a b. a -> Either a b
Left (Name -> Either Name Const)
-> ((Name, FC) -> Name) -> (Name, FC) -> Either Name Const
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, FC) -> Name
forall a b. (a, b) -> a
fst ((Name, FC) -> PTactic) -> (Name, FC) -> PTactic
forall a b. (a -> b) -> a -> b
$ [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)
updateB [(Name, SynMatch)]
ns (Name
n, FC
NoFC)
    updTactic ns :: [(Name, SynMatch)]
ns t :: PTactic
t = (PTerm -> PTerm) -> PTactic -> PTactic
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns) PTactic
t

    updTacImp :: [(Name, SynMatch)] -> Plicity -> Plicity
updTacImp ns :: [(Name, SynMatch)]
ns (TacImp o :: [ArgOpt]
o st :: Static
st scr :: PTerm
scr r :: RigCount
r) = [ArgOpt] -> Static -> PTerm -> RigCount -> Plicity
TacImp [ArgOpt]
o Static
st ([(Name, SynMatch)] -> PTerm -> PTerm
update [(Name, SynMatch)]
ns PTerm
scr) RigCount
r
    updTacImp _  x :: Plicity
x                   = Plicity
x

    dropn :: Name -> [(Name, a)] -> [(Name, a)]
    dropn :: Name -> [(Name, a)] -> [(Name, a)]
dropn n :: Name
n [] = []
    dropn n :: Name
n ((x :: Name
x,t :: a
t) : xs :: [(Name, a)]
xs) | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = [(Name, a)]
xs
                         | Bool
otherwise = (Name
x,a
t)(Name, a) -> [(Name, a)] -> [(Name, a)]
forall a. a -> [a] -> [a]
:Name -> [(Name, a)] -> [(Name, a)]
forall a. Name -> [(Name, a)] -> [(Name, a)]
dropn Name
n [(Name, a)]
xs


{- | Parses a (normal) built-in expression
@
InternalExpr ::=
    UnifyLog
  | RecordType
  | SimpleExpr
  | Lambda
  | QuoteGoal
  | Let
  | If
  | RewriteTerm
  | CaseExpr
  | DoBlock
  | App
  ;
@
-}
internalExpr :: SyntaxInfo -> IdrisParser PTerm
internalExpr :: SyntaxInfo -> IdrisParser PTerm
internalExpr syn :: SyntaxInfo
syn =
         SyntaxInfo -> IdrisParser PTerm
unifyLog SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
runElab SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
disamb SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
noImplicits SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
recordType SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
if_ SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
lambda SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
quoteGoal SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
let_ SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
rewriteTerm SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
doBlock SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
caseExpr SyntaxInfo
syn
     IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
app SyntaxInfo
syn
     IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "expression"

{- | Parses the "impossible" keyword
@
Impossible ::= 'impossible'
@
-}
impossible :: IdrisParser PTerm
impossible :: IdrisParser PTerm
impossible = PTerm
PImpossible PTerm
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser PTerm
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 "impossible"

{- | Parses a case expression
@
CaseExpr ::=
  'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;
@
-}
caseExpr :: SyntaxInfo -> IdrisParser PTerm
caseExpr :: SyntaxInfo -> IdrisParser PTerm
caseExpr syn :: SyntaxInfo
syn = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "case"
                  (scr :: PTerm
scr, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                  String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "of"
                  [(PTerm, PTerm)]
opts <- IdrisParser (PTerm, PTerm) -> IdrisParser [(PTerm, PTerm)]
forall a. IdrisParser a -> IdrisParser [a]
indentedBlock1 (SyntaxInfo -> IdrisParser (PTerm, PTerm)
caseOption SyntaxInfo
syn)
                  PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc PTerm
scr [(PTerm, PTerm)]
opts)
               IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "case expression"

{- | Parses a case in a case expression
@
CaseOption ::=
  Expr (Impossible | '=>' Expr) Terminator
  ;
@
-}
caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
caseOption syn :: SyntaxInfo
syn = do PTerm
lhs <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
disallowImp (SyntaxInfo
syn { inPattern :: Bool
inPattern = Bool
True }))
                    PTerm
r <- IdrisParser PTerm
impossible IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
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 ()
symbol "=>" StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                    (PTerm, PTerm) -> IdrisParser (PTerm, PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
lhs, PTerm
r)
                 IdrisParser (PTerm, PTerm) -> String -> IdrisParser (PTerm, PTerm)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "case option"

warnTacticDeprecation :: FC -> IdrisParser ()
warnTacticDeprecation :: FC -> StateT IState (WriterT FC (Parsec Void String)) ()
warnTacticDeprecation fc :: FC
fc =
 FC
-> Maybe Opt
-> Err
-> StateT IState (WriterT FC (Parsec Void String)) ()
parserWarning FC
fc (Opt -> Maybe Opt
forall a. a -> Maybe a
Just Opt
NoOldTacticDeprecationWarnings) (String -> Err
forall t. String -> Err' t
Msg "This style of tactic proof is deprecated. See %runElab for the replacement.")

{- | Parses a proof block
@
ProofExpr ::=
  'proof' OpenBlock Tactic'* CloseBlock
  ;
@
-}
proofExpr :: SyntaxInfo -> IdrisParser PTerm
proofExpr :: SyntaxInfo -> IdrisParser PTerm
proofExpr syn :: SyntaxInfo
syn = do FC
kw <- 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 "proof"
                   [PTactic]
ts <- IdrisParser PTactic -> IdrisParser [PTactic]
forall a. IdrisParser a -> IdrisParser [a]
indentedBlock1 (SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn)
                   FC -> StateT IState (WriterT FC (Parsec Void String)) ()
warnTacticDeprecation FC
kw
                   PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ [PTactic] -> PTerm
PProof [PTactic]
ts
                IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "proof block"

{- | Parses a tactics block
@
TacticsExpr :=
  'tactics' OpenBlock Tactic'* CloseBlock
;
@
-}
tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
tacticsExpr syn :: SyntaxInfo
syn = do FC
kw <- 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 "tactics"
                     [PTactic]
ts <- IdrisParser PTactic -> IdrisParser [PTactic]
forall a. IdrisParser a -> IdrisParser [a]
indentedBlock1 (SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn)
                     FC -> StateT IState (WriterT FC (Parsec Void String)) ()
warnTacticDeprecation FC
kw
                     PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ [PTactic] -> PTerm
PTactics [PTactic]
ts
                  IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "tactics block"

{- | Parses a simple expression
@
SimpleExpr ::=
    {- External (User-defined) Simple Expression -}
  | '?' Name
  | % 'implementation'
  | 'Refl' ('{' Expr '}')?
  | ProofExpr
  | TacticsExpr
  | FnName
  | Idiom
  | List
  | Alt
  | Bracketed
  | Constant
  | Type
  | 'Void'
  | Quasiquote
  | NameQuote
  | Unquote
  | '_'
  ;
@
-}
simpleExpr :: SyntaxInfo -> IdrisParser PTerm
simpleExpr :: SyntaxInfo -> IdrisParser PTerm
simpleExpr syn :: SyntaxInfo
syn =
            IdrisParser PTerm -> IdrisParser PTerm
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser PTerm
simpleExternalExpr SyntaxInfo
syn)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do (x :: Name
x, FC f :: String
f (l :: Int
l, c :: Int
c) end :: (Int, Int)
end) <- StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
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 '?' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC)
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
name)
               PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Name -> PTerm
PMetavar (String -> (Int, Int) -> (Int, Int) -> FC
FC String
f (Int
l, Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) (Int, Int)
end) Name
x)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
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 '%'; FC
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 => String -> m ()
reserved "implementation"; PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm
PResolveTC FC
fc)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
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 '%'; FC
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 => String -> m ()
reserved "instance"
               FC
-> Maybe Opt
-> Err
-> StateT IState (WriterT FC (Parsec Void String)) ()
parserWarning FC
fc Maybe Opt
forall a. Maybe a
Nothing (Err -> StateT IState (WriterT FC (Parsec Void String)) ())
-> Err -> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> Err
forall t. String -> Err' t
Msg "The use of %instance is deprecated, use %implementation instead."
               PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm
PResolveTC FC
fc)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
proofExpr SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
tacticsExpr SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser PTerm -> IdrisParser PTerm
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do FC
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 (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved "Type*"); PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ FC -> Universe -> PTerm
PUniverse FC
fc Universe
AllTypes)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do FC
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 => String -> m ()
reserved "AnyType"; PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ FC -> Universe -> PTerm
PUniverse FC
fc Universe
AllTypes
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FC -> PTerm
PType (FC -> PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) FC
-> IdrisParser PTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved "Type")
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do FC
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 => String -> m ()
reserved "UniqueType"; PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ FC -> Universe -> PTerm
PUniverse FC
fc Universe
UniqueType
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do FC
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 => String -> m ()
reserved "NullType"; PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ FC -> Universe -> PTerm
PUniverse FC
fc Universe
NullType
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do (c :: Const
c, cfc :: FC
cfc) <- StateT IState (WriterT FC (Parsec Void String)) Const
-> StateT IState (WriterT FC (Parsec Void String)) (Const, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent StateT IState (WriterT FC (Parsec Void String)) Const
forall (m :: * -> *). Parsing m => m Const
constant
               PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (SyntaxInfo -> FC -> PTerm -> PTerm
modifyConst SyntaxInfo
syn FC
cfc (FC -> Const -> PTerm
PConstant FC
cfc Const
c))
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
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 "'"; (str :: Name
str, fc :: FC
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
               PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN "Symbol_"))
                          [PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> Const -> PTerm
PConstant FC
NoFC (String -> Const
Str (Name -> String
forall a. Show a => a -> String
show Name
str)))])
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do (x :: Name
x, fc :: FC
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
fnName
               if SyntaxInfo -> Bool
inPattern SyntaxInfo
syn
                  then PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC
fc] Name
x)
                                (do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp "@"
                                    (s :: PTerm
s, fcIn :: FC
fcIn) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
                                    PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Name -> PTerm -> PTerm
PAs FC
fcIn Name
x PTerm
s))
                  else PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC
fc] Name
x)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
idiom SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
listExpr SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
alt SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
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 ()
reservedOp "!"
               (s :: PTerm
s, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
               PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> [PArg] -> PTerm
PAppBind FC
fc PTerm
s [])
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
bracketed (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
quasiquote SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
namequote SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
unquote SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
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 '_'; PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
Placeholder
        IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "expression"

{- |Parses an expression in parentheses
@
Bracketed ::= '(' Bracketed'
@
 -}
bracketed :: SyntaxInfo -> IdrisParser PTerm
bracketed :: SyntaxInfo -> IdrisParser PTerm
bracketed syn :: SyntaxInfo
syn = do (FC fn :: String
fn (sl :: Int
sl, sc :: Int
sc) _) <- StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '(') StateT IState (WriterT FC (Parsec Void String)) FC
-> String -> StateT IState (WriterT FC (Parsec Void String)) FC
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "parenthesized expression"
                   FC -> SyntaxInfo -> IdrisParser PTerm
bracketed' (String -> (Int, Int) -> (Int, Int) -> FC
FC String
fn (Int
sl, Int
sc) (Int
sl, Int
scInt -> Int -> Int
forall a. Num a => a -> a -> a
+1)) (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
True })

{- |Parses the rest of an expression in braces
@
Bracketed' ::=
  ')'
  | Expr ')'
  | ExprList ')'
  | DependentPair ')'
  | Operator Expr ')'
  | Expr Operator ')'
  ;
@
-}
bracketed' :: FC -> SyntaxInfo -> IdrisParser PTerm
bracketed' :: FC -> SyntaxInfo -> IdrisParser PTerm
bracketed' open :: FC
open syn :: SyntaxInfo
syn =
            do FC
fc <- StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (FC -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). MonadWriter FC m => FC -> m ()
addExtent FC
open StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ')')
               PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ FC -> PunInfo -> PTerm
PTrue FC
fc PunInfo
TypeOrTerm
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser PTerm -> IdrisParser PTerm
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (PunInfo
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> FC
-> SyntaxInfo
-> IdrisParser PTerm
dependentPair PunInfo
TypeOrTerm [] FC
open SyntaxInfo
syn)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser PTerm -> IdrisParser PTerm
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (opName :: Name
opName, fc :: FC
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
operatorName
                      Name -> StateT IState (WriterT FC (Parsec Void String)) ()
guardNotPrefix Name
opName

                      PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                      Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ')'
                      PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> String -> Name
sMN 1000 "ARG") FC
NoFC PTerm
Placeholder
                        (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
opName) [PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> String -> Name
sMN 1000 "ARG")),
                                                      PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
e]))
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser PTerm -> IdrisParser PTerm
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn IdrisParser PTerm
-> (PTerm -> IdrisParser PTerm) -> IdrisParser PTerm
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \l :: PTerm
l ->
                     IdrisParser PTerm -> IdrisParser PTerm
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (opName :: Name
opName, fc :: FC
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
operatorName
                               Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ')'
                               PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> String -> Name
sMN 1000 "ARG") FC
NoFC PTerm
Placeholder
                                 (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
opName) [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
l,
                                                               PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> String -> Name
sMN 1000 "ARG"))]))
                 IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
bracketedExpr SyntaxInfo
syn FC
open PTerm
l)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do PTerm
l <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
allowConstr SyntaxInfo
syn)
               SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
bracketedExpr (SyntaxInfo -> SyntaxInfo
allowConstr SyntaxInfo
syn) FC
open PTerm
l
  where
    justPrefix                          :: FixDecl -> Maybe Name
    justPrefix :: FixDecl -> Maybe Name
justPrefix (Fix (PrefixN _) opName :: String
opName) = Name -> Maybe Name
forall a. a -> Maybe a
Just (String -> Name
sUN String
opName)
    justPrefix _                        = Maybe Name
forall a. Maybe a
Nothing

    guardNotPrefix        :: Name -> IdrisParser ()
    guardNotPrefix :: Name -> StateT IState (WriterT FC (Parsec Void String)) ()
guardNotPrefix opName :: Name
opName = do
      Bool -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> StateT IState (WriterT FC (Parsec Void String)) ())
-> Bool -> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ Name
opName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= String -> Name
sUN "-"
      Bool -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> StateT IState (WriterT FC (Parsec Void String)) ())
-> Bool -> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ Name
opName Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= String -> Name
sUN "!"

      [FixDecl]
ops <- IState -> [FixDecl]
idris_infixes (IState -> [FixDecl])
-> StateT IState (WriterT FC (Parsec Void String)) IState
-> StateT IState (WriterT FC (Parsec Void String)) [FixDecl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
      Bool -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> StateT IState (WriterT FC (Parsec Void String)) ())
-> ([FixDecl] -> Bool)
-> [FixDecl]
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Bool
not (Bool -> Bool) -> ([FixDecl] -> Bool) -> [FixDecl] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name
opName Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) ([Name] -> Bool) -> ([FixDecl] -> [Name]) -> [FixDecl] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FixDecl -> Maybe Name) -> [FixDecl] -> [Name]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe FixDecl -> Maybe Name
justPrefix ([FixDecl] -> StateT IState (WriterT FC (Parsec Void String)) ())
-> [FixDecl] -> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ [FixDecl]
ops

{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}
dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm
dependentPair :: PunInfo
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> FC
-> SyntaxInfo
-> IdrisParser PTerm
dependentPair pun :: PunInfo
pun prev :: [(PTerm, Maybe (FC, PTerm), FC)]
prev openFC :: FC
openFC syn :: SyntaxInfo
syn =
  if [(PTerm, Maybe (FC, PTerm), FC)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(PTerm, Maybe (FC, PTerm), FC)]
prev then
      IdrisParser PTerm
nametypePart IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser PTerm
namePart
  else
    case PunInfo
pun of
      IsType -> IdrisParser PTerm
nametypePart IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser PTerm
namePart IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> IdrisParser PTerm
exprPart Bool
True
      IsTerm -> Bool -> IdrisParser PTerm
exprPart Bool
False
      TypeOrTerm -> IdrisParser PTerm
nametypePart IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser PTerm
namePart IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> IdrisParser PTerm
exprPart Bool
False
  where nametypePart :: IdrisParser PTerm
nametypePart = do
          (ln :: Name
ln, lnfc :: FC
lnfc, colonFC :: FC
colonFC) <- StateT IState (WriterT FC (Parsec Void String)) (Name, FC, FC)
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC, FC)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (StateT IState (WriterT FC (Parsec Void String)) (Name, FC, FC)
 -> StateT IState (WriterT FC (Parsec Void String)) (Name, FC, FC))
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC, FC)
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC, FC)
forall a b. (a -> b) -> a -> b
$ do
            (ln :: Name
ln, lnfc :: FC
lnfc) <- 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
            FC
colonFC <- StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ':')
            (Name, FC, FC)
-> StateT IState (WriterT FC (Parsec Void String)) (Name, FC, FC)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
ln, FC
lnfc, FC
colonFC)
          PTerm
lty <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
          FC
starsFC <- 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 => String -> m ()
reservedOp "**"
          PunInfo
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> FC
-> SyntaxInfo
-> IdrisParser PTerm
dependentPair PunInfo
IsType ((FC -> [FC] -> Name -> PTerm
PRef FC
lnfc [] Name
ln, (FC, PTerm) -> Maybe (FC, PTerm)
forall a. a -> Maybe a
Just (FC
colonFC, PTerm
lty), FC
starsFC)(PTerm, Maybe (FC, PTerm), FC)
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> [(PTerm, Maybe (FC, PTerm), FC)]
forall a. a -> [a] -> [a]
:[(PTerm, Maybe (FC, PTerm), FC)]
prev) FC
openFC SyntaxInfo
syn
        namePart :: IdrisParser PTerm
namePart = IdrisParser PTerm -> IdrisParser PTerm
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisParser PTerm -> IdrisParser PTerm)
-> IdrisParser PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
          (ln :: Name
ln, lnfc :: FC
lnfc) <- 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
          FC
starsFC <- 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 => String -> m ()
reservedOp "**"
          PunInfo
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> FC
-> SyntaxInfo
-> IdrisParser PTerm
dependentPair PunInfo
pun ((FC -> [FC] -> Name -> PTerm
PRef FC
lnfc [] Name
ln, Maybe (FC, PTerm)
forall a. Maybe a
Nothing, FC
starsFC)(PTerm, Maybe (FC, PTerm), FC)
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> [(PTerm, Maybe (FC, PTerm), FC)]
forall a. a -> [a] -> [a]
:[(PTerm, Maybe (FC, PTerm), FC)]
prev) FC
openFC SyntaxInfo
syn
        exprPart :: Bool -> IdrisParser PTerm
exprPart isEnd :: Bool
isEnd = do
          PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
          Either FC FC
sepFCE <-
            let stars :: StateT IState (WriterT FC (Parsec Void String)) (Either FC b)
stars = (FC -> Either FC b
forall a b. a -> Either a b
Left (FC -> Either FC b)
-> StateT IState (WriterT FC (Parsec Void String)) FC
-> StateT IState (WriterT FC (Parsec Void String)) (Either FC b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp "**"))
                ending :: StateT IState (WriterT FC (Parsec Void String)) (Either a FC)
ending = (FC -> Either a FC
forall a b. b -> Either a b
Right (FC -> Either a FC)
-> StateT IState (WriterT FC (Parsec Void String)) FC
-> StateT IState (WriterT FC (Parsec Void String)) (Either a FC)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ')'))
            in if Bool
isEnd then StateT IState (WriterT FC (Parsec Void String)) (Either FC FC)
forall a.
StateT IState (WriterT FC (Parsec Void String)) (Either a FC)
ending else StateT IState (WriterT FC (Parsec Void String)) (Either FC FC)
forall b.
StateT IState (WriterT FC (Parsec Void String)) (Either FC b)
stars StateT IState (WriterT FC (Parsec Void String)) (Either FC FC)
-> StateT IState (WriterT FC (Parsec Void String)) (Either FC FC)
-> StateT IState (WriterT FC (Parsec Void String)) (Either FC FC)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) (Either FC FC)
forall a.
StateT IState (WriterT FC (Parsec Void String)) (Either a FC)
ending
          case Either FC FC
sepFCE of
            Left starsFC :: FC
starsFC -> PunInfo
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> FC
-> SyntaxInfo
-> IdrisParser PTerm
dependentPair PunInfo
IsTerm ((PTerm
e, Maybe (FC, PTerm)
forall a. Maybe a
Nothing, FC
starsFC)(PTerm, Maybe (FC, PTerm), FC)
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> [(PTerm, Maybe (FC, PTerm), FC)]
forall a. a -> [a] -> [a]
:[(PTerm, Maybe (FC, PTerm), FC)]
prev) FC
openFC SyntaxInfo
syn
            Right closeFC :: FC
closeFC ->
              PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PunInfo
-> FC -> FC -> [(PTerm, Maybe (FC, PTerm), FC)] -> PTerm -> PTerm
mkPDPairs PunInfo
pun FC
openFC FC
closeFC ([(PTerm, Maybe (FC, PTerm), FC)]
-> [(PTerm, Maybe (FC, PTerm), FC)]
forall a. [a] -> [a]
reverse [(PTerm, Maybe (FC, PTerm), FC)]
prev) PTerm
e)
        mkPDPairs :: PunInfo
-> FC -> FC -> [(PTerm, Maybe (FC, PTerm), FC)] -> PTerm -> PTerm
mkPDPairs pun :: PunInfo
pun openFC :: FC
openFC closeFC :: FC
closeFC ((e :: PTerm
e, cfclty :: Maybe (FC, PTerm)
cfclty, starsFC :: FC
starsFC):bnds :: [(PTerm, Maybe (FC, PTerm), FC)]
bnds) r :: PTerm
r =
              (FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
openFC ([FC
openFC] [FC] -> [FC] -> [FC]
forall a. [a] -> [a] -> [a]
++ [FC] -> ((FC, PTerm) -> [FC]) -> Maybe (FC, PTerm) -> [FC]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((FC -> [FC] -> [FC]
forall a. a -> [a] -> [a]
: []) (FC -> [FC]) -> ((FC, PTerm) -> FC) -> (FC, PTerm) -> [FC]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FC, PTerm) -> FC
forall a b. (a, b) -> a
fst) Maybe (FC, PTerm)
cfclty [FC] -> [FC] -> [FC]
forall a. [a] -> [a] -> [a]
++ [FC
starsFC, FC
closeFC] [FC] -> [FC] -> [FC]
forall a. [a] -> [a] -> [a]
++ ((PTerm, Maybe (FC, PTerm), FC) -> [FC])
-> [(PTerm, Maybe (FC, PTerm), FC)] -> [FC]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
(=<<) (\(_,cfclty :: Maybe (FC, PTerm)
cfclty,sfc :: FC
sfc) -> [FC] -> ((FC, PTerm) -> [FC]) -> Maybe (FC, PTerm) -> [FC]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((FC -> [FC] -> [FC]
forall a. a -> [a] -> [a]
: []) (FC -> [FC]) -> ((FC, PTerm) -> FC) -> (FC, PTerm) -> [FC]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FC, PTerm) -> FC
forall a b. (a, b) -> a
fst) Maybe (FC, PTerm)
cfclty [FC] -> [FC] -> [FC]
forall a. [a] -> [a] -> [a]
++ [FC
sfc]) [(PTerm, Maybe (FC, PTerm), FC)]
bnds)
                               PunInfo
pun PTerm
e (PTerm -> ((FC, PTerm) -> PTerm) -> Maybe (FC, PTerm) -> PTerm
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PTerm
Placeholder (FC, PTerm) -> PTerm
forall a b. (a, b) -> b
snd Maybe (FC, PTerm)
cfclty) (PunInfo -> FC -> [(PTerm, Maybe (FC, PTerm), FC)] -> PTerm -> PTerm
forall a.
PunInfo -> FC -> [(PTerm, Maybe (a, PTerm), FC)] -> PTerm -> PTerm
mergePDPairs PunInfo
pun FC
starsFC [(PTerm, Maybe (FC, PTerm), FC)]
bnds PTerm
r))
        mergePDPairs :: PunInfo -> FC -> [(PTerm, Maybe (a, PTerm), FC)] -> PTerm -> PTerm
mergePDPairs pun :: PunInfo
pun starsFC' :: FC
starsFC' [] r :: PTerm
r = PTerm
r
        mergePDPairs pun :: PunInfo
pun starsFC' :: FC
starsFC' ((e :: PTerm
e, cfclty :: Maybe (a, PTerm)
cfclty, starsFC :: FC
starsFC):bnds :: [(PTerm, Maybe (a, PTerm), FC)]
bnds) r :: PTerm
r =
           FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm -> PTerm
PDPair FC
starsFC' [] PunInfo
pun PTerm
e (PTerm -> ((a, PTerm) -> PTerm) -> Maybe (a, PTerm) -> PTerm
forall b a. b -> (a -> b) -> Maybe a -> b
maybe PTerm
Placeholder (a, PTerm) -> PTerm
forall a b. (a, b) -> b
snd Maybe (a, PTerm)
cfclty) (PunInfo -> FC -> [(PTerm, Maybe (a, PTerm), FC)] -> PTerm -> PTerm
mergePDPairs PunInfo
pun FC
starsFC [(PTerm, Maybe (a, PTerm), FC)]
bnds PTerm
r)

-- | Parse the contents of parentheses, after an expression has been parsed.
bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm
bracketedExpr syn :: SyntaxInfo
syn openParenFC :: FC
openParenFC e :: PTerm
e =
             do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ')'; PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
e
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  do [(PTerm, FC)]
exprs <- StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
-> StateT IState (WriterT FC (Parsec Void String)) [(PTerm, FC)]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some (do FC
comma <- StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ',')
                                  PTerm
r <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                                  (PTerm, FC)
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
r, FC
comma))
                FC
closeParenFC <- StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ')')
                let hilite :: [FC]
hilite = [FC
openParenFC, FC
closeParenFC] [FC] -> [FC] -> [FC]
forall a. [a] -> [a] -> [a]
++ ((PTerm, FC) -> FC) -> [(PTerm, FC)] -> [FC]
forall a b. (a -> b) -> [a] -> [b]
map (PTerm, FC) -> FC
forall a b. (a, b) -> b
snd [(PTerm, FC)]
exprs
                PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
openParenFC [FC]
hilite PunInfo
TypeOrTerm PTerm
e ([(PTerm, FC)] -> PTerm
mergePairs [(PTerm, FC)]
exprs)
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  do FC
starsFC <- 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 => String -> m ()
reservedOp "**"
                PunInfo
-> [(PTerm, Maybe (FC, PTerm), FC)]
-> FC
-> SyntaxInfo
-> IdrisParser PTerm
dependentPair PunInfo
IsTerm [(PTerm
e, Maybe (FC, PTerm)
forall a. Maybe a
Nothing, FC
starsFC)] FC
openParenFC SyntaxInfo
syn
        IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "end of bracketed expression"
  where mergePairs :: [(PTerm, FC)] -> PTerm
        mergePairs :: [(PTerm, FC)] -> PTerm
mergePairs [(t :: PTerm
t, fc :: FC
fc)]    = PTerm
t
        mergePairs ((t :: PTerm
t, fc :: FC
fc):rs :: [(PTerm, FC)]
rs) = FC -> [FC] -> PunInfo -> PTerm -> PTerm -> PTerm
PPair FC
fc [] PunInfo
TypeOrTerm PTerm
t ([(PTerm, FC)] -> PTerm
mergePairs [(PTerm, FC)]
rs)

-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
-- big integer, otherwise try fromInteger and the constants as alternatives.
-- a better solution would be to fix fromInteger to work with Integer, as the
-- name suggests, rather than Int
{-| Finds optimal type for integer constant -}
modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
modifyConst syn :: SyntaxInfo
syn fc :: FC
fc (PConstant inFC :: FC
inFC (BI x :: Integer
x))
    | Bool -> Bool
not (SyntaxInfo -> Bool
inPattern SyntaxInfo
syn)
        = FC -> PTerm -> PTerm
PConstSugar FC
inFC (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ -- wrap in original span for highlighting
            [(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [] PAltType
FirstSuccess
              (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN "fromInteger")) [PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> Const -> PTerm
PConstant FC
NoFC (Integer -> Const
BI (Integer -> Integer
forall a. Num a => Integer -> a
fromInteger Integer
x)))]
              PTerm -> [PTerm] -> [PTerm]
forall a. a -> [a] -> [a]
: [PTerm]
consts)
    | Bool
otherwise = FC -> PTerm -> PTerm
PConstSugar FC
inFC (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$
                    [(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [] PAltType
FirstSuccess [PTerm]
consts
    where
      consts :: [PTerm]
consts = [ FC -> Const -> PTerm
PConstant FC
inFC (Integer -> Const
BI Integer
x)
               , FC -> Const -> PTerm
PConstant FC
inFC (Int -> Const
I (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
x))
               , FC -> Const -> PTerm
PConstant FC
inFC (Word8 -> Const
B8 (Integer -> Word8
forall a. Num a => Integer -> a
fromInteger Integer
x))
               , FC -> Const -> PTerm
PConstant FC
inFC (Word16 -> Const
B16 (Integer -> Word16
forall a. Num a => Integer -> a
fromInteger Integer
x))
               , FC -> Const -> PTerm
PConstant FC
inFC (Word32 -> Const
B32 (Integer -> Word32
forall a. Num a => Integer -> a
fromInteger Integer
x))
               , FC -> Const -> PTerm
PConstant FC
inFC (Word64 -> Const
B64 (Integer -> Word64
forall a. Num a => Integer -> a
fromInteger Integer
x))
               ]
modifyConst syn :: SyntaxInfo
syn fc :: FC
fc x :: PTerm
x = PTerm
x

{- | Parses an alternative expression
@
  Alt ::= '(|' Expr_List '|)';

  Expr_List ::=
    Expr'
    | Expr' ',' Expr_List
  ;
@
-}
alt :: SyntaxInfo -> IdrisParser PTerm
alt :: SyntaxInfo -> IdrisParser PTerm
alt syn :: SyntaxInfo
syn = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "(|"; [PTerm]
alts <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) [PTerm]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser PTerm
expr' (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })) (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ','); String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "|)"
             PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Name)] -> PAltType -> [PTerm] -> PTerm
PAlternative [] PAltType
FirstSuccess [PTerm]
alts)

{- | Parses a possibly hidden simple expression
@
HSimpleExpr ::=
  '.' SimpleExpr
  | SimpleExpr
  ;
@
-}
hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
hsimpleExpr syn :: SyntaxInfo
syn =
  do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '.'
     PTerm
e <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
     PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ PTerm -> PTerm
PHidden PTerm
e
  IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
  IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "expression"

{- | Parses a unification log expression
UnifyLog ::=
  '%' 'unifyLog' SimpleExpr
  ;
-}
unifyLog :: SyntaxInfo -> IdrisParser PTerm
unifyLog :: SyntaxInfo -> IdrisParser PTerm
unifyLog syn :: SyntaxInfo
syn = do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ 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 (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
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 "unifyLog"
                  PTerm -> PTerm
PUnifyLog (PTerm -> PTerm) -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
               IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "unification log expression"

{- | Parses a new-style tactics expression
RunTactics ::=
  '%' 'runElab' SimpleExpr
  ;
-}
runElab :: SyntaxInfo -> IdrisParser PTerm
runElab :: SyntaxInfo -> IdrisParser PTerm
runElab syn :: SyntaxInfo
syn = do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ 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 (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
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 "runElab"
                 (tm :: PTerm
tm, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
                 PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ FC -> PTerm -> [String] -> PTerm
PRunElab FC
fc PTerm
tm (SyntaxInfo -> [String]
syn_namespace SyntaxInfo
syn)
              IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "new-style tactics expression"

{- | Parses a disambiguation expression
Disamb ::=
  'with' NameList Expr
  ;
-}
disamb :: SyntaxInfo -> IdrisParser PTerm
disamb :: SyntaxInfo -> IdrisParser PTerm
disamb syn :: SyntaxInfo
syn = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "with"
                [Name]
ns <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) [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 ',')
                PTerm
tm <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
                PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return ([[Text]] -> PTerm -> PTerm
PDisamb ((Name -> [Text]) -> [Name] -> [[Text]]
forall a b. (a -> b) -> [a] -> [b]
map Name -> [Text]
tons [Name]
ns) PTerm
tm)
               IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "namespace disambiguation expression"
  where tons :: Name -> [Text]
tons (NS n :: Name
n s :: [Text]
s) = String -> Text
txt (Name -> String
forall a. Show a => a -> String
show Name
n) Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
s
        tons n :: Name
n = [String -> Text
txt (Name -> String
forall a. Show a => a -> String
show Name
n)]
{- | Parses a no implicits expression
@
NoImplicits ::=
  '%' 'noImplicits' SimpleExpr
  ;
@
-}
noImplicits :: SyntaxInfo -> IdrisParser PTerm
noImplicits :: SyntaxInfo -> IdrisParser PTerm
noImplicits syn :: SyntaxInfo
syn = do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
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 '%' StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
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 "noImplicits")
                     PTerm
tm <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
                     PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> PTerm
PNoImplicits PTerm
tm)
                 IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "no implicits expression"

{- | Parses a function application expression
@
App ::=
  'mkForeign' Arg Arg*
  | MatchApp
  | SimpleExpr Arg*
  ;
MatchApp ::=
  SimpleExpr '<==' FnName
  ;
@
-}
app :: SyntaxInfo -> IdrisParser PTerm
app :: SyntaxInfo -> IdrisParser PTerm
app syn :: SyntaxInfo
syn = (StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm)
-> IdrisParser PTerm
forall (m :: * -> *) a. MonadWriter FC m => m (FC -> a) -> m a
appExtent (StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm)
 -> IdrisParser PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm)
-> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
    PTerm
f <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
    (do StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp "<=="
        Name
ff <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
        (FC -> PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (\fc :: FC
fc -> (FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
RigW (Int -> String -> Name
sMN 0 "match") FC
NoFC
                          PTerm
f
                          (FC -> Name -> PTerm
PMatchApp FC
fc Name
ff)
                          (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> String -> Name
sMN 0 "match"))))
          StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm)
-> String
-> StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "matching application expression") StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
      (do [PArg]
args <- StateT IState (WriterT FC (Parsec Void String)) PArg
-> StateT IState (WriterT FC (Parsec Void String)) [PArg]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (do StateT IState (WriterT FC (Parsec Void String)) ()
notEndApp; SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PArg
arg SyntaxInfo
syn)
          [PTerm]
wargs <- if SyntaxInfo -> Bool
withAppAllowed SyntaxInfo
syn Bool -> Bool -> Bool
&& Bool -> Bool
not (SyntaxInfo -> Bool
inPattern SyntaxInfo
syn)
                     then IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) [PTerm]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (do StateT IState (WriterT FC (Parsec Void String)) ()
notEndApp; String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp "|"; SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn)
                     else [PTerm] -> StateT IState (WriterT FC (Parsec Void String)) [PTerm]
forall (m :: * -> *) a. Monad m => a -> m a
return []
          case [PArg]
args of
            [] -> (FC -> PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return ((FC -> PTerm)
 -> StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm))
-> (FC -> PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm)
forall a b. (a -> b) -> a -> b
$ \fc :: FC
fc -> PTerm
f
            _  -> (FC -> PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return ((FC -> PTerm)
 -> StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm))
-> (FC -> PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) (FC -> PTerm)
forall a b. (a -> b) -> a -> b
$ \fc :: FC
fc -> (FC -> PTerm -> [PTerm] -> PTerm
withApp FC
fc (FC -> PTerm -> [PArg] -> PTerm
flattenFromInt FC
fc PTerm
f [PArg]
args) [PTerm]
wargs)))
     IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "function application"
  where
    -- bit of a hack to deal with the situation where we're applying a
    -- literal to an argument, which we may want for obscure applications
    -- of fromInteger, and this will help disambiguate better.
    -- We know, at least, it won't be one of the constants!
    flattenFromInt :: FC -> PTerm -> [PArg] -> PTerm
flattenFromInt fc :: FC
fc (PAlternative _ x :: PAltType
x alts :: [PTerm]
alts) args :: [PArg]
args
      | Just i :: PArg
i <- [PTerm] -> Maybe PArg
getFromInt [PTerm]
alts
           = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN "fromInteger")) (PArg
i PArg -> [PArg] -> [PArg]
forall a. a -> [a] -> [a]
: [PArg]
args)
    flattenFromInt fc :: FC
fc f :: PTerm
f args :: [PArg]
args = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
f [PArg]
args

    withApp :: FC -> PTerm -> [PTerm] -> PTerm
withApp fc :: FC
fc tm :: PTerm
tm [] = PTerm
tm
    withApp fc :: FC
fc tm :: PTerm
tm (a :: PTerm
a : as :: [PTerm]
as) = FC -> PTerm -> [PTerm] -> PTerm
withApp FC
fc (FC -> PTerm -> PTerm -> PTerm
PWithApp FC
fc PTerm
tm PTerm
a) [PTerm]
as

    getFromInt :: [PTerm] -> Maybe PArg
getFromInt ((PApp _ (PRef _ _ n :: Name
n) [a :: PArg
a]) : _) | Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "fromInteger" = PArg -> Maybe PArg
forall a. a -> Maybe a
Just PArg
a
    getFromInt (_ : xs :: [PTerm]
xs) = [PTerm] -> Maybe PArg
getFromInt [PTerm]
xs
    getFromInt _ = Maybe PArg
forall a. Maybe a
Nothing

{-| Parses a function argument
@
Arg ::=
  ImplicitArg
  | ConstraintArg
  | SimpleExpr
  ;
@
-}
arg :: SyntaxInfo -> IdrisParser PArg
arg :: SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PArg
arg syn :: SyntaxInfo
syn =  SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PArg
implicitArg SyntaxInfo
syn
       StateT IState (WriterT FC (Parsec Void String)) PArg
-> StateT IState (WriterT FC (Parsec Void String)) PArg
-> StateT IState (WriterT FC (Parsec Void String)) PArg
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PArg
constraintArg SyntaxInfo
syn
       StateT IState (WriterT FC (Parsec Void String)) PArg
-> StateT IState (WriterT FC (Parsec Void String)) PArg
-> StateT IState (WriterT FC (Parsec Void String)) PArg
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do PTerm
e <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
              PArg -> StateT IState (WriterT FC (Parsec Void String)) PArg
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
e)
       StateT IState (WriterT FC (Parsec Void String)) PArg
-> String -> StateT IState (WriterT FC (Parsec Void String)) PArg
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "function argument"

{-| Parses an implicit function argument
@
ImplicitArg ::=
  '{' Name ('=' Expr)? '}'
  ;
@
-}
implicitArg :: SyntaxInfo -> IdrisParser PArg
implicitArg :: SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PArg
implicitArg syn :: SyntaxInfo
syn = do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '{'
                     (n :: Name
n, nfc :: FC
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
name
                     PTerm
v <- PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (FC -> [FC] -> Name -> PTerm
PRef FC
nfc [FC
nfc] Name
n) (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '='
                                                          SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn)
                     Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '}'
                     PArg -> StateT IState (WriterT FC (Parsec Void String)) PArg
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> PTerm -> Bool -> PArg
forall t. Name -> t -> Bool -> PArg' t
pimp Name
n PTerm
v Bool
True)
                  StateT IState (WriterT FC (Parsec Void String)) PArg
-> String -> StateT IState (WriterT FC (Parsec Void String)) PArg
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "implicit function argument"

{-| Parses a constraint argument (for selecting a named interface implementation)

>    ConstraintArg ::=
>      '@{' Expr '}'
>      ;

-}
constraintArg :: SyntaxInfo -> IdrisParser PArg
constraintArg :: SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PArg
constraintArg syn :: SyntaxInfo
syn = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "@{"
                       PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                       String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "}"
                       PArg -> StateT IState (WriterT FC (Parsec Void String)) PArg
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> PArg
forall t. t -> PArg' t
pconst PTerm
e)
                    StateT IState (WriterT FC (Parsec Void String)) PArg
-> String -> StateT IState (WriterT FC (Parsec Void String)) PArg
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "constraint argument"

{-| Parses a quasiquote expression (for building reflected terms using the elaborator)

> Quasiquote ::= '`(' Expr ')'

-}
quasiquote :: SyntaxInfo -> IdrisParser PTerm
quasiquote :: SyntaxInfo -> IdrisParser PTerm
quasiquote syn :: SyntaxInfo
syn = (OutputAnnotation -> IdrisParser PTerm -> IdrisParser PTerm
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnQuasiquote (IdrisParser PTerm -> IdrisParser PTerm)
-> IdrisParser PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
                    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 (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "`("
                    PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn { syn_in_quasiquote :: Int
syn_in_quasiquote = (SyntaxInfo -> Int
syn_in_quasiquote SyntaxInfo
syn) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 ,
                                    inPattern :: Bool
inPattern = Bool
False }
                    Maybe PTerm
g <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe PTerm)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (Maybe PTerm))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe PTerm)
forall a b. (a -> b) -> a -> b
$
                           do 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 (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol ":"
                              SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn { inPattern :: Bool
inPattern = Bool
False } -- don't allow antiquotes
                    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 (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol ")"
                    PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ PTerm -> Maybe PTerm -> PTerm
PQuasiquote PTerm
e Maybe PTerm
g)
                  IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "quasiquotation"
{-| Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)

> Unquote ::= ',' Expr

-}
unquote :: SyntaxInfo -> IdrisParser PTerm
unquote :: SyntaxInfo -> IdrisParser PTerm
unquote syn :: SyntaxInfo
syn = (OutputAnnotation -> IdrisParser PTerm -> IdrisParser PTerm
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnAntiquote (IdrisParser PTerm -> IdrisParser PTerm)
-> IdrisParser PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
                 Bool -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (SyntaxInfo -> Int
syn_in_quasiquote SyntaxInfo
syn Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0)
                 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 (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "~"
                 PTerm
e <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn { syn_in_quasiquote :: Int
syn_in_quasiquote = SyntaxInfo -> Int
syn_in_quasiquote SyntaxInfo
syn Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1 }
                 PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm -> IdrisParser PTerm) -> PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ PTerm -> PTerm
PUnquote PTerm
e)
               IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "unquotation"
{-| Parses a quotation of a name (for using the elaborator to resolve boring details)

> NameQuote ::= '`{' Name '}'

-}
namequote :: SyntaxInfo -> IdrisParser PTerm
namequote :: SyntaxInfo -> IdrisParser PTerm
namequote syn :: SyntaxInfo
syn = OutputAnnotation -> IdrisParser PTerm -> IdrisParser PTerm
forall (m :: * -> *) a.
(MonadState IState m, Parsing m) =>
OutputAnnotation -> m a -> m a
highlight OutputAnnotation
AnnQuasiquote ((IdrisParser PTerm -> IdrisParser PTerm
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisParser PTerm -> IdrisParser PTerm)
-> IdrisParser PTerm -> IdrisParser PTerm
forall a b. (a -> b) -> a -> b
$ do
                     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 (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "`{{"
                     (n :: Name
n, nfc :: FC
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
                     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 (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "}}"
                     PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Bool -> FC -> PTerm
PQuoteName Name
n Bool
False FC
nfc))
                  IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do 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 (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "`{"
                          (n :: Name
n, nfc :: FC
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
                          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 (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "}"
                          PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Bool -> FC -> PTerm
PQuoteName Name
n Bool
True FC
nfc)))
                IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "quoted name"


{-| Parses a record field setter expression
@
RecordType ::=
  'record' '{' FieldTypeList '}';
@
@
FieldTypeList ::=
  FieldType
  | FieldType ',' FieldTypeList
  ;
@
@
FieldType ::=
  FnName '=' Expr
  ;
@
-}

data SetOrUpdate = FieldSet PTerm | FieldUpdate PTerm

recordType :: SyntaxInfo -> IdrisParser PTerm
recordType :: SyntaxInfo -> IdrisParser PTerm
recordType syn :: SyntaxInfo
syn =
      do ((fgs :: Either [([Name], SetOrUpdate)] [Name]
fgs, rec :: Maybe PTerm
rec), fc :: FC
fc) <- StateT
  IState
  (WriterT FC (Parsec Void String))
  (Either [([Name], SetOrUpdate)] [Name], Maybe PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     ((Either [([Name], SetOrUpdate)] [Name], Maybe PTerm), FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (StateT
   IState
   (WriterT FC (Parsec Void String))
   (Either [([Name], SetOrUpdate)] [Name], Maybe PTerm)
 -> StateT
      IState
      (WriterT FC (Parsec Void String))
      ((Either [([Name], SetOrUpdate)] [Name], Maybe PTerm), FC))
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Either [([Name], SetOrUpdate)] [Name], Maybe PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     ((Either [([Name], SetOrUpdate)] [Name], Maybe 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 "record"
            Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '{'
            Either [([Name], SetOrUpdate)] [Name]
fgs <- IdrisParser (Either [([Name], SetOrUpdate)] [Name])
fieldGetOrSet
            Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '}'
            Maybe PTerm
rec <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe PTerm)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do StateT IState (WriterT FC (Parsec Void String)) ()
notEndApp; SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn)
            (Either [([Name], SetOrUpdate)] [Name], Maybe PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (Either [([Name], SetOrUpdate)] [Name], Maybe PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [([Name], SetOrUpdate)] [Name]
fgs, Maybe PTerm
rec)
         case Either [([Name], SetOrUpdate)] [Name]
fgs of
              Left fields :: [([Name], SetOrUpdate)]
fields ->
                case Maybe PTerm
rec of
                   Nothing ->
                       PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> String -> Name
sMN 0 "fldx") FC
NoFC PTerm
Placeholder
                                   (FC -> [([Name], SetOrUpdate)] -> PTerm -> PTerm
applyAll FC
fc [([Name], SetOrUpdate)]
fields (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> String -> Name
sMN 0 "fldx"))))
                   Just v :: PTerm
v -> PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [([Name], SetOrUpdate)] -> PTerm -> PTerm
applyAll FC
fc [([Name], SetOrUpdate)]
fields PTerm
v)
              Right fields :: [Name]
fields ->
                case Maybe PTerm
rec of
                   Nothing ->
                       PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> String -> Name
sMN 0 "fldx") FC
NoFC PTerm
Placeholder
                                 (FC -> [Name] -> PTerm -> PTerm
getAll FC
fc ([Name] -> [Name]
forall a. [a] -> [a]
reverse [Name]
fields)
                                     (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> String -> Name
sMN 0 "fldx"))))
                   Just v :: PTerm
v -> PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> [Name] -> PTerm -> PTerm
getAll FC
fc ([Name] -> [Name]
forall a. [a] -> [a]
reverse [Name]
fields) PTerm
v)

       IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "record setting expression"
   where fieldSet :: IdrisParser ([Name], SetOrUpdate)
         fieldSet :: IdrisParser ([Name], SetOrUpdate)
fieldSet = do [Name]
ns <- StateT IState (WriterT FC (Parsec Void String)) [Name]
fieldGet
                       (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '='
                           PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                           ([Name], SetOrUpdate) -> IdrisParser ([Name], SetOrUpdate)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
ns, PTerm -> SetOrUpdate
FieldSet PTerm
e))
                         IdrisParser ([Name], SetOrUpdate)
-> IdrisParser ([Name], SetOrUpdate)
-> IdrisParser ([Name], SetOrUpdate)
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 "$="
                                PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                                ([Name], SetOrUpdate) -> IdrisParser ([Name], SetOrUpdate)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name]
ns, PTerm -> SetOrUpdate
FieldUpdate PTerm
e)
                    IdrisParser ([Name], SetOrUpdate)
-> String -> IdrisParser ([Name], SetOrUpdate)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "field setter"

         fieldGet :: IdrisParser [Name]
         fieldGet :: StateT IState (WriterT FC (Parsec Void String)) [Name]
fieldGet = StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) [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
fnName (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "->")

         fieldGetOrSet :: IdrisParser (Either [([Name], SetOrUpdate)] [Name])
         fieldGetOrSet :: IdrisParser (Either [([Name], SetOrUpdate)] [Name])
fieldGetOrSet = IdrisParser (Either [([Name], SetOrUpdate)] [Name])
-> IdrisParser (Either [([Name], SetOrUpdate)] [Name])
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([([Name], SetOrUpdate)] -> Either [([Name], SetOrUpdate)] [Name]
forall a b. a -> Either a b
Left ([([Name], SetOrUpdate)] -> Either [([Name], SetOrUpdate)] [Name])
-> StateT
     IState (WriterT FC (Parsec Void String)) [([Name], SetOrUpdate)]
-> IdrisParser (Either [([Name], SetOrUpdate)] [Name])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IdrisParser ([Name], SetOrUpdate)
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT
     IState (WriterT FC (Parsec Void String)) [([Name], SetOrUpdate)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 IdrisParser ([Name], SetOrUpdate)
fieldSet (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ','))
                     IdrisParser (Either [([Name], SetOrUpdate)] [Name])
-> IdrisParser (Either [([Name], SetOrUpdate)] [Name])
-> IdrisParser (Either [([Name], SetOrUpdate)] [Name])
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do [Name]
f <- StateT IState (WriterT FC (Parsec Void String)) [Name]
fieldGet
                            Either [([Name], SetOrUpdate)] [Name]
-> IdrisParser (Either [([Name], SetOrUpdate)] [Name])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Either [([Name], SetOrUpdate)] [Name]
forall a b. b -> Either a b
Right [Name]
f)

         applyAll :: FC -> [([Name], SetOrUpdate)] -> PTerm -> PTerm
         applyAll :: FC -> [([Name], SetOrUpdate)] -> PTerm -> PTerm
applyAll fc :: FC
fc [] x :: PTerm
x = PTerm
x
         applyAll fc :: FC
fc ((ns :: [Name]
ns, e :: SetOrUpdate
e) : es :: [([Name], SetOrUpdate)]
es) x :: PTerm
x
            = FC -> [([Name], SetOrUpdate)] -> PTerm -> PTerm
applyAll FC
fc [([Name], SetOrUpdate)]
es (FC -> [Name] -> SetOrUpdate -> PTerm -> PTerm
doUpdate FC
fc [Name]
ns SetOrUpdate
e PTerm
x)

         doUpdate :: FC -> [Name] -> SetOrUpdate -> PTerm -> PTerm
doUpdate fc :: FC
fc ns :: [Name]
ns (FieldUpdate e :: PTerm
e) get :: PTerm
get
              = let get' :: PTerm
get' = FC -> [Name] -> PTerm -> PTerm
getAll FC
fc ([Name] -> [Name]
forall a. [a] -> [a]
reverse [Name]
ns) PTerm
get in
                    FC -> [Name] -> SetOrUpdate -> PTerm -> PTerm
doUpdate FC
fc [Name]
ns (PTerm -> SetOrUpdate
FieldSet (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc PTerm
e [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
get'])) PTerm
get
         doUpdate fc :: FC
fc [n :: Name
n] (FieldSet e :: PTerm
e) get :: PTerm
get
              = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Name -> Name
mkType Name
n)) [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
e, PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
get]
         doUpdate fc :: FC
fc (n :: Name
n : ns :: [Name]
ns) e :: SetOrUpdate
e get :: PTerm
get
              = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Name -> Name
mkType Name
n))
                  [PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> [Name] -> SetOrUpdate -> PTerm -> PTerm
doUpdate FC
fc [Name]
ns SetOrUpdate
e (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
get])),
                   PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
get]

         getAll :: FC -> [Name] -> PTerm -> PTerm
         getAll :: FC -> [Name] -> PTerm -> PTerm
getAll fc :: FC
fc [n :: Name
n] e :: PTerm
e = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
e]
         getAll fc :: FC
fc (n :: Name
n:ns :: [Name]
ns) e :: PTerm
e = FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] Name
n) [PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> [Name] -> PTerm -> PTerm
getAll FC
fc [Name]
ns PTerm
e)]


-- | Creates setters for record types on necessary functions
mkType :: Name -> Name
mkType :: Name -> Name
mkType (UN n :: Text
n) = String -> Name
sUN ("set_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
mkType (MN 0 n :: Text
n) = Int -> String -> Name
sMN 0 ("set_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
str Text
n)
mkType (NS n :: Name
n s :: [Text]
s) = Name -> [Text] -> Name
NS (Name -> Name
mkType Name
n) [Text]
s

{- | Parses a type signature
@
TypeSig ::=
  ':' Expr
  ;
@
@
TypeExpr ::= ConstraintList? Expr;
@
 -}
typeExpr :: SyntaxInfo -> IdrisParser PTerm
typeExpr :: SyntaxInfo -> IdrisParser PTerm
typeExpr syn :: SyntaxInfo
syn = do [(RigCount, Name, FC, PTerm)]
cs <- if SyntaxInfo -> Bool
implicitAllowed SyntaxInfo
syn then SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList SyntaxInfo
syn else [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
                  PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
allowConstr SyntaxInfo
syn)
                  PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return ((RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm)
-> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList (\r :: RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
constraint { pcount :: RigCount
pcount = RigCount
r })) [(RigCount, Name, FC, PTerm)]
cs PTerm
sc)
               IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "type signature"

{- | Parses a lambda expression
@
Lambda ::=
    '\\' TypeOptDeclList LambdaTail
  | '\\' SimpleExprList  LambdaTail
  ;
@
@
SimpleExprList ::=
  SimpleExpr
  | SimpleExpr ',' SimpleExprList
  ;
@
@
LambdaTail ::=
    Impossible
  | '=>' Expr
@
-}
lambda :: SyntaxInfo -> IdrisParser PTerm
lambda :: SyntaxInfo -> IdrisParser PTerm
lambda syn :: SyntaxInfo
syn = do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '\\' StateT IState (WriterT FC (Parsec Void String)) Char
-> String -> StateT IState (WriterT FC (Parsec Void String)) Char
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "lambda expression"
                ((do [(RigCount, Name, FC, PTerm)]
xt <- IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (IdrisParser [(RigCount, Name, FC, PTerm)]
 -> IdrisParser [(RigCount, Name, FC, PTerm)])
-> IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
tyOptDeclList (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                     (sc :: PTerm
sc, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent IdrisParser PTerm
lambdaTail
                     PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return ((RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm)
-> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList (\r :: RigCount
r -> FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc) [(RigCount, Name, FC, PTerm)]
xt PTerm
sc))
                 IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                 (do [(FC, PTerm)]
ps <- StateT IState (WriterT FC (Parsec Void String)) (FC, PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) [(FC, PTerm)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy (do (e :: PTerm
e, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
simpleExpr (SyntaxInfo -> SyntaxInfo
disallowImp (SyntaxInfo
syn { inPattern :: Bool
inPattern = Bool
True }))
                                       (FC, PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) (FC, PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (FC
fc, PTerm
e))
                                   (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ',')
                     PTerm
sc <- IdrisParser PTerm
lambdaTail
                     PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, (FC, PTerm))] -> PTerm -> PTerm
pmList ([Int] -> [(FC, PTerm)] -> [(Int, (FC, PTerm))]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [(FC, PTerm)]
ps) PTerm
sc)))
                  IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "lambda expression"
    where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
          pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
pmList [] sc :: PTerm
sc = PTerm
sc
          pmList ((i :: Int
i, (fc :: FC
fc, x :: PTerm
x)) : xs :: [(Int, (FC, PTerm))]
xs) sc :: PTerm
sc
                = FC -> Name -> FC -> PTerm -> PTerm -> PTerm
PLam FC
fc (Int -> String -> Name
sMN Int
i "lamp") FC
NoFC PTerm
Placeholder
                        (FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Int -> String -> Name
sMN Int
i "lamp"))
                                [(PTerm
x, [(Int, (FC, PTerm))] -> PTerm -> PTerm
pmList [(Int, (FC, PTerm))]
xs PTerm
sc)])
          lambdaTail :: IdrisParser PTerm
          lambdaTail :: IdrisParser PTerm
lambdaTail = IdrisParser PTerm
impossible IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
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 ()
symbol "=>" StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn

{- | Parses a term rewrite expression
@
RewriteTerm ::=
  'rewrite' Expr ('==>' Expr)? 'in' Expr
  ;
@
-}
rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
rewriteTerm syn :: SyntaxInfo
syn = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "rewrite"
                     (prf :: PTerm
prf, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                     Maybe PTerm
giving <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe PTerm)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "==>"; SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn)
                     Maybe Name
using <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe Name)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved "using"
                                           Name
n <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
                                           Name -> StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n)
                     String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "in";  PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                     PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> PTerm
PRewrite FC
fc Maybe Name
using PTerm
prf PTerm
sc Maybe PTerm
giving)
                  IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "term rewrite expression"

-- | Parse rig count for linear types
rigCount :: Parsing m => m RigCount
rigCount :: m RigCount
rigCount = RigCount -> m RigCount -> m RigCount
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option RigCount
RigW (m RigCount -> m RigCount) -> m RigCount -> m RigCount
forall a b. (a -> b) -> a -> b
$ do Char -> m Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '1'; RigCount -> m RigCount
forall (m :: * -> *) a. Monad m => a -> m a
return RigCount
Rig1
                       m RigCount -> m RigCount -> m RigCount
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do Char -> m Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '0'; RigCount -> m RigCount
forall (m :: * -> *) a. Monad m => a -> m a
return RigCount
Rig0

{- |Parses a let binding
@
Let ::=
  'let' Name TypeSig'? '=' Expr  'in' Expr
| 'let' Expr'          '=' Expr' 'in' Expr

TypeSig' ::=
  ':' Expr'
  ;
@
 -}
let_ :: SyntaxInfo -> IdrisParser PTerm
let_ :: SyntaxInfo -> IdrisParser PTerm
let_ syn :: SyntaxInfo
syn = IdrisParser PTerm -> IdrisParser PTerm
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "let"
                     [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
ls <- IdrisParser (FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])
-> IdrisParser
     [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
forall a. IdrisParser a -> IdrisParser [a]
indentedBlock (SyntaxInfo
-> IdrisParser
     (FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])
let_binding SyntaxInfo
syn)
                     String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "in";  PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                     PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return ([(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
-> PTerm -> PTerm
buildLets [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
ls PTerm
sc))
           IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "let binding"
  where buildLets :: [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
-> PTerm -> PTerm
buildLets [] sc :: PTerm
sc = PTerm
sc
        buildLets ((fc :: FC
fc, rc :: RigCount
rc, PRef nfc :: FC
nfc _ n :: Name
n, ty :: PTerm
ty, v :: PTerm
v, []) : ls :: [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
ls) sc :: PTerm
sc
          = FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm -> PTerm
PLet FC
fc RigCount
rc Name
n FC
nfc PTerm
ty PTerm
v ([(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
-> PTerm -> PTerm
buildLets [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
ls PTerm
sc)
        buildLets ((fc :: FC
fc, _, pat :: PTerm
pat, ty :: PTerm
ty, v :: PTerm
v, alts :: [(PTerm, PTerm)]
alts) : ls :: [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
ls) sc :: PTerm
sc
          = FC -> PTerm -> [(PTerm, PTerm)] -> PTerm
PCase FC
fc PTerm
v ((PTerm
pat, [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
-> PTerm -> PTerm
buildLets [(FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])]
ls PTerm
sc) (PTerm, PTerm) -> [(PTerm, PTerm)] -> [(PTerm, PTerm)]
forall a. a -> [a] -> [a]
: [(PTerm, PTerm)]
alts)

let_binding :: SyntaxInfo
-> IdrisParser
     (FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])
let_binding syn :: SyntaxInfo
syn = do RigCount
rc <- StateT IState (WriterT FC (Parsec Void String)) RigCount
forall (m :: * -> *). Parsing m => m RigCount
rigCount
                     (pat :: PTerm
pat, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr' (SyntaxInfo
syn { inPattern :: Bool
inPattern = Bool
True })
                     PTerm
ty <- PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option PTerm
Placeholder (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ':'; SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn)
                     Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '='
                     PTerm
v <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = PTerm -> Bool
isVar PTerm
pat })
                     [(PTerm, PTerm)]
ts <- [(PTerm, PTerm)]
-> IdrisParser [(PTerm, PTerm)] -> IdrisParser [(PTerm, PTerm)]
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option [] (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '|'
                                           IdrisParser (PTerm, PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [(PTerm, PTerm)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser (PTerm, PTerm)
do_alt SyntaxInfo
syn) (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '|'))
                     (FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])
-> IdrisParser
     (FC, RigCount, PTerm, PTerm, PTerm, [(PTerm, PTerm)])
forall (m :: * -> *) a. Monad m => a -> m a
return (FC
fc,RigCount
rc,PTerm
pat,PTerm
ty,PTerm
v,[(PTerm, PTerm)]
ts)
   where isVar :: PTerm -> Bool
isVar (PRef _ _ _) = Bool
True
         isVar _ = Bool
False

{- | Parses a conditional expression
@
If ::= 'if' Expr 'then' Expr 'else' Expr
@

-}
if_ :: SyntaxInfo -> IdrisParser PTerm
if_ :: SyntaxInfo -> IdrisParser PTerm
if_ syn :: SyntaxInfo
syn = (do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "if"
              (c :: PTerm
c, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
              String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "then"
              PTerm
t <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
              String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "else"
              PTerm
f <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
              PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> PTerm -> PTerm -> PTerm
PIfThenElse FC
fc PTerm
c PTerm
t PTerm
f))
          IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "conditional expression"


{- | Parses a quote goal

@
QuoteGoal ::=
  'quoteGoal' Name 'by' Expr 'in' Expr
  ;
@
 -}
quoteGoal :: SyntaxInfo -> IdrisParser PTerm
quoteGoal :: SyntaxInfo -> IdrisParser PTerm
quoteGoal syn :: SyntaxInfo
syn = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "quoteGoal"; Name
n <- StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name;
                   String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "by"
                   PTerm
r <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                   String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "in"
                   (sc :: PTerm
sc, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                   PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> Name -> PTerm -> PTerm
PGoal FC
fc PTerm
r Name
n PTerm
sc)
                IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "quote goal expression"

{- | Parses a dependent type signature

@
Pi ::= PiOpts Static? Pi'
@

@
Pi' ::=
    OpExpr ('->' Pi)?
  | '(' TypeDeclList           ')'            '->' Pi
  | '{' TypeDeclList           '}'            '->' Pi
  | '{' 'auto'    TypeDeclList '}'            '->' Pi
  | '{' 'default' SimpleExpr TypeDeclList '}' '->' Pi
  ;
@
 -}

bindsymbol :: [ArgOpt] -> Static -> p -> m Plicity
bindsymbol opts :: [ArgOpt]
opts st :: Static
st syn :: p
syn
     = do String -> m ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "->"
          Plicity -> m Plicity
forall (m :: * -> *) a. Monad m => a -> m a
return ([ArgOpt] -> Static -> Bool -> RigCount -> Plicity
Exp [ArgOpt]
opts Static
st Bool
False RigCount
RigW)

explicitPi :: [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
explicitPi opts :: [ArgOpt]
opts st :: Static
st syn :: SyntaxInfo
syn
   = do [(RigCount, Name, FC, PTerm)]
xt <- IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
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 '(' StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
typeDeclList SyntaxInfo
syn IdrisParser [(RigCount, Name, FC, PTerm)]
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [(RigCount, Name, FC, PTerm)]
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 ')')
        Plicity
binder <- [ArgOpt]
-> Static
-> SyntaxInfo
-> StateT IState (WriterT FC (Parsec Void String)) Plicity
forall (m :: * -> *) p.
(MonadFail m, MonadParsec Void String m, MonadWriter FC m) =>
[ArgOpt] -> Static -> p -> m Plicity
bindsymbol [ArgOpt]
opts Static
st SyntaxInfo
syn
        PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
allowConstr SyntaxInfo
syn)
        PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return ((RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm)
-> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList (\r :: RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
binder { pcount :: RigCount
pcount = RigCount
r })) [(RigCount, Name, FC, PTerm)]
xt PTerm
sc)

autoImplicit :: p -> Static -> SyntaxInfo -> IdrisParser PTerm
autoImplicit opts :: p
opts st :: Static
st syn :: SyntaxInfo
syn
   = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "auto"
        Bool
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Static
st Static -> Static -> Bool
forall a. Eq a => a -> a -> Bool
== Static
Static) (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "auto implicits can not be static"
        [(RigCount, Name, FC, PTerm)]
xt <- SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
typeDeclList SyntaxInfo
syn
        Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '}'
        String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "->"
        PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
allowConstr SyntaxInfo
syn)
        PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return ((RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm)
-> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList (\r :: RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi
          ([ArgOpt] -> Static -> PTerm -> RigCount -> Plicity
TacImp [] Static
Dynamic ([PTactic] -> PTerm
PTactics [Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic
forall t.
Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic' t
ProofSearch Bool
True Bool
True 100 Maybe Name
forall a. Maybe a
Nothing [] []]) RigCount
r)) [(RigCount, Name, FC, PTerm)]
xt PTerm
sc)

defaultImplicit :: p -> Static -> SyntaxInfo -> IdrisParser PTerm
defaultImplicit opts :: p
opts st :: Static
st syn :: SyntaxInfo
syn = do
   String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "default"
   Bool
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Static
st Static -> Static -> Bool
forall a. Eq a => a -> a -> Bool
== Static
Static) (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "default implicits can not be static"
   IState
ist <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
   PTerm
script' <- SyntaxInfo -> IdrisParser PTerm
simpleExpr SyntaxInfo
syn
   let script :: PTerm
script = 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
ist (PTerm -> PTerm) -> PTerm -> PTerm
forall a b. (a -> b) -> a -> b
$ PTerm
script'
   [(RigCount, Name, FC, PTerm)]
xt <- SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
typeDeclList SyntaxInfo
syn
   Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '}'
   String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "->"
   PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
allowConstr SyntaxInfo
syn)
   PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return ((RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm)
-> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList (\r :: RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([ArgOpt] -> Static -> PTerm -> RigCount -> Plicity
TacImp [] Static
Dynamic PTerm
script RigCount
r)) [(RigCount, Name, FC, PTerm)]
xt PTerm
sc)

normalImplicit :: [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
normalImplicit opts :: [ArgOpt]
opts st :: Static
st syn :: SyntaxInfo
syn = do
   [(RigCount, Name, FC, PTerm)]
xt <- SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
typeDeclList SyntaxInfo
syn IdrisParser [(RigCount, Name, FC, PTerm)]
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [(RigCount, Name, FC, PTerm)]
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 '}'
   String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "->"
   [(RigCount, Name, FC, PTerm)]
cs <- SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList SyntaxInfo
syn
   PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
   let (im :: Plicity
im,cl :: Plicity
cl)
          = if SyntaxInfo -> Bool
implicitAllowed SyntaxInfo
syn
               then ([ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [ArgOpt]
opts Static
st Bool
False (ImplicitInfo -> Maybe ImplicitInfo
forall a. a -> Maybe a
Just (Bool -> Bool -> Bool -> ImplicitInfo
Impl Bool
False Bool
True Bool
False)) Bool
True RigCount
RigW,
                      Plicity
constraint)
               else ([ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [ArgOpt]
opts Static
st Bool
False (ImplicitInfo -> Maybe ImplicitInfo
forall a. a -> Maybe a
Just (Bool -> Bool -> Bool -> ImplicitInfo
Impl Bool
False Bool
False Bool
False)) Bool
True RigCount
RigW,
                     [ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [ArgOpt]
opts Static
st Bool
False (ImplicitInfo -> Maybe ImplicitInfo
forall a. a -> Maybe a
Just (Bool -> Bool -> Bool -> ImplicitInfo
Impl Bool
True Bool
False Bool
False)) Bool
True RigCount
RigW)
   PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return ((RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm)
-> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList (\r :: RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
im { pcount :: RigCount
pcount = RigCount
r })) [(RigCount, Name, FC, PTerm)]
xt
           ((RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm)
-> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList (\r :: RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi (Plicity
cl { pcount :: RigCount
pcount = RigCount
r })) [(RigCount, Name, FC, PTerm)]
cs PTerm
sc))

constraintPi :: [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
constraintPi opts :: [ArgOpt]
opts st :: Static
st syn :: SyntaxInfo
syn =
   do [(RigCount, Name, FC, PTerm)]
cs <- SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList1 SyntaxInfo
syn
      PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
      if SyntaxInfo -> Bool
implicitAllowed SyntaxInfo
syn
         then PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return ((RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm)
-> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList (\r :: RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
constraint { pcount :: RigCount
pcount = RigCount
r }) [(RigCount, Name, FC, PTerm)]
cs PTerm
sc)
         else PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return ((RigCount -> Name -> FC -> PTerm -> PTerm -> PTerm)
-> [(RigCount, Name, FC, PTerm)] -> PTerm -> PTerm
bindList (\r :: RigCount
r -> Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi ([ArgOpt]
-> Static
-> Bool
-> Maybe ImplicitInfo
-> Bool
-> RigCount
-> Plicity
Imp [ArgOpt]
opts Static
st Bool
False (ImplicitInfo -> Maybe ImplicitInfo
forall a. a -> Maybe a
Just (Bool -> Bool -> Bool -> ImplicitInfo
Impl Bool
True Bool
False Bool
False)) Bool
True RigCount
r))
                               [(RigCount, Name, FC, PTerm)]
cs PTerm
sc)

implicitPi :: [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
implicitPi opts :: [ArgOpt]
opts st :: Static
st syn :: SyntaxInfo
syn =
      [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
forall p. p -> Static -> SyntaxInfo -> IdrisParser PTerm
autoImplicit [ArgOpt]
opts Static
st SyntaxInfo
syn
        IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
forall p. p -> Static -> SyntaxInfo -> IdrisParser PTerm
defaultImplicit [ArgOpt]
opts Static
st SyntaxInfo
syn
          IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
normalImplicit [ArgOpt]
opts Static
st SyntaxInfo
syn

unboundPi :: [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
unboundPi opts :: [ArgOpt]
opts st :: Static
st syn :: SyntaxInfo
syn = do
       PTerm
x <- SyntaxInfo -> IdrisParser PTerm
opExpr SyntaxInfo
syn
       (do Plicity
binder <- [ArgOpt]
-> Static
-> SyntaxInfo
-> StateT IState (WriterT FC (Parsec Void String)) Plicity
forall (m :: * -> *) p.
(MonadFail m, MonadParsec Void String m, MonadWriter FC m) =>
[ArgOpt] -> Static -> p -> m Plicity
bindsymbol [ArgOpt]
opts Static
st SyntaxInfo
syn
           PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
           PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
binder (String -> Name
sUN "__pi_arg") FC
NoFC PTerm
x PTerm
sc))
              IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
x

-- This is used when we need to disambiguate from a constraint list
unboundPiNoConstraint :: [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
unboundPiNoConstraint opts :: [ArgOpt]
opts st :: Static
st syn :: SyntaxInfo
syn = do
       PTerm
x <- SyntaxInfo -> IdrisParser PTerm
opExpr SyntaxInfo
syn
       (do Plicity
binder <- [ArgOpt]
-> Static
-> SyntaxInfo
-> StateT IState (WriterT FC (Parsec Void String)) Plicity
forall (m :: * -> *) p.
(MonadFail m, MonadParsec Void String m, MonadWriter FC m) =>
[ArgOpt] -> Static -> p -> m Plicity
bindsymbol [ArgOpt]
opts Static
st SyntaxInfo
syn
           PTerm
sc <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
           StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
P.notFollowedBy (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp "=>"
           PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (Plicity -> Name -> FC -> PTerm -> PTerm -> PTerm
PPi Plicity
binder (String -> Name
sUN "__pi_arg") FC
NoFC PTerm
x PTerm
sc))
              IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
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 e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
P.notFollowedBy (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp "=>"
                     PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return PTerm
x


pi :: SyntaxInfo -> IdrisParser PTerm
pi :: SyntaxInfo -> IdrisParser PTerm
pi syn :: SyntaxInfo
syn =
     do [ArgOpt]
opts <- SyntaxInfo -> IdrisParser [ArgOpt]
piOpts SyntaxInfo
syn
        Static
st   <- IdrisParser Static
static
        [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
explicitPi [ArgOpt]
opts Static
st SyntaxInfo
syn
         IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser PTerm -> IdrisParser PTerm
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 '{'; [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
implicitPi [ArgOpt]
opts Static
st SyntaxInfo
syn)
         IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> if SyntaxInfo -> Bool
constraintAllowed SyntaxInfo
syn
                then IdrisParser PTerm -> IdrisParser PTerm
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try ([ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
unboundPiNoConstraint [ArgOpt]
opts Static
st SyntaxInfo
syn)
                           IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
constraintPi [ArgOpt]
opts Static
st SyntaxInfo
syn
                else [ArgOpt] -> Static -> SyntaxInfo -> IdrisParser PTerm
unboundPi [ArgOpt]
opts Static
st SyntaxInfo
syn
  IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "dependent type signature"

{- | Parses Possible Options for Pi Expressions
@
  PiOpts ::= '.'?
@
-}
piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]
piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]
piOpts syn :: SyntaxInfo
syn | SyntaxInfo -> Bool
implicitAllowed SyntaxInfo
syn =
        Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '.' StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [ArgOpt] -> IdrisParser [ArgOpt]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [ArgOpt] -> IdrisParser [ArgOpt]
forall (m :: * -> *) a. Monad m => a -> m a
return [ArgOpt
InaccessibleArg]
    IdrisParser [ArgOpt]
-> IdrisParser [ArgOpt] -> IdrisParser [ArgOpt]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [ArgOpt] -> IdrisParser [ArgOpt]
forall (m :: * -> *) a. Monad m => a -> m a
return []
piOpts syn :: SyntaxInfo
syn = [ArgOpt] -> IdrisParser [ArgOpt]
forall (m :: * -> *) a. Monad m => a -> m a
return []

{- | Parses a type constraint list

@
ConstraintList ::=
    '(' Expr_List ')' '=>'
  | Expr              '=>'
  ;
@
-}
constraintList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList syn :: SyntaxInfo
syn = IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList1 SyntaxInfo
syn)
                     IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (m :: * -> *) a. Monad m => a -> m a
return []

constraintList1 :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList1 :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
constraintList1 syn :: SyntaxInfo
syn = IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
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 '('
                                [(RigCount, Name, FC, PTerm)]
tys <- StateT
  IState
  (WriterT FC (Parsec Void String))
  (RigCount, Name, FC, PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 StateT
  IState
  (WriterT FC (Parsec Void String))
  (RigCount, Name, FC, PTerm)
nexpr (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
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ')'
                                String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp "=>"
                                [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(RigCount, Name, FC, PTerm)]
tys)
                  IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do PTerm
t <- SyntaxInfo -> IdrisParser PTerm
opExpr (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                                String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp "=>"
                                [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(RigCount
RigW, Name
defname, FC
NoFC, PTerm
t)])
                  IdrisParser [(RigCount, Name, FC, PTerm)]
-> String -> IdrisParser [(RigCount, Name, FC, PTerm)]
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "type constraint list"
  where nexpr :: StateT
  IState
  (WriterT FC (Parsec Void String))
  (RigCount, Name, FC, PTerm)
nexpr = StateT
  IState
  (WriterT FC (Parsec Void String))
  (RigCount, Name, FC, PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (RigCount, Name, FC, PTerm)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (n :: Name
n, fc :: FC
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; Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ':'
                          PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                          (RigCount, Name, FC, PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (RigCount, Name, FC, PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (RigCount
RigW, Name
n, FC
fc, PTerm
e))
                StateT
  IState
  (WriterT FC (Parsec Void String))
  (RigCount, Name, FC, PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (RigCount, Name, FC, PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (RigCount, Name, FC, PTerm)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do PTerm
e <- SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                       (RigCount, Name, FC, PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (RigCount, Name, FC, PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (RigCount
RigW, Name
defname, FC
NoFC, PTerm
e)
        defname :: Name
defname = Int -> String -> Name
sMN 0 "constraint"

{- | Parses a type declaration list
@
TypeDeclList ::=
    FunctionSignatureList
  | NameList TypeSig
  ;
@

@
FunctionSignatureList ::=
    Name TypeSig
  | Name TypeSig ',' FunctionSignatureList
  ;
@
-}
typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
typeDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
typeDeclList syn :: SyntaxInfo
syn = IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (StateT
  IState
  (WriterT FC (Parsec Void String))
  (RigCount, Name, FC, PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (do RigCount
rig <- StateT IState (WriterT FC (Parsec Void String)) RigCount
forall (m :: * -> *). Parsing m => m RigCount
rigCount
                                       (x :: Name
x, xfc :: FC
xfc) <- 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 ':'
                                       PTerm
t <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                                       (RigCount, Name, FC, PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (RigCount, Name, FC, PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (RigCount
rig, Name
x, FC
xfc, PTerm
t))
                             (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ','))
                   IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do [(Name, FC)]
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
name) (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
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ':'
                          PTerm
t <- SyntaxInfo -> IdrisParser PTerm
typeExpr (SyntaxInfo -> SyntaxInfo
disallowImp SyntaxInfo
syn)
                          [(RigCount, Name, FC, PTerm)]
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (m :: * -> *) a. Monad m => a -> m a
return (((Name, FC) -> (RigCount, Name, FC, PTerm))
-> [(Name, FC)] -> [(RigCount, Name, FC, PTerm)]
forall a b. (a -> b) -> [a] -> [b]
map (\(x :: Name
x, xfc :: FC
xfc) -> (RigCount
RigW, Name
x, FC
xfc, PTerm
t)) [(Name, FC)]
ns)
                   IdrisParser [(RigCount, Name, FC, PTerm)]
-> String -> IdrisParser [(RigCount, Name, FC, PTerm)]
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "type declaration list"

{- | Parses a type declaration list with optional parameters
@
TypeOptDeclList ::=
    NameOrPlaceholder TypeSig?
  | NameOrPlaceholder TypeSig? ',' TypeOptDeclList
  ;
@

@
NameOrPlaceHolder ::= Name | '_';
@
-}
tyOptDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
tyOptDeclList :: SyntaxInfo -> IdrisParser [(RigCount, Name, FC, PTerm)]
tyOptDeclList syn :: SyntaxInfo
syn = StateT
  IState
  (WriterT FC (Parsec Void String))
  (RigCount, Name, FC, PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [(RigCount, Name, FC, PTerm)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (do (x :: Name
x, fc :: FC
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
nameOrPlaceholder
                                 PTerm
t <- PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option PTerm
Placeholder (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ':'
                                                               SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn)
                                 (RigCount, Name, FC, PTerm)
-> StateT
     IState
     (WriterT FC (Parsec Void String))
     (RigCount, Name, FC, PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (RigCount
RigW, Name
x, FC
fc, PTerm
t))
                             (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ',')
                    IdrisParser [(RigCount, Name, FC, PTerm)]
-> String -> IdrisParser [(RigCount, Name, FC, PTerm)]
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "type declaration list"
    where  nameOrPlaceholder :: IdrisParser Name
           nameOrPlaceholder :: StateT IState (WriterT FC (Parsec Void String)) Name
nameOrPlaceholder = 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)) Name
-> StateT IState (WriterT FC (Parsec Void String)) Name
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> String -> Name
sMN 0 "underscore" Name
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) Name
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp "_"
                           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
<?> "name or placeholder"

{- | Parses a list literal expression e.g. [1,2,3] or a comprehension [ (x, y) | x <- xs , y <- ys ]
@
ListExpr ::=
     '[' ']'
  | '[' Expr '|' DoList ']'
  | '[' ExprList ']'
;
@
@
DoList ::=
    Do
  | Do ',' DoList
  ;
@
@
ExprList ::=
  Expr
  | Expr ',' ExprList
  ;
@
 -}
listExpr :: SyntaxInfo -> IdrisParser PTerm
listExpr :: SyntaxInfo -> IdrisParser PTerm
listExpr syn :: SyntaxInfo
syn = do (FC f :: String
f (l :: Int
l, c :: Int
c) _) <- StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '[')
                  (do (FC _ _ (l' :: Int
l', c' :: Int
c')) <- StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ']') StateT IState (WriterT FC (Parsec Void String)) FC
-> String -> StateT IState (WriterT FC (Parsec Void String)) FC
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "end of list expression"
                      PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm
mkNil (String -> (Int, Int) -> (Int, Int) -> FC
FC String
f (Int
l, Int
c) (Int
l', Int
c'))))
                   IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do (x :: PTerm
x, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })) StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
-> String
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "expression"
                           (do StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) Char
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 '|') StateT IState (WriterT FC (Parsec Void String)) Char
-> String -> StateT IState (WriterT FC (Parsec Void String)) Char
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "list comprehension"
                               [PDo]
qs <- StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) [PDo]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PDo
do_ SyntaxInfo
syn) (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
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ']'
                               PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return ([PDo] -> PTerm
PDoBlock ((PDo -> PDo) -> [PDo] -> [PDo]
forall a b. (a -> b) -> [a] -> [b]
map PDo -> PDo
addGuard [PDo]
qs [PDo] -> [PDo] -> [PDo]
forall a. [a] -> [a] -> [a]
++
                                          [FC -> PTerm -> PDo
forall t. FC -> t -> PDo' t
DoExp FC
fc (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN "pure"))
                                                       [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
x])]))) IdrisParser PTerm -> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
                            (do [(PTerm, FC)]
xs <- StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
-> StateT IState (WriterT FC (Parsec Void String)) [(PTerm, FC)]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (do FC
commaFC <- StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ',') StateT IState (WriterT FC (Parsec Void String)) FC
-> String -> StateT IState (WriterT FC (Parsec Void String)) FC
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "list element"
                                               PTerm
elt <- SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                                               (PTerm, FC)
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
elt, FC
commaFC))
                                FC
rbrackFC <- StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) FC
forall (m :: * -> *) a. MonadWriter FC m => m a -> m FC
extent (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ']') StateT IState (WriterT FC (Parsec Void String)) FC
-> String -> StateT IState (WriterT FC (Parsec Void String)) FC
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "end of list expression"
                                PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> FC -> [(PTerm, FC)] -> PTerm
mkList FC
fc FC
rbrackFC ((PTerm
x, (String -> (Int, Int) -> (Int, Int) -> FC
FC String
f (Int
l, Int
c) (Int
l, Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
+1))) (PTerm, FC) -> [(PTerm, FC)] -> [(PTerm, FC)]
forall a. a -> [a] -> [a]
: [(PTerm, FC)]
xs))))
                IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "list expression"
  where
    mkNil :: FC -> PTerm
    mkNil :: FC -> PTerm
mkNil fc :: FC
fc = FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC
fc] (String -> Name
sUN "Nil")
    mkList :: FC -> FC -> [(PTerm, FC)] -> PTerm
    mkList :: FC -> FC -> [(PTerm, FC)] -> PTerm
mkList errFC :: FC
errFC nilFC :: FC
nilFC [] = FC -> [FC] -> Name -> PTerm
PRef FC
nilFC [FC
nilFC] (String -> Name
sUN "Nil")
    mkList errFC :: FC
errFC nilFC :: FC
nilFC ((x :: PTerm
x, fc :: FC
fc) : xs :: [(PTerm, FC)]
xs) = FC -> PTerm -> [PArg] -> PTerm
PApp FC
errFC (FC -> [FC] -> Name -> PTerm
PRef FC
fc [FC
fc] (String -> Name
sUN "::")) [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
x, PTerm -> PArg
forall t. t -> PArg' t
pexp (FC -> FC -> [(PTerm, FC)] -> PTerm
mkList FC
errFC FC
nilFC [(PTerm, FC)]
xs)]
    addGuard :: PDo -> PDo
    addGuard :: PDo -> PDo
addGuard (DoExp fc :: FC
fc e :: PTerm
e) = FC -> PTerm -> PDo
forall t. FC -> t -> PDo' t
DoExp FC
fc (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN "guard"))
                                              [PTerm -> PArg
forall t. t -> PArg' t
pexp PTerm
e])
    addGuard x :: PDo
x = PDo
x

{- | Parses a do-block
@
Do' ::= Do KeepTerminator;
@

@
DoBlock ::=
  'do' OpenBlock Do'+ CloseBlock
  ;
@
 -}
doBlock :: SyntaxInfo -> IdrisParser PTerm
doBlock :: SyntaxInfo -> IdrisParser PTerm
doBlock syn :: SyntaxInfo
syn
    = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "do"
         [PDo] -> PTerm
PDoBlock ([PDo] -> PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) [PDo]
-> IdrisParser PTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) [PDo]
forall a. IdrisParser a -> IdrisParser [a]
indentedBlock1 (SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PDo
do_ SyntaxInfo
syn)
      IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "do block"

{- | Parses an expression inside a do block
@
Do ::=
    'let' Name  TypeSig'?      '=' Expr
  | 'let' Expr'                '=' Expr
  | 'rewrite Expr
  | Name  '<-' Expr
  | Expr' '<-' Expr
  | Expr
  ;
@
-}
do_ :: SyntaxInfo -> IdrisParser PDo
do_ :: SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) PDo
do_ syn :: SyntaxInfo
syn
     = StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "let"
                 (i :: Name
i, ifc :: FC
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
                 Maybe PTerm
ty' <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (Maybe PTerm)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
P.optional (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ':'
                                       SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn)
                 String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp "="
                 (e :: PTerm
e, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })
                 -- If there is an explicit type, this can’t be a pattern-matching let, so do not parse alternatives
                 PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (FC -> RigCount -> Name -> FC -> PTerm -> PTerm -> PDo
forall t. FC -> RigCount -> Name -> FC -> t -> t -> PDo' t
DoLet FC
fc RigCount
RigW Name
i FC
ifc (PTerm -> Maybe PTerm -> PTerm
forall a. a -> Maybe a -> a
fromMaybe PTerm
Placeholder Maybe PTerm
ty') PTerm
e)
                          (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '|'
                              Bool
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe PTerm -> Bool
forall a. Maybe a -> Bool
isJust Maybe PTerm
ty') (StateT IState (WriterT FC (Parsec Void String)) ()
 -> StateT IState (WriterT FC (Parsec Void String)) ())
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) ()
forall a b. (a -> b) -> a -> b
$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "a pattern-matching let may not have an explicit type annotation"
                              [(PTerm, PTerm)]
ts <- IdrisParser (PTerm, PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [(PTerm, PTerm)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser (PTerm, PTerm)
do_alt (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })) (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '|')
                              PDo -> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> PTerm -> [(PTerm, PTerm)] -> PDo
forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoLetP FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
ifc [FC
ifc] Name
i) PTerm
e [(PTerm, PTerm)]
ts)))
   StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "let"
                 PTerm
i <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
                 String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reservedOp "="
                 (e :: PTerm
e, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })
                 PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (FC -> PTerm -> PTerm -> [(PTerm, PTerm)] -> PDo
forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoLetP FC
fc PTerm
i PTerm
e [])
                          (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '|'
                              [(PTerm, PTerm)]
ts <- IdrisParser (PTerm, PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [(PTerm, PTerm)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser (PTerm, PTerm)
do_alt (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })) (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '|')
                              PDo -> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> PTerm -> [(PTerm, PTerm)] -> PDo
forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoLetP FC
fc PTerm
i PTerm
e [(PTerm, PTerm)]
ts)))
   StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (sc :: PTerm
sc, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *).
(Parsing m, MonadState IState m) =>
String -> m ()
keyword "rewrite" StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn)
                 PDo -> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> PDo
forall t. FC -> t -> PDo' t
DoRewrite FC
fc PTerm
sc))
   StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do (i :: Name
i, ifc :: FC
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
                 String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "<-"
                 (e :: PTerm
e, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False });
                 PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (FC -> Name -> FC -> PTerm -> PDo
forall t. FC -> Name -> FC -> t -> PDo' t
DoBind FC
fc Name
i FC
ifc PTerm
e)
                          (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '|'
                              [(PTerm, PTerm)]
ts <- IdrisParser (PTerm, PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [(PTerm, PTerm)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser (PTerm, PTerm)
do_alt (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })) (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '|')
                              PDo -> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> PTerm -> [(PTerm, PTerm)] -> PDo
forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoBindP FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
ifc [FC
ifc] Name
i) PTerm
e [(PTerm, PTerm)]
ts)))
   StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (do PTerm
i <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
                 String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "<-"
                 (e :: PTerm
e, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False });
                 PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (FC -> PTerm -> PTerm -> [(PTerm, PTerm)] -> PDo
forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoBindP FC
fc PTerm
i PTerm
e [])
                          (do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '|'
                              [(PTerm, PTerm)]
ts <- IdrisParser (PTerm, PTerm)
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [(PTerm, PTerm)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser (PTerm, PTerm)
do_alt (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })) (Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '|')
                              PDo -> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> PTerm -> [(PTerm, PTerm)] -> PDo
forall t. FC -> t -> t -> [(t, t)] -> PDo' t
DoBindP FC
fc PTerm
i PTerm
e [(PTerm, PTerm)]
ts)))
   StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
-> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> do (e :: PTerm
e, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
          PDo -> StateT IState (WriterT FC (Parsec Void String)) PDo
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> PDo
forall t. FC -> t -> PDo' t
DoExp FC
fc PTerm
e)
   StateT IState (WriterT FC (Parsec Void String)) PDo
-> String -> StateT IState (WriterT FC (Parsec Void String)) PDo
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "do block expression"

do_alt :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
do_alt syn :: SyntaxInfo
syn = do PTerm
l <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
                (PTerm, PTerm)
-> IdrisParser (PTerm, PTerm) -> IdrisParser (PTerm, PTerm)
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option (PTerm
Placeholder, PTerm
l)
                         (do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "=>"
                             PTerm
r <- SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
                             (PTerm, PTerm) -> IdrisParser (PTerm, PTerm)
forall (m :: * -> *) a. Monad m => a -> m a
return (PTerm
l, PTerm
r))

{- | Parses an expression in idiom brackets
@
Idiom ::= '[|' Expr '|]';
@
-}
idiom :: SyntaxInfo -> IdrisParser PTerm
idiom :: SyntaxInfo -> IdrisParser PTerm
idiom syn :: SyntaxInfo
syn
    = do String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "[|"
         (e :: PTerm
e, fc :: FC
fc) <- IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall (m :: * -> *) a. MonadWriter FC m => m a -> m (a, FC)
withExtent (IdrisParser PTerm
 -> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC))
-> IdrisParser PTerm
-> StateT IState (WriterT FC (Parsec Void String)) (PTerm, FC)
forall a b. (a -> b) -> a -> b
$ SyntaxInfo -> IdrisParser PTerm
expr (SyntaxInfo
syn { withAppAllowed :: Bool
withAppAllowed = Bool
False })
         String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
symbol "|]"
         PTerm -> IdrisParser PTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (FC -> PTerm -> PTerm
PIdiom FC
fc PTerm
e)
      IdrisParser PTerm -> String -> IdrisParser PTerm
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "expression in idiom brackets"

{- |Parses a constant or literal expression

@
Constant ::=
    'Integer'
  | 'Int'
  | 'Char'
  | 'Double'
  | 'String'
  | 'Bits8'
  | 'Bits16'
  | 'Bits32'
  | 'Bits64'
  | Float_t
  | Natural_t
  | VerbatimString_t
  | String_t
  | Char_t
  ;
@
-}

constants :: [(String, Idris.Core.TT.Const)]
constants :: [(String, Const)]
constants =
  [ ("Integer",            ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITBig))
  , ("Int",                ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITNative))
  , ("Char",               ArithTy -> Const
AType (IntTy -> ArithTy
ATInt IntTy
ITChar))
  , ("Double",             ArithTy -> Const
AType ArithTy
ATFloat)
  , ("String",             Const
StrType)
  , ("prim__WorldType",    Const
WorldType)
  , ("prim__TheWorld",     Const
TheWorld)
  , ("Bits8",              ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT8)))
  , ("Bits16",             ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT16)))
  , ("Bits32",             ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT32)))
  , ("Bits64",             ArithTy -> Const
AType (IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT64)))
  ]

-- | Parse a constant and its source span
constant :: Parsing m => m Idris.Core.TT.Const
constant :: m Const
constant = [m Const] -> m Const
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice [ Const
ty Const -> m () -> m Const
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> m ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved String
name | (name :: String
name, ty :: Const
ty) <- [(String, Const)]
constants ]
       m Const -> m Const -> m Const
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m Const -> m Const
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Double -> Const
Fl (Double -> Const) -> m Double -> m Const
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Double
forall (m :: * -> *). Parsing m => m Double
float)
       m Const -> m Const -> m Const
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Integer -> Const
BI (Integer -> Const) -> m Integer -> m Const
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Integer
forall (m :: * -> *). Parsing m => m Integer
natural
       m Const -> m Const -> m Const
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Const
Str (String -> Const) -> m String -> m Const
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m String
forall (m :: * -> *). Parsing m => m String
verbatimStringLiteral
       m Const -> m Const -> m Const
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Const
Str (String -> Const) -> m String -> m Const
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m String
forall (m :: * -> *). Parsing m => m String
stringLiteral
       m Const -> m Const -> m Const
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> m Const -> m Const
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (Char -> Const
Ch (Char -> Const) -> m Char -> m Const
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Char
forall (m :: * -> *). Parsing m => m Char
charLiteral) --Currently ambigous with symbols
       m Const -> String -> m Const
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "constant or literal"

{- | Parses a verbatim multi-line string literal (triple-quoted)

@
VerbatimString_t ::=
  '\"\"\"' ~'\"\"\"' '\"'* '\"\"\"'
;
@
 -}
verbatimStringLiteral :: Parsing m => m String
verbatimStringLiteral :: m String
verbatimStringLiteral = m String -> m String
forall (m :: * -> *) a. Parsing m => m a -> m a
token (m String -> m String) -> m String -> m String
forall a b. (a -> b) -> a -> b
$ do m String -> m String
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (m String -> m String) -> m String -> m String
forall a b. (a -> b) -> a -> b
$ String -> m String
forall (m :: * -> *). Parsing m => String -> m String
string "\"\"\""
                                   String
str <- m Char -> m String -> m String
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.manyTill m Char
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
P.anySingle (m String -> m String) -> m String -> m String
forall a b. (a -> b) -> a -> b
$ m String -> m String
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
P.try (String -> m String
forall (m :: * -> *). Parsing m => String -> m String
string "\"\"\"")
                                   String
moreQuotes <- m Char -> m String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
P.many (m Char -> m String) -> m Char -> m String
forall a b. (a -> b) -> a -> b
$ Token String -> m (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
P.char Token String
'"'
                                   String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
moreQuotes

{- | Parses a static modifier

@
Static ::=
  '%static'
;
@
-}
static :: IdrisParser Static
static :: IdrisParser Static
static =     Static
Static Static
-> StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser Static
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => String -> m ()
reserved "%static"
         IdrisParser Static -> IdrisParser Static -> IdrisParser Static
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Static -> IdrisParser Static
forall (m :: * -> *) a. Monad m => a -> m a
return Static
Dynamic
         IdrisParser Static -> String -> IdrisParser Static
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "static modifier"

{- | Parses a tactic script

@
Tactic ::= 'intro' NameList?
       |   'intros'
       |   'refine'      Name Imp+
       |   'mrefine'     Name
       |   'rewrite'     Expr
       |   'induction'   Expr
       |   'equiv'       Expr
       |   'let'         Name ':' Expr' '=' Expr
       |   'let'         Name           '=' Expr
       |   'focus'       Name
       |   'exact'       Expr
       |   'applyTactic' Expr
       |   'reflect'     Expr
       |   'fill'        Expr
       |   'try'         Tactic '|' Tactic
       |   '{' TacticSeq '}'
       |   'compute'
       |   'trivial'
       |   'solve'
       |   'attack'
       |   'state'
       |   'term'
       |   'undo'
       |   'qed'
       |   'abandon'
       |   ':' 'q'
       ;

Imp ::= '?' | '_';

TacticSeq ::=
    Tactic ';' Tactic
  | Tactic ';' TacticSeq
  ;
@
-}

-- | A specification of the arguments that tactics can take
data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
               | ExprTArg
               | AltsTArg
               | StringLitTArg

-- The FIXMEs are Issue #1766 in the issue tracker.
--     https://github.com/idris-lang/Idris-dev/issues/1766
-- | A list of available tactics and their argument requirements
tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]
tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]
tactics =
  [ (["intro"], Maybe TacticArg
forall a. Maybe a
Nothing, IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. a -> b -> a
const (IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic)
-> IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$ -- FIXME syntax for intro (fresh name)
      do [Name]
ns <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) [Name]
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
forall (f :: * -> *) b.
(MonadFail f, MonadParsec Void String f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced 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 ','); PTactic -> IdrisParser PTactic
forall (m :: * -> *) a. Monad m => a -> m a
return (PTactic -> IdrisParser PTactic) -> PTactic -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$ [Name] -> PTactic
forall t. [Name] -> PTactic' t
Intro [Name]
ns)
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["intros"] PTactic
forall t. PTactic' t
Intros
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["unfocus"] PTactic
forall t. PTactic' t
Unfocus
  , (["refine"], TacticArg -> Maybe TacticArg
forall a. a -> Maybe a
Just TacticArg
ExprTArg, IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. a -> b -> a
const (IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic)
-> IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$
       do Name
n <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) Name
forall (f :: * -> *) b.
(MonadFail f, MonadParsec Void String f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
          [Bool]
imps <- StateT IState (WriterT FC (Parsec Void String)) Bool
-> StateT IState (WriterT FC (Parsec Void String)) [Bool]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many StateT IState (WriterT FC (Parsec Void String)) Bool
imp
          PTactic -> IdrisParser PTactic
forall (m :: * -> *) a. Monad m => a -> m a
return (PTactic -> IdrisParser PTactic) -> PTactic -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$ Name -> [Bool] -> PTactic
forall t. Name -> [Bool] -> PTactic' t
Refine Name
n [Bool]
imps)
  , (["claim"], Maybe TacticArg
forall a. Maybe a
Nothing, \syn :: SyntaxInfo
syn ->
       do Name
n <- StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) Name
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
name
          PTerm
goal <- StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
          PTactic -> IdrisParser PTactic
forall (m :: * -> *) a. Monad m => a -> m a
return (PTactic -> IdrisParser PTactic) -> PTactic -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$ Name -> PTerm -> PTactic
forall t. Name -> t -> PTactic' t
Claim Name
n PTerm
goal)
  , (["mrefine"], TacticArg -> Maybe TacticArg
forall a. a -> Maybe a
Just TacticArg
ExprTArg, IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. a -> b -> a
const (IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic)
-> IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$
       do Name
n <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) Name
forall (f :: * -> *) b.
(MonadFail f, MonadParsec Void String f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
fnName
          PTactic -> IdrisParser PTactic
forall (m :: * -> *) a. Monad m => a -> m a
return (PTactic -> IdrisParser PTactic) -> PTactic -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$ Name -> PTactic
forall t. Name -> PTactic' t
MatchRefine Name
n)
  , [String]
-> (PTerm -> PTactic)
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall a b.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) b)
expressionTactic ["rewrite"] PTerm -> PTactic
forall t. t -> PTactic' t
Rewrite
  , [String]
-> (PTerm -> PTactic)
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall a b.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) b)
expressionTactic ["equiv"] PTerm -> PTactic
forall t. t -> PTactic' t
Equiv
  , (["let"], Maybe TacticArg
forall a. Maybe a
Nothing, \syn :: SyntaxInfo
syn -> -- FIXME syntax for let
       do Name
n <- (StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) Name
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
name)
          (do StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ':'
              PTerm
ty <- StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr' SyntaxInfo
syn
              StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '='
              PTerm
t <- StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
              IState
i <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
              PTactic -> IdrisParser PTactic
forall (m :: * -> *) a. Monad m => a -> m a
return (PTactic -> IdrisParser PTactic) -> PTactic -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$ Name -> PTerm -> PTerm -> PTactic
forall t. Name -> t -> t -> PTactic' t
LetTacTy Name
n (SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
i PTerm
ty) (SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
i PTerm
t))
            IdrisParser PTactic -> IdrisParser PTactic -> IdrisParser PTactic
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (do StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt StateT IState (WriterT FC (Parsec Void String)) ()
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> StateT IState (WriterT FC (Parsec Void String)) Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '='
                    PTerm
t <- StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt StateT IState (WriterT FC (Parsec Void String)) ()
-> IdrisParser PTerm -> IdrisParser PTerm
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SyntaxInfo -> IdrisParser PTerm
expr SyntaxInfo
syn
                    IState
i <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
                    PTactic -> IdrisParser PTactic
forall (m :: * -> *) a. Monad m => a -> m a
return (PTactic -> IdrisParser PTactic) -> PTactic -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$ Name -> PTerm -> PTactic
forall t. Name -> t -> PTactic' t
LetTac Name
n (SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
i PTerm
t)))

  , (["focus"], TacticArg -> Maybe TacticArg
forall a. a -> Maybe a
Just TacticArg
ExprTArg, IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. a -> b -> a
const (IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic)
-> IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$
       do Name
n <- StateT IState (WriterT FC (Parsec Void String)) Name
-> StateT IState (WriterT FC (Parsec Void String)) Name
forall (f :: * -> *) b.
(MonadFail f, MonadParsec Void String f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced StateT IState (WriterT FC (Parsec Void String)) Name
forall (m :: * -> *). (Parsing m, MonadState IState m) => m Name
name
          PTactic -> IdrisParser PTactic
forall (m :: * -> *) a. Monad m => a -> m a
return (PTactic -> IdrisParser PTactic) -> PTactic -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$ Name -> PTactic
forall t. Name -> PTactic' t
Focus Name
n)
  , [String]
-> (PTerm -> PTactic)
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall a b.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) b)
expressionTactic ["exact"] PTerm -> PTactic
forall t. t -> PTactic' t
Exact
  , [String]
-> (PTerm -> PTactic)
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall a b.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) b)
expressionTactic ["applyTactic"] PTerm -> PTactic
forall t. t -> PTactic' t
ApplyTactic
  , [String]
-> (PTerm -> PTactic)
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall a b.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) b)
expressionTactic ["byReflection"] PTerm -> PTactic
forall t. t -> PTactic' t
ByReflection
  , [String]
-> (PTerm -> PTactic)
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall a b.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) b)
expressionTactic ["reflect"] PTerm -> PTactic
forall t. t -> PTactic' t
Reflect
  , [String]
-> (PTerm -> PTactic)
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall a b.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) b)
expressionTactic ["fill"] PTerm -> PTactic
forall t. t -> PTactic' t
Fill
  , (["try"], TacticArg -> Maybe TacticArg
forall a. a -> Maybe a
Just TacticArg
AltsTArg, \syn :: SyntaxInfo
syn ->
        do PTactic
t <- IdrisParser PTactic -> IdrisParser PTactic
forall (f :: * -> *) b.
(MonadFail f, MonadParsec Void String f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced (SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn)
           Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '|'
           PTactic
t1 <- IdrisParser PTactic -> IdrisParser PTactic
forall (f :: * -> *) b.
(MonadFail f, MonadParsec Void String f, MonadWriter FC f,
 MonadState IState f) =>
f b -> f b
spaced (SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn)
           PTactic -> IdrisParser PTactic
forall (m :: * -> *) a. Monad m => a -> m a
return (PTactic -> IdrisParser PTactic) -> PTactic -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$ PTactic -> PTactic -> PTactic
forall t. PTactic' t -> PTactic' t -> PTactic' t
Try PTactic
t PTactic
t1)
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["compute"] PTactic
forall t. PTactic' t
Compute
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["trivial"] PTactic
forall t. PTactic' t
Trivial
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["unify"] PTactic
forall t. PTactic' t
DoUnify
  , (["search"], Maybe TacticArg
forall a. Maybe a
Nothing, IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. a -> b -> a
const (IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic)
-> IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$
      do Integer
depth <- Integer
-> StateT IState (WriterT FC (Parsec Void String)) Integer
-> StateT IState (WriterT FC (Parsec Void String)) Integer
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
P.option 10 StateT IState (WriterT FC (Parsec Void String)) Integer
forall (m :: * -> *). Parsing m => m Integer
natural
         PTactic -> IdrisParser PTactic
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic
forall t.
Bool -> Bool -> Int -> Maybe Name -> [Name] -> [Name] -> PTactic' t
ProofSearch Bool
True Bool
True (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
depth) Maybe Name
forall a. Maybe a
Nothing [] []))
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["implementation"] PTactic
forall t. PTactic' t
TCImplementation
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["solve"] PTactic
forall t. PTactic' t
Solve
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["attack"] PTactic
forall t. PTactic' t
Attack
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["state", ":state"] PTactic
forall t. PTactic' t
ProofState
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["term", ":term"] PTactic
forall t. PTactic' t
ProofTerm
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["undo", ":undo"] PTactic
forall t. PTactic' t
Undo
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["qed", ":qed"] PTactic
forall t. PTactic' t
Qed
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["abandon", ":q"] PTactic
forall t. PTactic' t
Abandon
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["skip"] PTactic
forall t. PTactic' t
Skip
  , [String]
-> PTactic
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall (m :: * -> *) a a a b.
Monad m =>
a -> a -> (a, Maybe a, b -> m a)
noArgs ["sourceLocation"] PTactic
forall t. PTactic' t
SourceFC
  , [String]
-> (PTerm -> PTactic)
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall a b.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) b)
expressionTactic [":e", ":eval"] PTerm -> PTactic
forall t. t -> PTactic' t
TEval
  , [String]
-> (PTerm -> PTactic)
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall a b.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) b)
expressionTactic [":t", ":type"] PTerm -> PTactic
forall t. t -> PTactic' t
TCheck
  , [String]
-> (PTerm -> PTactic)
-> ([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)
forall a b.
a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) b)
expressionTactic [":search"] PTerm -> PTactic
forall t. t -> PTactic' t
TSearch
  , (["fail"], TacticArg -> Maybe TacticArg
forall a. a -> Maybe a
Just TacticArg
StringLitTArg, IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. a -> b -> a
const (IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic)
-> IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$
       do String
msg <- StateT IState (WriterT FC (Parsec Void String)) String
forall (m :: * -> *). Parsing m => m String
stringLiteral
          PTactic -> IdrisParser PTactic
forall (m :: * -> *) a. Monad m => a -> m a
return (PTactic -> IdrisParser PTactic) -> PTactic -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$ [ErrorReportPart] -> PTactic
forall t. [ErrorReportPart] -> PTactic' t
TFail [String -> ErrorReportPart
Idris.Core.TT.TextPart String
msg])
  , ([":doc"], TacticArg -> Maybe TacticArg
forall a. a -> Maybe a
Just TacticArg
ExprTArg, IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. a -> b -> a
const (IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic)
-> IdrisParser PTactic -> SyntaxInfo -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$
       do StateT IState (WriterT FC (Parsec Void String)) ()
forall (m :: * -> *). Parsing m => m ()
whiteSpace
          Either Name Const
doc <- (Const -> Either Name Const
forall a b. b -> Either a b
Right (Const -> Either Name Const)
-> StateT IState (WriterT FC (Parsec Void String)) Const
-> 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)) 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 (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)
          StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
          PTactic -> IdrisParser PTactic
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Name Const -> PTactic
forall t. Either Name Const -> PTactic' t
TDocStr Either Name Const
doc))
  ]
  where
  expressionTactic :: a
-> (PTerm -> b)
-> (a, Maybe TacticArg,
    SyntaxInfo -> StateT IState (WriterT FC (Parsec Void String)) b)
expressionTactic names :: a
names tactic :: PTerm -> b
tactic = (a
names, TacticArg -> Maybe TacticArg
forall a. a -> Maybe a
Just TacticArg
ExprTArg, \syn :: SyntaxInfo
syn ->
     do PTerm
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
syn)
        IState
i <- StateT IState (WriterT FC (Parsec Void String)) IState
forall s (m :: * -> *). MonadState s m => m s
get
        b -> StateT IState (WriterT FC (Parsec Void String)) b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> StateT IState (WriterT FC (Parsec Void String)) b)
-> b -> StateT IState (WriterT FC (Parsec Void String)) b
forall a b. (a -> b) -> a -> b
$ PTerm -> b
tactic (SyntaxInfo -> IState -> PTerm -> PTerm
desugar SyntaxInfo
syn IState
i PTerm
t))
  noArgs :: a -> a -> (a, Maybe a, b -> m a)
noArgs names :: a
names tactic :: a
tactic = (a
names, Maybe a
forall a. Maybe a
Nothing, m a -> b -> m a
forall a b. a -> b -> a
const (a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
tactic))
  spaced :: f b -> f b
spaced parser :: f b
parser = f ()
forall (m :: * -> *). (Parsing m, MonadState IState m) => m ()
indentGt f () -> f b -> f b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> f b
parser
  imp :: IdrisParser Bool
  imp :: StateT IState (WriterT FC (Parsec Void String)) Bool
imp = do Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '?'; Bool -> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
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 (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 '_'; Bool -> StateT IState (WriterT FC (Parsec Void String)) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True


tactic :: SyntaxInfo -> IdrisParser PTactic
tactic :: SyntaxInfo -> IdrisParser PTactic
tactic syn :: SyntaxInfo
syn = [IdrisParser PTactic] -> IdrisParser PTactic
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
P.choice [ 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
P.choice ((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]
names); SyntaxInfo -> IdrisParser PTactic
parser SyntaxInfo
syn
                      | (names :: [String]
names, _, parser :: SyntaxInfo -> IdrisParser PTactic
parser) <- [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]
tactics ]
          IdrisParser PTactic -> IdrisParser PTactic -> IdrisParser PTactic
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 '{'
                 PTactic
t <- SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn;
                 Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ';';
                 [PTactic]
ts <- IdrisParser PTactic
-> StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser [PTactic]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
P.sepBy1 (SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn) (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
forall (m :: * -> *). Parsing m => Char -> m Char
lchar '}'
                 PTactic -> IdrisParser PTactic
forall (m :: * -> *) a. Monad m => a -> m a
return (PTactic -> IdrisParser PTactic) -> PTactic -> IdrisParser PTactic
forall a b. (a -> b) -> a -> b
$ PTactic -> PTactic -> PTactic
forall t. PTactic' t -> PTactic' t -> PTactic' t
TSeq PTactic
t ([PTactic] -> PTactic
mergeSeq [PTactic]
ts)
          IdrisParser PTactic -> IdrisParser PTactic -> IdrisParser PTactic
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((Char -> StateT IState (WriterT FC (Parsec Void String)) Char
forall (m :: * -> *). Parsing m => Char -> m Char
lchar ':' StateT IState (WriterT FC (Parsec Void String)) Char
-> IdrisParser PTactic -> IdrisParser PTactic
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IdrisParser PTactic
forall (f :: * -> *) a. Alternative f => f a
empty) IdrisParser PTactic -> String -> IdrisParser PTactic
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "prover command")
          IdrisParser PTactic -> String -> IdrisParser PTactic
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "tactic"
  where
    mergeSeq :: [PTactic] -> PTactic
    mergeSeq :: [PTactic] -> PTactic
mergeSeq [t :: PTactic
t]    = PTactic
t
    mergeSeq (t :: PTactic
t:ts :: [PTactic]
ts) = PTactic -> PTactic -> PTactic
forall t. PTactic' t -> PTactic' t -> PTactic' t
TSeq PTactic
t ([PTactic] -> PTactic
mergeSeq [PTactic]
ts)

-- | Parses a tactic as a whole
fullTactic :: SyntaxInfo -> IdrisParser PTactic
fullTactic :: SyntaxInfo -> IdrisParser PTactic
fullTactic syn :: SyntaxInfo
syn = do PTactic
t <- SyntaxInfo -> IdrisParser PTactic
tactic SyntaxInfo
syn
                    StateT IState (WriterT FC (Parsec Void String)) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
P.eof
                    PTactic -> IdrisParser PTactic
forall (m :: * -> *) a. Monad m => a -> m a
return PTactic
t