Как я могу заставить мое правило уволиться?

Question

Я работаю над правилами объединения списков для fromListN в Data.Primitive.Array и я немного застрял. Функция выглядит так:

fromListNArray :: Int -> [a] -> Array a
fromListNArray !n l =
  createArray n fromListN_too_short $ \mi ->
    let go i (x:xs)
          | i < n = writeArray mi i x >> go (i+1) xs
          | otherwise = fromListN_too_long
        go i [] = unless (i == n) fromListN_too_short
     in go 0 l
{-# NOINLINE fromListNArray #-}

fromListN_too_short а также fromListN_too_long это просто сообщения об ошибках.

Мои правила переписывания

{-# RULES
"fromListNArray/foldr" [~1] forall n xs.
  fromListNArray n xs = createArray n fromListN_too_short $ \mary ->
    foldr (fillArray_go n mary) (fillArray_stop n) xs 0

"fillArrayN/list" [1] forall n mary xs i.
  foldr (fillArray_go n mary) (fillArray_stop n) xs i = fillArrayN n mary xs i
 #-}

где определены помощники

fillArrayN :: Int -> MutableArray s a -> [a] -> Int -> ST s ()
fillArrayN !n !mary xs0 !i0 = go i0 xs0
  where
    go i (x:xs)
      | i < n = writeArray mary i x >> go (i+1) xs
      | otherwise = fromListN_too_long
    go i [] = unless (i == n) fromListN_too_short
{-# NOINLINE fillArrayN #-}

fillArray_go :: Int
             -> MutableArray s a
             -> a
             -> (Int -> ST s ())
             -> Int
             -> ST s ()
fillArray_go !n !mary = \x r i ->
  if i < n
    then writeArray mary i x >> r (i + 1)
    else fromListN_too_long
{-# INLINE CONLIKE [0] fillArray_go #-}

fillArray_stop :: Int -> Int -> ST s ()
fillArray_stop !n = \i -> unless (i == n) fromListN_too_short
{-# INLINE [0] fillArray_stop #-}

Первое правило перезаписи, кажется, хорошо. Второе правило с обратной записью - это проблема. Я никогда не смогу заставить его выстрелить. Кто-нибудь может предложить предложение?

---

Примечание: я знаю, что могу просто слиться с build а также augment чтобы избежать необходимости писать обратно, но это... не очень хорошее зрелище.

Answer 1

Главная проблема - ошибка с моей стороны. В

"fillArrayN/list" [1] forall n mary xs i.
  foldr (fillArray_go n mary) (fillArray_stop n) xs i = fillArrayN n mary xs i

foldr является Data.Foldable.foldr, который является методом класса и поэтому не работает на LHS правила. Исправление этой проблемы заставляет правило обратной записи работать в простых случаях.

К сожалению, когда fromListNArray сливается с augment (что обычно происходит, когда оно применяется к добавленным спискам), правило не запускается по другой причине. GHC создает функцию для fillArray_go n maryи не вставляет это. Я до сих пор не понимаю, почему это происходит.