08cef17 · Idris-dev · git.iko.soy

src/IRTS/CodegenC.hs+1−1

@@ -808,7 +808,7 @@ genDispatcher tags = "void* _idris_get_wrapper(VAL con)\n" ++

808808

809809genWrapper :: (FDesc, Int) -> String

810810genWrapper (desc, tag) | (toFType desc) == FFunctionIO =

811− error $ "Cannot create C callbacks for IO functions, wrap them with unsafePerformIO.\n"

811+ error "Cannot create C callbacks for IO functions, wrap them with unsafePerformIO.\n"

812812genWrapper (desc, tag) = ret ++ " " ++ wrapperName tag ++ "(" ++

813813 renderArgs argList ++")\n" ++

814814 "{\n" ++

src/IRTS/Compiler.hs+6−6

@@ -483,11 +483,11 @@ irTerm top vs env (Proj t (-1)) = do

483483 [t', LConst (BI 1)]

484484

485485irTerm top vs env (Proj t i) = LProj <$> irTerm top vs env t <*> pure i

486−irTerm top vs env (Constant TheWorld) = return $ LNothing

487−irTerm top vs env (Constant c) = return $ LConst c

488−irTerm top vs env (TType _) = return $ LNothing

489−irTerm top vs env Erased = return $ LNothing

490−irTerm top vs env Impossible = return $ LNothing

486+irTerm top vs env (Constant TheWorld) = return LNothing

487+irTerm top vs env (Constant c) = return (LConst c)

488+irTerm top vs env (TType _) = return LNothing

489+irTerm top vs env Erased = return LNothing

490+irTerm top vs env Impossible = return LNothing

491491

492492doForeign :: Vars -> [Name] -> [Term] -> Idris LExp

493493doForeign vs env (ret : fname : world : args)

@@ -500,7 +500,7 @@ doForeign vs env (ret : fname : world : args)

500500 = do let l' = toFDesc l

501501 r' <- irTerm (sMN 0 "__foreignCall") vs env r

502502 return (l', r')

503− splitArg _ = ifail $ "Badly formed foreign function call"

503+ splitArg _ = ifail "Badly formed foreign function call"

504504

505505 toFDesc (Constant (Str str)) = FStr str

506506 toFDesc tm

src/IRTS/JavaScript/AST.hs+1−1

@@ -99,7 +99,7 @@ ffi code args = let parsed = ffiParse code in

9999 where

100100 ffiParse :: String -> [FFI]

101101 ffiParse "" = []

102− ffiParse ['%'] = [FFIError $ "FFI - Invalid positional argument"]

102+ ffiParse ['%'] = [FFIError "FFI - Invalid positional argument"]

103103 ffiParse ('%':'%':ss) = FFICode '%' : ffiParse ss

104104 ffiParse ('%':s:ss)

105105 | isDigit s =

src/IRTS/Lang.hs+1−1

@@ -213,7 +213,7 @@ lift env (LForeign t s args) = do args' <- mapM (liftF env) args

213213lift env (LOp f args) = do args' <- mapM (lift env) args

214214 return (LOp f args')

215215lift env (LError str) = return $ LError str

216−lift env LNothing = return $ LNothing

216+lift env LNothing = return LNothing

217217

218218allocUnique :: LDefs -> (Name, LDecl) -> (Name, LDecl)

219219allocUnique defs p@(n, LConstructor _ _ _) = p

src/IRTS/Simplified.hs+1−1

@@ -214,7 +214,7 @@ scopecheck fn ctxt envTop tm = sc envTop tm where

214214 Just i -> do lvar i; return (Loc i)

215215 Nothing -> case lookupCtxtExact n ctxt of

216216 Just (DConstructor _ i ar) ->

217− failsc $ "can't pass constructor here"

217+ failsc "can't pass constructor here"

218218 Just _ -> return (Glob n)

219219 Nothing -> failsc $ "No such variable " ++ show n ++

220220 " in " ++ show tm ++ " " ++ show envTop

src/Idris/AbsSyntax.hs+5−5

@@ -583,7 +583,7 @@ getSO = do i <- getIState

583583

584584setSO :: Maybe String -> Idris ()

585585setSO s = do i <- getIState

586− putIState $ (i { compiled_so = s })

586+ putIState (i { compiled_so = s })

587587

588588getIState :: Idris IState

589589getIState = get

@@ -617,7 +617,7 @@ runIO x = liftIO (tryIOError x) >>= either (throwError . Msg . show) return

617617getName :: Idris Int

618618getName = do i <- getIState;

619619 let idx = idris_name i;

620− putIState $ (i { idris_name = idx + 1 })

620+ putIState (i { idris_name = idx + 1 })

621621 return idx

622622

623623-- | InternalApp keeps track of the real function application for

@@ -686,10 +686,10 @@ isUndefined fc n

686686 _ -> return True

687687

688688setContext :: Context -> Idris ()

689−setContext ctxt = do i <- getIState; putIState $ (i { tt_ctxt = ctxt } )

689+setContext ctxt = do i <- getIState; putIState (i { tt_ctxt = ctxt } )

690690

691691updateContext :: (Context -> Context) -> Idris ()

692−updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) } )

692+updateContext f = do i <- getIState; putIState (i { tt_ctxt = f (tt_ctxt i) } )

693693

694694addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()

695695addConstraints fc (v, cs)

@@ -1741,7 +1741,7 @@ implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

