Transformation.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
4673N/A{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
4673N/A{- |
4673N/AModule : ./CSL/Transformation.hs
4673N/ADescription : Program transformations
4673N/ACopyright : (c) Ewaryst Schulz, DFKI Bremen 2010
4673N/ALicense : GPLv2 or higher, see LICENSE.txt
4673N/A
4673N/AMaintainer : ewaryst.schulz@dfki.de
4673N/AStability : experimental
4673N/APortability : non-portable (various glasgow extensions)
6982N/A
6982N/AProgram transformations from CSL specifications to CAS programs
4673N/Aand utilities for lemma generation
4673N/A
4673N/A-}
4673N/A
6982N/Amodule CSL.Transformation where
6982N/A
6982N/Aimport Control.Monad.State (State, StateT (..), MonadState (get, put))
6982N/Aimport Control.Monad.Trans (lift)
4673N/Aimport Prelude hiding (lookup)
4673N/A
4673N/Aimport CSL.AS_BASIC_CSL
4673N/Aimport CSL.ASUtils
4673N/Aimport Common.Id
5821N/A
4673N/A{- ----------------------------------------------------------------------
4673N/ADatatypes and Classes for Term- and Program Transformations
4673N/A---------------------------------------------------------------------- -}
4673N/A
4673N/A
4673N/AmkOperator :: String -> [EXTPARAM] -> [EXPRESSION] -> Range -> EXPRESSION
4673N/AmkOperator = mkAndAnalyzeOp ()
4673N/A
4673N/A-- | A class to abstract from the concrete variable generation facility
4673N/Aclass Monad m => VarGen m where
4673N/A genVar :: m String
4673N/A
4673N/Ainstance VarGen (State Int) where
4673N/A genVar = do
4673N/A i <- get
4673N/A put $ i + 1
4673N/A return $ "gv" ++ show i
4673N/A
4673N/Ainstance VarGen (State (Int, String)) where
4673N/A genVar = do
4673N/A (i, s) <- get
4673N/A put (i + 1, s)
4673N/A return $ s ++ show i
4673N/A
4673N/Ainstance VarGen m => VarGen (StateT s m) where
4673N/A genVar = lift genVar
4673N/A
4673N/A
4673N/A-- | A class to construct EXPRESSIONs from simple tuple structures
4865N/Aclass SExp a where
4673N/A toExp :: a -> EXPRESSION
4673N/A
4673N/Aclass SOp a where
4673N/A toOp :: a -> OpDecl
4865N/A
4673N/Ainstance SExp EXPRESSION where
4673N/A toExp e = e
4673N/A
4673N/Ainstance SExp APInt where
4865N/A toExp i = Int i nullRange
4673N/A
4673N/Ainstance SExp APFloat where
4673N/A toExp f = Rat f nullRange
4673N/A
4673N/Ainstance SExp String where
4673N/A toExp s = mkOperator s [] [] nullRange
4673N/A
4673N/Ainstance SOp String where
4673N/A toOp s = OpDecl (SimpleConstant s) [] [] nullRange
4673N/A
4865N/Ainstance SExp OPNAME where
4673N/A toExp n = mkPredefOp n []
4673N/A
4673N/Ainstance SExp ConstantName where
4673N/A toExp (SimpleConstant s) = mkOperator s [] [] nullRange
4865N/A toExp x = error $ "toExp: elim-constant not supported " ++ show x
4865N/A
4673N/Ainstance SExp a => SExp (String, a) where
4865N/A toExp (s, x) = mkOperator s [] [toExp x] nullRange
4865N/A
4865N/Ainstance SExp a => SExp (ConstantName, [a]) where
4865N/A toExp (n, l) = Op (OpUser n) [] (map toExp l) nullRange
4865N/A
4865N/Ainstance (SExp a, SExp b) => SExp (String, a, b) where
4865N/A toExp (s, x, y) = mkOperator s [] [toExp x, toExp y] nullRange
4865N/A
4865N/Ainstance (SExp a, SExp b, SExp c) => SExp (String, a, b, c) where
4865N/A toExp (s, x, y, z) =
4865N/A mkOperator s [] [toExp x, toExp y, toExp z] nullRange
4865N/A
4865N/A
4865N/A{- strangely, ghc says that we would have overlapping instances with
4865N/Ainstance SExp a => SExp (String, a), but I can't see it. I introduce
4865N/Athis strange looking instance -}
4865N/Ainstance (SExp a) => SExp ((), String, [a]) where
4865N/A toExp (_, s, l) = mkOperator s [] (map toExp l) nullRange
4865N/A
4673N/A-- | A class to construct CMDs from simple tuple structures
4673N/Aclass SCmd a where
4673N/A toCmd :: a -> CMD
4673N/A
4673N/Ainstance (SExp a, SExp b) => SCmd (String, a, b) where
4673N/A toCmd (s, x, y) = Cmd s [toExp x, toExp y]
4673N/A
4865N/Ainstance (SOp a, SExp b) => SCmd (a, b) where
4673N/A toCmd (x, y) = Ass (toOp x) $ toExp y
4673N/A
4865N/Aclass IntervalLike a where
4865N/A toIntervalExp :: a -> EXPRESSION
4865N/A
4673N/Ainstance IntervalLike EXPRESSION where
4865N/A toIntervalExp = id
4865N/A
4865N/Ainstance IntervalLike (Double, Double) where
4865N/A toIntervalExp (a, b) = Interval a b nullRange
4673N/A