5784N/A{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, TypeSynonymInstances, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
5784N/ADescription : Program transformations
5784N/ACopyright : (c) Ewaryst Schulz, DFKI Bremen 2010
5784N/AMaintainer : ewaryst.schulz@dfki.de
5784N/APortability : non-portable (various glasgow extensions)
5784N/AProgram transformations from CSL specifications to CAS programs
5784N/Aand utilities for lemma generation
5784N/Aimport Prelude hiding (lookup)
5784N/A-- ----------------------------------------------------------------------
5784N/A-- * Datatypes and Classes for Term- and Program Transformations
5784N/A-- ----------------------------------------------------------------------
5784N/A-- | A class to abstract from the concrete variable generation facility
5784N/Aclass Monad m => VarGen m where
5784N/Ainstance VarGen (State Int) where
5784N/Ainstance VarGen (State (Int, String)) where
5784N/Ainstance VarGen m => VarGen (StateT s m) where
5784N/A-- | A class to construct EXPRESSIONs from simple tuple structures
5784N/Ainstance SExp EXPRESSION where
5784N/A toExp f = Double f nullRange
5784N/A toExp s = Op s [] [] nullRange
5784N/Ainstance SExp a => SExp (String, a) where
5784N/A toExp (s, x) = Op s [] [toExp x] nullRange
5784N/Ainstance (SExp a, SExp b) => SExp (String, a, b) where
5784N/A toExp (s, x, y) = Op s [] [toExp x, toExp y] nullRange
5784N/Ainstance (SExp a, SExp b, SExp c) => SExp (String, a, b, c) where
5784N/A toExp (s, x, y, z) = Op s [] [toExp x, toExp y, toExp z] nullRange
5784N/A-- strangely, ghc says that we would have overlapping instances with
5784N/A-- instance SExp a => SExp (String, a), but I can't see it. I introduce
5784N/A-- this strange looking instance
5784N/Ainstance (SExp a) => SExp ((), String, [a]) where
5784N/A toExp (_, s, l) = Op s [] (map toExp l) nullRange
5784N/A-- | A class to construct CMDs from simple tuple structures
5784N/Ainstance (SExp a, SExp b) => SCmd (String, a, b) where
5784N/A toCmd (s, x, y) = Cmd s [toExp x, toExp y]
5784N/Ainstance (SExp a, SExp b) => SCmd (a, b) where
5784N/A toCmd (x, y) = Ass (toExp x) $ toExp y
5784N/Atype VarRange = (APFloat, APFloat)
5784N/A toIntervalExp :: a -> EXPRESSION
5784N/Ainstance IntervalLike EXPRESSION where
5784N/Ainstance IntervalLike VarRange where
5784N/A toIntervalExp (a, b) = Interval a b nullRange
5784N/A-- ----------------------------------------------------------------------
5784N/A-- * Transformations of assignments to conditional statements
5784N/A-- ----------------------------------------------------------------------
5784N/A-- ** A simple cache implemenation with variable container
5784N/A-- | We store all results from the backup lookup in the map, even the negative
5784N/A-- backupLookup is set once the data is created, the cachemap and varcontainer
5784N/Adata VCCache = VCCache { varcontainer ::
Map.Map String VarRange
5784N/A , cachemap ::
Map.Map String (Maybe EXPRESSION) } deriving Show
5784N/AlookupCached :: MonadState VCCache m => (String -> m (Maybe EXPRESSION)) -> String
5784N/AlookupCached = lookupCachedWithTrans return
5784N/AlookupCachedWithTrans :: MonadState VCCache m =>
5784N/A (EXPRESSION -> m EXPRESSION) -- ^ Transformation function
5784N/A -> (String -> m (Maybe EXPRESSION)) -- ^ lookup function
5784N/A -> m (Maybe EXPRESSION) -- ^ lookuped and transformed result
5784N/AlookupCachedWithTrans f lk k = do
5784N/A Just v -> f v >>= return . Just
5784N/A -- f can change the state, so read it again here!
5784N/AresetCache :: Monad m => VCCache -> m VCCache
5784N/A-- | Given a lookupfunction we initialize the VCCache
5784N/Aclass VariableContainer a b where
5784N/A insertVar :: String -> b -> a -> a
5784N/A toVarList :: a -> [(String, b)]
5784N/Ainstance VariableContainer VCCache VarRange where
5784N/A-- | If the state of a statemonad is a VariableContainer then we provide a
5784N/A-- simplified insert function, which hides the state handling
5784N/AinsertVarM :: (Monad m, VariableContainer a b) => String -> b -> StateT a m ()
5784N/AinsertVarM s iRng = fmap (insertVar s iRng) get >>= put
5784N/A-- | If the state of a statemonad is a VariableContainer then we provide a
5784N/A-- simplified insert function, which hides the state handling
5784N/AtoVarListM :: (VariableContainer a b, Monad m) => StateT a m [(String, b)]
5784N/AtoVarListM = fmap toVarList get
5784N/A-- | Given an expression containing intervals we code out the intervals
5784N/A-- replacing them by variables and assign to those variables ranges
5784N/A-- (the intervals). Does not replace toplevel intervals.
5784N/A (VarGen c, VariableContainer a VarRange, CalculationSystem c) =>
5784N/A EXPRESSION -> StateT a c EXPRESSION
5784N/AreplaceIntervals e@(Interval _ _ _) = return e
5784N/AreplaceIntervals e = replaceIntervals' e
5784N/A-- | Like replaceIntervals but works also on toplevel intervals
5784N/A (VarGen c, VariableContainer a VarRange, CalculationSystem c) =>
5784N/A EXPRESSION -> StateT a c EXPRESSION
5784N/A nargs <- mapM replaceIntervals' args
5784N/A nelms <- mapM replaceIntervals' elms
5784N/A-- | Replaces all occurrences of defined variables by their lookuped terms
5784N/AsubstituteDefined :: ( VarGen c, CalculationSystem c)
5784N/A => EXPRESSION -> StateT VCCache c EXPRESSION
5784N/A nargs <- mapM substituteDefined args
5784N/A mE <- lookupCachedWithTrans replaceIntervals lookup s
5784N/A Just (Interval from to _) ->
5784N/A -- enter the interval into the VariableContainer
5784N/A _ -> error "substituteDefined: defined constant not found"
5784N/A else return $ Op s epl nargs rg
5784N/A nelms <- mapM substituteDefined elms
5784N/AbuildConditionalExpression :: VCCache -> EXPRESSION -> EXPRESSION
5784N/AbuildConditionalExpression vcc e =
5784N/A let condlist = map (uncurry toIntervalCondition)
5784N/A [c] -> toExp ("impl", c, e)
5784N/A _ -> toExp ("impl", toExp ((), "and", condlist), e)
5784N/AtoIntervalCondition :: (SExp e, IntervalLike i) => e -> i -> EXPRESSION
5784N/AtoIntervalCondition e i = toExp ("in", e, toIntervalExp i)
5784N/A-- | Produces a verification condition for the given Assignment c := t
5784N/AverificationCondition :: ( VarGen c, CalculationSystem c)
5784N/A => EXPRESSION -- ^ the lookuped value of a constant
5784N/A -> EXPRESSION -- ^ the definiens of this constant
5784N/A -> c EXPRESSION -- ^ the conditional statement,
5784N/A -- conditional in occurring interval
5784N/AverificationCondition c e = do
5784N/A (_, vcc1) <- runStateT (replaceIntervals c) emptyVCCache
5784N/A (e', vcc2) <- runStateT (substituteDefined e >>= replaceIntervals')
5784N/A -- 1. c is an interval -> vcc2 => e' in c
5784N/A -- 2. c contains intervals -> error, don't know how to build conditional
5784N/A -- 3. e contains intervals -> error, can't bound interval expression by constant
5784N/A let vericond = toIntervalCondition e' c
5784N/A return $ buildConditionalExpression vcc2 vericond
5784N/A error $ "verificationCondition: don't know how to build conditional"
5784N/A ++ "from interval expression"
5784N/A error $ "verificationCondition: can't bound interval expression by"
5784N/A | otherwise -> return $ toExp ("=", e', c)
5784N/A-- ----------------------------------------------------------------------
5784N/A-- * Transformations for Repeat
5784N/A-- ----------------------------------------------------------------------
5784N/A-- | Transforms a repeat command using the convergence predicate in a repeat
5784N/A-- command where the body and the condition are extended by some intermediate
5784N/A-- variables and their assignments
5784N/AtransRepeat :: VarGen m => EXPRESSION -> [CMD] -> m CMD
5784N/A (l, e') <- transRepeatCondition e
5784N/A let f (v1, v2, tm) = (toCmd (v1, v2), toCmd (v2, tm))
5784N/A return $ Repeat e' $ l1 ++ cl ++ l2
5784N/A-- | Replaces the convergence expressions in the repeat condition using the
5784N/A-- transConvergence function
5784N/AtransRepeatCondition :: VarGen m => EXPRESSION -- ^ The repeat condition
5784N/A -> m ([(String, String, EXPRESSION)], EXPRESSION)
5784N/A -- ^ A list of intermediate convergence vars together
5784N/A -- with the term to converge and the translated repeat
5784N/A Op "convergence" [] [lt, tm] _ -> do
5784N/A return ([(v1, v2, tm)], transConvergence v1 v2 lt)
5784N/A | elem o ["and", "or"] -> do
5784N/A l <- mapM transRepeatCondition al
5784N/A return (concat ssel, Op o [] el rg)
5784N/A | otherwise -> return ([], c)
5784N/A-- | Returns the the program expression for the convergence predicate.
5784N/AtransConvergence :: String -- ^ The variable name to store the preceeding value
5784N/A -> String -- ^ The variable name to store the current value
5784N/A -> EXPRESSION -- ^ The numerical expression for the limit
5784N/A -> EXPRESSION -- ^ A nested if-expression corresponding to the
5784N/A toExp ( "if", ("not", ("numberp", v1)), "false"
5784N/A ,( "if", ("neq", v2, 0::Integer)
5784N/A ,( "<", ("abs", ("/", ("-", v1, v2), v2)), lt)
5784N/A ,( "if", ("eq", v1, 0::Integer), "true", "false")))