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

src/IRTS/CodegenC.hs+1−1

compare with master

unifiedsplit

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

808

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

810genWrapper (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"

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

813 renderArgs argList ++")\n" ++

814 "{\n" ++

src/IRTS/Compiler.hs+6−6

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

483 [t', LConst (BI 1)]

484

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

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

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

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

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

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

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

489−irTerm top vs env Erased = return $ LNothing

489+irTerm top vs env Erased = return LNothing

490−irTerm top vs env Impossible = return $ LNothing

490+irTerm top vs env Impossible = return LNothing

491

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

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

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

500 = do let l' = toFDesc l

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

502 return (l', r')

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

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

504

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

506 toFDesc tm

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

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

99 where

100 ffiParse :: String -> [FFI]

101 ffiParse "" = []

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

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

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

104 ffiParse ('%':s:ss)

105 | isDigit s =

src/IRTS/Lang.hs+1−1

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

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

214 return (LOp f args')

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

216−lift env LNothing = return $ LNothing

216+lift env LNothing = return LNothing

217

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

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

src/IRTS/Simplified.hs+1−1

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

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

215 Nothing -> case lookupCtxtExact n ctxt of

216 Just (DConstructor _ i ar) ->

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

217+ failsc "can't pass constructor here"

218 Just _ -> return (Glob n)

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

220 " in " ++ show tm ++ " " ++ show envTop

src/Idris/AbsSyntax.hs+5−5

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

583

584setSO :: Maybe String -> Idris ()

585setSO s = do i <- getIState

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

586+ putIState (i { compiled_so = s })

587

588getIState :: Idris IState

589getIState = get

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

617getName :: Idris Int

618getName = do i <- getIState;

619 let idx = idris_name i;

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

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

621 return idx

622

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

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

686 _ -> return True

687

688setContext :: Context -> Idris ()

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

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

690

691updateContext :: (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) } )

693

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

695addConstraints fc (v, cs)

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

1741 = case lookup n using of

1742 Just ty -> PPi impl_gen

1743 n NoFC ty (pibind using ns sc)

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

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

1745 n NoFC Placeholder (pibind using ns sc)

1746

1747-- | 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

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

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

1872 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

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

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

1876 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) []

143 let file = extractFileName f

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

145 ibcsd <- lift $ valIBCSubDir i

146− ids <- lift $ allImportDirs

146+ ids <- lift allImportDirs

147− fp <- lift $ findImport ids ibcsd file

147+ fp <- lift $ findImport ids ibcsd file

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

149 mt <- lift $ runIO $ getIModTime fp

150 if (file `elem` built)

src/Idris/CmdOptions.hs+1−1

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

226parseLogCats s =

227 case lastMay (readP_to_S (doParse) s) of

228 Just (xs, _) -> return xs

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

229+ _ -> fail "Incorrect categories specified"

230 where

231 doParse :: ReadP [LogCat]

232 doParse = do

src/Idris/Completion.hs+2−2

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

148 completeArg (OptionalArg a) = completeArg a

149 completeArg (SeqArgs a b) = completeArg a

150 completeArg _ = noCompletion (prev, next)

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

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

152

153-- | Complete REPL commands and defined identifiers

154replCompletion :: CompletionFunc Idris

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

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

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

170 lookup tac tacticArgs

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

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

172 completeArg Nothing = noCompletion (prev, next)

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

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

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

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

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

655 ulog <- getUnifyLog

656 g <- goal

657+ traceWhen ulog

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

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

658− end_unify

659+ end_unify

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

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

660 where updateUnify us n = case lookup n us of

661 where updateUnify us n = case lookup n us of

661 Just (P _ t _) -> t

662 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)

182unbindEnv :: EnvTT n -> TT n -> TT n

183unbindEnv [] tm = tm

184unbindEnv (_: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."

186

187usable :: Bool -- specialising

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

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

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

559

560instance Quote Value where

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

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

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

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

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

564 b' <- quoteB b

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

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

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

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

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

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

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

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

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

576− quote i VErased = return $ Erased

576+ quote i VErased = return Erased

577− quote i VImpossible = return $ Impossible

577+ quote i VImpossible = return Impossible

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

579 return (Proj v' j)

580 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

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

766 [elimTy] -> do

767 param_pos <- case lookupMetaInformation tnm ctxt of

768− [DataMI param_pos] -> return param_pos

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)

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)

770 _ -> return []

771 let (params, indicies) = splitTyArgs param_pos tyargs

772 let args = getArgTys elimTy

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

774 let args' = drop (length params) args

775 let propTy = head args'

776 let restargs = init $ tail args'

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

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

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

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

779 let scr = last $ tail args'

780 let indxnames = makeIndexNames indicies

781 currentNames <- query $ allTTNames . getProofTerm . pterm

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

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

791 recents = x : recents ps })

