idris 0.10.1 → 0.10.2
raw patch · 5 files changed
+62/−74 lines, 5 files
Files
- idris.cabal +1/−1
- main/Main.hs +41/−44
- src/Idris/AbsSyntax.hs +13/−24
- src/Idris/Elab/Clause.hs +1/−1
- src/Idris/Parser.hs +6/−4
idris.cabal view
@@ -1,5 +1,5 @@ Name: idris-Version: 0.10.1+Version: 0.10.2 License: BSD3 License-file: LICENSE Author: Edwin Brady
main/Main.hs view
@@ -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
src/Idris/AbsSyntax.hs view
@@ -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
src/Idris/Elab/Clause.hs view
@@ -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), _) <-
src/Idris/Parser.hs view
@@ -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