Language.SMTLib2.Internals.Type.Struct

Documentation

data Tree a

Constructors

Leaf a

Node [Tree a]

Instances

GCompare a e => GCompare (Tree a) (Struct a e)

Methods

gcompare :: f a -> f b -> GOrdering (Struct a e) a b

GEq a e => GEq (Tree a) (Struct a e)

Methods

geq :: f a -> f b -> Maybe ((Struct a e := a) b)

GShow a e => GShow (Tree a) (Struct a e)

Methods

gshowsPrec :: Int -> t a -> ShowS

data Struct e tp where

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)

Methods

gcompare :: f a -> f b -> GOrdering (Struct a e) a b

GEq a e => GEq (Tree a) (Struct a e)

Methods

geq :: f a -> f b -> Maybe ((Struct a e := a) b)

GShow a e => GShow (Tree a) (Struct a e)

Methods

gshowsPrec :: Int -> t a -> ShowS

GEq a e => Eq (Struct a e tps)

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)

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)

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 ...

Equations

Index x '[] = x

Index (Node xs) (n ': ns) = Index (Index xs n) ns

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

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 ...

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 ...

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 ...

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)

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)))

index :: Struct e tp -> List Natural idx -> Struct e (Index tp idx)

elementIndex :: Struct e tp -> List Natural idx -> e (ElementIndex tp idx)

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

remove :: Struct e tps -> List Natural idx -> Struct e (Remove tps idx)

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

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

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

size :: Struct e tps -> Natural (Size tps)

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

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

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

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