src/Core/Execute.hs · Idris-dev

git.iko.soy/Idris-dev

on 93fa7ce help sign in

Idris-dev/src/Core/Execute.hs

511 lines 23 kB history raw

1{-# LANGUAGE PatternGuards, ExistentialQuantification #-}

2module Core.Execute (execute) where

4import Idris.AbsSyntax

5import Idris.AbsSyntaxTree

7import Core.TT

8import Core.Evaluate

9import Core.CaseTree

11import Debug.Trace

13import Util.DynamicLinker

14import Util.System

16import Control.Applicative hiding (Const)

17import Control.Monad.Trans

18import Control.Monad.Trans.State.Strict

19import Control.Monad.Trans.Error

20import Control.Monad

21import Data.Maybe

22import qualified Data.Map as M

24import Foreign.LibFFI

25import Foreign.C.String

26import Foreign.Marshal.Alloc (free)

27import Foreign.Ptr

29import System.IO

32data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Show

34data ExecState = ExecState { exec_thunks :: M.Map Int Lazy -- ^ Thunks - the result of evaluating "lazy" or calling lazy funcs

35 , exec_next_thunk :: Int -- ^ Ensure thunk key uniqueness

36 , exec_implicits :: Ctxt [PArg] -- ^ Necessary info on laziness from idris monad

37 , exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad

38 }

40data ExecVal = EP NameType Name ExecVal

41 | EV Int

42 | EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)

43 | EApp ExecVal ExecVal

44 | EType UExp

45 | EErased

46 | EConstant Const

47 | forall a. EPtr (Ptr a)

48 | EThunk Int

49 | EHandle Handle

51instance Show ExecVal where

52 show (EP _ n _) = show n

53 show (EV i) = "!!V" ++ show i ++ "!!"

54 show (EBind n b body) = "EBind " ++ show b ++ " <<fn>>"

55 show (EApp e1 e2) = show e1 ++ " (" ++ show e2 ++ ")"

56 show (EType _) = "Type"

57 show EErased = "[__]"

58 show (EConstant c) = show c

59 show (EPtr p) = "<<ptr " ++ show p ++ ">>"

60 show (EThunk i) = "<<thunk " ++ show i ++ ">>"

61 show (EHandle h) = "<<handle " ++ show h ++ ">>"

63toTT :: ExecVal -> Exec Term

64toTT (EP nt n ty) = (P nt n) <$> (toTT ty)

65toTT (EV i) = return $ V i

66toTT (EBind n b body) = do body' <- body $ EP Bound n EErased

67 b' <- fixBinder b

68 Bind n b' <$> toTT body'

69 where fixBinder (Lam t) = Lam <$> toTT t

70 fixBinder (Pi t) = Pi <$> toTT t

71 fixBinder (Let t1 t2) = Let <$> toTT t1 <*> toTT t2

72 fixBinder (NLet t1 t2) = NLet <$> toTT t1 <*> toTT t2

73 fixBinder (Hole t) = Hole <$> toTT t

74 fixBinder (GHole t) = GHole <$> toTT t

75 fixBinder (Guess t1 t2) = Guess <$> toTT t1 <*> toTT t2

76 fixBinder (PVar t) = PVar <$> toTT t

77 fixBinder (PVTy t) = PVTy <$> toTT t

78toTT (EApp e1 e2) = do e1' <- toTT e1

79 e2' <- toTT e2

80 return $ App e1' e2'

81toTT (EType u) = return $ TType u

82toTT EErased = return Erased

83toTT (EConstant c) = return (Constant c)

84toTT (EThunk i) = return (P (DCon 0 0) (MN i "THUNK") Erased) --(force i) >>= toTT

85toTT (EHandle _) = return Erased

87unApplyV :: ExecVal -> (ExecVal, [ExecVal])

88unApplyV tm = ua [] tm

89 where ua args (EApp f a) = ua (a:args) f

90 ua args t = (t, args)

92mkEApp :: ExecVal -> [ExecVal] -> ExecVal

93mkEApp f [] = f

94mkEApp f (a:args) = mkEApp (EApp f a) args

