Language.SMTLib2.Internals.Type.Struct

Documentation

data Tree a

Constructors

Leaf a

Node [Tree a]

Instances

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

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

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

data Struct e tp where

Constructors

Singleton :: e t -> Struct e (Leaf t)

Struct :: List (Struct e) ts -> Struct e (Node ts)

Instances

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

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

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

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

GCompare k e => Ord (Struct k e tps)

GShow k e => Show (Struct k e tps)

type family Index struct idx :: Tree a

Equations

Index x `[]` = x

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

type family ElementIndex struct idx :: a

Equations

ElementIndex (Leaf x) `[]` = x

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

type family Insert struct idx el :: Tree a

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 idx :: Tree a

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 :: Nat

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