{- |
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