17411741 = case lookup n using of

17421742 Just ty -> PPi impl_gen

17431743 n NoFC ty (pibind using ns sc)

1744− Nothing -> PPi (impl_gen { pargopts = [InaccessibleArg] })

1744+ Nothing -> PPi (impl_gen { pargopts = [InaccessibleArg] })

17451745 n NoFC Placeholder (pibind using ns sc)

17461746

17471747-- | Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+1−1

@@ -1870,7 +1870,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

18701870 text "![" <> pretty r <> text "]"

18711871 prettySe d p bnd (PPatvar fc n) = pretty n

18721872 prettySe d p bnd e

1873− | Just str <- slist d p bnd e = depth d $ str

1873+ | Just str <- slist d p bnd e = depth d str

18741874 | Just n <- snat ppo d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))

18751875 prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n

18761876 prettySe d p bnd (PLam fc n nfc ty sc) =

src/Idris/Chaser.hs+2−2

@@ -143,8 +143,8 @@ buildTree built importlists fp = evalStateT (btree [] fp) []

143143 let file = extractFileName f

144144 lift $ logLvl 1 $ "CHASING " ++ show file ++ " (" ++ show fp ++ ")"

145145 ibcsd <- lift $ valIBCSubDir i

146− ids <- lift $ allImportDirs

147− fp <- lift $ findImport ids ibcsd file

146+ ids <- lift allImportDirs

147+ fp <- lift $ findImport ids ibcsd file

148148 lift $ logLvl 1 $ "Found " ++ show fp

149149 mt <- lift $ runIO $ getIModTime fp

150150 if (file `elem` built)

src/Idris/CmdOptions.hs+1−1

@@ -226,7 +226,7 @@ parseLogCats :: Monad m => String -> m [LogCat]

226226parseLogCats s =

227227 case lastMay (readP_to_S (doParse) s) of

228228 Just (xs, _) -> return xs

229− _ -> fail $ "Incorrect categories specified"

229+ _ -> fail "Incorrect categories specified"

230230 where

231231 doParse :: ReadP [LogCat]

232232 doParse = do

src/Idris/Completion.hs+2−2

@@ -148,7 +148,7 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lo

148148 completeArg (OptionalArg a) = completeArg a

149149 completeArg (SeqArgs a b) = completeArg a

150150 completeArg _ = noCompletion (prev, next)

151− completeCmdName = return $ ("", completeWith commands cmd)

151+ completeCmdName = return ("", completeWith commands cmd)

152152

153153-- | Complete REPL commands and defined identifiers

154154replCompletion :: CompletionFunc Idris

@@ -168,7 +168,7 @@ completePkg = completeWord Nothing " \t()" completeP

168168completeTactic :: [String] -> String -> CompletionFunc Idris

169169completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeArg $

170170 lookup tac tacticArgs

171− where completeTacName = return $ ("", completeWith tactics tac)

171+ where completeTacName = return ("", completeWith tactics tac)

172172 completeArg Nothing = noCompletion (prev, next)

173173 completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!

174174 completeArg (Just ExprTArg) = completeExpr as (prev, next)

src/Idris/Core/Elaborate.hs+3−2

@@ -654,8 +654,9 @@ apply' fillt fn imps =

654654 fillt (raw_apply fn (map (Var . snd) args))

655655 ulog <- getUnifyLog

656656 g <- goal

657− traceWhen ulog ("Goal " ++ show g ++ " -- when elaborating " ++ show fn) $

658− end_unify

657+ traceWhen ulog

658+ ("Goal " ++ show g ++ " -- when elaborating " ++ show fn)

659+ end_unify

659660 return $! (map (\(argName, argHole) -> (argName, updateUnify unify argHole)) args)

660661 where updateUnify us n = case lookup n us of

661662 Just (P _ t _) -> t

src/Idris/Core/Evaluate.hs+7−7

@@ -182,7 +182,7 @@ bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)

182182unbindEnv :: EnvTT n -> TT n -> TT n

183183unbindEnv [] tm = tm

184184unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

185−unbindEnv env tm = error $ "Impossible case occurred: couldn't unbind env."

185+unbindEnv env tm = error "Impossible case occurred: couldn't unbind env."

186186

187187usable :: Bool -- specialising

188188 -> Int -- Reduction depth limit (when simplifying/at REPL)

@@ -558,8 +558,8 @@ class Quote a where

558558 quote :: Int -> a -> Eval (TT Name)

559559

560560instance Quote Value where

561− quote i (VP nt n v) = liftM (P nt n) (quote i v)

562− quote i (VV x) = return $ V x

561+ quote i (VP nt n v) = liftM (P nt n) (quote i v)

562+ quote i (VV x) = return $ V x

563563 quote i (VBind _ n b sc) = do sc' <- sc (VTmp i)

564564 b' <- quoteB b

565565 liftM (Bind n b') (quote (i+1) sc')

@@ -571,10 +571,10 @@ instance Quote Value where

