Explaining a part of https://github.com/effectfully/random-stuff/blob/master/AST_transformation_proofs.agda

IsMatching.hs

module IsMatching where

import Data.Function
import Data.List
import Data.Maybe

getSubterms :: (Integer -> Integer -> [Integer]) -> [Integer] -> Maybe (Integer, Integer)
getSubterms f xs =
  let subtermIndices =
        map (snd . head) . groupBy ((==) `on` fst) . sortBy (compare `on` fst) . catMaybes $
          zipWith3 (\i x y -> if x == y then Nothing else Just (x, i))
            [0..]
            (f 0 1)
            (f 2 3)
      subterms = map (xs !!) subtermIndices
  in case subterms of
        [x, y] -> Just (x, y)
        _      -> Nothing

isMatching :: (Integer -> Integer -> [Integer]) -> [Integer] -> Bool
isMatching f xs = case getSubterms f xs of
  Nothing     -> False
  Just (x, y) -> f x y == xs

example :: Integer -> Integer -> [Integer]
example a b = [4, a, b, 2, a]

-- >>> isMatching example [4, 3, 1, 2, 3]
-- True
-- >>> isMatching example [4, 3, 1, 2, 1]
-- False
-- >>> isMatching example [4, 3, 1, 2]
-- False
-- >>> isMatching example [4, 3, 1, 2, 3, 5]
-- False
-- >>> isMatching example [3, 1, 2, 3]
-- False

example' :: Integer -> Integer -> [Integer]
example' a b = [b, a, 4, 2, b]

-- >>> isMatching example' [3, 1, 4, 2, 3]
-- True
-- >>> isMatching example' [3, 1, 4, 2, 1]
-- False
-- >>> isMatching example' [3, 1, 4, 2]
-- False
-- >>> isMatching example' [3, 1, 4, 2, 3, 5]
-- False
-- >>> isMatching example' [1, 4, 2, 3]
-- False