96initState :: Idris ExecState

97initState = do ist <- getIState

98 return $ ExecState M.empty 0 (idris_implicits ist) (idris_dynamic_libs ist)

100type Exec = ErrorT String (StateT ExecState IO)

101

102runExec :: Exec a -> ExecState -> IO (Either String a)

103runExec ex st = fst <$> runStateT (runErrorT ex) st

104

105getExecState :: Exec ExecState

106getExecState = lift get

107

108putExecState :: ExecState -> Exec ()

109putExecState = lift . put

110

111execFail :: String -> Exec a

112execFail = throwError

113

114execIO :: IO a -> Exec a

115execIO = lift . lift

116

117delay :: ExecEnv -> Context -> Term -> Exec ExecVal

118delay env ctxt tm =

119 do st <- getExecState

120 let i = exec_next_thunk st

121 putExecState $ st { exec_thunks = M.insert i (Delayed env ctxt tm) (exec_thunks st)

122 , exec_next_thunk = exec_next_thunk st + 1

123 }

124 return $ EThunk i

125

126force :: Int -> Exec ExecVal

127force i = do st <- getExecState

128 case M.lookup i (exec_thunks st) of

129 Just (Delayed env ctxt tm) -> do tm' <- doExec env ctxt tm

130 case tm' of

131 EThunk i ->

132 do res <- force i

133 update res i

134 return res

135 _ -> do update tm' i

136 return tm'

137 Just (Forced tm) -> return tm

138 Nothing -> execFail "Tried to exec non-existing thunk. This is a bug!"

139 where update :: ExecVal -> Int -> Exec ()

140 update tm i = do est <- getExecState

141 putExecState $ est { exec_thunks = M.insert i (Forced tm) (exec_thunks est) }

142

143tryForce :: ExecVal -> Exec ExecVal

144tryForce (EThunk i) = force i

145tryForce tm = return tm

146

147debugThunks :: Exec ()

148debugThunks = do st <- getExecState

149 execIO $ putStrLn (take 4000 (show (exec_thunks st)))

150

151execute :: Term -> Idris Term

152execute tm = do est <- initState

153 ctxt <- getContext

154 res <- lift $ flip runExec est $ do res <- doExec [] ctxt tm

155 toTT res

156 case res of

157 Left err -> fail err

158 Right tm' -> return tm'

159

160ioWrap :: ExecVal -> ExecVal

161ioWrap tm = mkEApp (EP (DCon 0 2) (UN "prim__IO") EErased) [EErased, tm]

162

163ioUnit :: ExecVal

164ioUnit = ioWrap (EP Ref unitCon EErased)

165

166type ExecEnv = [(Name, ExecVal)]

167

168doExec :: ExecEnv -> Context -> Term -> Exec ExecVal

169doExec env ctxt p@(P Ref n ty) =

170 do let val = lookupDef n ctxt

171 case val of

172 [Function _ tm] -> doExec env ctxt tm

173 [TyDecl _ _] -> return (EP Ref n EErased) -- abstract def

174 [Operator tp arity op] -> return (EP Ref n EErased) -- will be special-cased later

175 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun

176 doExec env ctxt tm

177 [CaseOp _ _ _ _ _ ns sc _ _] -> return (EP Ref n EErased)

178 thing -> trace (take 200 $ "got to " ++ show thing ++ " lookup up " ++ show n) $ undefined

179doExec env ctxt p@(P Bound n ty) =

180 case lookup n env of

181 Nothing -> execFail "not found"

182 Just tm -> return tm

183doExec env ctxt (P (DCon a b) n _) = return (EP (DCon a b) n EErased)

184doExec env ctxt (P (TCon a b) n _) = return (EP (TCon a b) n EErased)

185doExec env ctxt v@(V i) | i < length env = return (snd (env !! i))

186 | otherwise = execFail "env too small"

187doExec env ctxt (Bind n (Let t v) body) = do v' <- doExec env ctxt v

