| ... |
... |
@@ -362,9 +362,11 @@ collectHsWrapBinders wrap = go wrap [] |
|
362
|
362
|
|
|
363
|
363
|
optHsWrapper :: HsWrapper -> HsWrapper
|
|
364
|
364
|
optHsWrapper wrap
|
|
365
|
|
- = foldr (<.>) WpHole (norm wrap [])
|
|
|
365
|
+ = let wrap' = foldr (<.>) WpHole (norm wrap [])
|
|
|
366
|
+ in pprTrace "optHsWrapper" (vcat [ text "in:" <+> ppr wrap, text "out:" <+> ppr wrap' ]) $
|
|
|
367
|
+ wrap'
|
|
366
|
368
|
where
|
|
367
|
|
- norm :: HsWrapper -> VarEnv EvVar -> [HsWrapper] -> [HsWrapper]
|
|
|
369
|
+ norm :: HsWrapper -> [HsWrapper] -> [HsWrapper]
|
|
368
|
370
|
-- norm w ws = w <.> (foldr <.> WpHole ws)
|
|
369
|
371
|
-- INVARIANT: ws:[HsWrapper] is normalised
|
|
370
|
372
|
norm WpHole ws = ws
|
| ... |
... |
@@ -393,6 +395,11 @@ optHsWrapper wrap |
|
393
|
395
|
-- = WpCast (ForAllCo a co) (WpTyLam <.> w)
|
|
394
|
396
|
norm_ty_lam tv (WpCast co : ws)
|
|
395
|
397
|
= norm_co (mkHomoForAllCo tv co) (norm_ty_lam tv ws)
|
|
|
398
|
+
|
|
|
399
|
+ norm_ty_lam tv (WpLet bs : ws)
|
|
|
400
|
+ | Just ws' <- pushWpLet bs ws
|
|
|
401
|
+ = norm_ty_lam tv ws'
|
|
|
402
|
+
|
|
396
|
403
|
norm_ty_lam tv ws
|
|
397
|
404
|
= WpTyLam tv : ws
|
|
398
|
405
|
|
| ... |
... |
@@ -412,10 +419,15 @@ optHsWrapper wrap |
|
412
|
419
|
(mkNomReflCo ManyTy)
|
|
413
|
420
|
(mkRepReflCo (idType ev))
|
|
414
|
421
|
co
|
|
|
422
|
+ norm_ev_lam ev (WpLet bs : ws)
|
|
|
423
|
+ | Just ws' <- pushWpLet bs ws
|
|
|
424
|
+ = norm_ev_lam ev ws'
|
|
|
425
|
+
|
|
415
|
426
|
norm_ev_lam ev ws
|
|
416
|
427
|
= WpEvLam ev : ws
|
|
417
|
428
|
|
|
418
|
429
|
-----------------
|
|
|
430
|
+ -- WpCast co <.> WpCast co' <+> ws = WpCast (co;co') ws
|
|
419
|
431
|
norm_co co (WpCast co' : ws) = norm_co (co `mkTransCo` co') ws
|
|
420
|
432
|
norm_co co ws | isReflexiveCo co = ws
|
|
421
|
433
|
| otherwise = WpCast co : ws
|
| ... |
... |
@@ -424,6 +436,7 @@ optHsWrapper wrap |
|
424
|
436
|
norm_fun w1 w2 (Scaled w t1) t2 ws
|
|
425
|
437
|
= case (optHsWrapper w1, optHsWrapper w2) of
|
|
426
|
438
|
(WpHole, WpHole) -> ws
|
|
|
439
|
+ (WpLet {}, WpHole) -> ws
|
|
427
|
440
|
(WpHole, WpCast co2) -> co_ify (mkRepReflCo t1) co2
|
|
428
|
441
|
(WpCast co1, WpHole) -> co_ify (mkSymCo co1) (mkRepReflCo t2)
|
|
429
|
442
|
(WpCast co1, WpCast co2) -> co_ify (mkSymCo co1) co2
|
| ... |
... |
@@ -431,6 +444,60 @@ optHsWrapper wrap |
|
431
|
444
|
where
|
|
432
|
445
|
co_ify co1 co2 = norm_co (mk_wp_fun_co w co1 co2) ws
|
|
433
|
446
|
|
|
|
447
|
+pushWpLet :: TcEvBinds -> [HsWrapper] -> Maybe [HsWrapper]
|
|
|
448
|
+pushWpLet tc_ev_binds ws
|
|
|
449
|
+ | EvBinds binds <- tc_ev_binds
|
|
|
450
|
+ , Just env <- evBindIdSwizzle binds
|
|
|
451
|
+ = case go env ws of
|
|
|
452
|
+ WpLet {} : _ -> Nothing
|
|
|
453
|
+ ws' -> Just ws'
|
|
|
454
|
+ | otherwise
|
|
|
455
|
+ = Nothing
|
|
|
456
|
+ where
|
|
|
457
|
+ go :: IdEnv Id -> [HsWrapper] -> [HsWrapper]
|
|
|
458
|
+ go env (WpTyApp ty : ws') = WpTyApp ty : go env ws'
|
|
|
459
|
+ go env (WpCast co : ws') = WpCast co : go env ws'
|
|
|
460
|
+ go env (WpTyLam tv : ws')
|
|
|
461
|
+ | not (tv_captures env tv)
|
|
|
462
|
+ = WpTyLam tv : go env ws'
|
|
|
463
|
+
|
|
|
464
|
+ go env (WpEvLam ev : ws')
|
|
|
465
|
+ | not (ev `elemVarEnv` env) -- `ev` must not be in the domain
|
|
|
466
|
+ , not (anyVarEnv (== ev) env) -- or range of `env`
|
|
|
467
|
+ = WpEvLam ev : go env ws'
|
|
|
468
|
+
|
|
|
469
|
+ go env (WpEvApp (EvExpr (Var v)) : ws')
|
|
|
470
|
+ | Just v' <- swizzleId env v
|
|
|
471
|
+ = WpEvApp (EvExpr (Var v')) : go env ws'
|
|
|
472
|
+
|
|
|
473
|
+ go _ ws = WpLet tc_ev_binds : ws
|
|
|
474
|
+
|
|
|
475
|
+ tv_captures :: IdEnv Id -> TyVar -> Bool
|
|
|
476
|
+ tv_captures env tv = anyVarEnv bad env
|
|
|
477
|
+ where
|
|
|
478
|
+ bad id = anyFreeVarsOfType (== tv) (idType id)
|
|
|
479
|
+
|
|
|
480
|
+
|
|
|
481
|
+swizzleId :: IdEnv Id -> Id -> Maybe Id
|
|
|
482
|
+-- Nothing <=> ran out of fuel
|
|
|
483
|
+-- Shoul
|
|
|
484
|
+swizzleId env v = go 100 v
|
|
|
485
|
+ where
|
|
|
486
|
+ go :: Int -> EvId -> Maybe EvId
|
|
|
487
|
+ go fuel v
|
|
|
488
|
+ | fuel == 0 = Nothing
|
|
|
489
|
+ | Just v' <- lookupVarEnv env v = go (fuel-1) v'
|
|
|
490
|
+ | otherwise = Just v
|
|
|
491
|
+
|
|
|
492
|
+evBindIdSwizzle :: Bag EvBind -> Maybe (IdEnv Id)
|
|
|
493
|
+evBindIdSwizzle evbs = foldl' do_one (Just emptyVarEnv) evbs
|
|
|
494
|
+ where
|
|
|
495
|
+ do_one :: Maybe (IdEnv Id) -> EvBind -> Maybe (IdEnv Id)
|
|
|
496
|
+ do_one Nothing _ = Nothing
|
|
|
497
|
+ do_one (Just swizzle) (EvBind {eb_lhs = bndr, eb_rhs = rhs})
|
|
|
498
|
+ = case rhs of
|
|
|
499
|
+ EvExpr (Var v) -> Just (extendVarEnv swizzle bndr v)
|
|
|
500
|
+ _ -> Nothing
|
|
434
|
501
|
|
|
435
|
502
|
{-
|
|
436
|
503
|
************************************************************************
|