module Language.Boogie.Heap (
Ref,
refDoc,
Heap,
emptyHeap,
at,
alloc,
hasGarbage,
dealloc,
update,
incRefCount,
decRefCount,
heapDoc
) where
import Language.Boogie.AST
import Language.Boogie.PrettyPrinter
import Language.Boogie.Util
import Data.Map (Map, (!))
import qualified Data.Map as M
import Data.Set (Set)
import qualified Data.Set as S
import Text.PrettyPrint
import Control.Lens hiding (Context, at)
type Ref = Int
refDoc :: Ref -> Doc
refDoc r = text ("ref_" ++ show r)
data Heap a = Heap {
_hValCounts :: Map Ref (a, Int),
_hGarbage :: Set Ref,
_hFree :: Set Ref,
_hFresh :: Ref
} deriving Eq
makeLenses ''Heap
emptyHeap = Heap {
_hValCounts = M.empty,
_hGarbage = S.empty,
_hFree = S.empty,
_hFresh = 0
}
at :: Show a => Heap a -> Ref -> a
at h r = case M.lookup r (h^.hValCounts) of
Nothing -> internalError . show $ text "Cannot find reference" <+> refDoc r <+> text "in heap" $+$ heapDoc h
Just (v, c) -> v
hasGarbage :: Heap a -> Bool
hasGarbage h = h ^. hGarbage . to S.null . to not
alloc :: a -> Heap a -> (Ref, Heap a)
alloc v h = let (r, h') = getFreshRef h in (r, insert r v h')
where
getFreshRef h = if h ^. hFree . to S.null
then let r = h^.hFresh in (r, h & hFresh .~ r + 1)
else let (r, f') = S.deleteFindMin (h^.hFree) in (r, h & hFree .~ f')
insert r v h = h & (over hValCounts (M.insert r (v, 0))) . (over hGarbage (S.insert r))
dealloc :: Heap a -> (Ref, Heap a)
dealloc h = let (r, g') = S.deleteFindMin (h^.hGarbage) in (r,
h & (over hValCounts (M.delete r)) .
(hGarbage .~ g') .
(over hFree (S.insert r))
)
update :: Ref -> a -> Heap a -> Heap a
update r v = over hValCounts (M.adjust (over _1 (const v)) r)
incRefCount :: Ref -> Heap a -> Heap a
incRefCount r h = let (v, c) = (h^.hValCounts) ! r
in h & (over hValCounts (M.insert r (v, c + 1))) .
(over hGarbage (if c == 0 then S.delete r else id)
)
decRefCount :: Ref -> Heap a -> Heap a
decRefCount r h = let (v, c) = (h^.hValCounts) ! r
in h & (over hValCounts (M.insert r (v, c 1))) .
(over hGarbage (if c == 1 then S.insert r else id))
heapDoc :: Show a => Heap a -> Doc
heapDoc h = (vsep $ map entryDoc (M.toList (h^.hValCounts))) $+$
text "Garbage" <+> braces (commaSep (map refDoc (S.toList (h^.hGarbage)))) $+$
text "Free" <+> braces (commaSep (map refDoc (S.toList (h^.hFree))))
where entryDoc (ref, (val, count)) = refDoc ref <> braces (int count) <+> text "->" <+> text (show val)
instance Show a => Show (Heap a) where
show h = show $ heapDoc h