findNode :: [G S] -> ConsPDTree -> ([G S], ConsPDTree)
findNode v tree =
    let nodes = go tree in
    -- trace (printf "\n\nNodes\n%s\n\n" (show nodes)) $
    case find nontrivial nodes of
      Just n -> (v, restrictSubsts $ simplify $ renameAmbigousVars n)
      Nothing -> error $ printf "Residualization error: no node for\n%s" (show v)
  where
    go node@(Or _ (Descend goal _) _) | goal == v = return node
    go node@(Conj _ goal _)           | goal == v = return node
    go node@(Split _ goal _)          | goal == v = return node
    go node@(Gen ch _ goal _ _)       | goal == v = [node, ch]
    go node@(Or _ (Descend goal _) _) | goal `isVariant` v = return node
    go node@(Conj _ goal _)           | goal `isVariant` v = return node
    go node@(Split _ goal _)          | goal `isVariant` v = return node
    go node@(Gen ch _ goal _ _)       | goal `isVariant` v = [node, ch]
    go (Or ch _ _)                    = concatMap go ch
    go (Conj ch _ _)                  = concatMap go ch
    go (Split ch _ _)                 = concatMap go ch
    go (Gen ch _ _ _ _)               = go ch
    go _                              = []
findNode :: [G S] -> ConsPDTree -> ([G S], ConsPDTree)
findNode v tree =
    let nodes = go tree in
    -- trace (printf "\n\nNodes\n%s\n\n" (show nodes)) $
    case find nontrivial nodes of
      Just n -> (v, restrictSubsts $ simplify $ renameAmbigousVars n)
      Nothing -> error $ printf "Residualization error: no node for\n%s" (show v)
  where
    go node@(Or _ (Descend goal _) _) | goal == v = return node
    go node@(Conj _ goal _)           | goal == v = return node
    go node@(Split _ goal _)          | goal == v = return node
    go node@(Gen ch _ goal _ _)       | goal == v = [node, ch]
    go node@(Or _ (Descend goal _) _) | goal `isVariant` v = return node
    go node@(Conj _ goal _)           | goal `isVariant` v = return node
    go node@(Split _ goal _)          | goal `isVariant` v = return node
    go node@(Gen ch _ goal _ _)       | goal `isVariant` v = [node, ch]
    go (Or ch _ _)                    = concatMap go ch
    go (Conj ch _ _)                  = concatMap go ch
    go (Split ch _ _)                 = concatMap go ch
    go (Gen ch _ _ _ _)               = go ch
    go _                              = []
findNode v tree =
    let nodes = go tree in
    -- trace (printf "\n\nNodes\n%s\n\n" (show nodes)) $
    case find nontrivial nodes of
      Just n -> (v, restrictSubsts $ simplify $ renameAmbigousVars n)
      Nothing -> error $ printf "Residualization error: no node for\n%s" (show v)
  where
    go node@(Or _ (Descend goal _) _) | goal == v = return node
    go node@(Conj _ goal _)           | goal == v = return node
    go node@(Split _ goal _)          | goal == v = return node
    go node@(Gen ch _ goal _ _)       | goal == v = [node, ch]
    go node@(Or _ (Descend goal _) _) | goal `isVariant` v = return node
    go node@(Conj _ goal _)           | goal `isVariant` v = return node
    go node@(Split _ goal _)          | goal `isVariant` v = return node
    go node@(Gen ch _ goal _ _)       | goal `isVariant` v = [node, ch]
    go (Or ch _ _)                    = concatMap go ch
    go (Conj ch _ _)                  = concatMap go ch
    go (Split ch _ _)                 = concatMap go ch
    go (Gen ch _ _ _ _)               = go ch
    go _                              = []