idris 0.9.9.1 → 0.9.9.2
raw patch · 24 files changed
+3080/−1938 lines, 24 filesdep +llvm-general-puredep +parsersdep +trifectadep ~llvm-general
Dependencies added: llvm-general-pure, parsers, trifecta, unordered-containers, utf8-string
Dependency ranges changed: llvm-general
Files
- idris.cabal +4/−3
- lib/Network/Cgi.idr +9/−4
- lib/Prelude.idr +5/−0
- lib/System.idr +47/−2
- llvm/defs.c +7/−0
- rts/idris_stdfgn.c +6/−0
- rts/idris_stdfgn.h +2/−0
- src/IRTS/Bytecode.hs +21/−17
- src/IRTS/CodegenLLVM.hs +7/−7
- src/Idris/AbsSyntax.hs +3/−2
- src/Idris/AbsSyntaxTree.hs +3/−2
- src/Idris/Chaser.hs +1/−1
- src/Idris/Coverage.hs +36/−2
- src/Idris/ElabDecls.hs +21/−18
- src/Idris/Parser.hs +2771/−1757
- src/Idris/Prover.hs +22/−20
- src/Idris/REPL.hs +47/−40
- src/Idris/REPLParser.hs +60/−56
- src/Main.hs +1/−1
- src/Util/LLVMStubs.hs +2/−1
- test/reg003/expected +1/−1
- test/test002/expected +0/−1
- test/test002/test002.idr +3/−2
- test/test020/expected +1/−1
idris.cabal view
@@ -1,5 +1,5 @@ Name: idris-Version: 0.9.9.1+Version: 0.9.9.2 License: BSD3 License-file: LICENSE Author: Edwin Brady@@ -285,7 +285,8 @@ containers, process, transformers, filepath, directory, binary, bytestring, text, pretty, language-java>=0.2.2, libffi,- vector, vector-binary-instances, ansi-terminal+ vector, vector-binary-instances, ansi-terminal,+ utf8-string, unordered-containers, parsers>=0.9, trifecta>=1.1 Extensions: MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, TemplateHaskell@@ -303,6 +304,6 @@ if flag(LLVM) other-modules: IRTS.CodegenLLVM cpp-options: -DIDRIS_LLVM- build-depends: llvm-general==3.3.5.*+ build-depends: llvm-general==3.3.8.*, llvm-general-pure==3.3.8.* else other-modules: Util.LLVMStubs
lib/Network/Cgi.idr view
@@ -115,15 +115,20 @@ getC (n-1) (strCons x acc) else (return "") +getCgiEnv : String -> IO String+getCgiEnv key = do+ val <- getEnv key+ return $ maybe "" id val + abstract runCGI : CGI a -> IO a runCGI prog = do - clen_in <- getEnv "CONTENT_LENGTH"+ clen_in <- getCgiEnv "CONTENT_LENGTH" let clen = prim__fromStrInt clen_in content <- getContent clen- query <- getEnv "QUERY_STRING"- cookie <- getEnv "HTTP_COOKIE"- agent <- getEnv "HTTP_USER_AGENT"+ query <- getCgiEnv "QUERY_STRING"+ cookie <- getCgiEnv "HTTP_COOKIE"+ agent <- getCgiEnv "HTTP_USER_AGENT" let get_vars = getVars ['&',';'] query let post_vars = getVars ['&'] content
lib/Prelude.idr view
@@ -479,6 +479,11 @@ return (ok /= 0); partial+nullStr : String -> IO Bool+nullStr p = do ok <- mkForeign (FFun "isNull" [FString] FInt) p+ return (ok /= 0);++partial validFile : File -> IO Bool validFile (FHandle h) = do x <- nullPtr h return (not x)
lib/System.idr view
@@ -20,8 +20,53 @@ do arg <- getArg i ga' (arg :: acc) (i+1) n -getEnv : String -> IO String-getEnv x = mkForeign (FFun "getenv" [FString] FString) x+-- Retrieves an value from the environment, if the given key is present,+-- otherwise it returns Nothing.+getEnv : String -> IO (Maybe String)+getEnv key = do + str_ptr <- getEnv'+ is_nil <- nullStr str_ptr+ if is_nil+ then pure Nothing+ else pure (Just str_ptr)+ where+ getEnv' : IO String+ getEnv' = mkForeign (FFun "getenv" [FString] FString) key++-- Sets an environment variable with a given value.+-- Returns true if the operation was successful.+setEnv : String -> String -> IO Bool+setEnv key value = do+ ok <- mkForeign (FFun "setenv" [FString, FString, FInt] FInt) key value 1+ return (ok == 0)++-- Unsets an environment variable.+-- Returns true if the variable was able to be unset.+unsetEnv : String -> IO Bool+unsetEnv key = do+ ok <- mkForeign (FFun "unsetenv" [FString] FInt) key+ return (ok == 0)++getEnvironment : IO (List (String, String))+getEnvironment = getAllPairs 0 []+ where+ getEnvPair : Int -> IO String+ getEnvPair i = mkForeign (FFun "getEnvPair" [FInt] FString) i++ splitEq : String -> (String, String)+ splitEq str =+ -- FIXME: There has to be a better way to split this up+ let (k, v) = break (== '=') str in+ let (_, v') = break (/= '=') v in+ (k, v')++ getAllPairs : Int -> List String -> IO (List (String, String))+ getAllPairs n acc = do+ envPair <- getEnvPair n+ is_nil <- nullStr envPair+ if is_nil+ then return $ reverse $ map splitEq acc+ else getAllPairs (n + 1) (envPair :: acc) exit : Int -> IO () exit code = mkForeign (FFun "exit" [FInt] FUnit) code
llvm/defs.c view
@@ -1,9 +1,12 @@+#include <stdlib.h> #include <stdio.h> #include <gmp.h> #include <gc.h> #include <string.h> #include <inttypes.h> +extern char** environ;+ void putStr(const char *str) { fputs(str, stdout); }@@ -117,6 +120,10 @@ int isNull(void* ptr) { return ptr==NULL;+}++char* getEnvPair(int i) {+ return *(environ + i); } void idris_memset(void* ptr, size_t offset, uint8_t c, size_t size) {
rts/idris_stdfgn.c view
@@ -1,6 +1,8 @@ #include "idris_stdfgn.h" #include "idris_rts.h" +extern char** environ;+ void putStr(char* str) { printf("%s", str); }@@ -36,4 +38,8 @@ void* idris_stdin() { return (void*)stdin;+}++char* getEnvPair(int i) {+ return *(environ + i); }
rts/idris_stdfgn.h view
@@ -15,4 +15,6 @@ int isNull(void* ptr); void* idris_stdin(); +char* getEnvPair(int i);+ #endif
src/IRTS/Bytecode.hs view
@@ -8,7 +8,7 @@ import Core.TT import Data.Maybe -{- We have: +{- We have: BASE: Current stack frame's base TOP: Top of stack@@ -32,14 +32,14 @@ | CASE Bool -- definitely a constructor, no need to check, if true Reg [(Int, [BC])] (Maybe [BC]) | PROJECT Reg Int Int -- get all args from reg, put them from Int onwards- | PROJECTINTO Reg Reg Int -- project argument from one reg into another + | PROJECTINTO Reg Reg Int -- project argument from one reg into another | CONSTCASE Reg [(Const, [BC])] (Maybe [BC]) | CALL Name | TAILCALL Name- | FOREIGNCALL Reg FLang FType String [(FType, Reg)] - | SLIDE Int -- move this number from TOP to BASE + | FOREIGNCALL Reg FLang FType String [(FType, Reg)]+ | SLIDE Int -- move this number from TOP to BASE | REBASE -- set BASE = OLDBASE- | RESERVE Int -- reserve n more stack items + | RESERVE Int -- reserve n more stack items -- (i.e. check there's space, grow if necessary) | ADDTOP Int -- move the top of stack up | TOPBASE Int -- set TOP = BASE + n@@ -51,7 +51,7 @@ deriving Show toBC :: (Name, SDecl) -> (Name, [BC])-toBC (n, SFun n' args locs exp) +toBC (n, SFun n' args locs exp) = (n, reserve locs ++ bc RVal exp True) where reserve 0 = [] reserve n = [RESERVE n, ADDTOP n]@@ -63,10 +63,14 @@ [BC] bc reg (SV (Glob n)) r = bc reg (SApp False n []) r bc reg (SV (Loc i)) r = assign reg (L i) ++ clean r-bc reg (SApp False f vs) r- = RESERVE (length vs) : moveReg 0 vs- ++ [STOREOLD, BASETOP 0, ADDTOP (length vs), CALL f] ++ - assign reg RVal ++ clean r+bc reg (SApp False f vs) r =+ if argCount == 0+ then moveReg 0 vs ++ [STOREOLD, BASETOP 0, CALL f] ++ ret+ else RESERVE argCount : moveReg 0 vs +++ [STOREOLD, BASETOP 0, ADDTOP argCount, CALL f] ++ ret+ where+ ret = assign reg RVal ++ clean r+ argCount = length vs bc reg (SApp True f vs) r = RESERVE (length vs) : moveReg 0 vs ++ [SLIDE (length vs), TOPBASE (length vs), TAILCALL f]@@ -78,16 +82,16 @@ ++ clean r bc reg (SCon i _ vs) r = MKCON reg i (map getL vs) : clean r where getL (Loc x) = L x-bc reg (SProj (Loc l) i) r = PROJECTINTO reg (L l) i : clean r +bc reg (SProj (Loc l) i) r = PROJECTINTO reg (L l) i : clean r bc reg (SConst i) r = ASSIGNCONST reg i : clean r bc reg (SOp p vs) r = OP reg p (map getL vs) : clean r where getL (Loc x) = L x bc reg (SError str) r = [ERROR str] bc reg SNothing r = NULL reg : clean r-bc reg (SCase (Loc l) alts) r +bc reg (SCase (Loc l) alts) r | isConst alts = constCase reg (L l) alts r | otherwise = conCase True reg (L l) alts r-bc reg (SChkCase (Loc l) alts) r +bc reg (SChkCase (Loc l) alts) r = conCase False reg (L l) alts r isConst [] = False@@ -107,12 +111,12 @@ constCase reg l xs r = [CONSTCASE l (mapMaybe (constAlt l reg r) xs) (defaultAlt reg xs r)] -caseAlt l reg r (SConCase lvar tag _ args e) - = Just (tag, PROJECT l lvar (length args) : bc reg e r) +caseAlt l reg r (SConCase lvar tag _ args e)+ = Just (tag, PROJECT l lvar (length args) : bc reg e r) caseAlt l reg r _ = Nothing -constAlt l reg r (SConstCase c e) - = Just (c, bc reg e r) +constAlt l reg r (SConstCase c e)+ = Just (c, bc reg e r) constAlt l reg r _ = Nothing defaultAlt reg [] r = Nothing
src/IRTS/CodegenLLVM.hs view
@@ -19,7 +19,7 @@ , initializeAllTargets, lookupTarget ) import LLVM.General.AST.DataLayout-import LLVM.General.PassManager+import qualified LLVM.General.PassManager as PM import qualified LLVM.General.Module as M import qualified LLVM.General.AST.IntegerPredicate as IPred import qualified LLVM.General.AST.Linkage as L@@ -59,7 +59,7 @@ codegenLLVM :: [(TT.Name, SDecl)] -> String -> -- target triple String -> -- target CPU- Int -> -- Optimization degree+ Word -> -- Optimization degree FilePath -> -- output file name OutputType -> IO ()@@ -71,12 +71,12 @@ do layout <- getTargetMachineDataLayout tm let ast = codegen (Target triple layout) (map snd defs) result <- runErrorT . M.withModuleFromAST context ast $ \m ->- do let opts = defaultCuratedPassSetSpec- { optLevel = Just optimize- , simplifyLibCalls = Just True- , useInlinerWithThreshold = Just 225+ do let opts = PM.defaultCuratedPassSetSpec+ { PM.optLevel = Just optimize+ , PM.simplifyLibCalls = Just True+ , PM.useInlinerWithThreshold = Just 225 }- when (optimize /= 0) $ withPassManager opts $ void . flip runPassManager m+ when (optimize /= 0) $ PM.withPassManager opts $ void . flip PM.runPassManager m outputModule tm file outty m case result of Right _ -> return ()
src/Idris/AbsSyntax.hs view
@@ -23,6 +23,7 @@ import Data.Char import Data.Either import Data.Maybe+import Data.Word (Word) import Debug.Trace @@ -435,13 +436,13 @@ targetCPU = do i <- getIState return (opt_cpu (idris_options i)) -setOptLevel :: Int -> Idris ()+setOptLevel :: Word -> Idris () setOptLevel t = do i <- getIState let opts = idris_options i opt' = opts { opt_optLevel = t } putIState $ i { idris_options = opt' } -optLevel :: Idris Int+optLevel :: Idris Word optLevel = do i <- getIState return (opt_optLevel (idris_options i))
src/Idris/AbsSyntaxTree.hs view
@@ -24,6 +24,7 @@ import Data.List import Data.Char import Data.Either+import Data.Word (Word) import Debug.Trace @@ -42,7 +43,7 @@ opt_importdirs :: [FilePath], opt_triple :: String, opt_cpu :: String,- opt_optLevel :: Int,+ opt_optLevel :: Word, opt_cmdline :: [Opt] -- remember whole command line } deriving (Show, Eq)@@ -278,7 +279,7 @@ | InterpretScript String | TargetTriple String | TargetCPU String- | OptLevel Int+ | OptLevel Word deriving (Show, Eq) -- Parsed declarations
src/Idris/Chaser.hs view
@@ -128,7 +128,7 @@ if exist then do file_in <- liftIO $ readFile f file <- if lit then tclift $ unlit f file_in else return file_in- (_, modules, _, _) <- parseImports f file+ (_, modules, _) <- parseImports f file ms <- mapM (btree done) modules return (concat ms) else return []) -- IBC with no source available
src/Idris/Coverage.hs view
@@ -130,8 +130,41 @@ genAll i args = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of [] -> [Placeholder]- xs -> xs+ xs -> inventConsts xs where + -- if they're constants, invent a new one to make sure that+ -- constants which are not explicitly handled are covered+ inventConsts cs@(PConstant c : _) = map PConstant (ic' (mapMaybe getConst cs))+ where getConst (PConstant c) = Just c+ getConst _ = Nothing+ inventConsts xs = xs++ -- try constants until they're not in the list. + -- FIXME: It is, of course, possible that someone has enumerated all + -- the constants and matched on them (maybe in generated code) and this + -- will be really slow. This is sufficiently unlikely that we won't + -- worry for now... ++ ic' xs@(I _ : _) = firstMissing xs (lotsOfNums I) + ic' xs@(BI _ : _) = firstMissing xs (lotsOfNums BI)+ ic' xs@(Fl _ : _) = firstMissing xs (lotsOfNums Fl) + ic' xs@(B8 _ : _) = firstMissing xs (lotsOfNums B8) + ic' xs@(B16 _ : _) = firstMissing xs (lotsOfNums B16) + ic' xs@(B32 _ : _) = firstMissing xs (lotsOfNums B32) + ic' xs@(B64 _ : _) = firstMissing xs (lotsOfNums B64) + ic' xs@(Ch _ : _) = firstMissing xs lotsOfChars+ ic' xs@(Str _ : _) = firstMissing xs lotsOfStrings + -- TODO: Bit vectors+ -- The rest are types with only one case+ ic' xs = xs++ firstMissing cs (x : xs) | x `elem` cs = firstMissing cs xs+ | otherwise = x : cs++ lotsOfNums t = map t [0..]+ lotsOfChars = map Ch ['a'..]+ lotsOfStrings = map Str (map (("some string " ++).show) [1..])+ conForm (PApp _ (PRef fc n) _) = isConName n (tt_ctxt i) conForm (PRef fc n) = isConName n (tt_ctxt i) conForm _ = False@@ -149,7 +182,8 @@ otherPats o@(PDPair fc t _ v) = ops fc (UN "Ex_intro") ([pimp (UN "a") Placeholder, pimp (UN "P") Placeholder] ++- [pexp t,pexp v]) o + [pexp t,pexp v]) o+ otherPats o@(PConstant c) = return o otherPats arg = return Placeholder ops fc n xs_in o
src/Idris/ElabDecls.hs view
@@ -62,7 +62,7 @@ (errAt "type of " n (erun fc (build i info False n ty))) ds <- checkDef fc defer addDeferred ds- mapM_ (elabCaseBlock info) is + mapM_ (elabCaseBlock info opts) is ctxt <- getContext logLvl 5 $ "Rechecking" logLvl 6 $ show tyT@@ -128,7 +128,7 @@ (erun fc (build i info False n t)) def' <- checkDef fc defer addDeferredTyCon def'- mapM_ (elabCaseBlock info) is+ mapM_ (elabCaseBlock info []) is (cty, _) <- recheckC fc [] t' logLvl 2 $ "---> " ++ show cty updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons@@ -145,7 +145,7 @@ (errAt "data declaration " n (erun fc (build i info False n t))) def' <- checkDef fc defer addDeferredTyCon def'- mapM_ (elabCaseBlock info) is+ mapM_ (elabCaseBlock info []) is (cty, _) <- recheckC fc [] t' logLvl 2 $ "---> " ++ show cty -- temporary, to check cons@@ -492,7 +492,7 @@ logLvl 2 $ "Rechecking " ++ show t' def' <- checkDef fc defer addDeferred def'- mapM_ (elabCaseBlock info) is+ mapM_ (elabCaseBlock info []) is ctxt <- getContext (cty, _) <- recheckC fc [] t' let cty' = normaliseC ctxt [] cty@@ -528,7 +528,7 @@ -- question: CAFs in where blocks? tclift $ tfail $ At fc (NoTypeDecl n) [ty] -> return ty- pats_in <- mapM (elabClause info (Dictionary `elem` opts)) + pats_in <- mapM (elabClause info opts) (zip [0..] cs) logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in @@ -748,7 +748,7 @@ (build i info aspat (MN 0 "val") (infTerm tm))) def' <- checkDef (FC "(input)" 0) defer addDeferred def'- mapM_ (elabCaseBlock info) is+ mapM_ (elabCaseBlock info []) is logLvl 3 ("Value: " ++ show tm') recheckC (FC "(input)" 0) [] tm'@@ -778,16 +778,18 @@ -- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b) err@(Error _) -> return False -elabClause :: ElabInfo -> Bool -> (Int, PClause) -> +elabClause :: ElabInfo -> FnOpts -> (Int, PClause) -> Idris (Either Term (Term, Term))-elabClause info tcgen (_, PClause fc fname lhs_in [] PImpossible [])- = do b <- checkPossible info fc tcgen fname lhs_in+elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])+ = do let tcgen = Dictionary `elem` opts+ b <- checkPossible info fc tcgen fname lhs_in case b of True -> fail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case" False -> do ptm <- mkPatTm lhs_in return (Left ptm)-elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock) - = do ctxt <- getContext+elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock) + = do let tcgen = Dictionary `elem` opts+ ctxt <- getContext -- Build the LHS as an "Infer", and pull out its type and -- pattern bindings i <- getIState@@ -857,7 +859,7 @@ -- from the where block mapM_ (elabDecl' EAll info) wafter- mapM_ (elabCaseBlock info) is+ mapM_ (elabCaseBlock info opts) is ctxt <- getContext logLvl 5 $ "Rechecking"@@ -937,8 +939,9 @@ = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x)) ps) propagateParams ps x = x -elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock) - = do ctxt <- getContext+elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock) + = do let tcgen = Dictionary `elem` opts+ ctxt <- getContext -- Build the LHS as an "Infer", and pull out its type and -- pattern bindings i <- getIState@@ -970,7 +973,7 @@ return (tt, d, is)) def' <- checkDef fc defer addDeferred def'- mapM_ (elabCaseBlock info) is+ mapM_ (elabCaseBlock info opts) is (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval') let cwvaltyN = explicitNames cwvalty let cwvalN = explicitNames cwval@@ -1026,7 +1029,7 @@ return (tt, d, is)) def' <- checkDef fc defer addDeferred def'- mapM_ (elabCaseBlock info) is+ mapM_ (elabCaseBlock info opts) is logLvl 5 ("Checked RHS " ++ show rhs') (crhs, crhsty) <- recheckC fc [] rhs' return $ Right (clhs, crhs)@@ -1549,10 +1552,10 @@ = elabTransform info fc safety old new elabDecl' _ _ _ = return () -- skipped this time -elabCaseBlock info d@(PClauses f o n ps) +elabCaseBlock info opts d@(PClauses f o n ps) = do addIBC (IBCDef n) logLvl 6 $ "CASE BLOCK: " ++ show (n, d)- elabDecl' EAll info d + elabDecl' EAll info (PClauses f (nub (o ++ opts)) n ps ) -- elabDecl' info (PImport i) = loadModule i
src/Idris/Parser.hs view
@@ -1,1758 +1,2772 @@-{-# LANGUAGE PatternGuards, ScopedTypeVariables #-}--- | Parse the full Idris language.-module Idris.Parser where--import Idris.AbsSyntax-import Idris.DSL-import Idris.Imports-import Idris.Error-import Idris.ElabDecls-import Idris.ElabTerm-import Idris.Coverage-import Idris.IBC-import Idris.Unlit-import Idris.Providers-import Paths_idris--import Util.DynamicLinker--import Core.CoreParser-import Core.TT-import Core.Evaluate--import Text.Parsec-import Text.Parsec.Error-import Text.Parsec.Expr-import Text.Parsec.Language-import Text.Parsec.String-import qualified Text.Parsec.Token as PTok--import Data.List-import Data.List.Split(splitOn)-import Control.Monad.State-import Control.Monad.Error-import Debug.Trace-import Data.Maybe-import System.FilePath--type TokenParser a = PTok.TokenParser a--type IParser = GenParser Char IState--lexer :: TokenParser IState-lexer = idrisLexer--whiteSpace = PTok.whiteSpace lexer-lexeme = PTok.lexeme lexer-symbol = PTok.symbol lexer-natural = PTok.natural lexer-parens = PTok.parens lexer-semi = PTok.semi lexer-comma = PTok.comma lexer-identifier = PTok.identifier lexer-reserved = PTok.reserved lexer-operator = PTok.operator lexer-reservedOp = PTok.reservedOp lexer-integer = PTok.integer lexer-float = PTok.float lexer-strlit = PTok.stringLiteral lexer-chlit = PTok.charLiteral lexer-lchar = lexeme.char--fixErrorMsg :: String -> [String] -> String-fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)---- Loading modules--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 "")--loadFromIFile :: IFileType -> Idris ()-loadFromIFile i@(IBC fn src) - = do iLOG $ "Skipping " ++ getSrcFile i- idrisCatch (loadIBC fn)- (\c -> do fail $ fn ++ " failed " ++ show c)--- loadFromIFile src)- 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--loadSource' lidr r - = idrisCatch (loadSource lidr r)- (\e -> do let msg = show e- setErrLine (getErrLine msg)- iputStrLn msg)--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, rest, pos) <- parseImports f file- i <- getIState- putIState (i { default_access = Hidden })--- mapM_ loadModule modules- clearIBC -- start a new .ibc file- mapM_ (addIBC . IBCImport) modules- ds' <- parseProg (defaultSyntax {syn_namespace = reverse mname }) - f rest 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 [] ds = ds- namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]-- 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--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)--parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"-parseTac i = runParser (do t <- pTactic defaultSyntax- eof- return t) i "(proof)"--parseImports :: FilePath -> String -> Idris ([String], [String], String, SourcePos)-parseImports fname input - = do i <- getIState- case runParser (do whiteSpace- mname <- pHeader- ps <- many pImport- rest <- getInput- pos <- getPosition- return ((mname, ps, rest, pos), i)) i fname input of- Left err -> fail (show err)- Right (x, i) -> do -- Discard state updates (there should be- -- none anyway) - return x--pHeader :: IParser [String]-pHeader = try (do reserved "module"; i <- identifier; option ';' (lchar ';')- return (parseName i))- <|> return []- where parseName x = case span (/='.') x of- (x, "") -> [x]- (x, '.':y) -> x : parseName y--pushIndent :: IParser ()-pushIndent = do pos <- getPosition- ist <- getState- setState (ist { indent_stack = sourceColumn pos :- indent_stack ist })--lastIndent :: IParser Int-lastIndent = do ist <- getState- case indent_stack ist of- (x : xs) -> return x- _ -> return 1--indent :: IParser Int-indent = liftM sourceColumn getPosition--popIndent :: IParser ()-popIndent = do ist <- getState- let (x : xs) = indent_stack ist- setState (ist { indent_stack = xs })--openBlock :: IParser ()-openBlock = do lchar '{'- ist <- getState- setState (ist { brace_stack = Nothing : brace_stack ist })- <|> do ist <- getState- 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'- setState (ist { brace_stack = Just lvl : brace_stack ist })--closeBlock :: IParser ()-closeBlock = do ist <- getState- bs <- case brace_stack ist of- [] -> eof >> return []- Nothing : xs -> (lchar '}' >> return xs) <|> (eof >> return [])- Just lvl : xs -> (do i <- indent- inp <- getInput--- trace (show (take 10 inp, i, lvl)) $- if i >= lvl && take 1 inp /= ")" - then fail "Not end of block"- else return xs) <|> (eof >> return [])- setState (ist { brace_stack = bs })--pTerminator = do lchar ';'; popIndent- <|> do c <- indent; l <- lastIndent- if c <= l - then popIndent- else fail "Not a terminator"- <|> do i <- getInput- if "}" `isPrefixOf` i || ")" `isPrefixOf` i- then popIndent - else fail "Not a terminator"- <|> lookAhead eof--pBarTerminator - = do lchar '|'; return ()- <|> do c <- indent; l <- lastIndent- unless (c <= l) $ fail "Not a terminator"- <|> lookAhead eof--pKeepTerminator - = do lchar ';'; return ()- <|> do c <- indent; l <- lastIndent- unless (c <= l) $ fail "Not a terminator"- <|> do i <- getInput- let h = take 1 i- unless (h `elem` ["}", ")", "|"]) $ fail "Not a terminator"- <|> lookAhead eof--notEndApp = do c <- indent; l <- lastIndent- i <- getInput- when (c <= l) $ fail "Terminator"--notEndBlock = do ist <- getState- case brace_stack ist of- Just lvl : xs -> do i <- indent- inp <- getInput- when (i < lvl || ")" `isPrefixOf` inp) $ fail "End of block"- _ -> return ()---- | Use Parsec's internal state to construct a source code position-pfc :: IParser FC-pfc = do s <- getPosition- let (dir, file) = splitFileName (sourceName s)- let f = if dir == addTrailingPathSeparator "." then file else sourceName s- return $ FC f (sourceLine s)--pImport :: IParser String-pImport = do reserved "import"; f <- identifier; option ';' (lchar ';')- return (toPath f)- where toPath n = foldl1' (</>) $ splitOn "." n---- | A program is a list of declarations, possibly with associated--- documentation strings.-parseProg :: SyntaxInfo -> FilePath -> String -> SourcePos -> - Idris [PDecl]-parseProg syn fname input pos- = do i <- getIState- case runParser (do setPosition pos- whiteSpace- ps <- many (pDecl syn)- eof- i' <- getState- return (concat ps, i')) i fname input of- Left err -> do iputStrLn (show err)- let errl = sourceLine (errorPos err)- i <- getIState- putIState (i { errLine = Just errl })- return []- Right (x, i) -> do putIState i- return (collect x)---- | Collect 'PClauses' with the same function name-collect :: [PDecl] -> [PDecl]-collect (c@(PClauses _ o _ _) : ds) - = clauses (cname c) [] (c : ds)- where 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 (getfc c) o n (reverse acc) : collect xs- clauses Nothing acc (x:xs) = collect xs- clauses Nothing acc [] = []-- cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n- cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n- cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing- cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing- getfc (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 [] = []--pFullExpr :: SyntaxInfo -> IParser PTerm-pFullExpr syn - = do x <- pExpr syn; eof;- i <- getState- return $ desugar syn i x---- | Parse a top-level declaration-pDecl :: SyntaxInfo -> IParser [PDecl]-pDecl syn = do notEndBlock- pDeclBody where- pDeclBody- = do d <- pDecl' syn- i <- getState- let d' = fmap (desugar syn i) d- return [d']- <|> pUsing syn- <|> pParams syn- <|> pMutual syn- <|> pNamespace syn- <|> pClass syn- <|> pInstance syn- <|> do d <- pDSL syn; return [d]- <|> pDirective syn- <|> try (pProvider syn)- <|> pTransform syn- <|> try (do reserved "import"; fp <- identifier- fail "imports must be at the top of file") --pFunDecl :: SyntaxInfo -> IParser [PDecl]-pFunDecl syn- = try (do notEndBlock- d <- pFunDecl' syn- i <- getState- let d' = fmap (desugar syn i) d- return [d'])----------- Top Level Declarations -----------pDecl' :: SyntaxInfo -> IParser PDecl-pDecl' syn- = try pFixity- <|> try (pFunDecl' syn)- <|> try (pData syn)- <|> try (pRecord syn)- <|> try (pSyntaxDecl syn)--pSyntaxDecl :: SyntaxInfo -> IParser PDecl-pSyntaxDecl syn- = do s <- pSyntaxRule syn- i <- getState- let rs = syntax_rules i- let ns = syntax_keywords i- let ibc = ibc_write i- let ks = map show (names s)- setState (i { syntax_rules = s : rs,- syntax_keywords = ks ++ ns,- ibc_write = IBCSyntax s : map IBCKeyword ks ++ ibc- })- fc <- pfc- return (PSyntax fc s)- where- names (Rule syms _ _) = mapMaybe ename syms- ename (Keyword n) = Just n- ename _ = Nothing--pSyntaxRule :: SyntaxInfo -> IParser Syntax-pSyntaxRule syn - = do pushIndent- sty <- option AnySyntax (do reserved "term"; return TermSyntax- <|> do reserved "pattern"; return PatternSyntax)- reserved "syntax"- syms <- many1 pSynSym- when (all expr syms) $ fail "No keywords in syntax rule"- let ns = mapMaybe name syms- when (length ns /= length (nub ns)) - $ fail "Repeated variable in syntax rule"- lchar '='- tm <- pTExpr (impOK syn)- pTerminator- return (Rule (mkSimple syms) tm sty)- where- expr (Expr _) = True- expr _ = False- name (Expr n) = Just n- name _ = 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' [] = []--pSynSym :: IParser SSymbol-pSynSym = try (do lchar '['; n <- pName; lchar ']'- return (Expr n))- <|> try (do lchar '{'; n <- pName; lchar '}'- return (Binding n))- <|> do n <- iName []- return (Keyword n)- <|> do sym <- strlit- return (Symbol sym)--pFunDecl' :: SyntaxInfo -> IParser PDecl-pFunDecl' syn = try (do doc <- option "" (pDocComment '|')- pushIndent- ist <- getState- let initOpts = if default_total ist- then [TotalFn]- else []- opts <- pFnOpts initOpts- acc <- pAccessibility- opts' <- pFnOpts opts- n_in <- pfName- let n = expandNS syn n_in- fc <- pfc- ty <- pTSig (impOK syn)- pTerminator --- ty' <- implicit syn n ty- addAcc n acc- return (PTy doc syn fc opts' n ty))- <|> try (pPostulate syn)- <|> try (pPattern syn)- <|> try (pCAF syn)--pPostulate :: SyntaxInfo -> IParser PDecl-pPostulate syn = do doc <- option "" (pDocComment '|')- pushIndent- reserved "postulate"- ist <- getState- let initOpts = if default_total ist- then [TotalFn]- else []- opts <- pFnOpts initOpts- acc <- pAccessibility- opts' <- pFnOpts opts- n_in <- pfName- let n = expandNS syn n_in- ty <- pTSig (impOK syn)- fc <- pfc- pTerminator - addAcc n acc- return (PPostulate doc syn fc opts' n ty)---pUsing :: SyntaxInfo -> IParser [PDecl]-pUsing syn = - do reserved "using"; lchar '('; ns <- usingDeclList syn; lchar ')'- openBlock- let uvars = using syn- ds <- many1 (pDecl (syn { using = uvars ++ ns }))- closeBlock- return (concat ds)--pParams :: SyntaxInfo -> IParser [PDecl]-pParams syn = - do reserved "parameters"; lchar '('; ns <- tyDeclList syn; lchar ')'- openBlock - let pvars = syn_params syn- ds <- many1 (pDecl syn { syn_params = pvars ++ ns })- closeBlock - fc <- pfc- return [PParams fc ns (concat ds)]--pMutual :: SyntaxInfo -> IParser [PDecl]-pMutual syn = - do reserved "mutual"- openBlock - let pvars = syn_params syn- ds <- many1 (pDecl syn)- closeBlock - fc <- pfc- return [PMutual fc (concat ds)]--pNamespace :: SyntaxInfo -> IParser [PDecl]-pNamespace syn =- do reserved "namespace"; n <- identifier;- openBlock - ds <- many1 (pDecl syn { syn_namespace = n : syn_namespace syn })- closeBlock- return [PNamespace n (concat ds)] ----------- Fixity -----------pFixity :: IParser PDecl-pFixity = do pushIndent- f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')- pTerminator - let prec = fromInteger i- istate <- getState- 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 setState (istate { idris_infixes = nub $ sort (fs ++ infixes)- , ibc_write = map IBCFix fs ++ ibc_write istate- })- fc <- pfc- return (PFix fc (f prec) ops)- else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""- ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill- 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--fixity :: IParser (Int -> Fixity) -fixity = try (do reserved "infixl"; return Infixl)- <|> try (do reserved "infixr"; return Infixr)- <|> try (do reserved "infix"; return InfixN)- <|> try (do reserved "prefix"; return PrefixN)----------- Type classes -----------pClass :: SyntaxInfo -> IParser [PDecl]-pClass syn = do doc <- option "" (pDocComment '|')- acc <- pAccessibility- reserved "class"; fc <- pfc; cons <- pConstList syn; n_in <- pName- let n = expandNS syn n_in- cs <- many carg- reserved "where"; openBlock - ds <- many $ pFunDecl syn- closeBlock- let allDs = concat ds- accData acc n (concatMap declared allDs)- return [PClass doc syn fc cons n cs allDs]- where- carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'- return (i, ty)- <|> do i <- pName;- return (i, PType)--pInstance :: SyntaxInfo -> IParser [PDecl]-pInstance syn = do reserved "instance"; fc <- pfc- en <- option Nothing- (do lchar '['; n_in <- pfName; lchar ']'- let n = expandNS syn n_in- return (Just n))- cs <- pConstList syn- cn <- pName- args <- many (pSimpleExpr syn)- let sc = PApp fc (PRef fc cn) (map pexp args)- let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc- reserved "where"; openBlock - ds <- many $ pFunDecl syn- closeBlock- return [PInstance syn fc cs cn args t en (concat ds)]----------- Expressions -----------pExpr syn = do i <- getState- buildExpressionParser (table (idris_infixes i)) (pExpr' syn)--pExpr' :: SyntaxInfo -> IParser PTerm-pExpr' syn - = try (pExtExpr syn)- <|> pNoExtExpr syn--pExtExpr :: SyntaxInfo -> IParser PTerm-pExtExpr syn = do i <- getState- pExtensions syn (syntax_rules i)--pSimpleExtExpr :: SyntaxInfo -> IParser PTerm-pSimpleExtExpr syn = do i <- getState- pExtensions syn (filter simple (syntax_rules i))- where- simple (Rule (Expr x:xs) _ _) = False- simple (Rule (SimpleExpr x:xs) _ _) = False- simple (Rule [Keyword _] _ _) = True- simple (Rule [Symbol _] _ _) = True- simple (Rule (_:xs) _ _) = case last xs of- Keyword _ -> True- Symbol _ -> True- _ -> False- simple _ = False--pNoExtExpr syn =- try (pApp syn) - <|> try (pMatchApp syn)- <|> try (pUnifyLog syn)- <|> pRecordType syn- <|> try (pSimpleExpr syn)- <|> pLambda syn- <|> pQuoteGoal syn- <|> pLet syn- <|> pRewriteTerm syn- <|> pPi syn - <|> pDoBlock syn- -pExtensions :: SyntaxInfo -> [Syntax] -> IParser PTerm-pExtensions syn rules = choice (map (try . pExt syn) (filter valid rules))- where- valid (Rule _ _ AnySyntax) = True- valid (Rule _ _ PatternSyntax) = inPattern syn- valid (Rule _ _ TermSyntax) = not (inPattern syn)---data SynMatch = SynTm PTerm | SynBind Name--pExt :: SyntaxInfo -> Syntax -> IParser PTerm-pExt syn (Rule ssym ptm _)- = do smap <- mapM pSymbol ssym- let ns = mapMaybe id smap- return (update ns ptm) -- updated with smap- where- pSymbol (Keyword n) = do reserved (show n); return Nothing- pSymbol (Expr n) = do tm <- pExpr syn- return $ Just (n, SynTm tm)- pSymbol (SimpleExpr n) = do tm <- pSimpleExpr syn- return $ Just (n, SynTm tm)- pSymbol (Binding n) = do b <- pName- return $ Just (n, SynBind b)- pSymbol (Symbol s) = do symbol s- return Nothing- dropn n [] = []- dropn n ((x,t) : xs) | n == x = xs- | otherwise = (x,t):dropn n xs-- updateB ns n = case lookup n ns of- Just (SynBind t) -> t- _ -> n-- 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 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--pName = do i <- getState- iName (syntax_keywords i)- <|> do reserved "instance"- i <- getState- UN n <- iName (syntax_keywords i)- return (UN ('@':n))---- | Parser for an operator in function position, i.e. enclosed by `()', with an--- optional namespace.-pOpFront = maybeWithNS pOpFrontNoNS False []- where pOpFrontNoNS = do lchar '('; o <- operator; lchar ')'; return o--pfName = try pOpFront- <|> pName--pTotality :: IParser Bool-pTotality- = do reserved "total"; return True- <|> do reserved "partial"; return False--pAccessibility' :: IParser Accessibility-pAccessibility'- = do reserved "public"; return Public- <|> do reserved "abstract"; return Frozen- <|> do reserved "private"; return Hidden--pAccessibility :: IParser (Maybe Accessibility)-pAccessibility- = do acc <- pAccessibility'; return (Just acc)- <|> return Nothing--pFnOpts :: [FnOpt] -> IParser [FnOpt]-pFnOpts opts- = do reserved "total"; pFnOpts (TotalFn : opts)- <|> do reserved "partial"; pFnOpts (PartialFn : (opts \\ [TotalFn]))- <|> try (do lchar '%'; reserved "export"; c <- strlit; - pFnOpts (CExport c : opts))- <|> try (do lchar '%'; reserved "assert_total"; - pFnOpts (AssertTotal : opts))- <|> try (do lchar '%'; reserved "reflection"; - pFnOpts (Reflection : opts))- <|> do lchar '%'; reserved "specialise"; - lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'- pFnOpts (Specialise ns : opts)- <|> do reserved "implicit"; pFnOpts (Implicit : opts)- <|> return opts- where nameTimes = do n <- pfName- t <- option Nothing (do reds <- natural- return (Just (fromInteger reds)))- return (n, t)--addAcc :: Name -> Maybe Accessibility -> IParser ()-addAcc n a = do i <- getState- setState (i { hide_list = (n, a) : hide_list i })--pCaseExpr syn = do- reserved "case"; fc <- pfc; scr <- pExpr syn; reserved "of";- openBlock - pushIndent- opts <- many1 (do notEndBlock- x <- pCaseOpt syn- pKeepTerminator- return x) -- sepBy1 (pCaseOpt syn) (lchar '|')- popIndent- closeBlock- return (PCase fc scr opts)--pProofExpr syn = do- reserved "proof"; lchar '{'- ts <- endBy (pTactic syn) (lchar ';')- lchar '}'- return (PProof ts)--pTacticsExpr syn = do- reserved "tactics"; lchar '{'- ts <- endBy (pTactic syn) (lchar ';')- lchar '}'- return (PTactics ts)--pSimpleExpr syn = - try (do symbol "!["; t <- pTerm; lchar ']'; return $ PQuote t)- <|> do lchar '?'; x <- pName; return (PMetavar x)- <|> do lchar '%'; fc <- pfc; reserved "instance"; return (PResolveTC fc)- <|> do reserved "refl"; fc <- pfc; - tm <- option Placeholder (do lchar '{'; t <- pExpr syn; lchar '}';- return t)- return (PRefl fc tm)--- <|> do reserved "return"; fc <- pfc; return (PReturn fc)- <|> pProofExpr syn - <|> pTacticsExpr syn- <|> pCaseExpr syn- <|> try (do x <- pfName- fc <- pfc- return (PRef fc x))- <|> try (pList syn)- <|> try (pComprehension syn)- <|> try (pAlt syn)- <|> try (pIdiom syn)- <|> try (do lchar '('- bracketed (noImp syn))- <|> try (do c <- pConstant- fc <- pfc- return (modifyConst syn fc (PConstant c)))- <|> do reserved "Type"; return PType- <|> try (do symbol "()"- fc <- pfc- return (PTrue fc))- <|> try (do symbol "_|_"- fc <- pfc- return (PFalse fc))- <|> do lchar '_'; return Placeholder- <|> pSimpleExtExpr syn--bracketed syn =- try (pPair syn)- <|> try (do e <- pExpr syn; lchar ')'; return e)--- <|> try (do reserved "typed"--- e <- pExpr syn; symbol ":"; t <- pExpr syn; lchar ')'--- return (PTyped e t))- <|> try (do fc <- pfc; o <- operator; e <- pExpr 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 <- pfc; e <- pSimpleExpr syn; o <- operator; lchar ')'- return $ PLam (MN 1000 "ARG") Placeholder- (PApp fc (PRef fc (UN o)) [pexp e,- pexp (PRef fc (MN 1000 "ARG"))]))--pCaseOpt :: SyntaxInfo -> IParser (PTerm, PTerm)-pCaseOpt syn = do lhs <- pExpr (syn { inPattern = True }) - symbol "=>"; rhs <- pExpr syn- return (lhs, rhs)---- 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--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---pList syn = do lchar '['; fc <- pfc; xs <- sepBy (pExpr syn) (lchar ','); lchar ']'- return (mkList fc xs)- where- mkList fc [] = PRef fc (UN "Nil")- mkList fc (x : xs) = PApp fc (PRef fc (UN "::")) [pexp x, pexp (mkList fc xs)] --pPair syn = try (do l <- pExpr syn - fc <- pfc- 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 <- pName; lchar ':'- lty <- pExpr syn- reservedOp "**"- fc <- pfc- r <- pExpr syn- lchar ')'- return (PDPair fc (PRef fc ln) lty r) - where- restTuple = do lchar ')'; return []- <|> do lchar ','- r <- pExpr syn- lchar ')'- return [Left r]- <|> do reservedOp "**"- r <- pExpr syn- lchar ')'- return [Right r]- ntuple = try (do l <- pExpr syn; fc <- pfc; lchar ','- rest <- ntuple- return (PPair fc l rest))- <|> (do l <- pExpr syn; fc <- pfc; lchar ','- r <- pExpr syn- return (PPair fc l r))- -pAlt syn = do symbol "(|"; alts <- sepBy1 (pExpr' syn) (lchar ','); symbol "|)"- return (PAlternative False alts)--pHSimpleExpr syn- = do lchar '.'- e <- pSimpleExpr syn- return $ PHidden e- <|> pSimpleExpr syn--pMatchApp syn = do ty <- pSimpleExpr syn- symbol "<=="- fc <- pfc- f <- pfName- return (PLet (MN 0 "match")- ty- (PMatchApp fc f)- (PRef fc (MN 0 "match")))--pUnifyLog syn = do lchar '%'; reserved "unifyLog";- tm <- pSimpleExpr syn- return (PUnifyLog tm)--pApp syn = do f <- reserved "mkForeign"- fc <- pfc- fn <- pArg syn- args <- many (do notEndApp; pArg syn)- i <- getState- -- 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 <- pSimpleExpr syn- fc <- pfc- args <- many1 (do notEndApp- pArg syn)- i <- getState- return (dslify i $ PApp fc f args)- where- 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--pArg :: SyntaxInfo -> IParser PArg-pArg syn = try (pImplicitArg syn)- <|> try (pConstraintArg syn)- <|> do e <- pSimpleExpr syn- return (pexp e)--pImplicitArg syn = do lchar '{'- n <- pName- fc <- pfc- v <- option (PRef fc n) (do lchar '='- pExpr syn)- lchar '}'- return (pimp n v)--pConstraintArg syn = do symbol "@{"- e <- pExpr syn- symbol "}"- return (pconst e)--pRecordType syn - = do reserved "record"- lchar '{'- fields <- sepBy1 pFieldType (lchar ',')- lchar '}'- fc <- pfc- rec <- option Nothing (do e <- pSimpleExpr syn- return (Just e))- 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)- where pFieldType = do n <- pfName- lchar '='- e <- pExpr syn- return (n, e)- applyAll fc [] x = x- applyAll fc ((n, e) : es) x- = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])- -mkType (UN n) = UN ("set_" ++ n)-mkType (MN 0 n) = MN 0 ("set_" ++ n)-mkType (NS n s) = NS (mkType n) s--noImp syn = syn { implicitAllowed = False }-impOK syn = syn { implicitAllowed = True }--pTSig syn = do lchar ':'; pTExpr syn--pTExpr syn = do cs <- if implicitAllowed syn then pConstList syn else return []- sc <- pExpr syn - return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)--pLambda syn = do lchar '\\'- try (do xt <- tyOptDeclList syn- symbol "=>"- sc <- pExpr syn- return (bindList PLam xt sc)- <|> (do ps <- sepBy (do fc <- pfc- e <- pSimpleExpr syn- return (fc, e)) (lchar ',')- symbol "=>"- sc <- pExpr syn- return (pmList (zip [0..] ps) sc)))- where 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)])--pRewriteTerm syn = - do reserved "rewrite"- fc <- pfc- prf <- pExpr syn- giving <- option Nothing- (do symbol "==>"; tm <- pExpr' syn- return (Just tm))- reserved "in"; sc <- pExpr syn- return (PRewrite fc - (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc- giving)--pLet syn = try (do reserved "let"; n <- pName; - ty <- option Placeholder (do lchar ':'; pExpr' syn)- lchar '='- v <- pExpr syn- reserved "in"; sc <- pExpr syn- return (PLet n ty v sc))- <|> (do reserved "let"; fc <- pfc; pat <- pExpr' (syn { inPattern = True } )- symbol "="; v <- pExpr syn- reserved "in"; sc <- pExpr syn- return (PCase fc v [(pat, sc)]))--pQuoteGoal syn = do reserved "quoteGoal"; n <- pName;- reserved "by"- r <- pExpr syn- reserved "in"- fc <- pfc- sc <- pExpr syn- return (PGoal fc r n sc)--pPi syn = - try (do lazy <- if implicitAllowed syn -- laziness is top level only- then option False (do lchar '|'; return True)- else return False- st <- pStatic- lchar '('; xt <- tyDeclList syn; lchar ')'- doc <- option "" (pDocComment '^')- symbol "->"- sc <- pExpr syn- return (bindList (PPi (Exp lazy st doc)) xt sc))- <|> try (if implicitAllowed syn - then do lazy <- option False (do lchar '|'- return True)- st <- pStatic- lchar '{'- xt <- tyDeclList syn- lchar '}'- symbol "->"- sc <- pExpr syn- return (bindList (PPi (Imp lazy st "")) xt sc)- else fail "No implicit arguments allowed here")- <|> try (do lchar '{'- reserved "auto"- xt <- tyDeclList syn- lchar '}'- symbol "->"- sc <- pExpr syn- return (bindList (PPi - (TacImp False Dynamic (PTactics [Trivial]) "")) xt sc))- <|> try (do lchar '{'- reserved "default"- script <- pSimpleExpr syn - xt <- tyDeclList syn- lchar '}'- symbol "->"- sc <- pExpr syn- return (bindList (PPi (TacImp False Dynamic script "")) xt sc))- <|> do --lazy <- option False (do lchar '|'; return True)- lchar '{'- reserved "static"- lchar '}'- t <- pExpr' syn- symbol "->"- sc <- pExpr syn- return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)--pConstList :: SyntaxInfo -> IParser [PTerm]-pConstList syn = try (do lchar '(' - tys <- sepBy1 (pExpr' (noImp syn)) (lchar ',')- lchar ')'- reservedOp "=>"- return tys)- <|> try (do t <- pExpr (noImp syn)- reservedOp "=>"- return [t])- <|> return []--usingDeclList syn - = try (sepBy1 (usingDecl syn) (lchar ','))- <|> do ns <- sepBy1 pName (lchar ',')- t <- pTSig (noImp syn)- return (map (\x -> UImplicit x t) ns)--usingDecl syn = try (do x <- pfName- t <- pTSig (noImp syn)- return (UImplicit x t))- <|> do c <- pfName- xs <- many1 pfName- return (UConstraint c xs)--tyDeclList syn = try (sepBy1 (do x <- pfName- t <- pTSig (noImp syn)- return (x,t))- (lchar ','))- <|> do ns <- sepBy1 pName (lchar ',')- t <- pTSig (noImp syn)- return (map (\x -> (x, t)) ns)--tyOptDeclList syn = sepBy1 (do x <- pNameOrPlaceholder - t <- option Placeholder (do lchar ':'- pExpr syn) - return (x,t))- (lchar ',')- where pNameOrPlaceholder = pfName- <|> do symbol "_"- return (MN 0 "underscore")--bindList b [] sc = sc-bindList b ((n, t):bs) sc = b n t (bindList b bs sc)--pComprehension syn- = do lchar '['- fc <- pfc- pat <- pExpr syn- lchar '|'- qs <- sepBy1 (pDo syn) (lchar ',')- lchar ']'- return (PDoBlock (map addGuard qs ++ - [DoExp fc (PApp fc (PRef fc (UN "return"))- [pexp pat])]))- where addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (UN "guard"))- [pexp e])- addGuard x = x--pDoBlock syn - = do reserved "do"- openBlock- pushIndent- ds <- many1 (do notEndBlock- x <- pDo syn- pKeepTerminator- return x)- popIndent- closeBlock- return (PDoBlock ds)--pDo syn- = try (do reserved "let"- i <- pName; - ty <- option Placeholder (do lchar ':'- pExpr' syn)- reservedOp "="- fc <- pfc- e <- pExpr syn- return (DoLet fc i ty e))- <|> try (do reserved "let"- i <- pExpr' syn- reservedOp "="- fc <- pfc- sc <- pExpr syn- return (DoLetP fc i sc))- <|> try (do i <- pName- symbol "<-"- fc <- pfc- e <- pExpr syn;- return (DoBind fc i e))- <|> try (do i <- pExpr' syn- symbol "<-"- fc <- pfc- e <- pExpr syn;- return (DoBindP fc i e))- <|> try (do e <- pExpr syn- fc <- pfc- return (DoExp fc e))--pIdiom syn- = do symbol "[|"- fc <- pfc- e <- pExpr syn- symbol "|]"- return (PIdiom fc e)--pConstant :: IParser Const-pConstant = 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 <- strlit; return $ Str s)- <|> try (do c <- chlit; return $ Ch c)--pStatic :: IParser Static-pStatic = do lchar '['- reserved "static"- lchar ']';- return Static- <|> return Dynamic--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]]--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 name f = Infix (do fc <- pfc- reservedOp name- doc <- option "" (pDocComment '^')- return (f fc)) -prefix name f = Prefix (do reservedOp name- fc <- pfc;- return (f fc))-backtick = Infix (do lchar '`'; n <- pfName- lchar '`'- fc <- pfc- return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone----------- Data declarations ------------- (works for classes too - 'abstract' means the data/class is visible but members not)-accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()-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--pRecord :: SyntaxInfo -> IParser PDecl-pRecord syn = do doc <- option "" (pDocComment '|')- acc <- pAccessibility- reserved "record"- fc <- pfc- tyn_in <- pfName- ty <- pTSig (impOK syn)- let tyn = expandNS syn tyn_in- reserved "where"- openBlock- pushIndent- (cdoc, cn, cty, _) <- pConstructor syn- pKeepTerminator- popIndent- closeBlock- 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- where- getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]- ++ getRecNames syn sc- getRecNames _ _ = []-- toFreeze (Just Frozen) = Just Hidden- toFreeze x = x--pDataI = do reserved "data"; return False- <|> do reserved "codata"; return True--pData :: SyntaxInfo -> IParser PDecl-pData syn = try (do doc <- option "" (pDocComment '|')- acc <- pAccessibility- co <- pDataI- fc <- pfc- tyn_in <- pfName- ty <- pTSig (impOK syn)- let tyn = expandNS syn tyn_in- option (PData doc syn fc co (PLaterdecl tyn ty)) (do- reserved "where"- openBlock- pushIndent- cons <- many (do notEndBlock- c <- pConstructor syn- pKeepTerminator- return c) -- (lchar '|')- popIndent- closeBlock - accData acc tyn (map (\ (_, n, _, _) -> n) cons)- return $ PData doc syn fc co (PDatadecl tyn ty cons)))- <|> try (do doc <- option "" (pDocComment '|')- pushIndent- acc <- pAccessibility- co <- pDataI- fc <- pfc- tyn_in <- pfName- args <- many pName- 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 (pSimpleCon syn) (lchar '|')- pTerminator- 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')))- where- 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--pConstructor :: SyntaxInfo -> IParser (String, Name, PTerm, FC)-pConstructor syn - = do doc <- option "" (pDocComment '|')- cn_in <- pfName; fc <- pfc- let cn = expandNS syn cn_in- ty <- pTSig (impOK syn)--- ty' <- implicit syn cn ty- return (doc, cn, ty, fc)- --pSimpleCon :: SyntaxInfo -> IParser (String, Name, [PTerm], FC)-pSimpleCon syn - = do cn_in <- pfName- let cn = expandNS syn cn_in- fc <- pfc- args <- many (do notEndApp- pSimpleExpr syn)- doc <- option "" (pDocComment '^')- return (doc, cn, args, fc)----------- DSL syntax overloading -----------pDSL :: SyntaxInfo -> IParser PDecl-pDSL syn = do reserved "dsl"- n <- pfName- openBlock- pushIndent- bs <- many1 (do notEndBlock- b <- pOverload syn- pKeepTerminator- return b)- popIndent; closeBlock- let dsl = mkDSL bs (dsl_info syn)- checkDSL dsl- i <- getState- setState (i { idris_dsls = addDef n dsl (idris_dsls i) })- return (PDSL n dsl)- where 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 }--checkDSL :: DSL -> IParser ()-checkDSL dsl = return ()--pOverload :: SyntaxInfo -> IParser (String, PTerm)-pOverload 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 <- pExpr syn- return (o, t)- where overloadable = ["let","lambda","index_first","index_next","variable"]----------- Pattern match clauses -----------pPattern :: SyntaxInfo -> IParser PDecl-pPattern syn = do fc <- pfc- clause <- pClause syn- return (PClauses fc [] (MN 2 "_") [clause]) -- collect together later--pCAF :: SyntaxInfo -> IParser PDecl-pCAF syn = do reserved "let"- n_in <- pfName; let n = expandNS syn n_in- lchar '='- t <- pExpr syn- pTerminator- fc <- pfc- return (PCAF fc n t)--pArgExpr syn = let syn' = syn { inPattern = True } in- try (pHSimpleExpr syn') <|> pSimpleExtExpr syn'--pRHS :: SyntaxInfo -> Name -> IParser PTerm-pRHS syn n = do lchar '='; pExpr syn- <|> do symbol "?="; - name <- option n' (do symbol "{"; n <- pfName; symbol "}";- return n)- rhs <- pExpr syn- return (addLet name rhs)- <|> do reserved "impossible"; return PImpossible- where mkN (UN x) = UN (x++"_lemma_1")- mkN (NS x n) = NS (mkN x) n- n' = mkN n-- addLet nm (PLet n ty val rhs) = PLet n ty val (addLet nm rhs)- addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)- where addLetC (l, r) = (l, addLet nm r)- addLet nm rhs = (PLet (UN "value") Placeholder rhs (PMetavar nm)) --pClause :: SyntaxInfo -> IParser PClause-pClause syn- = try (do pushIndent- n_in <- pfName; let n = expandNS syn n_in- cargs <- many (pConstraintArg syn)- iargs <- many (pImplicitArg (syn { inPattern = True } ))- fc <- pfc- args <- many (try (pImplicitArg (syn { inPattern = True } ))- <|> (fmap pexp (pArgExpr syn)))- wargs <- many (pWExpr syn)- rhs <- pRHS syn n- ist <- getState- let ctxt = tt_ctxt ist- let wsyn = syn { syn_namespace = [] }- (wheres, nmap) <- choice [do x <- pWhereblock n wsyn- popIndent- return x, - do pTerminator- return ([], [])]- let capp = PApp fc (PRef fc n) - (iargs ++ cargs ++ args)- ist <- getState- setState (ist { lastParse = Just n })- return $ PClause fc n capp wargs rhs wheres)- <|> try (do pushIndent- ty <- pSimpleExpr syn- symbol "<=="- fc <- pfc- n_in <- pfName; let n = expandNS syn n_in- rhs <- pRHS syn n- ist <- getState- let ctxt = tt_ctxt ist- let wsyn = syn { syn_namespace = [] }- (wheres, nmap) <- choice [do x <- pWhereblock n wsyn- popIndent- return x, - do pTerminator- return ([], [])]- let capp = PLet (MN 0 "match")- ty- (PMatchApp fc n)- (PRef fc (MN 0 "match"))- ist <- getState- setState (ist { lastParse = Just n })- return $ PClause fc n capp [] rhs wheres)- <|> try (do pushIndent- wargs <- many1 (pWExpr syn)- ist <- getState- n <- case lastParse ist of- Just t -> return t- Nothing -> fail "Invalid clause"- fc <- pfc- rhs <- pRHS syn n- let ctxt = tt_ctxt ist- let wsyn = syn { syn_namespace = [] }- (wheres, nmap) <- choice [do x <- pWhereblock n wsyn- popIndent- return x, - do pTerminator- return ([], [])]- return $ PClauseR fc wargs rhs wheres)-- <|> try (do pushIndent- n_in <- pfName; let n = expandNS syn n_in- cargs <- many (pConstraintArg syn)- iargs <- many (pImplicitArg (syn { inPattern = True } ))- fc <- pfc- args <- many (try (pImplicitArg (syn { inPattern = True } )) - <|> (fmap pexp (pArgExpr syn)))- wargs <- many (pWExpr syn)- let capp = PApp fc (PRef fc n) - (iargs ++ cargs ++ args)- ist <- getState- setState (ist { lastParse = Just n })- reserved "with"- wval <- pSimpleExpr syn- openBlock- ds <- many1 $ pFunDecl syn- let withs = map (fillLHSD n capp wargs) $ concat ds- closeBlock- popIndent- return $ PWith fc n capp wargs wval withs)-- <|> try (do wargs <- many1 (pWExpr syn)- fc <- pfc- reserved "with"- wval <- pSimpleExpr syn- openBlock- ds <- many1 $ pFunDecl syn- let withs = concat ds- closeBlock- return $ PWithR fc wargs wval withs)- - <|> do pushIndent- l <- pArgExpr syn- op <- operator- let n = expandNS syn (UN op)- r <- pArgExpr syn- fc <- pfc- wargs <- many (pWExpr syn)- rhs <- pRHS syn n- let wsyn = syn { syn_namespace = [] }- (wheres, nmap) <- choice [do x <- pWhereblock n wsyn- popIndent- return x, - do pTerminator- return ([], [])]- ist <- getState- let capp = PApp fc (PRef fc n) [pexp l, pexp r]- setState (ist { lastParse = Just n })- return $ PClause fc n capp wargs rhs wheres-- <|> do l <- pArgExpr syn- op <- operator- let n = expandNS syn (UN op)- r <- pArgExpr syn- fc <- pfc- wargs <- many (pWExpr syn)- reserved "with"- wval <- pSimpleExpr syn- openBlock - ds <- many1 $ pFunDecl syn- closeBlock- ist <- getState- let capp = PApp fc (PRef fc n) [pexp l, pexp r]- let withs = map (fillLHSD n capp wargs) $ concat ds- setState (ist { lastParse = Just n })- return $ PWith fc n capp wargs wval withs- where- 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 n c a (PClauses fc o fn cs) = PClauses fc o fn (map (fillLHS n c a) cs)- fillLHSD n c a x = x--pWExpr :: SyntaxInfo -> IParser PTerm-pWExpr syn = do lchar '|'- pExpr' syn--pWhereblock :: Name -> SyntaxInfo -> IParser ([PDecl], [(Name, Name)])-pWhereblock n syn - = do reserved "where"; openBlock- ds <- many1 $ pDecl syn- let dns = concatMap (concatMap declared) ds- closeBlock- return (concat ds, map (\x -> (x, decoration syn x)) dns)--pCodegen :: IParser Codegen-pCodegen = 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)--pDirective :: SyntaxInfo -> IParser [PDecl]-pDirective syn = try (do lchar '%'; reserved "lib"; cgn <- pCodegen; lib <- strlit;- return [PDirective (do addLib cgn lib- addIBC (IBCLib cgn lib))])- <|> try (do lchar '%'; reserved "link"; cgn <- pCodegen; obj <- strlit;- 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 <- pCodegen;- flag <- strlit- return [PDirective (do addIBC (IBCCGFlag cgn flag)- addFlag cgn flag)])- <|> try (do lchar '%'; reserved "include"; cgn <- pCodegen; hdr <- strlit;- 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 <- pAccessibility'- return [PDirective (do i <- getIState- putIState (i { default_access = acc }))])- <|> try (do lchar '%'; reserved "default"; tot <- pTotality- i <- getState- setState (i { default_total = tot } )- return [PDirective (do i <- getIState- putIState (i { default_total = tot }))])- <|> try (do lchar '%'; reserved "logging"; i <- natural;- return [PDirective (setLogLevel (fromInteger i))])- <|> try (do lchar '%'; reserved "dynamic"; libs <- sepBy1 strlit (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)])--pProvider :: SyntaxInfo -> IParser [PDecl]-pProvider syn = do lchar '%'; reserved "provide";- lchar '('; n <- pfName; t <- pTSig syn; lchar ')'- fc <- pfc- reserved "with"- e <- pExpr syn- return [PProvider syn fc n t e]--pTransform :: SyntaxInfo -> IParser [PDecl]-pTransform 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)- lhs <- pExpr syn- fc <- pfc- symbol "==>"- rhs <- pExpr syn- return [PTransform fc False lhs rhs]--pTactic :: SyntaxInfo -> IParser PTactic-pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')- return $ Intro ns- <|> do reserved "intros"; return Intros- <|> try (do reserved "refine"; n <- pName- imps <- many1 imp- return $ Refine n imps)- <|> do reserved "refine"; n <- pName- i <- getState- return $ Refine n []- <|> do reserved "mrefine"; n <- pName- i <- getState- return $ MatchRefine n- <|> do reserved "rewrite"; t <- pExpr syn;- i <- getState- return $ Rewrite (desugar syn i t)- <|> do reserved "equiv"; t <- pExpr syn;- i <- getState- return $ Equiv (desugar syn i t)- <|> try (do reserved "let"; n <- pName; lchar ':'; - ty <- pExpr' syn; lchar '='; t <- pExpr syn;- i <- getState- return $ LetTacTy n (desugar syn i ty) (desugar syn i t))- <|> try (do reserved "let"; n <- pName; lchar '=';- t <- pExpr syn;- i <- getState- return $ LetTac n (desugar syn i t))- <|> do reserved "focus"; n <- pName- return $ Focus n- <|> do reserved "exact"; t <- pExpr syn;- i <- getState- return $ Exact (desugar syn i t)- <|> do reserved "applyTactic"; t <- pExpr syn;- i <- getState- return $ ApplyTactic (desugar syn i t)- <|> do reserved "reflect"; t <- pExpr syn;- i <- getState- return $ Reflect (desugar syn i t)- <|> do reserved "fill"; t <- pExpr syn;- i <- getState- return $ Fill (desugar syn i t)- <|> do reserved "try"; t <- pTactic syn;- lchar '|';- t1 <- pTactic syn- return $ Try t t1- <|> do lchar '{'- t <- pTactic syn;- lchar ';';- t1 <- pTactic syn;- lchar '}'- return $ TSeq t t1- <|> 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- where- imp = do lchar '?'; return False- <|> do lchar '_'; return True+{-# 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)
src/Idris/Prover.hs view
@@ -16,6 +16,8 @@ import Idris.Completion import Idris.IdeSlave +import Text.Trifecta.Result(Result(..))+ import System.Console.Haskeline import System.Console.Haskeline.History import Control.Monad.State@@ -167,31 +169,31 @@ return (i, h) (cmd, step) <- case x of Nothing -> do iFail ""; fail "Abandoned"- Just input -> do return (parseTac i input, input)+ Just input -> do return (parseTactic i input, input) case cmd of- Right Abandon -> do iFail ""; fail "Abandoned"+ Success Abandon -> do iFail ""; fail "Abandoned" _ -> return () (d, st, done, prf') <- idrisCatch (case cmd of- Left err -> do iFail (show err)- return (False, e, False, prf)- Right Undo -> do (_, st) <- elabStep e loadState- iResult ""- return (True, st, False, init prf)- Right ProofState -> do iResult ""- return (True, e, False, prf)- Right ProofTerm -> do tm <- lifte e get_term- iResult $ "TT: " ++ show tm ++ "\n"- return (False, e, False, prf)- Right Qed -> do hs <- lifte e get_holes- when (not (null hs)) $ fail "Incomplete proof"- iResult "Proof completed!"- return (False, e, True, prf)- Right tac -> do (_, e) <- elabStep e saveState- (_, st) <- elabStep e (runTac True i tac)+ Failure err -> do iFail (show err)+ return (False, e, False, prf)+ Success Undo -> do (_, st) <- elabStep e loadState+ iResult ""+ return (True, st, False, init prf)+ Success ProofState -> do iResult ""+ return (True, e, False, prf)+ Success ProofTerm -> do tm <- lifte e get_term+ iResult $ "TT: " ++ show tm ++ "\n"+ return (False, e, False, prf)+ Success Qed -> do hs <- lifte e get_holes+ when (not (null hs)) $ fail "Incomplete proof"+ iResult "Proof completed!"+ return (False, e, True, prf)+ Success tac -> do (_, e) <- elabStep e saveState+ (_, st) <- elabStep e (runTac True i tac) -- trace (show (problems (proof st))) $- iResult ""- return (True, st, False, prf ++ [step]))+ iResult ""+ return (True, st, False, prf ++ [step])) (\err -> do iFail (show err) return (False, e, False, prf)) ideslavePutSExp "write-proof-state" (prf', length prf')
src/Idris/REPL.hs view
@@ -36,6 +36,8 @@ import IRTS.LParser import IRTS.CodegenCommon +import Text.Trifecta.Result(Result(..))+ -- import RTS.SC -- import RTS.Bytecode -- import RTS.PreC@@ -59,6 +61,7 @@ import Data.List import Data.Char import Data.Version+import Data.Word (Word) import Debug.Trace @@ -114,15 +117,15 @@ (f:_) -> f _ -> "" case parseCmd i "(input)" cmd of- Left err -> iFail $ show err- Right (Prove n') -> do iResult ""- idrisCatch- (do process fn (Prove n'))- (\e -> do iFail $ show e)- isetPrompt (mkPrompt mods)- Right cmd -> idrisCatch- (do ideslaveProcess fn cmd)- (\e -> do iFail $ show e)+ Failure err -> iFail $ show err+ Success (Prove n') -> do iResult ""+ idrisCatch+ (do process fn (Prove n'))+ (\e -> do iFail $ show e)+ isetPrompt (mkPrompt mods)+ Success cmd -> idrisCatch+ (do ideslaveProcess fn cmd)+ (\e -> do iFail $ show e) Just (REPLCompletions str) -> do (unused, compls) <- replCompletion (reverse str, "") let good = SexpList [SymbolAtom "ok", toSExp (map replacement compls, reverse unused)]@@ -215,31 +218,35 @@ (f:_) -> f _ -> "" case parseCmd i "(input)" cmd of- Left err -> do liftIO $ print err- return (Just inputs)- Right Reload -> - do putIState (orig { idris_options = idris_options i })+ Failure err -> do liftIO $ print err+ return (Just inputs)+ Success Reload ->+ do putIState $ orig { idris_options = idris_options i+ , idris_colourTheme = idris_colourTheme i+ } clearErr- mods <- loadInputs inputs + mods <- loadInputs inputs return (Just inputs)- Right (Load f) -> - do putIState (orig { idris_options = idris_options i })+ Success (Load f) ->+ do putIState orig { idris_options = idris_options i+ , idris_colourTheme = idris_colourTheme i+ } clearErr mod <- loadModule f return (Just [f])- Right (ModImport f) -> + Success (ModImport f) -> do clearErr fmod <- loadModule f return (Just (inputs ++ [fmod]))- Right Edit -> do edit fn orig- return (Just inputs)- Right Proofs -> do proofs orig+ Success Edit -> do edit fn orig return (Just inputs)- Right Quit -> do when (not quiet) (iputStrLn "Bye bye")- return Nothing- Right cmd -> do idrisCatch (process fn cmd)- (\e -> iputStrLn (show e))- return (Just inputs)+ Success Proofs -> do proofs orig+ return (Just inputs)+ Success Quit -> do when (not quiet) (iputStrLn "Bye bye")+ return Nothing+ Success cmd -> do idrisCatch (process fn cmd)+ (\e -> iputStrLn (show e))+ return (Just inputs) resolveProof :: Name -> Idris Name resolveProof n'@@ -834,12 +841,12 @@ execScript :: String -> Idris () execScript expr = do i <- getIState case parseExpr i expr of- Left err -> do iputStrLn $ show err- liftIO $ exitWith (ExitFailure 1)- Right term -> do ctxt <- getContext- (tm, _) <- elabVal toplevel False term- res <- execute tm- liftIO $ exitWith ExitSuccess+ Failure err -> do iputStrLn $ show err+ liftIO $ exitWith (ExitFailure 1)+ Success term -> do ctxt <- getContext+ (tm, _) <- elabVal toplevel False term+ res <- execute tm+ liftIO $ exitWith ExitSuccess -- | Get the platform-specific, user-specific Idris dir getIdrisUserDataDir :: Idris FilePath@@ -869,14 +876,14 @@ runInit h processLine i cmd input = case parseCmd i input cmd of- Left err -> liftIO $ print err- Right Reload -> iFail "Init scripts cannot reload the file"- Right (Load f) -> iFail "Init scripts cannot load files"- Right (ModImport f) -> iFail "Init scripts cannot import modules"- Right Edit -> iFail "Init scripts cannot invoke the editor"- Right Proofs -> proofs i- Right Quit -> iFail "Init scripts cannot quit Idris"- Right cmd -> process [] cmd+ Failure err -> liftIO $ print err+ Success Reload -> iFail "Init scripts cannot reload the file"+ Success (Load f) -> iFail "Init scripts cannot load files"+ Success (ModImport f) -> iFail "Init scripts cannot import modules"+ Success Edit -> iFail "Init scripts cannot invoke the editor"+ Success Proofs -> proofs i+ Success Quit -> iFail "Init scripts cannot quit Idris"+ Success cmd -> process [] cmd getFile :: Opt -> Maybe String getFile (Filename str) = Just str@@ -939,7 +946,7 @@ getCPU (TargetCPU x) = Just x getCPU _ = Nothing -getOptLevel :: Opt -> Maybe Int+getOptLevel :: Opt -> Maybe Word getOptLevel (OptLevel x) = Just x getOptLevel _ = Nothing
src/Idris/REPLParser.hs view
@@ -4,77 +4,81 @@ import System.Console.ANSI (Color(..)) import Idris.Colours-import Idris.Parser import Idris.AbsSyntax import Core.TT+import qualified Idris.Parser as P -import Text.ParserCombinators.Parsec-import Text.ParserCombinators.Parsec.Expr-import Text.ParserCombinators.Parsec.Language-import qualified Text.ParserCombinators.Parsec.Token as PTok+import Control.Applicative+import Control.Monad.State.Strict +import Text.Parser.Combinators+import Text.Parser.Char(anyChar)+import Text.Trifecta(Result, parseString)+import Text.Trifecta.Delta+ import Debug.Trace import Data.List import Data.List.Split(splitOn) import Data.Char(toLower)+import qualified Data.ByteString.UTF8 as UTF8 -parseCmd :: IState -> String -> String -> Either ParseError Command-parseCmd i inputname = runParser pCmd i inputname+parseCmd :: IState -> String -> String -> Result Command+parseCmd i inputname = parseString (evalStateT pCmd i) (Directed (UTF8.fromString inputname) 0 0 0 0) -cmd :: [String] -> IParser ()-cmd xs = do lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)+cmd :: [String] -> P.IdrisParser ()+cmd xs = do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs) where docmd [] = fail "No such command"- docmd (x:xs) = try (discard (symbol x)) <|> docmd xs+ docmd (x:xs) = try (discard (P.symbol x)) <|> docmd xs -pCmd :: IParser Command-pCmd = do spaces; try (do cmd ["q", "quit"]; eof; return Quit)+pCmd :: P.IdrisParser Command+pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit) <|> try (do cmd ["h", "?", "help"]; eof; return Help) <|> try (do cmd ["r", "reload"]; eof; return Reload)- <|> try (do cmd ["m", "module"]; f <- identifier; eof;+ <|> try (do cmd ["m", "module"]; f <- P.identifier; eof; return (ModImport (toPath f))) <|> try (do cmd ["e", "edit"]; eof; return Edit) <|> try (do cmd ["exec", "execute"]; eof; return Execute) <|> try (do cmd ["ttshell"]; eof; return TTShell)- <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile ViaC f))- <|> try (do cmd ["jc", "newcompile"]; f <- identifier; eof; return (Compile ViaJava f))- <|> try (do cmd ["js", "javascript"]; f <- identifier; eof; return (Compile ViaJavaScript f))+ <|> try (do cmd ["c", "compile"]; f <- P.identifier; eof; return (Compile ViaC f))+ <|> try (do cmd ["jc", "newcompile"]; f <- P.identifier; eof; return (Compile ViaJava f))+ <|> try (do cmd ["js", "javascript"]; f <- P.identifier; eof; return (Compile ViaJavaScript f)) <|> try (do cmd ["m", "metavars"]; eof; return Metavars) <|> try (do cmd ["proofs"]; eof; return Proofs)- <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))- <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- pName;+ <|> try (do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n))+ <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name; return (Just x)) eof; return (AddProof n))- <|> try (do cmd ["rmproof"]; n <- pName; eof; return (RmProof n))- <|> try (do cmd ["showproof"]; n <- pName; eof; return (ShowProof n))- <|> try (do cmd ["log"]; i <- natural; eof; return (LogLvl (fromIntegral i)))- <|> try (do cmd ["l", "load"]; f <- getInput; return (Load f))- <|> try (do cmd ["cd"]; f <- getInput; return (ChangeDirectory f))- <|> try (do cmd ["spec"]; whiteSpace; t <- pFullExpr defaultSyntax; return (Spec t))- <|> try (do cmd ["hnf"]; whiteSpace; t <- pFullExpr defaultSyntax; return (HNF t))- <|> try (do cmd ["doc"]; n <- pfName; eof; return (DocStr n))- <|> try (do cmd ["d", "def"]; many1 (char ' ') ; n <- pfName; eof; return (Defn n))- <|> try (do cmd ["total"]; do n <- pfName; eof; return (TotCheck n))- <|> try (do cmd ["t", "type"]; do whiteSpace; t <- pFullExpr defaultSyntax; return (Check t))+ <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))+ <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))+ <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))+ <|> try (do cmd ["l", "load"]; f <- many anyChar; return (Load f))+ <|> try (do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f))+ <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))+ <|> try (do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t))+ <|> try (do cmd ["doc"]; n <- P.fnName; eof; return (DocStr n))+ <|> try (do cmd ["d", "def"]; some (P.char ' ') ; n <- P.fnName; eof; return (Defn n))+ <|> try (do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n))+ <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t)) <|> try (do cmd ["u", "universes"]; eof; return Universes)- <|> try (do cmd ["di", "dbginfo"]; n <- pfName; eof; return (DebugInfo n))- <|> try (do cmd ["i", "info"]; n <- pfName; eof; return (Info n))- <|> try (do cmd ["miss", "missing"]; n <- pfName; eof; return (Missing n))+ <|> try (do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n))+ <|> try (do cmd ["i", "info"]; n <- P.fnName; eof; return (Info n))+ <|> try (do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n)) <|> try (do cmd ["dynamic"]; eof; return ListDynamic)- <|> try (do cmd ["dynamic"]; l <- getInput; return (DynamicLink l))+ <|> try (do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l)) <|> try (do cmd ["color", "colour"]; pSetColourCmd) <|> try (do cmd ["set"]; o <-pOption; return (SetOpt o)) <|> try (do cmd ["unset"]; o <-pOption; return (UnsetOpt o))- <|> try (do cmd ["s", "search"]; whiteSpace; t <- pFullExpr defaultSyntax; return (Search t))- <|> try (do cmd ["x"]; whiteSpace; t <- pFullExpr defaultSyntax; return (ExecVal t))- <|> try (do cmd ["patt"]; whiteSpace; t <- pFullExpr defaultSyntax; return (Pattelab t))- <|> do whiteSpace; do eof; return NOP- <|> do t <- pFullExpr defaultSyntax; return (Eval t)+ <|> try (do cmd ["s", "search"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Search t))+ <|> try (do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t))+ <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))+ <|> do P.whiteSpace; do eof; return NOP+ <|> do t <- P.fullExpr defaultSyntax; return (Eval t) where toPath n = foldl1' (</>) $ splitOn "." n -pOption :: IParser Opt-pOption = do discard (symbol "errorcontext"); return ErrContext- <|> do discard (symbol "showimplicits"); return ShowImpl+pOption :: P.IdrisParser Opt+pOption = do discard (P.symbol "errorcontext"); return ErrContext+ <|> do discard (P.symbol "showimplicits"); return ShowImpl colours :: [(String, Color)]@@ -88,18 +92,18 @@ , ("white", White) ] -pColour :: IParser Color+pColour :: P.IdrisParser Color pColour = doColour colours where doColour [] = fail "Unknown colour"- doColour ((s, c):cs) = (try (symbol s) >> return c) <|> doColour cs+ doColour ((s, c):cs) = (try (P.symbol s) >> return c) <|> doColour cs -pColourMod :: IParser (IdrisColour -> IdrisColour)-pColourMod = try (symbol "vivid" >> return doVivid)- <|> try (symbol "dull" >> return doDull)- <|> try (symbol "underline" >> return doUnderline)- <|> try (symbol "nounderline" >> return doNoUnderline)- <|> try (symbol "bold" >> return doBold)- <|> try (symbol "nobold" >> return doNoBold)+pColourMod :: P.IdrisParser (IdrisColour -> IdrisColour)+pColourMod = try (P.symbol "vivid" >> return doVivid)+ <|> try (P.symbol "dull" >> return doDull)+ <|> try (P.symbol "underline" >> return doUnderline)+ <|> try (P.symbol "nounderline" >> return doNoUnderline)+ <|> try (P.symbol "bold" >> return doBold)+ <|> try (P.symbol "nobold" >> return doNoBold) <|> try (pColour >>= return . doSetColour) where doVivid i = i { vivid = True } doDull i = i { vivid = False }@@ -114,17 +118,17 @@ colourTypes = map (\x -> ((map toLower . reverse . drop 6 . reverse . show) x, x)) $ enumFromTo minBound maxBound -pColourType :: IParser ColourType+pColourType :: P.IdrisParser ColourType pColourType = doColourType colourTypes where doColourType [] = fail $ "Unknown colour category. Options: " ++ (concat . intersperse ", " . map fst) colourTypes- doColourType ((s,ct):cts) = (try (symbol s) >> return ct) <|> doColourType cts+ doColourType ((s,ct):cts) = (try (P.symbol s) >> return ct) <|> doColourType cts -pSetColourCmd :: IParser Command+pSetColourCmd :: P.IdrisParser Command pSetColourCmd = (do c <- pColourType let defaultColour = IdrisColour Black True False False- opts <- sepBy pColourMod spaces+ opts <- sepBy pColourMod (P.whiteSpace) let colour = foldr ($) defaultColour $ reverse opts return $ SetColour c colour)- <|> try (symbol "on" >> return ColourOn)- <|> try (symbol "off" >> return ColourOff)+ <|> try (P.symbol "on" >> return ColourOn)+ <|> try (P.symbol "off" >> return ColourOff)
src/Main.hs view
@@ -80,7 +80,7 @@ "Usage: idris [input file] [options]\n" ++ "Options:\n" ++ "\t--quiet Quiet mode (for editors)\n" ++- "\t--[no]colour Control REPL colour highlighting" +++ "\t--[no]colour Control REPL colour highlighting\n" ++ "\t--check Type check only\n" ++ "\t-o [file] Specify output filename\n" ++ "\t-i [dir] Add directory to the list of import paths\n" ++
src/Util/LLVMStubs.hs view
@@ -11,6 +11,7 @@ import IRTS.Simplified import IRTS.CodegenCommon +import Data.Word (Word) getDefaultTargetTriple :: IO String getDefaultTargetTriple = return ""@@ -22,7 +23,7 @@ codegenLLVM :: [(TT.Name, SDecl)] -> String -> -- target triple String -> -- target CPU- Int -> -- Optimization degree+ Word -> -- Optimization degree FilePath -> -- output file name OutputType -> IO ()
test/reg003/expected view
@@ -2,6 +2,6 @@ No such variable OddList reg003a.idr:7:When elaborating constructor OCons: No such variable EvenList-reg003a.idr:10:When elaborating type of test:+reg003a.idr:9:When elaborating type of test: No such variable EvenList reg003a.idr:10:No type declaration for test
test/test002/expected view
@@ -1,1 +0,0 @@-test002.idr:5:Universe inconsistency
test/test002/test002.idr view
@@ -1,8 +1,9 @@ myid : a -> a myid x = x -idid : (a : Type) -> a -> a-idid = myid ![myid]+-- FIXME: Raw TT quotations currently unsupported in parser+--idid : (a : Type) -> a -> a+--idid = myid ![myid] app : (a -> b) -> a -> b app f x = f x
test/test020/expected view
@@ -1,5 +1,5 @@ When elaborating right hand side of foo:-test020a.idr:16:Can't unify+test020a.idr:14:Can't unify Vect n a with List a