571571 let sc'' = pToV (sMN vd "vlet") (addBinder sc')

572572 return (Bind n (Let t' v') sc'')

573573 quote i (VApp f a) = liftM2 (App MaybeHoles) (quote i f) (quote i a)

574− quote i (VType u) = return $ TType u

575− quote i (VUType u) = return $ UType u

576− quote i VErased = return $ Erased

577− quote i VImpossible = return $ Impossible

574+ quote i (VType u) = return (TType u)

575+ quote i (VUType u) = return (UType u)

576+ quote i VErased = return Erased

577+ quote i VImpossible = return Impossible

578578 quote i (VProj v j) = do v' <- quote i v

579579 return (Proj v' j)

580580 quote i (VConstant c) = return $ Constant c

src/Idris/Core/ProofState.hs+5−5

@@ -765,8 +765,8 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

765765 case lookupTy (SN (tacn tnm)) ctxt of

766766 [elimTy] -> do

767767 param_pos <- case lookupMetaInformation tnm ctxt of

768− [DataMI param_pos] -> return param_pos

769− m | length tyargs > 0 -> fail $ "Invalid meta information for " ++ show tnm ++ " where the metainformation is " ++ show m ++ " and definition is" ++ show (lookupDef tnm ctxt)

768+ [DataMI param_pos] -> return param_pos

769+ m | not (null tyargs) -> fail $ "Invalid meta information for " ++ show tnm ++ " where the metainformation is " ++ show m ++ " and definition is" ++ show (lookupDef tnm ctxt)

770770 _ -> return []

771771 let (params, indicies) = splitTyArgs param_pos tyargs

772772 let args = getArgTys elimTy

@@ -774,8 +774,8 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

774774 let args' = drop (length params) args

775775 let propTy = head args'

776776 let restargs = init $ tail args'

777− let consargs = take (length restargs - length indicies) $ restargs

778− let indxargs = drop (length restargs - length indicies) $ restargs

777+ let consargs = take (length restargs - length indicies) restargs

778+ let indxargs = drop (length restargs - length indicies) restargs

779779 let scr = last $ tail args'

780780 let indxnames = makeIndexNames indicies

781781 currentNames <- query $ allTTNames . getProofTerm . pterm

@@ -790,7 +790,7 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

790790 action (\ps -> ps {holes = holes ps \\ [x],

791791 recents = x : recents ps })

792792 mapM_ addConsHole (reverse consargs')

793− let res' = forget $ res

793+ let res' = forget res

794794 (scv, sct) <- lift $ check ctxt env res'

795795 let (scv', _) = specialise ctxt env [] scv

796796 return scv'

src/Idris/Coverage.hs+1−2

@@ -758,8 +758,7 @@ type MultiPath = [SCGEntry]

758758

759759mkMultiPaths :: IState -> MultiPath -> [SCGEntry] -> [MultiPath]

760760mkMultiPaths ist path [] = [reverse path]

761−mkMultiPaths ist path cg

762− = concat (map extend cg)

761+mkMultiPaths ist path cg = concatMap extend cg

763762 where extend (nextf, args)

764763 | (nextf, args) `elem` path = [ reverse ((nextf, args) : path) ]

765764 | [Unchecked] <- lookupTotal nextf (tt_ctxt ist)

src/Idris/Directives.hs+2−2

@@ -54,7 +54,7 @@ directiveAction (DThaw n') = do

5454 ctxt <- getContext

5555 case lookupDefAccExact n False ctxt of

5656 Just (_, Frozen) -> do setAccessibility n Public

57− addIBC (IBCAccess n Public)

57+ addIBC (IBCAccess n Public)

5858 _ -> throwError (Msg (show n ++ " is not frozen"))) ns

5959directiveAction (DInjective n') = do

6060 ns <- allNamespaces n'

@@ -77,7 +77,7 @@ directiveAction (DDynamicLibs libs) = do

7777 added <- addDyLib libs

7878 case added of

7979 Left lib -> addIBC (IBCDyLib (lib_name lib))

80− Right msg -> fail $ msg

80+ Right msg -> fail msg

8181

8282directiveAction (DNameHint ty tyFC ns) = do

8383 ty' <- disambiguate ty

src/Idris/Elab/Class.hs+3−3

@@ -138,7 +138,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

138138 (map fst (filter (\(_, (inj, _, _, _, _)) -> inj) imethods))

139139

140140 -- add the default definitions

141− mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))

141+ mapM_ (rec_elabDecl info EAll info) (concatMap (snd.snd) defs)

142142 addIBC (IBCClass tn)

143143

144144 sendHighlighting $

@@ -164,12 +164,12 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

164164 checkDefaultSuperclassInstance :: PDecl -> Idris ()

165165 checkDefaultSuperclassInstance (PInstance _ _ _ fc cs _ _ _ n _ ps _ _ _ _)

166166 = do when (not $ null cs) . tclift

167− $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

167+ $ tfail (At fc (Msg "Default superclass instances can't have constraints."))

168168 i <- getIState

169169 let t = PApp fc (PRef fc [] n) (map pexp ps)

170170 let isConstrained = any (== t) (map snd constraints)

171171 when (not isConstrained) . tclift

172− $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))

172+ $ tfail (At fc (Msg "Default instances must be for a superclass constraint on the containing class."))

173173 return ()

174174

175175 checkConstraintName :: [Name] -> Name -> Idris ()

src/Idris/Elab/Clause.hs+8−8

@@ -421,7 +421,7 @@ elabPE info fc caller r =

421421 PClause fc newnm lhs' [] rhs [])

422422 (pe_clauses specdecl)

423423 trans <- elabTransform info fc False rhs lhs

424− elabClauses (info {pe_depth = pe_depth info + 1}) fc

424+ elabClauses (info {pe_depth = pe_depth info + 1}) fc

425425 (PEGenerated:opts) newnm def

426426 return [trans]

427427 else return [])

