{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-} {-# OPTIONS_GHC -O0 #-} module Idris.Parser(module Idris.Parser, module Idris.ParseExpr, module Idris.ParseData, module Idris.ParseHelpers, module Idris.ParseOps) where import Prelude hiding (pi) import Text.Trifecta.Delta import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err) 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 Text.PrettyPrint.ANSI.Leijen (Doc, plain) import qualified Text.PrettyPrint.ANSI.Leijen as ANSI import Idris.AbsSyntax hiding (namespace, params) import Idris.DSL import Idris.Imports import Idris.Delaborate import Idris.Error import Idris.Elab.Value import Idris.ElabDecls import Idris.ElabTerm import Idris.Coverage import Idris.IBC import Idris.Unlit import Idris.Providers import Idris.Output import Idris.ParseHelpers import Idris.ParseOps import Idris.ParseExpr import Idris.ParseData import Idris.Docstrings hiding (Unchecked) import Paths_idris import Util.DynamicLinker import qualified Util.Pretty as P import Idris.Core.TT import Idris.Core.Evaluate import Control.Applicative hiding (Const) import Control.Monad import Control.Monad.State.Strict import Data.Function import Data.Maybe import qualified Data.List.Split as Spl import Data.List import Data.Monoid import Data.Char import Data.Ord import qualified Data.Map as M import qualified Data.HashSet as HS import qualified Data.Text as T import qualified Data.ByteString.UTF8 as UTF8 import qualified Data.Set as S import Debug.Trace import System.FilePath import System.IO {- @ grammar shortcut notation: ~CHARSEQ = complement of char sequence (i.e. any character except CHARSEQ) RULE? = optional rule (i.e. RULE or nothing) RULE* = repeated rule (i.e. RULE zero or more times) RULE+ = repeated rule with at least one match (i.e. RULE one or more times) RULE! = invalid rule (i.e. rule that is not valid in context, report meaningful error in case) RULE{n} = rule repeated n times @ -} {- * Main grammar -} {- | Parses module definition @ ModuleHeader ::= DocComment_t? 'module' Identifier_t ';'?; @ -} moduleHeader :: IdrisParser (Maybe (Docstring ()), [String]) moduleHeader = try (do docs <- optional docComment noArgs docs reserved "module" i <- identifier option ';' (lchar ';') return (fmap fst docs, moduleName i)) <|> try (do lchar '%'; reserved "unqualified" return (Nothing, [])) <|> return (Nothing, moduleName "Main") where moduleName x = case span (/='.') x of (x, "") -> [x] (x, '.':y) -> x : moduleName y noArgs (Just (_, args)) | not (null args) = fail "Modules do not take arguments" noArgs _ = return () {- | Parses an import statement @ Import ::= 'import' Identifier_t ';'?; @ -} import_ :: IdrisParser (Bool, String, Maybe String, FC) import_ = do fc <- getFC reserved "import" reexport <- option False (do reserved "public"; return True) id <- identifier newName <- optional (reserved "as" *> identifier) option ';' (lchar ';') return (reexport, toPath id, toPath <$> newName, fc) "import statement" where toPath = foldl1' () . Spl.splitOn "." {- | Parses program source @ Prog ::= Decl* EOF; @ -} prog :: SyntaxInfo -> IdrisParser [PDecl] prog syn = do whiteSpace decls <- many (decl syn) let c = (concat decls) case maxline syn of Nothing -> do notOpenBraces; eof _ -> return () ist <- get fc <- getFC put ist { idris_parsedSpan = Just (FC (fc_fname fc) (0,0) (fc_end fc)), ibc_write = IBCParsedRegion fc : ibc_write ist } 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 fc <- getFC -- if we're after maxline, stop here let continue = case maxline syn of Nothing -> True Just l -> if fst (fc_end fc) > l then mut_nesting syn /= 0 else True if continue then do notEndBlock declBody else fail "End of readable input" 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 <|> provider syn <|> transform syn <|> do import_; fail "imports must be at top of file" "declaration" declBody' :: IdrisParser [PDecl] declBody' = do d <- decl' syn i <- get let d' = fmap (debindApp syn . (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 = fixity <|> syntaxDecl syn <|> fnDecl' syn <|> data_ syn <|> record 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 put (i `addSyntax` s) fc <- getFC return (PSyntax fc s) -- | Extend an 'IState' with a new syntax extension. See also 'addReplSyntax'. addSyntax :: IState -> Syntax -> IState addSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs, syntax_keywords = ks ++ ns, ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc } where rs = syntax_rules i ns = syntax_keywords i ibc = ibc_write i ks = map show (syntaxNames s) -- | Like 'addSyntax', but no effect on the IBC. addReplSyntax :: IState -> Syntax -> IState addReplSyntax i s = i { syntax_rules = updateSyntaxRules [s] rs, syntax_keywords = ks ++ ns } where rs = syntax_rules i ns = syntax_keywords i ks = map show (syntaxNames s) {- | Parses a syntax extension declaration @ SyntaxRuleOpts ::= 'term' | 'pattern'; @ @ SyntaxRule ::= SyntaxRuleOpts? 'syntax' SyntaxSym+ '=' TypeExpr Terminator; @ @ SyntaxSym ::= '[' Name_t ']' | '{' Name_t '}' | Name_t | StringLiteral_t ; @ -} syntaxRule :: SyntaxInfo -> IdrisParser Syntax syntaxRule syn = do sty <- try (do pushIndent sty <- option AnySyntax (do reserved "term"; return TermSyntax <|> do reserved "pattern"; return PatternSyntax) reserved "syntax" return sty) 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 -- Can't parse a full expression followed by operator like characters due to ambiguity mkSimple' (Expr e : Symbol s : es) | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es where ts = dropWhile isSpace . dropWhileEnd isSpace $ s 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 = checkFixity $ do (doc, argDocs, fc, opts', n, acc) <- try (do pushIndent (doc, argDocs) <- docstring syn 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 lchar ':' return (doc, argDocs, fc, opts', n, acc)) ty <- typeExpr (allowImp syn) terminator addAcc n acc return (PTy doc argDocs syn fc opts' n ty) <|> postulate syn <|> caf syn <|> pattern syn "function declaration" where checkFixity :: IdrisParser PDecl -> IdrisParser PDecl checkFixity p = do decl <- p case getName decl of Nothing -> return decl Just n -> do fOk <- fixityOK n unless fOk . fail $ "Missing fixity declaration for " ++ show n return decl getName (PTy _ _ _ _ _ n _) = Just n getName _ = Nothing fixityOK (NS n _) = fixityOK n fixityOK (UN n) | all (flip elem opChars) (str n) = do fixities <- fmap idris_infixes get return . elem (str n) . map (\ (Fix _ op) -> op) $ fixities | otherwise = return True fixityOK _ = return True {-| Parses function options given initial options @ FnOpts ::= 'total' | 'partial' | 'implicit' | '%' 'no_implicit' | '%' 'assert_total' | '%' 'error_handler' | '%' 'reflection' | '%' 'specialise' '[' NameTimesList? ']' ; @ @ NameTimes ::= FnName Natural?; @ @ NameTimesList ::= NameTimes | NameTimes ',' NameTimesList ; @ -} -- FIXME: Check compatability for function options (i.e. partal/total) -- -- Issue #1574 on the issue tracker. -- https://github.com/idris-lang/Idris-dev/issues/1574 fnOpts :: [FnOpt] -> IdrisParser [FnOpt] fnOpts opts = do reserved "total"; fnOpts (TotalFn : opts) <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn])) <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn])) <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral; fnOpts (CExport c : opts) <|> do try (lchar '%' *> reserved "no_implicit"); fnOpts (NoImplicit : opts) <|> do try (lchar '%' *> reserved "inline"); fnOpts (Inlinable : opts) <|> do try (lchar '%' *> reserved "assert_total"); fnOpts (AssertTotal : opts) <|> do try (lchar '%' *> reserved "error_handler"); fnOpts (ErrorHandler : opts) <|> do try (lchar '%' *> reserved "error_reverse"); fnOpts (ErrorReverse : opts) <|> do try (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 a postulate @ Postulate ::= DocComment_t? 'postulate' FnOpts* Accesibility? FnOpts* FnName TypeSig Terminator ; @ -} postulate :: SyntaxInfo -> IdrisParser PDecl postulate syn = do doc <- try $ do (doc, _) <- docstring syn pushIndent reserved "postulate" return doc 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 lchar ':' ty <- typeExpr (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 { mut_nesting = mut_nesting syn + 1 } )) 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 methods block (for instances) @ InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock @ -} instanceBlock :: SyntaxInfo -> IdrisParser [PDecl] instanceBlock syn = do reserved "where" openBlock ds <- many (fnDecl syn) closeBlock return (concat ds) "instance block" {- | Parses a methods and instances block (for type classes) @ MethodOrInstance ::= FnDecl | Instance ; @ @ ClassBlock ::= 'where' OpenBlock MethodOrInstance* CloseBlock ; @ -} classBlock :: SyntaxInfo -> IdrisParser [PDecl] classBlock syn = do reserved "where" openBlock ds <- many (notEndBlock >> instance_ syn <|> fnDecl syn) closeBlock return (concat ds) "class block" {-| Parses a type class declaration @ ClassArgument ::= Name | '(' Name ':' Expr ')' ; @ @ Class ::= DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock? ; @ -} class_ :: SyntaxInfo -> IdrisParser [PDecl] class_ syn = do (doc, argDocs, acc) <- try (do (doc, argDocs) <- docstring syn acc <- optional accessibility reserved "class" return (doc, argDocs, acc)) fc <- getFC cons <- constraintList syn n_in <- fnName let n = expandNS syn n_in cs <- many carg fds <- option (map fst cs) fundeps ds <- option [] (classBlock syn) accData acc n (concatMap declared ds) return [PClass doc syn fc cons n cs argDocs fds ds] "type-class declaration" where fundeps :: IdrisParser [Name] fundeps = do lchar '|'; sepBy name (lchar ',') 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 ::= DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock? ; @ @ InstanceName ::= '[' Name ']'; @ -} instance_ :: SyntaxInfo -> IdrisParser [PDecl] instance_ syn = do (doc, argDocs) <- try (docstring syn <* reserved "instance") fc <- getFC en <- optional instanceName cs <- constraintList syn cn <- fnName args <- many (simpleExpr syn) let sc = PApp fc (PRef fc cn) (map pexp args) let t = bindList (PPi constraint) cs sc ds <- option [] (instanceBlock syn) return [PInstance doc argDocs 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" -- | Parse a docstring docstring :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name,Docstring (Either Err PTerm))]) docstring syn = do (doc, argDocs) <- option noDocs docComment ist <- get let doc' = annotCode (tryFullExpr syn ist) doc argDocs' = [ (n, annotCode (tryFullExpr syn ist) d) | (n, d) <- argDocs ] return (doc', argDocs') {- | Parses a using declaration list @ UsingDeclList ::= UsingDeclList' | NameList TypeSig ; @ @ UsingDeclList' ::= UsingDecl | UsingDecl ',' UsingDeclList' ; @ @ NameList ::= Name | Name ',' NameList ; @ -} usingDeclList :: SyntaxInfo -> IdrisParser [Using] usingDeclList syn = try (sepBy1 (usingDecl syn) (lchar ',')) <|> do ns <- sepBy1 name (lchar ',') lchar ':' t <- typeExpr (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 lchar ':' t <- typeExpr (disallowImp syn) return (UImplicit x t)) <|> do c <- fnName xs <- some fnName return (UConstraint c xs) "using declaration" {- | Parse a clause with patterns @ Pattern ::= Clause; @ -} pattern :: SyntaxInfo -> IdrisParser PDecl pattern syn = do fc <- getFC clause <- clause syn return (PClauses fc [] (sMN 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 "?="; fc <- getFC name <- option n' (do symbol "{"; n <- fnName; symbol "}"; return n) r <- expr syn return (addLet fc name r) <|> do reserved "impossible"; return PImpossible "function right hand side" where mkN :: Name -> Name mkN (UN x) = if (tnull x || not (isAlpha (thead x))) then sUN "infix_op_lemma_1" else sUN (str x++"_lemma_1") mkN (NS x n) = NS (mkN x) n n' :: Name n' = mkN n addLet :: FC -> Name -> PTerm -> PTerm addLet fc nm (PLet fc' n ty val r) = PLet fc' n ty val (addLet fc nm r) addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs) where addLetC (l, r) = (l, addLet fc nm r) addLet fc nm r = (PLet fc (sUN "value") Placeholder r (PMetavar nm)) {- |Parses a function clause @ RHSOrWithBlock ::= RHS WhereOrTerminator | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock ; @ @ Clause ::= WExpr+ RHSOrWithBlock | SimpleExpr '<==' FnName RHS WhereOrTerminator | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -} | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock ; @ @ ImplicitOrArgExpr ::= ImplicitArg | ArgExpr; @ @ WhereOrTerminator ::= WhereBlock | Terminator; @ -} clause :: SyntaxInfo -> IdrisParser PClause clause syn = do wargs <- try (do pushIndent; some (wExpr syn)) fc <- getFC ist <- get n <- case lastParse ist of Just t -> return t Nothing -> fail "Invalid clause" (do 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) <|> (do popIndent reserved "with" wval <- simpleExpr syn pn <- optProof openBlock ds <- some $ fnDecl syn let withs = concat ds closeBlock return $ PWithR fc wargs wval pn withs) <|> do ty <- try (do pushIndent ty <- simpleExpr syn symbol "<==" return ty) 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 fc (sMN 0 "match") ty (PMatchApp fc n) (PRef fc (sMN 0 "match")) ist <- get put (ist { lastParse = Just n }) return $ PClause fc n capp [] r wheres <|> do (l, op) <- try (do pushIndent l <- argExpr syn op <- operator when (op == "=" || op == "?=" ) $ fail "infix clause definition with \"=\" and \"?=\" not supported " return (l, op)) let n = expandNS syn (sUN op) r <- argExpr syn fc <- getFC wargs <- many (wExpr syn) (do 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 popIndent reserved "with" wval <- bracketed syn pn <- optProof 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 pn withs) <|> 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) (do 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 ([], [])] ist <- get put (ist { lastParse = Just n }) return $ PClause fc n capp wargs r wheres) <|> (do reserved "with" ist <- get put (ist { lastParse = Just n }) wval <- bracketed syn pn <- optProof openBlock ds <- some $ fnDecl syn let withs = map (fillLHSD n capp wargs) $ concat ds closeBlock popIndent return $ PWith fc n capp wargs wval pn withs) "function clause" where optProof = option Nothing (do reserved "proof" n <- fnName return (Just n)) 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 pn ws) = PWith fc n capp (owargs ++ wargs) v pn (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 { inPattern = True }) "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_ = do n <- identifier; return (Via (map toLower n)) <|> 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 | 'name' Name NameList | 'error_handlers' Name NameList | 'language' 'TypeProviders' | 'language' 'ErrorReflection' ; @ -} directive :: SyntaxInfo -> IdrisParser [PDecl] directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral; return [PDirective (do addLib cgn lib addIBC (IBCLib cgn lib))] <|> do try (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)] <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_; flag <- stringLiteral return [PDirective (do addIBC (IBCCGFlag cgn flag) addFlag cgn flag)] <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral; return [PDirective (do addHdr cgn hdr addIBC (IBCHeader cgn hdr))] <|> do try (lchar '%' *> reserved "hide"); n <- fnName return [PDirective (do setAccessibility n Hidden addIBC (IBCAccess n Hidden))] <|> do try (lchar '%' *> reserved "freeze"); n <- iName [] return [PDirective (do setAccessibility n Frozen addIBC (IBCAccess n Frozen))] <|> do try (lchar '%' *> reserved "access"); acc <- accessibility return [PDirective (do i <- get put(i { default_access = acc }))] <|> do try (lchar '%' *> reserved "default"); tot <- totality i <- get put (i { default_total = tot } ) return [PDirective (do i <- get put(i { default_total = tot }))] <|> do try (lchar '%' *> reserved "logging"); i <- natural; return [PDirective (setLogLevel (fromInteger i))] <|> do try (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)] <|> do try (lchar '%' *> reserved "name") ty <- fnName ns <- sepBy1 name (lchar ',') return [PDirective (do ty' <- disambiguate ty mapM_ (addNameHint ty') ns mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)] <|> do try (lchar '%' *> reserved "error_handlers") fn <- fnName arg <- fnName ns <- sepBy1 name (lchar ',') return [PDirective (do fn' <- disambiguate fn ns' <- mapM disambiguate ns addFunctionErrorHandlers fn' arg ns' mapM_ (addIBC . IBCFunctionErrorHandler fn' arg) ns')] <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt; return [PDirective (addLangExt ext)] <|> do fc <- getFC try (lchar '%' *> reserved "used") fn <- fnName arg <- iName [] return [PDirective (addUsedName fc fn arg)] "directive" where disambiguate :: Name -> Idris Name disambiguate n = do i <- getIState case lookupCtxtName n (idris_implicits i) of [(n', _)] -> return n' [] -> throwError (NoSuchVariable n) more -> throwError (CantResolveAlts (map fst more)) pLangExt :: IdrisParser LanguageExt pLangExt = (reserved "TypeProviders" >> return TypeProviders) <|> (reserved "ErrorReflection" >> return ErrorReflection) {- | 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 ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr; ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate' @ -} provider :: SyntaxInfo -> IdrisParser [PDecl] provider syn = do doc <- try (do (doc, _) <- docstring syn lchar '%' reserved "provide" return doc) provideTerm doc <|> providePostulate doc "type provider" where provideTerm doc = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')' fc <- getFC reserved "with" e <- expr syn "provider expression" return [PProvider doc syn fc (ProvTerm t e) n] providePostulate doc = do reserved "postulate" n <- fnName fc <- getFC reserved "with" e <- expr syn "provider expression" return [PProvider doc syn fc (ProvPostulate e) n] {- | Parses a transform @ Transform ::= '%' 'transform' Expr '==>' Expr @ -} transform :: SyntaxInfo -> IdrisParser [PDecl] transform syn = do try (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" {- * Loading and parsing -} {- | Parses an expression from input -} parseExpr :: IState -> String -> Result PTerm parseExpr st = runparser (fullExpr defaultSyntax) st "(input)" {- | Parses a constant form input -} parseConst :: IState -> String -> Result Const parseConst st = runparser constant st "(input)" {- | Parses a tactic from input -} parseTactic :: IState -> String -> Result PTactic parseTactic st = runparser (fullTactic defaultSyntax) st "(input)" -- | Parse module header and imports parseImports :: FilePath -> String -> Idris (Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta) parseImports fname input = do i <- getIState case parseString (runInnerParser (evalStateT imports i)) (Directed (UTF8.fromString fname) 0 0 0 0) input of Failure err -> fail (show err) Success (x, i) -> do putIState i return x where imports :: IdrisParser ((Maybe (Docstring ()), [String], [(Bool, String, Maybe String, FC)], Maybe Delta), IState) imports = do whiteSpace (mdoc, mname) <- moduleHeader ps <- many import_ mrk <- mark isEof <- lookAheadMatches eof let mrk' = if isEof then Nothing else Just mrk i <- get return ((mdoc, mname, ps, mrk'), i) -- | There should be a better way of doing this... findFC :: Doc -> (FC, String) findFC x = let s = show (plain x) in case span (/= ':') s of (failname, ':':rest) -> case span isDigit rest of (line, ':':rest') -> case span isDigit rest' of (col, ':':msg) -> let pos = (read line, read col) in (FC failname pos pos, msg) -- | Check if the coloring matches the options and corrects if necessary fixColour :: Bool -> ANSI.Doc -> ANSI.Doc fixColour False doc = ANSI.plain doc fixColour True doc = doc -- | 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 runparser mainProg i fname input of Failure doc -> do -- FIXME: Get error location from trifecta -- this can't be the solution! -- Issue #1575 on the issue tracker. -- https://github.com/idris-lang/Idris-dev/issues/1575 let (fc, msg) = findFC doc i <- getIState case idris_outputmode i of RawOutput h -> iputStrLn (show $ fixColour (idris_colourRepl i) doc) IdeMode n h -> iWarn fc (P.text msg) putIState (i { errSpan = Just fc }) return [] Success (x, i) -> do putIState i reportParserWarnings 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') {- | Load idris module and show error if something wrong happens -} loadModule :: FilePath -> Idris (Maybe String) loadModule f = idrisCatch (loadModule' f) (\e -> do setErrSpan (getErrSpan e) ist <- getIState iWarn (getErrSpan e) $ pprintErr ist e return Nothing) {- | Load idris module -} loadModule' :: FilePath -> Idris (Maybe String) loadModule' f = do i <- getIState let file = takeWhile (/= ' ') f ibcsd <- valIBCSubDir i ids <- allImportDirs fp <- findImport ids ibcsd file if file `elem` imported i then do iLOG $ "Already read " ++ file return Nothing else do putIState (i { imported = file : imported i }) case fp of IDR fn -> loadSource False fn Nothing LIDR fn -> loadSource True fn Nothing IBC fn src -> idrisCatch (loadIBC True fn) (\c -> do iLOG $ fn ++ " failed " ++ pshow i c case src of IDR sfn -> loadSource False sfn Nothing LIDR sfn -> loadSource True sfn Nothing) return $ Just file {- | Load idris code from file -} loadFromIFile :: Bool -> IFileType -> Maybe Int -> Idris () loadFromIFile reexp i@(IBC fn src) maxline = do iLOG $ "Skipping " ++ getSrcFile i idrisCatch (loadIBC reexp fn) (\err -> ierror $ LoadingFailed fn err) where getSrcFile (IDR fn) = fn getSrcFile (LIDR fn) = fn getSrcFile (IBC f src) = getSrcFile src loadFromIFile _ (IDR fn) maxline = loadSource' False fn maxline loadFromIFile _ (LIDR fn) maxline = loadSource' True fn maxline {-| Load idris source code and show error if something wrong happens -} loadSource' :: Bool -> FilePath -> Maybe Int -> Idris () loadSource' lidr r maxline = idrisCatch (loadSource lidr r maxline) (\e -> do setErrSpan (getErrSpan e) ist <- getIState case e of At f e' -> iWarn f (pprintErr ist e') _ -> iWarn (getErrSpan e) (pprintErr ist e)) {- | Load Idris source code-} loadSource :: Bool -> FilePath -> Maybe Int -> Idris () loadSource lidr f toline = do iLOG ("Reading " ++ f) i <- getIState let def_total = default_total i file_in <- runIO $ readFile f file <- if lidr then tclift $ unlit f file_in else return file_in (mdocs, mname, imports_in, pos) <- parseImports f file ai <- getAutoImports let imports = map (\n -> (True, n, Just n, emptyFC)) ai ++ imports_in ids <- allImportDirs ibcsd <- valIBCSubDir i mapM_ (\(re, f) -> do fp <- findImport ids ibcsd f case fp of LIDR fn -> ifail $ "No ibc for " ++ f IDR fn -> ifail $ "No ibc for " ++ f IBC fn src -> loadIBC True fn) [(re, fn) | (re, fn, _, _) <- imports] reportParserWarnings -- process and check module aliases let modAliases = M.fromList [(prep alias, prep realName) | (reexport, realName, Just alias, fc) <- imports] prep = map T.pack . reverse . Spl.splitOn "/" aliasNames = [(alias, fc) | (_, _, Just alias, fc) <- imports] histogram = groupBy ((==) `on` fst) . sortBy (comparing fst) $ aliasNames case map head . filter ((/= 1) . length) $ histogram of [] -> logLvl 3 $ "Module aliases: " ++ show (M.toList modAliases) (n,fc):_ -> throwError . At fc . Msg $ "import alias not unique: " ++ show n i <- getIState putIState (i { default_access = Hidden, module_aliases = modAliases }) clearIBC -- start a new .ibc file -- record package info in .ibc imps <- allImportDirs mapM_ addIBC (map IBCImportDir imps) mapM_ (addIBC . IBCImport) [(reexport, realName) | (reexport, realName, alias, fc) <- imports] let syntax = defaultSyntax{ syn_namespace = reverse mname, maxline = toline } ist <- getIState -- Save the span from parsing the module header, because -- an empty program parse might obliterate it. let oldSpan = idris_parsedSpan ist ds' <- parseProg syntax f file pos case (ds', oldSpan) of ([], Just fc) -> -- If no program elements were parsed, we dind't -- get a loaded region in the IBC file. That -- means we need to add it back. do ist <- getIState putIState ist { idris_parsedSpan = oldSpan , ibc_write = IBCParsedRegion fc : ibc_write ist } _ -> return () -- Parsing done, now process declarations let ds = namespaces mname ds' logLvl 3 (show $ showDecls verbosePPOption ds) i <- getIState logLvl 10 (show (toAlist (idris_implicits i))) logLvl 3 (show (idris_infixes i)) -- Now add all the declarations to the context 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 $ getErasureInfo i)) (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) -- Redo totality check for deferred names let deftots = idris_defertotcheck i iLOG $ "Totality checking " ++ show deftots mapM_ (\x -> do tot <- getTotality x case tot of Total _ -> setTotality x Unchecked _ -> return ()) (map snd deftots) mapM_ buildSCG deftots mapM_ checkDeclTotality deftots iLOG ("Finished " ++ f) ibcsd <- valIBCSubDir i iLOG "Universe checking" iucheck let ibc = ibcPathNoFallback ibcsd f i <- getIState addHides (hide_list i) -- Save module documentation if applicable i <- getIState case mdocs of Nothing -> return () Just docs -> addModDoc syntax mname docs -- Finally, write an ibc if checking was successful 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 () 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 (PNamespace x ds) = PNamespace x (map toMutual ds) toMutual x = let r = PMutual (fileFC "single mutual") [x] in case x of PClauses{} -> r PClass{} -> r PInstance{} -> r _ -> x addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris () addModDoc syn mname docs = do ist <- getIState docs' <- elabDocTerms recinfo (parsedDocs ist) let modDocs' = addDef docName docs' (idris_moduledocs ist) putIState ist { idris_moduledocs = modDocs' } addIBC (IBCModDocs docName) where docName = NS modDocName (map T.pack (reverse mname)) parsedDocs ist = annotCode (tryFullExpr syn ist) docs {- | 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)