replaceVariable :: ( OpenAlg xs "atomF" AtomF (OpenADT xs)
, (ApplyRow (OpenADT xs) xs .- "atomF") ~ ApplyRow (OpenADT xs) (xs .- "atomF")
, ((xs .- "atomF") .\/ 'R '["atomF" ':-> AtomF]) ~ xs
, (ApplyRow (OpenADT xs) (xs .- "atomF") .\/ 'R '["atomF" ':-> AtomF (Fix (VarF xs))])
~ ApplyRow (OpenADT xs) xs
, (Forall (xs .- "atomF") Functor)
)
=> Text -> Term -> OpenADT xs -> OpenADT xs
replaceVariable variable value formula =
case trialF (unfix formula) #atomF of
Right other -> other & (fmap (replaceVariable variable value)) & diversifyF @("atomF" .== AtomF) & Fix
Left (AtomF' α name terms) -> Atom α name $ fmap go terms
where go t =
case t of
GText text -> if text == variable then value else t
_ -> t
Some of the constraints in the signature seem to be stating the obvious.