module Language.Boogie.Util (
TypeBinding,
typeSubst,
isFreeIn,
unifier,
oneSidedUnifier,
boundUnifier,
(<==>),
freeVarsTwoState,
freeVars,
freeOldVars,
VarBinding,
exprSubst,
paramSubst,
preconditions,
postconditions,
modifies,
assumePreconditions,
FSig (..),
FDef (..),
PSig (..),
psigParams,
psigArgTypes,
psigRetTypes,
psigModifies,
psigRequires,
psigEnsures,
PDef (..),
num, eneg, enot,
(|+|), (|-|), (|*|), (|/|), (|%|), (|=|), (|!=|), (|<|), (|<=|), (|>|), (|>=|), (|&|), (|||), (|=>|), (|<=>|),
assume,
interval,
fromRight,
mapFst,
mapSnd,
mapBoth,
changeState,
withLocalState
) where
import Language.Boogie.AST
import Language.Boogie.Position
import Language.Boogie.Tokens
import Data.Maybe
import Data.List
import Data.Map (Map)
import qualified Data.Map as M
import Control.Applicative
import Control.Monad.State
type TypeBinding = Map Id Type
typeSubst :: TypeBinding -> Type -> Type
typeSubst _ BoolType = BoolType
typeSubst _ IntType = IntType
typeSubst binding (Instance id []) = case M.lookup id binding of
Just t -> t
Nothing -> Instance id []
typeSubst binding (Instance id args) = Instance id (map (typeSubst binding) args)
typeSubst binding (MapType bv domains range) = MapType bv (map (typeSubst removeBound) domains) (typeSubst removeBound range)
where removeBound = deleteAll bv binding
fromTVNames :: [Id] -> [Id] -> TypeBinding
fromTVNames tvs tvs' = M.fromList (zip tvs (map nullaryType tvs'))
isFreeIn :: Id -> Type -> Bool
x `isFreeIn` (Instance y []) = x == y
x `isFreeIn` (Instance y args) = any (x `isFreeIn`) args
x `isFreeIn` (MapType bv domains range) = x `notElem` bv && any (x `isFreeIn`) (range:domains)
_ `isFreeIn` _ = False
unifier :: [Id] -> [Type] -> [Type] -> Maybe TypeBinding
unifier _ [] [] = Just M.empty
unifier fv (IntType:xs) (IntType:ys) = unifier fv xs ys
unifier fv (BoolType:xs) (BoolType:ys) = unifier fv xs ys
unifier fv ((Instance id1 args1):xs) ((Instance id2 args2):ys) | id1 == id2 = unifier fv (args1 ++ xs) (args2 ++ ys)
unifier fv ((Instance id []):xs) (y:ys) | id `elem` fv =
if id `isFreeIn` y then Nothing
else M.insert id y <$> unifier fv (update xs) (update ys)
where update = map (typeSubst (M.singleton id y))
unifier fv (x:xs) ((Instance id []):ys) | id `elem` fv =
if id `isFreeIn` x then Nothing
else M.insert id x <$> unifier fv (update xs) (update ys)
where update = map (typeSubst (M.singleton id x))
unifier fv ((MapType bv1 domains1 range1):xs) ((MapType bv2 domains2 range2):ys) =
case boundUnifier fv bv1 (range1:domains1) bv2 (range2:domains2) of
Nothing -> Nothing
Just u -> M.union u <$> (unifier fv (update u xs) (update u ys))
where
update u = map (typeSubst u)
unifier _ _ _ = Nothing
removeClashesWith :: [Id] -> [Id] -> [Id]
removeClashesWith tvs tvs' = map freshName tvs
where
freshName tv = if tv `elem` tvs' then replicate (level + 1) nonIdChar ++ tv else tv
level = maximum [fromJust (findIndex (\c -> c /= nonIdChar) id) | id <- tvs']
oneSidedUnifier :: [Id] -> [Type] -> [Id] -> [Type] -> Maybe TypeBinding
oneSidedUnifier fv xs tv ys = M.map old <$> unifier fv xs (map new ys)
where
freshTV = tv `removeClashesWith` fv
new = typeSubst (fromTVNames tv freshTV)
old = typeSubst (fromTVNames freshTV tv)
boundUnifier :: [Id] -> [Id] -> [Type] -> [Id] -> [Type] -> Maybe TypeBinding
boundUnifier fv bv1 xs bv2 ys = if length bv1 /= length bv2 || length xs /= length ys
then Nothing
else case unifier (fv ++ bv1) xs (map withFreshBV ys) of
Nothing -> Nothing
Just u -> if all isFreshBV (M.elems (bound u)) && not (any hasFreshBV (M.elems (free u)))
then Just (free u)
else Nothing
where
freshBV = bv2 `removeClashesWith` bv1
withFreshBV = typeSubst (fromTVNames bv2 freshBV)
isFreshBV (Instance id []) = id `elem` freshBV
isFreshBV _ = False
hasFreshBV t = any (`isFreeIn` t) freshBV
free = deleteAll bv1
bound = deleteAll (fv \\ bv1)
t1 <==> t2 = isJust (unifier [] [t1] [t2])
freeVarsTwoState :: Expression -> ([Id], [Id])
freeVarsTwoState e = freeVarsTwoState' (node e)
freeVarsTwoState' FF = ([], [])
freeVarsTwoState' TT = ([], [])
freeVarsTwoState' (Numeral _) = ([], [])
freeVarsTwoState' (Var x) = ([x], [])
freeVarsTwoState' (Application name args) = mapBoth (nub . concat) (unzip (map freeVarsTwoState args))
freeVarsTwoState' (MapSelection m args) = mapBoth (nub . concat) (unzip (map freeVarsTwoState (m : args)))
freeVarsTwoState' (MapUpdate m args val) = mapBoth (nub . concat) (unzip (map freeVarsTwoState (val : m : args)))
freeVarsTwoState' (Old e) = let (state, old) = freeVarsTwoState e in ([], state ++ old)
freeVarsTwoState' (IfExpr cond e1 e2) = mapBoth (nub . concat) (unzip [freeVarsTwoState cond, freeVarsTwoState e1, freeVarsTwoState e2])
freeVarsTwoState' (Coercion e _) = freeVarsTwoState e
freeVarsTwoState' (UnaryExpression _ e) = freeVarsTwoState e
freeVarsTwoState' (BinaryExpression _ e1 e2) = mapBoth (nub . concat) (unzip [freeVarsTwoState e1, freeVarsTwoState e2])
freeVarsTwoState' (Quantified _ _ boundVars e) = let (state, old) = freeVarsTwoState e in (state \\ map fst boundVars, old)
freeVars = fst . freeVarsTwoState
freeOldVars = snd . freeVarsTwoState
type VarBinding = Map Id BareExpression
exprSubst :: VarBinding -> Expression -> Expression
exprSubst binding (Pos pos e) = attachPos pos $ exprSubst' binding e
exprSubst' binding (Var id) = case M.lookup id binding of
Nothing -> Var id
Just e -> e
exprSubst' binding (Application id args) = Application id (map (exprSubst binding) args)
exprSubst' binding (MapSelection m args) = MapSelection (exprSubst binding m) (map (exprSubst binding) args)
exprSubst' binding (MapUpdate m args val) = MapUpdate (exprSubst binding m) (map (exprSubst binding) args) (exprSubst binding val)
exprSubst' binding (Old e) = Old (exprSubst binding e)
exprSubst' binding (IfExpr cond e1 e2) = IfExpr (exprSubst binding cond) (exprSubst binding e1) (exprSubst binding e2)
exprSubst' binding (Coercion e t) = Coercion (exprSubst binding e) t
exprSubst' binding (UnaryExpression op e) = UnaryExpression op (exprSubst binding e)
exprSubst' binding (BinaryExpression op e1 e2) = BinaryExpression op (exprSubst binding e1) (exprSubst binding e2)
exprSubst' binding (Quantified qop tv boundVars e) = Quantified qop tv boundVars (exprSubst binding' e)
where binding' = deleteAll (map fst boundVars) binding
exprSubst' _ e = e
paramBinding :: PSig -> PDef -> VarBinding
paramBinding sig def = M.fromList $ zip (sigIns ++ sigOuts) (defIns ++ defOuts)
where
sigIns = map itwId $ psigArgs sig
sigOuts = map itwId $ psigRets sig
defIns = map Var $ pdefIns def
defOuts = map Var $ pdefOuts def
paramSubst :: PSig -> PDef -> Expression -> Expression
paramSubst sig def = if not (pdefParamsRenamed def)
then id
else exprSubst (paramBinding sig def)
preconditions :: [Contract] -> [SpecClause]
preconditions specs = catMaybes (map extractPre specs)
where
extractPre (Requires f e) = Just (SpecClause Precondition f e)
extractPre _ = Nothing
postconditions :: [Contract] -> [SpecClause]
postconditions specs = catMaybes (map extractPost specs)
where
extractPost (Ensures f e) = Just (SpecClause Postcondition f e)
extractPost _ = Nothing
modifies :: [Contract] -> [Id]
modifies specs = (nub . concat . catMaybes) (map extractMod specs)
where
extractMod (Modifies _ ids) = Just ids
extractMod _ = Nothing
assumePreconditions :: PSig -> PSig
assumePreconditions sig = sig { psigContracts = map assumePrecondition (psigContracts sig) }
where
assumePrecondition (Requires _ e) = Requires True e
assumePrecondition c = c
data FSig = FSig {
fsigName :: Id,
fsigTypeVars :: [Id],
fsigArgTypes :: [Type],
fsigRetType :: Type
}
data FDef = FDef {
fdefArgs :: [Id],
fdefGuard :: Expression,
fdefBody :: Expression
}
data PSig = PSig {
psigName :: Id,
psigTypeVars :: [Id],
psigArgs :: [IdTypeWhere],
psigRets :: [IdTypeWhere],
psigContracts :: [Contract]
}
psigParams sig = psigArgs sig ++ psigRets sig
psigArgTypes = (map itwType) . psigArgs
psigRetTypes = (map itwType) . psigRets
psigModifies = modifies . psigContracts
psigRequires = preconditions . psigContracts
psigEnsures = postconditions . psigContracts
data PDef = PDef {
pdefIns :: [Id],
pdefOuts :: [Id],
pdefParamsRenamed :: Bool,
pdefBody :: BasicBody,
pdefPos :: SourcePos
}
num i = gen $ Numeral i
eneg e = inheritPos (UnaryExpression Neg) e
enot e = inheritPos (UnaryExpression Not) e
e1 |+| e2 = inheritPos2 (BinaryExpression Plus) e1 e2
e1 |-| e2 = inheritPos2 (BinaryExpression Minus) e1 e2
e1 |*| e2 = inheritPos2 (BinaryExpression Times) e1 e2
e1 |/| e2 = inheritPos2 (BinaryExpression Div) e1 e2
e1 |%| e2 = inheritPos2 (BinaryExpression Mod) e1 e2
e1 |=| e2 = inheritPos2 (BinaryExpression Eq) e1 e2
e1 |!=| e2 = inheritPos2 (BinaryExpression Neq) e1 e2
e1 |<| e2 = inheritPos2 (BinaryExpression Ls) e1 e2
e1 |<=| e2 = inheritPos2 (BinaryExpression Leq) e1 e2
e1 |>| e2 = inheritPos2 (BinaryExpression Gt) e1 e2
e1 |>=| e2 = inheritPos2 (BinaryExpression Geq) e1 e2
e1 |&| e2 = inheritPos2 (BinaryExpression And) e1 e2
e1 ||| e2 = inheritPos2 (BinaryExpression Or) e1 e2
e1 |=>| e2 = inheritPos2 (BinaryExpression Implies) e1 e2
e1 |<=>| e2 = inheritPos2 (BinaryExpression Equiv) e1 e2
assume e = attachPos (position e) (Predicate (SpecClause Inline True e))
interval (lo, hi) = [lo..hi]
fromRight :: Either a b -> b
fromRight (Right x) = x
deleteAll :: Ord k => [k] -> Map k a -> Map k a
deleteAll keys m = foldr M.delete m keys
mapFst f (x, y) = (f x, y)
mapSnd f (x, y) = (x, f y)
mapBoth f (x, y) = (f x, f y)
changeState :: (s -> t) -> (t -> s -> s) -> State t a -> State s a
changeState getter modifier e = do
st <- gets getter
let (res, st') = runState e st
modify $ modifier st'
return res
withLocalState :: (s -> t) -> State t a -> State s a
withLocalState localState e = changeState localState (flip const) e