188 doExec ((n, v'):env) ctxt body

189doExec env ctxt (Bind n (NLet t v) body) = trace "NLet" $ undefined

190doExec env ctxt tm@(Bind n b body) = return $

191 EBind n (fmap (\_->EErased) b)

192 (\arg -> doExec ((n, arg):env) ctxt body)

193doExec env ctxt a@(App _ _) = execApp env ctxt (unApply a)

194doExec env ctxt (Constant c) = return (EConstant c)

195doExec env ctxt (Proj tm i) = let (x, xs) = unApply tm in

196 doExec env ctxt ((x:xs) !! i)

197doExec env ctxt Erased = return EErased

198doExec env ctxt Impossible = fail "Tried to execute an impossible case"

199doExec env ctxt (TType u) = return (EType u)

200

201execApp :: ExecEnv -> Context -> (Term, [Term]) -> Exec ExecVal

202execApp env ctxt (f, args) = do newF <- doExec env ctxt f

203 laziness <- (++ repeat False) <$> (getLaziness newF)

204 newArgs <- mapM argExec (zip args laziness)

205 execApp' env ctxt newF newArgs

206 where getLaziness (EP _ (UN "lazy") _) = return [False, True]

207 getLaziness (EP _ n _) = do est <- getExecState

208 let argInfo = exec_implicits est

209 case lookupCtxtName n argInfo of

210 [] -> return (repeat False)

211 [ps] -> return $ map lazyarg (snd ps)

212 many -> execFail $ "Ambiguous " ++ show n ++ ", found " ++ (take 200 $ show many)

213 getLaziness _ = return (repeat False) -- ok due to zip above

214 argExec :: (Term, Bool) -> Exec ExecVal

215 argExec (tm, False) = doExec env ctxt tm

216 argExec (tm, True) = delay env ctxt tm

217

218

219execApp' :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal

220execApp' env ctxt v [] = return v -- no args is just a constant! can result from function calls

221execApp' env ctxt (EP _ (UN "unsafePerformIO") _) (ty:action:rest) | (prim__IO, [_, v]) <- unApplyV action =

222 execApp' env ctxt v rest

223

224execApp' env ctxt (EP _ (UN "io_bind") _) args@(_:_:v:k:rest) | (prim__IO, [_, v']) <- unApplyV v =

225 do v'' <- tryForce v'

226 res <- execApp' env ctxt k [v''] >>= tryForce

227 execApp' env ctxt res rest

228execApp' env ctxt con@(EP _ (UN "io_return") _) args@(tp:v:rest) =

229 do v' <- tryForce v

230 execApp' env ctxt (mkEApp con [tp, v']) rest

231

232-- Special cases arising from not having access to the C RTS in the interpreter

233execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str arg):rest)

234 | Just (FFun "putStr" _ _) <- foreignFromTT fn = do execIO (putStr arg)

235 execApp' env ctxt ioUnit rest

236execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:EConstant (Str f):EConstant (Str mode):rest)

237 | Just (FFun "fileOpen" _ _) <- foreignFromTT fn = do m <- case mode of

238 "r" -> return ReadMode

239 "w" -> return WriteMode

240 "a" -> return AppendMode

241 "rw" -> return ReadWriteMode

242 "wr" -> return ReadWriteMode

243 "r+" -> return ReadWriteMode

244 _ -> execFail ("Invalid mode for " ++ f ++ ": " ++ mode)

245 h <- execIO $ openFile f m

246 execApp' env ctxt (ioWrap (EHandle h)) rest

247

248execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)

249 | Just (FFun "fileEOF" _ _) <- foreignFromTT fn = do eofp <- execIO $ hIsEOF h

250 let res = ioWrap (EConstant (I $ if eofp then 1 else 0))

251 execApp' env ctxt res rest

252

253execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EHandle h):rest)

254 | Just (FFun "fileClose" _ _) <- foreignFromTT fn = do execIO $ hClose h

255 execApp' env ctxt ioUnit rest

256

257execApp' env ctxt (EP _ (UN "mkForeign") _) (_:fn:(EPtr p):rest)

258 | Just (FFun "isNull" _ _) <- foreignFromTT fn = let res = if p == nullPtr then 1 else 0 in