@@ -555,8 +555,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

555555

556556 -- Check if we have "with" patterns outside of "with" block

557557 when (isOutsideWith lhs_in && (not $ null withs)) $

558− ierror $ (At fc (Elaborating "left hand side of " fname Nothing

559− (Msg "unexpected patterns outside of \"with\" block")))

558+ ierror (At fc (Elaborating "left hand side of " fname Nothing

559+ (Msg "unexpected patterns outside of \"with\" block")))

560560

561561 -- get the parameters first, to pass through to any where block

562562 let fn_ty = case lookupTy fname ctxt of

@@ -713,7 +713,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

713713 mapM_ (elabCaseBlock winfo opts) is

714714

715715 ctxt <- getContext

716− logElab 5 $ "Rechecking"

716+ logElab 5 "Rechecking"

717717 logElab 6 $ " ==> " ++ show (forget rhs')

718718

719719 (crhs, crhsty) -- if there's holes && deferred things, it's okay

@@ -760,7 +760,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

760760 addIBC (IBCErrRev (crhs, clhs))

761761 addErrRev (crhs, clhs)

762762 pop_estack

763− return $ (Right (clhs, crhs), lhs)

763+ return (Right (clhs, crhs), lhs)

764764 where

765765 pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo

766766 pinfo info ns ds i

@@ -903,7 +903,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

903903 Just (n, nfc) -> Just (uniqueName n (map fst bargs))

904904

905905 -- Highlight explicit proofs

906− sendHighlighting $ [(fc, AnnBoundName n False) | (n, fc) <- maybeToList pn_in]

906+ sendHighlighting [(fc, AnnBoundName n False) | (n, fc) <- maybeToList pn_in]

907907

908908 logElab 10 ("With type " ++ show (getRetTy cwvaltyN) ++

909909 " depends on " ++ show pdeps ++ " from " ++ show pvars)

@@ -991,7 +991,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

991991 mapM_ (elabCaseBlock info opts) is

992992 logElab 5 ("Checked RHS " ++ show rhs')

993993 (crhs, crhsty) <- recheckC (constraintNS info) fc id [] rhs'

994− return $ (Right (clhs, crhs), lhs)

994+ return (Right (clhs, crhs), lhs)

995995 where

996996 getImps (Bind n (Pi _ _ _) t) = pexp Placeholder : getImps t

997997 getImps _ = []

@@ -999,7 +999,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

999999 mkAuxC pn wname lhs ns ns' (PClauses fc o n cs)

10001000 = do cs' <- mapM (mkAux pn wname lhs ns ns') cs

10011001 return $ PClauses fc o wname cs'

1002− mkAuxC pn wname lhs ns ns' d = return $ d

1002+ mkAuxC pn wname lhs ns ns' d = return d

10031003

10041004 mkAux pn wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)

10051005 = do i <- getIState

src/Idris/Elab/Data.hs+4−4

@@ -258,11 +258,11 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

258258 checkUniqueKind (UType AllTypes) _

259259 = tclift $ tfail (At fc (UniqueKindError AllTypes n))

260260 checkUniqueKind _ _ = return ()

261−

261+

262262addParamConstraints :: FC -> [Int] -> Type -> [(Name, Type)] -> Idris ()

263263addParamConstraints fc ps cty cons

264264 = case getRetTy cty of

265− TType cvar -> mapM_ (addConConstraint ps cvar)

265+ TType cvar -> mapM_ (addConConstraint ps cvar)

266266 (map getParamNames cons)

267267 _ -> return ()

268268 where

@@ -277,7 +277,7 @@ addParamConstraints fc ps cty cons

277277 paramArgs i (_ : args) = paramArgs (i + 1) args

278278 paramArgs i [] = []

279279

280− addConConstraint ps cvar (ty, pnames) = constraintTy ty

280+ addConConstraint ps cvar (ty, pnames) = constraintTy ty

281281 where

282282 constraintTy (Bind n (Pi _ ty _) sc)

283283 = case getRetTy ty of

@@ -305,7 +305,7 @@ elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->

305305 [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name])] ->

306306 ElabInfo -> EliminatorState ()

307307elabCaseFun ind paramPos n ty cons info = do

308− elimLog $ "Elaborating case function"

308+ elimLog "Elaborating case function"

309309 put (Map.fromList $ zip (concatMap (\(_, p, _, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))

310310 let (cnstrs, _) = splitPi ty

311311 let (splittedTy@(pms, idxs)) = splitPms cnstrs

src/Idris/Elab/Instance.hs+1−1

@@ -147,7 +147,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

147147 logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (class_methods ci)))

148148 let ds_defs = insertDefaults ist iname (class_defaults ci) ns ds

149149 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")

150− let ds' = reorderDefs (map fst (class_methods ci)) $ ds_defs

150+ let ds' = reorderDefs (map fst (class_methods ci)) ds_defs

151151 logElab 1 ("Reordered: " ++ show ds' ++ "\n")

152152

153153 mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))

src/Idris/Elab/Type.hs+3−3

@@ -104,8 +104,8 @@ buildType info syn fc opts n ty' = do

104104

105105 mapM_ (elabCaseBlock info opts) is

106106 ctxt <- getContext

107− logElab 5 $ "Rechecking"

108− logElab 6 $ show tyT

107+ logElab 5 "Rechecking"

108+ logElab 6 (show tyT)

