3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
116546d9eacf9c9629d6360bc010dd6143725186Ewaryst SchulzDescription : Program transformations
116546d9eacf9c9629d6360bc010dd6143725186Ewaryst SchulzCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
116546d9eacf9c9629d6360bc010dd6143725186Ewaryst SchulzMaintainer : ewaryst.schulz@dfki.de
116546d9eacf9c9629d6360bc010dd6143725186Ewaryst SchulzStability : experimental
62281905648914793072631d80b66789d94156e9Ewaryst SchulzPortability : non-portable (various glasgow extensions)
116546d9eacf9c9629d6360bc010dd6143725186Ewaryst SchulzProgram transformations from CSL specifications to CAS programs
ce4924a895ca1c5859c24f5523d1e167fa04094aEwaryst Schulzand utilities for lemma generation
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Control.Monad.State (State, StateT (..), MonadState (get, put))
baec30a71697583b5e73008fb17c2563da2830f5Ewaryst Schulzimport Prelude hiding (lookup)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederDatatypes and Classes for Term- and Program Transformations
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------------------------------------------------------- -}
7b4b3c800d82cbdef5ce44d26e3037c714b03c07Ewaryst SchulzmkOperator :: String -> [EXTPARAM] -> [EXPRESSION] -> Range -> EXPRESSION
ee3bb87ab2da52ee1ad0c6675ea8b699b0af9ddcEwaryst SchulzmkOperator = mkAndAnalyzeOp ()
3ca65516621518fb1295bfac8da689233ba38772Ewaryst Schulz-- | A class to abstract from the concrete variable generation facility
ce4924a895ca1c5859c24f5523d1e167fa04094aEwaryst Schulzclass Monad m => VarGen m where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder genVar :: m String
ce4924a895ca1c5859c24f5523d1e167fa04094aEwaryst Schulzinstance VarGen (State Int) where
ce4924a895ca1c5859c24f5523d1e167fa04094aEwaryst Schulz return $ "gv" ++ show i
ce4924a895ca1c5859c24f5523d1e167fa04094aEwaryst Schulzinstance VarGen (State (Int, String)) where
ce4924a895ca1c5859c24f5523d1e167fa04094aEwaryst Schulz (i, s) <- get
ce4924a895ca1c5859c24f5523d1e167fa04094aEwaryst Schulz return $ s ++ show i
bb2619647109faecd1613f1a7bd45ce0cbe6662eEwaryst Schulzinstance VarGen m => VarGen (StateT s m) where
bb2619647109faecd1613f1a7bd45ce0cbe6662eEwaryst Schulz genVar = lift genVar
3ca65516621518fb1295bfac8da689233ba38772Ewaryst Schulz-- | A class to construct EXPRESSIONs from simple tuple structures
116546d9eacf9c9629d6360bc010dd6143725186Ewaryst Schulzclass SExp a where
116546d9eacf9c9629d6360bc010dd6143725186Ewaryst Schulz toExp :: a -> EXPRESSION
76408af596b604997cabe1ebde1caaa43f58b1e6Ewaryst Schulzclass SOp a where
76408af596b604997cabe1ebde1caaa43f58b1e6Ewaryst Schulz toOp :: a -> OpDecl
3ca65516621518fb1295bfac8da689233ba38772Ewaryst Schulzinstance SExp EXPRESSION where
ce4924a895ca1c5859c24f5523d1e167fa04094aEwaryst Schulzinstance SExp APInt where
116546d9eacf9c9629d6360bc010dd6143725186Ewaryst Schulz toExp i = Int i nullRange
ce4924a895ca1c5859c24f5523d1e167fa04094aEwaryst Schulzinstance SExp APFloat where
213ff2bc64713dccda8de3db300ba188bd585866Ewaryst Schulz toExp f = Rat f nullRange
116546d9eacf9c9629d6360bc010dd6143725186Ewaryst Schulzinstance SExp String where
7b4b3c800d82cbdef5ce44d26e3037c714b03c07Ewaryst Schulz toExp s = mkOperator s [] [] nullRange
76408af596b604997cabe1ebde1caaa43f58b1e6Ewaryst Schulzinstance SOp String where
76408af596b604997cabe1ebde1caaa43f58b1e6Ewaryst Schulz toOp s = OpDecl (SimpleConstant s) [] [] nullRange
213ff2bc64713dccda8de3db300ba188bd585866Ewaryst Schulzinstance SExp OPNAME where
213ff2bc64713dccda8de3db300ba188bd585866Ewaryst Schulz toExp n = mkPredefOp n []
25ae784bc2e848d6c2d53de84b4236449857e4ccEwaryst Schulzinstance SExp ConstantName where
7b4b3c800d82cbdef5ce44d26e3037c714b03c07Ewaryst Schulz toExp (SimpleConstant s) = mkOperator s [] [] nullRange
25ae784bc2e848d6c2d53de84b4236449857e4ccEwaryst Schulz toExp x = error $ "toExp: elim-constant not supported " ++ show x
116546d9eacf9c9629d6360bc010dd6143725186Ewaryst Schulzinstance SExp a => SExp (String, a) where
7b4b3c800d82cbdef5ce44d26e3037c714b03c07Ewaryst Schulz toExp (s, x) = mkOperator s [] [toExp x] nullRange
819c43ddaab748a3668c192fb2d1f70070dced59Ewaryst Schulzinstance SExp a => SExp (ConstantName, [a]) where
819c43ddaab748a3668c192fb2d1f70070dced59Ewaryst Schulz toExp (n, l) = Op (OpUser n) [] (map toExp l) nullRange
116546d9eacf9c9629d6360bc010dd6143725186Ewaryst Schulzinstance (SExp a, SExp b) => SExp (String, a, b) where
7b4b3c800d82cbdef5ce44d26e3037c714b03c07Ewaryst Schulz toExp (s, x, y) = mkOperator s [] [toExp x, toExp y] nullRange
3ca65516621518fb1295bfac8da689233ba38772Ewaryst Schulzinstance (SExp a, SExp b, SExp c) => SExp (String, a, b, c) where
2acb7fe145aa2e45c4c75ab76d380d3322850031Ewaryst Schulz toExp (s, x, y, z) =
7b4b3c800d82cbdef5ce44d26e3037c714b03c07Ewaryst Schulz mkOperator s [] [toExp x, toExp y, toExp z] nullRange
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- strangely, ghc says that we would have overlapping instances with
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance SExp a => SExp (String, a), but I can't see it. I introduce
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederthis strange looking instance -}
62281905648914793072631d80b66789d94156e9Ewaryst Schulzinstance (SExp a) => SExp ((), String, [a]) where
7b4b3c800d82cbdef5ce44d26e3037c714b03c07Ewaryst Schulz toExp (_, s, l) = mkOperator s [] (map toExp l) nullRange
3ca65516621518fb1295bfac8da689233ba38772Ewaryst Schulz-- | A class to construct CMDs from simple tuple structures
3ca65516621518fb1295bfac8da689233ba38772Ewaryst Schulzclass SCmd a where
3ca65516621518fb1295bfac8da689233ba38772Ewaryst Schulz toCmd :: a -> CMD
3ca65516621518fb1295bfac8da689233ba38772Ewaryst Schulzinstance (SExp a, SExp b) => SCmd (String, a, b) where
3ca65516621518fb1295bfac8da689233ba38772Ewaryst Schulz toCmd (s, x, y) = Cmd s [toExp x, toExp y]
76408af596b604997cabe1ebde1caaa43f58b1e6Ewaryst Schulzinstance (SOp a, SExp b) => SCmd (a, b) where
76408af596b604997cabe1ebde1caaa43f58b1e6Ewaryst Schulz toCmd (x, y) = Ass (toOp x) $ toExp y
62281905648914793072631d80b66789d94156e9Ewaryst Schulzclass IntervalLike a where
62281905648914793072631d80b66789d94156e9Ewaryst Schulz toIntervalExp :: a -> EXPRESSION
62281905648914793072631d80b66789d94156e9Ewaryst Schulzinstance IntervalLike EXPRESSION where
62281905648914793072631d80b66789d94156e9Ewaryst Schulz toIntervalExp = id
213ff2bc64713dccda8de3db300ba188bd585866Ewaryst Schulzinstance IntervalLike (Double, Double) where
62281905648914793072631d80b66789d94156e9Ewaryst Schulz toIntervalExp (a, b) = Interval a b nullRange