diff --git a/idris.cabal b/idris.cabal --- a/idris.cabal +++ b/idris.cabal @@ -1,5 +1,5 @@ Name: idris -Version: 0.10.1 +Version: 0.10.2 License: BSD3 License-file: LICENSE Author: Edwin Brady diff --git a/main/Main.hs b/main/Main.hs --- a/main/Main.hs +++ b/main/Main.hs @@ -4,12 +4,10 @@ import System.IO import System.Environment import System.Exit -import System.FilePath ((), addTrailingPathSeparator) import System.Directory import Data.Maybe import Data.Version -import Control.Monad.Trans.State.Strict ( execStateT, get, put ) import Control.Monad ( when ) import Idris.Core.TT @@ -44,66 +42,65 @@ runIdris :: [Opt] -> Idris () runIdris opts = do - runIO setupBundledCC - when (ShowLoggingCats `elem` opts) $ runIO showLoggingCats - when (ShowIncs `elem` opts) $ runIO showIncs - when (ShowLibs `elem` opts) $ runIO showLibs - when (ShowLibdir `elem` opts) $ runIO showLibdir - when (ShowPkgs `elem` opts) $ runIO showPkgs - case opt getClient opts of - [] -> return () - (c:_) -> do setVerbose False - setQuiet True - runIO $ runClient (getPort opts) c - runIO $ exitWith ExitSuccess - case opt getPkgCheck opts of - [] -> return () - fs -> do runIO $ mapM_ (checkPkg (WarnOnly `elem` opts) True) fs - runIO $ exitWith ExitSuccess - case opt getPkgClean opts of - [] -> return () - fs -> do runIO $ mapM_ cleanPkg fs - runIO $ exitWith ExitSuccess - case opt getPkgMkDoc opts of -- IdrisDoc - [] -> return () - fs -> do runIO $ mapM_ documentPkg fs - runIO $ exitWith ExitSuccess - case opt getPkgTest opts of - [] -> return () - fs -> do runIO $ mapM_ testPkg fs - runIO $ exitWith ExitSuccess - case opt getPkg opts of - [] -> case opt getPkgREPL opts of - [] -> idrisMain opts - [f] -> replPkg f - _ -> ifail "Too many packages" - fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs + runIO setupBundledCC + when (ShowLoggingCats `elem` opts) $ runIO showLoggingCats + when (ShowIncs `elem` opts) $ runIO showIncs + when (ShowLibs `elem` opts) $ runIO showLibs + when (ShowLibdir `elem` opts) $ runIO showLibdir + when (ShowPkgs `elem` opts) $ runIO showPkgs + case opt getClient opts of + [] -> return () + (c:_) -> do setVerbose False + setQuiet True + runIO $ runClient (getPort opts) c + runIO exitSuccess + case opt getPkgCheck opts of + [] -> return () + fs -> do runIO $ mapM_ (checkPkg (WarnOnly `elem` opts) True) fs + runIO exitSuccess + case opt getPkgClean opts of + [] -> return () + fs -> do runIO $ mapM_ cleanPkg fs + runIO exitSuccess + case opt getPkgMkDoc opts of -- IdrisDoc + [] -> return () + fs -> do runIO $ mapM_ documentPkg fs + runIO exitSuccess + case opt getPkgTest opts of + [] -> return () + fs -> do runIO $ mapM_ testPkg fs + runIO exitSuccess + case opt getPkg opts of + [] -> case opt getPkgREPL opts of + [] -> idrisMain opts + [f] -> replPkg f + _ -> ifail "Too many packages" + fs -> runIO $ mapM_ (buildPkg (WarnOnly `elem` opts)) fs showver :: IO b showver = do putStrLn $ "Idris version " ++ ver - exitWith ExitSuccess + exitSuccess showLibs :: IO b showLibs = do libFlags <- getLibFlags putStrLn $ unwords libFlags - exitWith ExitSuccess + exitSuccess showLibdir :: IO b -showLibdir = do dir <- getIdrisLibDir - putStrLn dir - exitWith ExitSuccess +showLibdir = do putStrLn =<< getIdrisLibDir + exitSuccess showIncs :: IO b showIncs = do incFlags <- getIncFlags putStrLn $ unwords incFlags - exitWith ExitSuccess + exitSuccess -- | List idris packages installed showPkgs :: IO b showPkgs = do mapM putStrLn =<< installedPackages - exitWith ExitSuccess + exitSuccess showLoggingCats :: IO b showLoggingCats = do putStrLn loggingCatsStr - exitWith ExitSuccess + exitSuccess diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -1702,9 +1702,9 @@ ai :: Bool -> Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm ai inpat qq env ds (PRef fc fcs f) | f `elem` infns = PInferRef fc fcs f - | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds [] [] + | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds [] ai inpat qq env ds (PHidden (PRef fc hl f)) - | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [] []) + | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds []) ai inpat qq env ds (PRewrite fc l r g) = let l' = ai inpat qq env ds l r' = ai inpat qq env ds r @@ -1733,9 +1733,8 @@ ai inpat qq env ds (PApp fc ftm@(PRef ffc hl f) as) | f `elem` infns = ai inpat qq env ds (PApp fc (PInferRef ffc hl f) as) | not (f `elem` map fst env) - = let as' = map (fmap (ai inpat qq env ds)) as - asdotted' = map (fmap (ai False qq env ds)) as in - handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as' asdotted' + = let as' = map (fmap (ai inpat qq env ds)) as in + handleErr $ aiFn topname inpat False qq imp_meths ist fc f ffc ds as' | Just (Just ty) <- lookup f env = let as' = map (fmap (ai inpat qq env ds)) as arity = getPArity ty in @@ -1808,9 +1807,8 @@ -> Name -- ^ function being applied -> FC -> [[T.Text]] -> [PArg] -- ^ initial arguments (if in a pattern) - -> [PArg] -- ^ initial arguments (if in an expression) -> Either Err PTerm -aiFn topname inpat True qq imp_meths ist fc f ffc ds [] _ +aiFn topname inpat True qq imp_meths ist fc f ffc ds [] | inpat && implicitable f && unqualified f = Right $ PPatvar ffc f | otherwise = case lookupDef f (tt_ctxt ist) of @@ -1820,7 +1818,7 @@ if (not (vname f) || tcname f || any (conCaf (tt_ctxt ist)) ialts) -- any constructor alts || any allImp ialts)) - then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] [] -- use it as a constructor + then aiFn topname inpat False qq imp_meths ist fc f ffc ds [] -- use it as a constructor else Right $ PPatvar ffc f where imp (PExp _ _ _ _) = False imp _ = True @@ -1838,9 +1836,9 @@ vname (UN n) = True -- non qualified vname _ = False -aiFn topname inpat expat qq imp_meths ist fc f ffc ds as asexp +aiFn topname inpat expat qq imp_meths ist fc f ffc ds as | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as -aiFn topname inpat expat qq imp_meths ist fc f ffc ds as asexp +aiFn topname inpat expat qq imp_meths ist fc f ffc ds as -- This is where namespaces get resolved by adding PAlternative = do let ns = lookupCtxtName f (idris_implicits ist) let nh = filter (\(n, _) -> notHidden n) ns @@ -1849,24 +1847,15 @@ x -> x case ns' of [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f')) - (insertImpl ns (chooseArgs f' as asexp)) + (insertImpl ns as) [] -> if f `elem` (map fst (idris_metavars ist)) then Right $ PApp fc (PRef ffc [ffc] f) as else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as alts -> Right $ PAlternative [] (ExactlyOne True) $ map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f')) - (insertImpl ns (chooseArgs f' as asexp))) alts + (insertImpl ns as)) alts where - -- choose whether to treat the arguments as patterns or expressions - -- if 'f' is a defined function, treat as expression, otherwise do the default. - -- This is so any names which later go under a PHidden are treated - -- as function names rather than bound pattern variables - chooseArgs f as asexp | isConName f (tt_ctxt ist) = as - | f == topname = as - | Nothing <- lookupDefExact f (tt_ctxt ist) = as - | otherwise = asexp - -- if the name is in imp_meths, we should actually refer to the bound -- name rather than the global one after expanding implicits isImpName f f' | f `elem` imp_meths = f @@ -1913,9 +1902,9 @@ case find n imps [] of Just (tm, imps') -> PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps' - Nothing -> let ph = if f `elem` imp_meths then PRef fc [] n else Placeholder in - PImp p True l n ph : - insImpAcc (M.insert n ph pnas) ps given imps + Nothing -> + PImp p True l n Placeholder : + insImpAcc (M.insert n Placeholder pnas) ps given imps insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps = let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in case find n imps [] of diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs --- a/src/Idris/Elab/Clause.hs +++ b/src/Idris/Elab/Clause.hs @@ -584,7 +584,7 @@ -- propagateParams i params fn_ty (addImplPat i lhs_in) logElab 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in)) logElab 5 ("LHS: " ++ show opts ++ "\n" ++ show fc ++ " " ++ showTmImpls lhs) - logElab 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++ + logElab 4 ("Fixed parameters: " ++ show params ++ " from " ++ showTmImpls lhs_in ++ "\n" ++ show (fn_ty, fn_is)) ((ElabResult lhs' dlhs [] ctxt' newDecls highlights, probs, inj), _) <- diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs --- a/src/Idris/Parser.hs +++ b/src/Idris/Parser.hs @@ -911,14 +911,16 @@ let initOpts = if default_total ist then [TotalFn] else [] + + (doc, argDocs) <- docstring syn opts <- fnOpts initOpts acc <- accessibility opts' <- fnOpts opts + + if kwopt then optional instanceKeyword + else do instanceKeyword + return (Just ()) - (doc, argDocs) - <- try (docstring syn <* if kwopt then optional instanceKeyword - else do instanceKeyword - return (Just ())) fc <- getFC en <- optional instanceName cs <- constraintList syn