109109 logElab 10 $ "Elaborated to " ++ showEnvDbg [] tyT

110110 (cty, ckind) <- recheckC (constraintNS info) fc id [] tyT

111111

@@ -224,7 +224,7 @@ elabType' norm info syn doc argDocs fc opts n nfc ty' = {- let ty' = piBind (par

224224 case fam of

225225 P _ tyn _ -> do addAutoHint tyn n

226226 addIBC (IBCAutoHint tyn n)

227− t -> ifail $ "Hints must return a data or record type"

227+ t -> ifail "Hints must return a data or record type"

228228

229229 -- If the function is declared as an error handler and the language

230230 -- extension is enabled, then add it to the list of error handlers.

src/Idris/IBC.hs+1−1

@@ -150,7 +150,7 @@ loadIBC reexport phase fp

150150

151151-- | Load an entire package from its index file

152152loadPkgIndex :: String -> Idris ()

153−loadPkgIndex pkg = do ddir <- runIO $ getIdrisLibDir

153+loadPkgIndex pkg = do ddir <- runIO getIdrisLibDir

154154 addImportDir (ddir </> pkg)

155155 fp <- findPkgIndex pkg

156156 loadIBC True IBC_Building fp

src/Idris/IdeMode.hs+12−12

@@ -258,18 +258,18 @@ data IdeModeCommand = REPLCompletions String

258258 | GetIdrisVersion

259259

260260sexpToCommand :: SExp -> Maybe IdeModeCommand

261−sexpToCommand (SexpList (x:[])) = sexpToCommand x

262−sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)

263−sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)

264−sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename, IntegerAtom line]) = Just (LoadFile filename (Just (fromInteger line)))

265−sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename Nothing)

266−sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)

267−sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)

268−sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)

269−sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)

270−sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)

271−sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)

272−sexpToCommand (SexpList [SymbolAtom "make-case", IntegerAtom line, StringAtom name]) = Just (MakeCaseBlock (fromInteger line) name)

261+sexpToCommand (SexpList ([x])) = sexpToCommand x

262+sexpToCommand (SexpList [SymbolAtom "interpret", StringAtom cmd]) = Just (Interpret cmd)

263+sexpToCommand (SexpList [SymbolAtom "repl-completions", StringAtom prefix]) = Just (REPLCompletions prefix)

264+sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename, IntegerAtom line]) = Just (LoadFile filename (Just (fromInteger line)))

265+sexpToCommand (SexpList [SymbolAtom "load-file", StringAtom filename]) = Just (LoadFile filename Nothing)

266+sexpToCommand (SexpList [SymbolAtom "type-of", StringAtom name]) = Just (TypeOf name)

267+sexpToCommand (SexpList [SymbolAtom "case-split", IntegerAtom line, StringAtom name]) = Just (CaseSplit (fromInteger line) name)

268+sexpToCommand (SexpList [SymbolAtom "add-clause", IntegerAtom line, StringAtom name]) = Just (AddClause (fromInteger line) name)

269+sexpToCommand (SexpList [SymbolAtom "add-proof-clause", IntegerAtom line, StringAtom name]) = Just (AddProofClause (fromInteger line) name)

270+sexpToCommand (SexpList [SymbolAtom "add-missing", IntegerAtom line, StringAtom name]) = Just (AddMissing (fromInteger line) name)

271+sexpToCommand (SexpList [SymbolAtom "make-with", IntegerAtom line, StringAtom name]) = Just (MakeWithBlock (fromInteger line) name)

272+sexpToCommand (SexpList [SymbolAtom "make-case", IntegerAtom line, StringAtom name]) = Just (MakeCaseBlock (fromInteger line) name)

273273-- The Boolean in ProofSearch means "search recursively"

274274-- If it's False, that means "refine", i.e. apply the name and fill in any

275275-- arguments which can be done by unification.

src/Idris/IdrisDoc.hs+2−2

@@ -423,7 +423,7 @@ createIndex :: S.Set NsName -- ^ Set of namespace names to

423423createIndex nss out =

424424 do (path, h) <- openTempFile out "index.html"

425425 BS2.hPut h $ renderHtml $ wrapper Nothing $ do

426− H.h1 $ "Namespaces"

426+ H.h1 "Namespaces"

427427 H.ul ! class_ "names" $ do

428428 let path ns = "docs" ++ "/" ++ genRelNsPath ns "html"

429429 item ns = do let n = toHtml $ nsName2Str ns

@@ -523,7 +523,7 @@ genTypeHeader ist (FD n _ args ftype _) = do

523523 docExtractor (_, _, _, Nothing) = Nothing

524524 docExtractor (n, _, _, Just d) = Just (n, doc2Str d)

525525 -- TODO: Remove <p> tags more robustly

526− doc2Str d = let dirty = renderMarkup $ contents $ Docstrings.renderHtml $ d

526+ doc2Str d = let dirty = renderMarkup $ contents $ Docstrings.renderHtml d

527527 in take (length dirty - 8) $ drop 3 dirty

528528

529529 name (NS n ns) = show (NS (sUN $ name n) ns)

src/Idris/Interactive.hs+3−3

@@ -380,7 +380,7 @@ makeLemma fn updatefile l n

380380 runIO $ writeSource fb (addProv before tyline lem_app later)

381381 runIO $ copyFile fb fn

382382 else case idris_outputmode i of

