{-# 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
allowImp :: SyntaxInfo -> SyntaxInfo
allowImp :: SyntaxInfo -> SyntaxInfo
allowImp syn :: SyntaxInfo
syn = SyntaxInfo
syn { implicitAllowed :: Bool
implicitAllowed = Bool
True,
constraintAllowed :: Bool
constraintAllowed = Bool
False }
disallowImp :: SyntaxInfo -> SyntaxInfo
disallowImp :: SyntaxInfo -> SyntaxInfo
disallowImp = SyntaxInfo -> SyntaxInfo
scopedImp
scopedImp :: SyntaxInfo -> SyntaxInfo
scopedImp :: SyntaxInfo -> SyntaxInfo
scopedImp syn :: SyntaxInfo
syn = SyntaxInfo
syn { implicitAllowed :: Bool
implicitAllowed = Bool
False,
constraintAllowed :: Bool
constraintAllowed = Bool
False }
allowConstr :: SyntaxInfo -> SyntaxInfo
allowConstr :: SyntaxInfo -> SyntaxInfo
allowConstr syn :: SyntaxInfo
syn = SyntaxInfo
syn { constraintAllowed :: Bool
constraintAllowed = Bool
True }
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 ""
expr :: SyntaxInfo -> IdrisParser PTerm
expr :: SyntaxInfo -> IdrisParser PTerm
expr = SyntaxInfo -> IdrisParser PTerm
pi
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))
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"
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
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
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
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
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
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
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]
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 :: 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
update ns :: [(Name, SynMatch)]
ns t :: PTerm
t = PTerm
t
updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic
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
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"
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"
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"
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.")
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"
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"
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"
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 })
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
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)
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)
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
$
[(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
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)
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"
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"
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"
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)]
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"
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
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
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"
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"
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"
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 }
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"
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"
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"
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)]
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
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"
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
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"
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
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
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"
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"
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
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"
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 []
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"
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"
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"
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
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"
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 })
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))
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"
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)))
]
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)
m Const -> String -> m Const
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> "constant or literal"
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
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"
data TacticArg = NameTArg
| ExprTArg
| AltsTArg
| StringLitTArg
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
$
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 ->
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)
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