792 mapM_ addConsHole (reverse consargs')

793− let res' = forget $ res

793+ let res' = forget res

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

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

796 return scv'

src/Idris/Coverage.hs+1−2

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

758

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

760mkMultiPaths ist path [] = [reverse path]

761−mkMultiPaths ist path cg

761+mkMultiPaths ist path cg = concatMap extend cg

762− = concat (map extend cg)

763 where extend (nextf, args)

762 where extend (nextf, args)

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

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

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

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

src/Idris/Directives.hs+2−2

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

54 ctxt <- getContext

55 case lookupDefAccExact n False ctxt of

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

57− addIBC (IBCAccess n Public)

57+ addIBC (IBCAccess n Public)

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

59directiveAction (DInjective n') = do

60 ns <- allNamespaces n'

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

77 added <- addDyLib libs

78 case added of

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

80− Right msg -> fail $ msg

80+ Right msg -> fail msg

81

82directiveAction (DNameHint ty tyFC ns) = do

83 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

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

139

140 -- 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)

142 addIBC (IBCClass tn)

143

144 sendHighlighting $

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

164 checkDefaultSuperclassInstance :: PDecl -> Idris ()

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

166 = 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."))

168 i <- getIState

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

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

171 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."))

173 return ()

174

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

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

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

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

422 (pe_clauses specdecl)

423 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

425 (PEGenerated:opts) newnm def

426 return [trans]

427 else return [])

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

555

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

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

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

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

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

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

560

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

562 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

713 mapM_ (elabCaseBlock winfo opts) is

714

715 ctxt <- getContext

716− logElab 5 $ "Rechecking"

716+ logElab 5 "Rechecking"

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

718

719 (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

760 addIBC (IBCErrRev (crhs, clhs))

761 addErrRev (crhs, clhs)

762 pop_estack

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

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

764 where

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

766 pinfo info ns ds i

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

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

904

905 -- 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]

907

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

909 " 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)

991 mapM_ (elabCaseBlock info opts) is

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

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

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

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

995 where

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

997 getImps _ = []

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

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

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

1001 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

1003

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

1005 = 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

258 checkUniqueKind (UType AllTypes) _

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

260 checkUniqueKind _ _ = return ()

261−

261+

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

263addParamConstraints fc ps cty cons

264 = case getRetTy cty of

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

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

266 (map getParamNames cons)

267 _ -> return ()

268 where

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

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

278 paramArgs i [] = []

279

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

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

281 where

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

283 = case getRetTy ty of

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

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

306 ElabInfo -> EliminatorState ()

307elabCaseFun ind paramPos n ty cons info = do

308− elimLog $ "Elaborating case function"

308+ elimLog "Elaborating case function"

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

310 let (cnstrs, _) = splitPi ty

311 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

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

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

149 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

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

152

153 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

104

105 mapM_ (elabCaseBlock info opts) is

106 ctxt <- getContext

107− logElab 5 $ "Rechecking"

107+ logElab 5 "Rechecking"

108− logElab 6 $ show tyT

108+ logElab 6 (show tyT)

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

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

111

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

224 case fam of

225 P _ tyn _ -> do addAutoHint tyn n

226 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"

228

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

230 -- 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

150

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

152loadPkgIndex :: String -> Idris ()

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

153+loadPkgIndex pkg = do ddir <- runIO getIdrisLibDir

154 addImportDir (ddir </> pkg)

155 fp <- findPkgIndex pkg

156 loadIBC True IBC_Building fp

src/Idris/IdeMode.hs+12−12

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

258 | GetIdrisVersion

259

260sexpToCommand :: SExp -> Maybe IdeModeCommand

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

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

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

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

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

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)))

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)

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

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

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)

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)

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)

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)

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)

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)

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

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

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

275-- 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

423createIndex nss out =

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

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

426− H.h1 $ "Namespaces"

426+ H.h1 "Namespaces"

427 H.ul ! class_ "names" $ do

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

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

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

523 docExtractor (_, _, _, Nothing) = Nothing

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

525 -- 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

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

528

529 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

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

381 runIO $ copyFile fb fn

382 else case idris_outputmode i of

383− RawOutput _ -> iPrintResult $ lem_app

383+ RawOutput _ -> iPrintResult lem_app

384 IdeMode n h ->

