{- |
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
  { FoldRec a -> Program -> a
foldAbort :: Program -> a
  , FoldRec a -> Program -> a
foldSkip :: Program -> a
  , FoldRec a -> Program -> VAR -> TERM () -> a
foldAssign :: Program -> VAR -> TERM () -> a
  , FoldRec a -> Program -> FORMULA () -> a
foldCall :: Program -> FORMULA () -> a
  , FoldRec a -> Program -> TERM () -> a
foldReturn :: Program -> TERM () -> a
  , FoldRec a -> Program -> [VAR_DECL] -> a -> a
foldBlock :: Program -> [VAR_DECL] -> a -> a
  , FoldRec a -> Program -> a -> a -> a
foldSeq :: Program -> a -> a -> a
  , FoldRec a -> Program -> FORMULA () -> a -> a -> a
foldIf :: Program -> FORMULA () -> a -> a -> a
  , FoldRec a -> Program -> FORMULA () -> a -> a
foldWhile :: Program -> FORMULA () -> a -> a }

-- | fold function
foldProg :: FoldRec a -> Program -> a
foldProg :: FoldRec a -> Program -> a
foldProg r :: FoldRec a
r p :: Program
p = case Program -> PlainProgram
forall a. Ranged a -> a
unRanged Program
p of
  Abort -> FoldRec a -> Program -> a
forall a. FoldRec a -> Program -> a
foldAbort FoldRec a
r Program
p
  Skip -> FoldRec a -> Program -> a
forall a. FoldRec a -> Program -> a
foldSkip FoldRec a
r Program
p
  Assign v :: VAR
v t :: TERM ()
t -> FoldRec a -> Program -> VAR -> TERM () -> a
forall a. FoldRec a -> Program -> VAR -> TERM () -> a
foldAssign FoldRec a
r Program
p VAR
v TERM ()
t
  Call f :: FORMULA ()
f -> FoldRec a -> Program -> FORMULA () -> a
forall a. FoldRec a -> Program -> FORMULA () -> a
foldCall FoldRec a
r Program
p FORMULA ()
f
  Return t :: TERM ()
t -> FoldRec a -> Program -> TERM () -> a
forall a. FoldRec a -> Program -> TERM () -> a
foldReturn FoldRec a
r Program
p TERM ()
t
  Block vs :: [VAR_DECL]
vs q :: Program
q -> FoldRec a -> Program -> [VAR_DECL] -> a -> a
forall a. FoldRec a -> Program -> [VAR_DECL] -> a -> a
foldBlock FoldRec a
r Program
p [VAR_DECL]
vs (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ FoldRec a -> Program -> a
forall a. FoldRec a -> Program -> a
foldProg FoldRec a
r Program
q
  Seq p1 :: Program
p1 p2 :: Program
p2 -> FoldRec a -> Program -> a -> a -> a
forall a. FoldRec a -> Program -> a -> a -> a
foldSeq FoldRec a
r Program
p (FoldRec a -> Program -> a
forall a. FoldRec a -> Program -> a
foldProg FoldRec a
r Program
p1) (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ FoldRec a -> Program -> a
forall a. FoldRec a -> Program -> a
foldProg FoldRec a
r Program
p2
  If f :: FORMULA ()
f p1 :: Program
p1 p2 :: Program
p2 -> FoldRec a -> Program -> FORMULA () -> a -> a -> a
forall a. FoldRec a -> Program -> FORMULA () -> a -> a -> a
foldIf FoldRec a
r Program
p FORMULA ()
f (FoldRec a -> Program -> a
forall a. FoldRec a -> Program -> a
foldProg FoldRec a
r Program
p1) (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ FoldRec a -> Program -> a
forall a. FoldRec a -> Program -> a
foldProg FoldRec a
r Program
p2
  While f :: FORMULA ()
f q :: Program
q -> FoldRec a -> Program -> FORMULA () -> a -> a
forall a. FoldRec a -> Program -> FORMULA () -> a -> a
foldWhile FoldRec a
r Program
p FORMULA ()
f (a -> a) -> a -> a
forall a b. (a -> b) -> a -> b
$ FoldRec a -> Program -> a
forall a. FoldRec a -> Program -> a
foldProg FoldRec a
r Program
q

mapRec :: FoldRec Program
mapRec :: FoldRec Program
mapRec = FoldRec :: forall a.
(Program -> a)
-> (Program -> a)
-> (Program -> VAR -> TERM () -> a)
-> (Program -> FORMULA () -> a)
-> (Program -> TERM () -> a)
-> (Program -> [VAR_DECL] -> a -> a)
-> (Program -> a -> a -> a)
-> (Program -> FORMULA () -> a -> a -> a)
-> (Program -> FORMULA () -> a -> a)
-> FoldRec a
FoldRec
  { foldAbort :: Program -> Program
foldAbort = Program -> Program
forall a. a -> a
id
  , foldSkip :: Program -> Program
foldSkip = Program -> Program
forall a. a -> a
id
  , foldAssign :: Program -> VAR -> TERM () -> Program
foldAssign = \ (Ranged _ r :: Range
r) v :: VAR
v t :: TERM ()
t -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (VAR -> TERM () -> PlainProgram
Assign VAR
v TERM ()
t) Range
r
  , foldCall :: Program -> FORMULA () -> Program
foldCall = \ (Ranged _ r :: Range
r) f :: FORMULA ()
f -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> PlainProgram
Call FORMULA ()
f) Range
r
  , foldReturn :: Program -> TERM () -> Program
foldReturn = \ (Ranged _ r :: Range
r) t :: TERM ()
t -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (TERM () -> PlainProgram
Return TERM ()
t) Range
r
  , foldBlock :: Program -> [VAR_DECL] -> Program -> Program
foldBlock = \ (Ranged _ r :: Range
r) vs :: [VAR_DECL]
vs p :: Program
p -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged ([VAR_DECL] -> Program -> PlainProgram
Block [VAR_DECL]
vs Program
p) Range
r
  , foldSeq :: Program -> Program -> Program -> Program
foldSeq = \ (Ranged _ r :: Range
r) p1 :: Program
p1 p2 :: Program
p2 -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (Program -> Program -> PlainProgram
Seq Program
p1 Program
p2) Range
r
  , foldIf :: Program -> FORMULA () -> Program -> Program -> Program
foldIf = \ (Ranged _ r :: Range
r) c :: FORMULA ()
c p1 :: Program
p1 p2 :: Program
p2 -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> Program -> Program -> PlainProgram
If FORMULA ()
c Program
p1 Program
p2) Range
r
  , foldWhile :: Program -> FORMULA () -> Program -> Program
foldWhile = \ (Ranged _ r :: Range
r) c :: FORMULA ()
c p :: Program
p -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> Program -> PlainProgram
While FORMULA ()
c Program
p) Range
r }

mapProg :: (TERM () -> TERM ()) -> (FORMULA () -> FORMULA ())
        -> FoldRec Program
mapProg :: (TERM () -> TERM ())
-> (FORMULA () -> FORMULA ()) -> FoldRec Program
mapProg mt :: TERM () -> TERM ()
mt mf :: FORMULA () -> FORMULA ()
mf = FoldRec Program
mapRec
  { foldAssign :: Program -> VAR -> TERM () -> Program
foldAssign = \ (Ranged _ r :: Range
r) v :: VAR
v t :: TERM ()
t -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (VAR -> TERM () -> PlainProgram
Assign VAR
v (TERM () -> PlainProgram) -> TERM () -> PlainProgram
forall a b. (a -> b) -> a -> b
$ TERM () -> TERM ()
mt TERM ()
t) Range
r
  , foldCall :: Program -> FORMULA () -> Program
foldCall = \ (Ranged _ r :: Range
r) f :: FORMULA ()
f -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> PlainProgram
Call (FORMULA () -> PlainProgram) -> FORMULA () -> PlainProgram
forall a b. (a -> b) -> a -> b
$ FORMULA () -> FORMULA ()
mf FORMULA ()
f) Range
r
  , foldReturn :: Program -> TERM () -> Program
foldReturn = \ (Ranged _ r :: Range
r) t :: TERM ()
t -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (TERM () -> PlainProgram
Return (TERM () -> PlainProgram) -> TERM () -> PlainProgram
forall a b. (a -> b) -> a -> b
$ TERM () -> TERM ()
mt TERM ()
t) Range
r
  , foldIf :: Program -> FORMULA () -> Program -> Program -> Program
foldIf = \ (Ranged _ r :: Range
r) c :: FORMULA ()
c p1 :: Program
p1 p2 :: Program
p2 -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> Program -> Program -> PlainProgram
If (FORMULA () -> FORMULA ()
mf FORMULA ()
c) Program
p1 Program
p2) Range
r
  , foldWhile :: Program -> FORMULA () -> Program -> Program