383− RawOutput _ -> iPrintResult $ lem_app

383+ RawOutput _ -> iPrintResult lem_app

384384 IdeMode n h ->

385385 let good = SexpList [SymbolAtom "ok",

386386 SexpList [SymbolAtom "provisional-definition-lemma",

@@ -495,7 +495,7 @@ makeLemma fn updatefile l n

495495 addLem before tyline lem lem_app later

496496 = let (bef_end, blankline : bef_start)

497497 = case span (not . blank) (reverse before) of

498− (bef, []) -> (bef, "" : [])

498+ (bef, []) -> (bef, [""])

499499 x -> x

500500 mvline = updateMeta tyline (show n) lem_app in

501501 unlines $ reverse bef_start ++

@@ -505,7 +505,7 @@ makeLemma fn updatefile l n

505505 addProv before tyline lem_app later

506506 = let (later_bef, blankline : later_end)

507507 = case span (not . blank) later of

508− (bef, []) -> (bef, "" : [])

508+ (bef, []) -> (bef, [""])

509509 x -> x in

510510 unlines $ before ++ tyline :

511511 (later_bef ++ [blankline, lem_app, blankline] ++

src/Idris/Parser/Data.hs+1−1

@@ -232,7 +232,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

232232 let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

233233 let n = show tyn_in ++ " "

234234 let s = kw ++ n

235− let as = concat (intersperse " " $ map show args) ++ " "

235+ let as = unwords (map show args) ++ " "

236236 let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)

237237 let ss = concat (intersperse " -> " $ map (const "Type") args)

238238 let fix1 = s ++ as ++ " = ..."

src/Idris/Parser/Expr.hs+1−1

@@ -499,7 +499,7 @@ bracketed' open syn =

499499{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}

500500dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm

501501dependentPair pun prev openFC syn =

502− if prev == [] then

502+ if null prev then

503503 nametypePart <|> namePart

504504 else

505505 case pun of

src/Idris/ProofSearch.hs+2−2

@@ -364,7 +364,7 @@ resolveTC def openOK depth top fn elab ist

364364 = do hs <- get_holes

365365 resTC' [] def openOK hs depth top fn elab ist

366366

367−resTC' tcs def openOK topholes 0 topg fn elab ist = fail $ "Can't resolve interface"

367+resTC' tcs def openOK topholes 0 topg fn elab ist = fail "Can't resolve interface"

368368resTC' tcs def openOK topholes 1 topg fn elab ist = try' (trivial elab ist) (resolveTC def False 0 topg fn elab ist) True

369369resTC' tcs defaultOn openOK topholes depth topg fn elab ist

370370 = do compute

@@ -484,7 +484,7 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

484484 solven n = replicateM_ n solve

485485

486486 resolve n depth

487− | depth == 0 = fail $ "Can't resolve interface"

487+ | depth == 0 = fail "Can't resolve interface"

488488 | otherwise

489489 = do lams <- introImps

490490 t <- goal

src/Idris/REPL.hs+11−11

@@ -782,7 +782,7 @@ edit :: FilePath -> IState -> Idris ()

782782edit "" orig = iputStrLn "Nothing to edit"

783783edit f orig

784784 = do i <- getIState

785− env <- runIO $ getEnvironment

785+ env <- runIO getEnvironment

786786 let editor = getEditor env

787787 let line = case errSpan i of

788788 Just l -> ['+' : show (fst (fc_start l))]

@@ -915,7 +915,7 @@ process fn (NewDefn decls) = do

915915 fixClauses (PInstance doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty instName decls) =

916916 PInstance doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty instName (map fixClauses decls)

917917 fixClauses decl = decl

918−

918+

919919 info = recinfo (fileFC "toplevel")

920920

921921process fn (Undefine names) = undefine names

@@ -1205,8 +1205,8 @@ process fn (Prove mode n')

12051205 n <- case metavars of

12061206 [] -> ierror (Msg $ "Cannot find metavariable " ++ show n')

12071207 [(n, (_,_,_,False,_))] -> return n

1208− [(_, (_,_,_,_,False))] -> ierror (Msg $ "Can't prove this hole as it depends on other holes")

1209− [(_, (_,_,_,True,_))] -> ierror (Msg $ "Declarations not solvable using prover")

1208+ [(_, (_,_,_,_,False))] -> ierror (Msg "Can't prove this hole as it depends on other holes")

1209+ [(_, (_,_,_,True,_))] -> ierror (Msg "Declarations not solvable using prover")

12101210 ns -> ierror (CantResolveAlts (map fst ns))

12111211 prover (toplevelWith fn) mode (lit fn) n

12121212 -- recheck totality

@@ -1280,7 +1280,7 @@ process fn (Missing n)

12801280 []

12811281 (idris_infixes i))

12821282 tms))

1283− _ -> iPrintError $ "Ambiguous name"

1283+ _ -> iPrintError "Ambiguous name"

12841284process fn (DynamicLink l)

12851285 = do i <- getIState

12861286 let importdirs = opt_importdirs (idris_options i)

@@ -1404,7 +1404,7 @@ process fn (MakeDoc s) =

14041404 parse n | Success x <- runparser (fmap fst name) istate fn n = Right x

14051405 parse n = Left n

14061406 (bad, nss) = partitionEithers $ map parse names

1407− cd <- runIO $ getCurrentDirectory

1407+ cd <- runIO getCurrentDirectory

14081408 let outputDir = cd </> "doc"

14091409 result <- if null bad then runIO $ generateDocs istate nss outputDir

14101410 else return . Left $ "Illegal name: " ++ head bad

@@ -1588,7 +1588,7 @@ loadInputs inputs toline -- furthest line to read in input source files

15881588 case errSpan inew of

15891589 Nothing ->

15901590 do putIState $!! ist { idris_tyinfodata = tidata }

1591− ibcfiles <- mapM findNewIBC (nub (concat (map snd ifiles)))

1591+ ibcfiles <- mapM findNewIBC (nub (concatMap snd ifiles))

15921592-- logLvl 0 $ "Loading from " ++ show ibcfiles

15931593 tryLoad True (IBC_REPL True) (mapMaybe id ibcfiles)

15941594 _ -> return ()

@@ -1717,7 +1717,7 @@ idrisMain opts =

17171717

17181718 when (DefaultTotal `elem` opts) $ do i <- getIState

17191719 putIState (i { default_total = DefaultCheckingTotal })

1720− tty <- runIO $ isATTY

1720+ tty <- runIO isATTY

17211721 setColourise $ not quiet && last (tty : opt getColour opts)

17221722

17231723

@@ -1791,7 +1791,7 @@ idrisMain opts =

17911791 runIO $ exitWith (ExitFailure 1)

17921792 Success e -> process "" (Eval e))

