idris-0.9.9.2: src/Idris/Parser.hs
{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
module Idris.Parser where
import Prelude hiding (pi)
import Text.Trifecta.Delta
import Text.Trifecta hiding (span, token, whiteSpace, stringLiteral, charLiteral, natural, symbol, char, string)
import Text.Parser.LookAhead
import Text.Parser.Expression
import qualified Text.Parser.Token as Tok
import qualified Text.Parser.Char as Chr
import qualified Text.Parser.Token.Highlight as Hi
import Idris.AbsSyntax
import Idris.DSL
import Idris.Imports
import Idris.Error
import Idris.ElabDecls
import Idris.ElabTerm hiding (namespace, params)
import Idris.Coverage
import Idris.IBC
import Idris.Unlit
import Idris.Providers
import Paths_idris
import Util.DynamicLinker
import Core.TT
import Core.Evaluate
import Control.Applicative
import Control.Monad
import Control.Monad.State.Strict
import Data.Maybe
import qualified Data.List.Split as Spl
import Data.List
import Data.Monoid
import Data.Char
import qualified Data.HashSet as HS
import qualified Data.Text as T
import qualified Data.ByteString.UTF8 as UTF8
import Debug.Trace
import System.FilePath
{-
grammar shortcut notation:
~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ)
RULE? = optional rule (i.e. RULE or nothing)
RULE* = repeated rule (i.e. RULE zero or more times)
RULE+ = repeated rule with at least one match (i.e. RULE one or more times)
RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case)
RULE{n} = rule repeated n times
-}
-- | Idris parser with state used during parsing
type IdrisParser = StateT IState Parser
-- | Generalized monadic parsing constraint type
type MonadicParsing m = (DeltaParsing m, LookAheadParsing m, TokenParsing m, Monad m)
{- * Space, comments and literals (token/lexing like parsers) -}
-- | Parses a token by applying parser and then consuming all following whiteSpace
lexeme :: MonadicParsing m => m a -> m a
lexeme p = p <* whiteSpace
-- | Consumes any simple whitespace (any character which satisfies Char.isSpace)
simpleWhiteSpace :: MonadicParsing m => m ()
simpleWhiteSpace = satisfy isSpace *> pure ()
-- | Checks if a charcter is end of line
isEol :: Char -> Bool
isEol '\n' = True
isEol '\0' = True -- Check eof too
isEol _ = False
-- | Checks if a character is a documentation comment marker
isDocCommentMarker :: Char -> Bool
isDocCommentMarker '|' = True
isDocCommentMarker '^' = True
isDocCommentMarker _ = False
{- | Consumes a single-line comment
SingleLineComment_t ::= '--' EOL_t
| '--' ~DocCommentMarker_t ~EOL_t* EOL_t
;
-}
singleLineComment :: MonadicParsing m => m ()
singleLineComment = try (string "--" *> satisfy isEol *> pure ())
<|> try (string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> (satisfy isEol <?> "end of line") *> pure ())
<?> "single-line comment"
{- | Consumes a multi-line comment
MultiLineComment_t ::=
'{ -- }'
| '{ -' ~DocCommentMarker_t InCommentChars_t
;
InCommentChars_t ::=
'- }'
| MultiLineComment_t InCommentChars_t
| ~'- }'+ InCommentChars_t
;
-}
multiLineComment :: MonadicParsing m => m ()
multiLineComment = try (string "{-" *> (string "-}") *> pure ())
<|> try (string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars)
<?> "multi-line comment"
where inCommentChars :: MonadicParsing m => m ()
inCommentChars = try (string "-}" *> pure ())
<|> try (multiLineComment *> inCommentChars)
<|> try (docComment '|' *> inCommentChars)
<|> try (docComment '^' *> inCommentChars)
<|> try (skipSome (noneOf startEnd) *> inCommentChars)
<|> oneOf startEnd *> inCommentChars
<?> "end of comment"
startEnd :: String
startEnd = "{}-"
{-| Parses a documentation comment (similar to haddoc) given a marker character
DocComment_t ::= '--' DocCommentMarker_t ~EOL_t* EOL_t
| '{ -' DocCommentMarket_t ~'- }'* '- }'
;
-}
docComment :: MonadicParsing m => Char -> m String
docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; return (T.unpack $ T.strip $ T.pack dc)
| otherwise = fail "internal error: tried to parse a documentation comment with invalid marker"
where docComment' :: MonadicParsing m => Char -> m String
docComment' marker = string "--" *> char marker *> many (satisfy (not . isEol)) <* satisfy isEol
<|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")
<?> "documentation comment"
-- | Consumes whitespace (and comments)
whiteSpace :: MonadicParsing m => m ()
whiteSpace = many (simpleWhiteSpace <|> singleLineComment <|> multiLineComment) *> pure ()
-- | Parses a string literal
stringLiteral :: MonadicParsing m => m String
stringLiteral = lexeme $ Tok.stringLiteral
-- | Parses a char literal
charLiteral :: MonadicParsing m => m Char
charLiteral = lexeme $ Tok.charLiteral
-- | Parses a natural number
natural :: MonadicParsing m => m Integer
natural = lexeme $ Tok.natural
-- | Parses an integral number
integer :: MonadicParsing m => m Integer
integer = lexeme $ Tok.integer
-- | Parses a floating point number
float :: MonadicParsing m => m Double
float = lexeme $ Tok.double
{- * Symbols, identifiers, names and operators -}
-- | Idris Style for parsing identifiers/reserved keywords
idrisStyle :: MonadicParsing m => IdentifierStyle m
idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved Hi.Identifier Hi.ReservedIdentifier
where _styleName = "Idris"
_styleStart = satisfy isAlpha
_styleLetter = satisfy isAlphaNum <|> oneOf "_'" <|> (lchar '.')
_styleReserved = HS.fromList ["let", "in", "data", "codata", "record", "Type",
"do", "dsl", "import", "impossible",
"case", "of", "total", "partial", "mutual",
"infix", "infixl", "infixr", "rewrite",
"where", "with", "syntax", "proof", "postulate",
"using", "namespace", "class", "instance",
"public", "private", "abstract", "implicit",
"quoteGoal",
"Int", "Integer", "Float", "Char", "String", "Ptr",
"Bits8", "Bits16", "Bits32", "Bits64",
"Bits8x16", "Bits16x8", "Bits32x4", "Bits64x2"]
char :: MonadicParsing m => Char -> m Char
char = Chr.char
string :: MonadicParsing m => String -> m String
string = Chr.string
-- | Parses a character as a lexeme
lchar :: MonadicParsing m => Char -> m Char
lchar = lexeme . char
-- | Parses string as a lexeme
symbol :: MonadicParsing m => String -> m String
symbol = lexeme . Tok.symbol
-- | Parses a reserved identifier
reserved :: MonadicParsing m => String -> m ()
reserved = lexeme . Tok.reserve idrisStyle
-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007
-- | Parses a reserved operator
reservedOp :: MonadicParsing m => String -> m ()
reservedOp name = lexeme $ try $
do string name
notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
-- | Parses an identifier as a lexeme
identifier :: MonadicParsing m => m String
identifier = lexeme $ Tok.ident idrisStyle
-- | Parses an identifier with possible namespace as a name
iName :: MonadicParsing m => [String] -> m Name
iName bad = maybeWithNS identifier False bad <?> "name"
-- | Parses an string possibly prefixed by a namespace
maybeWithNS :: MonadicParsing m => m String -> Bool -> [String] -> m Name
maybeWithNS parser ascend bad = do
i <- option "" (lookAhead identifier)
when (i `elem` bad) $ unexpected "reserved identifier"
let transf = if ascend then id else reverse
(x, xs) <- choice (transf (parserNoNS parser : parsersNS parser i))
return $ mkName (x, xs)
where parserNoNS :: MonadicParsing m => m String -> m (String, String)
parserNoNS parser = do x <- parser; return (x, "")
parserNS :: MonadicParsing m => m String -> String -> m (String, String)
parserNS parser ns = do xs <- string ns; lchar '.'; x <- parser; return (x, xs)
parsersNS :: MonadicParsing m => m String -> String -> [m (String, String)]
parsersNS parser i = [try (parserNS parser ns) | ns <- (initsEndAt (=='.') i)]
-- | Parses a name
name :: IdrisParser Name
name = do i <- get
iName (syntax_keywords i)
<?> "name"
{- | List of all initial segments in ascending order of a list. Every such
initial segment ends right before an element satisfying the given
condition.
-}
initsEndAt :: (a -> Bool) -> [a] -> [[a]]
initsEndAt p [] = []
initsEndAt p (x:xs) | p x = [] : x_inits_xs
| otherwise = x_inits_xs
where x_inits_xs = [x : cs | cs <- initsEndAt p xs]
{- | Create a `Name' from a pair of strings representing a base name and its
namespace.
-}
mkName :: (String, String) -> Name
mkName (n, "") = UN n
mkName (n, ns) = NS (UN n) (reverse (parseNS ns))
where parseNS x = case span (/= '.') x of
(x, "") -> [x]
(x, '.':y) -> x : parseNS y
operatorLetter :: MonadicParsing m => m Char
operatorLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"
-- | Parses an operator
operator :: MonadicParsing m => m String
operator = lexeme . some $ operatorLetter
{- * Position helpers -}
{- | Get filename from position (returns "(interactive)" when no source file is given) -}
fileName :: Delta -> String
fileName (Directed fn _ _ _ _) = UTF8.toString fn
fileName _ = "(interactive)"
{- | Get line number from position -}
lineNum :: Delta -> Int
lineNum (Lines l _ _ _) = fromIntegral l + 1
lineNum (Directed _ l _ _ _) = fromIntegral l + 1
{- | Get file position as FC -}
getFC :: MonadicParsing m => m FC
getFC = do s <- position
let (dir, file) = splitFileName (fileName s)
let f = if dir == addTrailingPathSeparator "." then file else fileName s
return $ FC f (lineNum s)
{-* Syntax helpers-}
-- | Bind constraints to term
bindList :: (Name -> PTerm -> PTerm -> PTerm) -> [(Name, PTerm)] -> PTerm -> PTerm
bindList b [] sc = sc
bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
{- |Creates table for fixtiy declarations to build expression parser using
pre-build and user-defined operator/fixity declarations -}
table :: [FixDecl] -> OperatorTable IdrisParser PTerm
table fixes
= [[prefix "-" (\fc x -> PApp fc (PRef fc (UN "-"))
[pexp (PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]
++ toTable (reverse fixes) ++
[[backtick],
[binary "=" PEq AssocLeft],
[binary "->" (\fc x y -> PPi expl (MN 42 "__pi_arg") x y) AssocRight]]
{- |Calculates table for fixtiy declarations -}
toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm
toTable fs = map (map toBin)
(groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)
where toBin (Fix (PrefixN _) op) = prefix op
(\fc x -> PApp fc (PRef fc (UN op)) [pexp x])
toBin (Fix f op)
= binary op (\fc x y -> PApp fc (PRef fc (UN op)) [pexp x,pexp y]) (assoc f)
assoc (Infixl _) = AssocLeft
assoc (Infixr _) = AssocRight
assoc (InfixN _) = AssocNone
{- |Binary operator -}
binary :: String -> (FC -> PTerm -> PTerm -> PTerm) -> Assoc -> Operator IdrisParser PTerm
binary name f = Infix (do fc <- getFC
reservedOp name
doc <- option "" (docComment '^')
return (f fc))
{- |Prefix operator -}
prefix :: String -> (FC -> PTerm -> PTerm) -> Operator IdrisParser PTerm
prefix name f = Prefix (do reservedOp name
fc <- getFC
return (f fc))
{- |Backtick operator -}
backtick :: Operator IdrisParser PTerm
backtick = Infix (do lchar '`'; n <- fnName
lchar '`'
fc <- getFC
return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone
-- | Allow implicit type declarations
allowImp :: SyntaxInfo -> SyntaxInfo
allowImp syn = syn { implicitAllowed = True }
-- | Disallow implicit type declarations
disallowImp :: SyntaxInfo -> SyntaxInfo
disallowImp syn = syn { implicitAllowed = False }
-- | Adds accessibility option for function
addAcc :: Name -> Maybe Accessibility -> IdrisParser ()
addAcc n a = do i <- get
put (i { hide_list = (n, a) : hide_list i })
{- | Add accessbility option for data declarations
(works for classes too - 'abstract' means the data/class is visible but members not) -}
accData :: Maybe Accessibility -> Name -> [Name] -> IdrisParser ()
accData (Just Frozen) n ns = do addAcc n (Just Frozen)
mapM_ (\n -> addAcc n (Just Hidden)) ns
accData a n ns = do addAcc n a
mapM_ (`addAcc` a) ns
{- * Error reporting helpers -}
{- | Error message with possible fixes list -}
fixErrorMsg :: String -> [String] -> String
fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)
{- * Layout helpers -}
-- | Push indentation to stack
pushIndent :: IdrisParser ()
pushIndent = do pos <- position
ist <- get
put (ist { indent_stack = (fromIntegral (column pos) + 1) : indent_stack ist })
-- | Pops indentation from stack
popIndent :: IdrisParser ()
popIndent = do ist <- get
let (x : xs) = indent_stack ist
put (ist { indent_stack = xs })
-- | Gets current indentation
indent :: IdrisParser Int
indent = liftM ((+1) . fromIntegral . column) position
-- | Gets last indentation
lastIndent :: IdrisParser Int
lastIndent = do ist <- get
case indent_stack ist of
(x : xs) -> return x
_ -> return 1
-- | Applies parser in an indented position
indented :: IdrisParser a -> IdrisParser a
indented p = notEndBlock *> p <* keepTerminator
-- | Applies parser to get a block (which has possibly indented statements)
indentedBlock :: IdrisParser a -> IdrisParser [a]
indentedBlock p = do openBlock
pushIndent
res <- many (indented p)
popIndent
closeBlock
return res
-- | Applies parser to get a block with at least one statement (which has possibly indented statements)
indentedBlock1 :: IdrisParser a -> IdrisParser [a]
indentedBlock1 p = do openBlock
pushIndent
res <- some (indented p)
popIndent
closeBlock
return res
-- | Applies parser to get a block with exactly one (possibly indented) statement
indentedBlockS :: IdrisParser a -> IdrisParser a
indentedBlockS p = do openBlock
pushIndent
res <- indented p
popIndent
closeBlock
return res
-- | Checks if the following character matches provided parser
lookAheadMatches :: MonadicParsing m => m a -> m Bool
lookAheadMatches p = do match <- lookAhead (optional p)
return $ isJust match
-- | Parses a start of block
openBlock :: IdrisParser ()
openBlock = do lchar '{'
ist <- get
put (ist { brace_stack = Nothing : brace_stack ist })
<|> do ist <- get
lvl' <- indent
-- if we're not indented further, it's an empty block, so
-- increment lvl to ensure we get to the end
let lvl = case brace_stack ist of
Just lvl_old : _ ->
if lvl' <= lvl_old then lvl_old+1
else lvl'
[] -> if lvl' == 1 then 2 else lvl'
_ -> lvl'
put (ist { brace_stack = Just lvl : brace_stack ist })
<?> "start of block"
-- | Parses an end of block
closeBlock :: IdrisParser ()
closeBlock = do ist <- get
bs <- case brace_stack ist of
[] -> eof >> return []
Nothing : xs -> lchar '}' >> return xs <?> "end of block"
Just lvl : xs -> (do i <- indent
isParen <- lookAheadMatches (char ')')
if i >= lvl && not isParen
then fail "not end of block"
else return xs)
<|> (do notOpenBraces
eof
return [])
put (ist { brace_stack = bs })
-- | Parses a terminator
terminator :: IdrisParser ()
terminator = do lchar ';'; popIndent
<|> do c <- indent; l <- lastIndent
if c <= l then popIndent else fail "not a terminator"
<|> do isParen <- lookAheadMatches (oneOf ")}")
if isParen then popIndent else fail "not a termiantor"
<|> lookAhead eof
-- | Parses and keeps a terminator
keepTerminator :: IdrisParser ()
keepTerminator = do lchar ';'; return ()
<|> do c <- indent; l <- lastIndent
unless (c <= l) $ fail "not a terminator"
<|> do isParen <- lookAheadMatches (oneOf ")}|")
unless isParen $ fail "not a terminator"
<|> lookAhead eof
-- | Checks if application expression does not end
notEndApp :: IdrisParser ()
notEndApp = do c <- indent; l <- lastIndent
when (c <= l) (fail "terminator")
-- | Checks that it is not end of block
notEndBlock :: IdrisParser ()
notEndBlock = do ist <- get
case brace_stack ist of
Just lvl : xs -> do i <- indent
isParen <- lookAheadMatches (char ')')
when (i < lvl || isParen) (fail "end of block")
_ -> return ()
notOpenBraces :: IdrisParser ()
notOpenBraces = do ist <- get
when (hasNothing $ brace_stack ist) $ fail "end of input"
where hasNothing :: [Maybe a] -> Bool
hasNothing = any isNothing
{- * Main grammar -}
{- | Parses module definition
ModuleHeader ::= 'module' Identifier_t ';'?;
-}
moduleHeader :: IdrisParser [String]
moduleHeader = try (do reserved "module"
i <- identifier
option ';' (lchar ';')
return (moduleName i))
<|> return []
where moduleName x = case span (/='.') x of
(x, "") -> [x]
(x, '.':y) -> x : moduleName y
{- | Parses an import statement
Import ::= 'import' Identifier_t ';'?;
-}
import_ :: IdrisParser String
import_ = do reserved "import"
id <- identifier
option ';' (lchar ';')
return (toPath id)
<?> "import statement"
where toPath f = foldl1' (</>) (Spl.splitOn "." f)
{- | Parses program source
Prog ::= Decl* EOF;
-}
prog :: SyntaxInfo -> IdrisParser [PDecl]
prog syn = do whiteSpace
decls <- many (decl syn)
notOpenBraces
eof
let c = (concat decls)
return c
{- | Parses a top-level declaration
Decl ::=
Decl'
| Using
| Params
| Mutual
| Namespace
| Class
| Instance
| DSL
| Directive
| Provider
| Transform
| Import!
;
-}
decl :: SyntaxInfo -> IdrisParser [PDecl]
decl syn = do notEndBlock
declBody
where declBody :: IdrisParser [PDecl]
declBody = declBody'
<|> using_ syn
<|> params syn
<|> mutual syn
<|> namespace syn
<|> class_ syn
<|> instance_ syn
<|> do d <- dsl syn; return [d]
<|> directive syn
<|> try(provider syn)
<|> transform syn
<|> try(do import_; fail "imports must be at top of file")
<?> "declaration"
declBody' :: IdrisParser [PDecl]
declBody' = do d <- decl' syn
i <- get
let d' = fmap (desugar syn i) d
return [d']
{- | Parses a top-level declaration with possible syntax sugar
Decl' ::=
Fixity
| FunDecl'
| Data
| Record
| SyntaxDecl
;
-}
decl' :: SyntaxInfo -> IdrisParser PDecl
decl' syn = try fixity
<|> try (fnDecl' syn)
<|> try (data_ syn)
<|> try (record syn)
<|> try (syntaxDecl syn)
<?> "declaration"
{- | Parses a syntax extension declaration (and adds the rule to parser state)
SyntaxDecl ::= SyntaxRule;
-}
syntaxDecl :: SyntaxInfo -> IdrisParser PDecl
syntaxDecl syn = do s <- syntaxRule syn
i <- get
let rs = syntax_rules i
let ns = syntax_keywords i
let ibc = ibc_write i
let ks = map show (names s)
put (i { syntax_rules = s : rs,
syntax_keywords = ks ++ ns,
ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc })
fc <- getFC
return (PSyntax fc s)
where names (Rule syms _ _) = mapMaybe ename syms
ename (Keyword n) = Just n
ename _ = Nothing
{- | Parses a syntax extension declaration
SyntaxRuleOpts ::= 'term' | 'pattern';
SyntaxRule ::=
SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator;
SyntaxSym ::= '[' Name_t ']'
| '{' Name_t '}'
| Name_t
| StringLiteral_t
;
-}
syntaxRule :: SyntaxInfo -> IdrisParser Syntax
syntaxRule syn
= do pushIndent
sty <- option AnySyntax (do reserved "term"; return TermSyntax
<|> do reserved "pattern"; return PatternSyntax)
reserved "syntax"
syms <- some syntaxSym
when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
let ns = mapMaybe getName syms
when (length ns /= length (nub ns))
$ unexpected "repeated variable in syntax rule"
lchar '='
tm <- typeExpr (allowImp syn)
terminator
return (Rule (mkSimple syms) tm sty)
where
isExpr (Expr _) = True
isExpr _ = False
getName (Expr n) = Just n
getName _ = Nothing
-- Can't parse two full expressions (i.e. expressions with application) in a row
-- so change them both to a simple expression
mkSimple (Expr e : es) = SimpleExpr e : mkSimple' es
mkSimple xs = mkSimple' xs
mkSimple' (Expr e : Expr e1 : es) = SimpleExpr e : SimpleExpr e1 :
mkSimple es
mkSimple' (e : es) = e : mkSimple' es
mkSimple' [] = []
{- | Parses a syntax symbol (either binding variable, keyword or expression)
SyntaxSym ::= '[' Name_t ']'
| '{' Name_t '}'
| Name_t
| StringLiteral_t
;
-}
syntaxSym :: IdrisParser SSymbol
syntaxSym = try (do lchar '['; n <- name; lchar ']'
return (Expr n))
<|> try (do lchar '{'; n <- name; lchar '}'
return (Binding n))
<|> do n <- iName []
return (Keyword n)
<|> do sym <- stringLiteral
return (Symbol sym)
<?> "syntax symbol"
{- | Parses a function declaration with possible syntax sugar
FunDecl ::= FunDecl';
-}
fnDecl :: SyntaxInfo -> IdrisParser [PDecl]
fnDecl syn
= try (do notEndBlock
d <- fnDecl' syn
i <- get
let d' = fmap (desugar syn i) d
return [d'])
<?> "function declaration"
{- Parses a function declaration
FunDecl' ::=
DocComment_t? FnOpts* Accessibility? FnOpts* FnName TypeSig Terminator
| Postulate
| Pattern
| CAF
;
-}
fnDecl' :: SyntaxInfo -> IdrisParser PDecl
fnDecl' syn = try (do doc <- option "" (docComment '|')
pushIndent
ist <- get
let initOpts = if default_total ist
then [TotalFn]
else []
opts <- fnOpts initOpts
acc <- optional accessibility
opts' <- fnOpts opts
n_in <- fnName
let n = expandNS syn n_in
fc <- getFC
ty <- typeSig (allowImp syn)
terminator
addAcc n acc
return (PTy doc syn fc opts' n ty))
<|> try (postulate syn)
<|> try (pattern syn)
<|> try (caf syn)
<?> "function declaration"
{- Parses function options given initial options
FnOpts ::= 'total'
| 'partial'
| 'implicit'
| '%' 'assert_total'
| '%' 'reflection'
| '%' 'specialise' '[' NameTimesList? ']'
;
NameTimes ::= FnName Natural?;
NameTimesList ::=
NameTimes
| NameTimes ',' NameTimesList
;
-}
-- FIXME: Check compatability for function options (i.e. partal/total)
fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
fnOpts opts
= do reserved "total"; fnOpts (TotalFn : opts)
<|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
<|> try (do lchar '%'; reserved "export"; c <- stringLiteral;
fnOpts (CExport c : opts))
<|> try (do lchar '%'; reserved "assert_total";
fnOpts (AssertTotal : opts))
<|> try (do lchar '%'; reserved "reflection";
fnOpts (Reflection : opts))
<|> do lchar '%'; reserved "specialise";
lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
fnOpts (Specialise ns : opts)
<|> do reserved "implicit"; fnOpts (Implicit : opts)
<|> return opts
<?> "function modifier"
where nameTimes :: IdrisParser (Name, Maybe Int)
nameTimes = do n <- fnName
t <- option Nothing (do reds <- natural
return (Just (fromInteger reds)))
return (n, t)
{- | Parses an operator in function position i.e. enclosed by `()', with an
optional namespace
OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';
-}
operatorFront :: IdrisParser Name
operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []
{- | Parses a function (either normal name or operator)
FnName ::= Name | OperatorFront;
-}
fnName :: IdrisParser Name
fnName = try operatorFront <|> name <?> "function name"
{- | Parses an accessibilty modifier (e.g. public, private) -}
accessibility :: IdrisParser Accessibility
accessibility = do reserved "public"; return Public
<|> do reserved "abstract"; return Frozen
<|> do reserved "private"; return Hidden
<?> "accessibility modifier"
{- | Parses a postulate
Postulate ::=
DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator
;
-}
postulate :: SyntaxInfo -> IdrisParser PDecl
postulate syn = do doc <- option "" (docComment '|')
pushIndent
reserved "postulate"
ist <- get
let initOpts = if default_total ist
then [TotalFn]
else []
opts <- fnOpts initOpts
acc <- optional accessibility
opts' <- fnOpts opts
n_in <- fnName
let n = expandNS syn n_in
ty <- typeSig (allowImp syn)
fc <- getFC
terminator
addAcc n acc
return (PPostulate doc syn fc opts' n ty)
<?> "postulate"
{- | Parses a using declaration
Using ::=
'using' '(' UsingDeclList ')' OpenBlock Decl* CloseBlock
;
-}
using_ :: SyntaxInfo -> IdrisParser [PDecl]
using_ syn =
do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'
openBlock
let uvars = using syn
ds <- many (decl (syn { using = uvars ++ ns }))
closeBlock
return (concat ds)
<?> "using declaration"
{- | Parses a parameters declaration
Params ::=
'parameters' '(' TypeDeclList ')' OpenBlock Decl* CloseBlock
;
-}
params :: SyntaxInfo -> IdrisParser [PDecl]
params syn =
do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
openBlock
let pvars = syn_params syn
ds <- many (decl syn { syn_params = pvars ++ ns })
closeBlock
fc <- getFC
return [PParams fc ns (concat ds)]
<?> "parameters declaration"
{- | Parses a mutual declaration (for mutually recursive functions)
Mutual ::=
'mutual' OpenBlock Decl* CloseBlock
;
-}
mutual :: SyntaxInfo -> IdrisParser [PDecl]
mutual syn =
do reserved "mutual"
openBlock
let pvars = syn_params syn
ds <- many (decl syn)
closeBlock
fc <- getFC
return [PMutual fc (concat ds)]
<?> "mutual block"
{- | Parses a namespace declaration
Namespace ::=
'namespace' identifier OpenBlock Decl+ CloseBlock
;
-}
namespace :: SyntaxInfo -> IdrisParser [PDecl]
namespace syn =
do reserved "namespace"; n <- identifier;
openBlock
ds <- some (decl syn { syn_namespace = n : syn_namespace syn })
closeBlock
return [PNamespace n (concat ds)]
<?> "namespace declaration"
{- | Parses a fixity declaration
Fixity ::=
FixityType Natural_t OperatorList Terminator
;
-}
fixity :: IdrisParser PDecl
fixity = do pushIndent
f <- fixityType; i <- natural; ops <- sepBy1 operator (lchar ',')
terminator
let prec = fromInteger i
istate <- get
let infixes = idris_infixes istate
let fs = map (Fix (f prec)) ops
let redecls = map (alreadyDeclared infixes) fs
let ill = filter (not . checkValidity) redecls
if null ill
then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)
, ibc_write = map IBCFix fs ++ ibc_write istate
})
fc <- getFC
return (PFix fc (f prec) ops)
else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""
++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill
<?> "fixity declaration"
where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])
alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)
checkValidity :: (FixDecl, [FixDecl]) -> Bool
checkValidity (f, fs) = all (== f) fs
extractName :: FixDecl -> String
extractName (Fix _ n) = n
{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)
FixityType ::=
'infixl'
| 'infixr'
| 'infix'
| 'prefix'
;
-}
fixityType :: IdrisParser (Int -> Fixity)
fixityType = try (do reserved "infixl"; return Infixl)
<|> try (do reserved "infixr"; return Infixr)
<|> try (do reserved "infix"; return InfixN)
<|> try (do reserved "prefix"; return PrefixN)
<?> "fixity type"
{- |Parses a methods block (for type classes and instances)
MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock
-}
methodsBlock :: SyntaxInfo -> IdrisParser [PDecl]
methodsBlock syn = do reserved "where"
openBlock
ds <- many (fnDecl syn)
closeBlock
return (concat ds)
<?> "methods block"
{- |Parses a type class declaration
ClassArgument ::=
Name
| '(' Name ':' Expr ')'
;
Class ::=
DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* MethodsBlock?
;
-}
class_ :: SyntaxInfo -> IdrisParser [PDecl]
class_ syn = do doc <- option "" (docComment '|')
acc <- optional accessibility
reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name
let n = expandNS syn n_in
cs <- many carg
ds <- option [] (methodsBlock syn)
accData acc n (concatMap declared ds)
return [PClass doc syn fc cons n cs ds]
<?> "type-class declaration"
where
carg :: IdrisParser (Name, PTerm)
carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'
return (i, ty)
<|> do i <- name;
return (i, PType)
{- |Parses a type class instance declaration
Instance ::=
'instance' InstanceName? ConstraintList? Name SimpleExpr* MethodsBlock?
;
InstanceName ::= '[' Name ']';
-}
instance_ :: SyntaxInfo -> IdrisParser [PDecl]
instance_ syn = do reserved "instance"; fc <- getFC
en <- optional instanceName
cs <- constraintList syn
cn <- name
args <- many (simpleExpr syn)
let sc = PApp fc (PRef fc cn) (map pexp args)
let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
ds <- option [] (methodsBlock syn)
return [PInstance syn fc cs cn args t en ds]
<?> "instance declaratioN"
where instanceName :: IdrisParser Name
instanceName = do lchar '['; n_in <- fnName; lchar ']'
let n = expandNS syn n_in
return n
<?> "instance name"
{- | Parses an expression as a whole
FullExpr ::= Expr EOF_t;
-}
fullExpr :: SyntaxInfo -> IdrisParser PTerm
fullExpr syn = do x <- expr syn
eof
i <- get
return $ desugar syn i x
{- |Parses an expression
Expr ::= Expr';
-}
expr :: SyntaxInfo -> IdrisParser PTerm
expr syn = do i <- get
buildExpressionParser (table (idris_infixes i)) (expr' syn)
{- | Parses either an internally defined expression or
a user-defined one
Expr' ::= "External (User-defined) Syntax"
| InternalExpr;
-}
expr' :: SyntaxInfo -> IdrisParser PTerm
expr' syn = try (externalExpr syn)
<|> internalExpr syn
<?> "expression"
{- | Parses a user-defined expression -}
externalExpr :: SyntaxInfo -> IdrisParser PTerm
externalExpr syn = do i <- get
extensions syn (syntax_rules i)
<?> "user-defined expression"
{- | Parses a simple user-defined expression -}
simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
simpleExternalExpr syn = do i <- get
extensions syn (filter isSimple (syntax_rules i))
where
isSimple (Rule (Expr x:xs) _ _) = False
isSimple (Rule (SimpleExpr x:xs) _ _) = False
isSimple (Rule [Keyword _] _ _) = True
isSimple (Rule [Symbol _] _ _) = True
isSimple (Rule (_:xs) _ _) = case last xs of
Keyword _ -> True
Symbol _ -> True
_ -> False
isSimple _ = False
{- | Tries to parse a user-defined expression given a list of syntactic extensions -}
extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
extensions syn rules = choice (map (try . extension syn) (filter isValid rules))
<?> "user-defined expression"
where
isValid :: Syntax -> Bool
isValid (Rule _ _ AnySyntax) = True
isValid (Rule _ _ PatternSyntax) = inPattern syn
isValid (Rule _ _ TermSyntax) = not (inPattern syn)
data SynMatch = SynTm PTerm | SynBind Name
{- | Tries to parse an expression given a user-defined rule -}
extension :: SyntaxInfo -> Syntax -> IdrisParser PTerm
extension syn (Rule ssym ptm _)
= do smap <- mapM extensionSymbol ssym
let ns = mapMaybe id smap
return (update ns ptm) -- updated with smap
where
extensionSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))
extensionSymbol (Keyword n) = do reserved (show n); return Nothing
extensionSymbol (Expr n) = do tm <- expr syn
return $ Just (n, SynTm tm)
extensionSymbol (SimpleExpr n) = do tm <- simpleExpr syn
return $ Just (n, SynTm tm)
extensionSymbol (Binding n) = do b <- name
return $ Just (n, SynBind b)
extensionSymbol (Symbol s) = do symbol s
return Nothing
dropn :: Name -> [(Name, a)] -> [(Name, a)]
dropn n [] = []
dropn n ((x,t) : xs) | n == x = xs
| otherwise = (x,t):dropn n xs
updateB :: [(Name, SynMatch)] -> Name -> Name
updateB ns n = case lookup n ns of
Just (SynBind t) -> t
_ -> n
update :: [(Name, SynMatch)] -> PTerm -> PTerm
update ns (PRef fc n) = case lookup n ns of
Just (SynTm t) -> t
_ -> PRef fc n
update ns (PLam n ty sc) = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)
update ns (PPi p n ty sc) = PPi p (updateB ns n) (update ns ty) (update (dropn n ns) sc)
update ns (PLet n ty val sc) = PLet (updateB ns n) (update ns ty) (update ns val)
(update (dropn n ns) sc)
update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)
update ns (PCase fc c opts) = PCase fc (update ns c) (map (pmap (update ns)) opts)
update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)
update ns (PDPair fc l t r) = PDPair fc (update ns l) (update ns t) (update ns r)
update ns (PAlternative a as) = PAlternative a (map (update ns) as)
update ns (PHidden t) = PHidden (update ns t)
update ns (PDoBlock ds) = PDoBlock $ upd ns ds
where upd :: [(Name, SynMatch)] -> [PDo] -> [PDo]
upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds
upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds
upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)
: upd (dropn n ns) ds
upd ns (DoBindP fc i t : ds) = DoBindP fc (update ns i) (update ns t)
: upd ns ds
upd ns (DoLetP fc i t : ds) = DoLetP fc (update ns i) (update ns t)
: upd ns ds
update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
update ns t = t
{- |Parses a (normal) built-in expression
InternalExpr ::=
App
| MatchApp
| UnifyLog
| RecordType
| SimpleExpr
| Lambda
| QuoteGoal
| Let
| RewriteTerm
| Pi
| DoBlock
;
-}
internalExpr :: SyntaxInfo -> IdrisParser PTerm
internalExpr syn =
try (app syn)
<|> try (matchApp syn)
<|> try (unifyLog syn)
<|> recordType syn
<|> try (simpleExpr syn)
<|> lambda syn
<|> quoteGoal syn
<|> let_ syn
<|> rewriteTerm syn
<|> pi syn
<|> doBlock syn
<?> "expression"
{- | Parses a case expression
CaseExpr ::=
'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;
-}
caseExpr :: SyntaxInfo -> IdrisParser PTerm
caseExpr syn = do reserved "case"; fc <- getFC
scr <- expr syn; reserved "of";
opts <- indentedBlock1 (caseOption syn)
return (PCase fc scr opts)
<?> "case expression"
{- | Parses a case in a case expression
CaseOption ::=
Expr '=>' Expr Terminator
;
-}
caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
caseOption syn = do lhs <- expr (syn { inPattern = True })
symbol "=>"; r <- expr syn
return (lhs, r)
<?> "case option"
{- | Parses a proof block
ProofExpr ::=
'proof' OpenBlock Tactic'* CloseBlock
;
-}
proofExpr :: SyntaxInfo -> IdrisParser PTerm
proofExpr syn = do reserved "proof"
ts <- indentedBlock (tactic syn)
return $ PProof ts
<?> "proof block"
{- | Parses a tactics block
TacticsExpr :=
'tactics' OpenBlock Tactic'* CloseBlock
;
-}
tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
tacticsExpr syn = do reserved "tactics"
ts <- indentedBlock (tactic syn)
return $ PTactics ts
<?> "tactics block"
{- | Parses a simple expresion
SimpleExpr ::=
'![' Term ']'
| '?' Name
| % 'instance'
| 'refl' ('{' Expr '}')?
| ProofExpr
| TacticsExpr
| CaseExpr
| FnName
| List
| Comprehension
| Alt
| Idiom
| '(' Bracketed
| Constant
| Type
| '()'
| '_|_'
| '_'
| {- External (User-defined) Simple Expression -}
;
-}
simpleExpr :: SyntaxInfo -> IdrisParser PTerm
simpleExpr syn =
{-try (do symbol "!["; t <- term; lchar ']'; return $ PQuote t)
<|>-} do lchar '?'; x <- name; return (PMetavar x)
<|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)
<|> do reserved "refl"; fc <- getFC;
tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';
return t)
return (PRefl fc tm)
<|> proofExpr syn
<|> tacticsExpr syn
<|> caseExpr syn
<|> try (do fc <- getFC
x <- fnName
return (PRef fc x))
<|> try (listExpr syn)
<|> try (comprehension syn)
<|> try (alt syn)
<|> try (idiom syn)
<|> try (do lchar '('
bracketed (disallowImp syn))
<|> try (do c <- constant
fc <- getFC
return (modifyConst syn fc (PConstant c)))
<|> do reserved "Type"; return PType
<|> try (do symbol "()"
fc <- getFC
return (PTrue fc))
<|> try (do symbol "_|_"
fc <- getFC
return (PFalse fc))
<|> do lchar '_'; return Placeholder
<|> simpleExternalExpr syn
<?> "expression"
{- |Parses the rest of an expression in braces
Bracketed ::=
| Pair
| Expr ')'
| Operator Expr ')'
| Expr Operator ')'
;
-}
bracketed :: SyntaxInfo -> IdrisParser PTerm
bracketed syn =
try (pair syn)
<|> try (do e <- expr syn; lchar ')'; return e)
<|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'
return $ PLam (MN 1000 "ARG") Placeholder
(PApp fc (PRef fc (UN o)) [pexp (PRef fc (MN 1000 "ARG")),
pexp e]))
<|> try (do fc <- getFC; e <- simpleExpr syn; o <- operator; lchar ')'
return $ PLam (MN 1000 "ARG") Placeholder
(PApp fc (PRef fc (UN o)) [pexp e,
pexp (PRef fc (MN 1000 "ARG"))]))
<?> "end of expression in braces"
-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a
-- big integer, otherwise try fromInteger and the constants as alternatives.
-- a better solution would be to fix fromInteger to work with Integer, as the
-- name suggests, rather than Int
{-| Finds optimal type for integer constant -}
modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
modifyConst syn fc (PConstant (BI x))
| not (inPattern syn)
= PAlternative False
(PApp fc (PRef fc (UN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]
: consts)
| otherwise = PAlternative False consts
where
consts = [ PConstant (BI x)
, PConstant (I (fromInteger x))
, PConstant (B8 (fromInteger x))
, PConstant (B16 (fromInteger x))
, PConstant (B32 (fromInteger x))
, PConstant (B64 (fromInteger x))
]
modifyConst syn fc x = x
{- | Parses a list literal expression e.g. [1,2,3]
ListExpr ::=
'[' ExprList? ']'
;
ExprList ::=
Expr
| Expr ',' ExprList
;
-}
listExpr :: SyntaxInfo -> IdrisParser PTerm
listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'
return (mkList fc xs)
<?> "list expression"
where
mkList :: FC -> [PTerm] -> PTerm
mkList fc [] = PRef fc (UN "Nil")
mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)]
{- | Parses rest of pair expression
Pair ::=
Expr RestTuple? ')'
| NTuple ')'
| Name ':' Expr '**' 'Expr' ')'
;
RestTuple ::=
',' Expr
| '**' Expr
;
NTuple ::=
Expr ',' Expr
| Expr ',' NTuple
;
-}
pair :: SyntaxInfo -> IdrisParser PTerm
pair syn = try (do l <- expr syn
fc <- getFC
rest <- restTuple
case rest of
[] -> return l
[Left r] -> return (PPair fc l r)
[Right r] -> return (PDPair fc l Placeholder r))
<|> try (do x <- ntuple
lchar ')'
return x)
<|> do ln <- name; lchar ':'
lty <- expr syn
reservedOp "**"
fc <- getFC
r <- expr syn
lchar ')'
return (PDPair fc (PRef fc ln) lty r)
<?> "pair expression"
where
restTuple :: IdrisParser [Either PTerm PTerm]
restTuple = do lchar ')'; return []
<|> do lchar ','
r <- expr syn
lchar ')'
return [Left r]
<|> do reservedOp "**"
r <- expr syn
lchar ')'
return [Right r]
<?> "end of pair expression"
ntuple :: IdrisParser PTerm
ntuple = try (do l <- expr syn; fc <- getFC; lchar ','
rest <- ntuple
return (PPair fc l rest))
<|> (do l <- expr syn; fc <- getFC; lchar ','
r <- expr syn
return (PPair fc l r))
<?> "tuple expression"
{- | Parses an alternative expression
Alt ::= '(|' Expr_List '|)';
Expr_List ::=
Expr'
| Expr' ',' Expr_List
;
-}
alt :: SyntaxInfo -> IdrisParser PTerm
alt syn = do symbol "(|"; alts <- sepBy1 (expr' syn) (lchar ','); symbol "|)"
return (PAlternative False alts)
{- | Parses a possibly hidden simple expression
HSimpleExpr ::=
'.' SimpleExpr
| SimpleExpr
;
-}
hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
hsimpleExpr syn =
do lchar '.'
e <- simpleExpr syn
return $ PHidden e
<|> simpleExpr syn
<?> "expression"
{- | Parses a matching application expression
MatchApp ::=
SimpleExpr '<==' FnName
;
-}
matchApp :: SyntaxInfo -> IdrisParser PTerm
matchApp syn = do ty <- simpleExpr syn
symbol "<=="
fc <- getFC
f <- fnName
return (PLet (MN 0 "match")
ty
(PMatchApp fc f)
(PRef fc (MN 0 "match")))
<?> "matching application expression"
{- | Parses a unification log expression
UnifyLog ::=
'%' 'unifyLog' SimpleExpr
;
-}
unifyLog :: SyntaxInfo -> IdrisParser PTerm
unifyLog syn = do lchar '%'; reserved "unifyLog";
tm <- simpleExpr syn
return (PUnifyLog tm)
<?> "unification log expression"
{- | Parses a function application expression
App ::=
'mkForeign' Arg Arg*
| SimpleExpr Arg+
;
-}
app :: SyntaxInfo -> IdrisParser PTerm
app syn = do f <- reserved "mkForeign"
fc <- getFC
fn <- arg syn
args <- many (do notEndApp; arg syn)
i <- get
-- mkForeign f args ==>
-- liftPrimIO (\w => mkForeignPrim f args w)
let ap = PApp fc (PRef fc (UN "liftPrimIO"))
[pexp (PLam (MN 0 "w")
Placeholder
(PApp fc (PRef fc (UN "mkForeignPrim"))
(fn : args ++
[pexp (PRef fc (MN 0 "w"))])))]
return (dslify i ap)
<|> do f <- simpleExpr syn
fc <- getFC
args <- some (do notEndApp; arg syn)
i <- get
return (dslify i $ PApp fc f args)
<?> "function application"
where
dslify :: IState -> PTerm -> PTerm
dslify i (PApp fc (PRef _ f) [a])
| [d] <- lookupCtxt f (idris_dsls i)
= desugar (syn { dsl_info = d }) i (getTm a)
dslify i t = t
{- |Parses a function argument
Arg ::=
ImplicitArg
| ConstraintArg
| SimpleExpr
;
-}
arg :: SyntaxInfo -> IdrisParser PArg
arg syn = try (implicitArg syn)
<|> try (constraintArg syn)
<|> do e <- simpleExpr syn
return (pexp e)
<?> "function argument"
{- |Parses an implicit function argument
ImplicitArg ::=
'{' Name ('=' Expr)? '}'
;
-}
implicitArg :: SyntaxInfo -> IdrisParser PArg
implicitArg syn = do lchar '{'
n <- name
fc <- getFC
v <- option (PRef fc n) (do lchar '='
expr syn)
lchar '}'
return (pimp n v)
<?> "implicit function argument"
{- |Parses a constraint argument (for selecting a named type class instance)
ConstraintArg ::=
'@{' Expr '}'
;
-}
constraintArg :: SyntaxInfo -> IdrisParser PArg
constraintArg syn = do symbol "@{"
e <- expr syn
symbol "}"
return (pconst e)
<?> "constraint argument"
{- |Parses a record field setter expression
RecordType ::=
'record' '{' FieldTypeList '}';
FieldTypeList ::=
FieldType
| FieldType ',' FieldTypeList
;
FieldType ::=
FnName '=' Expr
;
-}
recordType :: SyntaxInfo -> IdrisParser PTerm
recordType syn
= do reserved "record"
lchar '{'
fields <- sepBy1 fieldType (lchar ',')
lchar '}'
fc <- getFC
rec <- optional (simpleExpr syn)
case rec of
Nothing ->
return (PLam (MN 0 "fldx") Placeholder
(applyAll fc fields (PRef fc (MN 0 "fldx"))))
Just v -> return (applyAll fc fields v)
<?> "record setting expression"
where fieldType :: IdrisParser (Name, PTerm)
fieldType = do n <- fnName
lchar '='
e <- expr syn
return (n, e)
<?> "field setter"
applyAll :: FC -> [(Name, PTerm)] -> PTerm -> PTerm
applyAll fc [] x = x
applyAll fc ((n, e) : es) x
= applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
{- |Creates setters for record types on necessary functions -}
mkType :: Name -> Name
mkType (UN n) = UN ("set_" ++ n)
mkType (MN 0 n) = MN 0 ("set_" ++ n)
mkType (NS n s) = NS (mkType n) s
{- |Parses a type for an expression
TypeSig ::=
':' Expr
;
-}
typeSig :: SyntaxInfo -> IdrisParser PTerm
typeSig syn = lchar ':' *> typeExpr syn <?> "type"
{- |Parses a type signature
TypeExpr ::= ConstraintList? Expr;
-}
typeExpr :: SyntaxInfo -> IdrisParser PTerm
typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []
sc <- expr syn
return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)
<?> "type signature"
{- |Parses a lambda expression
Lambda ::=
'\\' TypeOptDeclList '=>' Expr
| '\\' SimpleExprList '=>' Expr
;
SimpleExprList ::=
SimpleExpr
| SimpleExpr ',' SimpleExprList
;
-}
lambda :: SyntaxInfo -> IdrisParser PTerm
lambda syn = do lchar '\\'
try (do xt <- tyOptDeclList syn
symbol "=>"
sc <- expr syn
return (bindList PLam xt sc)
<|> (do ps <- sepBy (do fc <- getFC
e <- simpleExpr syn
return (fc, e)) (lchar ',')
symbol "=>"
sc <- expr syn
return (pmList (zip [0..] ps) sc)))
<?> "lambda expression"
where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
pmList [] sc = sc
pmList ((i, (fc, x)) : xs) sc
= PLam (MN i "lamp") Placeholder
(PCase fc (PRef fc (MN i "lamp"))
[(x, pmList xs sc)])
{- |Parses a term rewrite expression
RewriteTerm ::=
'rewrite' Expr ('==>' Expr)? 'in' Expr
;
-}
rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
rewriteTerm syn = do reserved "rewrite"
fc <- getFC
prf <- expr syn
giving <- optional (do symbol "==>"; expr' syn)
reserved "in"; sc <- expr syn
return (PRewrite fc
(PApp fc (PRef fc (UN "sym")) [pexp prf]) sc
giving)
<?> "term rewrite expression"
{- |Parses a let binding
Let ::=
'let' Name TypeSig'? '=' Expr 'in' Expr
| 'let' Expr' '=' Expr' 'in' Expr
TypeSig' ::=
':' Expr'
;
-}
let_ :: SyntaxInfo -> IdrisParser PTerm
let_ syn = try (do reserved "let"; n <- name;
ty <- option Placeholder (do lchar ':'; expr' syn)
lchar '='
v <- expr syn
reserved "in"; sc <- expr syn
return (PLet n ty v sc))
<|> (do reserved "let"; fc <- getFC; pat <- expr' (syn { inPattern = True } )
symbol "="; v <- expr syn
reserved "in"; sc <- expr syn
return (PCase fc v [(pat, sc)]))
<?> "let binding"
{- |Parses a quote goal
QuoteGoal ::=
'quoteGoal' Name 'by' Expr 'in' Expr
;
-}
quoteGoal :: SyntaxInfo -> IdrisParser PTerm
quoteGoal syn = do reserved "quoteGoal"; n <- name;
reserved "by"
r <- expr syn
reserved "in"
fc <- getFC
sc <- expr syn
return (PGoal fc r n sc)
<?> "quote goal expression"
{- |Parses a dependent type signature
Pi ::=
'|'? Static? '(' TypeDeclList ')' DocComment '->' Expr
| '|'? Static? '{' TypeDeclList '}' '->' Expr
| '{' 'auto' TypeDeclList '}' '->' Expr
| '{' 'default' TypeDeclList '}' '->' Expr
| '{' 'static' '}' Expr' '->' Expr
;
-}
pi syn =
try (do lazy <- if implicitAllowed syn -- laziness is top level only
then option False (do lchar '|'; return True)
else return False
st <- static
lchar '('; xt <- typeDeclList syn; lchar ')'
doc <- option "" (docComment '^')
symbol "->"
sc <- expr syn
return (bindList (PPi (Exp lazy st doc)) xt sc))
<|> try (if implicitAllowed syn
then do lazy <- option False (do lchar '|'
return True)
st <- static
lchar '{'
xt <- typeDeclList syn
lchar '}'
symbol "->"
sc <- expr syn
return (bindList (PPi (Imp lazy st "")) xt sc)
else fail "no implicit arguments allowed here")
<|> try (do lchar '{'
reserved "auto"
xt <- typeDeclList syn
lchar '}'
symbol "->"
sc <- expr syn
return (bindList (PPi
(TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))
<|> try (do lchar '{'
reserved "default"
script <- simpleExpr syn
xt <- typeDeclList syn
lchar '}'
symbol "->"
sc <- expr syn
return (bindList (PPi (TacImp False Dynamic script "")) xt sc))
<|> do lchar '{'
reserved "static"
lchar '}'
t <- expr' syn
symbol "->"
sc <- expr syn
return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)
<?> "dependent type signature"
{- | Parses a type constraint list
ConstraintList ::=
'(' Expr_List ')' '=>'
| Expr '=>'
;
-}
constraintList :: SyntaxInfo -> IdrisParser [PTerm]
constraintList syn = try (do lchar '('
tys <- sepBy1 (expr' (disallowImp syn)) (lchar ',')
lchar ')'
reservedOp "=>"
return tys)
<|> try (do t <- expr (disallowImp syn)
reservedOp "=>"
return [t])
<|> return []
<?> "type constraint list"
{- | Parses a using declaration list
UsingDeclList ::=
UsingDeclList'
| NameList TypeSig
;
UsingDeclList' ::=
UsingDecl
| UsingDecl ',' UsingDeclList'
;
NameList ::=
Name
| Name ',' NameList
;
-}
usingDeclList :: SyntaxInfo -> IdrisParser [Using]
usingDeclList syn
= try (sepBy1 (usingDecl syn) (lchar ','))
<|> do ns <- sepBy1 name (lchar ',')
t <- typeSig (disallowImp syn)
return (map (\x -> UImplicit x t) ns)
<?> "using declaration list"
{- |Parses a using declaration
UsingDecl ::=
FnName TypeSig
| FnName FnName+
;
-}
usingDecl :: SyntaxInfo -> IdrisParser Using
usingDecl syn = try (do x <- fnName
t <- typeSig (disallowImp syn)
return (UImplicit x t))
<|> do c <- fnName
xs <- some fnName
return (UConstraint c xs)
<?> "using declaration"
{- |Parses a type declaration list
TypeDeclList ::=
FunctionSignatureList
| NameList TypeSig
;
FunctionSignatureList ::=
Name TypeSig
| Name TypeSig ',' FunctionSignatureList
;
-}
typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
typeDeclList syn = try (sepBy1 (do x <- fnName
t <- typeSig (disallowImp syn)
return (x,t))
(lchar ','))
<|> do ns <- sepBy1 name (lchar ',')
t <- typeSig (disallowImp syn)
return (map (\x -> (x, t)) ns)
<?> "type declaration list"
{- |Parses a type declaration list with optional parameters
TypeOptDeclList ::=
NameOrPlaceholder TypeSig?
| NameOrPlaceholder TypeSig? ',' TypeOptDeclList
;
NameOrPlaceHolder ::= Name | '_';
-}
tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder
t <- option Placeholder (do lchar ':'
expr syn)
return (x,t))
(lchar ',')
<?> "type declaration list"
where nameOrPlaceholder :: IdrisParser Name
nameOrPlaceholder = fnName
<|> do symbol "_"
return (MN 0 "underscore")
<?> "name or placeholder"
{- |Parses a list comprehension
Comprehension ::= '[' Expr '|' DoList ']';
DoList ::=
Do
| Do ',' DoList
;
-}
comprehension :: SyntaxInfo -> IdrisParser PTerm
comprehension syn
= do lchar '['
fc <- getFC
pat <- expr syn
lchar '|'
qs <- sepBy1 (do_ syn) (lchar ',')
lchar ']'
return (PDoBlock (map addGuard qs ++
[DoExp fc (PApp fc (PRef fc (UN "return"))
[pexp pat])]))
<?> "list comprehension"
where addGuard :: PDo -> PDo
addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))
[pexp e])
addGuard x = x
{- |Parses a do-block
Do' ::= Do KeepTerminator;
DoBlock ::=
'do' OpenBlock Do'+ CloseBlock
;
-}
doBlock :: SyntaxInfo -> IdrisParser PTerm
doBlock syn
= do reserved "do"
ds <- indentedBlock (do_ syn)
return (PDoBlock ds)
<?> "do block"
{- |Parses an expression inside a do block
Do ::=
'let' Name TypeSig'? '=' Expr
| 'let' Expr' '=' Expr
| Name '<-' Expr
| Expr' '<-' Expr
| Expr
;
-}
do_ :: SyntaxInfo -> IdrisParser PDo
do_ syn
= try (do reserved "let"
i <- name
ty <- option Placeholder (do lchar ':'
expr' syn)
reservedOp "="
fc <- getFC
e <- expr syn
return (DoLet fc i ty e))
<|> try (do reserved "let"
i <- expr' syn
reservedOp "="
fc <- getFC
sc <- expr syn
return (DoLetP fc i sc))
<|> try (do i <- name
symbol "<-"
fc <- getFC
e <- expr syn;
return (DoBind fc i e))
<|> try (do i <- expr' syn
symbol "<-"
fc <- getFC
e <- expr syn;
return (DoBindP fc i e))
<|> try (do e <- expr syn
fc <- getFC
return (DoExp fc e))
<?> "do block expression"
{- |Parses an expression in idiom brackets
Idiom ::= '[|' Expr '|]';
-}
idiom :: SyntaxInfo -> IdrisParser PTerm
idiom syn
= do symbol "[|"
fc <- getFC
e <- expr syn
symbol "|]"
return (PIdiom fc e)
<?> "expression in idiom brackets"
{- |Parses a constant or literal expression
Constant ::=
'Integer'
| 'Int'
| 'Char'
| 'Float'
| 'String'
| 'Ptr'
| 'Bits8'
| 'Bits16'
| 'Bits32'
| 'Bits64'
| 'Bits8x16'
| 'Bits16x8'
| 'Bits32x4'
| 'Bits64x2'
| Float_t
| Natural_t
| String_t
| Char_t
;
-}
constant :: IdrisParser Core.TT.Const
constant = do reserved "Integer";return (AType (ATInt ITBig))
<|> do reserved "Int"; return (AType (ATInt ITNative))
<|> do reserved "Char"; return (AType (ATInt ITChar))
<|> do reserved "Float"; return (AType ATFloat)
<|> do reserved "String"; return StrType
<|> do reserved "Ptr"; return PtrType
<|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))
<|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))
<|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32)))
<|> do reserved "Bits64"; return (AType (ATInt (ITFixed IT64)))
<|> do reserved "Bits8x16"; return (AType (ATInt (ITVec IT8 16)))
<|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))
<|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))
<|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))
<|> try (do f <- float; return $ Fl f)
<|> try (do i <- natural; return $ BI i)
<|> try (do s <- stringLiteral; return $ Str s)
<|> try (do c <- charLiteral; return $ Ch c)
<?> "constant or literal"
{- |Parses a static modifier
Static ::=
'[' static ']'
;
-}
static :: IdrisParser Static
static = do lchar '['; reserved "static"; lchar ']'; return Static
<|> return Dynamic
<?> "static modifier"
{- |Parses a record type declaration
Record ::=
DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
-}
record :: SyntaxInfo -> IdrisParser PDecl
record syn = do doc <- option "" (docComment '|')
acc <- optional accessibility
reserved "record"
fc <- getFC
tyn_in <- fnName
ty <- typeSig (allowImp syn)
let tyn = expandNS syn tyn_in
reserved "where"
(cdoc, cn, cty, _) <- indentedBlockS (constructor syn)
accData acc tyn [cn]
let rsyn = syn { syn_namespace = show (nsroot tyn) :
syn_namespace syn }
let fns = getRecNames rsyn cty
mapM_ (\n -> addAcc n acc) fns
return $ PRecord doc rsyn fc tyn ty cdoc cn cty
<?> "record type declaration"
where
getRecNames :: SyntaxInfo -> PTerm -> [Name]
getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
++ getRecNames syn sc
getRecNames _ _ = []
toFreeze :: Maybe Accessibility -> Maybe Accessibility
toFreeze (Just Frozen) = Just Hidden
toFreeze x = x
{- | Parses data declaration type (normal or codata)
DataI ::= 'data' | 'codata';
-}
dataI :: IdrisParser Bool
dataI = do reserved "data"; return False
<|> do reserved "codata"; return True
{- | Parses a data type declaration
Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?
| DocComment? Accessibility? DataI FnName Name* DataRest?
;
Constructor' ::= Constructor KeepTerminator;
ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;
DataRest ::= '=' SimpleConstructorList Terminator
| 'where'!
;
SimpleConstructorList ::=
SimpleConstructor
| SimpleConstructor '|' SimpleConstructorList
;
-}
data_ :: SyntaxInfo -> IdrisParser PDecl
data_ syn = try (do doc <- option "" (docComment '|')
acc <- optional accessibility
co <- dataI
fc <- getFC
tyn_in <- fnName
ty <- typeSig (allowImp syn)
let tyn = expandNS syn tyn_in
option (PData doc syn fc co (PLaterdecl tyn ty)) (do
reserved "where"
cons <- indentedBlock (constructor syn)
accData acc tyn (map (\ (_, n, _, _) -> n) cons)
return $ PData doc syn fc co (PDatadecl tyn ty cons)))
<|> try (do doc <- option "" (docComment '|')
pushIndent
acc <- optional accessibility
co <- dataI
fc <- getFC
tyn_in <- fnName
args <- many name
let ty = bindArgs (map (const PType) args) PType
let tyn = expandNS syn tyn_in
option (PData doc syn fc co (PLaterdecl tyn ty)) (do
try (lchar '=') <|> do reserved "where"
let kw = (if co then "co" else "") ++ "data "
let n = show tyn_in ++ " "
let s = kw ++ n
let as = concat (intersperse " " $ map show args) ++ " "
let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)
let ss = concat (intersperse " -> " $ map (const "Type") args)
let fix1 = s ++ as ++ " = ..."
let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."
let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."
fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]
cons <- sepBy1 (simpleConstructor syn) (lchar '|')
terminator
let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)
cons' <- mapM (\ (doc, x, cargs, cfc) ->
do let cty = bindArgs cargs conty
return (doc, x, cty, cfc)) cons
accData acc tyn (map (\ (_, n, _, _) -> n) cons')
return $ PData doc syn fc co (PDatadecl tyn ty cons')))
<?> "data type declaration"
where
mkPApp :: FC -> PTerm -> [PTerm] -> PTerm
mkPApp fc t [] = t
mkPApp fc t xs = PApp fc t (map pexp xs)
bindArgs :: [PTerm] -> PTerm -> PTerm
bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs
{- | Parses a type constructor declaration
Constructor ::= DocComment? FnName TypeSig;
-}
constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC)
constructor syn
= do doc <- option "" (docComment '|')
cn_in <- fnName; fc <- getFC
let cn = expandNS syn cn_in
ty <- typeSig (allowImp syn)
return (doc, cn, ty, fc)
<?> "constructor"
{- | Parses a constructor for simple discriminative union data types
SimpleConstructor ::= FnName SimpleExpr* DocComment?
-}
simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC)
simpleConstructor syn
= do cn_in <- fnName
let cn = expandNS syn cn_in
fc <- getFC
args <- many (do notEndApp
simpleExpr syn)
doc <- option "" (docComment '^')
return (doc, cn, args, fc)
<?> "constructor"
{- | Parses a dsl block declaration
DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;
-}
dsl :: SyntaxInfo -> IdrisParser PDecl
dsl syn = do reserved "dsl"
n <- fnName
bs <- indentedBlock (overload syn)
let dsl = mkDSL bs (dsl_info syn)
checkDSL dsl
i <- get
put (i { idris_dsls = addDef n dsl (idris_dsls i) })
return (PDSL n dsl)
<?> "dsl block declaration"
where mkDSL :: [(String, PTerm)] -> DSL -> DSL
mkDSL bs dsl = let var = lookup "variable" bs
first = lookup "index_first" bs
next = lookup "index_next" bs
leto = lookup "let" bs
lambda = lookup "lambda" bs in
initDSL { dsl_var = var,
index_first = first,
index_next = next,
dsl_lambda = lambda,
dsl_let = leto }
{- | Checks DSL for errors -}
-- FIXME: currently does nothing, check if DSL is really sane
checkDSL :: DSL -> IdrisParser ()
checkDSL dsl = return ()
{- | Parses a DSL overload declaration
OverloadIdentifier ::= 'let' | Identifier;
Overload ::= OverloadIdentifier '=' Expr;
-}
overload :: SyntaxInfo -> IdrisParser (String, PTerm)
overload syn = do o <- identifier <|> do reserved "let"
return "let"
if o `notElem` overloadable
then fail $ show o ++ " is not an overloading"
else do
lchar '='
t <- expr syn
return (o, t)
<?> "dsl overload declaratioN"
where overloadable = ["let","lambda","index_first","index_next","variable"]
{- | Parse a clause with patterns
Pattern ::= Clause;
-}
pattern :: SyntaxInfo -> IdrisParser PDecl
pattern syn = do fc <- getFC
clause <- clause syn
return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later
<?> "pattern"
{- | Parse a constant applicative form declaration
CAF ::= 'let' FnName '=' Expr Terminator;
-}
caf :: SyntaxInfo -> IdrisParser PDecl
caf syn = do reserved "let"
n_in <- fnName; let n = expandNS syn n_in
lchar '='
t <- expr syn
terminator
fc <- getFC
return (PCAF fc n t)
<?> "constant applicative form declaration"
{- | Parse an argument expression
ArgExpr ::= HSimpleExpr | {- In Pattern External (User-defined) Expression -};
-}
argExpr :: SyntaxInfo -> IdrisParser PTerm
argExpr syn = let syn' = syn { inPattern = True } in
try (hsimpleExpr syn') <|> simpleExternalExpr syn'
<?> "argument expression"
{- | Parse a right hand side of a function
RHS ::= '=' Expr
| '?=' RHSName? Expr
| 'impossible'
;
RHSName ::= '{' FnName '}';
-}
rhs :: SyntaxInfo -> Name -> IdrisParser PTerm
rhs syn n = do lchar '='; expr syn
<|> do symbol "?=";
name <- option n' (do symbol "{"; n <- fnName; symbol "}";
return n)
r <- expr syn
return (addLet name r)
<|> do reserved "impossible"; return PImpossible
<?> "function right hand side"
where mkN :: Name -> Name
mkN (UN x) = UN (x++"_lemma_1")
mkN (NS x n) = NS (mkN x) n
n' :: Name
n' = mkN n
addLet :: Name -> PTerm -> PTerm
addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)
addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)
where addLetC (l, r) = (l, addLet nm r)
addLet nm r = (PLet (UN "value") Placeholder r (PMetavar nm))
{- |Parses a function clause
Clause ::= FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHS WhereOrTerminator
| SimpleExpr '<==' FnName RHS WhereOrTerminator
| WExpr+ RHS WhereOrTerminator
| FnName ConstraintArg* ImplicitOrArgExpr* WExpr* 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
| WExpr+ 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
| ArgExpr Operator ArgExpr WExpr* RHS WhereOrTerminator
| ArgExpr Operator ArgExpr WExpr* 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
;
ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
WhereOrTerminator ::= WhereBlock | Terminator;
-}
clause :: SyntaxInfo -> IdrisParser PClause
clause syn
= try (do pushIndent
n_in <- fnName; let n = expandNS syn n_in
cargs <- many (constraintArg syn)
fc <- getFC
args <- many (try (implicitArg (syn { inPattern = True } ))
<|> (fmap pexp (argExpr syn)))
wargs <- many (wExpr syn)
r <- rhs syn n
ist <- get
let ctxt = tt_ctxt ist
let wsyn = syn { syn_namespace = [] }
(wheres, nmap) <- choice [do x <- whereBlock n wsyn
popIndent
return x,
do terminator
return ([], [])]
let capp = PApp fc (PRef fc n)
(cargs ++ args)
ist <- get
put (ist { lastParse = Just n })
return $ PClause fc n capp wargs r wheres)
<|> try (do pushIndent
ty <- simpleExpr syn
symbol "<=="
fc <- getFC
n_in <- fnName; let n = expandNS syn n_in
r <- rhs syn n
ist <- get
let ctxt = tt_ctxt ist
let wsyn = syn { syn_namespace = [] }
(wheres, nmap) <- choice [do x <- whereBlock n wsyn
popIndent
return x,
do terminator
return ([], [])]
let capp = PLet (MN 0 "match")
ty
(PMatchApp fc n)
(PRef fc (MN 0 "match"))
ist <- get
put (ist { lastParse = Just n })
return $ PClause fc n capp [] r wheres)
<|> try (do pushIndent
wargs <- some (wExpr syn)
ist <- get
n <- case lastParse ist of
Just t -> return t
Nothing -> fail "Invalid clause"
fc <- getFC
r <- rhs syn n
let ctxt = tt_ctxt ist
let wsyn = syn { syn_namespace = [] }
(wheres, nmap) <- choice [do x <- whereBlock n wsyn
popIndent
return x,
do terminator
return ([], [])]
return $ PClauseR fc wargs r wheres)
<|> try (do pushIndent
n_in <- fnName; let n = expandNS syn n_in
cargs <- many (constraintArg syn)
fc <- getFC
args <- many (try (implicitArg (syn { inPattern = True } ))
<|> (fmap pexp (argExpr syn)))
wargs <- many (wExpr syn)
let capp = PApp fc (PRef fc n)
(cargs ++ args)
ist <- get
put (ist { lastParse = Just n })
reserved "with"
wval <- simpleExpr syn
openBlock
ds <- some $ fnDecl syn
let withs = map (fillLHSD n capp wargs) $ concat ds
closeBlock
popIndent
return $ PWith fc n capp wargs wval withs)
<|> try (do wargs <- some (wExpr syn)
fc <- getFC
reserved "with"
wval <- simpleExpr syn
openBlock
ds <- some $ fnDecl syn
let withs = concat ds
closeBlock
return $ PWithR fc wargs wval withs)
<|> try(do pushIndent
l <- argExpr syn
op <- operator
let n = expandNS syn (UN op)
r <- argExpr syn
fc <- getFC
wargs <- many (wExpr syn)
rs <- rhs syn n
let wsyn = syn { syn_namespace = [] }
(wheres, nmap) <- choice [do x <- whereBlock n wsyn
popIndent
return x,
do terminator
return ([], [])]
ist <- get
let capp = PApp fc (PRef fc n) [pexp l, pexp r]
put (ist { lastParse = Just n })
return $ PClause fc n capp wargs rs wheres)
<|> do l <- argExpr syn
op <- operator
let n = expandNS syn (UN op)
r <- argExpr syn
fc <- getFC
wargs <- many (wExpr syn)
reserved "with"
wval <- simpleExpr syn
openBlock
ds <- some $ fnDecl syn
closeBlock
ist <- get
let capp = PApp fc (PRef fc n) [pexp l, pexp r]
let withs = map (fillLHSD n capp wargs) $ concat ds
put (ist { lastParse = Just n })
return $ PWith fc n capp wargs wval withs
<?> "function clause"
where
fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
fillLHS n capp owargs (PClauseR fc wargs v ws)
= PClause fc n capp (owargs ++ wargs) v ws
fillLHS n capp owargs (PWithR fc wargs v ws)
= PWith fc n capp (owargs ++ wargs) v
(map (fillLHSD n capp (owargs ++ wargs)) ws)
fillLHS _ _ _ c = c
fillLHSD :: Name -> PTerm -> [PTerm] -> PDecl -> PDecl
fillLHSD n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)
fillLHSD n c a x = x
{- |Parses with pattern
WExpr ::= '|' Expr';
-}
wExpr :: SyntaxInfo -> IdrisParser PTerm
wExpr syn = do lchar '|'
expr' syn
<?> "with pattern"
{- |Parses a where block
WhereBlock ::= 'where' OpenBlock Decl+ CloseBlock;
-}
whereBlock :: Name -> SyntaxInfo -> IdrisParser ([PDecl], [(Name, Name)])
whereBlock n syn
= do reserved "where"
ds <- indentedBlock1 (decl syn)
let dns = concatMap (concatMap declared) ds
return (concat ds, map (\x -> (x, decoration syn x)) dns)
<?> "where block"
{- |Parses a code generation target language name
Codegen ::= 'C'
| 'Java'
| 'JavaScript'
| 'Node'
| 'LLVM'
| 'Bytecode'
;
-}
codegen_ :: IdrisParser Codegen
codegen_ = try (do reserved "C"; return ViaC)
<|> try (do reserved "Java"; return ViaJava)
<|> try (do reserved "JavaScript"; return ViaJavaScript)
<|> try (do reserved "Node"; return ViaNode)
<|> try (do reserved "LLVM"; return ViaLLVM)
<|> try (do reserved "Bytecode"; return Bytecode)
<?> "code generation language"
{- |Parses a compiler directive
StringList ::=
String
| String ',' StringList
;
Directive ::= '%' Directive';
Directive' ::= 'lib' CodeGen String_t
| 'link' CodeGen String_t
| 'flag' CodeGen String_t
| 'include' CodeGen String_t
| 'hide' Name
| 'freeze' Name
| 'access' Accessibility
| 'default' Totality
| 'logging' Natural
| 'dynamic' StringList
| 'language' 'TypeProviders'
;
-}
directive :: SyntaxInfo -> IdrisParser [PDecl]
directive syn = try (do lchar '%'; reserved "lib"; cgn <- codegen_; lib <- stringLiteral;
return [PDirective (do addLib cgn lib
addIBC (IBCLib cgn lib))])
<|> try (do lchar '%'; reserved "link"; cgn <- codegen_; obj <- stringLiteral;
return [PDirective (do dirs <- allImportDirs
o <- liftIO $ findInPath dirs obj
addIBC (IBCObj cgn obj) -- just name, search on loading ibc
addObjectFile cgn o)])
<|> try (do lchar '%'; reserved "flag"; cgn <- codegen_;
flag <- stringLiteral
return [PDirective (do addIBC (IBCCGFlag cgn flag)
addFlag cgn flag)])
<|> try (do lchar '%'; reserved "include"; cgn <- codegen_; hdr <- stringLiteral;
return [PDirective (do addHdr cgn hdr
addIBC (IBCHeader cgn hdr))])
<|> try (do lchar '%'; reserved "hide"; n <- iName []
return [PDirective (do setAccessibility n Hidden
addIBC (IBCAccess n Hidden))])
<|> try (do lchar '%'; reserved "freeze"; n <- iName []
return [PDirective (do setAccessibility n Frozen
addIBC (IBCAccess n Frozen))])
<|> try (do lchar '%'; reserved "access"; acc <- accessibility
return [PDirective (do i <- get
put(i { default_access = acc }))])
<|> try (do lchar '%'; reserved "default"; tot <- totality
i <- get
put (i { default_total = tot } )
return [PDirective (do i <- get
put(i { default_total = tot }))])
<|> try (do lchar '%'; reserved "logging"; i <- natural;
return [PDirective (setLogLevel (fromInteger i))])
<|> try (do lchar '%'; reserved "dynamic"; libs <- sepBy1 stringLiteral (lchar ',');
return [PDirective (do added <- addDyLib libs
case added of
Left lib -> addIBC (IBCDyLib (lib_name lib))
Right msg ->
fail $ msg)])
<|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";
return [PDirective (addLangExt TypeProviders)])
<?> "directive"
{- | Parses a totality
Totality ::= 'partial' | 'total'
-}
totality :: IdrisParser Bool
totality
= do reserved "total"; return True
<|> do reserved "partial"; return False
{- | Parses a type provider
Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
-}
provider :: SyntaxInfo -> IdrisParser [PDecl]
provider syn = do lchar '%'; reserved "provide";
lchar '('; n <- fnName; t <- typeSig syn; lchar ')'
fc <- getFC
reserved "with"
e <- expr syn
return [PProvider syn fc n t e]
<?> "type provider"
{- | Parses a transform
Transform ::= '%' 'transform' Expr '==>' Expr
-}
transform :: SyntaxInfo -> IdrisParser [PDecl]
transform syn = do lchar '%'; reserved "transform";
-- leave it unchecked, until we work out what this should
-- actually mean...
-- safety <- option True (do reserved "unsafe"
-- return False)
l <- expr syn
fc <- getFC
symbol "==>"
r <- expr syn
return [PTransform fc False l r]
<?> "transform"
{- | Parses a tactic script
Tactic ::= 'intro' NameList?
| 'intros'
| 'refine' Name Imp+
| 'mrefine' Name
| 'rewrite' Expr
| 'equiv' Expr
| 'let' Name ':' Expr' '=' Expr
| 'let' Name '=' Expr
| 'focus' Name
| 'exact' Expr
| 'applyTactic' Expr
| 'reflect' Expr
| 'fill' Expr
| 'try' Tactic '|' Tactic
| '{' TacticSeq '}'
| 'compute'
| 'trivial'
| 'solve'
| 'attack'
| 'state'
| 'term'
| 'undo'
| 'qed'
| 'abandon'
| ':' 'q'
;
Imp ::= '?' | '_';
TacticSeq ::=
Tactic ';' Tactic
| Tactic ';' TacticSeq
;
-}
tactic :: SyntaxInfo -> IdrisParser PTactic
tactic syn = do reserved "intro"; ns <- sepBy name (lchar ',')
return $ Intro ns
<|> do reserved "intros"; return Intros
<|> try (do reserved "refine"; n <- name
imps <- some imp
return $ Refine n imps)
<|> do reserved "refine"; n <- name
i <- get
return $ Refine n []
<|> do reserved "mrefine"; n <- name
i <- get
return $ MatchRefine n
<|> do reserved "rewrite"; t <- expr syn;
i <- get
return $ Rewrite (desugar syn i t)
<|> do reserved "equiv"; t <- expr syn;
i <- get
return $ Equiv (desugar syn i t)
<|> try (do reserved "let"; n <- name; lchar ':';
ty <- expr' syn; lchar '='; t <- expr syn;
i <- get
return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
<|> try (do reserved "let"; n <- name; lchar '=';
t <- expr syn;
i <- get
return $ LetTac n (desugar syn i t))
<|> do reserved "focus"; n <- name
return $ Focus n
<|> do reserved "exact"; t <- expr syn;
i <- get
return $ Exact (desugar syn i t)
<|> do reserved "applyTactic"; t <- expr syn;
i <- get
return $ ApplyTactic (desugar syn i t)
<|> do reserved "reflect"; t <- expr syn;
i <- get
return $ Reflect (desugar syn i t)
<|> do reserved "fill"; t <- expr syn;
i <- get
return $ Fill (desugar syn i t)
<|> do reserved "try"; t <- tactic syn;
lchar '|';
t1 <- tactic syn
return $ Try t t1
<|> do lchar '{'
t <- tactic syn;
lchar ';';
ts <- sepBy1 (tactic syn) (lchar ';')
lchar '}'
return $ TSeq t (mergeSeq ts)
<|> do reserved "compute"; return Compute
<|> do reserved "trivial"; return Trivial
<|> do reserved "solve"; return Solve
<|> do reserved "attack"; return Attack
<|> do reserved "state"; return ProofState
<|> do reserved "term"; return ProofTerm
<|> do reserved "undo"; return Undo
<|> do reserved "qed"; return Qed
<|> do reserved "abandon"; return Abandon
<|> do lchar ':'; reserved "q"; return Abandon
<?> "tactic"
where
imp :: IdrisParser Bool
imp = do lchar '?'; return False
<|> do lchar '_'; return True
mergeSeq :: [PTactic] -> PTactic
mergeSeq [t] = t
mergeSeq (t:ts) = TSeq t (mergeSeq ts)
{- | Parses a tactic as a whole -}
fullTactic :: SyntaxInfo -> IdrisParser PTactic
fullTactic syn = do t <- tactic syn
eof
return t
{- * Loading and parsing -}
{- | Parses an expression from input -}
parseExpr :: IState -> String -> Result PTerm
parseExpr st = parseString (evalStateT (fullExpr defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)
{- | Parses a tactic from input -}
parseTactic :: IState -> String -> Result PTactic
parseTactic st = parseString (evalStateT (fullTactic defaultSyntax) st) (Directed (UTF8.fromString "(input)") 0 0 0 0)
-- | Parse module header and imports
parseImports :: FilePath -> String -> Idris ([String], [String], Maybe Delta)
parseImports fname input
= do i <- getIState
case parseString (evalStateT imports i) (Directed (UTF8.fromString fname) 0 0 0 0) input of
Failure err -> fail (show err)
Success (x, i) -> do -- Discard state updates (there should be
-- none anyway)
return x
where imports :: IdrisParser (([String], [String], Maybe Delta), IState)
imports = do whiteSpace
mname <- moduleHeader
ps <- many import_
mrk <- mark
isEof <- lookAheadMatches eof
let mrk' = if isEof
then Nothing
else Just mrk
i <- get
return ((mname, ps, mrk'), i)
-- | A program is a list of declarations, possibly with associated
-- documentation strings.
parseProg :: SyntaxInfo -> FilePath -> String -> Maybe Delta ->
Idris [PDecl]
parseProg syn fname input mrk
= do i <- getIState
case parseString (evalStateT mainProg i) (Directed (UTF8.fromString fname) 0 0 0 0) input of
Failure doc -> do iputStrLn (show doc)
-- FIXME: Get error location from trifecta
--let errl = sourceLine (errorPos err)
i <- getIState
putIState (i { errLine = Just 0 }) -- Just errl })
return []
Success (x, i) -> do putIState i
return $ collect x
where mainProg :: IdrisParser ([PDecl], IState)
mainProg = case mrk of
Nothing -> do i <- get; return ([], i)
Just mrk -> do
release mrk
ds <- prog syn
i' <- get
return (ds, i')
-- | Collect 'PClauses' with the same function name
collect :: [PDecl] -> [PDecl]
collect (c@(PClauses _ o _ _) : ds)
= clauses (cname c) [] (c : ds)
where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]
clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)
| n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds
clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)
| n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds
clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs
clauses Nothing acc (x:xs) = collect xs
clauses Nothing acc [] = []
cname :: PDecl -> Maybe Name
cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n
cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n
cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing
cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing
fcOf :: PDecl -> FC
fcOf (PClauses fc _ _ _) = fc
collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds
collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds
collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds
collect (PClass doc f s cs n ps ds : ds')
= PClass doc f s cs n ps (collect ds) : collect ds'
collect (PInstance f s cs n ps t en ds : ds')
= PInstance f s cs n ps t en (collect ds) : collect ds'
collect (d : ds) = d : collect ds
collect [] = []
{- | Load idris module -}
loadModule :: FilePath -> Idris String
loadModule f
= idrisCatch (do i <- getIState
let file = takeWhile (/= ' ') f
ibcsd <- valIBCSubDir i
ids <- allImportDirs
fp <- liftIO $ findImport ids ibcsd file
if file `elem` imported i
then iLOG $ "Already read " ++ file
else do putIState (i { imported = file : imported i })
case fp of
IDR fn -> loadSource False fn
LIDR fn -> loadSource True fn
IBC fn src ->
idrisCatch (loadIBC fn)
(\c -> do iLOG $ fn ++ " failed " ++ show c
case src of
IDR sfn -> loadSource False sfn
LIDR sfn -> loadSource True sfn)
let (dir, fh) = splitFileName file
return (dropExtension fh))
(\e -> do let msg = show e
setErrLine (getErrLine msg)
iputStrLn msg
return "")
{- | Load idris code from file -}
loadFromIFile :: IFileType -> Idris ()
loadFromIFile i@(IBC fn src)
= do iLOG $ "Skipping " ++ getSrcFile i
idrisCatch (loadIBC fn)
(\c -> do fail $ fn ++ " failed " ++ show c)
where
getSrcFile (IDR fn) = fn
getSrcFile (LIDR fn) = fn
getSrcFile (IBC f src) = getSrcFile src
loadFromIFile (IDR fn) = loadSource' False fn
loadFromIFile (LIDR fn) = loadSource' True fn
{-| Load idris source code and show error if something wrong happens -}
loadSource' :: Bool -> FilePath -> Idris ()
loadSource' lidr r
= idrisCatch (loadSource lidr r)
(\e -> do let msg = show e
setErrLine (getErrLine msg)
iputStrLn msg)
{- | Load Idris source code-}
loadSource :: Bool -> FilePath -> Idris ()
loadSource lidr f
= do iLOG ("Reading " ++ f)
i <- getIState
let def_total = default_total i
file_in <- liftIO $ readFile f
file <- if lidr then tclift $ unlit f file_in else return file_in
(mname, modules, pos) <- parseImports f file
i <- getIState
putIState (i { default_access = Hidden })
clearIBC -- start a new .ibc file
mapM_ (addIBC . IBCImport) modules
ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname })
f file pos
unless (null ds') $ do
let ds = namespaces mname ds'
logLvl 3 (dumpDecls ds)
i <- getIState
logLvl 10 (show (toAlist (idris_implicits i)))
logLvl 3 (show (idris_infixes i))
-- Now add all the declarations to the context
v <- verbose
when v $ iputStrLn $ "Type checking " ++ f
-- we totality check after every Mutual block, so if
-- anything is a single definition, wrap it in a
-- mutual block on its own
elabDecls toplevel (map toMutual ds)
i <- getIState
-- simplify every definition do give the totality checker
-- a better chance
mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n
updateContext (simplifyCasedef n))
(map snd (idris_totcheck i))
-- build size change graph from simplified definitions
iLOG "Totality checking"
i <- getIState
mapM_ buildSCG (idris_totcheck i)
mapM_ checkDeclTotality (idris_totcheck i)
iLOG ("Finished " ++ f)
ibcsd <- valIBCSubDir i
iLOG "Universe checking"
iucheck
let ibc = ibcPathNoFallback ibcsd f
i <- getIState
addHides (hide_list i)
ok <- noErrors
when ok $
idrisCatch (do writeIBC f ibc; clearIBC)
(\c -> return ()) -- failure is harmless
i <- getIState
putIState (i { default_total = def_total,
hide_list = [] })
return ()
return ()
where
namespaces :: [String] -> [PDecl] -> [PDecl]
namespaces [] ds = ds
namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]
toMutual :: PDecl -> PDecl
toMutual m@(PMutual _ d) = m
toMutual x = let r = PMutual (FC "single mutual" 0) [x] in
case x of
PClauses _ _ _ _ -> r
PClass _ _ _ _ _ _ _ -> r
PInstance _ _ _ _ _ _ _ _ -> r
_ -> x
{- | Adds names to hide list -}
addHides :: [(Name, Maybe Accessibility)] -> Idris ()
addHides xs = do i <- getIState
let defh = default_access i
let (hs, as) = partition isNothing xs
unless (null as) $
mapM_ doHide
(map (\ (n, _) -> (n, defh)) hs ++
map (\ (n, Just a) -> (n, a)) as)
where isNothing (_, Nothing) = True
isNothing _ = False
doHide (n, a) = do setAccessibility n a
addIBC (IBCAccess n a)