foldWhile = \ (Ranged _ r :: Range
r) c :: FORMULA ()
c p :: Program
p -> PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged (FORMULA () -> Program -> PlainProgram
While (FORMULA () -> FORMULA ()
mf FORMULA ()
c) Program
p) Range
r }

-- | collect i.e. variables to be universally bound on the top level
constProg :: (TERM () -> a) -> (FORMULA () -> a) -> ([a] -> a) -> a -> FoldRec a
constProg :: (TERM () -> a) -> (FORMULA () -> a) -> ([a] -> a) -> a -> FoldRec a
constProg ft :: TERM () -> a
ft ff :: FORMULA () -> a
ff join :: [a] -> a
join c :: a
c = FoldRec :: forall a.
(Program -> a)
-> (Program -> a)
-> (Program -> VAR -> TERM () -> a)
-> (Program -> FORMULA () -> a)
-> (Program -> TERM () -> a)
-> (Program -> [VAR_DECL] -> a -> a)
-> (Program -> a -> a -> a)
-> (Program -> FORMULA () -> a -> a -> a)
-> (Program -> FORMULA () -> a -> a)
-> FoldRec a
FoldRec
  { foldAbort :: Program -> a
foldAbort = a -> Program -> a
forall a b. a -> b -> a
const a
c
  , foldSkip :: Program -> a
foldSkip = a -> Program -> a
forall a b. a -> b -> a
const a
c
  , foldAssign :: Program -> VAR -> TERM () -> a
foldAssign = \ _ _ t :: TERM ()
t -> TERM () -> a
ft TERM ()
t
  , foldCall :: Program -> FORMULA () -> a
foldCall = \ _ f :: FORMULA ()
f -> FORMULA () -> a
ff FORMULA ()
f
  , foldReturn :: Program -> TERM () -> a
foldReturn = \ _ t :: TERM ()
t -> TERM () -> a
ft TERM ()
t
  , foldBlock :: Program -> [VAR_DECL] -> a -> a
foldBlock = \ _ _ p :: a
p -> a
p
  , foldSeq :: Program -> a -> a -> a
foldSeq = \ _ p1 :: a
p1 p2 :: a
p2 -> [a] -> a
join [a
p1, a
p2]
  , foldIf :: Program -> FORMULA () -> a -> a -> a
foldIf = \ _ f :: FORMULA ()
f p1 :: a
p1 p2 :: a
p2 -> [a] -> a
join [FORMULA () -> a
ff FORMULA ()
f, a
p1, a
p2]
  , foldWhile :: Program -> FORMULA () -> a -> a
foldWhile = \ _ f :: FORMULA ()
f p :: a
p -> [a] -> a
join [FORMULA () -> a
ff FORMULA ()
f, a
p] }

progToSetRec :: Ord a => (TERM () -> Set.Set a) -> (FORMULA () -> Set.Set a)
             -> FoldRec (Set.Set a)
progToSetRec :: (TERM () -> Set a) -> (FORMULA () -> Set a) -> FoldRec (Set a)
progToSetRec ft :: TERM () -> Set a
ft ff :: FORMULA () -> Set a
ff = (TERM () -> Set a)
-> (FORMULA () -> Set a)
-> ([Set a] -> Set a)
-> Set a
-> FoldRec (Set a)
forall a.
(TERM () -> a) -> (FORMULA () -> a) -> ([a] -> a) -> a -> FoldRec a
constProg TERM () -> Set a
ft FORMULA () -> Set a
ff [Set a] -> Set a
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions Set a
forall a. Set a
Set.empty