1
1
mirror of https://github.com/github/semantic.git synced 2024-12-26 08:25:19 +03:00

Turn the wheel to maximum fastness.

This commit is contained in:
Rob Rix 2019-06-28 13:15:05 -04:00
parent bc2c536822
commit 30873a7762
No known key found for this signature in database
GPG Key ID: F188A01508EA1CF7

View File

@ -255,14 +255,14 @@ efold :: forall l m n z b
-> Core (l b) -> Core (l b)
-> n (z b) -> n (z b)
efold var let' seq' lam app unit bool if' string load edge frame dot assign ann k = eiter var alg efold var let' seq' lam app unit bool if' string load edge frame dot assign ann k = eiter var alg
where alg :: forall x l' c z' . Functor c => (forall l'' z'' x . (l'' x -> m (z'' x)) -> c (l'' x) -> n (z'' x)) -> (l' x -> m (z' x)) -> CoreF c (l' x) -> n (z' x) where alg :: forall x l' c z' . (forall a b . Coercible a b => Coercible (c a) (c b)) => (forall l'' z'' x . (l'' x -> m (z'' x)) -> c (l'' x) -> n (z'' x)) -> (l' x -> m (z' x)) -> CoreF c (l' x) -> n (z' x)
alg go h = \case alg go h = \case
LetF a -> let' a LetF a -> let' a
a :>>$ b -> go h a `seq'` go h b a :>>$ b -> go h a `seq'` go h b
LamF b -> lam (coerce (go LamF b -> lam (coerce (go
(coerce (k . fmap (go h)) (coerce (k . fmap (go h))
:: ((Incr :.: c :.: l') x -> m ((Incr :.: n :.: z') x))) :: ((Incr :.: c :.: l') x -> m ((Incr :.: n :.: z') x)))
(fmap coerce b))) -- FIXME: can we avoid this fmap and just coerce harder? (coerce b)))
a :$$ b -> go h a `app` go h b a :$$ b -> go h a `app` go h b
UnitF -> unit UnitF -> unit
BoolF b -> bool b BoolF b -> bool b
@ -278,7 +278,7 @@ efold var let' seq' lam app unit bool if' string load edge frame dot assign ann
-- | Efficient Mendler-style iteration. -- | Efficient Mendler-style iteration.
eiter :: forall l m n z b eiter :: forall l m n z b
. (forall a . m a -> n a) . (forall a . m a -> n a)
-> (forall a l' c z' . Functor c => (forall l'' z'' x . (l'' x -> m (z'' x)) -> c (l'' x) -> n (z'' x)) -> (l' a -> m (z' a)) -> CoreF c (l' a) -> n (z' a)) -> (forall a l' c z' . (forall a b . Coercible a b => Coercible (c a) (c b)) => (forall l'' z'' x . (l'' x -> m (z'' x)) -> c (l'' x) -> n (z'' x)) -> (l' a -> m (z' a)) -> CoreF c (l' a) -> n (z' a))
-> (l b -> m (z b)) -> (l b -> m (z b))
-> Core (l b) -> Core (l b)
-> n (z b) -> n (z b)