module Common.Once (once, oneTD, oneBU, fullTD, fullBU) where

import Common.Logic

once = somewhere

somewhere :: (Logic -> [Logic]) -> Logic -> [Logic]
somewhere f p = f p ++ one (somewhere f) p

oneTD :: (Logic -> [Logic]) -> Logic -> [Logic]
oneTD f p = f p +> one (oneTD f) p

oneBU :: (Logic -> [Logic]) -> Logic -> [Logic]
oneBU f p = one (oneBU f) p +> f p

fullTD :: (Logic -> [Logic]) -> Logic -> [Logic]
fullTD f p = [ p'' | p' <- f p, p'' <- full (fullTD f) p' ]

fullBU :: (Logic -> [Logic]) -> Logic -> [Logic]
fullBU f p = [ p'' | p' <- full (fullBU f) p, p'' <- f p' ] 

one :: (Logic -> [Logic]) -> Logic -> [Logic]
one f p = 
   case p of
      p :->:  q -> make (:->:  q) p ++ make (p :->:)  q
      p :<->: q -> make (:<->: q) p ++ make (p :<->:) q
      p :&&:  q -> make (:&&:  q) p ++ make (p :&&:)  q
      p :||:  q -> make (:||:  q) p ++ make (p :||:)  q
      Not p     -> make Not p
      _ -> []
 where
   make :: (Logic -> Logic) -> Logic -> [Logic]
   make g = map g . f

full :: (Logic -> [Logic]) -> Logic -> [Logic]
full f p = 
   case p of
      p :->:  q -> [ p' :->:  q' | p' <- f p, q' <- f q ] 
      p :<->: q -> [ p' :<->: q' | p' <- f p, q' <- f q ] 
      p :&&:  q -> [ p' :&&:  q' | p' <- f p, q' <- f q ] 
      p :||:  q -> [ p' :||:  q' | p' <- f p, q' <- f q ] 
      Not p     -> [ Not p'      | p' <- f p ] 
      _ -> [p]

(+>) :: [a] -> [a] -> [a]
[] +> ys = ys
xs +> _  = xs