17931793 exprs

1794− runIO $ exitWith ExitSuccess

1794+ runIO exitSuccess

17951795

17961796

17971797 case script of

@@ -1829,7 +1829,7 @@ idrisMain opts =

18291829 makeOption _ = return ()

18301830

18311831 addPkgDir :: String -> Idris ()

1832− addPkgDir p = do ddir <- runIO $ getIdrisLibDir

1832+ addPkgDir p = do ddir <- runIO getIdrisLibDir

18331833 addImportDir (ddir </> p)

18341834 addIBC (IBCImportDir (ddir </> p))

18351835

@@ -1848,7 +1848,7 @@ execScript expr = do i <- getIState

18481848 Success term -> do ctxt <- getContext

18491849 (tm, _) <- elabVal (recinfo (fileFC "toplevel")) ERHS term

18501850 res <- execute tm

1851− runIO $ exitWith ExitSuccess

1851+ runIO $ exitSuccess

18521852

18531853-- | Get the platform-specific, user-specific Idris dir

18541854getIdrisUserDataDir :: Idris FilePath

src/Idris/Reflection.hs+40−31

@@ -173,9 +173,9 @@ reifyTT :: Term -> ElabD Term

173173reifyTT t@(App _ _ _)

174174 | (P _ f _, args) <- unApply t = reifyTTApp f args

175175reifyTT t@(P _ n _)

176− | n == reflm "Erased" = return $ Erased

176+ | n == reflm "Erased" = return Erased

177177reifyTT t@(P _ n _)

178− | n == reflm "Impossible" = return $ Impossible

178+ | n == reflm "Impossible" = return Impossible

179179reifyTT t = fail ("Unknown reflection term: " ++ show t)

180180

181181reifyTTApp :: Name -> [Term] -> ElabD Term

@@ -217,7 +217,7 @@ reifyRaw :: Term -> ElabD Raw

217217reifyRaw t@(App _ _ _)

218218 | (P _ f _, args) <- unApply t = reifyRawApp f args

219219reifyRaw t@(P _ n _)

220− | n == reflm "RType" = return $ RType

220+ | n == reflm "RType" = return RType

221221reifyRaw t = fail ("Unknown reflection raw term in reifyRaw: " ++ show t)

222222

223223reifyRawApp :: Name -> [Term] -> ElabD Raw

@@ -332,9 +332,9 @@ reifyTTBinderApp reif f [t]

332332reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))

333333

334334reifyTTConst :: Term -> ElabD Const

335−reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType

336−reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType

337−reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot

335+reifyTTConst (P _ n _) | n == reflm "StrType" = return StrType

336+reifyTTConst (P _ n _) | n == reflm "VoidType" = return VoidType

337+reifyTTConst (P _ n _) | n == reflm "Forgot" = return Forgot

338338reifyTTConst t@(App _ _ _)

339339 | (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg

340340reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)

@@ -343,23 +343,23 @@ reifyTTConstApp :: Name -> Term -> ElabD Const

343343reifyTTConstApp f aty

344344 | f == reflm "AType" = fmap AType (reifyArithTy aty)

345345reifyTTConstApp f (Constant c@(I _))

346− | f == reflm "I" = return $ c

346+ | f == reflm "I" = return c

347347reifyTTConstApp f (Constant c@(BI _))

348− | f == reflm "BI" = return $ c

348+ | f == reflm "BI" = return c

349349reifyTTConstApp f (Constant c@(Fl _))

350− | f == reflm "Fl" = return $ c

350+ | f == reflm "Fl" = return c

351351reifyTTConstApp f (Constant c@(Ch _))

352− | f == reflm "Ch" = return $ c

352+ | f == reflm "Ch" = return c

353353reifyTTConstApp f (Constant c@(Str _))

354− | f == reflm "Str" = return $ c

354+ | f == reflm "Str" = return c

355355reifyTTConstApp f (Constant c@(B8 _))

356− | f == reflm "B8" = return $ c

356+ | f == reflm "B8" = return c

357357reifyTTConstApp f (Constant c@(B16 _))

