smtlib2-1.0: A type-safe interface to communicate with an SMT solver.

Safe HaskellNone
LanguageHaskell98

Language.SMTLib2.Internals.Type.Struct

Documentation

data Tree a Source

Constructors

Leaf a 
Node [Tree a] 

Instances

GCompare k e => GCompare (Tree k) (Struct k e) Source 
GEq k e => GEq (Tree k) (Struct k e) Source 
GShow k e => GShow (Tree k) (Struct k e) Source 

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 k e => GCompare (Tree k) (Struct k e) Source 
GEq k e => GEq (Tree k) (Struct k e) Source 
GShow k e => GShow (Tree k) (Struct k e) Source 
GEq k e => Eq (Struct k e tps) Source 
GCompare k e => Ord (Struct k e tps) Source 
GShow k e => Show (Struct k e tps) Source 

type family Index struct idx :: Tree a Source

Equations

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

type family ElementIndex struct idx :: a Source

Equations

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

type family Insert struct idx el :: Tree a 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 idx :: Tree a 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 :: Nat 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

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

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

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

remove :: Struct e tps -> List Natural idx -> Struct e (Remove tps idx) 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

size :: Struct e tps -> Natural (Size 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