----------------------------------------------------------------------------- -- | -- Module : Data.SBV.Tools.STree -- Copyright : (c) Levent Erkok -- License : BSD3 -- Maintainer: erkokl@gmail.com -- Stability : experimental -- -- Implementation of full-binary symbolic trees, providing logarithmic -- time access to elements. Both reads and writes are supported. ----------------------------------------------------------------------------- {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} module Data.SBV.Tools.STree (STree, readSTree, writeSTree, mkSTree) where import Data.SBV.Core.Data import Data.SBV.Core.Model import Data.Proxy -- | A symbolic tree containing values of type e, indexed by -- elements of type i. Note that these are full-trees, and their -- their shapes remain constant. There is no API provided that -- can change the shape of the tree. These structures are useful -- when dealing with data-structures that are indexed with symbolic -- values where access time is important. 'STree' structures provide -- logarithmic time reads and writes. type STree i e = STreeInternal (SBV i) (SBV e) -- Internal representation, not exposed to the user data STreeInternal i e = SLeaf e -- NB. parameter 'i' is phantom | SBin (STreeInternal i e) (STreeInternal i e) deriving Show instance SymVal e => Mergeable (STree i e) where symbolicMerge f b (SLeaf i) (SLeaf j) = SLeaf (symbolicMerge f b i j) symbolicMerge f b (SBin l r) (SBin l' r') = SBin (symbolicMerge f b l l') (symbolicMerge f b r r') symbolicMerge _ _ _ _ = error "SBV.STree.symbolicMerge: Impossible happened while merging states" -- | Reading a value. We bit-blast the index and descend down the full tree -- according to bit-values. readSTree :: (SFiniteBits i, SymVal e) => STree i e -> SBV i -> SBV e readSTree s i = walk (blastBE i) s where walk [] (SLeaf v) = v walk (b:bs) (SBin l r) = ite b (walk bs r) (walk bs l) walk _ _ = error $ "SBV.STree.readSTree: Impossible happened while reading: " ++ show i -- | Writing a value, similar to how reads are done. The important thing is that the tree -- representation keeps updates to a minimum. writeSTree :: (SFiniteBits i, SymVal e) => STree i e -> SBV i -> SBV e -> STree i e writeSTree s i j = walk (blastBE i) s where walk [] _ = SLeaf j walk (b:bs) (SBin l r) = SBin (ite b l (walk bs l)) (ite b (walk bs r) r) walk _ _ = error $ "SBV.STree.writeSTree: Impossible happened while reading: " ++ show i -- | Construct the fully balanced initial tree using the given values. mkSTree :: forall i e. HasKind i => [SBV e] -> STree i e mkSTree ivals | isReal (Proxy @i) = error "SBV.STree.mkSTree: Cannot build a real-valued sized tree" | not (isBounded (Proxy @i)) = error "SBV.STree.mkSTree: Cannot build an infinitely large tree" | reqd /= given = error $ "SBV.STree.mkSTree: Required " ++ show reqd ++ " elements, received: " ++ show given | True = go ivals where reqd = 2 ^ intSizeOf (Proxy @i) given = length ivals go [] = error "SBV.STree.mkSTree: Impossible happened, ran out of elements" go [l] = SLeaf l go ns = let (l, r) = splitAt (length ns `div` 2) ns in SBin (go l) (go r)