385 let good = SexpList [SymbolAtom "ok",

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

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

495 addLem before tyline lem lem_app later

496 = let (bef_end, blankline : bef_start)

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

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

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

499 x -> x

500 mvline = updateMeta tyline (show n) lem_app in

501 unlines $ reverse bef_start ++

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

505 addProv before tyline lem_app later

506 = let (later_bef, blankline : later_end)

507 = case span (not . blank) later of

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

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

509 x -> x in

510 unlines $ before ++ tyline :

511 (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

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

233 let n = show tyn_in ++ " "

234 let s = kw ++ n

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

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

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

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

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

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

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

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

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

501dependentPair pun prev openFC syn =

502− if prev == [] then

502+ if null prev then

503 nametypePart <|> namePart

504 else

505 case pun of

src/Idris/ProofSearch.hs+2−2

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

364 = do hs <- get_holes

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

366

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"

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

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

370 = do compute

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

484 solven n = replicateM_ n solve

485

486 resolve n depth

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

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

488 | otherwise

489 = do lams <- introImps

490 t <- goal

src/Idris/REPL.hs+11−11

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

782edit "" orig = iputStrLn "Nothing to edit"

783edit f orig

784 = do i <- getIState

785− env <- runIO $ getEnvironment

785+ env <- runIO getEnvironment

786 let editor = getEditor env

787 let line = case errSpan i of

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

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

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

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

917 fixClauses decl = decl

918−

918+

919 info = recinfo (fileFC "toplevel")

920

921process fn (Undefine names) = undefine names

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

1205 n <- case metavars of

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

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

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

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

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

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

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

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

1212 -- recheck totality

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

1280 []

1281 (idris_infixes i))

1282 tms))

1283− _ -> iPrintError $ "Ambiguous name"

1283+ _ -> iPrintError "Ambiguous name"

1284process fn (DynamicLink l)

1285 = do i <- getIState

1286 let importdirs = opt_importdirs (idris_options i)

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

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

1405 parse n = Left n

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

1407− cd <- runIO $ getCurrentDirectory

1407+ cd <- runIO getCurrentDirectory

1408 let outputDir = cd </> "doc"

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

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

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

1588 case errSpan inew of

1589 Nothing ->

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

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

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

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

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

1594 _ -> return ()

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

1717

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

1719 putIState (i { default_total = DefaultCheckingTotal })

1720− tty <- runIO $ isATTY

1720+ tty <- runIO isATTY

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

1722

1723

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

1791 runIO $ exitWith (ExitFailure 1)

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

1793 exprs

1794− runIO $ exitWith ExitSuccess

1794+ runIO exitSuccess

1795

1796

1797 case script of

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

1829 makeOption _ = return ()

1830

1831 addPkgDir :: String -> Idris ()

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

1832+ addPkgDir p = do ddir <- runIO getIdrisLibDir

1833 addImportDir (ddir </> p)

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

1835

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

1848 Success term -> do ctxt <- getContext

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

1850 res <- execute tm

1851− runIO $ exitWith ExitSuccess

1851+ runIO $ exitSuccess

1852

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

1854getIdrisUserDataDir :: Idris FilePath

src/Idris/Reflection.hs+40−31

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

173reifyTT t@(App _ _ _)

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

175reifyTT t@(P _ n _)

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

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

177reifyTT t@(P _ n _)

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

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

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

180

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

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

217reifyRaw t@(App _ _ _)

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

219reifyRaw t@(P _ n _)

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

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

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

222

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

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

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

333

334reifyTTConst :: Term -> ElabD Const

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

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

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

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

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

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

338reifyTTConst t@(App _ _ _)

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

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

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

343reifyTTConstApp f aty

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

364 lift . tfail . Msg $

365 "Can't reify the variable " ++

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

389reifyTTUExp :: Term -> ElabD UExp

390reifyTTUExp t@(App _ _ _)

391 = case unApply t of

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

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

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

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

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

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

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

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

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

487reflectTTQuotePattern unq Erased

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

489 movelast erased

490− fill $ (Var erased)

490+ fill (Var erased)

491reflectTTQuotePattern unq Impossible

492 = lift . tfail . InternalMsg $

493 "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) =

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

1191 , reflectRaw tyConRes

1192 , 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"))

1194 (Var $ reflm "Raw"))

1195 (Var $ reflm "Raw"))

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

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

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

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

1198+ (Var $ tacN "CtorArg"))

1197− (Var $ reflm "Raw"))

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

1198− (reflectName cn,

1200+ (reflectName cn

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

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

1202+ (map reflectCtorArg cargs)

1200− reflectRaw cty)

1203+ ,reflectRaw cty)

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

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

1202 ]

1205 ]

1203 ]

1206 ]

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

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

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

1208

1211

1209reflectFunClause :: RFunClause Term -> Raw

1212reflectFunClause :: RFunClause Term -> Raw

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

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

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

1215+

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

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

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

1212

1218

1213reflectFunDefn :: RFunDefn Term -> Raw

1219reflectFunDefn :: RFunDefn Term -> Raw

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

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

1221+ [ Var $ reflm "TT"

1215− , reflectName name

1222+ , reflectName name

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

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

1224+ (Var $ reflm "TT"))

1225+ (map reflectFunClause clauses)

1217− ]

1226+ ]

src/Pkg/Package.hs+1−1

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

139 let mod = idris_main pkgdesc

140 let f = toPath (showCG mod)

141 putIState orig

142− dir <- runIO $ getCurrentDirectory

142+ dir <- runIO getCurrentDirectory

143 runIO $ setCurrentDirectory $ dir </> sourcedir pkgdesc

144

145 if (f /= "")