Всякое разное про насыщение равенствами и графы. Не очень много.

[thesz]

Программа:
testEqXX x = eqB x x
boolNot x = case x of
True -> False
False -> True
eqB x y = case x of
True -> y
False -> boolNot y
Сейчас я пытаюсь упростить testEqXX. Из правил упрощения работает только применение абстракции - и то через пень-колоду, - когда f x заменяется на телоf[x]. В моём понимании, это означает, что мы должны взять кусок графа App (Abs var body) expr и заменить все ссылки на var в body на ссылку на expr.

Вот код правила:
applyAbs = equality "app abs" $ \apply -> do
-- MonadIO позволяет печатать всё, что нужно.
liftIO $ putStrLn $ "Apply maybe at "++show apply
-- у нас list monad, мы отваливаемся, если сравнение проваливается.
-- по идее, getValue должен возвратить все узлы, вместе с эквивалентно
-- преобразованными. То есть, правило выполнится для всех GApp,
-- что попали под руку.
app@(GApp func appExpr) <- getValue apply
liftIO $ putStrLn $ "Apply definitely is at "++show apply
-- получить все узлы, что используют наш apply.
applyUses <- getUses apply
liftIO $ putStrLn $ "Touching "++show applyUses
-- поднять их всех обратно на рассмотрение.
touch applyUses
f@(GLam _ var expr) <- getValue func
-- получить все узлы, что ссылаются на переменную.
varUses <- getUses var
forM varUses $ \use -> do -- добавить эквивалентно преобразованные узлы.
old <- getValue use
let new = changeRef var appExpr old
r <- valueRef new
recordTransform use r -- записать преобразование.
--liftIO $ putStrLn $ "Changed from "++show old++" to "++show new
return ()

(похоже, у меня тут где-то ошибка, но в качестве демонстрации вполне сойдёт)

Тут на картинке видно, как это работает. Внутри, в прямоугольнике-кластере initial мы имеем созданный по нашей исходной программе граф. Далее мы накатываем на него правила, получая другой граф, дополненный.

Пока у меня правила применяются один раз, почему-то, как раз занят выяснением, почему.

Картинка:


Для создания вложенных структур я воспользовался возможностью формата dot - если название подграфа начинается с cluster, то он оформляется в отдельный прямоугольничек. Для вот таких вложенных преобразований очень удобно.

Через некоторое время выложу исходники.