358− | f == reflm "B16" = return $ c

358+ | f == reflm "B16" = return c

359359reifyTTConstApp f (Constant c@(B32 _))

360− | f == reflm "B32" = return $ c

360+ | f == reflm "B32" = return c

361361reifyTTConstApp f (Constant c@(B64 _))

362− | f == reflm "B64" = return $ c

362+ | f == reflm "B64" = return c

363363reifyTTConstApp f v@(P _ _ _) =

364364 lift . tfail . Msg $

365365 "Can't reify the variable " ++

@@ -389,9 +389,9 @@ reifyIntTy tm = fail $ "The term " ++ show tm ++ " is not a reflected IntTy"

389389reifyTTUExp :: Term -> ElabD UExp

390390reifyTTUExp t@(App _ _ _)

391391 = case unApply t of

392− (P _ f _, [Constant (Str str), Constant (I i)])

392+ (P _ f _, [Constant (Str str), Constant (I i)])

393393 | f == reflm "UVar" -> return $ UVar str i

394− (P _ f _, [Constant (I i)])

394+ (P _ f _, [Constant (I i)])

395395 | f == reflm "UVal" -> return $ UVal i

396396 _ -> fail ("Unknown reflection type universe expression: " ++ show t)

397397reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)

@@ -487,7 +487,7 @@ reflectTTQuotePattern unq (Proj t i)

487487reflectTTQuotePattern unq Erased

488488 = do erased <- claimTy (sMN 0 "erased") (Var (reflm "TT"))

489489 movelast erased

490− fill $ (Var erased)

490+ fill (Var erased)

491491reflectTTQuotePattern unq Impossible

492492 = lift . tfail . InternalMsg $

493493 "Phase error! The Impossible constructor is for optimization only and should not have been reflected during elaboration."

@@ -1190,14 +1190,17 @@ reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =

11901190 , rawList (Var $ tacN "TyConArg") (map reflectConArg tyConArgs)

11911191 , reflectRaw tyConRes

11921192 , rawList (rawTripleTy (Var $ reflm "TTName")

1193− (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "CtorArg"))

1193+ (RApp (Var (sNS (sUN "List") ["List", "Prelude"]))

1194+ (Var $ tacN "CtorArg"))

11941195 (Var $ reflm "Raw"))

1195− [ rawTriple ((Var $ reflm "TTName"),

1196− (RApp (Var (sNS (sUN "List") ["List", "Prelude"])) (Var $ tacN "CtorArg")),

1197− (Var $ reflm "Raw"))

1198− (reflectName cn,

1199− rawList (Var $ tacN "CtorArg") (map reflectCtorArg cargs),

1200− reflectRaw cty)

1196+ [ rawTriple ((Var $ reflm "TTName")

1197+ ,(RApp (Var (sNS (sUN "List") ["List", "Prelude"]))

1198+ (Var $ tacN "CtorArg"))

1199+ ,(Var $ reflm "Raw"))

1200+ (reflectName cn

1201+ ,rawList (Var $ tacN "CtorArg")

1202+ (map reflectCtorArg cargs)

1203+ ,reflectRaw cty)

12011204 | (cn, cargs, cty) <- constrs

12021205 ]

12031206 ]

@@ -1207,11 +1210,17 @@ reflectDatatype (RDatatype tyn tyConArgs tyConRes constrs) =

12071210 RApp (Var $ tacN "TyConIndex") (reflectArg a)

12081211

12091212reflectFunClause :: RFunClause Term -> Raw

1210−reflectFunClause (RMkFunClause lhs rhs) = raw_apply (Var $ tacN "MkFunClause") $ (Var $ reflm "TT") : map reflect [ lhs, rhs ]

1211−reflectFunClause (RMkImpossibleClause lhs) = raw_apply (Var $ tacN "MkImpossibleClause") $ [ Var $ reflm "TT", reflect lhs ]

1213+reflectFunClause (RMkFunClause lhs rhs) = raw_apply (Var $ tacN "MkFunClause")

1214+ $ (Var $ reflm "TT") : map reflect [ lhs, rhs ]

1215+

1216+reflectFunClause (RMkImpossibleClause lhs) = raw_apply (Var $ tacN "MkImpossibleClause")

1217+ [ Var $ reflm "TT", reflect lhs ]

12121218

12131219reflectFunDefn :: RFunDefn Term -> Raw

1214−reflectFunDefn (RDefineFun name clauses) = raw_apply (Var $ tacN "DefineFun") [ Var $ reflm "TT"

1215− , reflectName name

1216− , rawList (RApp (Var $ tacN "FunClause") (Var $ reflm "TT")) (map reflectFunClause clauses)

1217− ]

1220+reflectFunDefn (RDefineFun name clauses) = raw_apply (Var $ tacN "DefineFun")

1221+ [ Var $ reflm "TT"

1222+ , reflectName name

1223+ , rawList (RApp (Var $ tacN "FunClause")

1224+ (Var $ reflm "TT"))

1225+ (map reflectFunClause clauses)

1226+ ]

src/Pkg/Package.hs+1−1

@@ -139,7 +139,7 @@ replPkg copts fp = do

139139 let mod = idris_main pkgdesc

140140 let f = toPath (showCG mod)

141141 putIState orig

142− dir <- runIO $ getCurrentDirectory

142+ dir <- runIO getCurrentDirectory

143143 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc

144144

145145 if (f /= "")