259 execApp' env ctxt (EConstant (I res)) rest

260

261execApp' env ctxt f@(EP _ (UN "mkForeign") _) args@(ty:fn:xs) | Just (FFun _ argTs retT) <- foreignFromTT fn

262 , length xs >= length argTs =

263 do res <- stepForeign (ty:fn:take (length argTs) xs)

264 case res of

265 Nothing -> fail "Could not call foreign function"

266 Just r -> return (mkEApp r (drop (length argTs) xs))

267 | otherwise = return (mkEApp f args)

268

269execApp' env ctxt f@(EP _ n _) args =

270 do let val = lookupDef n ctxt

271 case val of

272 [Function _ tm] -> fail "should already have been eval'd"

273 [TyDecl nt ty] -> return $ mkEApp f args

274 [Operator tp arity op] ->

275 if length args >= arity

276 then do args' <- mapM tryForce $ take arity args

277 case getOp n args' of

278 Just res -> do r <- res

279 execApp' env ctxt r (drop arity args)

280 Nothing -> return (mkEApp f args)

281 else return (mkEApp f args)

282 [CaseOp _ _ _ _ _ [] (STerm tm) _ _] -> -- nullary fun

283 do rhs <- doExec env ctxt tm

284 execApp' env ctxt rhs args

285 [CaseOp _ _ _ _ _ ns sc _ _] ->

286 do res <- execCase env ctxt ns sc args

287 return $ fromMaybe (mkEApp f args) res

288 thing -> return $ mkEApp f args

289 where getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal)

290 getOp (UN "prim__addInt") [EConstant (I i1), EConstant (I i2)] =

291 primRes I (i1 + i2)

292 getOp (UN "prim__charToInt") [EConstant (Ch c)] =

293 primRes I (fromEnum c)

294 getOp (UN "prim__concat") [EConstant (Str s1), EConstant (Str s2)] =

295 primRes Str (s1 ++ s2)

296 getOp (UN "prim__eqChar") [EConstant (Ch c1), EConstant (Ch c2)] =

297 primResBool (c1 == c2)

298 getOp (UN "prim__eqInt") [EConstant (I i1), EConstant (I i2)] =

299 primResBool (i1 == i2)

300 getOp (UN "prim__eqString") [EConstant (Str s1), EConstant (Str s2)] =

301 primResBool (s1 == s2)

302 getOp (UN "prim__intToFloat") [EConstant (I i)] =

303 primRes Fl (fromRational (toRational i))

304 getOp (UN "prim__intToStr") [EConstant (I i)] =

305 primRes Str (show i)

306 getOp (UN "prim_lenString") [EConstant (Str s)] =

307 primRes I (length s)

308 getOp (UN "prim__ltInt") [EConstant (I i1), EConstant (I i2)] =

309 primResBool (i1 < i2)

310 getOp (UN "prim__mulBigInt") [EConstant (BI i1), EConstant (BI i2)] =

311 primRes BI (i1 * i2)

312 getOp (UN "prim__mulFloat") [EConstant (Fl i1), EConstant (Fl i2)] =

313 primRes Fl (i1 * i2)

314 getOp (UN "prim__mulInt") [EConstant (I i1), EConstant (I i2)] =

315 primRes I (i1 * i2)

316 getOp (UN "prim__readString") [EP _ (UN "prim__stdin") _] =

317 Just $ do line <- execIO getLine

318 return (EConstant (Str line))

319 getOp (UN "prim__readString") [EHandle h] =

320 Just $ do contents <- execIO $ hGetLine h

321 return (EConstant (Str contents))

322 getOp (UN "prim__strCons") [EConstant (Ch c), EConstant (Str s)] =

323 primRes Str (c:s)

324 getOp (UN "prim__strHead") [EConstant (Str (c:s))] =

325 primRes Ch c

326 getOp (UN "prim__strRev") [EConstant (Str s)] =

327 primRes Str (reverse s)

328 getOp (UN "prim__strTail") [EConstant (Str (c:s))] =

329 primRes Str s

