32f91a6 · Idris-dev · git.iko.soy

289 --trace ("ELAB " ++ show t') $

290 let fc = fileFC "Force"

291 env <- get_env

292− handleError (forceErr env)

292+ handleError (forceErr t' env)

293 (elab' ina fc' t')

294 (elab' ina fc' (PApp fc (PRef fc (sUN "Force"))

295 [pimp (sUN "t") Placeholder True,

296 pimp (sUN "a") Placeholder True,

297 pexp ct])) True

298

299− forceErr env (CantUnify _ (t,_) (t',_) _ _ _)

299+ forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

300 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

301− ht == txt "Lazy'" = True

301+ ht == txt "Lazy'" = notDelay orig

302− forceErr env (CantUnify _ (t,_) (t',_) _ _ _)

302+ forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

303 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),

304− ht == txt "Lazy'" = True

304+ ht == txt "Lazy'" = notDelay orig

305− forceErr env (InfiniteUnify _ t _)

305+ forceErr orig env (InfiniteUnify _ t _)

306 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

307− ht == txt "Lazy'" = True

307+ ht == txt "Lazy'" = notDelay orig

308− forceErr env (Elaborating _ _ t) = forceErr env t

308+ forceErr orig env (Elaborating _ _ t) = forceErr orig env t

309− forceErr env (ElaboratingArg _ _ _ t) = forceErr env t

309+ forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t

310− forceErr env (At _ t) = forceErr env t

310+ forceErr orig env (At _ t) = forceErr orig env t

311− forceErr env t = False

311+ forceErr orig env t = False

312+

313+ notDelay t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = False

314+ notDelay _ = True

312

315

313 local f = do e <- get_env

316 local f = do e <- get_env

314 return (f `elem` map fst e)

317 return (f `elem` map fst e)