content: {- |
  Module      :  ./VSE/Fold.hs
  Description :  folding functions for VSE progams
  Copyright   :  (c) Christian Maeder, DFKI Bremen 2008
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  folding functions for VSE progams
  -}
  
  module VSE.Fold where
  
  import qualified Data.Set as Set
  import CASL.AS_Basic_CASL
  import VSE.As
  
  -- | fold record
  data FoldRec a = FoldRec
    { foldAbort :: Program -> a
    , foldSkip :: Program -> a
    , foldAssign :: Program -> VAR -> TERM () -> a
    , foldCall :: Program -> FORMULA () -> a
    , foldReturn :: Program -> TERM () -> a
    , foldBlock :: Program -> [VAR_DECL] -> a -> a
    , foldSeq :: Program -> a -> a -> a
    , foldIf :: Program -> FORMULA () -> a -> a -> a
    , foldWhile :: Program -> FORMULA () -> a -> a }
  
  -- | fold function
  foldProg :: FoldRec a -> Program -> a
  foldProg r p = case unRanged p of
    Abort -> foldAbort r p
    Skip -> foldSkip r p
    Assign v t -> foldAssign r p v t
    Call f -> foldCall r p f
    Return t -> foldReturn r p t
    Block vs q -> foldBlock r p vs $ foldProg r q
    Seq p1 p2 -> foldSeq r p (foldProg r p1) $ foldProg r p2
    If f p1 p2 -> foldIf r p f (foldProg r p1) $ foldProg r p2
    While f q -> foldWhile r p f $ foldProg r q
  
  mapRec :: FoldRec Program
  mapRec = FoldRec
    { foldAbort = id
    , foldSkip = id
    , foldAssign = \ (Ranged _ r) v t -> Ranged (Assign v t) r
    , foldCall = \ (Ranged _ r) f -> Ranged (Call f) r
    , foldReturn = \ (Ranged _ r) t -> Ranged (Return t) r
    , foldBlock = \ (Ranged _ r) vs p -> Ranged (Block vs p) r
    , foldSeq = \ (Ranged _ r) p1 p2 -> Ranged (Seq p1 p2) r
    , foldIf = \ (Ranged _ r) c p1 p2 -> Ranged (If c p1 p2) r
    , foldWhile = \ (Ranged _ r) c p -> Ranged (While c p) r }
  
  mapProg :: (TERM () -> TERM ()) -> (FORMULA () -> FORMULA ())
          -> FoldRec Program
  mapProg mt mf = mapRec
    { foldAssign = \ (Ranged _ r) v t -> Ranged (Assign v $ mt t) r
    , foldCall = \ (Ranged _ r) f -> Ranged (Call $ mf f) r
    , foldReturn = \ (Ranged _ r) t -> Ranged (Return $ mt t) r
    , foldIf = \ (Ranged _ r) c p1 p2 -> Ranged (If (mf c) p1 p2) r
    , foldWhile = \ (Ranged _ r) c p -> Ranged (While (mf c) p) r }
  
  -- | collect i.e. variables to be universally bound on the top level
  constProg :: (TERM () -> a) -> (FORMULA () -> a) -> ([a] -> a) -> a -> FoldRec a
  constProg ft ff join c = FoldRec
    { foldAbort = const c
    , foldSkip = const c
    , foldAssign = \ _ _ t -> ft t
    , foldCall = \ _ f -> ff f
    , foldReturn = \ _ t -> ft t
    , foldBlock = \ _ _ p -> p
    , foldSeq = \ _ p1 p2 -> join [p1, p2]
    , foldIf = \ _ f p1 p2 -> join [ff f, p1, p2]
    , foldWhile = \ _ f p -> join [ff f, p] }
  
  progToSetRec :: Ord a => (TERM () -> Set.Set a) -> (FORMULA () -> Set.Set a)
               -> FoldRec (Set.Set a)
  progToSetRec ft ff = constProg ft ff Set.unions Set.empty
  