Safe Haskell	None
Language	Haskell98

Language.SMTLib2.Internals.Type.Struct

Documentation

Constructors

Leaf a
Node [Tree a]

Instances

GCompare a e => GCompare (Tree a) (Struct a e) Source #
Methods gcompare :: f a -> f b -> GOrdering (Struct a e) a b #
GEq a e => GEq (Tree a) (Struct a e) Source #
Methods geq :: f a -> f b -> Maybe ((Struct a e := a) b) #
GShow a e => GShow (Tree a) (Struct a e) Source #
Methods gshowsPrec :: Int -> t a -> ShowS #

data Struct e tp where Source #

Constructors

Singleton :: e t -> Struct e (Leaf t)
Struct :: List (Struct e) ts -> Struct e (Node ts)

Instances

GCompare a e => GCompare (Tree a) (Struct a e) Source #
Methods gcompare :: f a -> f b -> GOrdering (Struct a e) a b #
GEq a e => GEq (Tree a) (Struct a e) Source #
Methods geq :: f a -> f b -> Maybe ((Struct a e := a) b) #
GShow a e => GShow (Tree a) (Struct a e) Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
GEq a e => Eq (Struct a e tps) Source #
Methods (==) :: Struct a e tps -> Struct a e tps -> Bool # (/=) :: Struct a e tps -> Struct a e tps -> Bool #
GCompare a e => Ord (Struct a e tps) Source #
Methods compare :: Struct a e tps -> Struct a e tps -> Ordering # (<) :: Struct a e tps -> Struct a e tps -> Bool # (<=) :: Struct a e tps -> Struct a e tps -> Bool # (>) :: Struct a e tps -> Struct a e tps -> Bool # (>=) :: Struct a e tps -> Struct a e tps -> Bool # max :: Struct a e tps -> Struct a e tps -> Struct a e tps # min :: Struct a e tps -> Struct a e tps -> Struct a e tps #
GShow a e => Show (Struct a e tps) Source #
Methods showsPrec :: Int -> Struct a e tps -> ShowS # show :: Struct a e tps -> String # showList :: [Struct a e tps] -> ShowS #

type family Index (struct :: Tree a) (idx :: [Nat]) :: Tree a where ... Source #

Equations

Index x '[] = x
Index (Node xs) (n ': ns) = Index (Index xs n) ns

type family ElementIndex (struct :: Tree a) (idx :: [Nat]) :: a where ... Source #

Equations

ElementIndex (Leaf x) '[] = x
ElementIndex (Node xs) (n ': ns) = ElementIndex (Index xs n) ns

type family Insert (struct :: Tree a) (idx :: [Nat]) (el :: Tree a) :: Tree a where ... Source #

Equations

Insert x '[] y = y
Insert (Node xs) (n ': ns) y = Node (Insert xs n (Insert (Index xs n) ns y))

type family Remove (struct :: Tree a) (idx :: [Nat]) :: Tree a where ... Source #

Equations

Remove (Node xs) '[n] = Node (Remove xs n)
Remove (Node xs) (n1 ': (n2 ': ns)) = Node (Insert xs n1 (Remove (Index xs n1) (n2 ': ns)))

type family Size (struct :: Tree a) :: Nat where ... Source #

Equations

Size (Leaf x) = S Z
Size (Node '[]) = Z
Size (Node (x ': xs)) = Size x + Size (Node xs)

access :: Monad m => Struct e tp -> List Natural idx -> (e (ElementIndex tp idx) -> m (a, e (ElementIndex tp idx))) -> m (a, Struct e tp) Source #

accessElement :: Monad m => Struct e tp -> List Natural idx -> (e (ElementIndex tp idx) -> m (a, e ntp)) -> m (a, Struct e (Insert tp idx (Leaf ntp))) Source #

insert :: Struct e tps -> List Natural idx -> Struct e tp -> Struct e (Insert tps idx tp) Source #

mapM :: Monad m => (forall x. e x -> m (e' x)) -> Struct e tps -> m (Struct e' tps) Source #

mapIndexM :: Monad m => (forall idx. List Natural idx -> e (ElementIndex tps idx) -> m (e' (ElementIndex tps idx))) -> Struct e tps -> m (Struct e' tps) Source #

map :: (forall x. e x -> e' x) -> Struct e tps -> Struct e' tps Source #

flatten :: Monad m => (forall x. e x -> m a) -> ([a] -> m a) -> Struct e tps -> m a Source #

flattenIndex :: Monad m => (forall idx. List Natural idx -> e (ElementIndex tps idx) -> m a) -> ([a] -> m a) -> Struct e tps -> m a Source #

zipWithM :: Monad m => (forall x. e1 x -> e2 x -> m (e3 x)) -> Struct e1 tps -> Struct e2 tps -> m (Struct e3 tps) Source #

zipFlatten :: Monad m => (forall x. e1 x -> e2 x -> m a) -> ([a] -> m a) -> Struct e1 tps -> Struct e2 tps -> m a Source #