330 getOp (UN "prim__subFloat") [EConstant (Fl i1), EConstant (Fl i2)] =

331 primRes Fl (i1 - i2)

332 getOp (UN "prim__subInt") [EConstant (I i1), EConstant (I i2)] =

333 primRes I (i1 - i2)

334 getOp n args = trace ("No prim " ++ show n ++ " for " ++ take 1000 (show args)) Nothing

335

336 primRes :: (a -> Const) -> a -> Maybe (Exec ExecVal)

337 primRes constr = Just . return . EConstant . constr

338

339 primResBool :: Bool -> Maybe (Exec ExecVal)

340 primResBool b = primRes I (if b then 1 else 0)

341

342execApp' env ctxt bnd@(EBind n b body) (arg:args) = do ret <- body arg

343 let (f', as) = unApplyV ret

344 execApp' env ctxt f' (as ++ args)

345execApp' env ctxt (EThunk i) args = do f <- force i

346 execApp' env ctxt f args

347execApp' env ctxt app@(EApp _ _) args2 | (f, args1) <- unApplyV app = execApp' env ctxt f (args1 ++ args2)

348execApp' env ctxt f args = return (mkEApp f args)

354-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,

355-- evaluates them, then begins the checks for matching cases.

356execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)

357execCase env ctxt ns sc args =

358 let arity = length ns in

359 if arity <= length args

360 then do let amap = zip ns args

361 caseRes <- execCase' env ctxt amap sc

362 case caseRes of

363 Just res -> Just <$> execApp' (map (\(n, tm) -> (n, tm)) amap ++ env) ctxt res (drop arity args)

364 Nothing -> return Nothing

365 else return Nothing

366

367-- | Take bindings and a case tree and examines them, executing the matching case if possible.

368execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)

369execCase' env ctxt amap (UnmatchedCase _) = return Nothing

370execCase' env ctxt amap (STerm tm) =

371 Just <$> doExec (map (\(n, v) -> (n, v)) amap ++ env) ctxt tm

372execCase' env ctxt amap (Case n alts) | Just tm <- lookup n amap =

373 do tm' <- tryForce tm

374 case chooseAlt tm' alts of

375 Just (newCase, newBindings) ->

376 let amap' = newBindings ++ (filter (\(x,_) -> not (elem x (map fst newBindings))) amap) in

377 execCase' env ctxt amap' newCase

378 Nothing -> return Nothing

379

380chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])

381chooseAlt _ (DefaultCase sc : alts) = Just (sc, [])

382chooseAlt (EConstant c) (ConstCase c' sc : alts) | c == c' = Just (sc, [])

383chooseAlt tm (ConCase n i ns sc : alts) | ((EP _ cn _), args) <- unApplyV tm

384 , cn == n = Just (sc, zip ns args)

385 | otherwise = chooseAlt tm alts

386chooseAlt tm (_:alts) = chooseAlt tm alts

387chooseAlt _ [] = Nothing

394idrisType :: FTy -> ExecVal

395idrisType FUnit = EP Ref unitTy EErased

396idrisType ft = EConstant (idr ft)

397 where idr FInt = IType

398 idr FFloat = FlType

399 idr FChar = ChType

400 idr FString = StrType

401 idr FPtr = PtrType

402

403data Foreign = FFun String [FTy] FTy deriving Show

404

405

406call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)

407call (FFun name argTypes retType) args =

408 do fn <- findForeign name

409 case fn of

410 Nothing -> return Nothing

411 Just f -> do res <- call' f args retType

412 return . Just . ioWrap $ res

413 where call' :: ForeignFun -> [ExecVal] -> FTy -> Exec ExecVal

414 call' (Fun _ h) args FInt = do res <- execIO $ callFFI h retCInt (prepArgs args)

415 return (EConstant (I (fromIntegral res)))

416 call' (Fun _ h) args FFloat = do res <- execIO $ callFFI h retCDouble (prepArgs args)

417 return (EConstant (Fl (realToFrac res)))

418 call' (Fun _ h) args FChar = do res <- execIO $ callFFI h retCChar (prepArgs args)

419 return (EConstant (Ch (castCCharToChar res)))

420 call' (Fun _ h) args FString = do res <- execIO $ callFFI h retCString (prepArgs args)

421 hStr <- execIO $ peekCString res

422-- lift $ free res

423 return (EConstant (Str hStr))

424

425 call' (Fun _ h) args FPtr = do res <- execIO $ callFFI h (retPtr retVoid) (prepArgs args)

426 return (EPtr res)

427 call' (Fun _ h) args FUnit = do res <- execIO $ callFFI h retVoid (prepArgs args)

428 return (EP Ref unitCon EErased)

429-- call' (Fun _ h) args other = fail ("Unsupported foreign return type " ++ show other)

430

431

432 prepArgs = map prepArg

433 prepArg (EConstant (I i)) = argCInt (fromIntegral i)

434 prepArg (EConstant (Fl f)) = argCDouble (realToFrac f)

435 prepArg (EConstant (Ch c)) = argCChar (castCharToCChar c) -- FIXME - castCharToCChar only safe for first 256 chars

436 prepArg (EConstant (Str s)) = argString s

437 prepArg (EPtr p) = argPtr p

438 prepArg other = trace ("Could not use " ++ take 100 (show other) ++ " as FFI arg.") undefined

439

440

441

442foreignFromTT :: ExecVal -> Maybe Foreign

443foreignFromTT t = case (unApplyV t) of

444 (_, [(EConstant (Str name)), args, ret]) ->

445 do argTy <- unEList args

446 argFTy <- sequence $ map getFTy argTy

447 retFTy <- getFTy ret

448 return $ FFun name argFTy retFTy

449 _ -> trace "failed to construct ffun" Nothing

450

451getFTy :: ExecVal -> Maybe FTy

452getFTy (EP _ (UN t) _) =

453 case t of

454 "FInt" -> Just FInt

455 "FFloat" -> Just FFloat

456 "FChar" -> Just FChar

457 "FString" -> Just FString

458 "FPtr" -> Just FPtr

459 "FUnit" -> Just FUnit

460 _ -> Nothing

461getFTy _ = Nothing

462

463unList :: Term -> Maybe [Term]

464unList tm = case unApply tm of

465 (nil, [_]) -> Just []

466 (cons, ([_, x, xs])) ->

467 do rest <- unList xs

468 return $ x:rest

469 (f, args) -> Nothing

470

471unEList :: ExecVal -> Maybe [ExecVal]

472unEList tm = case unApplyV tm of

473 (nil, [_]) -> Just []

474 (cons, ([_, x, xs])) ->

475 do rest <- unEList xs

476 return $ x:rest

477 (f, args) -> Nothing

478

479

480toConst :: Term -> Maybe Const

481toConst (Constant c) = Just c

482toConst _ = Nothing

483

484stepForeign :: [ExecVal] -> Exec (Maybe ExecVal)

485stepForeign (ty:fn:args) = do let ffun = foreignFromTT fn

486 f' <- case (call <$> ffun) of

487 Just f -> f args

488 Nothing -> return Nothing

489 return f'

490stepForeign _ = fail "Tried to call foreign function that wasn't mkForeign"

491

492mapMaybeM :: Monad m => (a -> m (Maybe b)) -> [a] -> m [b]

493mapMaybeM f [] = return []

494mapMaybeM f (x:xs) = do rest <- mapMaybeM f xs

495 x' <- f x

496 case x' of

497 Just x'' -> return (x'':rest)

498 Nothing -> return rest

499

500findForeign :: String -> Exec (Maybe ForeignFun)

501findForeign fn = do est <- getExecState

502 let libs = exec_dynamic_libs est

503 fns <- mapMaybeM getFn libs

504 case fns of

505 [f] -> return (Just f)

506 [] -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" not found"

507 return Nothing

508 fs -> do execIO . putStrLn $ "Symbol \"" ++ fn ++ "\" is ambiguous. Found " ++

509 show (length fs) ++ " occurrences."

510 return Nothing

511 where getFn lib = execIO $ catchIO (tryLoadFn fn lib) (\_ -> return Nothing)